Formalizing Structural Graph Theory in Lean 4

Catalog/VC/EasyEpsilonNetLemma/Full.lean
1import Catalog.VC.EpsilonNet.Full
2import Mathlib.Analysis.SpecialFunctions.Log.Basic
3import Mathlib.Algebra.Order.Floor.Semiring
4import Mathlib.Data.Finset.BooleanAlgebra
5import Mathlib.Data.Fintype.BigOperators
6import Mathlib.Data.Fintype.Powerset
7
8namespace Catalog.VC.EasyEpsilonNetLemma
9
10open Classical
11
12private lemma ground_card_pos {Ξ± : Type*} [DecidableEq Ξ±] [Fintype Ξ±]
13 (π’œ : Finset (Finset Ξ±)) (hπ’œ : 2 ≀ π’œ.card) : 0 < Fintype.card Ξ± := by
14 have hfamily : 2 ≀ Fintype.card (Finset Ξ±) := le_trans hπ’œ (Finset.card_le_univ π’œ)
15 rw [Fintype.card_finset] at hfamily
16 by_contra hΞ±
17 have hΞ±0 : Fintype.card Ξ± = 0 := Nat.eq_zero_of_not_pos hΞ±
18 simp [hΞ±0] at hfamily
19
20private lemma sampleSize_pos {n : β„•} (hn : 2 ≀ n) {r : ℝ} (hr : 1 < r) :
21 0 < ⌈r * Real.log (n : ℝ)βŒ‰β‚Š := by
22 refine Nat.ceil_pos.mpr ?_
23 have hnR : (1 : ℝ) < n := by
24 exact_mod_cast (lt_of_lt_of_le (by decide : 1 < 2) hn)
25 have hlogn : 0 < Real.log (n : ℝ) := Real.log_pos hnR
26 positivity
27
28private lemma sampleSize_bound {n : β„•} (hn : 2 ≀ n) {r : ℝ} (hr : 1 < r) :
29 (((⌈r * Real.log (n : ℝ)βŒ‰β‚Š : β„•) : ℝ)) ≀ r * Real.log (n : ℝ) + 1 := by
30 have hnR : (1 : ℝ) < n := by
31 exact_mod_cast (lt_of_lt_of_le (by decide : 1 < 2) hn)
32 have hlogn : 0 < Real.log (n : ℝ) := Real.log_pos hnR
33 have hx : 0 ≀ r * Real.log (n : ℝ) := by positivity
34 linarith [Nat.ceil_lt_add_one hx]
35
36private lemma badTupleCount_eq {Ξ± : Type*} [DecidableEq Ξ±] [Fintype Ξ±]
37 (S : Finset Ξ±) (s : β„•) :
38 (Finset.univ.filter (fun f : Fin s β†’ Ξ± => βˆ€ i, f i βˆ‰ S)).card =
39 (Fintype.card Ξ± - S.card) ^ s := by
40 let p : Set (Fin s β†’ Ξ±) := {f | βˆ€ i, f i βˆ‰ S}
41 have hcard :
42 Fintype.card p = (Finset.univ.filter (fun f : Fin s β†’ Ξ± => βˆ€ i, f i βˆ‰ S)).card := by
43 simpa [p] using
44 (Fintype.card_ofFinset (p := p)
45 (Finset.univ.filter (fun f : Fin s β†’ Ξ± => βˆ€ i, f i βˆ‰ S))
46 (fun f => by simp [p]))
47 have hsub : Fintype.card p = (Fintype.card Ξ± - S.card) ^ s := by
48 let e : p ≃ (Fin s β†’ β†₯(Sᢜ : Finset Ξ±)) :=
49 { toFun := fun f i => ⟨f.1 i, by exact Finset.mem_compl.mpr (f.2 i)⟩
50 invFun := fun g => ⟨fun i => (g i).1, by intro i; exact Finset.mem_compl.mp (g i).2⟩
51 left_inv := by intro f; ext i; rfl
52 right_inv := by intro g; ext i; rfl }
53 rw [Fintype.card_congr e, Fintype.card_fun, Fintype.card_coe, Finset.card_compl,
54 Fintype.card_fin]
55 exact hcard.symm.trans hsub
56
57private lemma tupleImage_isEpsilonNet {Ξ± : Type*} [DecidableEq Ξ±] [Fintype Ξ±]
58 (π’œ : Finset (Finset Ξ±)) {r : ℝ} {s : β„•} (f : Fin s β†’ Ξ±)
59 (hf : βˆ€ S ∈ π’œ, (1 / r) * (Fintype.card Ξ± : ℝ) ≀ (S.card : ℝ) β†’ βˆƒ i, f i ∈ S) :
60 Catalog.VC.EpsilonNet.IsEpsilonNet π’œ (1 / r) (Finset.univ.image f) := by
61 intro S hS hheavy
62 rcases hf S hS hheavy with ⟨i, hi⟩
63 refine ⟨f i, Finset.mem_inter.mpr ⟨?_, hi⟩⟩
64 exact Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩
65
66private lemma tupleImage_card_le {Ξ± : Type*} [DecidableEq Ξ±] [Fintype Ξ±]
67 {s : β„•} (f : Fin s β†’ Ξ±) :
68 (((Finset.univ.image f).card : β„•) : ℝ) ≀ s := by
69 exact_mod_cast (show (Finset.univ.image f).card ≀ s by
70 simpa [Fintype.card_fin] using
71 (Finset.card_image_le : (Finset.univ.image f).card ≀ Finset.univ.card))
72
73/-- For any finite set family and `r > 1`, there exists a `(1/r)`-net of size
74 at most `r Β· ln |π’œ| + 1`. (Lemma 5.11) -/
75theorem easyEpsilonNetLemma {Ξ± : Type*} [DecidableEq Ξ±] [Fintype Ξ±]
76 (π’œ : Finset (Finset Ξ±)) (hπ’œ : 2 ≀ π’œ.card) {r : ℝ} (hr : 1 < r) :
77 βˆƒ N : Finset Ξ±, Catalog.VC.EpsilonNet.IsEpsilonNet π’œ (1 / r) N ∧
78 (N.card : ℝ) ≀ r * Real.log (π’œ.card : ℝ) + 1 := by
79 let s : β„• := ⌈r * Real.log (π’œ.card : ℝ)βŒ‰β‚Š
80 have hΞ±pos : 0 < Fintype.card Ξ± := ground_card_pos π’œ hπ’œ
81 have hs_pos : 0 < s := by
82 simpa [s] using sampleSize_pos hπ’œ hr
83 have hs_bound : ((s : β„•) : ℝ) ≀ r * Real.log (π’œ.card : ℝ) + 1 := by
84 simpa [s] using sampleSize_bound hπ’œ hr
85 have hgood :
86 βˆƒ f : Fin s β†’ Ξ±,
87 βˆ€ S ∈ π’œ, (1 / r) * (Fintype.card Ξ± : ℝ) ≀ (S.card : ℝ) β†’ βˆƒ i, f i ∈ S := by
88 let H : Finset (Finset Ξ±) :=
89 π’œ.filter (fun S => (1 / r) * (Fintype.card Ξ± : ℝ) ≀ (S.card : ℝ))
90 let B : Finset Ξ± β†’ Finset (Fin s β†’ Ξ±) :=
91 fun S => Finset.univ.filter (fun f : Fin s β†’ Ξ± => βˆ€ i, f i βˆ‰ S)
92 let Bad : Finset (Fin s β†’ Ξ±) := H.biUnion B
93 have hHcard : H.card ≀ π’œ.card := by
94 simpa [H] using
95 (Finset.card_filter_le
96 (s := π’œ) (p := fun S => (1 / r) * (Fintype.card Ξ± : ℝ) ≀ (S.card : ℝ)))
97 have hbase_nonneg : 0 ≀ 1 - 1 / r := by
98 have hr1 : (1 : ℝ) / r < 1 := by
99 have hr0 : (0 : ℝ) < r := lt_trans zero_lt_one hr
100 rw [div_lt_iffβ‚€ hr0]
101 simpa using hr
102 linarith
103 have hB_bound :
104 βˆ€ S ∈ H, ((B S).card : ℝ) ≀ (Fintype.card Ξ± : ℝ) ^ s * (1 - 1 / r) ^ s := by
105 intro S hS
106 have hSheavy : (1 / r) * (Fintype.card Ξ± : ℝ) ≀ (S.card : ℝ) := by
107 simpa [H] using Finset.mem_filter.mp hS |>.2
108 have hcard_le :
109 ((Fintype.card Ξ± - S.card : β„•) : ℝ) ≀ (Fintype.card Ξ± : ℝ) * (1 - 1 / r) := by
110 have hScard_le_nat : S.card ≀ Fintype.card Ξ± := Finset.card_le_univ S
111 have hScard_le : (S.card : ℝ) ≀ Fintype.card Ξ± := by exact_mod_cast hScard_le_nat
112 rw [Nat.cast_sub hScard_le_nat]
113 linarith
114 calc
115 ((B S).card : ℝ) = ((Fintype.card Ξ± - S.card : β„•) : ℝ) ^ s := by
116 simp [B, badTupleCount_eq]
117 _ ≀ ((Fintype.card Ξ± : ℝ) * (1 - 1 / r)) ^ s := by
118 exact pow_le_pow_leftβ‚€ (by positivity) hcard_le s
119 _ = (Fintype.card Ξ± : ℝ) ^ s * (1 - 1 / r) ^ s := by
120 rw [mul_pow]
121 have hBad_bound :
122 (Bad.card : ℝ) ≀ (H.card : ℝ) * ((Fintype.card Ξ± : ℝ) ^ s * (1 - 1 / r) ^ s) := by
123 have hbiUnion :
124 Bad.card ≀ βˆ‘ S ∈ H, (B S).card := by
125 simpa [Bad] using (Finset.card_biUnion_le : (H.biUnion B).card ≀ βˆ‘ S ∈ H, (B S).card)
126 calc
127 (Bad.card : ℝ) ≀ (βˆ‘ S ∈ H, (B S).card : β„•) := by
128 exact_mod_cast hbiUnion
129 _ = βˆ‘ S ∈ H, ((B S).card : ℝ) := by rw [Nat.cast_sum]
130 _ ≀ βˆ‘ S ∈ H, ((Fintype.card Ξ± : ℝ) ^ s * (1 - 1 / r) ^ s) := by
131 exact Finset.sum_le_sum fun S hS => hB_bound S hS
132 _ = (H.card : ℝ) * ((Fintype.card Ξ± : ℝ) ^ s * (1 - 1 / r) ^ s) := by
133 rw [Finset.sum_const, nsmul_eq_mul]
134 have hdecay_exp :
135 (1 - 1 / r) ^ s < Real.exp (-(s : ℝ) / r) := by
136 have hone :
137 1 - 1 / r < Real.exp (-(1 / r)) := by
138 have hr0 : (0 : ℝ) < r := lt_trans zero_lt_one hr
139 refine Real.one_sub_lt_exp_neg ?_
140 exact one_div_ne_zero hr0.ne'
141 calc
142 (1 - 1 / r) ^ s < (Real.exp (-(1 / r))) ^ s := by
143 exact pow_lt_pow_leftβ‚€ hone hbase_nonneg (Nat.ne_of_gt hs_pos)
144 _ = Real.exp ((s : ℝ) * (-(1 / r))) := by
145 rw [← Real.exp_nat_mul]
146 _ = Real.exp (-(s : ℝ) / r) := by ring_nf
147 have hs_ge : r * Real.log (π’œ.card : ℝ) ≀ (s : ℝ) := by
148 simpa [s] using (Nat.le_ceil (r * Real.log (π’œ.card : ℝ)))
149 have hexp_le : Real.exp (-(s : ℝ) / r) ≀ 1 / (π’œ.card : ℝ) := by
150 have hApos_nat : 0 < π’œ.card := lt_of_lt_of_le (by decide : 0 < 2) hπ’œ
151 have hApos : (0 : ℝ) < π’œ.card := by exact_mod_cast hApos_nat
152 have hs_div : Real.log (π’œ.card : ℝ) ≀ (s : ℝ) / r := by
153 have hr0 : (0 : ℝ) < r := lt_trans zero_lt_one hr
154 exact (le_div_iffβ‚€ hr0).2 <| by simpa [mul_comm] using hs_ge
155 have hneg : -(s : ℝ) / r ≀ -Real.log (π’œ.card : ℝ) := by
156 simpa [neg_div] using
157 (neg_le_neg hs_div : -((s : ℝ) / r) ≀ -Real.log (π’œ.card : ℝ))
158 calc
159 Real.exp (-(s : ℝ) / r) ≀ Real.exp (-Real.log (π’œ.card : ℝ)) := by
160 exact Real.exp_le_exp.mpr hneg
161 _ = 1 / (π’œ.card : ℝ) := by
162 rw [Real.exp_neg, Real.exp_log hApos, one_div]
163 have hfactor_lt_one : (H.card : ℝ) * (1 - 1 / r) ^ s < 1 := by
164 have hHcardR : (H.card : ℝ) ≀ π’œ.card := by
165 exact_mod_cast hHcard
166 calc
167 (H.card : ℝ) * (1 - 1 / r) ^ s
168 ≀ (π’œ.card : ℝ) * (1 - 1 / r) ^ s := by
169 exact mul_le_mul_of_nonneg_right hHcardR (by positivity)
170 _ < (π’œ.card : ℝ) * Real.exp (-(s : ℝ) / r) := by
171 gcongr
172 _ ≀ (π’œ.card : ℝ) * (1 / (π’œ.card : ℝ)) := by
173 gcongr
174 _ = 1 := by
175 have hApos_nat : 0 < π’œ.card := lt_of_lt_of_le (by decide : 0 < 2) hπ’œ
176 have hAne : (π’œ.card : ℝ) β‰  0 := by
177 exact_mod_cast (Nat.ne_of_gt hApos_nat)
178 field_simp [hAne]
179 have htotal_pos : 0 < (Fintype.card Ξ± : ℝ) ^ s := by positivity
180 have hBad_lt_total : (Bad.card : ℝ) < (Fintype.card (Fin s β†’ Ξ±) : ℝ) := by
181 calc
182 (Bad.card : ℝ)
183 ≀ (H.card : ℝ) * ((Fintype.card Ξ± : ℝ) ^ s * (1 - 1 / r) ^ s) := hBad_bound
184 _ = ((Fintype.card Ξ± : ℝ) ^ s) * ((H.card : ℝ) * (1 - 1 / r) ^ s) := by ring
185 _ < ((Fintype.card Ξ± : ℝ) ^ s) * 1 := by
186 gcongr
187 _ = Fintype.card (Fin s β†’ Ξ±) := by
188 rw [mul_one, Fintype.card_fun, Fintype.card_fin, Nat.cast_pow]
189 have hBad_lt_total_nat : Bad.card < Fintype.card (Fin s β†’ Ξ±) := by
190 exact_mod_cast hBad_lt_total
191 rcases Finset.exists_mem_notMem_of_card_lt_card hBad_lt_total_nat with ⟨f, hf_univ, hfBad⟩
192 refine ⟨f, ?_⟩
193 intro S hS hSheavy
194 have hSH : S ∈ H := by
195 change S ∈ π’œ.filter (fun T => (1 / r) * (Fintype.card Ξ± : ℝ) ≀ (T.card : ℝ))
196 exact Finset.mem_filter.mpr ⟨hS, hSheavy⟩
197 have hf_notB : f βˆ‰ B S := by
198 intro hfB
199 exact hfBad (by
200 simpa [Bad, Finset.mem_biUnion] using ⟨S, hSH, hfB⟩)
201 by_contra hhit
202 apply hf_notB
203 simp [B]
204 intro i hi
205 exact hhit ⟨i, hi⟩
206 rcases hgood with ⟨f, hf⟩
207 refine ⟨Finset.univ.image f, tupleImage_isEpsilonNet π’œ f hf, ?_⟩
208 calc
209 (((Finset.univ.image f).card : β„•) : ℝ) ≀ s := tupleImage_card_le f
210 _ ≀ r * Real.log (π’œ.card : ℝ) + 1 := hs_bound
211
212end Catalog.VC.EasyEpsilonNetLemma
213