feat(combinatorics/simple_graph/triangle/basic): add ε-triangle-free far graph predicate

[YaelDillies]

Define the property of being triangle-free far. This comes up in the triangle counting and triangle removal lemmas.

Co-authored-by: Bhavik Mehta [email protected]

---

• [x] depends on: #12982
• [x] depends on: #13552

From SRL

[leanprover-community-bot-assistant]

This PR/issue depends on:

• ~~leanprover-community/mathlib#12982~~
• ~~leanprover-community/mathlib#13552~~ By Dependent Issues (🤖). Happy coding!

[kmill]

I mentioned this to Yael already, but I had a couple documentation suggestions in #13726 along with an arguably missing lemma, but the lemma can wait for a future PR if you want.

[kmill]

@robertylewis I had some documentation suggestions in #13726 (a PR targeting this branch), and there's a lemma that would be nice to have (triangle_free_far_iff) since the exact definition of triangle_free_far doesn't match what the docstring says it defines. That part could wait for a future PR though.

It'd be nice to get a better name for triangle_free_far (it still raises mental parse errors for me), and far_from_triangle_free is the best I've heard so far.

[robertylewis]

Oh, I see, the PR to a branch tripped me up -- sorry!

"mental parse error" is a great way to describe how I feel about triangle_free_far :grin:

[collares]

It would be really useful to have a more general definition such as "For some property P, G is t-close to P if there exists a graph H on the same vertex set whose edit distance (cardinality of the symmetric difference of the edge sets) has size at most t". Taking P(G) = G is triangle-free and t = \eps n^2 leads to the definition here. The reason I mention this is because I will use it for P(G) = G is r-partite and t absolute (that is, not multiplied by n^2) for proving Erdős-Simonovits. I can also generalize this definition in a separate PR when the time comes if you prefer.

[YaelDillies]

I made Kyle's characterisation the definition, renamed the predicate to something more human-readable.

I also generalized the predicate, but are you sure this is what you want, @collares? My delete_far is about the difference of edge sets, not the symmetric difference.

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests