Turán's theorem

Stream: mathlib4

[Jeremy Tan]

In the turan branch:

theorem cliqueFree_of_replaceVertex_cliqueFree (s t : V) (h : G.CliqueFree r) :
    (G.replaceVertex s t).CliqueFree r := by
  contrapose h
  obtain ⟨⟨f, hi⟩, ha⟩ := topEmbeddingOfNotCliqueFree h
  simp only [Function.Embedding.coeFn_mk, top_adj, replaceVertex, incidenceSet,
    mem_neighborSet, Set.mem_diff, Set.mem_singleton_iff, Pi.sup_apply, Pi.sdiff_apply,
    Sym2.toRel_prop, Set.mem_setOf_eq, mem_edgeSet, Sym2.mem_iff, Quotient.eq, Sym2.rel_iff,
    ge_iff_le, le_Prop_eq, forall_exists_index, and_imp, sdiff_le_iff, sup_Prop_eq, ne_eq] at ha
  rw [not_cliqueFree_iff]
  by_cases mt : t ∈ Set.range f
  · by_cases ms : s ∈ Set.range f
    · sorry
    · sorry
  · use ⟨f, hi⟩
    simp_all
    intro a b
    rw [← @ha a b]
    have mta := eq_false (mt a)
    rw [@eq_comm _ _ t] at mta
    have mtb := eq_false (mt b)
    rw [@eq_comm _ _ t] at mtb
    simp only [mta, mtb, or_self, and_false, false_and, exists_false, or_false]

After simp only [mta, mtb, or_self, and_false, false_and, exists_false, or_false] I have the goal Adj G (f a) (f b) ↔ Adj G (f a) (f b) \ False which neither aesop or simp or tauto can close. How do I close it?

[Jeremy Tan]

This is part of proving the first step in the "non-adjacency is an equivalence relation" proof, that a graph with more edges can be obtained from a graph with non-adjacent edges of different degrees

[Jeremy Tan]

Or is there a cheaper way to show cliqueFree_of_replaceVertex_cliqueFree?

/-- The graph formed by replacing `t` with a copy of `s`, by changing `t`'s neighbours to match.
The `s-t` edge is removed if present. -/
def replaceVertex (s t : V) : SimpleGraph V where
  Adj := G.Adj \ Sym2.ToRel (G.incidenceSet t) ⊔ Sym2.ToRel {⟦(t, v)⟧ | v ∈ G.neighborSet s \ {t}}
  symm v w := by
    intro h; cases h
    · exact Or.inl (by simpa [adj_comm, Sym2.eq_swap])
    · aesop
  loopless v := by simp only [Set.mem_diff, Pi.sup_apply, Pi.sdiff_apply, SimpleGraph.irrefl,
    Sym2.toRel_prop, Set.mem_setOf_eq, Quotient.eq, Sym2.rel_iff, or_self, exists_eq_right_right,
    le_Prop_eq, sdiff_le_iff, IsEmpty.forall_iff, sup_of_le_right]; tauto

[Kyle Miller]

I think docs#sdiff_bot is supposed to be able to apply, but something's gone wrong and bot became False. I've noticed this sort of thing happening before but didn't investigate.

[Jeremy Tan]

Well a change works, but this branch of the proof looks very unsightly. There must be a better way to rewrite cliqueFree_of_replaceVertex_cliqueFree and/or replaceVertex

/-- Clique-freeness is preserved by `replaceVertex`. -/
theorem cliqueFree_of_replaceVertex_cliqueFree (s t : V) (h : G.CliqueFree r) :
    (G.replaceVertex s t).CliqueFree r := by
  contrapose h
  obtain ⟨⟨f, hi⟩, ha⟩ := topEmbeddingOfNotCliqueFree h
  simp only [Function.Embedding.coeFn_mk, top_adj, replaceVertex, incidenceSet,
    mem_neighborSet, Set.mem_diff, Set.mem_singleton_iff, Pi.sup_apply, Pi.sdiff_apply,
    Sym2.toRel_prop, Set.mem_setOf_eq, mem_edgeSet, Sym2.mem_iff, Quotient.eq, Sym2.rel_iff,
    ge_iff_le, le_Prop_eq, forall_exists_index, and_imp, sdiff_le_iff, sup_Prop_eq, ne_eq] at ha
  rw [not_cliqueFree_iff]
  by_cases mt : t ∈ Set.range f
  · by_cases ms : s ∈ Set.range f
    · sorry
    · sorry
  · use ⟨f, hi⟩
    simp_all only [Set.mem_range, not_exists, Function.Embedding.coeFn_mk, top_adj, ne_eq]
    intro a b
    rw [← @ha a b]
    have mta := eq_false (mt a)
    rw [@eq_comm _ _ t] at mta
    have mtb := eq_false (mt b)
    rw [@eq_comm _ _ t] at mtb
    simp only [mta, mtb, or_self, and_false, false_and, exists_false, or_false]
    change _ ↔ _ \ ⊥
    simp only [sdiff_bot]

[Eric Wieser]

I think we're missing some simp lemmas for the lattice instance on Prop

[Jeremy Tan]

I've completed the proof of cliqueFree_of_vertexReplace_cliqueFree. Now I am at the following sorry:

lemma one (v w : V) (hm : G ∈ turanSet n r) (ha : ¬G.Adj v w) (hd : G.degree v ≠ G.degree w) :
    ¬G.IsTuranMaximal n r := by
  wlog hg : G.degree w < G.degree v generalizing v w
  · rw [adj_comm] at ha
    exact this w v ha hd.symm (hd.lt_or_lt.resolve_right hg)
  clear hd
  simp only [IsTuranMaximal, isMaxOn_iff, not_forall, Function.comp_apply, not_le]
  use G.replaceVertex v w, G.mem_replaceVertex_of_mem_turanSet n r v w hm
  sorry

The goal at the sorry is Set.ncard (edgeSet G) < Set.ncard (edgeSet (replaceVertex G v w)). This seems impenetrable. Is there a way forth?

[Jeremy Tan]

The definition of vertex replacement is now at #6808

[Jeremy Tan]

lemma one says that "if there are two nonadjacent vertices in a clique-free graph with differing degree, I can get a clique-free graph with more edges"

[Jeremy Tan]

Then there will be lemma two: once nonadjacent vertices have the same degree, if three vertices a b c are such that a !~ b (non-adjacent) and b !~c but a ~ c (adjacent), I still can form a clique-free graph with more edges by replacing a c with copies of b