diff --git a/LeanPool/RemovalExtremalStability.lean b/LeanPool/RemovalExtremalStability.lean new file mode 100644 index 000000000..7ff481385 --- /dev/null +++ b/LeanPool/RemovalExtremalStability.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ + +module + +public import LeanPool.RemovalExtremalStability.FewCopiesStability + +/-! +# Graph removal and extremal stability + +Source: url:https://github.com/jtraverso/turan-stability +Authors: Juan Pablo Traverso Gianini +Status: verified +Main declarations: `TuranStability.stability`, `RemovalLemma.graph_removal` +Tags: graph-theory, graph-removal, extremal-graph-theory, stability, regularity +MSC: 05C35 +-/ diff --git a/LeanPool/RemovalExtremalStability/CliqueCounting.lean b/LeanPool/RemovalExtremalStability/CliqueCounting.lean new file mode 100644 index 000000000..c72b6268b --- /dev/null +++ b/LeanPool/RemovalExtremalStability/CliqueCounting.lean @@ -0,0 +1,287 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Triangle.Counting +public import Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform +public import Mathlib.Tactic + +/-! + +Adapted from [jtraverso/turan-stability](https://github.com/jtraverso/turan-stability/blob/3eb99033cc931add291781f77b7446dcba8f5f9d/StabilityLib/CliqueCounting.lean) (Palomar-registered source). +# The clique counting lemma + +This file generalises Mathlib's triangle counting lemma (`SimpleGraph.triangle_counting'`, +`SimpleGraph.triangle_counting`) from triangles to cliques of any size `r`. + +The parts are given by a family `s : Fin r → Finset α`. A tuple `x` with `x i ∈ s i` for every +`i` is a *transversal clique* if `G.Adj (x i) (x j)` for all `i ≠ j`. + +* `CliqueCounting.card_transversalCliques_ge`: **counting lemma, robust-density form.** If, for + all `i ≠ j`, every pair of subsets `A ⊆ s i`, `B ⊆ s j` with `#A ≥ η #(s i)` and + `#B ≥ η #(s j)` has edge density at least `d`, `η ≤ 1` and `2 r η ≤ d ^ (r - 1)`, then at least + `d ^ (r choose 2) / 2 ^ r · ∏ i, #(s i)` tuples are transversal cliques. +* `CliqueCounting.card_transversalCliques_ge_of_isUniform`: **counting lemma, uniform form.** The + same conclusion when every pair `(s i, s j)` is `ε`-uniform (`SimpleGraph.IsUniform`) with edge + density at least `d + ε`, and `2 r ε ≤ d ^ (r - 1)`. +* `CliqueCounting.card_cliqueFinset_ge`: **clique counting lemma.** For pairwise disjoint parts + the same lower bound holds for the number of `r`-cliques of `G`, `#(G.cliqueFinset r)`. +-/ + +@[expose] public section + +open Finset Fintype SimpleGraph + +namespace CliqueCounting + +variable {α : Type*} (G : SimpleGraph α) [DecidableRel G.Adj] + +/-- Vertices of `S` with fewer than `d · #T` neighbours in `T` form a set of size `< η · #S`, +provided all large subsets of `S` have density at least `d` to `T`. -/ +theorem card_badVertices_lt {η d : ℝ} (hd : 0 < d) {S T : Finset α} (hT : η * #T ≤ #T) + (h : ∀ A ⊆ S, η * #S ≤ #A → η * #T ≤ #T → d ≤ G.edgeDensity A T) : + (#{x ∈ S | (#{y ∈ T | G.Adj x y} : ℝ) < d * #T} : ℝ) < η * #S := by + classical + by_contra! hle + set B := {x ∈ S | (#{y ∈ T | G.Adj x y} : ℝ) < d * #T} with hB + have h1 := h B (filter_subset _ _) hle hT + rw [edgeDensity_def] at h1 + push_cast at h1 + rcases B.eq_empty_or_nonempty with hBe | hBne + · rw [hBe] at h1; simp at h1; linarith + have hlt : (#(G.interedges B T) : ℝ) < #B * #T * d := by + refine (Nat.cast_le.2 <| (card_le_card <| subset_of_eq (Rel.interedges_eq_biUnion _)).trans + card_biUnion_le).trans_lt ?_ + simp_rw [Nat.cast_sum, card_map] + calc ∑ x ∈ B, (#{y ∈ T | G.Adj x y} : ℝ) < ∑ x ∈ B, d * #T := + sum_lt_sum_of_nonempty hBne fun x hx => (mem_filter.1 hx).2 + _ = _ := by rw [sum_const, nsmul_eq_mul]; ring + have hTpos : (0 : ℝ) < #T := by + rcases Nat.eq_zero_or_pos #T with h0 | h0 + · rw [h0, Nat.cast_zero, mul_zero, zero_mul] at hlt + exact absurd hlt (not_lt.2 (Nat.cast_nonneg _)) + · exact_mod_cast h0 + have hBpos : (0 : ℝ) < #B := by exact_mod_cast hBne.card_pos + rw [le_div_iff₀ (by positivity)] at h1 + linarith + +/-- The statement of the counting lemma for `r` parts, with the extra hypothesis `η ≤ 1`. -/ +def CountingStatement (r : ℕ) : Prop := + ∀ (s : Fin r → Finset α) (η d : ℝ), 0 < η → η ≤ 1 → 0 < d → 2 * r * η ≤ d ^ (r - 1) → + (∀ i j, i ≠ j → ∀ A ⊆ s i, ∀ B ⊆ s j, η * #(s i) ≤ #A → η * #(s j) ≤ #B → + d ≤ G.edgeDensity A B) → + d ^ r.choose 2 / 2 ^ r * ∏ i, (#(s i) : ℝ) ≤ + #{x ∈ Fintype.piFinset s | ∀ i j, i ≠ j → G.Adj (x i) (x j)} + +theorem countingStatement_of_le_one {r : ℕ} (hr : r ≤ 1) : CountingStatement G r := by + intro s η d _ _ _ _ _ + have hsub : ∀ i j : Fin r, i = j := fun i j => by ext; omega + rw [filter_true_of_mem fun x _ i j hij => absurd (hsub i j) hij, card_piFinset, + Nat.choose_eq_zero_of_lt (by omega)] + push_cast + have hP : (0 : ℝ) ≤ ∏ i, (#(s i) : ℝ) := by positivity + have : (1 : ℝ) / 2 ^ r ≤ 1 := by + rw [div_le_one (by positivity)]; exact one_le_pow₀ (by norm_num) + rw [pow_zero] + nlinarith + +theorem countingStatement_succ {r : ℕ} (hr : 1 ≤ r) (ih : CountingStatement G r) : + CountingStatement G (r + 1) := by + classical + obtain ⟨k, rfl⟩ : ∃ k, r = k + 1 := ⟨r - 1, by omega⟩ + intro s η d hη hη1 hd hηd hs + simp only [Nat.add_sub_cancel] at hηd ih ⊢ + push_cast at hηd + set j1 : Fin (k + 1 + 1) := ⟨1, by omega⟩ + have hd1 : d ≤ 1 := + (hs 0 j1 (by simp [j1]) _ subset_rfl _ subset_rfl + (mul_le_of_le_one_left (Nat.cast_nonneg _) hη1) + (mul_le_of_le_one_left (Nat.cast_nonneg _) hη1)).trans + (by exact_mod_cast edgeDensity_le_one _ _ _) + have hdk : d ^ k ≤ 1 := pow_le_one₀ hd.le hd1 + have hdk1 : d ^ (k + 1) = d * d ^ k := by ring + have hrη : ((k : ℝ) + 1) * η ≤ 1 / 2 := by nlinarith + -- bad vertices + let Bad : Fin (k + 1) → Finset α := fun i => + {x ∈ s 0 | (#{y ∈ s i.succ | G.Adj x y} : ℝ) < d * #(s i.succ)} + have hBad : ∀ i, (#(Bad i) : ℝ) < η * #(s 0) := fun i => + card_badVertices_lt G hd (mul_le_of_le_one_left (Nat.cast_nonneg _) hη1) + fun A hA hA' hT => hs 0 i.succ (Fin.succ_ne_zero i).symm A hA _ subset_rfl hA' hT + let X := (s 0).filter (fun x => ∀ i, x ∉ Bad i) + have hX : (#(s 0) : ℝ) / 2 ≤ #X := by + have hsub : s 0 ⊆ X ∪ univ.biUnion Bad := by + intro x hx + by_cases h : ∀ i, x ∉ Bad i + · exact mem_union_left _ (mem_filter.2 ⟨hx, h⟩) + · push Not at h + obtain ⟨i, hi⟩ := h + exact mem_union_right _ (mem_biUnion.2 ⟨i, mem_univ _, hi⟩) + have h1 : (#(s 0) : ℝ) ≤ #X + ∑ i, (#(Bad i) : ℝ) := by + have := (card_le_card hsub).trans ((card_union_le _ _).trans + (Nat.add_le_add_left card_biUnion_le _)) + exact_mod_cast this + have h2 : ∑ i, (#(Bad i) : ℝ) ≤ ∑ _i : Fin (k + 1), η * #(s 0) := + sum_le_sum fun i _ => (hBad i).le + rw [sum_const, card_univ, Fintype.card_fin, nsmul_eq_mul] at h2 + push_cast at h2 + have : (0 : ℝ) ≤ #(s 0) := Nat.cast_nonneg _ + nlinarith + -- neighbourhoods + let s' : α → Fin (k + 1) → Finset α := fun x i => {y ∈ s i.succ | G.Adj x y} + let C' : α → Finset (Fin (k + 1) → α) := fun x => + {t ∈ Fintype.piFinset (s' x) | ∀ i j, i ≠ j → G.Adj (t i) (t j)} + have hC' : ∀ x ∈ X, d ^ (k + 1).choose 2 / 2 ^ (k + 1) * + (d ^ (k + 1) * ∏ i : Fin (k + 1), (#(s i.succ) : ℝ)) ≤ #(C' x) := by + intro x hx + have hx' := (mem_filter.1 hx).2 + have hs'card : ∀ i, d * #(s i.succ) ≤ #(s' x i) := fun i => by + have := hx' i + simp only [Bad, mem_filter, not_and, not_lt] at this + exact this (mem_filter.1 hx).1 + have hη' : 2 * ((k : ℝ) + 1) * (η / d) ≤ d ^ k := by + rw [mul_div_assoc', div_le_iff₀ hd]; nlinarith + have hη'1 : η / d ≤ 1 := by + have : (0 : ℝ) ≤ k := Nat.cast_nonneg _ + have : 0 < η / d := div_pos hη hd + nlinarith + have := ih (s' x) (η / d) d (div_pos hη hd) hη'1 hd (by push_cast; exact hη') (by + intro i j hij A hA B hB hA' hB' + refine hs i.succ j.succ ((Fin.succ_injective _).ne hij) A + (hA.trans (filter_subset _ _)) B (hB.trans (filter_subset _ _)) ?_ ?_ + · calc η * (#(s i.succ) : ℝ) = η / d * (d * #(s i.succ)) := by field_simp + _ ≤ η / d * #(s' x i) := by gcongr; exact hs'card i + _ ≤ _ := hA' + · calc η * (#(s j.succ) : ℝ) = η / d * (d * #(s j.succ)) := by field_simp + _ ≤ η / d * #(s' x j) := by gcongr; exact hs'card j + _ ≤ _ := hB') + refine le_trans ?_ this + gcongr + calc d ^ (k + 1) * ∏ i : Fin (k + 1), (#(s i.succ) : ℝ) + = ∏ i : Fin (k + 1), (d * #(s i.succ)) := by + rw [prod_mul_distrib, prod_const, card_univ, Fintype.card_fin] + _ ≤ _ := prod_le_prod₀ (fun i _ => mul_nonneg hd.le (Nat.cast_nonneg _)) fun i _ => hs'card i + -- prepend + have hinj : #(X.sigma C') ≤ + #{x ∈ Fintype.piFinset s | ∀ i j, i ≠ j → G.Adj (x i) (x j)} := by + refine card_le_card_of_injOn (fun p => Fin.cons p.1 p.2) ?_ ?_ + · rintro ⟨x, t⟩ hp + simp only [coe_sigma, Set.mem_sigma_iff, mem_coe] at hp + obtain ⟨hx, ht⟩ := hp + simp only [C', mem_filter, Fintype.mem_piFinset, s'] at ht + obtain ⟨ht1, ht2⟩ := ht + simp only [coe_filter, Set.mem_ofPred_eq, Fintype.mem_piFinset] + refine ⟨fun i => Fin.cases (mem_filter.1 hx).1 (fun i => (ht1 i).1) i, ?_⟩ + intro i j hij + induction i using Fin.cases with + | zero => + induction j using Fin.cases with + | zero => exact absurd rfl hij + | succ j => simpa using (ht1 j).2 + | succ i => + induction j using Fin.cases with + | zero => simpa using ((ht1 i).2).symm + | succ j => simpa using ht2 i j fun h => hij (by rw [h]) + · rintro ⟨x, t⟩ _ ⟨y, u⟩ _ h + simp only [Fin.cons_inj] at h + obtain ⟨rfl, rfl⟩ := h + rfl + rw [Finset.card_sigma] at hinj + have hsum : ∑ x ∈ X, d ^ (k + 1).choose 2 / 2 ^ (k + 1) * + (d ^ (k + 1) * ∏ i : Fin (k + 1), (#(s i.succ) : ℝ)) ≤ ∑ x ∈ X, (#(C' x) : ℝ) := + sum_le_sum hC' + rw [sum_const, nsmul_eq_mul] at hsum + have hfin := (Nat.cast_le (α := ℝ)).2 hinj + rw [Nat.cast_sum] at hfin + refine le_trans ?_ (hsum.trans hfin) + rw [Fin.prod_univ_succ, Nat.choose_succ_succ (k + 1) 1, Nat.choose_one_right] + have hK : (0 : ℝ) ≤ d ^ (k + 1).choose 2 / 2 ^ (k + 1) * + (d ^ (k + 1) * ∏ i : Fin (k + 1), (#(s i.succ) : ℝ)) := + mul_nonneg (div_nonneg (pow_nonneg hd.le _) (pow_nonneg zero_le_two _)) + (mul_nonneg (pow_nonneg hd.le _) (prod_nonneg fun i _ => Nat.cast_nonneg _)) + calc d ^ (k + 1 + (k + 1).choose 2) / 2 ^ (k + 1 + 1) * + ((#(s 0) : ℝ) * ∏ i : Fin (k + 1), (#(s i.succ) : ℝ)) + = (#(s 0) : ℝ) / 2 * (d ^ (k + 1).choose 2 / 2 ^ (k + 1) * + (d ^ (k + 1) * ∏ i : Fin (k + 1), (#(s i.succ) : ℝ))) := by ring + _ ≤ _ := mul_le_mul_of_nonneg_right hX hK + +theorem countingStatement (r : ℕ) : CountingStatement G r := by + rcases Nat.lt_or_ge r 1 with hr | hr + · exact countingStatement_of_le_one G (by omega) + induction r, hr using Nat.le_induction with + | base => exact countingStatement_of_le_one G le_rfl + | succ r hr ih => exact countingStatement_succ G hr ih + + +/-- **Clique counting lemma, robust-density form.** If any two of the parts `s i`, `s j` +(`i ≠ j`) have edge density at least `d` between all subsets of relative size at least `η`, +`η ≤ 1` and `2 r η ≤ d ^ (r - 1)`, then at least `d ^ (r choose 2) / 2 ^ r` of the tuples in +`∏ i, s i` are cliques. (Without `η ≤ 1` the hypothesis on subsets would be vacuous.) -/ +theorem card_transversalCliques_ge {r : ℕ} (s : Fin r → Finset α) {η d : ℝ} (hη : 0 < η) + (hη₁ : η ≤ 1) (hd : 0 < d) (hηd : 2 * r * η ≤ d ^ (r - 1)) + (hs : ∀ i j, i ≠ j → ∀ A ⊆ s i, ∀ B ⊆ s j, η * #(s i) ≤ #A → η * #(s j) ≤ #B → + d ≤ G.edgeDensity A B) : + d ^ r.choose 2 / 2 ^ r * ∏ i, (#(s i) : ℝ) ≤ + #{x ∈ Fintype.piFinset s | ∀ i j, i ≠ j → G.Adj (x i) (x j)} := + countingStatement G r s η d hη hη₁ hd hηd hs + +/-- **Clique counting lemma, uniform form.** If every pair of distinct parts is `ε`-uniform with +edge density at least `d + ε`, and `2 r ε ≤ d ^ (r - 1)`, then at least +`d ^ (r choose 2) / 2 ^ r` of the tuples in `∏ i, s i` are cliques. -/ +theorem card_transversalCliques_ge_of_isUniform {r : ℕ} (s : Fin r → Finset α) {ε d : ℝ} + (hε : 0 < ε) (hd : 0 < d) (hεd : 2 * r * ε ≤ d ^ (r - 1)) + (hu : ∀ i j, i ≠ j → G.IsUniform ε (s i) (s j)) + (hdens : ∀ i j, i ≠ j → d + ε ≤ G.edgeDensity (s i) (s j)) : + d ^ r.choose 2 / 2 ^ r * ∏ i, (#(s i) : ℝ) ≤ + #{x ∈ Fintype.piFinset s | ∀ i j, i ≠ j → G.Adj (x i) (x j)} := by + refine card_transversalCliques_ge G s (η := min ε 1) (lt_min hε one_pos) + (min_le_right _ _) hd + ((mul_le_mul_of_nonneg_left (min_le_left _ _) (by positivity)).trans hεd) + ?_ + intro i j hij A hA B hB hA' hB' + have h1 := hdens i j hij + have h2 : (G.edgeDensity (s i) (s j) : ℝ) ≤ 1 := by exact_mod_cast edgeDensity_le_one _ _ _ + rw [min_eq_left (by linarith)] at hA' hB' + have := hu i j hij hA hB (by rw [mul_comm]; exact hA') (by rw [mul_comm]; exact hB') + rw [abs_sub_lt_iff] at this + linarith + +/-- **Clique counting lemma.** If `s : Fin r → Finset α` are pairwise disjoint sets of vertices, +every two of them `ε`-uniform with edge density at least `d + ε`, and `2 r ε ≤ d ^ (r - 1)`, +then `G` has at least `d ^ (r choose 2) / 2 ^ r · ∏ i, #(s i)` cliques of size `r`. -/ +theorem card_cliqueFinset_ge [Fintype α] [DecidableEq α] {r : ℕ} (s : Fin r → Finset α) + {ε d : ℝ} (hε : 0 < ε) (hd : 0 < d) (hεd : 2 * r * ε ≤ d ^ (r - 1)) + (hdisj : ∀ i j, i ≠ j → Disjoint (s i) (s j)) + (hu : ∀ i j, i ≠ j → G.IsUniform ε (s i) (s j)) + (hdens : ∀ i j, i ≠ j → d + ε ≤ G.edgeDensity (s i) (s j)) : + d ^ r.choose 2 / 2 ^ r * ∏ i, (#(s i) : ℝ) ≤ #(G.cliqueFinset r) := by + refine (card_transversalCliques_ge_of_isUniform G s hε hd hεd hu hdens).trans ?_ + have key : ∀ x ∈ Fintype.piFinset s, ∀ i j, x i = x j → i = j := by + intro x hx i j hij + by_contra h + rw [Fintype.mem_piFinset] at hx + exact disjoint_left.1 (hdisj i j h) (hx i) (hij ▸ hx j) + exact_mod_cast card_le_card_of_injOn (fun x => univ.image x) (by + intro x hx + simp only [coe_filter, Set.mem_ofPred_eq] at hx + obtain ⟨hx, hadj⟩ := hx + simp only [coe_cliqueFinset] + refine (isNClique_iff G).2 ⟨?_, ?_⟩ + · rw [isClique_iff, coe_image] + rintro _ ⟨i, -, rfl⟩ _ ⟨j, -, rfl⟩ hne + exact hadj i j fun h => hne (by rw [h]) + · rw [card_image_of_injective _ fun i j h => key x hx i j h, card_univ, Fintype.card_fin]) (by + intro x hx y hy hxy + simp only [coe_filter, Set.mem_ofPred_eq, Fintype.mem_piFinset] at hx hy + funext i + have : x i ∈ univ.image y := by + simp only at hxy; rw [← hxy]; exact mem_image_of_mem _ (mem_univ _) + obtain ⟨j, -, hj⟩ := mem_image.1 this + obtain rfl : j = i := by + by_contra h + exact disjoint_left.1 (hdisj j i h) (hy.1 j) (hj ▸ hx.1 i) + exact hj.symm) + +end CliqueCounting diff --git a/LeanPool/RemovalExtremalStability/CliqueRemoval.lean b/LeanPool/RemovalExtremalStability/CliqueRemoval.lean new file mode 100644 index 000000000..ab8d48fbd --- /dev/null +++ b/LeanPool/RemovalExtremalStability/CliqueRemoval.lean @@ -0,0 +1,235 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Triangle.Removal +public import Mathlib.Tactic +public import LeanPool.RemovalExtremalStability.CliqueCounting + +/-! + +Adapted from [jtraverso/turan-stability](https://github.com/jtraverso/turan-stability/blob/3eb99033cc931add291781f77b7446dcba8f5f9d/StabilityLib/CliqueRemoval.lean) (Palomar-registered source). +# The clique removal lemma + +This file generalises Mathlib's triangle removal lemma (`SimpleGraph.triangle_removal`, +`SimpleGraph.FarFromTriangleFree.le_card_cliqueFinset`) from triangles to cliques of any size `r`, +using Szemerédi's regularity lemma (`SzemerediRegularity`, `szemeredi_regularity`), Mathlib's +reduced graph `SimpleGraph.regularityReduced` and the clique counting lemma +`CliqueCounting.card_cliqueFinset_ge`. + +* `CliqueRemoval.le_card_cliqueFinset_of_deleteFar`: **clique removal lemma, far form.** For every + `r` and `ε > 0` there is `δ > 0` such that every finite graph from which one must delete at least + `ε n²` edges to destroy all `r`-cliques has at least `δ n^r` cliques of size `r`. +* `CliqueRemoval.clique_removal`: **clique removal lemma.** For every `r` and `ε > 0` there is + `δ > 0` such that every finite graph on `n` vertices with fewer than `δ n^r` cliques of size `r` + can be made `K_r`-free by deleting fewer than `ε n²` edges. +-/ + +@[expose] public section + +open Finset Fintype SimpleGraph + +namespace CliqueRemoval + +variable {α : Type*} [DecidableEq α] [Fintype α] {G : SimpleGraph α} [DecidableRel G.Adj] + {P : Finpartition (univ : Finset α)} + +/-- Arithmetic helper: `n < 2 k (n / k)` when `0 < k ≤ n`. -/ +theorem aux_lt_two_mul {n k : ℕ} (hk : 0 < k) (hn : k ≤ n) : n < 2 * k * (n / k) := by + rw [mul_assoc, two_mul, ← add_lt_add_iff_right (n % k), add_right_comm, add_assoc, + Nat.mod_add_div n k, add_comm, add_lt_add_iff_right] + apply (Nat.mod_lt n hk).trans_le + simpa using Nat.mul_le_mul_left k ((Nat.one_le_div_iff hk).2 hn) + +/-- Parts of an equipartition with at most `B` parts have size at least `card α / (2 B)`. -/ +theorem card_bound {B : ℕ} {s : Finset α} (hP₁ : P.IsEquipartition) (hP₃ : #P.parts ≤ B) + (hX : s ∈ P.parts) : card α / (2 * B : ℝ) ≤ #s := by + cases isEmpty_or_nonempty α + · simp [Fintype.card_eq_zero] + have := Finset.Nonempty.card_pos ⟨_, hX⟩ + calc + _ ≤ card α / (2 * #P.parts : ℝ) := by gcongr + _ ≤ ↑(card α / #P.parts) := + (div_le_iff₀' (by positivity)).2 <| mod_cast (aux_lt_two_mul ‹_› P.card_parts_le_card).le + _ ≤ (#s : ℝ) := mod_cast hP₁.average_le_card_part hX + +/-- Generalisation of `SimpleGraph.unreduced_edges_subset` to arbitrary parameters. -/ +theorem unreduced_edges_subset' {η δ : ℝ} : + (univ ×ˢ univ).filter (fun (x, y) ↦ G.Adj x y ∧ ¬ (G.regularityReduced P η δ).Adj x y) ⊆ + (P.nonUniforms G η).biUnion (fun (U, V) ↦ U ×ˢ V) ∪ P.parts.biUnion offDiag ∪ + (P.sparsePairs G δ).biUnion fun (U, V) ↦ G.interedges U V := by + rintro ⟨x, y⟩ + simp only [mem_filter, regularityReduced_adj, not_and, not_exists, + not_le, mem_biUnion, mem_union, mem_product, Prod.exists, mem_offDiag, and_imp, + or_assoc, and_assoc, P.mk_mem_nonUniforms, Finpartition.mk_mem_sparsePairs, mem_interedges_iff] + intro hx hy h h' + replace h' := h' h + obtain ⟨U, hU, hx⟩ := P.exists_mem hx + obtain ⟨V, hV, hy⟩ := P.exists_mem hy + obtain rfl | hUV := eq_or_ne U V + · exact Or.inr (Or.inl ⟨U, hU, hx, hy, G.ne_of_adj h⟩) + by_cases h₂ : G.IsUniform η U V + · exact Or.inr <| Or.inr ⟨U, V, hU, hV, hUV, h' _ hU _ hV hx hy hUV h₂, hx, hy, h⟩ + · exact Or.inl ⟨U, V, hU, hV, hUV, h₂, hx, hy⟩ + +/-- Generalisation of `SimpleGraph.regularityReduced_edges_card_aux` to a uniformity parameter +`η ≤ ε / 8`. -/ +theorem regularityReduced_edges_card_aux' [Nonempty α] {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) + (hηε : η ≤ ε / 8) (hP : P.IsEquipartition) + (hPε : P.IsUniform G η) (hP' : 4 / ε ≤ #P.parts) : + (#G.edgeFinset - #(G.regularityReduced P η (ε / 4)).edgeFinset : ℝ) + < ε * (card α ^ 2 : ℕ) := by + let A := (P.nonUniforms G η).biUnion fun (U, V) ↦ U ×ˢ V + let B := P.parts.biUnion offDiag + let C := (P.sparsePairs G (ε / 4)).biUnion fun (U, V) ↦ G.interedges U V + suffices h : 2 * (#G.edgeFinset - #(G.regularityReduced P η (ε / 4)).edgeFinset : ℝ) + < 2 * ε * (card α ^ 2 : ℕ) by linarith + calc + _ = (#((univ ×ˢ univ).filter fun (x, y) ↦ + G.Adj x y ∧ ¬(G.regularityReduced P η (ε / 4)).Adj x y) : ℝ) := by + rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff] + · norm_cast + rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset] + · gcongr with xy _ + exact fun hxy ↦ regularityReduced_le hxy + _ ≤ (#(A ∪ B ∪ C) : ℝ) := by + exact_mod_cast card_le_card (unreduced_edges_subset' (G := G) (P := P) (η := η) (δ := ε / 4)) + _ ≤ #(A ∪ B) + #C := mod_cast (card_union_le _ _) + _ ≤ #A + #B + #C := by gcongr; exact mod_cast card_union_le _ _ + _ < 4 * η * card α ^ 2 + _ + _ := by + gcongr; exact hP.sum_nonUniforms_lt univ_nonempty hη hPε + _ ≤ 4 * (ε / 8) * card α ^ 2 + ε / 2 * card α ^ 2 + 4 * (ε / 4) * card α ^ 2 := by + gcongr + · exact hP.card_biUnion_offDiag_le hε hP' + · exact hP.card_interedges_sparsePairs_le (G := G) (ε := ε / 4) (by positivity) + _ = 2 * ε * (card α ^ 2 : ℕ) := by push_cast; ring + +/-- An `r`-clique of the reduced graph yields many `r`-cliques of `G`. -/ +theorem card_cliqueFinset_ge_of_mem_reduced {r B : ℕ} {ε η d : ℝ} (hη : 0 < η) (hd : 0 < d) + (hηd : 2 * r * η ≤ d ^ (r - 1)) (hdη : d + η ≤ ε / 4) (hP₁ : P.IsEquipartition) + (hP₃ : #P.parts ≤ B) {t : Finset α} + (ht : (G.regularityReduced P η (ε / 4)).IsNClique r t) : + d ^ r.choose 2 / 2 ^ r * (card α / (2 * B : ℝ)) ^ r ≤ #(G.cliqueFinset r) := by + let e := t.equivFin + let v : Fin r → α := fun i ↦ (e.symm (Fin.cast ht.card_eq.symm i) : α) + have hv : ∀ i j, i ≠ j → (G.regularityReduced P η (ε / 4)).Adj (v i) (v j) := by + intro i j hij + refine ht.isClique (e.symm _).2 (e.symm _).2 ?_ + intro h + apply hij + have := e.symm.injective (Subtype.ext h) + exact Fin.cast_injective _ this + let U : Fin r → Finset α := fun i ↦ P.part (v i) + have key : ∀ i j, i ≠ j → U i ∈ P.parts ∧ U j ∈ P.parts ∧ U i ≠ U j ∧ + G.IsUniform η (U i) (U j) ∧ ε / 4 ≤ G.edgeDensity (U i) (U j) := by + intro i j hij + obtain ⟨-, X, hX, Y, hY, hxX, hyY, hXY, hu, hdens⟩ := hv i j hij + have h1 : U i = X := P.part_eq_of_mem hX hxX + have h2 : U j = Y := P.part_eq_of_mem hY hyY + rw [h1, h2] + exact ⟨hX, hY, hXY, hu, hdens⟩ + have hcount := CliqueCounting.card_cliqueFinset_ge G U hη hd hηd + (fun i j hij ↦ by + obtain ⟨h1, h2, h3, -⟩ := key i j hij + exact P.disjoint h1 h2 h3) + (fun i j hij ↦ (key i j hij).2.2.2.1) + (fun i j hij ↦ hdη.trans (key i j hij).2.2.2.2) + refine le_trans ?_ hcount + gcongr + calc + (card α / (2 * B : ℝ)) ^ r = ∏ _i : Fin r, (card α / (2 * B : ℝ)) := by + rw [prod_const, card_univ, Fintype.card_fin] + _ ≤ ∏ i, (#(U i) : ℝ) := by + gcongr with i + exact card_bound hP₁ hP₃ (P.part_mem.2 (mem_univ _)) + +/-- **Clique removal lemma, far form.** For every `r` and `ε > 0` there is `δ > 0` such that a +finite graph on `n` vertices that is `ε n²`-far from being `K_r`-free (in the sense of Mathlib's +`SimpleGraph.DeleteFar`) has at least `δ n^r` cliques of size `r`. -/ +theorem le_card_cliqueFinset_of_deleteFar (r : ℕ) {ε : ℝ} (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∀ (α : Type) [Fintype α] [DecidableEq α] (G : SimpleGraph α) + [DecidableRel G.Adj], G.DeleteFar (fun H ↦ H.CliqueFree r) (ε * (card α ^ 2 : ℕ)) → + δ * card α ^ r ≤ #(G.cliqueFinset r) := by + classical + obtain rfl | hr := Nat.eq_zero_or_pos r + · refine ⟨1, one_pos, fun α _ _ G _ _ ↦ ?_⟩ + have : 0 < #(G.cliqueFinset 0) := card_pos.2 ⟨∅, by simp⟩ + simp only [pow_zero, mul_one, Nat.one_le_cast] + exact this + set d : ℝ := ε / 8 with hd_def + have hd : 0 < d := by positivity + set η : ℝ := min (ε / 8) (d ^ (r - 1) / (2 * r + 1)) with hη_def + have hη : 0 < η := lt_min (by positivity) (by positivity) + have hηε : η ≤ ε / 8 := min_le_left _ _ + have hηd : 2 * r * η ≤ d ^ (r - 1) := by + have h1 : η ≤ d ^ (r - 1) / (2 * r + 1) := min_le_right _ _ + have hp : 0 < d ^ (r - 1) := by positivity + rw [le_div_iff₀ (by positivity)] at h1 + nlinarith + have hdη : d + η ≤ ε / 4 := by linarith + set l : ℕ := ⌈4 / ε⌉₊ with hl_def + have hl : 4 / ε ≤ l := Nat.le_ceil _ + set B : ℕ := SzemerediRegularity.bound η l with hB_def + have hB : (0 : ℝ) < B := by positivity + set δ : ℝ := min 1 (min (1 / (2 * (l + 1) ^ r)) (d ^ r.choose 2 / 2 ^ r * (1 / (2 * B)) ^ r)) + with hδ_def + have hδ1 : δ ≤ 1 / (2 * (l + 1) ^ r) := (min_le_right _ _).trans (min_le_left _ _) + have hδ2 : δ ≤ d ^ r.choose 2 / 2 ^ r * (1 / (2 * B)) ^ r := + (min_le_right _ _).trans (min_le_right _ _) + refine ⟨δ, by positivity, fun α _ _ G _ hG ↦ ?_⟩ + have hδ0 : 0 ≤ δ := by positivity + obtain hn | hn := Nat.eq_zero_or_pos (card α) + · rw [hn, Nat.cast_zero, zero_pow hr.ne', mul_zero] + positivity + have hnc : ¬ G.CliqueFree r := by + intro h + have := hG (s := ∅) (empty_subset _) (by simpa only [coe_empty, deleteEdges_empty] using h) + rw [Finset.card_empty, Nat.cast_zero] at this + have : (0 : ℝ) < ε * (card α ^ 2 : ℕ) := by positivity + linarith + rcases le_total (card α) l with hl' | hl' + · obtain ⟨t, ht⟩ : ∃ t, G.IsNClique r t := by + simpa [CliqueFree] using hnc + have h1 : (1 : ℝ) ≤ #(G.cliqueFinset r) := by + exact_mod_cast card_pos.2 ⟨t, mem_cliqueFinset_iff.2 ht⟩ + calc δ * card α ^ r ≤ 1 / (2 * (l + 1) ^ r) * (l + 1) ^ r := by + gcongr + exact_mod_cast hl'.trans (Nat.le_succ l) + _ = 1 / 2 := by field_simp + _ ≤ _ := by linarith + · have : Nonempty α := Fintype.card_pos_iff.1 hn + obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := szemeredi_regularity G hη hl' + have hP' : 4 / ε ≤ #P.parts := hl.trans (Nat.cast_le.2 hP₂) + have k := regularityReduced_edges_card_aux' hε hη hηε hP₁ hP₄ hP' + have hnc' : ¬ (G.regularityReduced P η (ε / 4)).CliqueFree r := by + intro h + have := (deleteFar_iff.1 hG) regularityReduced_le h + linarith + obtain ⟨t, ht⟩ : ∃ t, (G.regularityReduced P η (ε / 4)).IsNClique r t := by + simpa [CliqueFree] using hnc' + have := card_cliqueFinset_ge_of_mem_reduced hη hd hηd hdη hP₁ hP₃ ht + calc δ * card α ^ r ≤ d ^ r.choose 2 / 2 ^ r * (1 / (2 * B)) ^ r * card α ^ r := by + gcongr + _ = d ^ r.choose 2 / 2 ^ r * (card α / (2 * B : ℝ)) ^ r := by + rw [div_pow, div_pow, div_pow, one_pow]; ring + _ ≤ _ := this + +/-- **Clique removal lemma.** For every `r` and `ε > 0` there is `δ > 0` such that every finite +graph on `n` vertices with fewer than `δ n^r` cliques of size `r` has a `K_r`-free subgraph +obtained by deleting fewer than `ε n²` edges. -/ +theorem clique_removal (r : ℕ) {ε : ℝ} (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∀ (α : Type) [Fintype α] [DecidableEq α] (G : SimpleGraph α) + [DecidableRel G.Adj], (#(G.cliqueFinset r) : ℝ) < δ * card α ^ r → + ∃ G' ≤ G, ∃ _ : DecidableRel G'.Adj, + (#G.edgeFinset - #G'.edgeFinset : ℝ) < ε * (card α ^ 2 : ℕ) ∧ G'.CliqueFree r := by + obtain ⟨δ, hδ, h⟩ := le_card_cliqueFinset_of_deleteFar r hε + refine ⟨δ, hδ, fun α _ _ G _ hG ↦ ?_⟩ + by_contra! h' + refine hG.not_ge (h α G (deleteFar_iff.2 ?_)) + intro G' _ hG' hG'' + exact le_of_not_gt fun i ↦ h' G' hG' _ i hG'' + +end CliqueRemoval diff --git a/LeanPool/RemovalExtremalStability/Embedding.lean b/LeanPool/RemovalExtremalStability/Embedding.lean new file mode 100644 index 000000000..7d479b1b5 --- /dev/null +++ b/LeanPool/RemovalExtremalStability/Embedding.lean @@ -0,0 +1,196 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform +public import Mathlib.Combinatorics.SimpleGraph.Copy +public import Mathlib.Tactic +public import LeanPool.RemovalExtremalStability.CliqueCounting +public import LeanPool.RemovalExtremalStability.PartialEmbedding + +/-! + +Adapted from [jtraverso/turan-stability](https://github.com/jtraverso/turan-stability/blob/3eb99033cc931add291781f77b7446dcba8f5f9d/StabilityLib/Embedding.lean) (Palomar-registered source). +# The embedding lemma + +Let `L` be a finite graph on `k` vertices with a proper colouring `c` by `r` colours, and let +`s : Fin r → Finset α` be parts of a graph `G` that are pairwise dense in a robust sense (or +pairwise `ε`-uniform and dense). Then `L` embeds into `G` with every vertex `x` of `L` mapped into +the part `s (c x)`. This is the "key lemma" of the regularity method, proved by greedy embedding. + +* `Embedding.exists_embedding`: **embedding lemma, robust-density form.** +* `Embedding.exists_embedding_of_isUniform`: **embedding lemma, uniform form.** +* `Embedding.isContained_of_isUniform`: in the uniform setting, `L ⊑ G`. +-/ + +@[expose] public section + +open Finset Fintype SimpleGraph + +namespace Embedding + +variable {α : Type*} (G : SimpleGraph α) [DecidableRel G.Adj] + +/-- **Embedding lemma, robust-density form.** Let `L` be a graph on a finite type `β` with +`k = card β` vertices and a proper colouring `c : β → Fin r`. Suppose that for all colours +`i ≠ j`, all subsets `A ⊆ s i`, `B ⊆ s j` with `#A ≥ η #(s i)` and `#B ≥ η #(s j)` have edge +density at least `d`, where `0 < η ≤ 1`, `0 < d ≤ 1`, `2 k η ≤ d ^ k`, and every part has at least +`2 k / d ^ k` vertices. Then there is an injective map `f : β → α` sending each `x` into `s (c x)` +and edges of `L` to edges of `G`. -/ +theorem exists_embedding {β : Type*} [Fintype β] (L : SimpleGraph β) {r : ℕ} + (c : β → Fin r) (hc : ∀ x y, L.Adj x y → c x ≠ c y) (s : Fin r → Finset α) {η d : ℝ} + (hη : 0 < η) (hη₁ : η ≤ 1) (hd : 0 < d) (hd₁ : d ≤ 1) + (hηd : 2 * card β * η ≤ d ^ card β) (hsize : ∀ i, 2 * card β ≤ d ^ card β * #(s i)) + (hs : ∀ i j, i ≠ j → ∀ A ⊆ s i, ∀ B ⊆ s j, η * #(s i) ≤ #A → η * #(s j) ≤ #B → + d ≤ G.edgeDensity A B) : + ∃ f : β → α, Function.Injective f ∧ (∀ x, f x ∈ s (c x)) ∧ + ∀ x y, L.Adj x y → G.Adj (f x) (f y) := by + classical + rcases isEmpty_or_nonempty β with hβ | hβ + · exact ⟨isEmptyElim, fun a => isEmptyElim a, fun a => isEmptyElim a, fun a => isEmptyElim a⟩ + have hk1 : (1 : ℝ) ≤ card β := by exact_mod_cast Fintype.card_pos + have hD : 0 < d ^ card β := pow_pos hd _ + have hηD : η ≤ d ^ card β := by nlinarith + let Cand : (β → α) → Finset β → β → Finset α := fun f S y => + {w ∈ s (c y) | ∀ z ∈ S, L.Adj z y → G.Adj (f z) w} + have hCandEq : ∀ f S y, + Cand f S y = PartialEmbedding.candidates G L (fun y => s (c y)) f S y := by + intros f S y + ext w + simp [Cand, PartialEmbedding.candidates] + let P : Finset β → Prop := fun S => ∃ f : β → α, Set.InjOn f S ∧ (∀ x ∈ S, f x ∈ s (c x)) ∧ + (∀ x ∈ S, ∀ y ∈ S, L.Adj x y → G.Adj (f x) (f y)) ∧ + ∀ y ∉ S, d ^ #S * #(s (c y)) ≤ #(Cand f S y) + have hP : ∀ S, P S := by + intro S + induction S using Finset.induction_on with + | empty => + obtain ⟨b⟩ := hβ + have hne : (s (c b)).Nonempty := by + rw [← Finset.card_pos] + by_contra h + have := hsize (c b) + rw [Nat.eq_zero_of_not_pos h] at this + simp at this + linarith + obtain ⟨a, -⟩ := hne + refine ⟨fun _ => a, by simp, by simp, by simp, fun y _ => ?_⟩ + simp [Cand] + | insert x S hxS ih => + obtain ⟨f, hinj, hmem, hadj, hcand⟩ := ih + have hSk : #S + 1 ≤ card β := by + have := card_le_univ (insert x S); rwa [card_insert_of_notMem hxS] at this + have hpowS : d ^ card β ≤ d ^ #S := pow_le_pow_of_le_one hd.le hd₁ (by omega) + have hCand_big : ∀ y ∉ S, d ^ card β * #(s (c y)) ≤ #(Cand f S y) := fun y hy => + (mul_le_mul_of_nonneg_right hpowS (Nat.cast_nonneg _)).trans (hcand y hy) + let Y := (univ \ insert x S).filter (L.Adj x) + let Bad : β → Finset α := fun y => + {v ∈ s (c x) | (#{w ∈ Cand f S y | G.Adj v w} : ℝ) < d * #(Cand f S y)} + have hBad : ∀ y ∈ Y, (#(Bad y) : ℝ) < η * #(s (c x)) := by + intro y hy + simp only [Y, mem_filter, mem_sdiff, mem_univ, true_and, mem_insert, not_or] at hy + refine CliqueCounting.card_badVertices_lt G hd + (mul_le_of_le_one_left (Nat.cast_nonneg _) hη₁) fun A hA hA' _ => + hs (c x) (c y) (hc x y hy.2) A hA _ (filter_subset _ _) hA' ?_ + refine le_trans ?_ (hCand_big y hy.1.2) + gcongr + have hYcard : #Y + #S + 1 ≤ card β := by + have h1 : #Y ≤ #(univ \ insert x S) := card_filter_le _ _ + rw [card_sdiff_of_subset (subset_univ _), card_insert_of_notMem hxS, card_univ] at h1 + omega + let Good := (Cand f S x).filter (fun v => v ∉ S.image f ∧ ∀ y ∈ Y, v ∉ Bad y) + have hGood : Good.Nonempty := by + by_contra hne + rw [not_nonempty_iff_eq_empty] at hne + have hsub : Cand f S x ⊆ S.image f ∪ Y.biUnion Bad := by + intro v hv + by_contra hv' + simp only [mem_union, not_or, mem_biUnion, not_exists, not_and] at hv' + have : v ∈ Good := mem_filter.2 ⟨hv, hv'.1, fun y hy => hv'.2 y hy⟩ + rw [hne] at this; simp at this + have h1 : (#(Cand f S x) : ℝ) ≤ #S + ∑ y ∈ Y, (#(Bad y) : ℝ) := by + have := (card_le_card hsub).trans ((card_union_le _ _).trans + (Nat.add_le_add card_image_le card_biUnion_le)) + exact_mod_cast this + have h2 : ∑ y ∈ Y, (#(Bad y) : ℝ) ≤ #Y * (η * #(s (c x))) := by + rw [← nsmul_eq_mul, ← sum_const]; exact sum_le_sum fun y hy => (hBad y hy).le + have h3 := hCand_big x hxS + have h4 := hsize (c x) + have h5 : ((#Y : ℕ) : ℝ) + #S + 1 ≤ card β := by exact_mod_cast hYcard + set N : ℝ := (#(s (c x)) : ℝ) + set D := d ^ card β + have hN : 0 ≤ N := Nat.cast_nonneg _ + have hY0 : (0 : ℝ) ≤ #Y := Nat.cast_nonneg _ + have hS0 : (0 : ℝ) ≤ #S := Nat.cast_nonneg _ + have e1 : 2 * card β * (#Y * (η * N)) ≤ #Y * (D * N) := by + have := mul_le_mul_of_nonneg_right hηd hN + nlinarith + have e2 : 2 * card β * (#S : ℝ) ≤ #S * (D * N) := by nlinarith + have e3 : (#Y + #S : ℝ) * (D * N) < 2 * card β * (D * N) := by + have : 0 < D * N := by nlinarith + nlinarith + nlinarith + obtain ⟨v, hv⟩ := hGood + obtain ⟨hvC, hvS, hvB⟩ := mem_filter.1 hv + have hvC' := mem_filter.1 hvC + have hgood : ∀ y, y ∉ insert x S → L.Adj x y → + d * #(Cand f S y) ≤ #{w ∈ Cand f S y | G.Adj v w} := by + intro y hy hxy + have hyY : y ∈ Y := by simp [Y, hy, hxy] + exact le_of_not_gt fun h => hvB y hyY (mem_filter.2 ⟨hvC'.1, h⟩) + have hcandShared : ∀ y ∉ S, d ^ #S * #(s (c y)) ≤ + #(PartialEmbedding.candidates G L (fun y => s (c y)) f S y) := by + simpa only [← hCandEq] using hcand + have hvCShared : v ∈ PartialEmbedding.candidates G L (fun y => s (c y)) f S x := by + simpa only [← hCandEq] using hvC + have hgoodShared : ∀ y, y ∉ insert x S → L.Adj x y → + d * #(PartialEmbedding.candidates G L (fun y => s (c y)) f S y) ≤ + #{w ∈ PartialEmbedding.candidates G L (fun y => s (c y)) f S y | G.Adj v w} := by + simpa only [← hCandEq] using hgood + obtain ⟨hinj', hmem', hadj', hcand'⟩ := + PartialEmbedding.extend G L (fun y => s (c y)) hd hd₁ S x hxS f v + hinj hmem hadj hcandShared hvCShared hvS hgoodShared + exact ⟨Function.update f x v, hinj', hmem', hadj', by simpa only [← hCandEq] using hcand'⟩ + obtain ⟨f, hinj, hmem, hadj, -⟩ := hP univ + exact ⟨f, fun a b h => hinj (mem_coe.2 (mem_univ a)) (mem_univ b) h, + fun x => hmem x (mem_univ x), fun x y h => hadj x (mem_univ x) y (mem_univ y) h⟩ + +/-- **Embedding lemma, uniform form.** Under the hypotheses of `exists_embedding`, with the +robust density condition replaced by: every pair of distinct parts is `ε`-uniform with edge +density at least `d + ε`, and `2 k ε ≤ d ^ k`. -/ +theorem exists_embedding_of_isUniform {β : Type*} [Fintype β] + (L : SimpleGraph β) {r : ℕ} (c : β → Fin r) (hc : ∀ x y, L.Adj x y → c x ≠ c y) + (s : Fin r → Finset α) {ε d : ℝ} (hε : 0 < ε) (hd : 0 < d) (hd₁ : d ≤ 1) + (hεd : 2 * card β * ε ≤ d ^ card β) (hsize : ∀ i, 2 * card β ≤ d ^ card β * #(s i)) + (hu : ∀ i j, i ≠ j → G.IsUniform ε (s i) (s j)) + (hdens : ∀ i j, i ≠ j → d + ε ≤ G.edgeDensity (s i) (s j)) : + ∃ f : β → α, Function.Injective f ∧ (∀ x, f x ∈ s (c x)) ∧ + ∀ x y, L.Adj x y → G.Adj (f x) (f y) := by + refine exists_embedding G L c hc s (η := min ε 1) (lt_min hε one_pos) (min_le_right _ _) hd hd₁ + ((mul_le_mul_of_nonneg_left (min_le_left _ _) (by positivity)).trans hεd) hsize ?_ + intro i j hij A hA B hB hA' hB' + have h1 := hdens i j hij + have h2 : (G.edgeDensity (s i) (s j) : ℝ) ≤ 1 := by exact_mod_cast edgeDensity_le_one _ _ _ + rw [min_eq_left (by linarith)] at hA' hB' + have := hu i j hij hA hB (by rw [mul_comm]; exact hA') (by rw [mul_comm]; exact hB') + rw [abs_sub_lt_iff] at this + linarith + +/-- **Embedding lemma, containment form.** Under the hypotheses of +`exists_embedding_of_isUniform`, `L` is contained in `G` (`L ⊑ G`, Mathlib's +`SimpleGraph.IsContained`). -/ +theorem isContained_of_isUniform {β : Type*} [Fintype β] + (L : SimpleGraph β) {r : ℕ} (c : β → Fin r) (hc : ∀ x y, L.Adj x y → c x ≠ c y) + (s : Fin r → Finset α) {ε d : ℝ} (hε : 0 < ε) (hd : 0 < d) (hd₁ : d ≤ 1) + (hεd : 2 * card β * ε ≤ d ^ card β) (hsize : ∀ i, 2 * card β ≤ d ^ card β * #(s i)) + (hu : ∀ i j, i ≠ j → G.IsUniform ε (s i) (s j)) + (hdens : ∀ i j, i ≠ j → d + ε ≤ G.edgeDensity (s i) (s j)) : + L.IsContained G := by + obtain ⟨f, hinj, -, hadj⟩ := + exists_embedding_of_isUniform G L c hc s hε hd hd₁ hεd hsize hu hdens + exact ⟨Hom.toCopy (⟨f, fun h => hadj _ _ h⟩ : L →g G) hinj⟩ + +end Embedding diff --git a/LeanPool/RemovalExtremalStability/FewCopiesStability.lean b/LeanPool/RemovalExtremalStability/FewCopiesStability.lean new file mode 100644 index 000000000..06619e9d5 --- /dev/null +++ b/LeanPool/RemovalExtremalStability/FewCopiesStability.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.RemovalExtremalStability.TuranStability +public import LeanPool.RemovalExtremalStability.GraphRemoval + +/-! +# Stability with few forbidden copies + +This combines the graph removal lemma with Erdős–Simonovits stability. The graph is allowed to +contain a small positive density of labelled copies of the forbidden graph. +-/ + +@[expose] public section + +open Finset Fintype SimpleGraph + +namespace RemovalExtremalStability + +/-- If `H` is `(p + 1)`-colourable, a graph with nearly the Turán number of edges and sufficiently +few labelled copies of `H` is close to a complete `p`-partite graph. -/ +theorem stability_of_few_copies {β : Type} [Fintype β] (H : SimpleGraph β) {p : ℕ} + (hp : 0 < p) (hH : H.Colorable (p + 1)) {ε : ℝ} (hε : 0 < ε) : + ∃ δ η : ℝ, 0 < δ ∧ 0 < η ∧ ∃ n₀ : ℕ, + ∀ (W : Type) [Fintype W] [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj], + n₀ ≤ card W → + (G.labelledCopyCount H : ℝ) < η * card W ^ card β → + (1 - 1 / (p : ℝ)) * (card W : ℝ) ^ 2 / 2 - δ * (card W : ℝ) ^ 2 ≤ + G.edgeSet.ncard → + ∃ f : W → Fin p, + ((symmDiff G ((⊤ : SimpleGraph (Fin p)).comap f)).edgeSet.ncard : ℝ) ≤ + ε * (card W : ℝ) ^ 2 := by + classical + obtain ⟨δ₀, hδ₀, n₀, hstab⟩ := TuranStability.stability H hp hH (half_pos hε) + let ξ : ℝ := min (δ₀ / 2) (ε / 2) + have hξ : 0 < ξ := lt_min (half_pos hδ₀) (half_pos hε) + obtain ⟨η, hη, hrem⟩ := RemovalLemma.graph_removal H hξ + refine ⟨δ₀ / 2, η, half_pos hδ₀, hη, n₀, ?_⟩ + intro W _ _ G _ hn hcopies hedges + obtain ⟨G', hsub, _, hdelete, hfree⟩ := hrem W G hcopies + have he : G.edgeSet.ncard = #G.edgeFinset := by + rw [← Set.ncard_coe_finset, coe_edgeFinset] + have he' : G'.edgeSet.ncard = #G'.edgeFinset := by + rw [← Set.ncard_coe_finset, coe_edgeFinset] + rw [← he, ← he'] at hdelete + have hcard : G'.edgeSet.ncard ≤ G.edgeSet.ncard := + Set.ncard_le_ncard (edgeSet_mono hsub) (Set.toFinite _) + have hdiff : ((G.edgeSet.ncard - G'.edgeSet.ncard : ℕ) : ℝ) < + ξ * (card W : ℝ) ^ 2 := by + rw [Nat.cast_sub hcard] + simpa only [Nat.cast_pow] using hdelete + have hedges' : + (1 - 1 / (p : ℝ)) * (card W : ℝ) ^ 2 / 2 - δ₀ * (card W : ℝ) ^ 2 ≤ + G'.edgeSet.ncard := by + have hξδ : ξ ≤ δ₀ / 2 := min_le_left _ _ + have hn2 : (0 : ℝ) ≤ (card W : ℝ) ^ 2 := sq_nonneg _ + rw [Nat.cast_sub hcard] at hdiff + nlinarith + obtain ⟨f, hf⟩ := hstab W G' hn (by exact hfree) hedges' + refine ⟨f, ?_⟩ + have hdist := ErdosSimonovits.ncard_symmDiff_le hsub + ((⊤ : SimpleGraph (Fin p)).comap f) + have hξε : ξ ≤ ε / 2 := min_le_right _ _ + have hn2 : (0 : ℝ) ≤ (card W : ℝ) ^ 2 := sq_nonneg _ + have hdist' : + ((symmDiff G ((⊤ : SimpleGraph (Fin p)).comap f)).edgeSet.ncard : ℝ) ≤ + ((symmDiff G' ((⊤ : SimpleGraph (Fin p)).comap f)).edgeSet.ncard : ℝ) + + ((G.edgeSet.ncard - G'.edgeSet.ncard : ℕ) : ℝ) := by + exact_mod_cast hdist + nlinarith + +end RemovalExtremalStability diff --git a/LeanPool/RemovalExtremalStability/Furedi.lean b/LeanPool/RemovalExtremalStability/Furedi.lean new file mode 100644 index 000000000..e428480f9 --- /dev/null +++ b/LeanPool/RemovalExtremalStability/Furedi.lean @@ -0,0 +1,288 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Extremal.Turan +public import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex +public import Mathlib.Tactic + +/-! + +Adapted from [jtraverso/turan-stability](https://github.com/jtraverso/turan-stability/blob/3eb99033cc931add291781f77b7446dcba8f5f9d/StabilityLib/Furedi.lean) (Palomar-registered source). +# Füredi's stability theorem for Turán's theorem + +For a finite simple graph `G` and a map `f : V → Fin p`, the graph +`(⊤ : SimpleGraph (Fin p)).comap f` is the complete `p`-partite graph whose parts are the fibres +of `f`; `G \ (⊤.comap f)` consists of the edges of `G` inside the parts. + +* `Furedi.card_edgeSet_add_le`: **Füredi (2015), partition inequality.** If `G` is + `K_{p+1}`-free, there is a partition `f` with `e(G) + Σᵢ e(G[Vᵢ]) ≤ e(K(V₁, …, V_p))`. +* `Furedi.furedi`: **Füredi (2015).** A `K_{p+1}`-free graph with at least + `turanNumber n p - t` edges has a `p`-partite subgraph with at least `e(G) - t` edges. +* `Furedi.exists_partition_symmDiff_le`: such a graph is at edit distance at most `3 t` from a + complete `p`-partite graph, with at most `t` edges inside the parts. +* `Furedi.erdos_simonovits_stability`: **Erdős–Simonovits stability for cliques.** For every + `ε > 0` there is `δ > 0` such that every `K_{p+1}`-free graph with at least + `(1 - 1/p) n² / 2 - δ n²` edges can be turned into a complete `p`-partite graph by changing + at most `ε n²` edges. +-/ + +@[expose] public section + +open Finset Fintype SimpleGraph + +namespace Furedi + +variable {V : Type*} [Fintype V] + +section Aux + +variable {W : Type*} (G : SimpleGraph W) [DecidableRel G.Adj] + +/-- Ordered count of `G`-edges plus `G`-edges inside fibres of `f`, within `S`. -/ +def lhsCount (S : Finset W) (f : W → ℕ) : ℕ := + ∑ u ∈ S, ∑ v ∈ S, ((if G.Adj u v then 1 else 0) + (if G.Adj u v ∧ f u = f v then 1 else 0)) + +/-- Ordered count of pairs in `S` with different `f`-values. -/ +def rhsCount (S : Finset W) (f : W → ℕ) : ℕ := + ∑ u ∈ S, ∑ v ∈ S, if f u ≠ f v then 1 else 0 + +lemma key_ineq (p : ℕ) : ∀ S : Finset W, (∀ t ⊆ S, ¬ G.IsNClique (p + 1) t) → + ∃ f : W → ℕ, (∀ w ∈ S, f w < p) ∧ lhsCount G S f ≤ rhsCount S f := by + induction p with + | zero => + intro S hS + have hSe : S = ∅ := by + by_contra h + obtain ⟨a, ha⟩ := Finset.nonempty_iff_ne_empty.mpr h + exact hS {a} (by simpa using ha) (isNClique_one.mpr ⟨a, rfl⟩) + subst hSe + exact ⟨fun _ => 0, by simp, by simp [lhsCount, rhsCount]⟩ + | succ p ih => + intro S hS + rcases S.eq_empty_or_nonempty with hSe | hSne + · subst hSe + exact ⟨fun _ => 0, by simp, by simp [lhsCount, rhsCount]⟩ + classical + obtain ⟨x, hxS, hxmax⟩ := Finset.exists_max_image S + (fun u => ∑ v ∈ S, if G.Adj u v then 1 else 0) hSne + set N := S.filter (G.Adj x) with hN + set V₁ := S.filter (fun w => ¬ G.Adj x w) with hV₁ + have hNcl : ∀ t ⊆ N, ¬ G.IsNClique (p + 1) t := by + intro t ht hcl + have hxt : x ∉ t := fun h => by + have := (Finset.mem_filter.mp (ht h)).2 + exact G.loopless.irrefl x this + refine hS (insert x t) ?_ (hcl.insert fun b hb => (Finset.mem_filter.mp (ht hb)).2) + intro y hy + rcases Finset.mem_insert.mp hy with rfl | hy + · exact hxS + · exact (Finset.mem_filter.mp (ht hy)).1 + obtain ⟨g, hg, hgle⟩ := ih N hNcl + refine ⟨fun w => if G.Adj x w then g w + 1 else 0, ?_, ?_⟩ + · intro w hw + by_cases h : G.Adj x w + · simp only [h, ite_true] + have := hg w (Finset.mem_filter.mpr ⟨hw, h⟩) + omega + · simp [h] + set f : W → ℕ := fun w => if G.Adj x w then g w + 1 else 0 with hf + have fN : ∀ u ∈ N, f u = g u + 1 := fun u hu => by + simp [hf, (Finset.mem_filter.mp hu).2] + have fV : ∀ u ∈ V₁, f u = 0 := fun u hu => by + simp [hf, (Finset.mem_filter.mp hu).2] + have split1 : ∀ F : W → ℕ, ∑ v ∈ S, F v = ∑ v ∈ N, F v + ∑ v ∈ V₁, F v := + fun F => (sum_filter_add_sum_filter_not _ _ _).symm + have split2 : ∀ F : W → W → ℕ, ∑ u ∈ S, ∑ v ∈ S, F u v = + ∑ u ∈ N, ∑ v ∈ N, F u v + ∑ u ∈ N, ∑ v ∈ V₁, F u v + + ∑ u ∈ V₁, ∑ v ∈ N, F u v + ∑ u ∈ V₁, ∑ v ∈ V₁, F u v := by + intro F + calc ∑ u ∈ S, ∑ v ∈ S, F u v = ∑ u ∈ S, (∑ v ∈ N, F u v + ∑ v ∈ V₁, F u v) := + sum_congr rfl fun u _ => split1 _ + _ = _ := by rw [split1]; simp only [sum_add_distrib]; ring + let A : W → W → ℕ := fun u v => if G.Adj u v then 1 else 0 + have hNN : ∑ u ∈ N, ∑ v ∈ N, ((if G.Adj u v then 1 else 0) + + (if G.Adj u v ∧ f u = f v then 1 else 0)) = lhsCount G N g := by + unfold lhsCount + refine sum_congr rfl fun u hu => sum_congr rfl fun v hv => ?_ + rw [fN u hu, fN v hv]; simp + have hNV : ∑ u ∈ N, ∑ v ∈ V₁, ((if G.Adj u v then 1 else 0) + + (if G.Adj u v ∧ f u = f v then 1 else 0)) = ∑ u ∈ N, ∑ v ∈ V₁, A u v := by + refine sum_congr rfl fun u hu => sum_congr rfl fun v hv => ?_ + rw [fN u hu, fV v hv]; simp [A] + have hVN : ∑ u ∈ V₁, ∑ v ∈ N, ((if G.Adj u v then 1 else 0) + + (if G.Adj u v ∧ f u = f v then 1 else 0)) = ∑ u ∈ V₁, ∑ v ∈ N, A u v := by + refine sum_congr rfl fun u hu => sum_congr rfl fun v hv => ?_ + rw [fV u hu, fN v hv]; simp [A] + have hVV : ∑ u ∈ V₁, ∑ v ∈ V₁, ((if G.Adj u v then 1 else 0) + + (if G.Adj u v ∧ f u = f v then 1 else 0)) = 2 * ∑ u ∈ V₁, ∑ v ∈ V₁, A u v := by + rw [mul_sum] + refine sum_congr rfl fun u hu => ?_ + rw [mul_sum] + refine sum_congr rfl fun v hv => ?_ + rw [fV u hu, fV v hv]; simp [A]; split_ifs <;> simp + have hNVc : ∑ u ∈ N, ∑ v ∈ V₁, A u v = ∑ u ∈ V₁, ∑ v ∈ N, A u v := by + rw [sum_comm] + exact sum_congr rfl fun u _ => sum_congr rfl fun v _ => by simp [A, G.adj_comm] + have hdeg : ∑ u ∈ V₁, ∑ v ∈ N, A u v + ∑ u ∈ V₁, ∑ v ∈ V₁, A u v ≤ #V₁ * #N := by + rw [← sum_add_distrib] + have : ∀ u ∈ V₁, ∑ v ∈ N, A u v + ∑ v ∈ V₁, A u v ≤ #N := by + intro u hu + rw [← split1 (A u), hN, card_filter] + exact hxmax u (Finset.mem_filter.mp hu).1 + calc _ ≤ ∑ u ∈ V₁, #N := sum_le_sum this + _ = _ := by simp + have rNN : ∑ u ∈ N, ∑ v ∈ N, (if f u ≠ f v then 1 else 0) = rhsCount N g := by + unfold rhsCount + refine sum_congr rfl fun u hu => sum_congr rfl fun v hv => ?_ + rw [fN u hu, fN v hv]; simp + have rNV : ∑ u ∈ N, ∑ v ∈ V₁, (if f u ≠ f v then 1 else 0) = #N * #V₁ := by + rw [card_eq_sum_ones, sum_mul] + refine sum_congr rfl fun u hu => ?_ + rw [one_mul, card_eq_sum_ones] + refine sum_congr rfl fun v hv => ?_ + rw [fN u hu, fV v hv]; simp + have rVN : ∑ u ∈ V₁, ∑ v ∈ N, (if f u ≠ f v then 1 else 0) = #V₁ * #N := by + rw [card_eq_sum_ones, sum_mul] + refine sum_congr rfl fun u hu => ?_ + rw [one_mul, card_eq_sum_ones] + refine sum_congr rfl fun v hv => ?_ + rw [fV u hu, fN v hv]; simp + have rVV : ∑ u ∈ V₁, ∑ v ∈ V₁, (if f u ≠ f v then 1 else 0) = 0 := by + refine sum_eq_zero fun u hu => sum_eq_zero fun v hv => ?_ + rw [fV u hu, fV v hv]; simp + change lhsCount G S f ≤ rhsCount S f + unfold lhsCount rhsCount + rw [split2, split2 (fun u v => if f u ≠ f v then 1 else 0), hNN, hNV, hVN, hVV, rNN, rNV, + rVN, rVV, hNVc] + rw [mul_comm #N] + linarith + +end Aux + +lemma two_mul_ncard_edgeSet {W : Type*} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] : + 2 * H.edgeSet.ncard = ∑ u, ∑ v, if H.Adj u v then 1 else 0 := by + classical + rw [← coe_edgeFinset, Set.ncard_coe_finset, ← sum_degrees_eq_twice_card_edges] + refine sum_congr rfl fun u _ => ?_ + rw [← card_neighborFinset_eq_degree, neighborFinset_eq_filter, card_filter] + +/-- **Füredi's partition inequality.** Every `K_{p+1}`-free finite graph has a partition into +`p` parts (the fibres of `f`) such that the number of edges of `G` plus the number of edges of +`G` inside the parts is at most the number of edges of the complete `p`-partite graph on these +parts. -/ +theorem card_edgeSet_add_le {W : Type*} [Finite W] (G : SimpleGraph W) {p : ℕ} (hp : 0 < p) + (hG : G.CliqueFree (p + 1)) : + ∃ f : W → Fin p, G.edgeSet.ncard + (G \ (⊤ : SimpleGraph (Fin p)).comap f).edgeSet.ncard ≤ + ((⊤ : SimpleGraph (Fin p)).comap f).edgeSet.ncard := by + have _ : 0 < p := hp + classical + have := Fintype.ofFinite W + obtain ⟨f, hf, hle⟩ := key_ineq G p univ (fun t _ => hG t) + let f' : W → Fin p := fun w => ⟨f w, hf w (mem_univ w)⟩ + refine ⟨f', ?_⟩ + have e1 := two_mul_ncard_edgeSet G + have e2 := two_mul_ncard_edgeSet (G \ (⊤ : SimpleGraph (Fin p)).comap f') + have e3 := two_mul_ncard_edgeSet ((⊤ : SimpleGraph (Fin p)).comap f') + have hl : lhsCount G univ f = (∑ u, ∑ v, if G.Adj u v then 1 else 0) + + ∑ u, ∑ v, if (G \ (⊤ : SimpleGraph (Fin p)).comap f').Adj u v then 1 else 0 := by + unfold lhsCount + rw [← sum_add_distrib] + refine sum_congr rfl fun u _ => ?_ + rw [← sum_add_distrib] + refine sum_congr rfl fun v _ => ?_ + by_cases h1 : G.Adj u v <;> by_cases h2 : f u = f v <;> simp [h1, h2, f', Fin.ext_iff] + have hr : rhsCount univ f = + ∑ u, ∑ v, if ((⊤ : SimpleGraph (Fin p)).comap f').Adj u v then 1 else 0 := by + unfold rhsCount + refine sum_congr rfl fun u _ => sum_congr rfl fun v _ => ?_ + by_cases h2 : f u = f v <;> simp [h2, f', Fin.ext_iff] + omega + +lemma ncard_comap_le_turanNumber {p : ℕ} (f : V → Fin p) : + ((⊤ : SimpleGraph (Fin p)).comap f).edgeSet.ncard ≤ turanNumber (card V) p := by + classical + have hc : ((⊤ : SimpleGraph (Fin p)).comap f).Colorable p := by + simpa using (Coloring.mk f (fun h => by simpa using h) : + ((⊤ : SimpleGraph (Fin p)).comap f).Coloring (Fin p)).colorable + have := (hc.cliqueFree (Nat.lt_succ_self p)).card_edgeFinset_le + rwa [← Set.ncard_coe_finset, coe_edgeFinset] at this + +/-- **Füredi's theorem (2015).** If `G` is a `K_{p+1}`-free graph on `n` vertices with at least +`turanNumber n p - t` edges, then `G` has a `p`-colourable (i.e. `p`-partite) subgraph `H` with +at least `e(G) - t` edges. -/ +theorem furedi (G : SimpleGraph V) {p t : ℕ} (hp : 0 < p) (hG : G.CliqueFree (p + 1)) + (ht : turanNumber (card V) p ≤ G.edgeSet.ncard + t) : + ∃ H : SimpleGraph V, H ≤ G ∧ H.Colorable p ∧ G.edgeSet.ncard ≤ H.edgeSet.ncard + t := by + obtain ⟨f, hf⟩ := card_edgeSet_add_le G hp hG + have hK := ncard_comap_le_turanNumber f + refine ⟨G ⊓ (⊤ : SimpleGraph (Fin p)).comap f, inf_le_left, ?_, ?_⟩ + · have hc : ((⊤ : SimpleGraph (Fin p)).comap f).Colorable p := by + simpa using (Coloring.mk f (fun h => by simpa using h) : + ((⊤ : SimpleGraph (Fin p)).comap f).Coloring (Fin p)).colorable + exact hc.mono_left inf_le_right + · have hsplit := Set.ncard_inter_add_ncard_sdiff_eq_ncard G.edgeSet + ((⊤ : SimpleGraph (Fin p)).comap f).edgeSet + rw [← edgeSet_inf, ← edgeSet_sdiff] at hsplit + omega + +/-- **Füredi's theorem, edit-distance form.** Under the hypotheses of `furedi`, there is a +partition into `p` parts with at most `t` edges of `G` inside the parts, and `G` differs from the +complete `p`-partite graph on these parts in at most `3 t` edges. -/ +theorem exists_partition_symmDiff_le (G : SimpleGraph V) {p t : ℕ} (hp : 0 < p) + (hG : G.CliqueFree (p + 1)) (ht : turanNumber (card V) p ≤ G.edgeSet.ncard + t) : + ∃ f : V → Fin p, (G \ (⊤ : SimpleGraph (Fin p)).comap f).edgeSet.ncard ≤ t ∧ + (symmDiff G ((⊤ : SimpleGraph (Fin p)).comap f)).edgeSet.ncard ≤ 3 * t := by + obtain ⟨f, hf⟩ := card_edgeSet_add_le G hp hG + have hK := ncard_comap_le_turanNumber f + refine ⟨f, ?_⟩ + set K := (⊤ : SimpleGraph (Fin p)).comap f + have hsplit := Set.ncard_inter_add_ncard_sdiff_eq_ncard G.edgeSet K.edgeSet + have hsplit2 := Set.ncard_inter_add_ncard_sdiff_eq_ncard K.edgeSet G.edgeSet + rw [Set.inter_comm, ← edgeSet_inf, ← edgeSet_sdiff] at hsplit2 + rw [← edgeSet_inf, ← edgeSet_sdiff] at hsplit + refine ⟨by omega, ?_⟩ + have hu : (symmDiff G K).edgeSet.ncard ≤ (G \ K).edgeSet.ncard + (K \ G).edgeSet.ncard := by + rw [symmDiff_def, edgeSet_sup] + exact Set.ncard_union_le _ _ + omega + +/-- **Erdős–Simonovits stability theorem for cliques** (Erdős 1967, Simonovits 1968), in the +form obtained from Füredi's theorem: for every `ε > 0` there is `δ > 0` such that every +`K_{p+1}`-free graph on `n` vertices with at least `(1 - 1/p) n² / 2 - δ n²` edges differs from +some complete `p`-partite graph on the same vertices in at most `ε n²` edges. -/ +theorem erdos_simonovits_stability {p : ℕ} (hp : 0 < p) {ε : ℝ} (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∀ (W : Type) [Fintype W] (G : SimpleGraph W), G.CliqueFree (p + 1) → + (1 - 1 / (p : ℝ)) * (card W : ℝ) ^ 2 / 2 - δ * (card W : ℝ) ^ 2 ≤ G.edgeSet.ncard → + ∃ f : W → Fin p, + ((symmDiff G ((⊤ : SimpleGraph (Fin p)).comap f)).edgeSet.ncard : ℝ) ≤ + ε * (card W : ℝ) ^ 2 := by + refine ⟨ε / 3, by positivity, fun W _ G hG hedge => ?_⟩ + set n := card W + set T := turanNumber n p + set e := G.edgeSet.ncard + obtain ⟨f, -, h2⟩ := exists_partition_symmDiff_le G hp hG (t := T - e) le_add_tsub + refine ⟨f, ?_⟩ + have hT : (T : ℝ) ≤ (1 - 1 / (p : ℝ)) * (n : ℝ) ^ 2 / 2 := by + have h := mul_turanNumber_le (r := p) (n := n) + have hp' : (0 : ℝ) < p := by exact_mod_cast hp + have hc : (2 * p * T : ℝ) ≤ ((p : ℝ) - 1) * (n : ℝ) ^ 2 := by + have := (Nat.cast_le (α := ℝ)).mpr h + push_cast [Nat.cast_sub (show 1 ≤ p from hp)] at this + exact this + rw [show (1 - 1 / (p : ℝ)) * (n : ℝ) ^ 2 / 2 = ((p - 1) * (n : ℝ) ^ 2) / (2 * p) by + field_simp] + rw [le_div_iff₀ (by positivity)] + linarith + have ht : ((T - e : ℕ) : ℝ) ≤ ε / 3 * (n : ℝ) ^ 2 := by + rcases le_total T e with h | h + · rw [Nat.sub_eq_zero_of_le h, Nat.cast_zero]; positivity + · rw [Nat.cast_sub h]; linarith + have := (Nat.cast_le (α := ℝ)).mpr h2 + push_cast at this + linarith + +end Furedi diff --git a/LeanPool/RemovalExtremalStability/GeneralGraphRemoval.lean b/LeanPool/RemovalExtremalStability/GeneralGraphRemoval.lean new file mode 100644 index 000000000..30dc75d52 --- /dev/null +++ b/LeanPool/RemovalExtremalStability/GeneralGraphRemoval.lean @@ -0,0 +1,390 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Triangle.Removal +public import Mathlib.Combinatorics.SimpleGraph.Copy +public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges +public import Mathlib.Tactic +public import LeanPool.RemovalExtremalStability.CliqueRemoval +public import LeanPool.RemovalExtremalStability.PartialEmbedding + +/-! + +Adapted from [jtraverso/graph-removal-lemma](https://github.com/jtraverso/graph-removal-lemma/blob/589cf03ef1e4c80ea8cdd6be77778232c62dd37c/RemovalLib/GraphRemoval.lean) (Palomar-registered source). +# The graph removal lemma for every fixed graph + +Let `H` be a fixed finite graph on `k` vertices. + +* `GraphRemoval.card_copies_ge`: **counting lemma for `H`.** If parts `s x` (one per vertex `x` of + `H`, possibly repeated) are pairwise dense in a robust sense *along the edges of `H`*, and large + enough, then the number of injective maps `f` with `f x ∈ s x` sending edges of `H` to edges of + `G` is at least `(d^k / 4)^k ∏ₓ #(s x)`. +* `GraphRemoval.le_labelledCopyCount_of_deleteFar`: **graph removal lemma, far form**. + For every `ε > 0` there is `δ > 0` such that a graph on `n` vertices + from which one must delete at least `ε n²` edges to destroy all copies of `H` (Mathlib's + `SimpleGraph.DeleteFar` and `SimpleGraph.Free`) has at least `δ n^k` labelled copies of `H` + (Mathlib's `SimpleGraph.labelledCopyCount`). +* `GraphRemoval.graph_removal`: **graph removal lemma.** A graph on `n` vertices with fewer than + `δ n^k` labelled copies of `H` can be made `H`-free by deleting fewer than `ε n²` edges. + +The quantitative copy-count formulation is stated in Conlon–Fox, *Graph removal lemmas*, +[Theorem 1.1](https://arxiv.org/pdf/1211.3487v1). For fixed `H`, changing from unlabelled copies to +injective labelled copies changes only a factor depending on `H`, which is absorbed into `δ`. +The far form is the contrapositive. Erdős–Frankl–Rödl (1986), +[Theorems 1.5 and 1.5′](https://www.renyi.hu/~p_erdos/1986-17.pdf), give related precursors: +starting from an `H`-free graph, they remove few edges to exclude a clique or a homomorphic image. +-/ + +@[expose] public section + +open Finset Fintype SimpleGraph + +namespace GraphRemoval + +private theorem finite_constrained_copies {α β : Type*} [Finite β] (L : SimpleGraph β) + (G : SimpleGraph α) (s : β → Finset α) : + Finite {f : β ↪ α // (∀ x, f x ∈ s x) ∧ ∀ x y, L.Adj x y → G.Adj (f x) (f y)} := by + classical + have : Fintype β := Fintype.ofFinite β + refine Finite.of_injective (β := ↥(Fintype.piFinset s)) + (fun p => ⟨⇑p.1, Fintype.mem_piFinset.2 p.2.1⟩) ?_ + intro p q h + exact Subtype.ext (DFunLike.coe_injective (congrArg Subtype.val h)) + +/-- **Counting lemma for a fixed graph.** Let `L` be a graph on a finite type `β` with +`k = card β` vertices, and `s : β → Finset α` parts of a graph `G` such that for every edge `xy` of +`L`, all subsets `A ⊆ s x`, `B ⊆ s y` with `#A ≥ η #(s x)`, `#B ≥ η #(s y)` have edge density at +least `d`, where `0 < η ≤ 1`, `0 < d ≤ 1`, `2 k η ≤ d ^ k` and every part has at least `4 k / d ^ k` +elements. Then there are at least `(d ^ k / 4) ^ k ∏ₓ #(s x)` injective maps `f : β → α` with +`f x ∈ s x` for every `x` that send edges of `L` to edges of `G`. -/ +theorem card_copies_ge {α β : Type*} [Fintype β] (L : SimpleGraph β) + (G : SimpleGraph α) [DecidableRel G.Adj] (s : β → Finset α) {η d : ℝ} (hη : 0 < η) + (hη₁ : η ≤ 1) (hd : 0 < d) (hd₁ : d ≤ 1) (hηd : 2 * card β * η ≤ d ^ card β) + (hsize : ∀ x, 4 * card β ≤ d ^ card β * #(s x)) + (hs : ∀ x y, L.Adj x y → ∀ A ⊆ s x, ∀ B ⊆ s y, η * #(s x) ≤ #A → η * #(s y) ≤ #B → + d ≤ G.edgeDensity A B) : + (d ^ card β / 4) ^ card β * ∏ x, (#(s x) : ℝ) ≤ + Nat.card {f : β ↪ α // (∀ x, f x ∈ s x) ∧ ∀ x y, L.Adj x y → G.Adj (f x) (f y)} := by + classical + set k := card β with hk + set D : ℝ := d ^ k with hD_def + have hfin : Finite {f : β ↪ α // (∀ x, f x ∈ s x) ∧ ∀ x y, L.Adj x y → G.Adj (f x) (f y)} := + finite_constrained_copies L G s + rcases isEmpty_or_nonempty β with hβ | hβ + · have hk0 : k = 0 := Fintype.card_eq_zero + have hne : Nonempty {f : β ↪ α // (∀ x, f x ∈ s x) ∧ ∀ x y, L.Adj x y → G.Adj (f x) (f y)} := + ⟨⟨Function.Embedding.ofIsEmpty, fun a => isEmptyElim a, fun a => isEmptyElim a⟩⟩ + simp only [hk0, pow_zero, univ_eq_empty, Finset.prod_empty] + exact_mod_cast Nat.card_pos + have hk1 : (1 : ℝ) ≤ k := by exact_mod_cast Fintype.card_pos + have hDpos : 0 < D := pow_pos hd _ + obtain ⟨a₀, -⟩ : (s hβ.some).Nonempty := by + rw [← Finset.card_pos] + by_contra h + have := hsize hβ.some + rw [Nat.eq_zero_of_not_pos h] at this + simp at this + linarith + let Cand : (β → α) → Finset β → β → Finset α := fun f S y => + {w ∈ s y | ∀ z ∈ S, L.Adj z y → G.Adj (f z) w} + have hCandEq : ∀ f S y, Cand f S y = PartialEmbedding.candidates G L s f S y := by + intros f S y + ext w + simp [Cand, PartialEmbedding.candidates] + let Good : Finset β → Finset (β → α) := fun S => + {f ∈ Fintype.piFinset (fun y => if y ∈ S then s y else {a₀}) | Set.InjOn f S ∧ + (∀ x ∈ S, ∀ y ∈ S, L.Adj x y → G.Adj (f x) (f y)) ∧ + ∀ y ∉ S, d ^ #S * #(s y) ≤ #(Cand f S y)} + have key : ∀ S, ∏ x ∈ S, (D / 4 * #(s x)) ≤ (#(Good S) : ℝ) := by + intro S + induction S using Finset.induction_on with + | empty => + rw [Finset.prod_empty, Nat.one_le_cast, Nat.one_le_iff_ne_zero, ← pos_iff_ne_zero, card_pos] + refine ⟨fun _ => a₀, ?_⟩ + simp [Good, Cand] + | insert x S hxS ih => + rw [prod_insert hxS] + have hSk : #S + 1 ≤ k := by + have := card_le_univ (insert x S); rwa [card_insert_of_notMem hxS] at this + have hpowS : D ≤ d ^ #S := pow_le_pow_of_le_one hd.le hd₁ (by omega) + let Y := (univ \ insert x S).filter (L.Adj x) + have hYcard : #Y + #S + 1 ≤ k := by + have h1 : #Y ≤ #(univ \ insert x S) := card_filter_le _ _ + rw [card_sdiff_of_subset (subset_univ _), card_insert_of_notMem hxS, card_univ] at h1 + omega + let Bad : (β → α) → β → Finset α := fun f y => + {v ∈ s x | (#{w ∈ Cand f S y | G.Adj v w} : ℝ) < d * #(Cand f S y)} + let Ext : (β → α) → Finset α := fun f => + (Cand f S x).filter (fun v => v ∉ S.image f ∧ ∀ y ∈ Y, v ∉ Bad f y) + have hExt : ∀ f ∈ Good S, D / 4 * #(s x) ≤ (#(Ext f) : ℝ) := by + intro f hf + obtain ⟨-, -, -, hcand⟩ := mem_filter.1 hf + have hCand_big : ∀ y ∉ S, D * #(s y) ≤ #(Cand f S y) := fun y hy => + (mul_le_mul_of_nonneg_right hpowS (Nat.cast_nonneg _)).trans (hcand y hy) + have hBad : ∀ y ∈ Y, (#(Bad f y) : ℝ) < η * #(s x) := by + intro y hy + simp only [Y, mem_filter, mem_sdiff, mem_univ, true_and, mem_insert, not_or] at hy + refine CliqueCounting.card_badVertices_lt G hd + (mul_le_of_le_one_left (Nat.cast_nonneg _) hη₁) fun A hA hA' _ => + hs x y hy.2 A hA _ (filter_subset _ _) hA' ?_ + refine le_trans ?_ (hCand_big y hy.1.2) + gcongr + nlinarith + have hsub : Cand f S x ⊆ S.image f ∪ Y.biUnion (Bad f) ∪ Ext f := by + intro v hv + by_contra hv' + simp only [mem_union, not_or, mem_biUnion, not_exists, not_and] at hv' + exact hv'.2 (mem_filter.2 ⟨hv, hv'.1.1, fun y hy => hv'.1.2 y hy⟩) + have h1 : (#(Cand f S x) : ℝ) ≤ #S + ∑ y ∈ Y, (#(Bad f y) : ℝ) + #(Ext f) := by + have := (card_le_card hsub).trans ((card_union_le _ _).trans + (Nat.add_le_add_right ((card_union_le _ _).trans + (Nat.add_le_add card_image_le card_biUnion_le)) _)) + exact_mod_cast this + have h2 : ∑ y ∈ Y, (#(Bad f y) : ℝ) ≤ #Y * (η * #(s x)) := by + rw [← nsmul_eq_mul, ← sum_const]; exact sum_le_sum fun y hy => (hBad y hy).le + have h3 := hCand_big x hxS + have h4 := hsize x + have h5 : ((#Y : ℕ) : ℝ) + #S + 1 ≤ k := by exact_mod_cast hYcard + set N : ℝ := (#(s x) : ℝ) + have hN : 0 ≤ N := Nat.cast_nonneg _ + have hY0 : (0 : ℝ) ≤ #Y := Nat.cast_nonneg _ + have hS0 : (0 : ℝ) ≤ #S := Nat.cast_nonneg _ + have e1 : 2 * #Y * (η * N) ≤ D * N := by + have := mul_le_mul_of_nonneg_right hηd hN + have : 2 * #Y * (η * N) ≤ 2 * k * η * N := by + have : 0 ≤ η * N := by positivity + nlinarith + linarith + nlinarith + have hmem : ∀ f ∈ Good S, ∀ v ∈ Ext f, Function.update f x v ∈ Good (insert x S) := by + intro f hf v hv + obtain ⟨hpi, hinj, hadj, hcand⟩ := mem_filter.1 hf + rw [Fintype.mem_piFinset] at hpi + obtain ⟨hvC, hvS, hvB⟩ := mem_filter.1 hv + have hvC' := mem_filter.1 hvC + have hmemS : ∀ z ∈ S, f z ∈ s z := by + intro z hz + simpa [hz] using hpi z + have hgood : ∀ y, y ∉ insert x S → L.Adj x y → + d * #(Cand f S y) ≤ #{w ∈ Cand f S y | G.Adj v w} := by + intro y hy hxy + have hyY : y ∈ Y := by simp [Y, hy, hxy] + exact le_of_not_gt fun h => hvB y hyY (mem_filter.2 ⟨hvC'.1, h⟩) + have hcandShared : ∀ y ∉ S, d ^ #S * #(s y) ≤ + #(PartialEmbedding.candidates G L s f S y) := by + simpa only [← hCandEq] using hcand + have hvCShared : v ∈ PartialEmbedding.candidates G L s f S x := by + simpa only [← hCandEq] using hvC + have hgoodShared : ∀ y, y ∉ insert x S → L.Adj x y → + d * #(PartialEmbedding.candidates G L s f S y) ≤ + #{w ∈ PartialEmbedding.candidates G L s f S y | G.Adj v w} := by + simpa only [← hCandEq] using hgood + obtain ⟨hinj', -, hadj', hcand'⟩ := + PartialEmbedding.extend G L s hd hd₁ S x hxS f v + hinj hmemS hadj hcandShared hvCShared hvS hgoodShared + have hcandFinal : ∀ y ∉ insert x S, + d ^ #(insert x S) * #(s y) ≤ #(Cand (Function.update f x v) (insert x S) y) := by + simpa only [← hCandEq] using hcand' + have hfS : ∀ z, z ≠ x → Function.update f x v z = f z := fun z hz => + Function.update_of_ne hz _ _ + refine mem_filter.2 ⟨Fintype.mem_piFinset.2 (fun y => ?_), hinj', hadj', hcandFinal⟩ + · by_cases hyx : y = x + · subst hyx; simpa using hvC'.1 + · rw [hfS y hyx] + have := hpi y + by_cases hyS : y ∈ S + · simpa [hyS] using this + · simpa [hyS, hyx] using this + have hinj : #((Good S).sigma Ext) ≤ #(Good (insert x S)) := by + refine card_le_card_of_injOn (fun p => Function.update p.1 x p.2) ?_ ?_ + · rintro ⟨f, v⟩ hp + simp only [coe_sigma, Set.mem_sigma_iff, mem_coe] at hp + exact hmem f hp.1 v hp.2 + · rintro ⟨f, v⟩ hp ⟨f', v'⟩ hp' h + simp only [coe_sigma, Set.mem_sigma_iff, mem_coe] at hp hp' + have hv : v = v' := by simpa using congrFun h x + subst hv + have hfx : ∀ g ∈ Good S, g x = a₀ := by + intro g hg + have := Fintype.mem_piFinset.1 (mem_filter.1 hg).1 x + simpa [hxS] using this + have : f = f' := by + funext z + by_cases hzx : z = x + · subst hzx; rw [hfx f hp.1, hfx f' hp'.1] + · have := congrFun h z + simpa [Function.update_of_ne hzx] using this + subst this; rfl + rw [Finset.card_sigma] at hinj + have hsum : ∑ f ∈ Good S, D / 4 * (#(s x) : ℝ) ≤ ∑ f ∈ Good S, (#(Ext f) : ℝ) := + sum_le_sum hExt + rw [sum_const, nsmul_eq_mul] at hsum + have hfin := (Nat.cast_le (α := ℝ)).2 hinj + rw [Nat.cast_sum] at hfin + have hc : (0 : ℝ) ≤ D / 4 * #(s x) := by positivity + calc D / 4 * #(s x) * ∏ x ∈ S, (D / 4 * #(s x)) + ≤ D / 4 * #(s x) * #(Good S) := mul_le_mul_of_nonneg_left ih hc + _ = #(Good S) * (D / 4 * #(s x)) := by ring + _ ≤ _ := hsum.trans hfin + have hfinal := key univ + rw [prod_mul_distrib, prod_const, card_univ] at hfinal + refine hfinal.trans ?_ + have hgood : ∀ f ∈ Good univ, Function.Injective f ∧ (∀ x, f x ∈ s x) ∧ + ∀ x y, L.Adj x y → G.Adj (f x) (f y) := by + intro f hf + obtain ⟨hpi, hinj, hadj, -⟩ := mem_filter.1 hf + refine ⟨fun a b h => hinj (mem_coe.2 (mem_univ a)) (mem_coe.2 (mem_univ b)) h, + fun x => by simpa using Fintype.mem_piFinset.1 hpi x, + fun x y h => hadj x (mem_univ x) y (mem_univ y) h⟩ + have hle : Nat.card ↥(Good univ) ≤ + Nat.card {f : β ↪ α // (∀ x, f x ∈ s x) ∧ ∀ x y, L.Adj x y → G.Adj (f x) (f y)} := by + refine Nat.card_le_card_of_injective + (fun p => ⟨⟨p.1, (hgood p.1 p.2).1⟩, (hgood p.1 p.2).2⟩) ?_ + intro p q h + have := congrArg (fun r => (r.1 : β → α)) h + exact Subtype.ext this + rw [Nat.card_eq_fintype_card, Fintype.card_coe] at hle + exact_mod_cast hle + +/-- **Graph removal lemma, far form.** The contrapositive of Conlon–Fox, +*Graph removal lemmas*, [Theorem 1.1](https://arxiv.org/pdf/1211.3487v1). +For every finite graph `H` and every `ε > 0` there is `δ > 0` such that every finite graph on `n` +vertices that is `ε n²`-far from being `H`-free has at least `δ n ^ (card β)` labelled copies of +`H`. -/ +theorem le_labelledCopyCount_of_deleteFar {β : Type} [Fintype β] (H : SimpleGraph β) {ε : ℝ} + (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∀ (α : Type) [Fintype α] [DecidableEq α] (G : SimpleGraph α) + [DecidableRel G.Adj], G.DeleteFar (fun G' ↦ H.Free G') (ε * (card α ^ 2 : ℕ)) → + δ * card α ^ card β ≤ G.labelledCopyCount H := by + classical + set k := card β with hk + rcases isEmpty_or_nonempty β with hβ | hβ + · refine ⟨1, one_pos, fun α _ _ G _ _ => ?_⟩ + have hk0 : k = 0 := Fintype.card_eq_zero + rw [hk0, pow_zero, mul_one, Nat.one_le_cast, Nat.one_le_iff_ne_zero, Ne, + labelledCopyCount_eq_zero] + exact fun h => h ⟨Hom.toCopy ⟨isEmptyElim, fun {a} => isEmptyElim a⟩ (fun a => isEmptyElim a)⟩ + have hk1 : (1 : ℝ) ≤ k := by exact_mod_cast Fintype.card_pos + set ε₁ : ℝ := min ε 1 with hε₁_def + have hε₁ : 0 < ε₁ := lt_min hε one_pos + have hε₁1 : ε₁ ≤ 1 := min_le_right _ _ + have hε₁ε : ε₁ ≤ ε := min_le_left _ _ + set d : ℝ := ε₁ / 8 with hd_def + have hd : 0 < d := by positivity + have hd₁ : d ≤ 1 := by linarith + set D : ℝ := d ^ k with hD_def + have hD : 0 < D := by positivity + set η : ℝ := min (ε₁ / 8) (D / (2 * k + 1)) with hη_def + have hη : 0 < η := lt_min (by positivity) (by positivity) + have hηε : η ≤ ε₁ / 8 := min_le_left _ _ + have hη₁ : η ≤ 1 := by linarith + have hηd : 2 * k * η ≤ D := by + have h1 : η ≤ D / (2 * k + 1) := min_le_right _ _ + rw [le_div_iff₀ (by positivity)] at h1 + nlinarith + set l : ℕ := ⌈4 / ε₁⌉₊ with hl_def + have hl : 4 / ε₁ ≤ l := Nat.le_ceil _ + set B : ℕ := SzemerediRegularity.bound η l with hB_def + have hB : (0 : ℝ) < B := by positivity + set T : ℕ := l + ⌈8 * k * B / D⌉₊ with hT_def + set δ : ℝ := min (1 / ((T : ℝ) + 1) ^ k) ((D / 4) ^ k * (1 / (2 * B)) ^ k) with hδ_def + have hδ1 : δ ≤ 1 / ((T : ℝ) + 1) ^ k := min_le_left _ _ + have hδ2 : δ ≤ (D / 4) ^ k * (1 / (2 * B)) ^ k := min_le_right _ _ + refine ⟨δ, by positivity, fun α _ _ G _ hG => ?_⟩ + have hδ0 : 0 ≤ δ := by positivity + obtain hn | hn := Nat.eq_zero_or_pos (card α) + · rw [hn, Nat.cast_zero, zero_pow (Fintype.card_ne_zero), mul_zero] + positivity + have hG₁ : G.DeleteFar (fun G' ↦ H.Free G') (ε₁ * (card α ^ 2 : ℕ)) := + hG.mono (by gcongr) + have hnc : ¬ H.Free G := by + intro h + have := hG (s := ∅) (empty_subset _) (by simpa only [coe_empty, deleteEdges_empty] using h) + rw [Finset.card_empty, Nat.cast_zero] at this + have : (0 : ℝ) < ε * (card α ^ 2 : ℕ) := by positivity + linarith + rcases le_total (card α) T with hT' | hT' + · have h1 : (1 : ℝ) ≤ G.labelledCopyCount H := by + rw [Nat.one_le_cast, Nat.one_le_iff_ne_zero, Ne, labelledCopyCount_eq_zero] + exact hnc + calc δ * card α ^ k ≤ 1 / ((T : ℝ) + 1) ^ k * ((T : ℝ) + 1) ^ k := by + gcongr + exact_mod_cast hT'.trans (Nat.le_succ T) + _ = 1 := by field_simp + _ ≤ _ := h1 + · have : Nonempty α := Fintype.card_pos_iff.1 hn + have hl' : l ≤ card α := le_trans (Nat.le_add_right _ _) hT' + have hn8 : 8 * k * B / D ≤ card α := by + refine (Nat.le_ceil _).trans ?_ + exact_mod_cast le_trans (Nat.le_add_left _ _) hT' + obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := szemeredi_regularity G hη hl' + have hP' : 4 / ε₁ ≤ #P.parts := hl.trans (Nat.cast_le.2 hP₂) + have hedges := CliqueRemoval.regularityReduced_edges_card_aux' hε₁ hη hηε hP₁ hP₄ hP' + have hnc' : ¬ H.Free (G.regularityReduced P η (ε₁ / 4)) := by + intro h + have := (deleteFar_iff.1 hG₁) regularityReduced_le h + linarith + obtain ⟨φ⟩ := not_not.1 hnc' + let s : β → Finset α := fun x => P.part (φ x) + have hs : ∀ x y, H.Adj x y → ∀ A ⊆ s x, ∀ B ⊆ s y, η * #(s x) ≤ #A → η * #(s y) ≤ #B → + d ≤ G.edgeDensity A B := by + intro x y hxy A hA B' hB' hA' hB'' + have hadj : (G.regularityReduced P η (ε₁ / 4)).Adj (φ x) (φ y) := by + simpa using φ.toHom.map_adj hxy + obtain ⟨-, X, hX, Y, hY, hxX, hyY, hXY, hu, hdens⟩ := hadj + have h1 : s x = X := P.part_eq_of_mem hX hxX + have h2 : s y = Y := P.part_eq_of_mem hY hyY + rw [h1] at hA hA' + rw [h2] at hB' hB'' + have := hu hA hB' (by rw [mul_comm]; exact hA') (by rw [mul_comm]; exact hB'') + rw [abs_sub_lt_iff] at this + linarith + have hsize : ∀ x, 4 * k ≤ D * #(s x) := by + intro x + have hb := CliqueRemoval.card_bound hP₁ hP₃ (P.part_mem.2 (mem_univ (φ x))) + rw [div_le_iff₀ (by positivity)] at hb hn8 + have : D * (card α) ≤ D * (#(s x) * (2 * B)) := by gcongr + have h3 : 4 * k * (2 * B) ≤ D * #(s x) * (2 * B) := by nlinarith + exact le_of_mul_le_mul_right h3 (by positivity) + have hcount := card_copies_ge H G s hη hη₁ hd hd₁ hηd hsize hs + have hinj : Nat.card {f : β ↪ α // (∀ x, f x ∈ s x) ∧ ∀ x y, H.Adj x y → G.Adj (f x) (f y)} + ≤ G.labelledCopyCount H := by + rw [labelledCopyCount, Fintype.card_eq_nat_card] + refine Nat.card_le_card_of_injective + (fun p => Hom.toCopy ⟨p.1, fun h => p.2.2 _ _ h⟩ p.1.injective) ?_ + intro p q h + have := congrArg (fun c : H.Copy G => (c : β → α)) h + exact Subtype.ext (DFunLike.coe_injective this) + calc δ * card α ^ k ≤ (D / 4) ^ k * (1 / (2 * B)) ^ k * card α ^ k := by gcongr + _ = (D / 4) ^ k * (card α / (2 * B : ℝ)) ^ k := by + rw [mul_assoc, ← mul_pow, one_div_mul_eq_div] + _ = (D / 4) ^ k * ∏ _x : β, (card α / (2 * B : ℝ)) := by + rw [prod_const, card_univ, ← hk] + _ ≤ (D / 4) ^ k * ∏ x, (#(s x) : ℝ) := by + gcongr with x + exact CliqueRemoval.card_bound hP₁ hP₃ (P.part_mem.2 (mem_univ _)) + _ ≤ _ := hcount + _ ≤ _ := by exact_mod_cast hinj + +/-- **Graph removal lemma.** See Conlon–Fox, *Graph removal lemmas*, +[Theorem 1.1](https://arxiv.org/pdf/1211.3487v1). +For every finite graph `H` and every `ε > 0` there is `δ > 0` such that every finite graph on `n` +vertices with fewer than `δ n ^ (card β)` labelled copies of `H` has an `H`-free subgraph obtained +by deleting fewer than `ε n²` edges. -/ +theorem graph_removal {β : Type} [Fintype β] (H : SimpleGraph β) {ε : ℝ} (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∀ (α : Type) [Fintype α] [DecidableEq α] (G : SimpleGraph α) + [DecidableRel G.Adj], (G.labelledCopyCount H : ℝ) < δ * card α ^ card β → + ∃ G' ≤ G, ∃ _ : DecidableRel G'.Adj, + (#G.edgeFinset - #G'.edgeFinset : ℝ) < ε * (card α ^ 2 : ℕ) ∧ H.Free G' := by + obtain ⟨δ, hδ, h⟩ := le_labelledCopyCount_of_deleteFar H hε + refine ⟨δ, hδ, fun α _ _ G _ hG => ?_⟩ + by_contra! h' + refine hG.not_ge (h α G (deleteFar_iff.2 ?_)) + intro G' _ hG' hG'' + exact le_of_not_gt fun i ↦ hG'' (h' G' hG' _ i) + +end GraphRemoval diff --git a/LeanPool/RemovalExtremalStability/GraphRemoval.lean b/LeanPool/RemovalExtremalStability/GraphRemoval.lean new file mode 100644 index 000000000..7d492a74d --- /dev/null +++ b/LeanPool/RemovalExtremalStability/GraphRemoval.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Copy +public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges +public import Mathlib.Tactic +public import LeanPool.RemovalExtremalStability.GeneralGraphRemoval + +/-! + +Adapted from [jtraverso/graph-removal-lemma](https://github.com/jtraverso/graph-removal-lemma/blob/589cf03ef1e4c80ea8cdd6be77778232c62dd37c/Solution.lean) (Palomar-registered source). +# Proofs of the statements in `Challenge.lean` + +The theorems are proved in `RemovalLib/GraphRemoval.lean` (namespace `GraphRemoval`), on top of +`StabilityLib/` (the clique counting, clique removal and embedding lemmas of the registered entry +PALOMAR-2026-10-16-000024, included unchanged). The counting lemma is the greedy embedding argument +of `StabilityLib/Embedding.lean`, turned into a count of partial embeddings. The far form applies +Mathlib's Szemerédi regularity lemma (`szemeredi_regularity`) and finds a copy of `H` in the +reduced graph; its parts satisfy the hypotheses of the counting lemma. The removal lemma is its +contrapositive. +-/ + +@[expose] public section + +open Finset Fintype SimpleGraph + +namespace RemovalLemma + +/-- **Counting lemma for a fixed graph.** Let `L` be a graph on a finite type `β` with +`k = card β` vertices, and `s : β → Finset α` parts of a graph `G` such that for every edge `xy` of +`L`, all subsets `A ⊆ s x`, `B ⊆ s y` with `#A ≥ η #(s x)`, `#B ≥ η #(s y)` have edge density at +least `d`, where `0 < η ≤ 1`, `0 < d ≤ 1`, `2 k η ≤ d ^ k` and every part has at least `4 k / d ^ k` +elements. Then there are at least `(d ^ k / 4) ^ k ∏ₓ #(s x)` injective maps `f : β → α` with +`f x ∈ s x` for every `x` that send edges of `L` to edges of `G`. -/ +theorem card_copies_ge {α β : Type*} [Fintype β] (L : SimpleGraph β) + (G : SimpleGraph α) [DecidableRel G.Adj] (s : β → Finset α) {η d : ℝ} (hη : 0 < η) + (hη₁ : η ≤ 1) (hd : 0 < d) (hd₁ : d ≤ 1) (hηd : 2 * card β * η ≤ d ^ card β) + (hsize : ∀ x, 4 * card β ≤ d ^ card β * #(s x)) + (hs : ∀ x y, L.Adj x y → ∀ A ⊆ s x, ∀ B ⊆ s y, η * #(s x) ≤ #A → η * #(s y) ≤ #B → + d ≤ G.edgeDensity A B) : + (d ^ card β / 4) ^ card β * ∏ x, (#(s x) : ℝ) ≤ + Nat.card {f : β ↪ α // (∀ x, f x ∈ s x) ∧ ∀ x y, L.Adj x y → G.Adj (f x) (f y)} := + GraphRemoval.card_copies_ge L G s hη hη₁ hd hd₁ hηd hsize hs + +/-- **Graph removal lemma, far form.** The contrapositive of Conlon–Fox, +*Graph removal lemmas*, [Theorem 1.1](https://arxiv.org/pdf/1211.3487v1). +For every finite graph `H` and every `ε > 0` there is `δ > 0` such that every finite graph on `n` +vertices that is `ε n²`-far from being `H`-free has at least `δ n ^ (card β)` labelled copies of +`H`. -/ +theorem le_labelledCopyCount_of_deleteFar {β : Type} [Fintype β] (H : SimpleGraph β) {ε : ℝ} + (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∀ (α : Type) [Fintype α] [DecidableEq α] (G : SimpleGraph α) + [DecidableRel G.Adj], G.DeleteFar (fun G' ↦ H.Free G') (ε * (card α ^ 2 : ℕ)) → + δ * card α ^ card β ≤ G.labelledCopyCount H := + GraphRemoval.le_labelledCopyCount_of_deleteFar H hε + +/-- **Graph removal lemma.** See Conlon–Fox, *Graph removal lemmas*, +[Theorem 1.1](https://arxiv.org/pdf/1211.3487v1). +For every finite graph `H` and every `ε > 0` there is `δ > 0` such that every finite graph on `n` +vertices with fewer than `δ n ^ (card β)` labelled copies of `H` has an `H`-free subgraph obtained +by deleting fewer than `ε n²` edges. -/ +theorem graph_removal {β : Type} [Fintype β] (H : SimpleGraph β) {ε : ℝ} (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∀ (α : Type) [Fintype α] [DecidableEq α] (G : SimpleGraph α) + [DecidableRel G.Adj], (G.labelledCopyCount H : ℝ) < δ * card α ^ card β → + ∃ G' ≤ G, ∃ _ : DecidableRel G'.Adj, + (#G.edgeFinset - #G'.edgeFinset : ℝ) < ε * (card α ^ 2 : ℕ) ∧ H.Free G' := + GraphRemoval.graph_removal H hε + +end RemovalLemma diff --git a/LeanPool/RemovalExtremalStability/Imports.lean b/LeanPool/RemovalExtremalStability/Imports.lean new file mode 100644 index 000000000..a6eba58ad --- /dev/null +++ b/LeanPool/RemovalExtremalStability/Imports.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ +module -- shake: keep-all --deprecated_module: ignore + +-- Generated project imports; run `lake exe mk_all`. +public import LeanPool.RemovalExtremalStability +public import LeanPool.RemovalExtremalStability.CliqueCounting +public import LeanPool.RemovalExtremalStability.CliqueRemoval +public import LeanPool.RemovalExtremalStability.Embedding +public import LeanPool.RemovalExtremalStability.FewCopiesStability +public import LeanPool.RemovalExtremalStability.Furedi +public import LeanPool.RemovalExtremalStability.GeneralGraphRemoval +public import LeanPool.RemovalExtremalStability.GraphRemoval +public import LeanPool.RemovalExtremalStability.PartialEmbedding +public import LeanPool.RemovalExtremalStability.StabilityGeneral +public import LeanPool.RemovalExtremalStability.TuranStability diff --git a/LeanPool/RemovalExtremalStability/PartialEmbedding.lean b/LeanPool/RemovalExtremalStability/PartialEmbedding.lean new file mode 100644 index 000000000..29c7892c2 --- /dev/null +++ b/LeanPool/RemovalExtremalStability/PartialEmbedding.lean @@ -0,0 +1,104 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform +public import Mathlib.Tactic + +/-! +# Extending a partial graph embedding + +The existence and counting lemmas use the same local extension step. Their estimates for how many +extension vertices exist remain separate. +-/ + +@[expose] public section + +open Finset SimpleGraph + +namespace PartialEmbedding + +/-- Vertices in `parts y` compatible with the partial edge map `f` on `S`. +Exclusion of already used vertices is handled separately when extending the embedding. -/ +noncomputable def candidates {α β : Type*} (G : SimpleGraph α) (L : SimpleGraph β) + (parts : β → Finset α) (f : β → α) (S : Finset β) (y : β) : Finset α := by + classical + exact {w ∈ parts y | ∀ z ∈ S, L.Adj z y → G.Adj (f z) w} + +/-- An admissible new image extends a partial embedding and preserves the lower bounds on all +remaining candidate sets. The density argument that produces an admissible image is kept in the +respective existence and counting lemmas. -/ +theorem extend {α β : Type*} [DecidableEq α] [DecidableEq β] + (G : SimpleGraph α) [DecidableRel G.Adj] (L : SimpleGraph β) + (parts : β → Finset α) {d : ℝ} (hd : 0 < d) (hd₁ : d ≤ 1) + (S : Finset β) (x : β) (hxS : x ∉ S) (f : β → α) (v : α) + (hinj : Set.InjOn f S) (hmem : ∀ z ∈ S, f z ∈ parts z) + (hadj : ∀ a ∈ S, ∀ b ∈ S, L.Adj a b → G.Adj (f a) (f b)) + (hcand : ∀ y ∉ S, d ^ #S * #(parts y) ≤ #(candidates G L parts f S y)) + (hvC : v ∈ candidates G L parts f S x) (hvS : v ∉ S.image f) + (hgood : ∀ y, y ∉ insert x S → L.Adj x y → + d * #(candidates G L parts f S y) ≤ + #{w ∈ candidates G L parts f S y | G.Adj v w}) : + Set.InjOn (Function.update f x v) (↑(insert x S) : Set β) ∧ + (∀ z ∈ insert x S, Function.update f x v z ∈ parts z) ∧ + (∀ a ∈ insert x S, ∀ b ∈ insert x S, L.Adj a b → + G.Adj (Function.update f x v a) (Function.update f x v b)) ∧ + ∀ y ∉ insert x S, + d ^ #(insert x S) * #(parts y) ≤ + #(candidates G L parts (Function.update f x v) (insert x S) y) := by + classical + have hvC' : v ∈ parts x ∧ ∀ z ∈ S, L.Adj z x → G.Adj (f z) v := by + simpa only [candidates, mem_filter] using hvC + have hfS : ∀ z ∈ S, Function.update f x v z = f z := fun z hz => + Function.update_of_ne (by rintro rfl; exact hxS hz) _ _ + refine ⟨?_, ?_, ?_, ?_⟩ + · rw [coe_insert, Set.injOn_insert (by simpa using hxS)] + refine ⟨fun a ha b hb h => hinj ha hb ?_, ?_⟩ + · rwa [hfS a ha, hfS b hb] at h + · rintro ⟨z, hz, hzv⟩ + rw [Function.update_self, hfS z hz] at hzv + exact hvS (mem_image.2 ⟨z, hz, hzv⟩) + · intro z hz + rcases mem_insert.1 hz with rfl | hz + · simpa using hvC'.1 + · rw [hfS z hz]; exact hmem z hz + · have key : ∀ z ∈ S, L.Adj z x → G.Adj (f z) v := fun z hz h => hvC'.2 z hz h + intro a ha b hb hab + rcases mem_insert.1 ha with hax | ha' <;> rcases mem_insert.1 hb with hbx | hb' + · subst hax; subst hbx; exact absurd hab (SimpleGraph.irrefl _) + · subst hax; rw [Function.update_self, hfS b hb']; exact (key b hb' hab.symm).symm + · subst hbx; rw [Function.update_self, hfS a ha']; exact key a ha' hab + · rw [hfS a ha', hfS b hb']; exact hadj a ha' b hb' hab + · intro y hy + rw [mem_insert, not_or] at hy + rw [card_insert_of_notMem hxS, pow_succ] + by_cases hxy : L.Adj x y + · have hsub : {w ∈ candidates G L parts f S y | G.Adj v w} ⊆ + candidates G L parts (Function.update f x v) (insert x S) y := by + intro w hw + simp only [candidates, mem_filter, mem_insert] at hw ⊢ + refine ⟨hw.1.1, ?_⟩ + rintro z (rfl | hz) hzy + · simpa using hw.2 + · rw [hfS z hz]; exact hw.1.2 z hz hzy + calc d ^ #S * d * (#(parts y) : ℝ) = d * (d ^ #S * #(parts y)) := by ring + _ ≤ d * #(candidates G L parts f S y) := by gcongr; exact hcand y hy.2 + _ ≤ _ := hgood y (by simp [hy.1, hy.2]) hxy + _ ≤ _ := by exact_mod_cast card_le_card hsub + · have hsub : candidates G L parts f S y ⊆ + candidates G L parts (Function.update f x v) (insert x S) y := by + intro w hw + simp only [candidates, mem_filter, mem_insert] at hw ⊢ + refine ⟨hw.1, ?_⟩ + rintro z (rfl | hz) hzy + · exact absurd hzy hxy + · rw [hfS z hz]; exact hw.2 z hz hzy + calc d ^ #S * d * (#(parts y) : ℝ) ≤ d ^ #S * 1 * #(parts y) := by gcongr + _ = d ^ #S * #(parts y) := by ring + _ ≤ _ := hcand y hy.2 + _ ≤ _ := by exact_mod_cast card_le_card hsub + +end PartialEmbedding diff --git a/LeanPool/RemovalExtremalStability/StabilityGeneral.lean b/LeanPool/RemovalExtremalStability/StabilityGeneral.lean new file mode 100644 index 000000000..2998ee6f9 --- /dev/null +++ b/LeanPool/RemovalExtremalStability/StabilityGeneral.lean @@ -0,0 +1,194 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Triangle.Removal +public import Mathlib.Combinatorics.SimpleGraph.Extremal.Turan +public import Mathlib.Tactic +public import LeanPool.RemovalExtremalStability.Furedi +public import LeanPool.RemovalExtremalStability.CliqueRemoval +public import LeanPool.RemovalExtremalStability.Embedding + +/-! + +Adapted from [jtraverso/turan-stability](https://github.com/jtraverso/turan-stability/blob/3eb99033cc931add291781f77b7446dcba8f5f9d/StabilityLib/StabilityGeneral.lean) (Palomar-registered source). +# The Erdős–Simonovits stability theorem + +**Erdős–Simonovits stability theorem** (Erdős 1967, Simonovits 1968), in the form derived by +Füredi (2015) from the regularity method: let `L` be a finite graph with chromatic number at most +`p + 1` (i.e. `L.Colorable (p + 1)`). For every `ε > 0` there are `δ > 0` and `n₀` such that every +`L`-free graph on `n ≥ n₀` vertices with at least `(1 - 1/p) n² / 2 - δ n²` edges differs from +some complete `p`-partite graph on the same vertices in at most `ε n²` edges. + +The proof combines Szemerédi's regularity lemma (through the reduced graph of +`StabilityLib/CliqueRemoval.lean`), the embedding lemma `Embedding.exists_embedding_of_isUniform` +(the reduced graph of an `L`-free graph is `K_{p+1}`-free) and Füredi's theorem +`Furedi.exists_partition_symmDiff_le` applied to the reduced graph. + +`ErdosSimonovits.stability`: the theorem above. The complete `p`-partite graph with parts the +fibres of `f : W → Fin p` is `(⊤ : SimpleGraph (Fin p)).comap f`; `L ⊑ G` is Mathlib's +`SimpleGraph.IsContained`. +-/ + +@[expose] public section + +open Finset Fintype SimpleGraph + +namespace ErdosSimonovits + +/-- The reduced graph of an `L`-free graph is `K_r`-free, provided `L` is properly +`r`-coloured and the parameters allow the embedding lemma. -/ +theorem regularityReduced_cliqueFree {α : Type*} [Fintype α] [DecidableEq α] + (G : SimpleGraph α) [DecidableRel G.Adj] {β : Type*} [Fintype β] (L : SimpleGraph β) + {r : ℕ} (c : β → Fin r) (hc : ∀ x y, L.Adj x y → c x ≠ c y) + {P : Finpartition (univ : Finset α)} {B : ℕ} {η d ε : ℝ} (hη : 0 < η) (hd : 0 < d) + (hd₁ : d ≤ 1) (hηd : 2 * card β * η ≤ d ^ card β) (hdη : d + η ≤ ε / 4) + (hP₁ : P.IsEquipartition) (hP₃ : #P.parts ≤ B) + (hsize : 2 * card β ≤ d ^ card β * (card α / (2 * B : ℝ))) (hL : ¬ L.IsContained G) : + (G.regularityReduced P η (ε / 4)).CliqueFree r := by + intro t ht + let e := t.equivFin + let v : Fin r → α := fun i ↦ (e.symm (Fin.cast ht.card_eq.symm i) : α) + have hv : ∀ i j, i ≠ j → (G.regularityReduced P η (ε / 4)).Adj (v i) (v j) := by + intro i j hij + refine ht.isClique (e.symm _).2 (e.symm _).2 ?_ + intro h + apply hij + have := e.symm.injective (Subtype.ext h) + exact Fin.cast_injective _ this + let U : Fin r → Finset α := fun i ↦ P.part (v i) + have key : ∀ i j, i ≠ j → G.IsUniform η (U i) (U j) ∧ ε / 4 ≤ G.edgeDensity (U i) (U j) := by + intro i j hij + obtain ⟨-, X, hX, Y, hY, hxX, hyY, -, hu, hdens⟩ := hv i j hij + have h1 : U i = X := P.part_eq_of_mem hX hxX + have h2 : U j = Y := P.part_eq_of_mem hY hyY + rw [h1, h2] + exact ⟨hu, hdens⟩ + refine hL (Embedding.isContained_of_isUniform G L c hc U hη hd hd₁ hηd (fun i ↦ ?_) + (fun i j hij ↦ (key i j hij).1) (fun i j hij ↦ hdη.trans (key i j hij).2)) + refine hsize.trans ?_ + gcongr + exact CliqueRemoval.card_bound hP₁ hP₃ (P.part_mem.2 (mem_univ _)) + +/-- Edit distance to `K` grows by at most the number of deleted edges when passing from a +subgraph `G'` to `G`. -/ +theorem ncard_symmDiff_le {W : Type*} [Finite W] {G G' : SimpleGraph W} (h : G' ≤ G) + (K : SimpleGraph W) : + (symmDiff G K).edgeSet.ncard ≤ + (symmDiff G' K).edgeSet.ncard + (G.edgeSet.ncard - G'.edgeSet.ncard) := by + have hle : symmDiff G K ≤ symmDiff G' K ⊔ (G \ G') := by + intro x y hxy + simp only [symmDiff_def, sup_adj, sdiff_adj] at hxy ⊢ + by_cases h1 : G'.Adj x y + · have := h h1 + tauto + · rcases hxy with hxy | hxy + · tauto + · exact Or.inl (Or.inr ⟨hxy.1, fun h2 ↦ hxy.2 (h h2)⟩) + calc (symmDiff G K).edgeSet.ncard ≤ (symmDiff G' K ⊔ (G \ G')).edgeSet.ncard := + Set.ncard_le_ncard (edgeSet_mono hle) (Set.toFinite _) + _ ≤ (symmDiff G' K).edgeSet.ncard + (G \ G').edgeSet.ncard := by + rw [edgeSet_sup]; exact Set.ncard_union_le _ _ + _ = _ := by + rw [edgeSet_sdiff, Set.ncard_sdiff (edgeSet_mono h) (Set.toFinite _)] + +/-- **Erdős–Simonovits stability theorem.** Let `L` be a finite graph that is +`(p + 1)`-colourable. For every `ε > 0` there are `δ > 0` and `n₀` such that every graph `G` on +`n ≥ n₀` vertices that does not contain `L` and has at least `(1 - 1/p) n² / 2 - δ n²` edges +differs from some complete `p`-partite graph on the same vertices in at most `ε n²` edges. -/ +theorem stability {β : Type} [Finite β] (L : SimpleGraph β) {p : ℕ} (hp : 0 < p) + (hL : L.Colorable (p + 1)) {ε : ℝ} (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∃ n₀ : ℕ, ∀ (W : Type) [Fintype W] (G : SimpleGraph W), n₀ ≤ card W → + ¬ L.IsContained G → + (1 - 1 / (p : ℝ)) * (card W : ℝ) ^ 2 / 2 - δ * (card W : ℝ) ^ 2 ≤ G.edgeSet.ncard → + ∃ f : W → Fin p, + ((symmDiff G ((⊤ : SimpleGraph (Fin p)).comap f)).edgeSet.ncard : ℝ) ≤ + ε * (card W : ℝ) ^ 2 := by + classical + have := Fintype.ofFinite β + set k := card β with hk_def + have C : L.Coloring (Fin (p + 1)) := hL.some + set ε' : ℝ := min ε 1 with hε'_def + have hε' : 0 < ε' := lt_min hε one_pos + have hε'ε : ε' ≤ ε := min_le_left _ _ + have hε'1 : ε' ≤ 1 := min_le_right _ _ + set ε₁ : ℝ := ε' / 8 with hε₁_def + have hε₁ : 0 < ε₁ := by positivity + set d : ℝ := ε₁ / 8 with hd_def + have hd : 0 < d := by positivity + have hd₁ : d ≤ 1 := by linarith + set η : ℝ := min (ε₁ / 8) (d ^ k / (2 * k + 1)) with hη_def + have hη : 0 < η := lt_min (by positivity) (by positivity) + have hηε : η ≤ ε₁ / 8 := min_le_left _ _ + have hηd : 2 * k * η ≤ d ^ k := by + have h1 : η ≤ d ^ k / (2 * k + 1) := min_le_right _ _ + have hp : 0 < d ^ k := by positivity + rw [le_div_iff₀ (by positivity)] at h1 + nlinarith + have hdη : d + η ≤ ε₁ / 4 := by linarith + set l : ℕ := ⌈4 / ε₁⌉₊ with hl_def + have hl : 4 / ε₁ ≤ l := Nat.le_ceil _ + set B : ℕ := SzemerediRegularity.bound η l with hB_def + have hB : (0 : ℝ) < B := by positivity + refine ⟨ε / 12, by positivity, max (l + 1) (⌈2 * B * (2 * k / d ^ k)⌉₊ + 1), ?_⟩ + intro W _ G hn hLG hedge + set n := card W with hn_def + have hn1 : l + 1 ≤ n := (le_max_left _ _).trans hn + have hn2 : ⌈2 * B * (2 * k / d ^ k)⌉₊ + 1 ≤ n := (le_max_right _ _).trans hn + have : Nonempty W := Fintype.card_pos_iff.1 (by omega) + obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := szemeredi_regularity G hη (show l ≤ card W by omega) + have hP' : 4 / ε₁ ≤ #P.parts := hl.trans (Nat.cast_le.2 hP₂) + have hrem := CliqueRemoval.regularityReduced_edges_card_aux' hε₁ hη hηε hP₁ hP₄ hP' + set G' := G.regularityReduced P η (ε₁ / 4) with hG'_def + have hG'G : G' ≤ G := regularityReduced_le + have hsize : 2 * (k : ℝ) ≤ d ^ k * (n / (2 * B : ℝ)) := by + have h1 : 2 * B * (2 * k / d ^ k) < (n : ℝ) := by + have := Nat.lt_of_ceil_lt (show ⌈2 * B * (2 * k / d ^ k)⌉₊ < n by omega) + exact this + have hdk : 0 < d ^ k := by positivity + rw [mul_div_assoc', le_div_iff₀ (by positivity)] + rw [mul_div_assoc', div_lt_iff₀ hdk] at h1 + nlinarith + have hfree : G'.CliqueFree (p + 1) := + regularityReduced_cliqueFree G L C (fun x y h ↦ C.valid h) hη hd hd₁ hηd hdη hP₁ hP₃ + hsize hLG + set T := turanNumber n p + set e' := G'.edgeSet.ncard + set e := G.edgeSet.ncard + obtain ⟨f, -, h2⟩ := Furedi.exists_partition_symmDiff_le G' hp hfree (t := T - e') le_add_tsub + refine ⟨f, ?_⟩ + have h3 := ncard_symmDiff_le hG'G ((⊤ : SimpleGraph (Fin p)).comap f) + have hee : e' ≤ e := Set.ncard_le_ncard (edgeSet_mono hG'G) (Set.toFinite _) + have hrem' : (e : ℝ) - e' < ε₁ * (n : ℝ) ^ 2 := by + have he : e = #G.edgeFinset := by rw [← Set.ncard_coe_finset, coe_edgeFinset] + have he' : e' = #G'.edgeFinset := by rw [← Set.ncard_coe_finset, coe_edgeFinset] + rw [he, he'] + push_cast at hrem + exact hrem + have hT : (T : ℝ) ≤ (1 - 1 / (p : ℝ)) * (n : ℝ) ^ 2 / 2 := by + have h := mul_turanNumber_le (r := p) (n := n) + have hp' : (0 : ℝ) < p := by exact_mod_cast hp + have hc : (2 * p * T : ℝ) ≤ ((p : ℝ) - 1) * (n : ℝ) ^ 2 := by + have := (Nat.cast_le (α := ℝ)).mpr h + push_cast [Nat.cast_sub (show 1 ≤ p from hp)] at this + exact this + rw [show (1 - 1 / (p : ℝ)) * (n : ℝ) ^ 2 / 2 = ((p - 1) * (n : ℝ) ^ 2) / (2 * p) by + field_simp] + rw [le_div_iff₀ (by positivity)] + linarith + have ht : ((T - e' : ℕ) : ℝ) ≤ ε / 12 * (n : ℝ) ^ 2 + ε₁ * (n : ℝ) ^ 2 := by + rcases le_total T e' with h | h + · rw [Nat.sub_eq_zero_of_le h, Nat.cast_zero]; positivity + · rw [Nat.cast_sub h]; linarith + have h4 : ((symmDiff G ((⊤ : SimpleGraph (Fin p)).comap f)).edgeSet.ncard : ℝ) ≤ + 3 * ((T - e' : ℕ) : ℝ) + ((e - e' : ℕ) : ℝ) := by + exact_mod_cast h3.trans (Nat.add_le_add_right h2 _) + rw [Nat.cast_sub hee] at h4 + have hn0 : (0 : ℝ) ≤ (n : ℝ) ^ 2 := by positivity + have : ε₁ * (n : ℝ) ^ 2 ≤ ε / 8 * (n : ℝ) ^ 2 := by gcongr; linarith + nlinarith + +end ErdosSimonovits diff --git a/LeanPool/RemovalExtremalStability/TuranStability.lean b/LeanPool/RemovalExtremalStability/TuranStability.lean new file mode 100644 index 000000000..a4e37bc56 --- /dev/null +++ b/LeanPool/RemovalExtremalStability/TuranStability.lean @@ -0,0 +1,204 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Extremal.Turan +public import Mathlib.Tactic +public import LeanPool.RemovalExtremalStability.StabilityGeneral + +/-! + +Adapted from [jtraverso/turan-stability](https://github.com/jtraverso/turan-stability/blob/3eb99033cc931add291781f77b7446dcba8f5f9d/Solution.lean) (Palomar-registered source). +# Proofs of the statements in `Challenge.lean` + +The proofs are in `StabilityLib/`: `Furedi.lean` (Füredi's greedy maximum-degree partition and +Mathlib's Turán bound), `CliqueCounting.lean` (induction on the clique size with good +neighbourhoods, generalising Mathlib's triangle counting lemma), `CliqueRemoval.lean` (Szemerédi's +regularity lemma and Mathlib's reduced graph, generalising Mathlib's triangle removal lemma), +`Embedding.lean` (greedy embedding) and `StabilityGeneral.lean` (the reduced graph of an `L`-free +graph is `K_{p+1}`-free by the embedding lemma, and Füredi's theorem applied to it). +-/ + +@[expose] public section + +open Finset Fintype SimpleGraph + +namespace TuranStability + +section Furedi + +variable {V : Type*} [Fintype V] + +/-- **Füredi's partition inequality.** Every `K_{p+1}`-free finite graph has a partition into +`p` parts (the fibres of `f`) such that the number of edges of `G` plus the number of edges of +`G` inside the parts is at most the number of edges of the complete `p`-partite graph on these +parts. -/ +theorem card_edgeSet_add_le {W : Type*} [Finite W] (G : SimpleGraph W) {p : ℕ} (hp : 0 < p) + (hG : G.CliqueFree (p + 1)) : + ∃ f : W → Fin p, G.edgeSet.ncard + (G \ (⊤ : SimpleGraph (Fin p)).comap f).edgeSet.ncard ≤ + ((⊤ : SimpleGraph (Fin p)).comap f).edgeSet.ncard := + _root_.Furedi.card_edgeSet_add_le G hp hG + +/-- **Füredi's theorem (2015).** If `G` is a `K_{p+1}`-free graph on `n` vertices with at least +`turanNumber n p - t` edges, then `G` has a `p`-colourable (i.e. `p`-partite) subgraph `H` with +at least `e(G) - t` edges. -/ +theorem furedi (G : SimpleGraph V) {p t : ℕ} (hp : 0 < p) (hG : G.CliqueFree (p + 1)) + (ht : turanNumber (card V) p ≤ G.edgeSet.ncard + t) : + ∃ H : SimpleGraph V, H ≤ G ∧ H.Colorable p ∧ G.edgeSet.ncard ≤ H.edgeSet.ncard + t := + _root_.Furedi.furedi G hp hG ht + +/-- **Füredi's theorem, edit-distance form.** Under the hypotheses of `furedi`, there is a +partition into `p` parts with at most `t` edges of `G` inside the parts, and `G` differs from the +complete `p`-partite graph on these parts in at most `3 t` edges. -/ +theorem exists_partition_symmDiff_le (G : SimpleGraph V) {p t : ℕ} (hp : 0 < p) + (hG : G.CliqueFree (p + 1)) (ht : turanNumber (card V) p ≤ G.edgeSet.ncard + t) : + ∃ f : V → Fin p, (G \ (⊤ : SimpleGraph (Fin p)).comap f).edgeSet.ncard ≤ t ∧ + (symmDiff G ((⊤ : SimpleGraph (Fin p)).comap f)).edgeSet.ncard ≤ 3 * t := + _root_.Furedi.exists_partition_symmDiff_le G hp hG ht + +/-- **Erdős–Simonovits stability theorem for cliques** (Erdős 1967, Simonovits 1968), in the +form obtained from Füredi's theorem: for every `ε > 0` there is `δ > 0` such that every +`K_{p+1}`-free graph on `n` vertices with at least `(1 - 1/p) n² / 2 - δ n²` edges differs from +some complete `p`-partite graph on the same vertices in at most `ε n²` edges. -/ +theorem erdos_simonovits_stability {p : ℕ} (hp : 0 < p) {ε : ℝ} (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∀ (W : Type) [Fintype W] (G : SimpleGraph W), G.CliqueFree (p + 1) → + (1 - 1 / (p : ℝ)) * (card W : ℝ) ^ 2 / 2 - δ * (card W : ℝ) ^ 2 ≤ G.edgeSet.ncard → + ∃ f : W → Fin p, + ((symmDiff G ((⊤ : SimpleGraph (Fin p)).comap f)).edgeSet.ncard : ℝ) ≤ + ε * (card W : ℝ) ^ 2 := + _root_.Furedi.erdos_simonovits_stability hp hε + +end Furedi + +section CliqueCounting + +variable {α : Type*} (G : SimpleGraph α) [DecidableRel G.Adj] + +/-- **Clique counting lemma, robust-density form.** If any two of the parts `s i`, `s j` +(`i ≠ j`) have edge density at least `d` between all subsets of relative size at least `η`, +`η ≤ 1` and `2 r η ≤ d ^ (r - 1)`, then at least `d ^ (r choose 2) / 2 ^ r` of the tuples in +`∏ i, s i` are cliques. (Without `η ≤ 1` the hypothesis on subsets would be vacuous.) -/ +theorem card_transversalCliques_ge {r : ℕ} (s : Fin r → Finset α) {η d : ℝ} (hη : 0 < η) + (hη₁ : η ≤ 1) (hd : 0 < d) (hηd : 2 * r * η ≤ d ^ (r - 1)) + (hs : ∀ i j, i ≠ j → ∀ A ⊆ s i, ∀ B ⊆ s j, η * #(s i) ≤ #A → η * #(s j) ≤ #B → + d ≤ G.edgeDensity A B) : + d ^ r.choose 2 / 2 ^ r * ∏ i, (#(s i) : ℝ) ≤ + #{x ∈ Fintype.piFinset s | ∀ i j, i ≠ j → G.Adj (x i) (x j)} := + _root_.CliqueCounting.card_transversalCliques_ge G s hη hη₁ hd hηd hs + +/-- **Clique counting lemma, uniform form.** If every pair of distinct parts is `ε`-uniform with +edge density at least `d + ε`, and `2 r ε ≤ d ^ (r - 1)`, then at least +`d ^ (r choose 2) / 2 ^ r` of the tuples in `∏ i, s i` are cliques. -/ +theorem card_transversalCliques_ge_of_isUniform {r : ℕ} (s : Fin r → Finset α) {ε d : ℝ} + (hε : 0 < ε) (hd : 0 < d) (hεd : 2 * r * ε ≤ d ^ (r - 1)) + (hu : ∀ i j, i ≠ j → G.IsUniform ε (s i) (s j)) + (hdens : ∀ i j, i ≠ j → d + ε ≤ G.edgeDensity (s i) (s j)) : + d ^ r.choose 2 / 2 ^ r * ∏ i, (#(s i) : ℝ) ≤ + #{x ∈ Fintype.piFinset s | ∀ i j, i ≠ j → G.Adj (x i) (x j)} := + _root_.CliqueCounting.card_transversalCliques_ge_of_isUniform G s hε hd hεd hu hdens + +/-- **Clique counting lemma.** If `s : Fin r → Finset α` are pairwise disjoint sets of vertices, +every two of them `ε`-uniform with edge density at least `d + ε`, and `2 r ε ≤ d ^ (r - 1)`, +then `G` has at least `d ^ (r choose 2) / 2 ^ r · ∏ i, #(s i)` cliques of size `r`. -/ +theorem card_cliqueFinset_ge [Fintype α] [DecidableEq α] {r : ℕ} (s : Fin r → Finset α) + {ε d : ℝ} (hε : 0 < ε) (hd : 0 < d) (hεd : 2 * r * ε ≤ d ^ (r - 1)) + (hdisj : ∀ i j, i ≠ j → Disjoint (s i) (s j)) + (hu : ∀ i j, i ≠ j → G.IsUniform ε (s i) (s j)) + (hdens : ∀ i j, i ≠ j → d + ε ≤ G.edgeDensity (s i) (s j)) : + d ^ r.choose 2 / 2 ^ r * ∏ i, (#(s i) : ℝ) ≤ #(G.cliqueFinset r) := + _root_.CliqueCounting.card_cliqueFinset_ge G s hε hd hεd hdisj hu hdens + +end CliqueCounting + +section CliqueRemoval + +/-- **Clique removal lemma, far form.** For every `r` and `ε > 0` there is `δ > 0` such that a +finite graph on `n` vertices that is `ε n²`-far from being `K_r`-free (in the sense of Mathlib's +`SimpleGraph.DeleteFar`) has at least `δ n^r` cliques of size `r`. -/ +theorem le_card_cliqueFinset_of_deleteFar (r : ℕ) {ε : ℝ} (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∀ (α : Type) [Fintype α] [DecidableEq α] (G : SimpleGraph α) + [DecidableRel G.Adj], G.DeleteFar (fun H ↦ H.CliqueFree r) (ε * (card α ^ 2 : ℕ)) → + δ * card α ^ r ≤ #(G.cliqueFinset r) := + _root_.CliqueRemoval.le_card_cliqueFinset_of_deleteFar r hε + +/-- **Clique removal lemma.** For every `r` and `ε > 0` there is `δ > 0` such that every finite +graph on `n` vertices with fewer than `δ n^r` cliques of size `r` has a `K_r`-free subgraph +obtained by deleting fewer than `ε n²` edges. -/ +theorem clique_removal (r : ℕ) {ε : ℝ} (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∀ (α : Type) [Fintype α] [DecidableEq α] (G : SimpleGraph α) + [DecidableRel G.Adj], (#(G.cliqueFinset r) : ℝ) < δ * card α ^ r → + ∃ G' ≤ G, ∃ _ : DecidableRel G'.Adj, + (#G.edgeFinset - #G'.edgeFinset : ℝ) < ε * (card α ^ 2 : ℕ) ∧ G'.CliqueFree r := + _root_.CliqueRemoval.clique_removal r hε + +end CliqueRemoval + +section Embedding + +variable {α : Type*} (G : SimpleGraph α) [DecidableRel G.Adj] + +/-- **Embedding lemma, robust-density form.** Let `L` be a graph on a finite type `β` with +`k = card β` vertices and a proper colouring `c : β → Fin r`. Suppose that for all colours +`i ≠ j`, all subsets `A ⊆ s i`, `B ⊆ s j` with `#A ≥ η #(s i)` and `#B ≥ η #(s j)` have edge +density at least `d`, where `0 < η ≤ 1`, `0 < d ≤ 1`, `2 k η ≤ d ^ k`, and every part has at least +`2 k / d ^ k` vertices. Then there is an injective map `f : β → α` sending each `x` into `s (c x)` +and edges of `L` to edges of `G`. -/ +theorem exists_embedding {β : Type*} [Fintype β] (L : SimpleGraph β) {r : ℕ} + (c : β → Fin r) (hc : ∀ x y, L.Adj x y → c x ≠ c y) (s : Fin r → Finset α) {η d : ℝ} + (hη : 0 < η) (hη₁ : η ≤ 1) (hd : 0 < d) (hd₁ : d ≤ 1) + (hηd : 2 * card β * η ≤ d ^ card β) (hsize : ∀ i, 2 * card β ≤ d ^ card β * #(s i)) + (hs : ∀ i j, i ≠ j → ∀ A ⊆ s i, ∀ B ⊆ s j, η * #(s i) ≤ #A → η * #(s j) ≤ #B → + d ≤ G.edgeDensity A B) : + ∃ f : β → α, Function.Injective f ∧ (∀ x, f x ∈ s (c x)) ∧ + ∀ x y, L.Adj x y → G.Adj (f x) (f y) := + _root_.Embedding.exists_embedding G L c hc s hη hη₁ hd hd₁ hηd hsize hs + +/-- **Embedding lemma, uniform form.** Under the hypotheses of `exists_embedding`, with the +robust density condition replaced by: every pair of distinct parts is `ε`-uniform with edge +density at least `d + ε`, and `2 k ε ≤ d ^ k`. -/ +theorem exists_embedding_of_isUniform {β : Type*} [Fintype β] + (L : SimpleGraph β) {r : ℕ} (c : β → Fin r) (hc : ∀ x y, L.Adj x y → c x ≠ c y) + (s : Fin r → Finset α) {ε d : ℝ} (hε : 0 < ε) (hd : 0 < d) (hd₁ : d ≤ 1) + (hεd : 2 * card β * ε ≤ d ^ card β) (hsize : ∀ i, 2 * card β ≤ d ^ card β * #(s i)) + (hu : ∀ i j, i ≠ j → G.IsUniform ε (s i) (s j)) + (hdens : ∀ i j, i ≠ j → d + ε ≤ G.edgeDensity (s i) (s j)) : + ∃ f : β → α, Function.Injective f ∧ (∀ x, f x ∈ s (c x)) ∧ + ∀ x y, L.Adj x y → G.Adj (f x) (f y) := + _root_.Embedding.exists_embedding_of_isUniform G L c hc s hε hd hd₁ hεd hsize hu hdens + +/-- **Embedding lemma, containment form.** Under the hypotheses of +`exists_embedding_of_isUniform`, `L` is contained in `G` (`L ⊑ G`, Mathlib's +`SimpleGraph.IsContained`). -/ +theorem isContained_of_isUniform {β : Type*} [Fintype β] + (L : SimpleGraph β) {r : ℕ} (c : β → Fin r) (hc : ∀ x y, L.Adj x y → c x ≠ c y) + (s : Fin r → Finset α) {ε d : ℝ} (hε : 0 < ε) (hd : 0 < d) (hd₁ : d ≤ 1) + (hεd : 2 * card β * ε ≤ d ^ card β) (hsize : ∀ i, 2 * card β ≤ d ^ card β * #(s i)) + (hu : ∀ i j, i ≠ j → G.IsUniform ε (s i) (s j)) + (hdens : ∀ i j, i ≠ j → d + ε ≤ G.edgeDensity (s i) (s j)) : + L.IsContained G := + _root_.Embedding.isContained_of_isUniform G L c hc s hε hd hd₁ hεd hsize hu hdens + +end Embedding + +section ErdosSimonovits + +/-- **Erdős–Simonovits stability theorem.** Let `L` be a finite graph that is +`(p + 1)`-colourable. For every `ε > 0` there are `δ > 0` and `n₀` such that every graph `G` on +`n ≥ n₀` vertices that does not contain `L` and has at least `(1 - 1/p) n² / 2 - δ n²` edges +differs from some complete `p`-partite graph on the same vertices in at most `ε n²` edges. -/ +theorem stability {β : Type} [Finite β] (L : SimpleGraph β) {p : ℕ} (hp : 0 < p) + (hL : L.Colorable (p + 1)) {ε : ℝ} (hε : 0 < ε) : + ∃ δ : ℝ, 0 < δ ∧ ∃ n₀ : ℕ, ∀ (W : Type) [Fintype W] (G : SimpleGraph W), n₀ ≤ card W → + ¬ L.IsContained G → + (1 - 1 / (p : ℝ)) * (card W : ℝ) ^ 2 / 2 - δ * (card W : ℝ) ^ 2 ≤ G.edgeSet.ncard → + ∃ f : W → Fin p, + ((symmDiff G ((⊤ : SimpleGraph (Fin p)).comap f)).edgeSet.ncard : ℝ) ≤ + ε * (card W : ℝ) ^ 2 := + _root_.ErdosSimonovits.stability L hp hL hε + +end ErdosSimonovits + +end TuranStability diff --git a/LeanPool/projects/graph-removal-extremal-stability.yaml b/LeanPool/projects/graph-removal-extremal-stability.yaml new file mode 100644 index 000000000..5de19614f --- /dev/null +++ b/LeanPool/projects/graph-removal-extremal-stability.yaml @@ -0,0 +1,49 @@ +slug: graph-removal-extremal-stability +title: Graph removal and extremal stability +summary: Formalizes the graph removal lemma for every fixed graph, Füredi's sharp + stability inequality and Erdős–Simonovits stability for colourable forbidden + graphs. A bridge theorem shows that near-extremal graphs with few labelled + forbidden copies are close to a complete multipartite graph. +branch: graph theory +entry_module: LeanPool.RemovalExtremalStability +authors: +- Juan Pablo Traverso Gianini +source: + title: Füredi and Erdős–Simonovits stability; general graph removal lemma + authors: + - Juan Pablo Traverso Gianini + url: https://github.com/jtraverso/turan-stability + github_repo: jtraverso/turan-stability + commit: 3eb99033cc931add291781f77b7446dcba8f5f9d +license: Apache-2.0 +status: verified +provenance: AI +main_declarations: +- TuranStability.stability +- RemovalLemma.graph_removal +main_results: +- declaration: TuranStability.furedi + informal: A clique-free graph near Turán's edge bound has a large colourable subgraph. + source_ref: Füredi's stability theorem. +- declaration: TuranStability.stability + informal: An L-free graph near the Turán density for a (p+1)-colourable L is + close in edit distance to a complete p-partite graph. + source_ref: Erdős–Simonovits stability theorem. +- declaration: RemovalLemma.graph_removal + informal: Few labelled copies of any fixed graph H can be destroyed by deleting + few edges. + source_ref: Conlon–Fox, Graph removal lemmas, Theorem 1.1 + (https://arxiv.org/pdf/1211.3487v1); Erdős–Frankl–Rödl (1986), Theorems 1.5 + and 1.5′, are related precursors; formal source + https://github.com/jtraverso/graph-removal-lemma/tree/589cf03ef1e4c80ea8cdd6be77778232c62dd37c. +- declaration: RemovalExtremalStability.stability_of_few_copies + informal: A graph near the Turán density with few labelled L copies is close + in edit distance to a complete multipartite graph. +tags: +- graph-theory +- graph-removal +- extremal-graph-theory +- stability +- regularity +msc: +- 05C35