Zulip Chat Archive

Stream: graph theory

Topic: Triangles

Yaël Dillies (Apr 29 2022 at 20:26):

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 (Apr 29 2022 at 20:35):

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 (Apr 29 2022 at 20:35):

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 (Apr 29 2022 at 20:37):

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 (Apr 29 2022 at 20:37):

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 (Apr 29 2022 at 20:39):

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 (Apr 29 2022 at 20:39):

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

Last updated: Aug 03 2023 at 10:10 UTC