Formalizing Structural Graph Theory in Lean 4

Catalog/VC/EpsilonNetTheorem/Full.lean
1import Catalog.VC.VCDimension.Full
2import Catalog.VC.EpsilonNet.Full
3import Catalog.VC.EpsilonApproximation.Full
4import Catalog.VC.EpsilonApproximationBound.Full
5import Catalog.VC.EasyEpsilonNetLemma.Full
6import Mathlib.Analysis.SpecialFunctions.Log.Basic
7import Mathlib.Analysis.Complex.ExponentialBounds
8
9namespace Catalog.VC.EpsilonNetTheorem
10
11open Real
12
13/-! ## Helper lemmas -/
14
15/-- The trace family obtained by restricting each `S ∈ π’œ` to `Y`,
16 viewed as a family on the subtype `Y`. -/
17private noncomputable def traceFamily {Ξ± : Type*} [DecidableEq Ξ±]
18 (π’œ : Finset (Finset Ξ±)) (Y : Finset Ξ±) : Finset (Finset Y) :=
19 π’œ.image (fun S => S.subtype (Β· ∈ Y))
20
21/-- If the trace family on `Y` shatters `s`, then `π’œ` shatters
22 `s.map Subtype.val` (which has the same cardinality). -/
23private lemma traceFamily_shatters {Ξ± : Type*} [DecidableEq Ξ±]
24 (π’œ : Finset (Finset Ξ±)) (Y : Finset Ξ±) (s : Finset Y)
25 (hs : (traceFamily π’œ Y).Shatters s) :
26 π’œ.Shatters (s.map (Function.Embedding.subtype _)) := by
27 intro tΞ± htΞ±
28 -- tΞ± βŠ† s.map val. Pull back to Y.
29 set sΞ± : Finset Ξ± := s.map (Function.Embedding.subtype _) with hsΞ±
30 -- Each element of tΞ± belongs to Y.
31 have htΞ±_Y : βˆ€ x ∈ tΞ±, x ∈ Y := by
32 intro x hx
33 have : x ∈ sα := htα hx
34 rw [hsΞ±, Finset.mem_map] at this
35 obtain ⟨y, _, rfl⟩ := this
36 exact y.2
37 -- Build t : Finset Y as the subtype of tΞ±
38 let t : Finset Y := tα.subtype (· ∈ Y)
39 have ht_sub : t βŠ† s := by
40 intro y hy
41 simp only [t, Finset.mem_subtype] at hy
42 have hy_sα : (y : α) ∈ sα := htα hy
43 rw [hsΞ±, Finset.mem_map] at hy_sΞ±
44 obtain ⟨y', hy', heq⟩ := hy_sα
45 have : y = y' := Subtype.ext heq.symm
46 rw [this]; exact hy'
47 obtain ⟨u', hu'_mem, hu'_eq⟩ := hs ht_sub
48 rw [traceFamily, Finset.mem_image] at hu'_mem
49 obtain ⟨S, hS_mem, rfl⟩ := hu'_mem
50 refine ⟨S, hS_mem, ?_⟩
51 ext x
52 simp only [Finset.mem_inter, hsΞ±, Finset.mem_map, Function.Embedding.subtype]
53 constructor
54 · rintro ⟨⟨y, hy_s, rfl⟩, hyS⟩
55 have hy_in : y ∈ s ∩ S.subtype (· ∈ Y) := by
56 refine Finset.mem_inter.mpr ⟨hy_s, ?_⟩
57 simpa [Finset.mem_subtype] using hyS
58 rw [hu'_eq] at hy_in
59 simp only [t, Finset.mem_subtype] at hy_in
60 exact hy_in
61 Β· intro hxt
62 have hxY : x ∈ Y := htα_Y x hxt
63 have : (⟨x, hxY⟩ : Y) ∈ t := by
64 simp [t, Finset.mem_subtype, hxt]
65 rw [← hu'_eq] at this
66 rw [Finset.mem_inter] at this
67 obtain ⟨h1, h2⟩ := this
68 refine ⟨⟨⟨x, hxY⟩, h1, rfl⟩, ?_⟩
69 simpa [Finset.mem_subtype] using h2
70
71/-- Restricting the family to `Y` cannot increase VC-dimension. -/
72private lemma traceFamily_vcDim_le {Ξ± : Type*} [DecidableEq Ξ±]
73 (π’œ : Finset (Finset Ξ±)) (Y : Finset Ξ±) :
74 (traceFamily π’œ Y).vcDim ≀ π’œ.vcDim := by
75 unfold Finset.vcDim
76 refine Finset.sup_le ?_
77 intro s hs
78 rw [Finset.mem_shatterer] at hs
79 have h := traceFamily_shatters π’œ Y s hs
80 have hcard := h.card_le_vcDim
81 rwa [Finset.card_map] at hcard
82
83/-- Cardinality of the subtype-restricted set in real numbers. -/
84private lemma card_subtype_eq_inter {Ξ± : Type*} [DecidableEq Ξ±]
85 (Y S : Finset Ξ±) :
86 ((S.subtype (Β· ∈ Y) : Finset Y).card : ℝ) = ((S ∩ Y).card : ℝ) := by
87 norm_cast
88 rw [Finset.card_subtype, ← Finset.filter_mem_eq_inter]
89
90/-- Sauer-Shelah bound applied to the trace family on `Y`:
91 `|traceFamily π’œ Y| ≀ βˆ‘_{k≀d} (|Y| choose k) ≀ (d+1)*(|Y|+1)^d`. -/
92private lemma traceFamily_card_le {Ξ± : Type*} [DecidableEq Ξ±]
93 (π’œ : Finset (Finset Ξ±)) (d : β„•) (hd : π’œ.vcDim ≀ d) (Y : Finset Ξ±) :
94 ((traceFamily π’œ Y).card : ℝ) ≀ (d + 1 : β„•) * (Y.card + 1 : ℝ) ^ d := by
95 classical
96 set π’œ' := traceFamily π’œ Y
97 have h1 : π’œ'.card ≀ βˆ‘ k ∈ Finset.Iic π’œ'.vcDim, (Fintype.card Y).choose k :=
98 le_trans π’œ'.card_le_card_shatterer Finset.card_shatterer_le_sum_vcDim
99 have hdim : π’œ'.vcDim ≀ d :=
100 le_trans (traceFamily_vcDim_le π’œ Y) hd
101 have h2 : βˆ‘ k ∈ Finset.Iic π’œ'.vcDim, (Fintype.card Y).choose k
102 ≀ βˆ‘ k ∈ Finset.Iic d, (Fintype.card Y).choose k := by
103 apply Finset.sum_le_sum_of_subset
104 intro k hk
105 simp only [Finset.mem_Iic] at *
106 exact le_trans hk hdim
107 have h3 : π’œ'.card ≀ βˆ‘ k ∈ Finset.Iic d, (Y.card).choose k := by
108 have := h1.trans h2
109 simpa [Fintype.card_coe] using this
110 -- Now βˆ‘_{k≀d} (n.choose k) ≀ (d+1) * (n+1)^d
111 have hbound : (βˆ‘ k ∈ Finset.Iic d, (Y.card).choose k : ℝ)
112 ≀ (d + 1 : β„•) * (Y.card + 1 : ℝ) ^ d := by
113 have hsum : (βˆ‘ k ∈ Finset.Iic d, ((Y.card).choose k : ℝ))
114 ≀ βˆ‘ _k ∈ Finset.Iic d, ((Y.card + 1 : ℝ) ^ d) := by
115 apply Finset.sum_le_sum
116 intro k hk
117 simp only [Finset.mem_Iic] at hk
118 have h_nat : ((Y.card).choose k : ℝ) ≀ (Y.card : ℝ) ^ k := by
119 exact_mod_cast Nat.choose_le_pow Y.card k
120 have h_pow : (Y.card : ℝ) ^ k ≀ (Y.card + 1 : ℝ) ^ d := by
121 have h_le : (Y.card : ℝ) ≀ Y.card + 1 := by linarith
122 have h_nn : (0 : ℝ) ≀ Y.card := by positivity
123 have h1 : (Y.card : ℝ) ^ k ≀ (Y.card + 1 : ℝ) ^ k :=
124 pow_le_pow_leftβ‚€ h_nn h_le k
125 have h2 : (Y.card + 1 : ℝ) ^ k ≀ (Y.card + 1 : ℝ) ^ d := by
126 apply pow_le_pow_rightβ‚€
127 Β· linarith
128 Β· exact hk
129 linarith
130 linarith
131 have : (βˆ‘ k ∈ Finset.Iic d, (Y.card).choose k : ℝ)
132 = βˆ‘ k ∈ Finset.Iic d, ((Y.card).choose k : ℝ) := rfl
133 rw [this]
134 refine hsum.trans ?_
135 rw [Finset.sum_const, Nat.card_Iic, nsmul_eq_mul]
136 have h4 : ((traceFamily π’œ Y).card : ℝ) ≀ (βˆ‘ k ∈ Finset.Iic d, (Y.card).choose k : ℝ) := by
137 exact_mod_cast h3
138 exact h4.trans hbound
139
140/-- Analytic constant: given `C₁ > 0` and `d : β„•`, produce `C > 0` such that
141 for all `r β‰₯ 2` and all `m β‰₯ 0` with
142 `m ≀ (d+1) * (C₁ Β· (4r)Β² Β· log(4r) + 1)^d`,
143 we have `2r Β· log m + 1 ≀ C Β· r Β· log r`. -/
144private lemma analytic_constant (C₁ : ℝ) (hC₁ : 0 < C₁) (d : β„•) :
145 βˆƒ C : ℝ, 1 ≀ C ∧ βˆ€ (r : ℝ), 2 ≀ r β†’
146 βˆ€ (m : ℝ), 0 < m β†’ m ≀ ((d : ℝ) + 1) * (C₁ * (4*r)^2 * Real.log (4*r) + 1)^d β†’
147 2 * r * Real.log m + 1 ≀ C * r * Real.log r := by
148 have hlog2_pos : 0 < Real.log 2 := Real.log_pos one_lt_two
149 have hlog2_gt : (1 : ℝ) / 2 < Real.log 2 := by
150 have := Real.log_two_gt_d9; linarith
151 have hbase_pos : (0 : ℝ) < 64 * C₁ + 1 := by linarith
152 have hbase_gt1 : (1 : ℝ) < 64 * C₁ + 1 := by linarith
153 set K : ℝ := Real.log ((d : ℝ) + 1) + (d : ℝ) * Real.log (64 * C₁ + 1) with hK_def
154 have hd_nn : (0 : ℝ) ≀ (d : ℝ) := by exact_mod_cast Nat.zero_le d
155 have hK_nn : 0 ≀ K := by
156 have h1 : (0 : ℝ) ≀ Real.log ((d : ℝ) + 1) :=
157 Real.log_nonneg (by linarith)
158 have h2 : (0 : ℝ) ≀ (d : ℝ) * Real.log (64 * C₁ + 1) :=
159 mul_nonneg hd_nn (Real.log_nonneg hbase_gt1.le)
160 linarith
161 set L : ℝ := K / Real.log 2 + 3 * (d : ℝ) with hL_def
162 have hL_nn : 0 ≀ L := by
163 have h1 : 0 ≀ K / Real.log 2 := div_nonneg hK_nn hlog2_pos.le
164 have h2 : 0 ≀ 3 * (d : ℝ) := by linarith
165 linarith
166 set C : ℝ := 2 * L + 1 / Real.log 2 + 1 with hC_def
167 have hlog2_lt1 : Real.log 2 < 1 := by
168 have := Real.log_two_lt_d9; linarith
169 have hinv_ge : (1 : ℝ) ≀ 1 / Real.log 2 := by
170 rw [le_div_iffβ‚€ hlog2_pos]; linarith
171 refine ⟨C, by linarith, ?_⟩
172 intro r hr m hm_pos hm_le
173 have hr_pos : 0 < r := by linarith
174 have hlogr_pos : 0 < Real.log r := Real.log_pos (by linarith)
175 have hlogr_ge_log2 : Real.log 2 ≀ Real.log r :=
176 Real.log_le_log (by norm_num) hr
177 -- r Β· log r β‰₯ 1
178 have hrlogr_ge1 : (1 : ℝ) ≀ r * Real.log r := by
179 nlinarith [hlogr_ge_log2, hlog2_gt, hr]
180 -- Bound on M := C₁·(4r)Β² Β· log(4r) + 1
181 set M : ℝ := C₁ * (4 * r) ^ 2 * Real.log (4 * r) + 1 with hM_def
182 have h4r_pos : 0 < 4 * r := by linarith
183 have h4r_ge1 : (1 : ℝ) ≀ 4 * r := by linarith
184 have hlog4r_nn : 0 ≀ Real.log (4 * r) := Real.log_nonneg h4r_ge1
185 have hlog4r_le : Real.log (4 * r) ≀ 4 * r := Real.log_le_self h4r_pos.le
186 have hM_pos : 0 < M := by
187 have : 0 ≀ C₁ * (4 * r) ^ 2 * Real.log (4 * r) := by positivity
188 linarith
189 have hr3_ge1 : (1 : ℝ) ≀ r ^ 3 := by nlinarith
190 have hr3_pos : 0 < r ^ 3 := by positivity
191 have hM_le : M ≀ (64 * C₁ + 1) * r ^ 3 := by
192 have hbody : C₁ * (4 * r) ^ 2 * Real.log (4 * r) ≀ 64 * C₁ * r ^ 3 := by
193 have hsq : (4 * r) ^ 2 = 16 * r ^ 2 := by ring
194 rw [hsq]
195 have h1 : C₁ * (16 * r ^ 2) * Real.log (4 * r)
196 ≀ C₁ * (16 * r ^ 2) * (4 * r) :=
197 mul_le_mul_of_nonneg_left hlog4r_le (by positivity)
198 nlinarith [h1]
199 nlinarith [hbody, hr3_ge1, hC₁]
200 have hRHS_pos : 0 < (64 * C₁ + 1) * r ^ 3 := by positivity
201 have hlogM_le : Real.log M ≀ Real.log (64 * C₁ + 1) + 3 * Real.log r := by
202 have h1 : Real.log M ≀ Real.log ((64 * C₁ + 1) * r ^ 3) :=
203 Real.log_le_log hM_pos hM_le
204 have h2 : Real.log ((64 * C₁ + 1) * r ^ 3)
205 = Real.log (64 * C₁ + 1) + 3 * Real.log r := by
206 rw [Real.log_mul hbase_pos.ne' hr3_pos.ne', Real.log_pow]
207 push_cast; ring
208 linarith
209 -- Bound on log of upper bound
210 set U : ℝ := ((d : ℝ) + 1) * M ^ d with hU_def
211 have hd1_pos : (0 : ℝ) < (d : ℝ) + 1 := by linarith
212 have hMd_pos : 0 < M ^ d := pow_pos hM_pos d
213 have hU_pos : 0 < U := mul_pos hd1_pos hMd_pos
214 have hlogU_eq : Real.log U
215 = Real.log ((d : ℝ) + 1) + (d : ℝ) * Real.log M := by
216 rw [hU_def, Real.log_mul hd1_pos.ne' hMd_pos.ne', Real.log_pow]
217 have hlogU_le : Real.log U ≀ K + 3 * (d : ℝ) * Real.log r := by
218 rw [hlogU_eq]
219 have h1 : (d : ℝ) * Real.log M
220 ≀ (d : ℝ) * (Real.log (64 * C₁ + 1) + 3 * Real.log r) :=
221 mul_le_mul_of_nonneg_left hlogM_le hd_nn
222 have h2 : (d : ℝ) * (Real.log (64 * C₁ + 1) + 3 * Real.log r)
223 = (d : ℝ) * Real.log (64 * C₁ + 1) + 3 * (d : ℝ) * Real.log r := by
224 ring
225 rw [hK_def]; linarith
226 have hlogm_le : Real.log m ≀ K + 3 * (d : ℝ) * Real.log r :=
227 le_trans (Real.log_le_log hm_pos hm_le) hlogU_le
228 -- K ≀ (K / log 2) Β· log r since log r β‰₯ log 2 and K β‰₯ 0
229 have hK_le : K ≀ (K / Real.log 2) * Real.log r := by
230 rw [div_mul_eq_mul_div, le_div_iffβ‚€ hlog2_pos]
231 exact mul_le_mul_of_nonneg_left hlogr_ge_log2 hK_nn
232 -- 2 r log m ≀ 2 L Β· r Β· log r
233 have h2r_nn : (0 : ℝ) ≀ 2 * r := by linarith
234 have hstep1 : 2 * r * Real.log m
235 ≀ 2 * r * (K + 3 * (d : ℝ) * Real.log r) :=
236 mul_le_mul_of_nonneg_left hlogm_le h2r_nn
237 have hstep2 : 2 * r * (K + 3 * (d : ℝ) * Real.log r)
238 ≀ 2 * L * (r * Real.log r) := by
239 have hK_mul : 2 * r * K ≀ 2 * r * ((K / Real.log 2) * Real.log r) :=
240 mul_le_mul_of_nonneg_left hK_le h2r_nn
241 have hexpand : 2 * r * ((K / Real.log 2) * Real.log r) + 2 * r * (3 * (d : ℝ) * Real.log r)
242 = 2 * L * (r * Real.log r) := by
243 rw [hL_def]; ring
244 linarith
245 -- 1 ≀ (1/log 2 + 1) Β· r Β· log r
246 have htail : (1 : ℝ) ≀ (1 / Real.log 2 + 1) * (r * Real.log r) := by
247 have h1 : (1 : ℝ) ≀ 1 * (r * Real.log r) := by linarith
248 have h2 : 0 ≀ (1 / Real.log 2) * (r * Real.log r) := by
249 apply mul_nonneg (by positivity)
250 linarith
251 nlinarith
252 have hCexpand : C * r * Real.log r
253 = 2 * L * (r * Real.log r) + (1 / Real.log 2 + 1) * (r * Real.log r) := by
254 rw [hC_def]; ring
255 rw [hCexpand]
256 linarith [hstep1, hstep2, htail]
257
258/-! ## Main theorem -/
259
260theorem epsilonNetTheorem (d : β„•) : βˆƒ C : ℝ, 0 < C ∧
261 βˆ€ (Ξ± : Type*) [DecidableEq Ξ±] [Fintype Ξ±] [Nonempty Ξ±] (π’œ : Finset (Finset Ξ±)),
262 π’œ.vcDim ≀ d β†’
263 βˆ€ (r : ℝ), 2 ≀ r β†’
264 βˆƒ N : Finset Ξ±, Catalog.VC.EpsilonNet.IsEpsilonNet π’œ (1 / r) N ∧
265 (N.card : ℝ) ≀ C * r * Real.log r := by
266 obtain ⟨C₁, hC₁_pos, happrox⟩ := Catalog.VC.EpsilonApproximationBound.epsilonApproxBound d
267 obtain ⟨C, hC_ge_one, hCbound⟩ := analytic_constant C₁ hC₁_pos d
268 have hC_pos : 0 < C := lt_of_lt_of_le one_pos hC_ge_one
269 refine ⟨C, hC_pos, ?_⟩
270 intro Ξ± _ _ _ π’œ hd r hr
271 -- Apply approxBound at parameter 4r
272 have hr_pos : 0 < r := by linarith
273 have h4r : (2 : ℝ) ≀ 4 * r := by linarith
274 have h4r_pos : 0 < 4 * r := by linarith
275 have h4r_one : (1 : ℝ) < 4 * r := by linarith
276 obtain ⟨Y, hY_approx, hY_size⟩ := happrox Ξ± π’œ hd (4 * r) h4r
277 set π’œ' : Finset (Finset Y) := traceFamily π’œ Y with hπ’œ'_def
278 -- Case split on |π’œ'| β‰₯ 2
279 by_cases hcard : 2 ≀ π’œ'.card
280 Β· -- Apply easyEpsilonNetLemma with parameter 2r
281 have h2r_one : (1 : ℝ) < 2 * r := by linarith
282 obtain ⟨N_β, hN_net, hN_size⟩ :=
283 Catalog.VC.EasyEpsilonNetLemma.easyEpsilonNetLemma π’œ' hcard (r := 2 * r) h2r_one
284 refine ⟨N_β.image (Subtype.val), ?_, ?_⟩
285 Β· -- IsEpsilonNet π’œ (1/r) N
286 intro S hS hheavy
287 -- The trace S' = S.subtype (· ∈ Y)
288 let S' : Finset Y := S.subtype (· ∈ Y)
289 have hS'_mem : S' ∈ π’œ' := by
290 rw [hπ’œ'_def, traceFamily, Finset.mem_image]
291 exact ⟨S, hS, rfl⟩
292 -- approx gives: |S'|/|Y| β‰₯ |S|/|Ξ±| - 1/(4r) β‰₯ 1/r - 1/(4r) = 3/(4r) β‰₯ 1/(2r)
293 have hY_approx_S := hY_approx S hS
294 have hΞ±_pos : (0 : ℝ) < Fintype.card Ξ± := by
295 exact_mod_cast (Fintype.card_pos : 0 < Fintype.card Ξ±)
296 have hSdens_lb : (1 : ℝ) / r ≀ (S.card : ℝ) / Fintype.card Ξ± := by
297 rw [le_div_iffβ‚€ hΞ±_pos]
298 linarith [hheavy]
299 have happrox_bound : |((S ∩ Y).card : ℝ) / Y.card - (S.card : ℝ) / Fintype.card Ξ±| ≀ 1 / (4 * r) :=
300 hY_approx S hS
301 have hcardY_pos : 0 < (Y.card : ℝ) := by
302 -- if Y.card = 0, then 0/0 - S.card/|Ξ±| has |.| ≀ 1/(4r) but S.card/|Ξ±| β‰₯ 1/r > 1/(4r)
303 rcases (Y.card.eq_zero_or_pos) with hY0 | hYp
304 Β· exfalso
305 have hYempty : Y = βˆ… := Finset.card_eq_zero.mp hY0
306 rw [hYempty] at happrox_bound
307 simp at happrox_bound
308 have heq : (r⁻¹ * 4⁻¹ : ℝ) = 1 / (4 * r) := by ring
309 rw [heq] at happrox_bound
310 have habs := abs_le.mp happrox_bound
311 have h14 : (1 : ℝ) / (4 * r) < 1 / r := by
312 apply one_div_lt_one_div_of_lt hr_pos; linarith
313 linarith [habs.2]
314 Β· exact_mod_cast hYp
315 have hcardYR_pos : 0 < (Fintype.card Y : ℝ) := by
316 rw [Fintype.card_coe]; exact hcardY_pos
317 have hS'_card : (S'.card : ℝ) = ((S ∩ Y).card : ℝ) := card_subtype_eq_inter Y S
318 -- |S'|/|Y| β‰₯ 1/r - 1/(4r) β‰₯ 1/(2r)
319 have h_inner : 1 / (2 * r) ≀ (S'.card : ℝ) / (Fintype.card Y : ℝ) := by
320 rw [hS'_card, Fintype.card_coe]
321 have habs := abs_le.mp happrox_bound
322 have h1 : (S.card : ℝ) / Fintype.card Ξ± - 1/(4*r) ≀ ((S ∩ Y).card : ℝ) / Y.card := by
323 linarith
324 have h14 : (1 : ℝ) / r - 1 / (4*r) = 3 / (4*r) := by field_simp; ring
325 have h_mono : (1 : ℝ) / (2*r) ≀ 3 / (4*r) := by
326 rw [div_le_div_iffβ‚€ (by linarith : (0:ℝ) < 2*r) (by linarith : (0:ℝ) < 4*r)]
327 linarith
328 linarith
329 have hS'_heavy : 1 / (2 * r) * (Fintype.card Y : ℝ) ≀ (S'.card : ℝ) := by
330 rw [← le_div_iffβ‚€ hcardYR_pos]
331 exact h_inner
332 have hN_S' := hN_net S' hS'_mem hS'_heavy
333 obtain ⟨x, hx⟩ := hN_S'
334 rw [Finset.mem_inter] at hx
335 have hx_S : (x : α) ∈ S := by
336 have := hx.2
337 simp only [S', Finset.mem_subtype] at this
338 exact this
339 refine ⟨(x : α), ?_⟩
340 rw [Finset.mem_inter]
341 refine ⟨?_, hx_S⟩
342 exact Finset.mem_image.mpr ⟨x, hx.1, rfl⟩
343 Β· -- size bound
344 have h_image_le : ((N_Ξ².image Subtype.val).card : ℝ) ≀ (N_Ξ².card : ℝ) := by
345 exact_mod_cast Finset.card_image_le
346 have hπ’œ'_pos : (0 : ℝ) < π’œ'.card := by exact_mod_cast (by omega : 0 < π’œ'.card)
347 have hπ’œ'_bound : ((traceFamily π’œ Y).card : ℝ) ≀
348 ((d : ℝ) + 1) * ((Y.card : ℝ) + 1) ^ d := by
349 have := traceFamily_card_le π’œ d hd Y
350 convert this using 2; push_cast; ring
351 have hY_size_R : (Y.card : ℝ) ≀ C₁ * (4 * r) ^ 2 * Real.log (4 * r) := hY_size
352 have hYcard_nn : (0 : ℝ) ≀ (Y.card : ℝ) := by positivity
353 -- (Y.card+1)^d ≀ (C₁·(4r)Β²Β·log(4r)+1)^d
354 have hYp1_bound : ((Y.card : ℝ) + 1) ^ d
355 ≀ (C₁ * (4 * r) ^ 2 * Real.log (4 * r) + 1) ^ d := by
356 apply pow_le_pow_leftβ‚€ (by linarith) (by linarith)
357 have hm_bound : ((d : ℝ) + 1) * ((Y.card : ℝ) + 1) ^ d
358 ≀ ((d : ℝ) + 1) * (C₁ * (4 * r) ^ 2 * Real.log (4 * r) + 1) ^ d := by
359 apply mul_le_mul_of_nonneg_left hYp1_bound (by positivity)
360 have hm_nn : (0 : ℝ) < ((traceFamily π’œ Y).card : ℝ) := hπ’œ'_pos
361 have hN_log_le : 2 * r * Real.log ((traceFamily π’œ Y).card : ℝ) + 1 ≀ C * r * Real.log r := by
362 apply hCbound r hr
363 Β· exact hm_nn
364 Β· exact hπ’œ'_bound.trans hm_bound
365 have hN_size' : (N_Ξ².card : ℝ) ≀ 2 * r * Real.log ((traceFamily π’œ Y).card : ℝ) + 1 := by
366 have := hN_size
367 show (N_Ξ².card : ℝ) ≀ 2 * r * Real.log (π’œ'.card : ℝ) + 1
368 exact this
369 linarith
370 Β· -- π’œ'.card < 2, i.e., ≀ 1.
371 push_neg at hcard
372 have hcard' : π’œ'.card ≀ 1 := Nat.lt_succ_iff.mp hcard
373 -- We'll show |N| ≀ 1 ≀ C * r * log r.
374 have hlog2_pos : 0 < Real.log 2 := Real.log_pos (by norm_num)
375 have hlog_r_pos : 0 < Real.log r := Real.log_pos (by linarith)
376 have hlog2_lb : (1 : ℝ) / 2 ≀ Real.log 2 := by
377 have := Real.log_two_gt_d9; linarith
378 have hlogr_lb : Real.log 2 ≀ Real.log r := Real.log_le_log (by norm_num) hr
379 have hone_le : (1 : ℝ) ≀ C * r * Real.log r := by
380 have h1 : (1 : ℝ) ≀ C := hC_ge_one
381 have hlogr_lb' : (1 : ℝ) / 2 ≀ Real.log r := le_trans hlog2_lb hlogr_lb
382 have h2 : (1 : ℝ) ≀ r * Real.log r := by
383 have : (1 : ℝ) = 2 * (1/2) := by norm_num
384 rw [this]
385 exact mul_le_mul hr hlogr_lb' (by norm_num) (by linarith)
386 calc (1 : ℝ) = 1 * 1 := by ring
387 _ ≀ C * (r * Real.log r) := mul_le_mul h1 h2 (by norm_num) (by linarith)
388 _ = C * r * Real.log r := by ring
389 by_cases hπ’œ_empty : π’œ.Nonempty
390 Β· obtain ⟨Sβ‚€, hSβ‚€βŸ© := hπ’œ_empty
391 let T : Finset Y := Sβ‚€.subtype (Β· ∈ Y)
392 have hT_mem : T ∈ π’œ' := Finset.mem_image.mpr ⟨Sβ‚€, hSβ‚€, rfl⟩
393 -- All traces in π’œ' equal T (since π’œ'.card ≀ 1)
394 have hall_T : βˆ€ S ∈ π’œ, (S.subtype (Β· ∈ Y) : Finset Y) = T := by
395 intro S hS
396 have hS_mem : (S.subtype (Β· ∈ Y) : Finset Y) ∈ π’œ' :=
397 Finset.mem_image.mpr ⟨S, hS, rfl⟩
398 -- π’œ'.card ≀ 1 and both elements in, so equal
399 have := Finset.card_le_one.mp hcard'
400 exact this _ hS_mem _ hT_mem
401 by_cases hT_empty : T.Nonempty
402 · obtain ⟨x, hxT⟩ := hT_empty
403 refine ⟨{(x : α)}, ?_, ?_⟩
404 Β· intro S hS _hheavy
405 have hSeq := hall_T S hS
406 have hxS' : x ∈ (S.subtype (· ∈ Y) : Finset Y) := by rw [hSeq]; exact hxT
407 rw [Finset.mem_subtype] at hxS'
408 refine ⟨(x : α), ?_⟩
409 rw [Finset.mem_inter, Finset.mem_singleton]
410 exact ⟨rfl, hxS'⟩
411 Β· simp only [Finset.card_singleton, Nat.cast_one]
412 exact hone_le
413 Β· -- T = βˆ…: no S in π’œ is heavy
414 rw [Finset.not_nonempty_iff_eq_empty] at hT_empty
415 refine βŸ¨βˆ…, ?_, ?_⟩
416 Β· intro S hS hheavy
417 exfalso
418 have hSeq := hall_T S hS
419 rw [hT_empty] at hSeq
420 -- S ∩ Y = βˆ…
421 have hSY_empty : S ∩ Y = βˆ… := by
422 ext x
423 simp only [Finset.mem_inter, Finset.notMem_empty, iff_false, not_and]
424 intro hxS hxY
425 have : (⟨x, hxY⟩ : Y) ∈ (S.subtype (· ∈ Y) : Finset Y) := by
426 rw [Finset.mem_subtype]; exact hxS
427 rw [hSeq] at this
428 exact (Finset.notMem_empty _ this)
429 have happrox_S := hY_approx S hS
430 rw [hSY_empty] at happrox_S
431 simp at happrox_S
432 have hΞ±_pos : (0 : ℝ) < Fintype.card Ξ± := by
433 exact_mod_cast (Fintype.card_pos : 0 < Fintype.card Ξ±)
434 have hSdens : (1 : ℝ) / r ≀ S.card / Fintype.card Ξ± := by
435 rw [le_div_iffβ‚€ hΞ±_pos]; linarith [hheavy]
436 have habs := abs_le.mp happrox_S
437 have heq : (r⁻¹ * 4⁻¹ : ℝ) = 1 / (4 * r) := by ring
438 have h14 : (1 : ℝ) / (4 * r) < 1 / r := by
439 apply one_div_lt_one_div_of_lt hr_pos; linarith
440 have : (S.card : ℝ) / Fintype.card Ξ± ≀ r⁻¹ * 4⁻¹ := habs.2
441 rw [heq] at this
442 linarith
443 Β· simp only [Finset.card_empty, Nat.cast_zero]
444 positivity
445 Β· -- π’œ = βˆ…
446 rw [Finset.not_nonempty_iff_eq_empty] at hπ’œ_empty
447 refine βŸ¨βˆ…, ?_, ?_⟩
448 Β· intro S hS; rw [hπ’œ_empty] at hS; exact (Finset.notMem_empty _ hS).elim
449 Β· simp only [Finset.card_empty, Nat.cast_zero]
450 positivity
451
452end Catalog.VC.EpsilonNetTheorem
453