Triangles

Stream: graph theory

[Yaël Dillies]

Now that we have two PRs talking about triangles (#12988 and #13758), how should we name the files? I'm happy to go with .triangle.free_far and triangle.free.

[Kyle Miller]

I had been planning on putting the main content of #13758 into combinatorics/simple_graph/triangle/basic.lean once #12988 was merged, but I hadn't really thought about it.

Do you expect there to be a lot more general theory about triangles?

[Mauricio Collares]

Probably I shouldn't opine since I haven't contributed anything yet, but in both cases triangles are just a special case: Saying "G is \eps-far from being H-free" is an useful thing for any H, removal lemmas are useful for any fixed sugraph H and extremal numbers make sense for any H. To prepare for a future where all of these things are proved in more generality, theorems could be structured the other way around (combinatorics.extremal.triangle, combinatorics.removal.triangle and so on).

[Mauricio Collares]

If people want to do everything for triangles first (sounds like a good idea), stability and "supersaturation" for triangles would certainly be interesting.

[Yaël Dillies]

Yes, this is why I am against generalizing triangle-free-far to clique-free-far. For now, because we only have combinatorics.simple_graph (which we could maybe shorten to combinatorics.graph?) anyway, it doesn't make much sense to separate further but I agree.

[Yaël Dillies]

When I first opened #12988, it contained a definition of triangles and the finset of triangles. This really was basic. But those are now about cliques so it doesn't really make sense anymore.

[Yaël Dillies]

For now I suggest

• combinatorics.simple_graph.triangle.free
• combinatorics.simple_graph.triangle.free_far
• combinatorics.simple_graph.triangle.counting
• combinatorics.simple_graph.triangle.removal