Andrasfai-Erdos-Sos theorem

Stream: graph theory

[John Talbot]

@Lian Tattersall and I have formalized the Andrasfai-Erdos-Sos theorem from extremal graph theory:

If $G$ is a $(r+1)$-clique-free graph with $n$ vertices and minimum degree $\delta(G) > (3r -1)n/(3r -4)$ then $G$ is $r$-colorable.

We have a draft PR here: https://github.com/leanprover-community/mathlib4/pull/21127

Our current plan is to split this up into small pieces to submit, starting with minor additions to existing mathlib files.

Any comments/advice would be very helpful!

[Kevin Buzzard]

@Bhavik Mehta this was what you missed at LLL on Friday because you were teaching my Lean course (now referred to as "your lean course") :-)

[John Talbot]

The proof we are following (due to Stefan Brandt) starts by assuming the graph is maximally clique-free, and then splits into cases depending on whether or not the graph is complete-multi-partite.

This led us to introduce two new definitions:

abbrev MaxCliqueFree (G : SimpleGraph α) (r : ℕ) : Prop :=
  Maximal (fun H => H.CliqueFree r) G

abbrev IsCompletePartite (G : SimpleGraph α) : Prop :=
  Transitive (fun u v => ¬G.Adj u v)

Are these reasonable definitions to add to mathlib?

[Mauricio Collares]

I think I've only seen the first one in the proof you're formalizing, but perhaps I'm just forgetting other applications. The second one is very natural, but I'd argue the equivalence between "G is complete partite" and Transitive (fun u v => ¬G.Adj u v) is a theorem.

[John Talbot]

I'll sketch how we use the two definitions below, but if we were going to have our IsCompletePartite definition as a theorem what definition should we be using? (The transitivity of non-adjacency seemed like the most natural definition to us.)

----- Sketch proof

The basic idea in Brandt's proof is that if $G$ is any maximally $K_{r+2}$-free graph, then either $G$ is complete-partite and hence has at most $r+1$ parts, or $G$ contains a 5-wheel-like-subgraph (see below for definition).

Using the definition of IsCompletePartite any non-complete partite graph must contain 3 distinct vertices $v,w_1,w_2$ such that $w_1w_2$ is the only edge induced by $\{v,w_1,w_2\}$.

Since $vw_1$ and $vw_2$ are not edges, the MaxCliqueFree condition implies the existence of sets $s$ and $t$ such that $s \cup \{v\}, s\cup \{w_1\}, t\cup\{v\},t\cup \{w_2\}$ are all $(r+1)$-cliques.

The proof then considers a 5-wheel-like subgraph of $G$, which is the subgraph induced by $s \cup t \cup \{v,w_1,w_2\}$.

For example, if $r = 1$ (triangle-free case) then $s$ and $t$ are disjoint 1-cliques and this subgraph is a copy of $C_5$.

[Mauricio Collares]

John Talbot said:

I'll sketch how we use the two definitions below, but if we were going to have our IsCompletePartite definition as a theorem what definition should we be using? (The transitivity of non-adjacency seemed like the most natural definition to us.)

I was thinking that it would be nice to have a theorem saying "$G$ satisfies Transitive (fun u v => ¬G.Adj u v) iff $G$ is isomorphic to a docs#SimpleGraph.completeMultipartiteGraph". But I think that this theorem would justify using transitivity of non-adjacency as a definition, so I don't have a preference for what the actual def should be.

[Bhavik Mehta]

Yes, I think so too. I would have guessed that being isomorphic to a docs#SimpleGraph.completeMultipartiteGraph is a better definition, but that could create universe issues, so your definition might be nicer here.

[John Talbot]

Thanks! So I've made a draft-PR with our definition but will now try to make the suggested alternative definition work for us: https://github.com/leanprover-community/mathlib4/pull/21293

[Bhavik Mehta]

To be clear, I think the definition in terms of transitive is the correct one, but that we should also have equivalence with the other ones

[John Talbot]

We now have a version of the AES proof that mainly uses facts about completeMultipartiteGraph and has the equivalence:

lemma isCompletePartite_iff : G.IsCompletePartite ↔ ∃ (ι : Type u) (V : ι → Type u)
  (_ : ∀ i, Nonempty (V i)), Nonempty (G ≃g (completeMultipartiteGraph V)) := by

So for example we have:

theorem notCliqueFree_le_card_completeMultipartiteGraph {ι : Type*} [Fintype ι] (V : ι → Type*)
    [∀ i, Nonempty (V i)] (hc : n ≤ Fintype.card ι ) :
  ¬ (completeMultipartiteGraph V).CliqueFree n := by

theorem CompleteMultipartiteGraph.chromaticNumber {ι : Type*} [Fintype ι] (V : ι → Type*)
    [∀ i, Nonempty (V i)] : (completeMultipartiteGraph V).chromaticNumber = Fintype.card ι := by

theorem CompleteMultipartiteGraph.colorable_of_cliqueFree {ι : Type*} {V : ι → Type*}
    [∀ i, Nonempty (V i)] (hc : (completeMultipartiteGraph V).CliqueFree n) :
    (completeMultipartiteGraph V).Colorable (n - 1) := by

https://github.com/leanprover-community/mathlib4/pull/21413

Does this look reasonable?

[Lian Tattersall]

Hi, @John Talbot and I formalised the Andrasfai Erdos Sos theorem:

If $G$ is a $(r+1)$-clique-free graph with $n$ vertices and minimum degree $δ(G)>(3r−1)n/(3r−4)$ then $G$ is $r$-colourable.

Brandt's proof of this theorem involves constructing a supergraph $H$ of $G$ that is maximally $(r + 1)$-clique free and showing that $H$ is $r$ colourable.

To do this in LEAN we used the following lemma to prove that such a supergraph exists. It's slightly more general and replaces being '$(r + 1)$ clique free' with any predicate on graphs with the same vertex set as $G$.

variable {V : Type*} {G : SimpleGraph V} [Fintype V]

/-- If `V` is finite and `P G` holds then there exists a maximal supergraph `H` of `G`
for which `P H` holds. --/
lemma exists_maximal_supergraph (P : SimpleGraph V → Prop) (hG : P G) :
    ∃ H, G ≤ H ∧ Maximal P H :=
  let ⟨_ , ⟨h1, h2⟩, hm⟩ := wellFounded_gt.has_min {H | G ≤ H ∧ P H} ⟨_, ⟨le_rfl, hG⟩⟩
  ⟨_, ⟨h1, h2, fun _ hk hf ↦ (eq_of_ge_of_not_gt hf (hm _ ⟨h1.trans hf, hk⟩)).le⟩⟩

We were wondering if this was something that you wanted to add to mathlib or if we should have it as a private lemma.

Also we were wondering if SimpleGraph V could be replaced with an ordered Fintype
Thanks

[Peter Nelson]

Does docs#Finite.exists_le_maximal give what you want?

[John Talbot]

Yes that is exactly what we should be using, thanks!