Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/Densification/Full.lean
1import Catalog.Sparsity.ShallowMinor.Full
2import Catalog.Sparsity.ChernoffBound.Full
3import Mathlib.Combinatorics.SimpleGraph.Finite
4import Mathlib.Analysis.SpecialFunctions.Log.Basic
5import Mathlib.Analysis.SpecialFunctions.Pow.Real
6import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
7import Mathlib.MeasureTheory.Constructions.Pi
8import Mathlib.MeasureTheory.Integral.Bochner.Set
9import Mathlib.Probability.Independence.Basic
10import Mathlib.Probability.ProbabilityMassFunction.Integrals
11
12open Catalog.Sparsity.ShallowMinor Real Filter Finset MeasureTheory ProbabilityTheory PMF NNReal
13
14namespace Catalog.Sparsity.Densification
15
16/-!
17## Proof structure
18
19The proof of `densification` follows Lemma 3.4 of the source, broken into:
20
211. `exists_good_pair` (probabilistic core): For large n, any graph with
22 min degree ≥ n^ε has disjoint A, B ⊆ V with |A| ∈ [n^{1-ε}, 3n^{1-ε} log n],
23 |B| ≥ n/2, and every b ∈ B having ≥ log n neighbors in A.
24 Proof uses Chernoff bounds on Bernoulli sums (not yet in Mathlib).
25
262. `greedy_densify` (graph construction): Given (A, B) as above, the
27 greedy process either finds K_{t+1} ≼₁ G for t ≥ log n, or builds a
28 depth-1 minor G' on vertex set A with ≥ |B| edges.
29 Each step: if N(b) ∩ A is a clique, use b to extend to a clique of size
30 |N(b) ∩ A| + 1 ≥ log n + 1; else contract b onto some a ∈ N(b) ∩ A,
31 adding an edge to G'[A]. Branch sets: {a} ∪ {contracted b's}, depth 1.
32
333. `edge_density_bound` (arithmetic): From n' = |A| ≤ 3n^{1-ε} log n
34 and n/2 ≤ edges, deduce (n')^{1+ε+ε²} ≤ edges for large n.
35 Proof: (n')^{1+ε+ε²} ≤ C · n^{1-ε³} · (log n)^{1+ε+ε²} ≤ n/2,
36 where the last step uses n^{ε³} dominates (log n)^{1+ε+ε²}
37 (from `isLittleO_log_rpow_rpow_atTop` with exponent ε³ > 0).
38-/
39
40/-- Under the product Bernoulli(p) measure on V → Bool,
41the indicator 𝟙[ω v = true] has mean p. -/
42private lemma pi_bernoulli_indicator_mean {V : Type} [DecidableEq V] [Fintype V]
43 {p : ℝ≥0} (hp : p ≤ 1) (v : V) :
44 ∫ (ω : V → Bool), (if ω v then (1 : ℝ) else 0)
45 ∂(Measure.pi (fun _ : V => (bernoulli p hp).toMeasure)) = p.toReal := by
46 -- Reduce to the single-factor Bernoulli integral via measure pushforward.
47 have step1 : ∫ (ω : V → Bool), (if ω v then (1 : ℝ) else 0)
48 ∂(Measure.pi (fun _ : V => (bernoulli p hp).toMeasure)) =
49 ∫ (b : Bool), (if b then (1 : ℝ) else 0) ∂(bernoulli p hp).toMeasure := by
50 conv_rhs => rw [← (measurePreserving_eval (μ := fun _ : V => (bernoulli p hp).toMeasure) v).map_eq]
51 exact (integral_map_of_stronglyMeasurable
52 (measurable_pi_apply (X := fun _ : V => Bool) v)
53 (measurable_of_countable (fun b : Bool => if b then (1:ℝ) else 0)).stronglyMeasurable).symm
54 rw [step1]
55 simp_rw [show (fun b : Bool => if b then (1 : ℝ) else 0) = fun b => cond b 1 0 from
56 funext fun b => by cases b <;> rfl]
57 exact bernoulli_expectation hp
58
59/-- Under the product Bernoulli(p) measure on V → Bool, the indicators 𝟙[ω v = true]
60for v : V are independent random variables (V → Bool) → ℝ. -/
61private lemma pi_bernoulli_iIndepFun {V : Type} [DecidableEq V] [Fintype V]
62 {p : ℝ≥0} (hp : p ≤ 1) :
63 iIndepFun (fun (v : V) (ω : V → Bool) => if ω v then (1 : ℝ) else 0)
64 (Measure.pi (fun _ : V => (bernoulli p hp).toMeasure)) :=
65 iIndepFun_pi (fun _ => (measurable_of_countable
66 (fun b : Bool => if b then (1 : ℝ) else 0)).aemeasurable)
67
68/-- **Step 1 (probabilistic core)**: For large n, a min-degree-n^ε graph has
69a "good pair" (A, B): disjoint vertex subsets with |A| in [n^{1-ε}, 3n^{1-ε} log n],
70|B| ≥ n/2, and every b ∈ B having ≥ log n neighbors in A.
71
72Source proof: sample each vertex with probability p = 2 log n / n^ε independently.
73For large n, p ∈ (0,1). Let A = sampled set, B = {v ∉ A | |N(v) ∩ A| ≥ log n}.
74- Chernoff (upper + lower tail) on |A| = ∑_v Bernoulli(p): since μ = np = 2n^{1-ε} log n,
75 P(|A| ∉ [n^{1-ε} log n, 3n^{1-ε} log n]) ≤ 2 exp(-n^{1-ε} log n / 6) → 0.
76- For each v with deg v ≥ n^ε: μ_v = deg(v) · p ≥ 2 log n, so by Chernoff lower tail,
77 P(|N(v) ∩ A| < log n) ≤ exp(-log n / 6) = n^{-1/6}.
78- Since p = 2 log n / n^ε → 0, P(v ∈ A) = p → 0 too.
79 So P(v ∉ B) ≤ p + n^{-1/6} → 0. For large n, P(v ∉ B) ≤ 1/6.
80- By linearity of expectation: E[|V \ B|] ≤ n/6.
81- By Markov: P(|B| ≥ n/2) ≥ 1 - P(|V \ B| ≥ n/2) ≥ 1 - 1/3 = 2/3.
82- Both events (good A size, |B| ≥ n/2) hold simultaneously with probability ≥ 2/3 + 3/4 - 1 > 0.
83- By the probabilistic method, a good (A, B) pair exists.
84
85Uses `Catalog.Sparsity.ChernoffBound.chernoffBound` applied twice (once for |A|, once per vertex
86for the neighbor count). The indicator variables X_v = 𝟙[ω v = true] are i.i.d. Bernoulli(p)
87under `Measure.pi (fun _ : V => (PMF.bernoulli p_nnr hp_nnr).toMeasure)`, with independence
88from `iIndepFun_pi` and mean from `bernoulli_expectation` + `measurePreserving_eval`. -/
89private lemma exists_good_pair (ε : ℝ) (hε_pos : 0 < ε) (hε_le : ε ≤ 2 / 3) :
90 ∃ M : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V]
91 (G : SimpleGraph V) [DecidableRel G.Adj],
92 M ≤ Fintype.card V →
93 (∀ v : V, (Fintype.card V : ℝ) ^ ε ≤ ↑(G.degree v)) →
94 ∃ (A B : Finset V), Disjoint A B ∧
95 (Fintype.card V : ℝ) ^ (1 - ε) ≤ ↑A.card ∧
96 (↑A.card : ℝ) ≤ 3 * (Fintype.card V : ℝ) ^ (1 - ε) * log ↑(Fintype.card V) ∧
97 (Fintype.card V : ℝ) / 2 ≤ ↑B.card ∧
98 ∀ b ∈ B, log ↑(Fintype.card V) ≤ ↑(G.neighborFinset b ∩ A).card := by
99 -- ======================== THRESHOLD SELECTION ========================
100 -- We need n large enough that:
101 -- (A) p_n := 2 * log n / n^ε is a valid probability in (0,1)
102 -- (B) The Chernoff bound gives < 1/4 error for |A|
103 -- (C) Bad-vertex probability p_n + n^{-1/6} ≤ 1/6
104 --
105 -- Asymptotic: log x = o(x^ε) from isLittleO_log_rpow_atTop
106 -- -------
107 -- (A) p_n ∈ (0,1) eventually:
108 have hp_pos_ev : ∀ᶠ n : ℕ in Filter.atTop,
109 0 < 2 * Real.log n / (n : ℝ) ^ ε := by
110 rw [Filter.eventually_atTop]
111 -- log n > 0 for n ≥ 3, and n^ε > 0 for n ≥ 1
112 exact ⟨3, fun n hn => div_pos (by
113 apply mul_pos two_pos
114 apply Real.log_pos
115 exact_mod_cast show 1 < n by omega) (Real.rpow_pos_of_pos (by exact_mod_cast show 0 < n by omega) ε)⟩
116 have hp_lt1_ev : ∀ᶠ n : ℕ in Filter.atTop,
117 2 * Real.log (n : ℝ) / (n : ℝ) ^ ε < 1 := by
118 have h := (isLittleO_log_rpow_atTop hε_pos).tendsto_div_nhds_zero
119 have h2 : Filter.Tendsto (fun n : ℕ => 2 * Real.log (n : ℝ) / (n : ℝ) ^ ε)
120 Filter.atTop (nhds 0) := by
121 have := h.comp (tendsto_natCast_atTop_atTop (R := ℝ))
122 simp only [] at this
123 have hcov : Filter.Tendsto (fun n : ℕ => 2 * (Real.log (n : ℝ) / (n : ℝ) ^ ε))
124 Filter.atTop (nhds 0) := by
125 simpa [mul_comm] using this.const_mul 2
126 simpa [mul_div_assoc] using hcov
127 exact h2.eventually (gt_mem_nhds (by norm_num : (0 : ℝ) < 1))
128 -- (B) Chernoff error < 1/4 eventually: 2·exp(−n^{1−ε}·log n/6) < 1/4
129 have hchernoff_ev : ∀ᶠ n : ℕ in Filter.atTop,
130 2 * Real.exp (-(((n : ℝ) ^ (1 - ε) * Real.log (n : ℝ)) / 6)) < 1 / 4 := by
131 have h1e : 0 < 1 - ε := by linarith
132 have h_rpow : Filter.Tendsto (fun n : ℕ => (n : ℝ) ^ (1 - ε)) Filter.atTop Filter.atTop :=
133 (_root_.tendsto_rpow_atTop h1e).comp (tendsto_natCast_atTop_atTop (R := ℝ))
134 have h_logn_ev : ∀ᶠ n : ℕ in Filter.atTop, 1 ≤ Real.log (n : ℝ) :=
135 (Real.tendsto_log_atTop.comp (tendsto_natCast_atTop_atTop (R := ℝ))).eventually_ge_atTop 1
136 filter_upwards [h_rpow.eventually_ge_atTop (18 * Real.log 2 + 1), h_logn_ev]
137 with n h_large h_logn
138 have h_nn : (0 : ℝ) ≤ (n : ℝ) ^ (1 - ε) := Real.rpow_nonneg (Nat.cast_nonneg _) _
139 have h_log8 : Real.log 8 = 3 * Real.log 2 := by
140 rw [show (8 : ℝ) = 2 ^ (3 : ℕ) by norm_num, Real.log_pow]; push_cast; ring
141 have h_lb : Real.log 8 < (n : ℝ) ^ (1 - ε) * Real.log n / 6 := by
142 have h1 : (n : ℝ) ^ (1 - ε) ≤ (n : ℝ) ^ (1 - ε) * Real.log n :=
143 le_mul_of_one_le_right h_nn h_logn
144 linarith
145 calc 2 * Real.exp (-((n : ℝ) ^ (1 - ε) * Real.log n / 6))
146 < 2 * Real.exp (-Real.log 8) := by
147 apply mul_lt_mul_of_pos_left _ two_pos
148 exact Real.exp_lt_exp.mpr (by linarith)
149 _ = 1 / 4 := by
150 rw [Real.exp_neg, Real.exp_log (by norm_num : (0 : ℝ) < 8)]; norm_num
151 -- (C) Bad vertex probability p + 2·n^{-1/6} < 1/6 eventually
152 -- (Factor 2 accounts for the two-sided Chernoff bound applied per vertex)
153 have hbad_ev : ∀ᶠ n : ℕ in Filter.atTop,
154 2 * Real.log (n : ℝ) / (n : ℝ) ^ ε + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ)) < 1 / 6 := by
155 have h_log_zero : Filter.Tendsto (fun n : ℕ => 2 * Real.log (n : ℝ) / (n : ℝ) ^ ε)
156 Filter.atTop (nhds 0) := by
157 have h := (isLittleO_log_rpow_atTop hε_pos).tendsto_div_nhds_zero
158 have h2 := (h.comp (tendsto_natCast_atTop_atTop (R := ℝ))).const_mul 2
159 simp only [mul_zero] at h2; simpa [mul_div_assoc] using h2
160 have h_pow_zero : Filter.Tendsto (fun n : ℕ => 2 * (n : ℝ) ^ (-(1 / 6 : ℝ)))
161 Filter.atTop (nhds 0) := by
162 have := (tendsto_rpow_neg_atTop (by norm_num : (0 : ℝ) < 1 / 6)).comp
163 (tendsto_natCast_atTop_atTop (R := ℝ))
164 simpa using this.const_mul 2
165 have h_sum : Filter.Tendsto
166 (fun n : ℕ => 2 * Real.log (n : ℝ) / (n : ℝ) ^ ε + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ)))
167 Filter.atTop (nhds 0) := by simpa using h_log_zero.add h_pow_zero
168 filter_upwards [h_sum.eventually (Iio_mem_nhds (by norm_num : (0 : ℝ) < 1 / 6))]
169 with n hn; exact hn
170 -- (D) log n ≥ 1 eventually (needed to relate n^{1-ε} lower bound to n·p/2)
171 have h_logn_ev : ∀ᶠ n : ℕ in Filter.atTop, 1 ≤ Real.log (n : ℝ) :=
172 (Real.tendsto_log_atTop.comp (tendsto_natCast_atTop_atTop (R := ℝ))).eventually_ge_atTop 1
173 -- Extract concrete M
174 obtain ⟨M, hM⟩ := Filter.eventually_atTop.mp
175 (hp_pos_ev.and (hp_lt1_ev.and (hchernoff_ev.and (hbad_ev.and h_logn_ev))))
176 refine ⟨M, ?_⟩
177 -- ======================== MAIN ARGUMENT ========================
178 intro V inst_deq inst_fin G inst_adj hn hG_deg
179 -- Set up notation
180 set n := Fintype.card V with hn_def
181 -- Unpack threshold conditions for this n
182 obtain ⟨hp_pos, hp_lt1, hchernoff, hbad, h_logn⟩ := hM n hn
183 -- Lift p to NNReal
184 have hp_nn_pos : (0 : ℝ) ≤ 2 * Real.log n / (n : ℝ) ^ ε := hp_pos.le
185 let p_nnr : ℝ≥0 := ⟨2 * Real.log n / (n : ℝ) ^ ε, hp_nn_pos⟩
186 have hp_nnr : p_nnr ≤ 1 := by
187 have : (p_nnr : ℝ) ≤ 1 := hp_lt1.le
188 exact_mod_cast this
189 -- ======================== PROBABILITY SPACE ========================
190 -- Product Bernoulli(p) measure on V → Bool
191 let μ := Measure.pi (fun _ : V => (bernoulli p_nnr hp_nnr).toMeasure)
192 haveI : IsProbabilityMeasure μ := inferInstance
193 -- Indicator variables: X_v ω = 𝟙[ω v = true]
194 let X : V → (V → Bool) → ℝ := fun v ω => if ω v then 1 else 0
195 -- Properties of X needed for Chernoff:
196 have hX_meas : ∀ v : V, Measurable (X v) :=
197 fun v => measurable_of_countable (X v)
198 have hX_bern : ∀ v : V, ∀ᵐ ω ∂μ, X v ω = 0 ∨ X v ω = 1 :=
199 fun v => Filter.Eventually.of_forall (fun ω => by simp [X])
200 have hX_mean : ∀ v : V, ∫ ω, X v ω ∂μ = p_nnr.toReal :=
201 fun v => pi_bernoulli_indicator_mean hp_nnr v
202 have hX_indep : iIndepFun X μ := pi_bernoulli_iIndepFun hp_nnr
203 -- ======================== CHERNOFF BOUND FOR |A| ========================
204 -- Use Fintype.equivFin to reindex V as Fin n
205 let e : V ≃ Fin n := Fintype.equivFin V
206 -- Reindexed variables: Y_i ω = X_{e.symm i} ω
207 let Y : Fin n → (V → Bool) → ℝ := fun i => X (e.symm i)
208 have hY_meas : ∀ i : Fin n, Measurable (Y i) := fun i => hX_meas (e.symm i)
209 have hY_bern : ∀ i : Fin n, ∀ᵐ ω ∂μ, Y i ω = 0 ∨ Y i ω = 1 :=
210 fun i => hX_bern (e.symm i)
211 have hY_mean : ∀ i : Fin n, ∫ ω, Y i ω ∂μ = p_nnr.toReal := fun i => hX_mean (e.symm i)
212 have hY_indep : iIndepFun Y μ :=
213 hX_indep.precomp e.symm.injective
214 -- p_nnr.toReal ∈ [0,1]
215 have hp_icc : p_nnr.toReal ∈ Set.Icc (0 : ℝ) 1 :=
216 ⟨NNReal.coe_nonneg _, NNReal.coe_le_one.mpr hp_nnr⟩
217 -- Chernoff bound: δ = 1/2
218 have hδ : (1/2 : ℝ) ∈ Set.Ioo 0 1 := by norm_num
219 have h_chernoff_A :=
220 Catalog.Sparsity.ChernoffBound.chernoffBound hp_icc hY_meas hY_indep hY_bern hY_mean hδ
221 -- h_chernoff_A : μ.real {ω | 1/2 * (n * p) ≤ |∑_i Y i ω - n * p|} ≤ 2*exp(−(1/4*n*p/3))
222 -- Note: ∑_i Y_i ω = ∑_v X_v ω = |{v | ω v}|
223 -- Good event for |A|: |∑_i Y_i ω - n*p| < n*p/2, i.e., ∑_i Y_i ∈ [n*p/2, 3*n*p/2]
224 -- ======================== GOOD PAIR HAS POSITIVE MEASURE ========================
225 -- A good ω: A = {v | ω v}, B = {v | !ω v ∧ |N(v) ∩ A| ≥ log n}, with A and B in right range.
226 let good_event : Set (V → Bool) := {ω |
227 -- A is in the right size range
228 (n : ℝ) ^ (1 - ε) ≤ (Finset.univ.filter (fun v => ω v)).card ∧
229 ((Finset.univ.filter (fun v => ω v)).card : ℝ) ≤
230 3 * (n : ℝ) ^ (1 - ε) * Real.log n ∧
231 -- B (vertices not in A with enough neighbors in A) has size ≥ n/2
232 (n : ℝ) / 2 ≤ (Finset.univ.filter (fun v =>
233 !ω v ∧ Real.log n ≤
234 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card)).card}
235 -- The good event has positive measure (the hard probabilistic argument)
236 have h_good_pos : 0 < μ.real good_event := by
237 -- ∑_i Y_i ω = |(Finset.univ.filter (fun v => ω v))| as reals
238 have h_sum_card : ∀ ω : V → Bool,
239 (∑ i : Fin n, Y i ω : ℝ) =
240 (Finset.univ.filter (fun v : V => ω v)).card := fun ω => by
241 simp only [Y, X]
242 rw [show (∑ i : Fin n, if ω (e.symm i) = true then (1:ℝ) else 0) =
243 ∑ v : V, if ω v = true then (1:ℝ) else 0 from
244 Equiv.sum_comp e.symm (fun v => if ω v = true then (1:ℝ) else 0)]
245 simp
246 -- P(|∑_i Y_i - n*p| ≥ n*p/2) ≤ 2*exp(-n*p/12) < 1/4 (from h_chernoff_A + hchernoff)
247 -- n*p = 2 * n^{1-ε} * log n, n*p/12 = n^{1-ε} * log n / 6
248 -- h_chernoff_A gives: μ.real {ω | 1/2*(n*p) ≤ |∑_i Y_i ω - n*p|} ≤ 2*exp(-1/4*n*p/3)
249 -- and 1/4 * n*p / 3 = n*p/12 = n^{1-ε}*log n/6
250 -- Relate: {ω | good A size} ⊇ {ω | |∑_i Y_i ω - n*p| < n*p/2}
251 -- So P(bad A) ≤ P(|∑_i Y_i - n*p| ≥ n*p/2) ≤ 2*exp(-n*p/12) < 1/4
252 have h_bad_A : μ.real {ω | ¬(
253 (n : ℝ) ^ (1 - ε) ≤ (Finset.univ.filter (fun v => ω v)).card ∧
254 ((Finset.univ.filter (fun v => ω v)).card : ℝ) ≤
255 3 * (n : ℝ) ^ (1 - ε) * Real.log n)} < 1 / 4 := by
256 -- n > 0 (otherwise hp_pos : 0 < 0, contradiction)
257 have hn_pos : (0 : ℝ) < n := by
258 rcases Nat.eq_zero_or_pos n with h | h
259 · simp only [h, Nat.cast_zero, Real.log_zero, mul_zero, zero_div] at hp_pos
260 exact absurd hp_pos (lt_irrefl _)
261 · exact Nat.cast_pos.mpr h
262 have h_npe : 0 < (n : ℝ)^(1 - ε) := Real.rpow_pos_of_pos hn_pos _
263 -- n * p = 2 * n^{1-ε} * log n (since p = 2*log n / n^ε and n/n^ε = n^{1-ε})
264 have hn_p : (n : ℝ) * (p_nnr : ℝ) = 2 * (n : ℝ)^(1-ε) * Real.log n := by
265 show (n : ℝ) * (2 * Real.log n / (n : ℝ)^ε) = 2 * (n : ℝ)^(1-ε) * Real.log n
266 have hdiv : (n : ℝ) / (n : ℝ)^ε = (n : ℝ)^(1-ε) := by
267 rw [Real.rpow_sub hn_pos, Real.rpow_one]
268 rw [show (n : ℝ) * (2 * Real.log n / (n : ℝ)^ε) =
269 2 * ((n : ℝ) / (n : ℝ)^ε) * Real.log n from by ring, hdiv]
270 -- {bad_A} ⊆ {Chernoff set}: if |A| ∉ [n^{1-ε}, 3n^{1-ε}logn] then |∑Yi - np| ≥ np/2
271 have h_sub_A : {ω | ¬((n : ℝ)^(1-ε) ≤ ↑(Finset.univ.filter (fun v => ω v)).card ∧
272 ↑(Finset.univ.filter (fun v => ω v)).card ≤ 3*(n:ℝ)^(1-ε)*Real.log n)} ⊆
273 {ω | 1/2 * ((n:ℝ) * ↑p_nnr) ≤ |∑ i, Y i ω - (n:ℝ) * ↑p_nnr|} := by
274 intro ω hω
275 simp only [Set.mem_setOf_eq, not_and_or, not_le] at hω
276 rw [← h_sum_card ω] at hω
277 simp only [Set.mem_setOf_eq, hn_p]
278 rcases hω with hlo | hhi
279 · -- lower tail: ∑Yi < n^{1-ε} ≤ n^{1-ε}·logn = np/2
280 have h_lt : ∑ i, Y i ω < (n:ℝ)^(1-ε) * Real.log n :=
281 hlo.trans_le (le_mul_of_one_le_right h_npe.le h_logn)
282 rw [abs_of_nonpos (by
283 have := mul_nonneg h_npe.le (by linarith : (0:ℝ) ≤ Real.log n)
284 linarith)]
285 linarith
286 · -- upper tail: ∑Yi > 3n^{1-ε}·logn = np/2 + np
287 have h_prod : 0 < (n:ℝ)^(1-ε) * Real.log n := mul_pos h_npe (by linarith)
288 rw [abs_of_pos (by linarith)]
289 linarith
290 -- Chain: μ(bad_A) ≤ μ(Chernoff) ≤ 2·exp(−np/12) = 2·exp(−n^{1-ε}·logn/6) < 1/4
291 have h_exp_simp : (1/2:ℝ)^2 * ((n:ℝ) * ↑p_nnr) / 3 = (n:ℝ)^(1-ε) * Real.log n / 6 := by
292 rw [hn_p]; ring
293 calc μ.real {ω | ¬((n:ℝ)^(1-ε) ≤ ↑(Finset.univ.filter (fun v => ω v)).card ∧
294 ↑(Finset.univ.filter (fun v => ω v)).card ≤ 3*(n:ℝ)^(1-ε)*Real.log n)}
295 ≤ μ.real {ω | 1/2 * ((n:ℝ) * ↑p_nnr) ≤ |∑ i, Y i ω - (n:ℝ) * ↑p_nnr|} :=
296 measureReal_mono h_sub_A
297 _ ≤ 2 * Real.exp (-((1/2:ℝ)^2 * ((n:ℝ) * ↑p_nnr) / 3)) := h_chernoff_A
298 _ = 2 * Real.exp (-((n:ℝ)^(1-ε) * Real.log n / 6)) := by
299 rw [show (1/2:ℝ)^2 * ((n:ℝ) * ↑p_nnr) / 3 = (n:ℝ)^(1-ε) * Real.log n / 6 from
300 h_exp_simp]
301 _ < 1/4 := hchernoff
302 -- P(|B| < n/2) < 1/3 (Markov on |V\B| with E[|V\B|] ≤ n*(p + 2*n^{-1/6}) and hbad)
303 have h_bad_B : μ.real {ω | ¬ ((n : ℝ) / 2 ≤
304 (Finset.univ.filter (fun v =>
305 !ω v ∧ Real.log n ≤
306 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card)).card)} < 1 / 3 := by
307 -- n > 0 (from hp_pos)
308 have hn_pos : (0 : ℝ) < n := by
309 rcases Nat.eq_zero_or_pos n with h | h
310 · simp only [h, Nat.cast_zero, Real.log_zero, mul_zero, zero_div] at hp_pos
311 exact absurd hp_pos (lt_irrefl _)
312 · exact Nat.cast_pos.mpr h
313 have h_npe : 0 < (n : ℝ) ^ ε := Real.rpow_pos_of_pos hn_pos _
314 have h_npi : 0 < (n : ℝ) ^ (-(1 / 6 : ℝ)) := Real.rpow_pos_of_pos hn_pos _
315 -- deg(v) * p ≥ 2 * log n for each v (from hG_deg and p = 2*log n/n^ε)
316 have h_dp_lower : ∀ v : V, 2 * Real.log n ≤ (G.degree v : ℝ) * (p_nnr : ℝ) := fun v => by
317 have hdeg := hG_deg v
318 calc 2 * Real.log n
319 = (n : ℝ) ^ ε * (p_nnr : ℝ) := by
320 show 2 * Real.log n = (n : ℝ) ^ ε * (2 * Real.log n / (n : ℝ) ^ ε)
321 field_simp
322 _ ≤ (G.degree v : ℝ) * (p_nnr : ℝ) :=
323 mul_le_mul_of_nonneg_right hdeg hp_pos.le
324 -- Per-vertex Chernoff: P(|N(v) ∩ A| < log n) ≤ 2 * n^{-1/6}
325 have h_chernoff_vtx : ∀ v : V,
326 μ.real {ω | (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card <
327 Real.log n} ≤ 2 * (n : ℝ) ^ (-(1 / 6 : ℝ)) := fun v => by
328 -- Sum identity: ∑_j X(nbr_j(v)) ω = |N(v) ∩ A(ω)|
329 have h_sum_v : ∀ ω : V → Bool,
330 (∑ j : Fin (G.degree v),
331 X ((Finset.equivFin (G.neighborFinset v)).symm j).val ω : ℝ) =
332 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card := fun ω => by
333 simp only [X]
334 rw [show G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u) =
335 (G.neighborFinset v).filter (fun u => ω u) by ext; simp]
336 rw [show (((G.neighborFinset v).filter (fun u => ω u)).card : ℝ) =
337 ∑ u ∈ G.neighborFinset v, if ω u then (1 : ℝ) else 0 by
338 push_cast [Finset.card_filter]
339 apply Finset.sum_congr rfl; intro x _; simp]
340 rw [← Finset.sum_coe_sort (G.neighborFinset v)]
341 apply Fintype.sum_equiv (Finset.equivFin (G.neighborFinset v)).symm
342 intro j; simp
343 -- Independence of neighbor indicators via precomp
344 have hg_inj : Function.Injective
345 (fun j : Fin (G.degree v) =>
346 ((Finset.equivFin (G.neighborFinset v)).symm j).val) := fun a b hab => by
347 have h1 := Subtype.val_injective hab
348 exact (Finset.equivFin (G.neighborFinset v)).symm.injective h1
349 -- Apply Chernoff with δ = 1/2
350 have h_chernoff_Z :=
351 Catalog.Sparsity.ChernoffBound.chernoffBound hp_icc
352 (fun j => hX_meas ((Finset.equivFin (G.neighborFinset v)).symm j).val)
353 (hX_indep.precomp hg_inj)
354 (fun j => hX_bern ((Finset.equivFin (G.neighborFinset v)).symm j).val)
355 (fun j => hX_mean ((Finset.equivFin (G.neighborFinset v)).symm j).val)
356 hδ
357 -- Subset: {|N(v)∩A| < log n} ⊆ {Chernoff condition}
358 have h_dp := h_dp_lower v
359 have h_sub_v : {ω | (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card <
360 Real.log n} ⊆
361 {ω | 1 / 2 * ((G.degree v : ℝ) * ↑p_nnr) ≤
362 |∑ j : Fin (G.degree v),
363 X ((Finset.equivFin (G.neighborFinset v)).symm j).val ω -
364 (G.degree v : ℝ) * ↑p_nnr|} := fun ω hω => by
365 simp only [Set.mem_setOf_eq] at hω ⊢
366 rw [h_sum_v]
367 have h_neg : ((G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card : ℝ) -
368 (G.degree v : ℝ) * ↑p_nnr < 0 := by linarith
369 rw [abs_of_nonpos (le_of_lt h_neg)]
370 linarith
371 -- Bound: 2*exp(−deg*p/12) ≤ 2*n^{−1/6} (since deg*p ≥ 2*log n)
372 have h_exp_bound : 2 * Real.exp (-((1 / 2 : ℝ) ^ 2 * ((G.degree v : ℝ) * ↑p_nnr) / 3)) ≤
373 2 * (n : ℝ) ^ (-(1 / 6 : ℝ)) := by
374 apply mul_le_mul_of_nonneg_left _ (by norm_num)
375 have h1 : (n : ℝ) ^ (-(1 / 6 : ℝ)) = Real.exp (-(Real.log n / 6)) := by
376 rw [Real.rpow_neg (le_of_lt hn_pos), Real.rpow_def_of_pos hn_pos, ← Real.exp_neg]
377 congr 1; ring
378 rw [h1]
379 apply Real.exp_le_exp_of_le
380 linarith
381 calc μ.real {ω | (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card <
382 Real.log n}
383 ≤ μ.real {ω | 1 / 2 * ((G.degree v : ℝ) * ↑p_nnr) ≤
384 |∑ j : Fin (G.degree v),
385 X ((Finset.equivFin (G.neighborFinset v)).symm j).val ω -
386 (G.degree v : ℝ) * ↑p_nnr|} := measureReal_mono h_sub_v
387 _ ≤ 2 * Real.exp (-((1 / 2 : ℝ) ^ 2 * ((G.degree v : ℝ) * ↑p_nnr) / 3)) :=
388 h_chernoff_Z
389 _ ≤ 2 * (n : ℝ) ^ (-(1 / 6 : ℝ)) := h_exp_bound
390 -- P(v ∉ B) ≤ p + 2*n^{-1/6} via union bound
391 have h_bad_v : ∀ v : V,
392 μ.real {ω | ¬(!ω v ∧ Real.log n ≤
393 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card)} ≤
394 (p_nnr : ℝ) + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ)) := fun v => by
395 -- {v ∉ B} ⊆ {ω v = true} ∪ {|N(v)∩A| < log n}
396 have h_sub : {ω | ¬(!ω v ∧ Real.log n ≤
397 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card)} ⊆
398 {ω : V → Bool | ω v = true} ∪
399 {ω | (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card <
400 Real.log n} := fun ω hω => by
401 simp only [Set.mem_setOf_eq, not_and_or, Bool.not_eq_true, not_le,
402 Set.mem_union] at *
403 rcases hω with h | h
404 · left; cases hv : ω v
405 · simp [hv] at h
406 · rfl
407 · right; exact h
408 -- P(ω v = true) = p
409 have h_p_v : μ.real {ω : V → Bool | ω v = true} = (p_nnr : ℝ) := by
410 rw [← hX_mean v, ← integral_indicator_one MeasurableSet.of_discrete]
411 congr 1; ext ω; simp [X, Set.indicator]
412 linarith [(measureReal_mono h_sub (measure_ne_top μ _)).trans (measureReal_union_le _ _),
413 h_chernoff_vtx v, h_p_v.symm.le]
414 -- Markov on f = |V\B| (count of bad vertices)
415 let notB_pred : V → (V → Bool) → Prop := fun v ω =>
416 ¬(!ω v ∧ Real.log n ≤
417 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card)
418 let f : (V → Bool) → ℝ :=
419 fun ω => (Finset.univ.filter (fun v => notB_pred v ω)).card
420 -- {bad_B} ⊆ {f ≥ n/2}
421 have h_sub_f : {ω | ¬ ((n : ℝ) / 2 ≤
422 (Finset.univ.filter (fun v =>
423 !ω v ∧ Real.log n ≤
424 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card)).card)} ⊆
425 {ω | (n : ℝ) / 2 ≤ f ω} := fun ω hω => by
426 simp only [Set.mem_setOf_eq, f, notB_pred] at *
427 have h_sum : ((Finset.univ.filter (fun v => !ω v ∧ Real.log n ≤
428 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card)).card : ℝ) +
429 ((Finset.univ.filter (fun v => ¬(!ω v ∧ Real.log n ≤
430 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card))).card : ℝ) =
431 n := by
432 have key := @Finset.card_filter_add_card_filter_not V Finset.univ
433 (fun v => !ω v ∧ Real.log n ≤
434 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card) _ _
435 rw [Finset.card_univ] at key
436 exact_mod_cast key.trans hn_def.symm
437 linarith
438 -- Markov inequality
439 have hf_nonneg : 0 ≤ᵐ[μ] f :=
440 Filter.Eventually.of_forall (fun ω => by positivity)
441 have h_markov :=
442 mul_meas_ge_le_integral_of_nonneg hf_nonneg Integrable.of_finite ((n : ℝ) / 2)
443 -- ∫ f ∂μ = ∑_v P(v ∉ B)
444 have h_int : ∫ ω, f ω ∂μ = ∑ v : V, μ.real {ω | notB_pred v ω} := by
445 conv_lhs =>
446 arg 2; ext ω
447 rw [show (f ω : ℝ) = ∑ v : V,
448 ({ω | notB_pred v ω} : Set _).indicator (fun _ => (1 : ℝ)) ω from by
449 simp [f, notB_pred, Set.indicator]]
450 rw [integral_finset_sum Finset.univ (fun v _ => Integrable.of_finite)]
451 congr 1; ext v
452 exact MeasureTheory.integral_indicator_one MeasurableSet.of_discrete
453 -- ∫ f ∂μ ≤ n * (p + 2*n^{-1/6})
454 have h_int_bound : ∫ ω, f ω ∂μ ≤ n * ((p_nnr : ℝ) + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ))) := by
455 rw [h_int]
456 calc ∑ v : V, μ.real {ω | notB_pred v ω}
457 ≤ ∑ v : V, ((p_nnr : ℝ) + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ))) :=
458 Finset.sum_le_sum (fun v _ => h_bad_v v)
459 _ = n * ((p_nnr : ℝ) + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ))) := by
460 simp [Finset.sum_const, Finset.card_univ, hn_def]; ring
461 -- Chain: P(bad_B) ≤ P(f ≥ n/2) ≤ E[f]/(n/2) ≤ 2*(p+2*n^{-1/6}) < 1/3
462 have hn_half : 0 < (n : ℝ) / 2 := by linarith
463 have h_Pf : μ.real {ω | (n : ℝ) / 2 ≤ f ω} ≤
464 2 * ((p_nnr : ℝ) + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ))) := by
465 have h_final : (n : ℝ) / 2 * μ.real {ω | (n : ℝ) / 2 ≤ f ω} ≤
466 n * ((p_nnr : ℝ) + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ))) :=
467 h_markov.trans h_int_bound
468 rw [show (n : ℝ) * ((p_nnr : ℝ) + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ))) =
469 (n : ℝ) / 2 * (2 * ((p_nnr : ℝ) + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ)))) from by ring]
470 at h_final
471 exact le_of_mul_le_mul_left h_final hn_half
472 have h_p_val : (p_nnr : ℝ) = 2 * Real.log n / (n : ℝ) ^ ε := rfl
473 have h_bound : 2 * ((p_nnr : ℝ) + 2 * (n : ℝ) ^ (-(1 / 6 : ℝ))) < 1 / 3 := by
474 linarith
475 linarith [measureReal_mono h_sub_f (measure_ne_top μ _)]
476 -- Combine: P(good_event^c) ≤ P(bad_A) + P(bad_B) < 1/4 + 1/3 = 7/12 < 1
477 -- So P(good_event) ≥ 5/12 > 0
478 have h_bad_total : μ.real good_eventᶜ < 1 := by
479 have h_sub : good_eventᶜ ⊆
480 {ω | ¬((n : ℝ) ^ (1 - ε) ≤ (Finset.univ.filter (fun v => ω v)).card ∧
481 (Finset.univ.filter (fun v => ω v)).card ≤
482 3 * (n : ℝ) ^ (1 - ε) * Real.log n)} ∪
483 {ω | ¬((n : ℝ) / 2 ≤ (Finset.univ.filter (fun v =>
484 !ω v ∧ Real.log n ≤
485 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card)).card)} := by
486 intro ω hω
487 simp only [good_event, Set.mem_compl_iff, Set.mem_setOf_eq, not_and] at hω
488 simp only [Set.mem_union, Set.mem_setOf_eq]
489 by_cases hA : (n : ℝ) ^ (1 - ε) ≤ (Finset.univ.filter (fun v => ω v)).card ∧
490 ((Finset.univ.filter (fun v => ω v)).card : ℝ) ≤ 3 * (n : ℝ) ^ (1 - ε) * Real.log n
491 · exact Or.inr (hω hA.1 hA.2)
492 · exact Or.inl hA
493 have h_union : μ.real (good_eventᶜ) ≤
494 μ.real {ω | ¬((n : ℝ) ^ (1 - ε) ≤ (Finset.univ.filter (fun v => ω v)).card ∧
495 ((Finset.univ.filter (fun v => ω v)).card : ℝ) ≤
496 3 * (n : ℝ) ^ (1 - ε) * Real.log n)} +
497 μ.real {ω | ¬((n : ℝ) / 2 ≤ (Finset.univ.filter (fun v =>
498 !ω v ∧ Real.log n ≤
499 (G.neighborFinset v ∩ Finset.univ.filter (fun u => ω u)).card)).card)} :=
500 (measureReal_mono h_sub).trans (measureReal_union_le _ _)
501 linarith
502 have h_meas : MeasurableSet good_event := MeasurableSet.of_discrete
503 rw [probReal_compl_eq_one_sub h_meas] at h_bad_total
504 linarith
505 -- ======================== EXTRACT WITNESS ========================
506 obtain ⟨ω, hω⟩ := nonempty_of_measureReal_ne_zero (ne_of_gt h_good_pos)
507 obtain ⟨hA_lo, hA_hi, hB_lo⟩ := hω
508 -- Define A = sampled vertices, B = non-sampled vertices with enough sampled neighbors
509 let A : Finset V := Finset.univ.filter (fun v => ω v)
510 let B : Finset V := Finset.univ.filter
511 (fun v => !ω v ∧ Real.log n ≤ (G.neighborFinset v ∩ A).card)
512 refine ⟨A, B, ?_, ?_, ?_, ?_, ?_⟩
513 · -- Disjoint A B: A ⊆ {ω v = true}, B ⊆ {ω v = false}
514 simp only [A, B, Finset.disjoint_filter]
515 intro v _ hv_A hv_B
516 simp [hv_A] at hv_B
517 · -- |A| ≥ n^{1-ε}
518 exact_mod_cast hA_lo
519 · -- |A| ≤ 3 n^{1-ε} log n
520 exact_mod_cast hA_hi
521 · -- |B| ≥ n/2
522 exact_mod_cast hB_lo
523 · -- Every b ∈ B has ≥ log n neighbors in A (by definition of B)
524 intro b hb
525 exact_mod_cast ((Finset.mem_filter.mp hb).2).2
526
527/-- **Auxiliary (minor model from assignment)**: Given an edge set `E` on `A` and an
528assignment `f` from the processed subset `B'` of `B` to `A` — with each `b` adjacent to
529`f b` in `G` — and a witness for every edge in `E` (some processed `b` whose assignment is
530one endpoint and is adjacent to the other), this constructs a depth-1 `ShallowMinorModel`
531of `fromEdgeSet E` in `G`.
532
533Branch set of `a ∈ A`: `{a.val} ∪ {b.val | b ∈ B', f b = a}`.
534Depth 1: each `b` is adjacent to its assigned vertex `f b = a` in `G`. -/
535private noncomputable def minorModelFromAssignment
536 {V : Type} [DecidableEq V] [Fintype V]
537 (G : SimpleGraph V) [DecidableRel G.Adj]
538 (A B' : Finset V) (hAB' : Disjoint A B')
539 (E : Finset (Sym2 {a : V // a ∈ A}))
540 (f : {b : V // b ∈ B'} → {a : V // a ∈ A})
541 (hf_adj : ∀ b : {b : V // b ∈ B'}, G.Adj (f b).val b.val)
542 (hE_witness : ∀ (a a' : {a : V // a ∈ A}),
543 (SimpleGraph.fromEdgeSet (↑E : Set (Sym2 {a : V // a ∈ A}))).Adj a a' →
544 ∃ b : {b : V // b ∈ B'},
545 (f b = a ∧ G.Adj b.val a'.val) ∨ (f b = a' ∧ G.Adj b.val a.val)) :
546 ShallowMinorModel
547 (SimpleGraph.fromEdgeSet (↑E : Set (Sym2 {a : V // a ∈ A}))) G 1 where
548 branchSet a := {v : V | v = a.val ∨ ∃ b : {b : V // b ∈ B'}, f b = a ∧ v = b.val}
549 center a := a.val
550 center_mem a := Set.mem_setOf.mpr (Or.inl rfl)
551 branchDisjoint := by
552 intro a₁ a₂ ha
553 apply Set.disjoint_left.mpr
554 intro v hv₁ hv₂
555 simp only [Set.mem_setOf_eq] at hv₁ hv₂
556 have hd := Finset.disjoint_left.mp hAB'
557 rcases hv₁ with rfl | ⟨b, hfb, rfl⟩ <;> rcases hv₂ with h | ⟨b', hfb', h'⟩
558 · exact ha (Subtype.ext h)
559 · exact hd a₁.property (h' ▸ b'.property)
560 · exact hd a₂.property (by rw [← h]; exact b.property)
561 · have hbb' : b = b' := Subtype.ext h'
562 have hfb_eq : f b = a₂ := by rw [hbb']; exact hfb'
563 exact ha (hfb.symm.trans hfb_eq)
564 branchRadius := by
565 intro a v hv
566 simp only [Set.mem_setOf_eq] at hv
567 rcases hv with rfl | ⟨b, hfb, rfl⟩
568 · exact ⟨SimpleGraph.Walk.nil, SimpleGraph.Walk.IsPath.nil, by simp,
569 fun w hw => by
570 simp only [SimpleGraph.Walk.support_nil, List.mem_singleton] at hw
571 exact hw ▸ Set.mem_setOf.mpr (Or.inl rfl)⟩
572 · have hadj : G.Adj a.val b.val := hfb ▸ hf_adj b
573 refine ⟨hadj.toWalk, SimpleGraph.Walk.IsPath.of_adj hadj,
574 by simp [SimpleGraph.Adj.toWalk, SimpleGraph.Walk.length_cons],
575 fun w hw => ?_⟩
576 simp only [SimpleGraph.Adj.toWalk, SimpleGraph.Walk.support_cons,
577 SimpleGraph.Walk.support_nil, List.mem_cons,
578 List.mem_nil_iff, or_false] at hw
579 rcases hw with rfl | rfl
580 · exact Set.mem_setOf.mpr (Or.inl rfl)
581 · exact Set.mem_setOf.mpr (Or.inr ⟨b, hfb, rfl⟩)
582 branchEdge := by
583 intro a₁ a₂ hadj
584 obtain ⟨b, hb | hb⟩ := hE_witness a₁ a₂ hadj
585 · exact ⟨b.val, Set.mem_setOf.mpr (Or.inr ⟨b, hb.1, rfl⟩),
586 a₂.val, Set.mem_setOf.mpr (Or.inl rfl), hb.2⟩
587 · exact ⟨a₁.val, Set.mem_setOf.mpr (Or.inl rfl),
588 b.val, Set.mem_setOf.mpr (Or.inr ⟨b, hb.1, rfl⟩), hb.2.symm⟩
589
590/-- Given a depth-1 minor model, a clique `S` in the source graph, and a vertex `b₀`
591adjacent in `G` to the center of every element of `S` and not in any branch set,
592we get `K_{|S|+1} ≼₁ G`. -/
593private noncomputable def clique_extension_minor
594 {V W : Type} [DecidableEq V] [DecidableEq W]
595 {H : SimpleGraph W} {G : SimpleGraph V}
596 (M : ShallowMinorModel H G 1)
597 (S : Finset W)
598 (hS_clique : ∀ a₁ ∈ S, ∀ a₂ ∈ S, a₁ ≠ a₂ → H.Adj a₁ a₂)
599 (b₀ : V)
600 (hb₀_adj : ∀ a ∈ S, G.Adj b₀ (M.center a))
601 (hb₀_not_branch : ∀ w : W, b₀ ∉ M.branchSet w) :
602 ShallowMinorModel (SimpleGraph.completeGraph (Fin (S.card + 1))) G 1 :=
603 let φ := S.equivFin
604 let toW : Fin S.card → W := fun i => (φ.symm i).val
605 have htoW_inj : Function.Injective toW := fun i j h =>
606 φ.symm.injective (Subtype.val_injective h)
607 have htoW_mem : ∀ i, toW i ∈ S := fun i => (φ.symm i).property
608 { branchSet := fun i =>
609 if h : (i : ℕ) < S.card then M.branchSet (toW ⟨i, h⟩) else {b₀}
610 center := fun i =>
611 if h : (i : ℕ) < S.card then M.center (toW ⟨i, h⟩) else b₀
612 center_mem := by
613 intro i; split
614 · exact M.center_mem _
615 · exact rfl
616 branchDisjoint := by
617 intro i j hij
618 by_cases hi : (i : ℕ) < S.card <;> by_cases hj : (j : ℕ) < S.card
619 · rw [dif_pos hi, dif_pos hj]
620 exact M.branchDisjoint _ _ (fun heq => hij (Fin.ext (by
621 exact_mod_cast congrArg Fin.val (htoW_inj heq))))
622 · rw [dif_pos hi, dif_neg hj]
623 exact Set.disjoint_singleton_right.mpr (hb₀_not_branch _)
624 · rw [dif_neg hi, dif_pos hj]
625 exact Set.disjoint_singleton_left.mpr (hb₀_not_branch _)
626 · exact absurd (Fin.ext (by omega)) hij
627 branchRadius := by
628 intro i x hx
629 by_cases h : (i : ℕ) < S.card
630 · rw [dif_pos h] at hx; rw [dif_pos h]; rw [dif_pos h]
631 exact M.branchRadius _ x hx
632 · rw [dif_neg h] at hx; rw [dif_neg h]; rw [dif_neg h]
633 rw [Set.mem_singleton_iff.mp hx]
634 exact ⟨SimpleGraph.Walk.nil, SimpleGraph.Walk.IsPath.nil, by norm_num,
635 fun w hw => by
636 simp only [SimpleGraph.Walk.support_nil, List.mem_singleton] at hw
637 exact hw⟩
638 branchEdge := by
639 intro i j hij
640 simp only [SimpleGraph.top_adj] at hij
641 by_cases hi : (i : ℕ) < S.card <;> by_cases hj : (j : ℕ) < S.card
642 · rw [dif_pos hi, dif_pos hj]
643 exact M.branchEdge _ _ (hS_clique _ (htoW_mem _) _ (htoW_mem _)
644 (fun heq => hij (Fin.ext (by exact_mod_cast congrArg Fin.val (htoW_inj heq)))))
645 · rw [dif_pos hi, dif_neg hj]
646 exact ⟨M.center _, M.center_mem _, b₀, rfl, (hb₀_adj _ (htoW_mem _)).symm⟩
647 · rw [dif_neg hi, dif_pos hj]
648 exact ⟨b₀, rfl, M.center _, M.center_mem _, hb₀_adj _ (htoW_mem _)⟩
649 · exact absurd (Fin.ext (by omega)) hij }
650
651/-- **Step 2 (greedy edges or clique)**: Core induction — either find `K_{t+1} ≼₁ G`
652for `t ≥ log n`, or find an edge set `E` with `|B| ≤ |E|`, an assignment `f : B → A`
653with `G.Adj (f b) b`, and witnesses for the minor-model construction. -/
654private lemma greedy_edges_or_clique
655 {V : Type} [DecidableEq V] [Fintype V]
656 (G : SimpleGraph V) [DecidableRel G.Adj]
657 (A B : Finset V) (hAB : Disjoint A B)
658 (hB_nbrs : ∀ b ∈ B, log ↑(Fintype.card V) ≤ ↑(G.neighborFinset b ∩ A).card) :
659 (∃ t : ℕ, log ↑(Fintype.card V) ≤ ↑t ∧
660 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) G 1) ∨
661 (∃ (E : Finset (Sym2 {a : V // a ∈ A}))
662 (f : {b : V // b ∈ B} → {a : V // a ∈ A}),
663 B.card ≤ E.card ∧
664 (∀ e ∈ E, ¬e.IsDiag) ∧
665 (∀ b : {b : V // b ∈ B}, G.Adj (f b).val b.val) ∧
666 ∀ (a a' : {a : V // a ∈ A}),
667 (SimpleGraph.fromEdgeSet (↑E : Set (Sym2 {a : V // a ∈ A}))).Adj a a' →
668 ∃ b : {b : V // b ∈ B},
669 (f b = a ∧ G.Adj b.val a'.val) ∨ (f b = a' ∧ G.Adj b.val a.val)) := by
670 classical
671 refine Finset.induction_on B ?_ ?_ hAB hB_nbrs
672 · intro hAB_empty hB_empty
673 refine Or.inr ?_
674 refine ⟨∅, (fun b => nomatch b.property), ?_⟩
675 simp
676 · intro b₀ B₀ hb₀ ih hAB_ins hB_ins
677 have hAB₀ : Disjoint A B₀ := by
678 rw [Finset.disjoint_left] at hAB_ins ⊢
679 intro a haA haB₀
680 exact hAB_ins haA (Finset.mem_insert_of_mem haB₀)
681 have hB₀_nbrs : ∀ b ∈ B₀, log ↑(Fintype.card V) ≤ ↑(G.neighborFinset b ∩ A).card := by
682 intro b hb
683 exact hB_ins b (Finset.mem_insert_of_mem hb)
684 rcases ih hAB₀ hB₀_nbrs with
685 hclique | ⟨E₀, f₀, hcard₀, hnd₀, hf₀_adj, hwitness₀⟩
686 · exact Or.inl hclique
687 · let S : Finset {a : V // a ∈ A} :=
688 (G.neighborFinset b₀ ∩ A).subtype (fun a => a ∈ A)
689 have hS_ge : log ↑(Fintype.card V) ≤ ↑S.card := by
690 have hS_card : S.card = (G.neighborFinset b₀ ∩ A).card := by
691 unfold S
692 rw [Finset.card_subtype]
693 apply congrArg Finset.card
694 ext a
695 simp [Finset.mem_inter]
696 rw [hS_card]
697 exact hB_ins b₀ (Finset.mem_insert_self b₀ B₀)
698 by_cases hnew :
699 ∃ a₁ ∈ S, ∃ a₂ ∈ S, a₁ ≠ a₂ ∧ s(a₁, a₂) ∉ E₀
700 · rcases hnew with ⟨a₁, ha₁S, a₂, ha₂S, ha12, hnotE₀⟩
701 let E : Finset (Sym2 {a : V // a ∈ A}) := insert (s(a₁, a₂)) E₀
702 let f : {b : V // b ∈ insert b₀ B₀} → {a : V // a ∈ A} := fun b =>
703 if h : b.val = b₀ then a₁ else f₀ ⟨b.val, (Finset.mem_insert.mp b.property).resolve_left h⟩
704 refine Or.inr ⟨E, f, ?_, ?_, ?_, ?_⟩
705 · calc
706 (insert b₀ B₀).card = B₀.card + 1 := by simp [hb₀]
707 _ ≤ E₀.card + 1 := Nat.succ_le_succ hcard₀
708 _ = E.card := by simp [E, hnotE₀]
709 · intro e he
710 rcases Finset.mem_insert.mp he with rfl | he₀
711 · simpa [Sym2.mk_isDiag_iff] using ha12
712 · exact hnd₀ e he₀
713 · intro b
714 by_cases hb : b.val = b₀
715 · rw [show f b = a₁ by simp [f, hb]]
716 have ha₁_mem : a₁.val ∈ G.neighborFinset b₀ ∩ A := by
717 simpa [S] using ha₁S
718 simpa [hb] using ((G.mem_neighborFinset b₀ a₁.val).mp (Finset.mem_inter.mp ha₁_mem).1).symm
719 · rw [show f b = f₀ ⟨b.val, (Finset.mem_insert.mp b.property).resolve_left hb⟩ by
720 simp [f, hb]]
721 exact hf₀_adj ⟨b.val, (Finset.mem_insert.mp b.property).resolve_left hb⟩
722 · intro a a' hadj
723 rw [SimpleGraph.fromEdgeSet_adj] at hadj
724 rcases Finset.mem_insert.mp hadj.1 with hE | hE
725 · have hs : s(a, a') = s(a₁, a₂) := hE
726 let b : {b : V // b ∈ insert b₀ B₀} := ⟨b₀, Finset.mem_insert_self b₀ B₀⟩
727 have ha₁_mem : a₁.val ∈ G.neighborFinset b₀ ∩ A := by
728 simpa [S] using ha₁S
729 have ha₂_mem : a₂.val ∈ G.neighborFinset b₀ ∩ A := by
730 simpa [S] using ha₂S
731 have ha₁_adj : G.Adj b₀ a₁.val :=
732 (G.mem_neighborFinset b₀ a₁.val).mp (Finset.mem_inter.mp ha₁_mem).1
733 have ha₂_adj : G.Adj b₀ a₂.val :=
734 (G.mem_neighborFinset b₀ a₂.val).mp (Finset.mem_inter.mp ha₂_mem).1
735 rcases Sym2.eq_iff.mp hs with h | h
736 · refine ⟨b, Or.inl ?_⟩
737 rcases h with ⟨rfl, rfl⟩
738 exact ⟨by simp [b, f], ha₂_adj⟩
739 · refine ⟨b, Or.inr ?_⟩
740 rcases h with ⟨rfl, rfl⟩
741 exact ⟨by simp [b, f], ha₂_adj⟩
742 · obtain ⟨b, hb | hb⟩ := hwitness₀ a a' ((SimpleGraph.fromEdgeSet_adj _).2 ⟨hE, hadj.2⟩)
743 · refine ⟨⟨b.val, Finset.mem_insert_of_mem b.property⟩, Or.inl ?_⟩
744 refine ⟨?_, hb.2⟩
745 have hbne : b.val ≠ b₀ := by
746 intro hEq
747 exact hb₀ (hEq ▸ b.property)
748 simp [f, hbne, hb.1]
749 · refine ⟨⟨b.val, Finset.mem_insert_of_mem b.property⟩, Or.inr ?_⟩
750 refine ⟨?_, hb.2⟩
751 have hbne : b.val ≠ b₀ := by
752 intro hEq
753 exact hb₀ (hEq ▸ b.property)
754 simp [f, hbne, hb.1]
755 · have hall :
756 ∀ a₁ ∈ S, ∀ a₂ ∈ S, a₁ ≠ a₂ → s(a₁, a₂) ∈ E₀ := by
757 intro a₁ ha₁S a₂ ha₂S ha12
758 by_contra hnotmem
759 exact hnew ⟨a₁, ha₁S, a₂, ha₂S, ha12, hnotmem⟩
760 let M₀ := minorModelFromAssignment G A B₀ hAB₀ E₀ f₀ hf₀_adj hwitness₀
761 have hS_clique :
762 ∀ a₁ ∈ S, ∀ a₂ ∈ S, a₁ ≠ a₂ →
763 (SimpleGraph.fromEdgeSet (↑E₀ : Set (Sym2 {a : V // a ∈ A}))).Adj a₁ a₂ := by
764 intro a₁ ha₁S a₂ ha₂S ha12
765 rw [SimpleGraph.fromEdgeSet_adj]
766 exact ⟨hall a₁ ha₁S a₂ ha₂S ha12, ha12⟩
767 have hb₀_adj :
768 ∀ a ∈ S, G.Adj b₀ (M₀.center a) := by
769 intro a haS
770 change G.Adj b₀ a.val
771 have ha_mem : a.val ∈ G.neighborFinset b₀ ∩ A := by
772 simpa [S] using haS
773 exact (G.mem_neighborFinset b₀ a.val).mp (Finset.mem_inter.mp ha_mem).1
774 have hb₀_not_branch :
775 ∀ w : {a : V // a ∈ A}, b₀ ∉ M₀.branchSet w := by
776 intro w
777 change b₀ ∉ {v : V | v = w.val ∨ ∃ b : {b : V // b ∈ B₀}, f₀ b = w ∧ v = b.val}
778 intro hb
779 rcases hb with hEq | ⟨b, -, hbval⟩
780 · rw [Finset.disjoint_left] at hAB_ins
781 exact (hAB_ins w.property) (hEq ▸ Finset.mem_insert_self b₀ B₀)
782 · exact hb₀ (hbval ▸ b.property)
783 exact Or.inl ⟨S.card, hS_ge, ⟨clique_extension_minor M₀ S hS_clique b₀ hb₀_adj hb₀_not_branch⟩⟩
784
785/-- **Step 2 (greedy construction)**: Given a "good pair" (A, B) in G, the greedy
786process either finds a clique minor K_{t+1} for t ≥ log n, or builds a depth-1
787minor G' on vertex set {a : V // a ∈ A} with ≥ |B| edges.
788
789Uses `greedy_edges_or_clique` for the inductive construction and
790`minorModelFromAssignment` to build the minor model from the assignment. -/
791private lemma greedy_densify
792 {V : Type} [DecidableEq V] [Fintype V]
793 (G : SimpleGraph V) [DecidableRel G.Adj]
794 (A B : Finset V) (hAB : Disjoint A B)
795 (hB_nbrs : ∀ b ∈ B, log ↑(Fintype.card V) ≤ ↑(G.neighborFinset b ∩ A).card) :
796 (∃ t : ℕ, log ↑(Fintype.card V) ≤ ↑t ∧
797 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) G 1) ∨
798 (∃ (G' : SimpleGraph {a : V // a ∈ A}) (_ : DecidableRel G'.Adj),
799 IsShallowMinor G' G 1 ∧
800 (↑B.card : ℝ) ≤ ↑G'.edgeFinset.card) := by
801 rcases greedy_edges_or_clique G A B hAB hB_nbrs with
802 clique | ⟨E, f, hcard, hnd, hf_adj, hwitness⟩
803 · exact Or.inl clique
804 · right
805 letI : DecidableRel (SimpleGraph.fromEdgeSet (↑E : Set (Sym2 {a : V // a ∈ A})) :
806 SimpleGraph {a : V // a ∈ A}).Adj :=
807 fun a a' => by rw [SimpleGraph.fromEdgeSet_adj]; exact inferInstance
808 refine ⟨SimpleGraph.fromEdgeSet (↑E : Set _), ‹_›,
809 ⟨minorModelFromAssignment G A B hAB E f hf_adj hwitness⟩, ?_⟩
810 simp only [Nat.cast_le]
811 apply hcard.trans
812 apply Finset.card_le_card
813 intro e he
814 simp only [SimpleGraph.mem_edgeFinset, SimpleGraph.edgeSet_fromEdgeSet,
815 Set.mem_diff, Finset.mem_coe, Sym2.mem_diagSet]
816 exact ⟨he, hnd e he⟩
817
818/-- **Step 3 (arithmetic)**: For large n, if n' ≤ 3n^{1-ε} log n then
819(n')^{1+ε+ε²} ≤ n/2.
820
821Proof:
822 (n')^{1+ε+ε²} ≤ (3n^{1-ε} log n)^{1+ε+ε²}
823 = 3^{1+ε+ε²} · n^{(1-ε)(1+ε+ε²)} · (log n)^{1+ε+ε²}
824 = 3^{1+ε+ε²} · n^{1-ε³} · (log n)^{1+ε+ε²} [since (1-ε)(1+ε+ε²) = 1-ε³]
825 By isLittleO_log_rpow_rpow_atTop (ε³ > 0): eventually
826 (log n)^{1+ε+ε²} ≤ n^{ε³} / (2 · 3^{1+ε+ε²})
827 So the bound is ≤ 3^{1+ε+ε²} · n^{1-ε³} · n^{ε³} / (2·3^{1+ε+ε²}) = n/2. -/
828private lemma edge_density_bound (ε : ℝ) (hε_pos : 0 < ε) :
829 ∃ M : ℕ, ∀ (n n' : ℕ), M ≤ n →
830 (↑n' : ℝ) ≤ 3 * (↑n : ℝ) ^ (1 - ε) * Real.log ↑n →
831 (↑n' : ℝ) ^ (1 + ε + ε ^ 2) ≤ (↑n : ℝ) / 2 := by
832 have hε3 : (0 : ℝ) < ε ^ 3 := by positivity
833 -- (log x)^(1+ε+ε²) =o[atTop] x^(ε³) since ε³ > 0
834 have hiso := isLittleO_log_rpow_rpow_atTop (1 + ε + ε ^ 2) hε3
835 -- Extract: eventually |log x|^(...) ≤ (2·3^{...})⁻¹ · x^(ε³)
836 have hc_pos : (0 : ℝ) < (2 * (3 : ℝ) ^ (1 + ε + ε ^ 2))⁻¹ := by positivity
837 have hbnd_nat : ∀ᶠ m : ℕ in atTop,
838 ‖Real.log (↑m : ℝ) ^ (1 + ε + ε ^ 2)‖ ≤
839 (2 * (3 : ℝ) ^ (1 + ε + ε ^ 2))⁻¹ * ‖(↑m : ℝ) ^ ε ^ 3‖ :=
840 tendsto_natCast_atTop_atTop.eventually (hiso.bound hc_pos)
841 rw [Filter.eventually_atTop] at hbnd_nat
842 obtain ⟨M₀, hM₀⟩ := hbnd_nat
843 -- M = max M₀ 3 ensures n ≥ 3 so log n ≥ 0
844 refine ⟨max M₀ 3, ?_⟩
845 intro n n' hn_ge hn'_le
846 have hM₀n : M₀ ≤ n := (Nat.le_max_left M₀ 3).trans hn_ge
847 have hn_ge3 : (3 : ℕ) ≤ n := (Nat.le_max_right M₀ 3).trans hn_ge
848 have hn_pos : (0 : ℝ) < (↑n : ℝ) := by exact_mod_cast show 0 < n by omega
849 have hnn : (0 : ℝ) ≤ (↑n : ℝ) := le_of_lt hn_pos
850 have hlog_nn : (0 : ℝ) ≤ Real.log (↑n : ℝ) :=
851 Real.log_nonneg (by norm_cast; linarith)
852 -- Trivial when n' = 0: (0:ℝ)^(1+ε+ε²) = 0 ≤ n/2
853 rcases Nat.eq_zero_or_pos n' with rfl | hn'_pos
854 · simp only [Nat.cast_zero,
855 Real.zero_rpow (show (1 + ε + ε ^ 2 : ℝ) ≠ 0 by positivity)]
856 positivity
857 -- Main case: n' > 0
858 have hn'_pos_r : (0 : ℝ) < (↑n' : ℝ) := Nat.cast_pos.mpr hn'_pos
859 -- Step 1: (n')^{1+ε+ε²} ≤ (3·n^{1-ε}·log n)^{1+ε+ε²}
860 have hstep1 : (↑n' : ℝ) ^ (1 + ε + ε ^ 2) ≤
861 (3 * (↑n : ℝ) ^ (1 - ε) * Real.log (↑n : ℝ)) ^ (1 + ε + ε ^ 2) :=
862 Real.rpow_le_rpow (by positivity) hn'_le (by positivity)
863 -- Step 2: expand (3·n^{1-ε}·log n)^{1+ε+ε²} = 3^{...}·n^{1-ε³}·(log n)^{...}
864 have hstep2 : (3 * (↑n : ℝ) ^ (1 - ε) * Real.log (↑n : ℝ)) ^ (1 + ε + ε ^ 2) =
865 (3 : ℝ) ^ (1 + ε + ε ^ 2) * (↑n : ℝ) ^ (1 - ε ^ 3) *
866 Real.log (↑n : ℝ) ^ (1 + ε + ε ^ 2) := by
867 rw [Real.mul_rpow (by positivity) hlog_nn,
868 Real.mul_rpow (by norm_num : (0 : ℝ) ≤ 3) (Real.rpow_nonneg hnn _),
869 ← Real.rpow_mul hnn, show (1 - ε) * (1 + ε + ε ^ 2) = 1 - ε ^ 3 from by ring]
870 -- Step 3: log bound from hM₀: (log n)^{...} ≤ (2·3^{...})⁻¹ · n^{ε³}
871 have hlog_bnd : Real.log (↑n : ℝ) ^ (1 + ε + ε ^ 2) ≤
872 (2 * (3 : ℝ) ^ (1 + ε + ε ^ 2))⁻¹ * (↑n : ℝ) ^ ε ^ 3 := by
873 have h := hM₀ n hM₀n
874 rwa [Real.norm_of_nonneg (Real.rpow_nonneg hlog_nn _),
875 Real.norm_of_nonneg (Real.rpow_nonneg hnn _)] at h
876 -- Step 4: algebraic simplification 3^r · n^{1-ε³} · (2·3^r)⁻¹ · n^{ε³} = n/2
877 have hstep4 : (3 : ℝ) ^ (1 + ε + ε ^ 2) * (↑n : ℝ) ^ (1 - ε ^ 3) *
878 ((2 * (3 : ℝ) ^ (1 + ε + ε ^ 2))⁻¹ * (↑n : ℝ) ^ ε ^ 3) = (↑n : ℝ) / 2 := by
879 have h3pos : (0 : ℝ) < (3 : ℝ) ^ (1 + ε + ε ^ 2) := by positivity
880 rw [show (3 : ℝ) ^ (1 + ε + ε ^ 2) * (↑n : ℝ) ^ (1 - ε ^ 3) *
881 ((2 * (3 : ℝ) ^ (1 + ε + ε ^ 2))⁻¹ * (↑n : ℝ) ^ ε ^ 3) =
882 (3 : ℝ) ^ (1 + ε + ε ^ 2) * (2 * (3 : ℝ) ^ (1 + ε + ε ^ 2))⁻¹ *
883 ((↑n : ℝ) ^ (1 - ε ^ 3) * (↑n : ℝ) ^ ε ^ 3) from by ring]
884 rw [← Real.rpow_add hn_pos, show (1 - ε ^ 3) + ε ^ 3 = 1 from by ring, Real.rpow_one]
885 have h_half : (3 : ℝ) ^ (1 + ε + ε ^ 2) * (2 * (3 : ℝ) ^ (1 + ε + ε ^ 2))⁻¹ = 1 / 2 := by
886 rw [mul_inv, mul_comm (2 : ℝ)⁻¹, ← mul_assoc,
887 mul_inv_cancel₀ h3pos.ne', one_mul, inv_eq_one_div]
888 rw [h_half]; ring
889 -- Chain the steps
890 calc (↑n' : ℝ) ^ (1 + ε + ε ^ 2)
891 ≤ (3 * (↑n : ℝ) ^ (1 - ε) * Real.log (↑n : ℝ)) ^ (1 + ε + ε ^ 2) := hstep1
892 _ = (3 : ℝ) ^ (1 + ε + ε ^ 2) * (↑n : ℝ) ^ (1 - ε ^ 3) *
893 Real.log (↑n : ℝ) ^ (1 + ε + ε ^ 2) := hstep2
894 _ ≤ (3 : ℝ) ^ (1 + ε + ε ^ 2) * (↑n : ℝ) ^ (1 - ε ^ 3) *
895 ((2 * (3 : ℝ) ^ (1 + ε + ε ^ 2))⁻¹ * (↑n : ℝ) ^ ε ^ 3) := by
896 gcongr
897 _ = (↑n : ℝ) / 2 := hstep4
898
899/-- Lemma 3.4/ch1: Densification lemma. -/
900theorem densification (ε : ℝ) (hε_pos : 0 < ε) (hε_le : ε ≤ 2 / 3) :
901 ∃ M : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V]
902 (G : SimpleGraph V) [DecidableRel G.Adj],
903 M ≤ Fintype.card V →
904 (∀ v : V, (Fintype.card V : ℝ) ^ ε ≤ ↑(G.degree v)) →
905 (∃ t : ℕ, Real.log ↑(Fintype.card V) ≤ ↑t ∧
906 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) G 1) ∨
907 (∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W)
908 (G' : SimpleGraph W) (_ : DecidableRel G'.Adj),
909 IsShallowMinor G' G 1 ∧
910 (Fintype.card V : ℝ) ^ (1 - ε) ≤ ↑(Fintype.card W) ∧
911 (Fintype.card W : ℝ) ^ (1 + ε + ε ^ 2) ≤ ↑(G'.edgeFinset.card)) := by
912 obtain ⟨M₁, hM₁⟩ := exists_good_pair ε hε_pos hε_le
913 obtain ⟨M₂, hM₂⟩ := edge_density_bound ε hε_pos
914 refine ⟨max M₁ M₂, ?_⟩
915 intro V _ _ G _ hn_ge hmin
916 have hM₁n : M₁ ≤ Fintype.card V := (Nat.le_max_left M₁ M₂).trans hn_ge
917 have hM₂n : M₂ ≤ Fintype.card V := (Nat.le_max_right M₁ M₂).trans hn_ge
918 obtain ⟨A, B, hAB, hA_lower, hA_upper, hB_lower, hB_nbrs⟩ := hM₁ G hM₁n hmin
919 rcases greedy_densify G A B hAB hB_nbrs with
920 ⟨t, ht_log, ht_minor⟩ | ⟨G', hG'_dec, hG'_minor, hG'_edges⟩
921 · exact Or.inl ⟨t, ht_log, ht_minor⟩
922 · right
923 refine ⟨{a : V // a ∈ A}, inferInstance, inferInstance, G', hG'_dec,
924 hG'_minor, ?_, ?_⟩
925 · -- (Fintype.card V)^{1-ε} ≤ Fintype.card W = A.card
926 simp only [Fintype.card_coe]
927 exact_mod_cast hA_lower
928 · -- (Fintype.card W)^{1+ε+ε²} ≤ G'.edgeFinset.card
929 simp only [Fintype.card_coe]
930 have h_arith : (↑A.card : ℝ) ^ (1 + ε + ε ^ 2) ≤ (↑(Fintype.card V) : ℝ) / 2 :=
931 hM₂ (Fintype.card V) A.card hM₂n (by exact_mod_cast hA_upper)
932 calc (↑A.card : ℝ) ^ (1 + ε + ε ^ 2)
933 ≤ (↑(Fintype.card V) : ℝ) / 2 := h_arith
934 _ ≤ ↑B.card := hB_lower
935 _ ≤ ↑G'.edgeFinset.card := hG'_edges
936
937end Catalog.Sparsity.Densification
938