Erdős-Stone-Simonovits

Stream: graph theory

[Mitchell Horner]

Hi all. For my undergrad pure maths honors thesis this year I learnt Lean and formalized the Erdős-Stone-Simonovits theorem writing a thesis about the process. If you care to take a look, the code is here https://github.com/mitchell-horner/ErdosStoneSimonovits. (I don't claim that this is the best way to do it, just a way that very closely mimicked the pen-and-paper proofs I came up with. :sweat_smile:)
I asked my supervisor(s) and looked online to find the various forms the Erdős-Stone-Simonovits theorem comes in and tried to formalize most of them:

• If r, t are natural numbers and ε>0 a real number then there exists N such that all simple graphs with n>N vertices with at least (1-1/r+ε)*n^2/2 edges contain a copy of the complete equi-partite graph K_{r+1}(t) as an isomorphic subgraph.
• If χ(H) = r+1 > 1 and ε>0 a real number then there exists N such that (1-1/r-ε)*n^2/2 < ex(n, H) ≤ (1-1/r+ε)*n^2/2 for all n > N . (ex(n, H) is the extremal number of H with n vertices, χ(H) is the chromatic number of H.)

And the asymptotic varieties:

• If χ(H) = r+1 > 1 then ex(n, H) = (1-1/r+o(1))*n^2/2.
• If χ(H) = r+1 > 1 then π(H) = 1-1/r. (π(H) is the Turán density of H.)
• If χ(H) = r+1 > 2 then ex(n, H) ~ (1-1/r)*(n.choose 2).

I understand that the mathlib library is generally considered for more "fundamental" type results, which might not include extremal combinatorics like the Erdős-Stone-Simonovits theorem (even though this theorem was called the "fundamental" theorem of extremal graph theory by Bollobás :laughing:). However, I think the Bipartite.lean, Extremal.lean, SpecialGraphs.lean, TuranDensity.lean files contain useful results about bipartite graphs for double counting, extremal definitions, definitions about complete equi-partite graphs and results about Turán density that might be "fundamental" enough to include. I'm relatively new so have no clue to the PR process, or if these results would be more appropriate in some dedicated combinatorics library elsewhere. Any suggestions would be appreciated. Thanks.

[Kim Morrison]

@Yaël Dillies will show up shortly with more specific advice (and know what bits exist elsewhere, and where things should go), but:

this is great, and absolutely everything here is clearly "in scope" for Mathlib.

[Kim Morrison]

We have https://leanprover-community.github.io/contribute/index.html as a basic guide for making contributions to Mathlib. But please ask here on zulip for help at any point!

[Mitchell Horner]

Hi hi.

I'm looking for some advice as to where in the mathlib library a few definitions/theorems might be put:

1. for Erdős-Stone I needed complete 'equipartite' graphs $K_\alpha(\beta)$. I initially used completeMultipartiteGraph (const α β) to make use of what already exists in mathlib, but dragging around that constant indexing function is very cumbersome. Instead I used this abbreviation (that is very easily isomorphic to the previous graph):

abbrev completeEquipartiteGraph (α β : Type*) : SimpleGraph (α × β) :=
  SimpleGraph.comap Prod.fst ⊤

I have a few basic results about the degrees of vertices, number of edges, coloring, etc. plus extremal graph theory results about when a graph contains a copy of one of these complete equipartite graphs.
Is there already a place for something like this? (I initially thought to create a SimpleGraphs/SpecialGraphs folder like the Analysis/SpecialFunctions folder.)

2. for a corollary of Erdős-Stone-Simonovits I needed n.choose k = Θ(n^k), I prove it via n.choose k ~ n^k/k! and n.descFactorial k ~ n^k.

I don't see a whole lot of theorems named isTheta_* or isEquivalent_* about specific functions all in the same place, are results like this to be put in a file like Analysis/SpecialFunctions/Choose.lean? (or do these results already exist somewhere?)