Formalizing Structural Graph Theory in Lean 4

Catalog/VC/EpsilonApproximationBound/Full.lean
1import Catalog.VC.VCDimension.Full
2import Catalog.VC.EpsilonApproximation.Full
3import Catalog.VC.ShatterFunctionLemma.Full
4import Catalog.Sparsity.ChernoffBound.Full
5import Mathlib.Analysis.SpecialFunctions.Log.Basic
6import Mathlib.Analysis.SpecialFunctions.Log.Monotone
7import Mathlib.Analysis.SpecialFunctions.Pow.Real
8import Mathlib.Analysis.Complex.ExponentialBounds
9import Mathlib.Algebra.Order.Field.GeomSum
10import Mathlib.Probability.ProbabilityMassFunction.Constructions
11import Mathlib.Probability.ProbabilityMassFunction.Integrals
12import Mathlib.Probability.Independence.Basic
13import Mathlib.MeasureTheory.Integral.Pi
14
15namespace Catalog.VC.EpsilonApproximationBound
16
17def IsRelativeApprox {α : Type*} [DecidableEq α]
18 (𝒜 : Finset (Finset α)) (Y Z : Finset α) (ε : ℝ) : Prop :=
19 ∀ S ∈ 𝒜, |((S ∩ Z).card : ℝ) / Z.card - ((S ∩ Y).card : ℝ) / Y.card| ≤ ε
20
21lemma approx_transitive {α : Type*} [DecidableEq α] [Fintype α]
22 (𝒜 : Finset (Finset α)) {Y Z : Finset α} {ε₁ ε₂ : ℝ}
23 (hY : Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 ε₁ Y)
24 (hZ : IsRelativeApprox 𝒜 Y Z ε₂) :
25 Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 (ε₁ + ε₂) Z := by
26 intro S hS
27 refine le_trans (abs_sub_le _ (((S ∩ Y).card : ℝ) / Y.card) _) ?_
28 simpa [add_comm, add_left_comm, add_assoc] using add_le_add (hZ S hS) (hY S hS)
29
30lemma relativeApprox_self {α : Type*} [DecidableEq α]
31 (𝒜 : Finset (Finset α)) (Y : Finset α) :
32 IsRelativeApprox 𝒜 Y Y 0 := by
33 intro S hS
34 simp
35
36lemma relativeApprox_mono {α : Type*} [DecidableEq α]
37 (𝒜 : Finset (Finset α)) {Y Z : Finset α} {ε ε' : ℝ}
38 (h : IsRelativeApprox 𝒜 Y Z ε) (hε : ε ≤ ε') :
39 IsRelativeApprox 𝒜 Y Z ε' := by
40 intro S hS
41 exact (h S hS).trans hε
42
43lemma relativeApprox_trans {α : Type*} [DecidableEq α]
44 (𝒜 : Finset (Finset α)) {W Y Z : Finset α} {ε₁ ε₂ : ℝ}
45 (h₁ : IsRelativeApprox 𝒜 W Y ε₁) (h₂ : IsRelativeApprox 𝒜 Y Z ε₂) :
46 IsRelativeApprox 𝒜 W Z (ε₁ + ε₂) := by
47 intro S hS
48 refine le_trans (abs_sub_le _ (((S ∩ Y).card : ℝ) / Y.card) _) ?_
49 linarith [h₂ S hS, h₁ S hS]
50
51private lemma trace_card_le {α : Type*} [DecidableEq α] [Fintype α]
52 (𝒜 : Finset (Finset α)) {d : ℕ} (hd : 𝒜.vcDim ≤ d) (Y : Finset α) :
53 (Catalog.VC.ShatterFunction.trace 𝒜 Y).card ≤
54 Catalog.VC.ShatterFunctionLemma.binomialSum d Y.card := by
55 calc (Catalog.VC.ShatterFunction.trace 𝒜 Y).card
56 ≤ Catalog.VC.ShatterFunction.shatterFun 𝒜 Y.card :=
57 Finset.le_sup_of_le (Finset.mem_filter.mpr ⟨Finset.mem_univ Y, rfl⟩) le_rfl
58 _ ≤ Catalog.VC.ShatterFunctionLemma.binomialSum d Y.card :=
59 Catalog.VC.ShatterFunctionLemma.shatterFunctionLemma 𝒜 hd Y.card
60
61lemma exists_half_subset {α : Type*} [DecidableEq α]
62 (Y : Finset α) (hY : 2 ≤ Y.card) :
63 ∃ Z : Finset α, Z ⊆ Y ∧ 0 < Z.card ∧ Z.card ≤ Y.card / 2 := by
64 let m := Y.card / 2
65 have hm_pos : 0 < m := by
66 dsimp [m]
67 omega
68 have hm_le : m ≤ Y.card := by
69 dsimp [m]
70 exact Nat.div_le_self _ _
71 rcases Finset.exists_subset_card_eq (s := Y) hm_le with ⟨Z, hZY, hZcard⟩
72 refine ⟨Z, hZY, ?_, ?_⟩
73 · simpa [hZcard] using hm_pos
74 · simpa [m] using hZcard.le
75
76lemma dyadic_error_decay_two_steps {m : ℕ} (hm : 2 ≤ m) :
77 Real.sqrt (Real.log ((2 : ℝ) ^ (m + 2)) / ((2 : ℝ) ^ (m + 2)))
78 ≤ (3 / 4 : ℝ) * Real.sqrt (Real.log ((2 : ℝ) ^ m) / ((2 : ℝ) ^ m)) := by
79 have hbase :
80 Real.log ((2 : ℝ) ^ (m + 2)) / ((2 : ℝ) ^ (m + 2))
81 ≤ ((3 / 4 : ℝ)^2) * (Real.log ((2 : ℝ) ^ m) / ((2 : ℝ) ^ m)) := by
82 rw [Real.log_pow, Real.log_pow, pow_add]
83 have hpow_ne : ((2 : ℝ) ^ m) ≠ 0 := by
84 positivity
85 field_simp [hpow_ne]
86 ring_nf
87 have hm36 : 16 * ((2 + m : ℕ) : ℝ) ≤ 36 * m := by
88 exact_mod_cast (show 16 * (2 + m) ≤ 36 * m by omega)
89 nlinarith [hm36, Real.log_pos (by norm_num : (1 : ℝ) < 2)]
90 have hsqrt34 : Real.sqrt ((3 / 4 : ℝ)^2) = (3 / 4 : ℝ) := by
91 rw [Real.sqrt_sq_eq_abs]
92 norm_num
93 calc
94 Real.sqrt (Real.log ((2 : ℝ) ^ (m + 2)) / ((2 : ℝ) ^ (m + 2)))
95 ≤ Real.sqrt (((3 / 4 : ℝ)^2) * (Real.log ((2 : ℝ) ^ m) / ((2 : ℝ) ^ m))) :=
96 Real.sqrt_le_sqrt hbase
97 _ = Real.sqrt ((3 / 4 : ℝ)^2) * Real.sqrt (Real.log ((2 : ℝ) ^ m) / ((2 : ℝ) ^ m)) := by
98 rw [Real.sqrt_mul (by positivity)]
99 _ = (3 / 4 : ℝ) * Real.sqrt (Real.log ((2 : ℝ) ^ m) / ((2 : ℝ) ^ m)) := by
100 rw [hsqrt34]
101
102private lemma relativeApprox_of_trace {α : Type*} [DecidableEq α]
103 (𝒜 : Finset (Finset α)) (Y Z : Finset α) (hZY : Z ⊆ Y) {ε : ℝ}
104 (htrace : ∀ T ∈ Catalog.VC.ShatterFunction.trace 𝒜 Y,
105 |((T ∩ Z).card : ℝ) / Z.card - (T.card : ℝ) / Y.card| ≤ ε) :
106 IsRelativeApprox 𝒜 Y Z ε := by
107 intro S hS
108 have hmem : S ∩ Y ∈ Catalog.VC.ShatterFunction.trace 𝒜 Y := by
109 exact Finset.mem_image.mpr ⟨S, hS, by simp⟩
110 have hsub :
111 Y ∩ (Z ∩ S) = Z ∩ S := by
112 ext x
113 constructor
114 · intro hx
115 simp only [Finset.mem_inter] at hx ⊢
116 exact ⟨hx.2.1, hx.2.2⟩
117 · intro hx
118 simp only [Finset.mem_inter] at hx ⊢
119 exact ⟨hZY hx.1, hx.1, hx.2⟩
120 simpa [Catalog.VC.ShatterFunction.trace, hsub, Finset.inter_assoc, Finset.inter_left_comm,
121 Finset.inter_comm] using htrace (S ∩ Y) hmem
122
123/-- Density deviation for any two nested subsets is at most 1. -/
124private lemma density_deviation_le_one {α : Type*} [DecidableEq α]
125 {T Y Z : Finset α} (hTY : T ⊆ Y) (hZY : Z ⊆ Y) (hZ : 0 < Z.card) :
126 |((T ∩ Z).card : ℝ) / Z.card - (T.card : ℝ) / Y.card| ≤ 1 := by
127 have hZcard : (0 : ℝ) < Z.card := Nat.cast_pos.mpr hZ
128 have hYcard : (0 : ℝ) < Y.card := by
129 exact_mod_cast lt_of_lt_of_le hZ (Finset.card_le_card hZY)
130 have h1 : ((T ∩ Z).card : ℝ) / Z.card ≤ 1 := by
131 rw [div_le_one hZcard]
132 exact_mod_cast Finset.card_le_card Finset.inter_subset_right
133 have h2 : (T.card : ℝ) / Y.card ≤ 1 := by
134 rw [div_le_one hYcard]
135 exact_mod_cast Finset.card_le_card hTY
136 have h3 : 0 ≤ ((T ∩ Z).card : ℝ) / Z.card := div_nonneg (Nat.cast_nonneg _) hZcard.le
137 have h4 : 0 ≤ (T.card : ℝ) / Y.card := div_nonneg (Nat.cast_nonneg _) hYcard.le
138 rw [abs_le]
139 exact ⟨by linarith, by linarith⟩
140
141/-- Additive-to-ratio conversion for density deviations.
142If |tz - k/2| ≤ t and |z - n/2| ≤ s and z ≥ n/4,
143then |tz/z - k/n| ≤ 4(t+s)/n. -/
144private lemma ratio_of_additive {n k z tz : ℝ}
145 (hn : 0 < n) (hz : 0 < z) (hk : k ≤ n) (hk0 : 0 ≤ k)
146 (hz_lb : n / 4 ≤ z)
147 {t s : ℝ}
148 (h_trace : |tz - k / 2| ≤ t)
149 (h_size : |z - n / 2| ≤ s) :
150 |tz / z - k / n| ≤ 4 * (t + s) / n := by
151 have hs : 0 ≤ s := le_trans (abs_nonneg _) h_size
152 have ht : 0 ≤ t := le_trans (abs_nonneg _) h_trace
153 rw [div_sub_div _ _ (ne_of_gt hz) (ne_of_gt hn)]
154 have h_denom_pos : 0 < z * n := mul_pos hz hn
155 rw [abs_div, abs_of_pos h_denom_pos, div_le_div_iff₀ h_denom_pos hn]
156 have key : |tz * n - z * k| ≤ n * (t + s) := by
157 have eq : tz * n - z * k = n * (tz - k / 2) - k * (z - n / 2) := by ring
158 rw [eq]
159 calc |n * (tz - k / 2) - k * (z - n / 2)|
160 ≤ |n * (tz - k / 2)| + |-(k * (z - n / 2))| := abs_add_le _ _
161 _ = n * |tz - k / 2| + k * |z - n / 2| := by
162 rw [abs_neg, abs_mul, abs_mul, abs_of_pos hn, abs_of_nonneg hk0]
163 _ ≤ n * t + k * s := by nlinarith
164 _ ≤ n * t + n * s := by nlinarith
165 _ = n * (t + s) := by ring
166 nlinarith [key, abs_nonneg (tz * n - z * k)]
167
168-- Product Bernoulli(1/2) probability space for the probabilistic method
169section ProbSetup
170open MeasureTheory ProbabilityTheory
171
172private noncomputable def bernHalf : PMF Bool :=
173 PMF.bernoulli (⟨1/2, by norm_num⟩ : NNReal)
174 (by show (⟨1/2, _⟩ : NNReal).val ≤ (1 : NNReal).val; simp; norm_num)
175
176private noncomputable def bernHalfMeas : Measure Bool := bernHalf.toMeasure
177private instance : IsProbabilityMeasure bernHalfMeas := by
178 unfold bernHalfMeas; infer_instance
179
180private noncomputable def prodBern (n : ℕ) : Measure (Fin n → Bool) :=
181 Measure.pi (fun (_ : Fin n) => bernHalfMeas)
182
183private instance (n : ℕ) : IsProbabilityMeasure (prodBern n) :=
184 Measure.pi.instIsProbabilityMeasure _
185
186private def ind (b : Bool) : ℝ := if b then 1 else 0
187
188private lemma exp_neg_mul_log_nat (n c : ℕ) (hn : 1 < n) :
189 Real.exp (-(↑c * Real.log (↑n : ℝ))) = ((↑n : ℝ) ^ c)⁻¹ := by
190 rw [show -(↑c * Real.log (↑n : ℝ)) = Real.log (((↑n : ℝ) ^ c)⁻¹) from by
191 rw [Real.log_inv, Real.log_pow]]
192 exact Real.exp_log (by positivity : (0:ℝ) < ((↑n : ℝ) ^ c)⁻¹)
193
194end ProbSetup
195
196
197section GoodOmega
198open MeasureTheory ProbabilityTheory Real Finset
199
200set_option maxHeartbeats 1600000 in
201private lemma good_omega_exists (d : ℕ) :
202 ∃ N : ℕ, 2 ≤ N ∧
203 ∀ (n : ℕ), N ≤ n →
204 ∀ (family : Finset (Finset (Fin n))),
205 family.card ≤ Catalog.VC.ShatterFunctionLemma.binomialSum d n →
206 ∃ ω : Fin n → Bool,
207 |(((Finset.univ.filter (fun i => ω i)).card : ℝ) - ↑n / 2)| ≤
208 Real.sqrt (3 * ↑n * Real.log ↑n) ∧
209 ∀ T ∈ family,
210 |(((T.filter (fun i => ω i)).card : ℝ) - ↑T.card / 2)| ≤
211 Real.sqrt (2 * (↑d + 1) * ↑n * Real.log ↑n) := by
212 refine ⟨max 512 (4 * (d + 2)), by omega, ?_⟩
213 intro n hn family hfamily
214 have hn512 : 512 ≤ n := by omega
215 have hn_pos : (0 : ℝ) < ↑n := by exact_mod_cast (show 0 < n by omega)
216 have hn_ne : (↑n : ℝ) ≠ 0 := ne_of_gt hn_pos
217 have hnd : 4 * (d + 2) ≤ n := by omega
218 have hn1 : (1 : ℝ) < ↑n := by exact_mod_cast (show 1 < n by omega)
219 have hn1' : 1 < n := by omega
220 -- ═══════════════════════════════════════════════════════
221 -- Probability space
222 -- ═══════════════════════════════════════════════════════
223 set μ := prodBern n
224 set X : Fin n → (Fin n → Bool) → ℝ := fun i ω => ind (ω i)
225 have hp : (1:ℝ)/2 ∈ Set.Icc 0 1 := ⟨by norm_num, by norm_num⟩
226 have hX_meas : ∀ i, Measurable (X i) := fun _ => measurable_of_finite _
227 have hX_indep : iIndepFun X μ :=
228 @iIndepFun_pi (Fin n) _ (fun _ => Bool) (fun _ => inferInstance)
229 (fun _ => bernHalfMeas) _ (fun _ => ℝ) (fun _ => inferInstance) (fun _ => ind)
230 (fun _ => (measurable_of_finite _).aemeasurable)
231 have hX_bern : ∀ i, ∀ᵐ ω ∂μ, X i ω = 0 ∨ X i ω = 1 :=
232 fun _ => Filter.Eventually.of_forall (fun ω => by simp [X, ind])
233 have hX_mean : ∀ i, ∫ ω, X i ω ∂μ = 1/2 := fun i => by
234 have h := @integral_comp_eval (Fin n) _ (fun _ => Bool) (fun _ => inferInstance)
235 (fun _ => bernHalfMeas) ℝ _ _ _ i ind
236 (Measurable.aestronglyMeasurable (measurable_of_finite _))
237 show ∫ ω, ind (ω i) ∂prodBern n = 1/2
238 unfold prodBern; rw [h, bernHalfMeas, PMF.integral_eq_sum]
239 simp [ind, bernHalf, PMF.bernoulli_apply]
240 rfl
241 -- ═══════════════════════════════════════════════════════
242 -- √(3n log n) ≤ n/4 for n ≥ 512
243 -- ═══════════════════════════════════════════════════════
244 have hlog_pos : 0 < log ↑n := log_pos hn1
245 have h_sz : sqrt (3 * ↑n * log ↑n) ≤ ↑n / 4 := by
246 rw [sqrt_le_left (by positivity)]
247 have h512R : (512 : ℝ) ≤ ↑n := by exact_mod_cast hn512
248 have hlog_bound : log ↑n ≤ 8 + ↑n / 512 := by
249 have hndiv_pos : (0 : ℝ) < ↑n / 512 := by linarith
250 linarith [log_div (ne_of_gt hn_pos) (by norm_num : (512:ℝ) ≠ 0),
251 show log (512 : ℝ) ≤ 9 from by
252 rw [show (512:ℝ) = 2^(9:ℕ) from by norm_num, log_pow]; push_cast
253 nlinarith [log_le_sub_one_of_pos (by norm_num : (0:ℝ) < 2)],
254 log_le_sub_one_of_pos hndiv_pos]
255 nlinarith [mul_le_mul_of_nonneg_left hlog_bound (show (0:ℝ) ≤ 3 * ↑n by positivity),
256 log_nonneg (le_of_lt hn1)]
257 -- ═══════════════════════════════════════════════════════
258 -- Size Chernoff: P(|Z - n/2| ≥ √(3n log n)) ≤ 2/n²
259 -- ═══════════════════════════════════════════════════════
260 -- δ = 2√(3n log n)/n ∈ (0,1)
261 have hδ_s_pos : 0 < 2 * sqrt (3 * ↑n * log ↑n) / ↑n :=
262 div_pos (mul_pos (by norm_num) (sqrt_pos.mpr (by nlinarith))) hn_pos
263 have hδ_s_lt : 2 * sqrt (3 * ↑n * log ↑n) / ↑n < 1 := by
264 rw [div_lt_one hn_pos]; linarith [h_sz]
265 -- Apply chernoffBound
266 have h_chern_s :=
267 Catalog.Sparsity.ChernoffBound.chernoffBound hp hX_meas hX_indep hX_bern hX_mean
268 (Set.mem_Ioo.mpr ⟨hδ_s_pos, hδ_s_lt⟩)
269 -- Threshold simplification: δ * (n * 1/2) = √(3n log n)
270 have h_thr_s : 2 * sqrt (3 * ↑n * log ↑n) / ↑n * (↑n * (1/2)) =
271 sqrt (3 * ↑n * log ↑n) := by field_simp
272 -- Exponent simplification: δ² * (n/2) / 3 = 2 log n
273 have h_exp_s : (2 * sqrt (3 * ↑n * log ↑n) / ↑n) ^ 2 * (↑n * (1/2)) / 3 =
274 2 * log ↑n := by
275 have hsq : sqrt (3 * ↑n * log ↑n) ^ 2 = 3 * ↑n * log ↑n := sq_sqrt (by positivity)
276 field_simp
277 nlinarith [hsq]
278 rw [h_thr_s] at h_chern_s
279 -- Combine: μ.real(bad_size) ≤ 2/n²
280 have h_size_bound : μ.real {ω | sqrt (3 * ↑n * log ↑n) ≤
281 |∑ i : Fin n, X i ω - ↑n * (1/2)|} ≤ 2 * ((↑n : ℝ) ^ 2)⁻¹ := by
282 have h2 : (2 : ℝ) = ↑(2 : ℕ) := by norm_num
283 calc μ.real _ ≤ 2 * rexp (-((2 * sqrt (3 * ↑n * log ↑n) / ↑n) ^ 2 *
284 (↑n * (1/2)) / 3)) := h_chern_s
285 _ = 2 * rexp (-(2 * log ↑n)) := by rw [h_exp_s]
286 _ = 2 * ((↑n : ℝ) ^ 2)⁻¹ := by rw [h2, exp_neg_mul_log_nat n 2 hn1']
287 -- ═══════════════════════════════════════════════════════
288 -- Trace Chernoff
289 -- ═══════════════════════════════════════════════════════
290 set t := sqrt (2 * (↑d + 1) * ↑n * log ↑n)
291 have ht_nonneg : 0 ≤ t := sqrt_nonneg _
292 have h_trace_bound : ∀ T ∈ family,
293 μ.real {ω | t < |(∑ j : Fin T.card,
294 X ((T.orderIsoOfFin rfl) j) ω) - ↑T.card * (1/2)|} ≤
295 2 * ((↑n : ℝ) ^ (d+1))⁻¹ := by
296 intro T hT
297 have hTn : T.card ≤ n := by
298 calc T.card ≤ univ.card := card_le_card (subset_univ T)
299 _ = n := by simp [Fintype.card_fin]
300 by_cases hT_big : (2 * t : ℝ) < ↑T.card
301 · -- Big trace: Chernoff via precomp
302 have hTcard_pos : (0 : ℝ) < ↑T.card := by linarith [ht_nonneg]
303 have hf_inj : Function.Injective
304 (fun j : Fin T.card => ((T.orderIsoOfFin rfl) j : Fin n)) := by
305 intro a b hab
306 exact_mod_cast (T.orderIsoOfFin rfl).injective (Subtype.val_injective hab)
307 have hXT_indep : iIndepFun (fun j (ω : Fin n → Bool) =>
308 X ((T.orderIsoOfFin rfl) j) ω) μ :=
309 hX_indep.precomp hf_inj
310 have hchern_T := Catalog.Sparsity.ChernoffBound.chernoffBound hp
311 (fun j => hX_meas _) hXT_indep (fun j => hX_bern _) (fun j => hX_mean _)
312 (Set.mem_Ioo.mpr ⟨show 0 < 2 * t / ↑T.card from div_pos (by positivity) hTcard_pos,
313 show 2 * t / ↑T.card < 1 from by rw [div_lt_one hTcard_pos]; linarith⟩)
314 -- Threshold: δ_T * (T.card/2) = t
315 have h_thr_T : 2 * t / ↑T.card * (↑T.card * (1/2)) = t := by
316 field_simp
317 -- Exponent bound: δ_T² * T.card/2/3 ≥ (d+1) * log n
318 have h_exp_T : (↑(d+1) : ℝ) * log ↑n ≤
319 (2 * t / ↑T.card) ^ 2 * (↑T.card * (1/2)) / 3 := by
320 have hsq : t ^ 2 = 2 * (↑d + 1) * ↑n * log ↑n := sq_sqrt (by positivity)
321 have hTR : (↑T.card : ℝ) ≤ ↑n := by exact_mod_cast hTn
322 have key : (2 * t / ↑T.card) ^ 2 * (↑T.card * (1/2)) / 3 =
323 2 * t ^ 2 / (3 * ↑T.card) := by field_simp
324 rw [key, hsq]
325 rw [le_div_iff₀ (by positivity : (0:ℝ) < 3 * ↑T.card)]
326 push_cast; nlinarith [hTcard_pos, hTR, hlog_pos]
327 rw [h_thr_T] at hchern_T
328 -- {t < |...|} ⊆ {t ≤ |...|}, and chernoff bounds the ≤ version
329 have h_subset : {ω : Fin n → Bool | t < |(∑ j : Fin T.card,
330 X ((T.orderIsoOfFin rfl) j) ω) - ↑T.card * (1/2)|} ⊆
331 {ω | t ≤ |(∑ j : Fin T.card,
332 X ((T.orderIsoOfFin rfl) j) ω) - ↑T.card * (1/2)|} :=
333 fun _ hω => Set.mem_setOf.mpr (le_of_lt (Set.mem_setOf.mp hω))
334 calc μ.real {ω | t < |(∑ j : Fin T.card, X ((T.orderIsoOfFin rfl) j) ω) -
335 ↑T.card * (1/2)|}
336 ≤ μ.real {ω | t ≤ |(∑ j : Fin T.card, X ((T.orderIsoOfFin rfl) j) ω) -
337 ↑T.card * (1/2)|} :=
338 measureReal_mono h_subset (measure_ne_top μ _)
339 _ ≤ 2 * rexp (-((2 * t / ↑T.card) ^ 2 * (↑T.card * (1/2)) / 3)) := hchern_T
340 _ ≤ 2 * rexp (-(↑(d+1) * log ↑n)) := by
341 apply mul_le_mul_of_nonneg_left _ (by norm_num : (0:ℝ) ≤ 2)
342 apply exp_le_exp.mpr; linarith [h_exp_T]
343 _ = 2 * ((↑n : ℝ) ^ (d+1))⁻¹ := by
344 congr 1; exact exp_neg_mul_log_nat n (d+1) hn1'
345 · -- Small trace: deterministic bound
346 push_neg at hT_big
347 have h_det : ∀ ω : Fin n → Bool, |(∑ j : Fin T.card,
348 X ((T.orderIsoOfFin rfl) j) ω) - ↑T.card * (1/2)| ≤ t := by
349 intro ω
350 have h_lo : 0 ≤ ∑ j : Fin T.card, X ((T.orderIsoOfFin rfl) j) ω :=
351 sum_nonneg (fun j _ => by simp [X, ind]; split <;> norm_num)
352 have h_hi : ∑ j : Fin T.card, X ((T.orderIsoOfFin rfl) j) ω ≤ ↑T.card :=
353 calc _ ≤ ∑ _j : Fin T.card, (1 : ℝ) :=
354 sum_le_sum (fun j _ => by simp [X, ind]; split <;> norm_num)
355 _ = ↑T.card := by simp
356 rw [abs_le]; constructor <;> nlinarith [hT_big]
357 have h_empty : {ω : Fin n → Bool | t < |(∑ j : Fin T.card,
358 X ((T.orderIsoOfFin rfl) j) ω) - ↑T.card * (1/2)|} = ∅ := by
359 ext ω; simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]
360 exact not_lt.mpr (h_det ω)
361 rw [h_empty]; simp [Measure.real]
362 -- ═══════════════════════════════════════════════════════
363 -- Union bound: total bad prob < 1
364 -- ═══════════════════════════════════════════════════════
365 set bad_size := {ω : Fin n → Bool | sqrt (3 * ↑n * log ↑n) ≤
366 |∑ i : Fin n, X i ω - ↑n * (1/2)|}
367 set bad_trace : Finset (Fin n) → Set (Fin n → Bool) := fun T =>
368 {ω | t < |(∑ j : Fin T.card, X ((T.orderIsoOfFin rfl) j) ω) -
369 ↑T.card * (1/2)|}
370 set bad := bad_size ∪ ⋃ T ∈ family, bad_trace T
371 have hbad_meas : MeasurableSet bad := Set.Finite.measurableSet (Set.toFinite _)
372 -- Convert μ.real bounds to ENNReal
373 have h_mu_size : μ bad_size ≤ ENNReal.ofReal (2 * ((↑n : ℝ) ^ 2)⁻¹) :=
374 (ENNReal.ofReal_toReal (measure_ne_top μ _)).symm ▸
375 ENNReal.ofReal_le_ofReal h_size_bound
376 have h_mu_trace : ∀ T ∈ family,
377 μ (bad_trace T) ≤ ENNReal.ofReal (2 * ((↑n : ℝ) ^ (d+1))⁻¹) := by
378 intro T hT
379 exact (ENNReal.ofReal_toReal (measure_ne_top μ _)).symm ▸
380 ENNReal.ofReal_le_ofReal (h_trace_bound T hT)
381 -- μ(bad) < 1
382 have h_mu_bad : μ bad < 1 := by
383 calc μ bad ≤ μ bad_size + μ (⋃ T ∈ family, bad_trace T) := measure_union_le _ _
384 _ ≤ μ bad_size + ∑ T ∈ family, μ (bad_trace T) := by
385 gcongr; exact measure_biUnion_finset_le _ _
386 _ ≤ ENNReal.ofReal (2 * ((↑n : ℝ) ^ 2)⁻¹) +
387 ∑ T ∈ family, ENNReal.ofReal (2 * ((↑n : ℝ) ^ (d+1))⁻¹) :=
388 add_le_add h_mu_size (sum_le_sum (fun T hT => h_mu_trace T hT))
389 _ = ENNReal.ofReal (2 * ((↑n : ℝ) ^ 2)⁻¹) +
390 ↑family.card * ENNReal.ofReal (2 * ((↑n : ℝ) ^ (d+1))⁻¹) := by
391 simp [sum_const, nsmul_eq_mul]
392 _ < 1 := by
393 -- Convert ↑family.card to ENNReal.ofReal
394 have hcast : (↑family.card : ENNReal) = ENNReal.ofReal ↑family.card := by
395 simp [ENNReal.ofReal_natCast]
396 rw [hcast]
397 rw [← ENNReal.ofReal_mul (by positivity)]
398 rw [← ENNReal.ofReal_add (by positivity) (by positivity)]
399 rw [show (1 : ENNReal) = ENNReal.ofReal 1 from ENNReal.ofReal_one.symm]
400 exact (ENNReal.ofReal_lt_ofReal_iff (by norm_num)).mpr (by
401 -- ℝ bound: 2/n² + family.card * 2/n^{d+1} < 1
402 have hn1R : (1 : ℝ) ≤ ↑n := by exact_mod_cast (show 1 ≤ n by omega)
403 have hbinom : family.card ≤ (d + 1) * n ^ d := by
404 calc family.card ≤ Catalog.VC.ShatterFunctionLemma.binomialSum d n := hfamily
405 _ ≤ (d + 1) * n ^ d := by
406 unfold Catalog.VC.ShatterFunctionLemma.binomialSum
407 exact le_trans
408 (Finset.sum_le_sum (fun k _ => Nat.choose_le_pow n k))
409 (le_trans
410 (Finset.sum_le_sum (fun k hk =>
411 Nat.pow_le_pow_right (by omega)
412 (Nat.le_of_lt_succ (Finset.mem_range.mp hk))))
413 (by simp [Finset.card_range]))
414 have hfc : (↑family.card : ℝ) ≤ (↑d + 1) * (↑n : ℝ) ^ d := by
415 exact_mod_cast hbinom
416 have h_t1 : ↑family.card * (2 * ((↑n : ℝ) ^ (d+1))⁻¹) ≤
417 2 * (↑d + 1) / ↑n := by
418 rw [show (↑n : ℝ) ^ (d+1) = (↑n : ℝ) ^ d * ↑n from by ring]
419 calc ↑family.card * (2 * ((↑n : ℝ) ^ d * ↑n)⁻¹)
420 ≤ ((↑d + 1) * (↑n : ℝ) ^ d) * (2 * ((↑n : ℝ) ^ d * ↑n)⁻¹) := by
421 gcongr
422 _ = (↑d + 1) * (2 / ↑n) := by rw [mul_inv]; field_simp
423 _ = 2 * (↑d + 1) / ↑n := by ring
424 have h_t2 : 2 * ((↑n : ℝ) ^ 2)⁻¹ ≤ 2 / ↑n := by
425 rw [show (↑n : ℝ) ^ 2 = ↑n * ↑n from by ring, mul_inv]
426 calc 2 * ((↑n : ℝ)⁻¹ * (↑n : ℝ)⁻¹)
427 ≤ 2 * ((↑n : ℝ)⁻¹ * 1) := by
428 gcongr; exact inv_le_one_of_one_le₀ hn1R
429 _ = 2 / ↑n := by ring
430 calc 2 * ((↑n : ℝ) ^ 2)⁻¹ + ↑family.card * (2 * ((↑n : ℝ) ^ (d+1))⁻¹)
431 ≤ 2 / ↑n + 2 * (↑d + 1) / ↑n := add_le_add h_t2 h_t1
432 _ = 2 * (↑d + 2) / ↑n := by ring
433 _ ≤ 2 * (↑d + 2) / (4 * (↑d + 2)) := by
434 gcongr; exact_mod_cast hnd
435 _ = 1 / 2 := by field_simp; norm_num
436 _ < 1 := by norm_num)
437 -- ═══════════════════════════════════════════════════════
438 -- Witness extraction
439 -- ═══════════════════════════════════════════════════════
440 have h_good : badᶜ.Nonempty := by
441 apply nonempty_of_measure_ne_zero
442 rw [measure_compl hbad_meas (measure_ne_top μ bad)]
443 simp [measure_univ]
444 exact ne_of_gt (tsub_pos_of_lt h_mu_bad)
445 obtain ⟨ω, hω⟩ := h_good
446 refine ⟨ω, ?_, ?_⟩
447 · -- Size bound
448 have hω_size : ω ∉ bad_size := fun h => hω (Set.mem_union_left _ h)
449 simp only [bad_size, Set.mem_setOf_eq, not_le] at hω_size
450 have hsum : ∑ i : Fin n, X i ω = ((univ.filter (fun i => ω i)).card : ℝ) := by
451 simp [X, ind, ← sum_boole]
452 rw [show (↑n : ℝ) / 2 = ↑n * (1/2) from by ring]
453 linarith [hsum ▸ hω_size]
454 · -- Trace bounds
455 intro T hT
456 have hω_trace : ω ∉ bad_trace T := by
457 intro h; exact hω (Set.mem_union_right _ (Set.mem_biUnion hT h))
458 simp only [bad_trace, Set.mem_setOf_eq, not_lt] at hω_trace
459 have hsum_T : ∑ j : Fin T.card, X ((T.orderIsoOfFin rfl) j) ω =
460 ((T.filter (fun i => ω i)).card : ℝ) := by
461 have h1 : ∑ j : Fin T.card, X ((T.orderIsoOfFin rfl) j) ω =
462 ∑ i ∈ T, X i ω := by
463 rw [← T.sum_coe_sort (fun i => X i ω)]
464 exact Fintype.sum_equiv (T.orderIsoOfFin rfl).toEquiv _ _ (fun j => rfl)
465 rw [h1]; simp [X, ind, ← sum_boole]
466 rw [show (↑T.card : ℝ) / 2 = ↑T.card * (1/2) from by ring]
467 linarith [hsum_T ▸ hω_trace]
468
469
470end GoodOmega
471
472/-- The probabilistic core for large sets: there exist a uniform constant `c > 0`
473and threshold `N` (depending only on `d`) such that for any `n ≥ N`, given a
474family of subsets of `Fin n` with polynomially bounded size, a half-sized subset
475with good simultaneous density control exists.
476
477The proof uses `good_omega_exists` for the probabilistic argument,
478then converts additive bounds to ratio bounds via `ratio_of_additive`,
479and handles the complement trick when |Z| > n/2. -/
480private lemma exists_good_half_subset_large (d : ℕ) :
481 ∃ (c : ℝ) (N : ℕ), 0 < c ∧ 2 ≤ N ∧
482 ∀ (n : ℕ), N ≤ n →
483 ∀ (family : Finset (Finset (Fin n))),
484 family.card ≤ Catalog.VC.ShatterFunctionLemma.binomialSum d n →
485 ∃ Z : Finset (Fin n), 0 < Z.card ∧ Z.card ≤ n / 2 ∧
486 ∀ T ∈ family,
487 |((T ∩ Z).card : ℝ) / Z.card - (T.card : ℝ) / n| ≤
488 c * Real.sqrt (Real.log (↑n) / ↑n) := by
489 obtain ⟨N₀, hN₀, hgood⟩ := good_omega_exists d
490 -- The density constant: 4(√(2(d+1)) + √3) accounts for the ratio conversion
491 refine ⟨4 * (Real.sqrt (2 * (↑d + 1)) + Real.sqrt 3), max N₀ 512, by positivity,
492 by omega, ?_⟩
493 intro n hn family hfamily
494 have hn0 : N₀ ≤ n := by omega
495 have hn512 : 512 ≤ n := by omega
496 have hn_pos : (0 : ℝ) < n := by positivity
497 obtain ⟨ω, h_size, h_trace⟩ := hgood n hn0 family hfamily
498 -- Z₀ = {i | ω i = true}
499 set Z₀ := Finset.univ.filter (fun i : Fin n => ω i) with hZ₀_def
500 have hZ₀_card_le : Z₀.card ≤ n := by
501 calc Z₀.card ≤ Finset.univ.card := Finset.card_filter_le _ _
502 _ = n := by simp [Fintype.card_fin]
503 -- T ∩ Z₀ = T.filter (ω ·) for any T
504 have hTZ₀ : ∀ T : Finset (Fin n), T ∩ Z₀ = T.filter (fun i => ω i) := by
505 intro T; ext x; simp [Z₀, Finset.mem_inter, Finset.mem_filter]
506 -- Size lower bound: ||Z₀| - n/2| ≤ √(3n log n) and n ≥ 512 imply n/4 ≤ |Z₀| ≤ 3n/4
507 have h_sz : Real.sqrt (3 * ↑n * Real.log ↑n) ≤ ↑n / 4 := by
508 rw [Real.sqrt_le_left (by positivity : (0:ℝ) ≤ (↑n : ℝ) / 4)]
509 have h512R : (512 : ℝ) ≤ (↑n : ℝ) := by exact_mod_cast hn512
510 have hlog_bound : Real.log (↑n : ℝ) ≤ 8 + (↑n : ℝ) / 512 := by
511 have hndiv_pos : (0 : ℝ) < (↑n : ℝ) / 512 := by linarith
512 have hlog_split : Real.log (↑n : ℝ) = Real.log 512 + Real.log ((↑n : ℝ) / 512) := by
513 linarith [Real.log_div (ne_of_gt hn_pos) (by norm_num : (512:ℝ) ≠ 0)]
514 rw [hlog_split]
515 have h1 : Real.log (512 : ℝ) ≤ 9 := by
516 rw [show (512:ℝ) = 2^(9:ℕ) from by norm_num, Real.log_pow]
517 have hlog2 : Real.log 2 ≤ 2 - 1 := Real.log_le_sub_one_of_pos (by norm_num)
518 push_cast; nlinarith
519 linarith [Real.log_le_sub_one_of_pos hndiv_pos]
520 nlinarith [mul_le_mul_of_nonneg_left hlog_bound (show (0:ℝ) ≤ 3 * ↑n by positivity),
521 Real.log_nonneg (show (1:ℝ) ≤ ↑n by linarith)]
522 have hZ₀_lb : n / 4 ≤ Z₀.card := by
523 have h := (abs_le.mp (le_trans h_size h_sz)).1
524 have hR : (↑(n / 4) : ℝ) ≤ ↑Z₀.card := by
525 have : (↑(n / 4) : ℝ) * 4 ≤ ↑n := by exact_mod_cast Nat.div_mul_le_self n 4
526 linarith
527 exact_mod_cast hR
528 have hZ₀_ub : Z₀.card ≤ 3 * n / 4 := by
529 have h := (abs_le.mp (le_trans h_size h_sz)).2
530 have h4 : 4 * (↑Z₀.card : ℝ) ≤ 3 * ↑n := by linarith
531 have h4N : 4 * Z₀.card ≤ 3 * n := by exact_mod_cast h4
532 omega
533 -- Complement Z₁ has the same properties (sign flip in deviations)
534 set Z₁ := Finset.univ.filter (fun i : Fin n => ¬ω i) with hZ₁_def
535 have hZ₀Z₁ : Z₀.card + Z₁.card = n := by
536 have hZ₀Z₁_eq : Z₀ ∪ Z₁ = Finset.univ := by
537 ext x; simp [Z₀, Z₁, Finset.mem_union, Finset.mem_filter, em]
538 have hZ₀Z₁_disj : Disjoint Z₀ Z₁ := by
539 simp [Finset.disjoint_filter, Z₀, Z₁]
540 rw [← Finset.card_union_of_disjoint hZ₀Z₁_disj, hZ₀Z₁_eq]
541 simp [Fintype.card_fin]
542 have hZ₁_lb : n / 4 ≤ Z₁.card := by omega
543 have hTZ₁ : ∀ T : Finset (Fin n), T ∩ Z₁ = T.filter (fun i => ¬ω i) := by
544 intro T; ext x; simp [Z₁, Finset.mem_inter, Finset.mem_filter]
545 -- Partition lemma: T.filter(ω) + T.filter(¬ω) = T.card
546 have hTpart : ∀ T : Finset (Fin n),
547 (T.filter (fun i => ω i)).card + (T.filter (fun i => ¬ω i)).card = T.card := by
548 intro T
549 have h := @Finset.card_filter_add_card_filter_not (Fin n) T (fun i => ω i = true) _ _
550 convert h using 1
551 -- Helper: ratio_of_additive application for either choice of Z
552 -- Both Z₀ and Z₁ have the same additive deviations (sign flip for complement)
553 have hsn : Real.sqrt ↑n ≠ 0 := Real.sqrt_ne_zero'.mpr hn_pos
554 -- Algebraic simplification lemma
555 have halg : 4 * (Real.sqrt (2 * (↑d + 1) * ↑n * Real.log ↑n) +
556 Real.sqrt (3 * ↑n * Real.log ↑n)) / ↑n =
557 4 * (Real.sqrt (2 * (↑d + 1)) + Real.sqrt 3) * Real.sqrt (Real.log ↑n / ↑n) := by
558 have hn' : (↑n : ℝ) ≠ 0 := ne_of_gt hn_pos
559 have h1 : Real.sqrt (2 * (↑d + 1) * ↑n * Real.log ↑n) =
560 Real.sqrt (2 * (↑d + 1)) * (Real.sqrt ↑n * Real.sqrt (Real.log ↑n)) := by
561 rw [show 2 * (↑d + 1) * ↑n * Real.log ↑n =
562 (2 * (↑d + 1)) * (↑n * Real.log ↑n) from by ring,
563 Real.sqrt_mul (by positivity), Real.sqrt_mul (by positivity : (0:ℝ) ≤ ↑n)]
564 have h3 : Real.sqrt (3 * ↑n * Real.log ↑n) =
565 Real.sqrt 3 * (Real.sqrt ↑n * Real.sqrt (Real.log ↑n)) := by
566 rw [show 3 * ↑n * Real.log ↑n = 3 * (↑n * Real.log ↑n) from by ring,
567 Real.sqrt_mul (by norm_num : (0:ℝ) ≤ 3), Real.sqrt_mul (by positivity : (0:ℝ) ≤ ↑n)]
568 have hlog : Real.sqrt (Real.log ↑n / ↑n) = Real.sqrt (Real.log ↑n) / Real.sqrt ↑n :=
569 Real.sqrt_div' _ (by positivity : (0:ℝ) ≤ ↑n)
570 rw [h1, h3, hlog]; field_simp; rw [Real.sq_sqrt (by positivity : (0:ℝ) ≤ ↑n)]; ring
571 -- ℝ lower bounds (from additive control, not from ℕ division)
572 have hZ₀_lb_R : (↑n : ℝ) / 4 ≤ ↑Z₀.card :=
573 le_of_neg_le_neg (by linarith [(abs_le.mp (le_trans h_size h_sz)).1])
574 have hZ₁_lb_R : (↑n : ℝ) / 4 ≤ ↑Z₁.card := by
575 have : (↑Z₁.card : ℝ) = ↑n - ↑Z₀.card := by push_cast [← hZ₀Z₁]; ring
576 linarith [(abs_le.mp (le_trans h_size h_sz)).2]
577 have hTcard : ∀ T : Finset (Fin n), T.card ≤ n := by
578 intro T
579 calc T.card ≤ Finset.univ.card := Finset.card_le_card (Finset.subset_univ T)
580 _ = n := by simp [Fintype.card_fin]
581 -- Choose Z₀ if Z₀.card ≤ n/2, else Z₁
582 by_cases hZ₀_half : Z₀.card ≤ n / 2
583 · -- Use Z₀
584 refine ⟨Z₀, by omega, hZ₀_half, ?_⟩
585 intro T hT
586 have h_trace_T := h_trace T hT
587 rw [← hTZ₀] at h_trace_T
588 have := ratio_of_additive hn_pos (by linarith [hZ₀_lb_R] : (0:ℝ) < ↑Z₀.card)
589 (by exact_mod_cast hTcard T) (by positivity : (0:ℝ) ≤ ↑T.card)
590 hZ₀_lb_R h_trace_T h_size
591 linarith [halg]
592 · -- Use Z₁ (complement)
593 push_neg at hZ₀_half
594 have hZ₁_le : Z₁.card ≤ n / 2 := by omega
595 refine ⟨Z₁, by omega, hZ₁_le, ?_⟩
596 intro T hT
597 -- Complement size deviation: |Z₁ - n/2| = |Z₀ - n/2| (sign flip)
598 have h_size_Z₁ : |(↑Z₁.card : ℝ) - ↑n / 2| ≤ Real.sqrt (3 * ↑n * Real.log ↑n) := by
599 have hZ₁R : (↑Z₁.card : ℝ) = ↑n - ↑Z₀.card := by push_cast [← hZ₀Z₁]; ring
600 rw [hZ₁R]; rw [show (↑n : ℝ) - ↑Z₀.card - ↑n / 2 = -(↑Z₀.card - ↑n / 2) from by ring]
601 rw [abs_neg]; exact h_size
602 -- Complement trace deviation: |T∩Z₁ - T/2| = |T∩Z₀ - T/2| (sign flip)
603 have h_trace_T : |((T ∩ Z₁).card : ℝ) - ↑T.card / 2| ≤
604 Real.sqrt (2 * (↑d + 1) * ↑n * Real.log ↑n) := by
605 have hpart := hTpart T
606 rw [← hTZ₀, ← hTZ₁] at hpart
607 have hpart_R : ((T ∩ Z₁).card : ℝ) = ↑T.card - ↑(T ∩ Z₀).card := by
608 push_cast [← hpart]; ring
609 rw [hpart_R]
610 rw [show (↑T.card : ℝ) - ↑(T ∩ Z₀).card - ↑T.card / 2 =
611 -(↑(T ∩ Z₀).card - ↑T.card / 2) from by ring]
612 rw [abs_neg]
613 have := h_trace T hT; rwa [← hTZ₀] at this
614 have := ratio_of_additive hn_pos (by linarith [hZ₁_lb_R] : (0:ℝ) < ↑Z₁.card)
615 (by exact_mod_cast hTcard T) (by positivity : (0:ℝ) ≤ ↑T.card)
616 hZ₁_lb_R h_trace_T h_size_Z₁
617 linarith [halg]
618
619/-- For traces of a family on Y, the density deviation is at most 1 when Z ⊆ Y. -/
620private lemma trace_deviation_le_one {α : Type*} [DecidableEq α]
621 {𝒜 : Finset (Finset α)} {Y Z : Finset α} (hZY : Z ⊆ Y) (hZ : 0 < Z.card)
622 {T : Finset α} (hT : T ∈ Catalog.VC.ShatterFunction.trace 𝒜 Y) :
623 |((T ∩ Z).card : ℝ) / Z.card - (T.card : ℝ) / Y.card| ≤ 1 := by
624 have hTY : T ⊆ Y := by
625 simp only [Catalog.VC.ShatterFunction.trace, Finset.mem_image] at hT
626 obtain ⟨S, _, rfl⟩ := hT
627 exact Finset.inter_subset_right
628 exact density_deviation_le_one hTY hZY hZ
629
630/-- Trace-level version of the random halving step.
631The constant `c` is chosen uniformly for all set sizes by combining:
632- For large Y (|Y| ≥ N(d)): the probabilistic argument from
633 `exists_good_half_subset_large`.
634- For small Y (2 ≤ |Y| < N): the trivial bound |deviation| ≤ 1, absorbed into
635 the constant since √(log|Y|/|Y|) is bounded below for |Y| in this range.
636
637The wrapper `random_halving_step` then lifts this to the original family
638by `relativeApprox_of_trace`. -/
639private lemma random_halving_trace_step (d : ℕ) :
640 ∃ c : ℝ, 0 < c ∧
641 ∀ {α : Type*} [DecidableEq α] [Fintype α]
642 (𝒜 : Finset (Finset α)) (hd : 𝒜.vcDim ≤ d) (Y : Finset α),
643 2 ≤ Y.card →
644 ∃ Z : Finset α, Z ⊆ Y ∧ 0 < Z.card ∧ Z.card ≤ Y.card / 2 ∧
645 ∀ T ∈ Catalog.VC.ShatterFunction.trace 𝒜 Y,
646 |((T ∩ Z).card : ℝ) / Z.card - (T.card : ℝ) / Y.card| ≤
647 c * Real.sqrt (Real.log (Y.card : ℝ) / Y.card) := by
648 -- Get probabilistic constant and threshold for large sets
649 obtain ⟨c_prob, N, hc_prob, hN, h_large⟩ := exists_good_half_subset_large d
650 -- For small Y (2 ≤ |Y| < N): |deviation| ≤ 1 ≤ c_small · √(log|Y|/|Y|)
651 -- when c_small = √(N / log 2), since N·log|Y| ≥ |Y|·log 2 for |Y| < N.
652 have hlog2_pos : (0 : ℝ) < Real.log 2 := Real.log_pos (by norm_num)
653 set c_small : ℝ := Real.sqrt (↑N / Real.log 2) with hc_small_def
654 have hc_small_pos : 0 < c_small := by
655 rw [hc_small_def]
656 exact Real.sqrt_pos.mpr (div_pos (Nat.cast_pos.mpr (by omega)) hlog2_pos)
657 -- Choose c = max(c_prob, c_small)
658 refine ⟨max c_prob c_small, lt_max_of_lt_left hc_prob, ?_⟩
659 intro α _ _ 𝒜 hd Y hY
660 by_cases hYN : N ≤ Y.card
661 · -- Large Y: transfer to Fin Y.card via embedding f : Fin Y.card ↪ α with image Y.
662 set n := Y.card with hn_def
663 have hn_pos : 0 < n := by omega
664 -- Embedding Fin n ↪ α with range = Y, via Y.equivFin.symm composed with subtype.
665 let e : Fin n ≃ ↥Y := Y.equivFin.symm
666 let f : Fin n ↪ α :=
667 e.toEmbedding.trans (Function.Embedding.subtype (· ∈ Y))
668 have hf_range : ∀ i, f i ∈ Y := fun i => (e i).2
669 have hf_inj : Function.Injective f := f.injective
670 -- For any T ⊆ Y, T = (preimage f) mapped back, so cardinality is preserved.
671 have h_round : ∀ T : Finset α, T ⊆ Y →
672 (T.preimage f hf_inj.injOn).map f = T := by
673 intro T hTY
674 ext x
675 simp only [Finset.mem_map, Finset.mem_preimage]
676 refine ⟨?_, fun hx => ?_⟩
677 · rintro ⟨i, hi, rfl⟩; exact hi
678 · refine ⟨e.symm ⟨x, hTY hx⟩, ?_, ?_⟩
679 · show f (e.symm ⟨x, hTY hx⟩) ∈ T
680 have : f (e.symm ⟨x, hTY hx⟩) = x := by
681 simp [f, e, Function.Embedding.trans_apply, Equiv.toEmbedding_apply]
682 rw [this]; exact hx
683 · simp [f, e, Function.Embedding.trans_apply, Equiv.toEmbedding_apply]
684 have h_card_pre : ∀ T : Finset α, T ⊆ Y →
685 (T.preimage f (hf_inj.injOn)).card = T.card := by
686 intro T hTY
687 have h := congrArg Finset.card (h_round T hTY)
688 rwa [Finset.card_map] at h
689 -- Transfer the trace family.
690 let toFin : Finset α → Finset (Fin n) :=
691 fun T => T.preimage f (hf_inj.injOn)
692 let family' : Finset (Finset (Fin n)) :=
693 (Catalog.VC.ShatterFunction.trace 𝒜 Y).image toFin
694 have hfam_card : family'.card ≤ Catalog.VC.ShatterFunctionLemma.binomialSum d n := by
695 calc family'.card
696 ≤ (Catalog.VC.ShatterFunction.trace 𝒜 Y).card := Finset.card_image_le
697 _ ≤ _ := trace_card_le 𝒜 hd Y
698 obtain ⟨Z'_fin, hZ'_pos, hZ'_half, hZ'_prop⟩ :=
699 h_large n hYN family' hfam_card
700 -- Pull back Z'_fin to Z ⊆ Y.
701 let Z : Finset α := Z'_fin.map f
702 have hZ_sub_Y : Z ⊆ Y := by
703 intro x hx
704 simp only [Z, Finset.mem_map] at hx
705 obtain ⟨i, _, rfl⟩ := hx
706 exact hf_range i
707 have hZ_card : Z.card = Z'_fin.card := by simp [Z]
708 refine ⟨Z, hZ_sub_Y, hZ_card.symm ▸ hZ'_pos, hZ_card.symm ▸ hZ'_half, ?_⟩
709 intro T hT
710 have hTY : T ⊆ Y := by
711 simp only [Catalog.VC.ShatterFunction.trace, Finset.mem_image] at hT
712 obtain ⟨S, _, rfl⟩ := hT
713 exact Finset.inter_subset_right
714 have hTfam : toFin T ∈ family' := Finset.mem_image.mpr ⟨T, hT, rfl⟩
715 have hT_card : (toFin T).card = T.card := h_card_pre T hTY
716 -- T ∩ Z = (toFin T ∩ Z'_fin).map f
717 have h_int : T ∩ Z = (toFin T ∩ Z'_fin).map f := by
718 ext x
719 simp only [Finset.mem_inter, Finset.mem_map, toFin, Finset.mem_preimage, Z]
720 constructor
721 · rintro ⟨hxT, ⟨i, hi, rfl⟩⟩
722 exact ⟨i, ⟨hxT, hi⟩, rfl⟩
723 · rintro ⟨i, ⟨hi1, hi2⟩, rfl⟩
724 exact ⟨hi1, ⟨i, hi2, rfl⟩⟩
725 have h_int_card : (T ∩ Z).card = ((toFin T) ∩ Z'_fin).card := by
726 rw [h_int, Finset.card_map]
727 have hprop := hZ'_prop _ hTfam
728 rw [hT_card, ← hZ_card, ← h_int_card] at hprop
729 calc |((T ∩ Z).card : ℝ) / Z.card - (T.card : ℝ) / ↑n|
730 ≤ c_prob * Real.sqrt (Real.log ↑n / ↑n) := hprop
731 _ ≤ max c_prob c_small * Real.sqrt (Real.log ↑n / ↑n) := by
732 gcongr; exact le_max_left _ _
733 · -- Small Y (2 ≤ Y.card < N): use trivial bound
734 push_neg at hYN
735 obtain ⟨Z, hZY, hZpos, hZhalf⟩ := exists_half_subset Y hY
736 refine ⟨Z, hZY, hZpos, hZhalf, ?_⟩
737 intro T hT
738 have hdev := trace_deviation_le_one hZY hZpos hT
739 -- Show: 1 ≤ max(c_prob, c_small) · √(log|Y|/|Y|)
740 -- Since max ≥ c_small and c_small · √(log|Y|/|Y|) ≥ 1
741 have hYcard_pos : (0 : ℝ) < Y.card := Nat.cast_pos.mpr (by omega)
742 have hlogY : Real.log 2 ≤ Real.log (↑Y.card) :=
743 Real.log_le_log (by positivity) (by exact_mod_cast hY)
744 have hN_ge_Y : (Y.card : ℝ) < ↑N := by exact_mod_cast hYN
745 -- Key: c_small² · (log|Y|/|Y|) = (N/log 2) · (log|Y|/|Y|) ≥ N/|Y| > 1
746 have h_prod_ge : c_small * Real.sqrt (Real.log (↑Y.card) / ↑Y.card) ≥ 1 := by
747 rw [hc_small_def, ← Real.sqrt_mul (by positivity : (0 : ℝ) ≤ ↑N / Real.log 2)]
748 rw [show (1 : ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm]
749 apply Real.sqrt_le_sqrt
750 have : ↑N / Real.log 2 * (Real.log (↑Y.card) / ↑Y.card) =
751 ↑N * Real.log (↑Y.card) / (Real.log 2 * ↑Y.card) := by ring
752 rw [this]
753 rw [le_div_iff₀ (mul_pos hlog2_pos hYcard_pos)]
754 nlinarith [hlogY, hN_ge_Y.le, hYcard_pos, hlog2_pos]
755 calc |((T ∩ Z).card : ℝ) / Z.card - (T.card : ℝ) / Y.card|
756 ≤ 1 := hdev
757 _ ≤ c_small * Real.sqrt (Real.log (↑Y.card) / ↑Y.card) := h_prod_ge
758 _ ≤ max c_prob c_small * Real.sqrt (Real.log (↑Y.card) / ↑Y.card) := by
759 gcongr
760 exact le_max_right _ _
761
762/-- Planned one-step helper for the repeated-halving proof.
763It expresses the source's passage from a current ground set `Y` to a smaller
764subset `Z` that approximates densities on `Y`. -/
765lemma random_halving_step (d : ℕ) :
766 ∃ c : ℝ, 0 < c ∧
767 ∀ {α : Type*} [DecidableEq α] [Fintype α]
768 (𝒜 : Finset (Finset α)) (hd : 𝒜.vcDim ≤ d) (Y : Finset α),
769 2 ≤ Y.card →
770 ∃ Z : Finset α, Z ⊆ Y ∧ 0 < Z.card ∧ Z.card ≤ Y.card / 2 ∧
771 IsRelativeApprox 𝒜 Y Z
772 (c * Real.sqrt (Real.log (Y.card : ℝ) / Y.card)) := by
773 rcases random_halving_trace_step d with ⟨c, hc, hstep⟩
774 refine ⟨c, hc, ?_⟩
775 intro α _ _ 𝒜 hd Y hY
776 rcases hstep 𝒜 hd Y hY with ⟨Z, hZY, hZpos, hZhalf, htrace⟩
777 refine ⟨Z, hZY, hZpos, hZhalf, relativeApprox_of_trace 𝒜 Y Z hZY htrace⟩
778
779/-- Planned summation helper for the repeated-halving iteration.
780It packages the geometric tail estimate used at the end of Matousek Lemma 5.13. -/
781lemma geometric_error_sum :
782 ∃ Cgeom : ℝ, 0 < Cgeom ∧
783 ∀ n : ℕ, 2 ≤ n →
784 Finset.sum (Finset.range n) (fun i =>
785 Real.sqrt (Real.log ((2 : ℝ) ^ (n - i)) / ((2 : ℝ) ^ (n - i)))) ≤
786 Cgeom * Real.sqrt (Real.log (2 : ℝ) / 2) := by
787 refine ⟨10, by positivity, ?_⟩
788 intro n hn
789 let b : ℕ → ℝ := fun m =>
790 Real.sqrt (Real.log ((2 : ℝ) ^ m) / ((2 : ℝ) ^ m))
791 let a : ℕ → ℝ := fun k => b (k + 1)
792 have hb0 : b 0 = 0 := by
793 dsimp [b]
794 simp
795 have ha0 : a 0 = Real.sqrt (Real.log (2 : ℝ) / 2) := by
796 dsimp [a, b]
797 simp
798 have ha1 : a 1 = Real.sqrt (Real.log (2 : ℝ) / 2) := by
799 dsimp [a, b]
800 rw [Real.log_pow]
801 congr 1
802 ring
803 have ha2 : a 2 ≤ Real.sqrt (Real.log (2 : ℝ) / 2) := by
804 dsimp [a, b]
805 apply Real.sqrt_le_sqrt
806 rw [Real.log_pow]
807 have hlog : 3 * Real.log (2 : ℝ) / ((2 : ℝ) ^ 3) ≤ Real.log (2 : ℝ) / 2 := by
808 have hpos : 0 < Real.log (2 : ℝ) := Real.log_pos (by norm_num)
809 nlinarith
810 simpa using hlog
811 have hforward :
812 Finset.sum (Finset.range n) (fun i => b (n - i)) =
813 Finset.sum (Finset.range n) (fun k => a k) := by
814 have hflip := Finset.sum_flip (f := b) (n := n)
815 rw [Finset.sum_range_succ, Finset.sum_range_succ'] at hflip
816 simpa [a, hb0] using hflip
817 have h_nonneg : ∀ k : ℕ, 0 ≤ a k := by
818 intro k
819 exact Real.sqrt_nonneg _
820 have h_extend :
821 Finset.sum (Finset.range n) (fun k => a k) ≤
822 Finset.sum (Finset.range (2 * (n / 2 + 1))) (fun k => a k) := by
823 apply Finset.sum_le_sum_of_subset_of_nonneg
824 · intro x hx
825 simp at hx ⊢
826 omega
827 · intro x hx hxN
828 exact h_nonneg x
829 have h_pairs : ∀ m : ℕ,
830 Finset.sum (Finset.range (2 * (m + 1))) a =
831 a 0 + a 1 + Finset.sum (Finset.range m) (fun t => a (2 * t + 2) + a (2 * t + 3)) := by
832 intro m
833 induction m with
834 | zero =>
835 norm_num [Finset.sum_range_succ]
836 | succ m ihm =>
837 rw [show 2 * (m.succ + 1) = 2 * (m + 1) + 2 by omega, Finset.sum_range_add, ihm]
838 have htwo : ∑ x ∈ Finset.range 2, a (2 * (m + 1) + x) = a (2 * m + 2) + a (2 * m + 3) := by
839 rw [Finset.sum_range_succ, Finset.sum_range_succ]
840 simp
841 ring_nf
842 rw [htwo]
843 have htail :
844 a (2 * m + 2) + a (2 * m + 3) +
845 Finset.sum (Finset.range m) (fun t => a (2 * t + 2) + a (2 * t + 3)) =
846 Finset.sum (Finset.range (m + 1)) (fun t => a (2 * t + 2) + a (2 * t + 3)) := by
847 simpa [add_assoc, add_left_comm, add_comm, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using
848 (Finset.sum_range_succ_comm (f := fun t => a (2 * t + 2) + a (2 * t + 3)) m).symm
849 linarith
850 have hb_even : ∀ t : ℕ,
851 b (2 * t + 2) ≤ (3 / 4 : ℝ) ^ t * Real.sqrt (Real.log (2 : ℝ) / 2) := by
852 intro t
853 induction t with
854 | zero =>
855 exact le_of_eq (by simpa [a] using ha1)
856 | succ t iht =>
857 have hdec := dyadic_error_decay_two_steps (m := 2 * t + 2) (by omega)
858 have hEq : 2 * t.succ + 2 = 2 * t + 4 := by omega
859 rw [hEq]
860 calc
861 b (2 * t + 4) ≤ (3 / 4 : ℝ) * b (2 * t + 2) := hdec
862 _ ≤ (3 / 4 : ℝ) * ((3 / 4 : ℝ) ^ t * Real.sqrt (Real.log (2 : ℝ) / 2)) := by
863 gcongr
864 _ = (3 / 4 : ℝ) ^ t.succ * Real.sqrt (Real.log (2 : ℝ) / 2) := by
865 rw [pow_succ]
866 ring
867 have hb_odd : ∀ t : ℕ,
868 b (2 * t + 3) ≤ (3 / 4 : ℝ) ^ t * Real.sqrt (Real.log (2 : ℝ) / 2) := by
869 intro t
870 induction t with
871 | zero =>
872 simpa [a] using ha2
873 | succ t iht =>
874 have hdec := dyadic_error_decay_two_steps (m := 2 * t + 3) (by omega)
875 have hEq : 2 * t.succ + 3 = 2 * t + 5 := by omega
876 rw [hEq]
877 calc
878 b (2 * t + 5) ≤ (3 / 4 : ℝ) * b (2 * t + 3) := hdec
879 _ ≤ (3 / 4 : ℝ) * ((3 / 4 : ℝ) ^ t * Real.sqrt (Real.log (2 : ℝ) / 2)) := by
880 gcongr
881 _ = (3 / 4 : ℝ) ^ t.succ * Real.sqrt (Real.log (2 : ℝ) / 2) := by
882 rw [pow_succ]
883 ring
884 have hpair_bound : ∀ t : ℕ,
885 a (2 * t + 2) + a (2 * t + 3) ≤
886 2 * ((3 / 4 : ℝ) ^ t) * Real.sqrt (Real.log (2 : ℝ) / 2) := by
887 intro t
888 have h1 : a (2 * t + 2) ≤ (3 / 4 : ℝ) ^ t * Real.sqrt (Real.log (2 : ℝ) / 2) := by
889 simpa [a, Nat.add_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using hb_odd t
890 have h2 : a (2 * t + 3) ≤ (3 / 4 : ℝ) ^ t * Real.sqrt (Real.log (2 : ℝ) / 2) := by
891 have h2raw : b (2 * (t + 1) + 2) ≤ (3 / 4 : ℝ) ^ (t + 1) * Real.sqrt (Real.log (2 : ℝ) / 2) :=
892 hb_even (t + 1)
893 have hEq : 2 * (t + 1) + 2 = 2 * t + 4 := by omega
894 rw [hEq] at h2raw
895 have hpow : (3 / 4 : ℝ) ^ (t + 1) * Real.sqrt (Real.log (2 : ℝ) / 2) ≤
896 (3 / 4 : ℝ) ^ t * Real.sqrt (Real.log (2 : ℝ) / 2) := by
897 have hpow' : (3 / 4 : ℝ) ^ (t + 1) ≤ (3 / 4 : ℝ) ^ t := by
898 rw [pow_succ]
899 have hnonneg : 0 ≤ (3 / 4 : ℝ) ^ t := pow_nonneg (by norm_num) t
900 nlinarith
901 gcongr
902 exact le_trans h2raw hpow
903 linarith
904 have hgeom : ∀ m : ℕ,
905 Finset.sum (Finset.range m) (fun t =>
906 2 * ((3 / 4 : ℝ) ^ t) * Real.sqrt (Real.log (2 : ℝ) / 2)) ≤
907 8 * Real.sqrt (Real.log (2 : ℝ) / 2) := by
908 intro m
909 have hs : ∑ t ∈ Finset.range m, ((3 / 4 : ℝ) ^ t) ≤ 4 := by
910 have hs' :=
911 geom_sum_Ico_le_of_lt_one (x := (3 / 4 : ℝ)) (m := 0) (n := m) (by positivity) (by norm_num)
912 norm_num at hs' ⊢
913 simpa using hs'
914 calc
915 Finset.sum (Finset.range m) (fun t =>
916 2 * ((3 / 4 : ℝ) ^ t) * Real.sqrt (Real.log (2 : ℝ) / 2)) =
917 Finset.sum (Finset.range m) (fun t =>
918 (2 * Real.sqrt (Real.log (2 : ℝ) / 2)) * ((3 / 4 : ℝ) ^ t)) := by
919 congr with t
920 ring
921 _ =
922 (2 * Real.sqrt (Real.log (2 : ℝ) / 2)) *
923 (∑ t ∈ Finset.range m, ((3 / 4 : ℝ) ^ t)) := by
924 rw [Finset.mul_sum]
925 _ ≤ (2 * Real.sqrt (Real.log (2 : ℝ) / 2)) * 4 := by
926 have hfac : 0 ≤ 2 * Real.sqrt (Real.log (2 : ℝ) / 2) := by positivity
927 exact mul_le_mul_of_nonneg_left hs hfac
928 _ = 8 * Real.sqrt (Real.log (2 : ℝ) / 2) := by
929 ring
930 calc
931 Finset.sum (Finset.range n) (fun i =>
932 Real.sqrt (Real.log ((2 : ℝ) ^ (n - i)) / ((2 : ℝ) ^ (n - i)))) =
933 Finset.sum (Finset.range n) (fun k => a k) := hforward
934 _ ≤ Finset.sum (Finset.range (2 * (n / 2 + 1))) (fun k => a k) := h_extend
935 _ = a 0 + a 1 + Finset.sum (Finset.range (n / 2)) (fun t => a (2 * t + 2) + a (2 * t + 3)) := by
936 simpa [h_pairs, Nat.add_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
937 _ ≤ Real.sqrt (Real.log (2 : ℝ) / 2) + Real.sqrt (Real.log (2 : ℝ) / 2) +
938 Finset.sum (Finset.range (n / 2)) (fun t =>
939 2 * ((3 / 4 : ℝ) ^ t) * Real.sqrt (Real.log (2 : ℝ) / 2)) := by
940 have hsum :
941 Finset.sum (Finset.range (n / 2)) (fun t => a (2 * t + 2) + a (2 * t + 3)) ≤
942 Finset.sum (Finset.range (n / 2)) (fun t =>
943 2 * ((3 / 4 : ℝ) ^ t) * Real.sqrt (Real.log (2 : ℝ) / 2)) := by
944 exact Finset.sum_le_sum (fun t ht => hpair_bound t)
945 linarith [le_of_eq ha0, le_of_eq ha1, hsum]
946 _ ≤ Real.sqrt (Real.log (2 : ℝ) / 2) + Real.sqrt (Real.log (2 : ℝ) / 2) +
947 8 * Real.sqrt (Real.log (2 : ℝ) / 2) := by
948 gcongr
949 exact hgeom (n / 2)
950 _ = 10 * Real.sqrt (Real.log (2 : ℝ) / 2) := by
951 ring
952
953/-- `Finset.univ` is a `0`-approximation for any family. -/
954private lemma univ_isEpsilonApprox {α : Type*} [DecidableEq α] [Fintype α]
955 (𝒜 : Finset (Finset α)) :
956 Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 0 Finset.univ := by
957 intro S _
958 simp [Finset.inter_univ, Finset.card_univ]
959
960/-- Monotonicity of `IsEpsilonApprox` in the tolerance parameter. -/
961private lemma isEpsilonApprox_mono {α : Type*} [DecidableEq α] [Fintype α]
962 {𝒜 : Finset (Finset α)} {Y : Finset α} {ε₁ ε₂ : ℝ}
963 (h : Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 ε₁ Y) (hε : ε₁ ≤ ε₂) :
964 Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 ε₂ Y := fun S hS =>
965 le_trans (h S hS) hε
966
967/-- The halving iteration: starting from `Finset.univ` (a 0-approximation),
968 repeatedly apply `random_halving_step` until the size drops below `threshold`.
969
970 The accumulated error is bounded by `K · c · √(log m / m)` where `m` is
971 the threshold, using the fact that the error terms
972 `c · √(log|Yᵢ|/|Yᵢ|)` along the halving chain sum to at most
973 `K · c · √(log m / m)` (the terms decay because `√(log x / x)` is
974 eventually decreasing and sizes at least double going backwards).
975
976 **Proof strategy**: by strong induction on `Fintype.card α`.
977 - If `Fintype.card α ≤ threshold`: `Finset.univ` works.
978 - Otherwise: apply `random_halving_step` to get `W` with `|W| ≤ |univ|/2`,
979 and use `approx_transitive` to compose the step error with the recursive
980 error. The total error is bounded by the analytic sum bound. -/
981private lemma iterate_halving_approx {c : ℝ} (hc : 0 ≤ c) {d : ℕ}
982 {α : Type*} [DecidableEq α] [Fintype α]
983 (step : ∀ (𝒜 : Finset (Finset α)), 𝒜.vcDim ≤ d → ∀ Y : Finset α, 2 ≤ Y.card →
984 ∃ Z, Z ⊆ Y ∧ 0 < Z.card ∧ Z.card ≤ Y.card / 2 ∧
985 IsRelativeApprox 𝒜 Y Z (c * Real.sqrt (Real.log (↑Y.card) / ↑Y.card)))
986 (𝒜 : Finset (Finset α)) (hd : 𝒜.vcDim ≤ d) (threshold : ℕ) (ht : 1 ≤ threshold)
987 (B : ℕ → ℝ) (hB_nonneg : ∀ n, 0 ≤ B n)
988 (hB_step : ∀ n m : ℕ, threshold < n → 2 ≤ n → m ≤ n / 2 →
989 c * Real.sqrt (Real.log (n : ℝ) / n) + B m ≤ B n) :
990 ∀ (Y₀ : Finset α), 0 < Y₀.card →
991 ∀ ε₀ : ℝ, 0 ≤ ε₀ →
992 Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 ε₀ Y₀ →
993 ∃ Z : Finset α, Z ⊆ Y₀ ∧ 0 < Z.card ∧ Z.card ≤ threshold ∧
994 Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 (ε₀ + B Y₀.card) Z := by
995 -- Strong induction on Y₀.card.
996 suffices h : ∀ (n : ℕ) (Y₀ : Finset α), Y₀.card = n → 0 < n →
997 ∀ ε₀ : ℝ, 0 ≤ ε₀ →
998 Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 ε₀ Y₀ →
999 ∃ Z : Finset α, Z ⊆ Y₀ ∧ 0 < Z.card ∧ Z.card ≤ threshold ∧
1000 Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 (ε₀ + B Y₀.card) Z by
1001 intro Y₀ hY₀ ε₀ hε₀ hYε
1002 exact h Y₀.card Y₀ rfl hY₀ ε₀ hε₀ hYε
1003 intro n
1004 induction n using Nat.strong_induction_on with
1005 | _ n ih =>
1006 intro Y₀ hYn hYpos ε₀ hε₀ hYε
1007 have hYpos' : 0 < Y₀.card := hYn ▸ hYpos
1008 by_cases hcase : n ≤ threshold
1009 · -- Base case: Y₀ already at or below threshold.
1010 refine ⟨Y₀, subset_refl _, hYpos', hYn ▸ hcase, ?_⟩
1011 exact isEpsilonApprox_mono hYε (by linarith [hB_nonneg Y₀.card])
1012 · -- Inductive case: halve Y₀.
1013 push_neg at hcase
1014 have hYcard_ge : 2 ≤ Y₀.card := by rw [hYn]; omega
1015 obtain ⟨W, hWY, hWpos, hWhalf, hWrel⟩ := step 𝒜 hd Y₀ hYcard_ge
1016 have hWlt : W.card < n := by
1017 rw [← hYn]
1018 exact lt_of_le_of_lt hWhalf (Nat.div_lt_self (by omega) (by norm_num))
1019 have hWnewε : Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜
1020 (ε₀ + c * Real.sqrt (Real.log (Y₀.card : ℝ) / Y₀.card)) W :=
1021 approx_transitive 𝒜 hYε hWrel
1022 have hsqrt_nonneg : 0 ≤ c * Real.sqrt (Real.log (Y₀.card : ℝ) / Y₀.card) :=
1023 mul_nonneg hc (Real.sqrt_nonneg _)
1024 have hε_new_nonneg : 0 ≤ ε₀ + c * Real.sqrt (Real.log (Y₀.card : ℝ) / Y₀.card) := by
1025 linarith
1026 obtain ⟨Z, hZW, hZpos, hZthresh, hZε⟩ :=
1027 ih W.card hWlt W rfl hWpos _ hε_new_nonneg hWnewε
1028 refine ⟨Z, hZW.trans hWY, hZpos, hZthresh, ?_⟩
1029 -- Combine: total error so far ≤ ε₀ + B Y₀.card via hB_step.
1030 have hbound :
1031 c * Real.sqrt (Real.log (Y₀.card : ℝ) / Y₀.card) + B W.card ≤ B Y₀.card :=
1032 hB_step Y₀.card W.card (by rw [hYn]; exact hcase) hYcard_ge hWhalf
1033 refine isEpsilonApprox_mono hZε ?_
1034 linarith
1035
1036/-- Helper: monotonicity of `√(log x / x)` on `[3, ∞)`. -/
1037private lemma sqrt_log_div_antitone {a b : ℝ} (ha : 3 ≤ a) (hab : a ≤ b) :
1038 Real.sqrt (Real.log b / b) ≤ Real.sqrt (Real.log a / a) := by
1039 apply Real.sqrt_le_sqrt
1040 have hexp_le : Real.exp 1 ≤ a := le_of_lt (lt_of_lt_of_le Real.exp_one_lt_three ha)
1041 exact Real.log_div_self_antitoneOn hexp_le (le_trans hexp_le hab) hab
1042
1043/-- Analytic geometric tail estimate along a dyadic chain.
1044 For an absolute constant `Kchain`, for any threshold `T ≥ 3` and any `L`,
1045 `∑_{j=0}^{L-1} √(log(T·2^j)/(T·2^j)) ≤ Kchain · √(log T / T)`.
1046
1047 This is the geometric-decay analog of `geometric_error_sum`,
1048 parameterized by an arbitrary base `T` rather than `2`.
1049 The sum converges because `√(log(T·2^j)/(T·2^j))` decays like
1050 `2^{-j/2} · √(log(T·2^j))`, and the logarithmic factor is dominated
1051 by the geometric decay. -/
1052private lemma dyadic_chain_geometric_bound :
1053 ∃ Kchain : ℝ, 0 < Kchain ∧ ∀ T : ℕ, 4 ≤ T → ∀ L : ℕ,
1054 ∑ j ∈ Finset.range L,
1055 Real.sqrt (Real.log ((T : ℝ) * 2^j) / ((T : ℝ) * 2^j))
1056 ≤ Kchain * Real.sqrt (Real.log T / T) := by
1057 refine ⟨10, by norm_num, ?_⟩
1058 intro T hT L
1059 have hT_pos : (0 : ℝ) < T := by exact_mod_cast (by omega : 0 < T)
1060 have hT_ge4 : (4 : ℝ) ≤ (T : ℝ) := by exact_mod_cast hT
1061 have hT_ge3 : (3 : ℝ) ≤ (T : ℝ) := by linarith
1062 set f : ℕ → ℝ := fun j =>
1063 Real.sqrt (Real.log ((T : ℝ) * 2^j) / ((T : ℝ) * 2^j)) with hf_def
1064 have hf_nn : ∀ j, 0 ≤ f j := fun j => Real.sqrt_nonneg _
1065 have hXpos : ∀ j : ℕ, (0 : ℝ) < (T : ℝ) * 2^j := fun j => by positivity
1066 have hXge4 : ∀ j : ℕ, (4 : ℝ) ≤ (T : ℝ) * 2^j := fun j => by
1067 have h1 : (1 : ℝ) ≤ (2 : ℝ)^j := one_le_pow₀ (by norm_num : (1:ℝ) ≤ 2)
1068 nlinarith
1069 -- f(0) = √(log T / T)
1070 have hf0 : f 0 = Real.sqrt (Real.log T / T) := by
1071 simp [f]
1072 -- Two-step decay: f(j+2) ≤ (3/4) f(j)
1073 have hdecay : ∀ j : ℕ, f (j+2) ≤ (3/4 : ℝ) * f j := by
1074 intro j
1075 have hXg := hXge4 j
1076 have hX := hXpos j
1077 have hlogX_pos : 0 < Real.log ((T : ℝ) * 2^j) := by
1078 apply Real.log_pos; linarith
1079 have hlogX_ge_log4 : Real.log 4 ≤ Real.log ((T : ℝ) * 2^j) :=
1080 Real.log_le_log (by norm_num) hXg
1081 have hpow_eq : ((T : ℝ) * 2^(j+2)) = 4 * ((T : ℝ) * 2^j) := by
1082 rw [pow_add]; ring
1083 have h4Xpos : (0 : ℝ) < 4 * ((T : ℝ) * 2^j) := by positivity
1084 have hbase :
1085 Real.log ((T : ℝ) * 2^(j+2)) / ((T : ℝ) * 2^(j+2))
1086 ≤ ((3/4 : ℝ)^2) * (Real.log ((T : ℝ) * 2^j) / ((T : ℝ) * 2^j)) := by
1087 rw [hpow_eq, Real.log_mul (by norm_num : (4:ℝ) ≠ 0) (ne_of_gt hX)]
1088 rw [div_le_iff₀ h4Xpos]
1089 have hX_ne : ((T : ℝ) * 2^j) ≠ 0 := ne_of_gt hX
1090 rw [show ((3/4 : ℝ))^2 * (Real.log ((T:ℝ) * 2^j) / ((T:ℝ) * 2^j)) * (4 * ((T:ℝ) * 2^j))
1091 = (9/4 : ℝ) * Real.log ((T:ℝ) * 2^j) from by
1092 field_simp; ring]
1093 have hlog4_pos : 0 < Real.log 4 := Real.log_pos (by norm_num)
1094 linarith [hlogX_ge_log4, hlog4_pos]
1095 have hsqrt34 : Real.sqrt ((3/4:ℝ)^2) = (3/4:ℝ) := by
1096 rw [Real.sqrt_sq_eq_abs]; norm_num
1097 show f (j+2) ≤ (3/4 : ℝ) * f j
1098 calc f (j+2)
1099 ≤ Real.sqrt (((3/4:ℝ)^2) * (Real.log ((T:ℝ)*2^j) / ((T:ℝ)*2^j))) :=
1100 Real.sqrt_le_sqrt hbase
1101 _ = Real.sqrt ((3/4:ℝ)^2) * Real.sqrt (Real.log ((T:ℝ)*2^j) / ((T:ℝ)*2^j)) := by
1102 rw [Real.sqrt_mul (by positivity)]
1103 _ = (3/4 : ℝ) * f j := by rw [hsqrt34]
1104 -- f(1) ≤ f(0)
1105 have hf1_le_f0 : f 1 ≤ f 0 := by
1106 show Real.sqrt (Real.log ((T:ℝ) * 2^1) / ((T:ℝ) * 2^1)) ≤
1107 Real.sqrt (Real.log ((T:ℝ) * 2^0) / ((T:ℝ) * 2^0))
1108 simp only [pow_zero, pow_one, mul_one]
1109 exact sqrt_log_div_antitone hT_ge3 (by linarith)
1110 -- f(2k) ≤ (3/4)^k f(0)
1111 have hf_even : ∀ k, f (2*k) ≤ (3/4 : ℝ)^k * f 0 := by
1112 intro k
1113 induction k with
1114 | zero => simp
1115 | succ k ih =>
1116 have heq : 2 * (k+1) = 2*k + 2 := by ring
1117 rw [heq]
1118 have h34_nn : (0 : ℝ) ≤ 3/4 := by norm_num
1119 calc f (2*k+2)
1120 ≤ (3/4 : ℝ) * f (2*k) := hdecay (2*k)
1121 _ ≤ (3/4 : ℝ) * ((3/4 : ℝ)^k * f 0) := by
1122 have := mul_le_mul_of_nonneg_left ih h34_nn
1123 linarith
1124 _ = (3/4 : ℝ)^(k+1) * f 0 := by rw [pow_succ]; ring
1125 -- f(2k+1) ≤ (3/4)^k f(0)
1126 have hf_odd : ∀ k, f (2*k+1) ≤ (3/4 : ℝ)^k * f 0 := by
1127 intro k
1128 induction k with
1129 | zero => simpa using hf1_le_f0
1130 | succ k ih =>
1131 have heq : 2 * (k+1) + 1 = (2*k+1) + 2 := by ring
1132 rw [heq]
1133 have h34_nn : (0 : ℝ) ≤ 3/4 := by norm_num
1134 calc f ((2*k+1)+2)
1135 ≤ (3/4 : ℝ) * f (2*k+1) := hdecay (2*k+1)
1136 _ ≤ (3/4 : ℝ) * ((3/4 : ℝ)^k * f 0) := by
1137 have := mul_le_mul_of_nonneg_left ih h34_nn
1138 linarith
1139 _ = (3/4 : ℝ)^(k+1) * f 0 := by rw [pow_succ]; ring
1140 -- f(j) ≤ (3/4)^(j/2) f(0)
1141 have hf_floor : ∀ j, f j ≤ (3/4 : ℝ)^(j/2) * f 0 := by
1142 intro j
1143 by_cases hpar : j % 2 = 0
1144 · have hjk : j = 2 * (j/2) := by omega
1145 have h := hf_even (j/2)
1146 rw [← hjk] at h
1147 exact h
1148 · have hjk : j = 2 * (j/2) + 1 := by omega
1149 have h := hf_odd (j/2)
1150 rw [← hjk] at h
1151 exact h
1152 -- ∑_{j<2m} (3/4)^(j/2) = 2 · ∑_{k<m} (3/4)^k
1153 have hpair : ∀ m : ℕ, ∑ j ∈ Finset.range (2*m), (3/4 : ℝ)^(j/2) =
1154 2 * ∑ k ∈ Finset.range m, (3/4 : ℝ)^k := by
1155 intro m
1156 induction m with
1157 | zero => simp
1158 | succ m ih =>
1159 have heq : 2 * (m+1) = 2*m + 2 := by ring
1160 rw [heq, Finset.sum_range_succ, Finset.sum_range_succ, ih, Finset.sum_range_succ]
1161 have h1 : (2*m)/2 = m := by omega
1162 have h2 : (2*m+1)/2 = m := by omega
1163 rw [h1, h2]; ring
1164 -- Bound on ∑ (3/4)^(j/2)
1165 have hgeom_floor : ∑ j ∈ Finset.range L, (3/4 : ℝ)^(j/2) ≤ 8 := by
1166 have hext :
1167 ∑ j ∈ Finset.range L, (3/4 : ℝ)^(j/2) ≤
1168 ∑ j ∈ Finset.range (2*(L/2 + 1)), (3/4 : ℝ)^(j/2) := by
1169 apply Finset.sum_le_sum_of_subset_of_nonneg
1170 · intro x hx; simp at hx ⊢; omega
1171 · intros; positivity
1172 rw [hpair (L/2 + 1)] at hext
1173 have hgeom_4 : ∑ k ∈ Finset.range (L/2 + 1), (3/4 : ℝ)^k ≤ 4 := by
1174 have h := geom_sum_Ico_le_of_lt_one (x := (3/4 : ℝ)) (m := 0) (n := L/2 + 1)
1175 (by norm_num) (by norm_num)
1176 rw [← Finset.range_eq_Ico] at h
1177 have h4 : ((3/4 : ℝ))^0 / (1 - 3/4) = 4 := by norm_num
1178 rw [h4] at h
1179 exact h
1180 linarith
1181 -- Combine: ∑ f(j) ≤ ∑ (3/4)^(j/2) f(0) = f(0) · ∑(3/4)^(j/2) ≤ 8·f(0) ≤ 10·f(0)
1182 have hf0_nn : 0 ≤ f 0 := hf_nn 0
1183 calc ∑ j ∈ Finset.range L, f j
1184 ≤ ∑ j ∈ Finset.range L, (3/4 : ℝ)^(j/2) * f 0 :=
1185 Finset.sum_le_sum (fun j _ => hf_floor j)
1186 _ = (∑ j ∈ Finset.range L, (3/4 : ℝ)^(j/2)) * f 0 := by
1187 rw [Finset.sum_mul]
1188 _ ≤ 8 * f 0 := by
1189 have := mul_le_mul_of_nonneg_right hgeom_floor hf0_nn
1190 linarith
1191 _ ≤ 10 * Real.sqrt (Real.log T / T) := by
1192 have h0 : 0 ≤ Real.sqrt (Real.log T / T) := Real.sqrt_nonneg _
1193 rw [hf0]; linarith
1194
1195/-- Analytic helper for `halving_budget_exists`: for any positive `c` and `K`,
1196 there is a constant `C₀` such that for any `C ≥ C₀` and `r ≥ 2`,
1197 setting `T := ⌊C·r²·log r⌋` we have `T ≥ 4` and
1198 `K·c·√(log T/T) ≤ 1/r`. -/
1199private lemma exists_threshold_const (c K : ℝ) (hc : 0 < c) (hK : 0 < K) :
1200 ∃ C₀ : ℝ, 0 < C₀ ∧ ∀ C : ℝ, C₀ ≤ C → ∀ r : ℝ, 2 ≤ r →
1201 4 ≤ Nat.floor (C * r^2 * Real.log r) ∧
1202 K * c * Real.sqrt (Real.log (Nat.floor (C * r^2 * Real.log r) : ℝ) /
1203 (Nat.floor (C * r^2 * Real.log r) : ℝ)) ≤ 1 / r := by
1204 set A : ℝ := K^2 * c^2 with hA_def
1205 have hA_pos : 0 < A := by positivity
1206 have hlog2_pos : 0 < Real.log 2 := Real.log_pos one_lt_two
1207 have hlog2_half : (1 : ℝ) / 2 < Real.log 2 := by
1208 have := Real.log_two_gt_d9; linarith
1209 -- Step 1: log x / x → 0, so eventually log x ≤ x · (log 2)/(8A)
1210 have htend : Filter.Tendsto (fun x : ℝ => Real.log x / x) Filter.atTop (nhds 0) := by
1211 have h := Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero
1212 simpa using h
1213 have hε_pos : 0 < Real.log 2 / (8 * A) := by positivity
1214 have hev : ∀ᶠ x in Filter.atTop, Real.log x / x < Real.log 2 / (8 * A) :=
1215 htend.eventually (gt_mem_nhds hε_pos)
1216 rw [Filter.eventually_atTop] at hev
1217 obtain ⟨C₁, hC₁⟩ := hev
1218 refine ⟨max (max C₁ 8) (24 * A), ?_, ?_⟩
1219 · have : (0 : ℝ) < 8 := by norm_num
1220 have h1 : (8 : ℝ) ≤ max C₁ 8 := le_max_right _ _
1221 have h2 : max C₁ 8 ≤ max (max C₁ 8) (24 * A) := le_max_left _ _
1222 linarith
1223 intro C hC r hr
1224 have hC₁_le : C₁ ≤ C := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hC
1225 have h8_le : (8 : ℝ) ≤ C :=
1226 le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hC
1227 have h24A_le : 24 * A ≤ C := le_trans (le_max_right _ _) hC
1228 have hC_pos : 0 < C := by linarith
1229 have hlogC_nn : 0 ≤ Real.log C := Real.log_nonneg (by linarith)
1230 have hlogr_pos : 0 < Real.log r := Real.log_pos (by linarith)
1231 have hlogr_ge : Real.log 2 ≤ Real.log r := Real.log_le_log (by norm_num) hr
1232 have hr_pos : 0 < r := by linarith
1233 have hr2 : (4 : ℝ) ≤ r^2 := by nlinarith
1234 -- log C / C < log 2 / (8A), so 8 A log C < C log 2
1235 have hlogC_bound : 8 * A * Real.log C ≤ C * Real.log 2 := by
1236 have hlt := hC₁ C hC₁_le
1237 have h8A : (0 : ℝ) < 8 * A := by positivity
1238 have h1 : Real.log C / C * (C * (8 * A)) < Real.log 2 / (8 * A) * (C * (8 * A)) :=
1239 mul_lt_mul_of_pos_right hlt (by positivity)
1240 have h2 : Real.log C * (8 * A) < Real.log 2 * C := by
1241 have e1 : Real.log C / C * (C * (8 * A)) = Real.log C * (8 * A) := by
1242 field_simp
1243 have e2 : Real.log 2 / (8 * A) * (C * (8 * A)) = Real.log 2 * C := by
1244 field_simp
1245 linarith [h1, e1.symm.le, e2.symm.le]
1246 linarith
1247 -- T setup
1248 set X : ℝ := C * r^2 * Real.log r with hX_def
1249 have hX_pos : 0 < X := by positivity
1250 -- X ≥ C * 4 * log 2 ≥ 8 * 4 * log 2 > 16
1251 have hX_ge16 : (16 : ℝ) ≤ X := by
1252 have h := mul_le_mul (a := C * 4) (b := C * r^2) (c := Real.log 2) (d := Real.log r)
1253 (by nlinarith) hlogr_ge hlog2_pos.le (by positivity)
1254 have hCge : C * 4 * Real.log 2 ≥ 16 := by
1255 have : 8 * 4 * Real.log 2 ≥ 16 := by nlinarith
1256 nlinarith
1257 linarith [h]
1258 set T : ℕ := Nat.floor X with hT_def
1259 have hT_le : (T : ℝ) ≤ X := Nat.floor_le hX_pos.le
1260 have hT_ge : X - 1 ≤ (T : ℝ) := by
1261 have := Nat.sub_one_lt_floor X
1262 linarith
1263 have hT_ge_half : X / 2 ≤ (T : ℝ) := by linarith
1264 have hT_pos_real : (0 : ℝ) < (T : ℝ) := by linarith
1265 have hT_ge4 : 4 ≤ T := by
1266 have : (4 : ℝ) ≤ (T : ℝ) := by linarith
1267 exact_mod_cast this
1268 refine ⟨hT_ge4, ?_⟩
1269 -- Bound on log T
1270 have hT_le_Cr3 : (T : ℝ) ≤ C * r^3 := by
1271 have hlogr_le_r : Real.log r ≤ r := (Real.log_le_self hr_pos.le)
1272 have : X ≤ C * r^2 * r := by
1273 have := mul_le_mul_of_nonneg_left hlogr_le_r (by positivity : (0 : ℝ) ≤ C * r^2)
1274 simpa [hX_def] using this
1275 have h2 : C * r^2 * r = C * r^3 := by ring
1276 linarith [hT_le, this, h2.le]
1277 have hCr3_pos : 0 < C * r^3 := by positivity
1278 have hlogT_le : Real.log T ≤ Real.log C + 3 * Real.log r := by
1279 have h1 : Real.log T ≤ Real.log (C * r^3) :=
1280 Real.log_le_log hT_pos_real hT_le_Cr3
1281 have h2 : Real.log (C * r^3) = Real.log C + 3 * Real.log r := by
1282 rw [Real.log_mul hC_pos.ne' (by positivity), Real.log_pow]; push_cast; ring
1283 linarith
1284 have hlogT_nn : 0 ≤ Real.log T := Real.log_nonneg (by
1285 have : (1 : ℝ) ≤ 4 := by norm_num
1286 have h4 : (4 : ℝ) ≤ T := by exact_mod_cast hT_ge4
1287 linarith)
1288 -- Main inequality: A * r² * log T ≤ T
1289 have hMain : A * r^2 * Real.log T ≤ (T : ℝ) := by
1290 have hstep1 : A * r^2 * Real.log T ≤ A * r^2 * (Real.log C + 3 * Real.log r) :=
1291 mul_le_mul_of_nonneg_left hlogT_le (by positivity)
1292 have hstep2 : A * r^2 * (Real.log C + 3 * Real.log r) ≤ X / 2 := by
1293 -- equivalent: 2 A (log C + 3 log r) ≤ C log r (after dividing by r²)
1294 have hgoal : 2 * A * (Real.log C + 3 * Real.log r) ≤ C * Real.log r := by
1295 -- 2 A log C + 6 A log r ≤ C log r
1296 -- We have 8 A log C ≤ C log 2 ≤ C log r, so 2 A log C ≤ C log r / 4
1297 have h1 : 2 * A * Real.log C ≤ C * Real.log r / 4 := by
1298 have : 8 * A * Real.log C ≤ C * Real.log r := by
1299 have := hlogC_bound
1300 nlinarith [mul_le_mul_of_nonneg_left hlogr_ge (by linarith : (0:ℝ) ≤ C)]
1301 linarith
1302 -- 6 A log r ≤ C log r / 4 since 24 A ≤ C
1303 have h2 : 6 * A * Real.log r ≤ C * Real.log r / 4 := by
1304 have : 24 * A * Real.log r ≤ C * Real.log r := by
1305 have := mul_le_mul_of_nonneg_right h24A_le hlogr_pos.le
1306 linarith
1307 linarith
1308 nlinarith
1309 -- multiply hgoal by r²/2
1310 have hX2 : X / 2 = C * r^2 * Real.log r / 2 := by simp [hX_def]
1311 rw [hX2]
1312 nlinarith [hgoal, sq_nonneg r, hr_pos]
1313 linarith [hT_ge_half]
1314 -- Now derive K c √(log T/T) ≤ 1/r
1315 have hKcr_pos : 0 < K * c * r := by positivity
1316 have hsq_le : (K * c * r * Real.sqrt (Real.log T / T))^2 ≤ 1 := by
1317 have hnn : (0 : ℝ) ≤ Real.log T / T := div_nonneg hlogT_nn hT_pos_real.le
1318 rw [mul_pow, Real.sq_sqrt hnn]
1319 have : (K * c * r)^2 * (Real.log T / T) = A * r^2 * Real.log T / T := by
1320 simp [hA_def]; ring
1321 rw [this, div_le_one hT_pos_real]
1322 exact hMain
1323 have hpos : 0 ≤ K * c * r * Real.sqrt (Real.log T / T) := by
1324 apply mul_nonneg hKcr_pos.le (Real.sqrt_nonneg _)
1325 have hKcr_le_1 : K * c * r * Real.sqrt (Real.log T / T) ≤ 1 := by
1326 have h := Real.sqrt_le_sqrt hsq_le
1327 rw [Real.sqrt_sq hpos, Real.sqrt_one] at h
1328 exact h
1329 rw [le_div_iff₀ hr_pos]
1330 have heq : K * c * Real.sqrt (Real.log T / T) * r =
1331 K * c * r * Real.sqrt (Real.log T / T) := by ring
1332 rw [heq]; exact hKcr_le_1
1333
1334/-- Construct the analytic budget for the halving iteration. -/
1335private lemma halving_budget_exists {c : ℝ} (hc : 0 < c) (Cgeom : ℝ) (hCgeom : 0 < Cgeom) :
1336 ∃ C : ℝ, 0 < C ∧ (max 1 (c * Cgeom + 1)) ^ 2 ≤ C ∧
1337 ∀ (r : ℝ), 2 ≤ r → ∀ (M : ℕ),
1338 ∃ (threshold : ℕ) (B : ℕ → ℝ),
1339 1 ≤ threshold ∧
1340 ((threshold : ℝ) ≤ C * r ^ 2 * Real.log r) ∧
1341 (∀ n, 0 ≤ B n) ∧
1342 B M ≤ 1 / r ∧
1343 (∀ n m : ℕ, threshold < n → 2 ≤ n → m ≤ n / 2 →
1344 c * Real.sqrt (Real.log (n : ℝ) / n) + B m ≤ B n) := by
1345 obtain ⟨Kchain, hKchain_pos, hdyadic⟩ := dyadic_chain_geometric_bound
1346 obtain ⟨C₀, hC₀_pos, hanalytic⟩ := exists_threshold_const c Kchain hc hKchain_pos
1347 refine ⟨max C₀ ((max 1 (c * Cgeom + 1)) ^ 2),
1348 lt_of_lt_of_le hC₀_pos (le_max_left _ _),
1349 le_max_right _ _, ?_⟩
1350 intro r hr M
1351 set Cmax := max C₀ ((max 1 (c * Cgeom + 1)) ^ 2) with hCmax_def
1352 have hC₀_le : C₀ ≤ Cmax := le_max_left _ _
1353 obtain ⟨hT_ge4, hanalytic_bnd⟩ := hanalytic Cmax hC₀_le r hr
1354 set T : ℕ := Nat.floor (Cmax * r^2 * Real.log r) with hT_def
1355 have hT_pos : 0 < T := by omega
1356 have hCmax_pos : 0 < Cmax := lt_of_lt_of_le hC₀_pos hC₀_le
1357 have hlogr_pos : 0 < Real.log r := Real.log_pos (by linarith)
1358 set L : ℕ → ℕ := fun n => if n ≤ T then 0 else Nat.log 2 (n / T) + 1 with hL_def
1359 set f : ℕ → ℝ := fun k =>
1360 Real.sqrt (Real.log ((T : ℝ) * 2^k) / ((T : ℝ) * 2^k)) with hf_def
1361 set B : ℕ → ℝ := fun n => c * ∑ k ∈ Finset.range (L n), f k with hB_def
1362 have hf_nn : ∀ k, 0 ≤ f k := fun k => Real.sqrt_nonneg _
1363 have hB_nn : ∀ n, 0 ≤ B n := fun n =>
1364 mul_nonneg (le_of_lt hc) (Finset.sum_nonneg (fun _ _ => hf_nn _))
1365 have hc_nn : 0 ≤ c := le_of_lt hc
1366 -- Key: For T < n, c*√(log n/n) ≤ c * f (L n - 1).
1367 have hkey : ∀ n : ℕ, T < n → c * Real.sqrt (Real.log (n : ℝ) / n) ≤ c * f (L n - 1) := by
1368 intro n hn
1369 have hL_n : L n = Nat.log 2 (n / T) + 1 := by
1370 simp only [hL_def]; rw [if_neg (not_le.mpr hn)]
1371 have hLn_pos : 0 < L n := by rw [hL_n]; omega
1372 have hk_eq : L n - 1 = Nat.log 2 (n / T) := by rw [hL_n]; omega
1373 have hnT_pos : 0 < n / T := Nat.div_pos (le_of_lt hn) hT_pos
1374 have hpow_le : 2 ^ (Nat.log 2 (n / T)) ≤ n / T :=
1375 Nat.pow_log_le_self 2 (Nat.pos_iff_ne_zero.mp hnT_pos)
1376 have hTpow_le_n : T * 2 ^ (L n - 1) ≤ n := by
1377 rw [hk_eq]
1378 calc T * 2 ^ (Nat.log 2 (n / T))
1379 ≤ T * (n / T) := Nat.mul_le_mul_left T hpow_le
1380 _ ≤ n := Nat.mul_div_le n T
1381 have hT_le_Tpow : T ≤ T * 2 ^ (L n - 1) := by
1382 apply Nat.le_mul_of_pos_right
1383 exact Nat.two_pow_pos _
1384 have hTpow_ge3_nat : 3 ≤ T * 2 ^ (L n - 1) := le_trans (by omega) hT_le_Tpow
1385 have hTpow_ge3 : (3 : ℝ) ≤ ((T * 2 ^ (L n - 1) : ℕ) : ℝ) := by exact_mod_cast hTpow_ge3_nat
1386 have hTpow_le_n_real : ((T * 2 ^ (L n - 1) : ℕ) : ℝ) ≤ (n : ℝ) := by exact_mod_cast hTpow_le_n
1387 have hsqrt_le :
1388 Real.sqrt (Real.log (n : ℝ) / (n : ℝ))
1389 ≤ Real.sqrt (Real.log ((T * 2 ^ (L n - 1) : ℕ) : ℝ) /
1390 ((T * 2 ^ (L n - 1) : ℕ) : ℝ)) :=
1391 sqrt_log_div_antitone hTpow_ge3 hTpow_le_n_real
1392 have heq : f (L n - 1) =
1393 Real.sqrt (Real.log ((T * 2 ^ (L n - 1) : ℕ) : ℝ) /
1394 ((T * 2 ^ (L n - 1) : ℕ) : ℝ)) := by
1395 simp only [hf_def]; push_cast; rfl
1396 rw [heq]
1397 exact mul_le_mul_of_nonneg_left hsqrt_le hc_nn
1398 refine ⟨T, B, by omega, ?_, hB_nn, ?_, ?_⟩
1399 · -- T ≤ Cmax·r²·log r
1400 have hprod_nn : 0 ≤ Cmax * r^2 * Real.log r := by positivity
1401 exact Nat.floor_le hprod_nn
1402 · -- B M ≤ 1/r
1403 have h1 : (∑ k ∈ Finset.range (L M), f k) ≤
1404 Kchain * Real.sqrt (Real.log (T : ℝ) / T) := hdyadic T hT_ge4 (L M)
1405 have h2 : B M ≤ c * (Kchain * Real.sqrt (Real.log (T : ℝ) / T)) := by
1406 show c * _ ≤ _
1407 exact mul_le_mul_of_nonneg_left h1 hc_nn
1408 have h3 : c * (Kchain * Real.sqrt (Real.log (T : ℝ) / T)) =
1409 Kchain * c * Real.sqrt (Real.log (T : ℝ) / T) := by ring
1410 rw [h3] at h2
1411 exact le_trans h2 hanalytic_bnd
1412 · -- recurrence
1413 intro n m hn_gt_T hn_ge2 hm_le_half
1414 have hL_n : L n = Nat.log 2 (n / T) + 1 := by
1415 simp only [hL_def]; rw [if_neg (not_le.mpr hn_gt_T)]
1416 have hLn_pos : 0 < L n := by rw [hL_n]; omega
1417 have hLm_lt_Ln : L m < L n := by
1418 by_cases hmT : m ≤ T
1419 · have hLm_zero : L m = 0 := by simp only [hL_def]; rw [if_pos hmT]
1420 rw [hLm_zero]; exact hLn_pos
1421 · push_neg at hmT
1422 have hL_m : L m = Nat.log 2 (m / T) + 1 := by
1423 simp only [hL_def]; rw [if_neg (not_le.mpr hmT)]
1424 have hmT_div : m / T ≤ (n / T) / 2 := by
1425 calc m / T ≤ (n / 2) / T := Nat.div_le_div_right hm_le_half
1426 _ = n / (2 * T) := Nat.div_div_eq_div_mul n 2 T
1427 _ = n / (T * 2) := by rw [mul_comm 2 T]
1428 _ = (n / T) / 2 := (Nat.div_div_eq_div_mul n T 2).symm
1429 have hnT_ge2 : 2 ≤ n / T := by
1430 have h2m : 2 * m ≤ n := by omega
1431 have hmge : T + 1 ≤ m := hmT
1432 have : 2 * T + 2 ≤ n := by omega
1433 calc 2 = (2 * T) / T := (Nat.mul_div_cancel 2 hT_pos).symm
1434 _ ≤ n / T := Nat.div_le_div_right (by omega)
1435 have hlog_div : Nat.log 2 ((n / T) / 2) = Nat.log 2 (n / T) - 1 :=
1436 Nat.log_div_base 2 (n / T)
1437 have hlog_le : Nat.log 2 (m / T) ≤ Nat.log 2 (n / T) - 1 := by
1438 calc Nat.log 2 (m / T) ≤ Nat.log 2 ((n / T) / 2) := Nat.log_mono_right hmT_div
1439 _ = Nat.log 2 (n / T) - 1 := hlog_div
1440 have hlog_n_pos : 1 ≤ Nat.log 2 (n / T) := by
1441 have h := Nat.log_mono_right (b := 2) hnT_ge2
1442 simpa using h
1443 rw [hL_m, hL_n]; omega
1444 have hLn_sub : L n - 1 < L n := by omega
1445 have hLm_le : L m ≤ L n - 1 := by omega
1446 have hsplit : ∑ k ∈ Finset.range (L n), f k =
1447 (∑ k ∈ Finset.range (L m), f k) +
1448 ∑ k ∈ Finset.Ico (L m) (L n), f k := by
1449 have h := (Finset.sum_Ico_consecutive f (Nat.zero_le (L m)) (le_of_lt hLm_lt_Ln)).symm
1450 simp only [Finset.range_eq_Ico]
1451 exact h
1452 have hIco_ge : f (L n - 1) ≤ ∑ k ∈ Finset.Ico (L m) (L n), f k := by
1453 apply Finset.single_le_sum (f := f) (s := Finset.Ico (L m) (L n))
1454 (fun i _ => hf_nn i)
1455 rw [Finset.mem_Ico]
1456 exact ⟨hLm_le, hLn_sub⟩
1457 have hBn_eq : B n = c * (∑ k ∈ Finset.range (L m), f k) +
1458 c * ∑ k ∈ Finset.Ico (L m) (L n), f k := by
1459 show c * _ = _
1460 rw [hsplit, mul_add]
1461 have hBm_eq : B m = c * ∑ k ∈ Finset.range (L m), f k := rfl
1462 have hkeyN := hkey n hn_gt_T
1463 have hIco_mul : c * f (L n - 1) ≤ c * ∑ k ∈ Finset.Ico (L m) (L n), f k :=
1464 mul_le_mul_of_nonneg_left hIco_ge hc_nn
1465 calc c * Real.sqrt (Real.log (n : ℝ) / n) + B m
1466 ≤ c * f (L n - 1) + B m := by linarith
1467 _ ≤ c * (∑ k ∈ Finset.Ico (L m) (L n), f k) + B m := by linarith
1468 _ = B n := by rw [hBn_eq, hBm_eq]; ring
1469
1470/-- For any finite set family of VC-dimension at most `d`, and `r ≥ 2`,
1471 there exists a `(1/r)`-approximation of size `O(r² log r)`.
1472 The constant `C` depends only on `d`. (Lemma 5.13) -/
1473theorem epsilonApproxBound (d : ℕ) : ∃ C : ℝ, 0 < C ∧
1474 ∀ (α : Type*) [DecidableEq α] [Fintype α] (𝒜 : Finset (Finset α)),
1475 𝒜.vcDim ≤ d →
1476 ∀ (r : ℝ), 2 ≤ r →
1477 ∃ Y : Finset α, Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 (1 / r) Y ∧
1478 (Y.card : ℝ) ≤ C * r ^ 2 * Real.log r := by
1479 -- Get the halving step constant and the geometric error sum constant
1480 obtain ⟨c, hc, step⟩ := random_halving_step d
1481 obtain ⟨Cgeom, hCgeom, geom_bound⟩ := geometric_error_sum
1482 obtain ⟨C, hCpos, _hCge, hbudget⟩ := halving_budget_exists hc Cgeom hCgeom
1483 refine ⟨C, hCpos, ?_⟩
1484 intro α inst1 inst2 𝒜 hd r hr
1485 -- Use step at this specific universe to fix the metavariable
1486 have hstep := @step α inst1 inst2
1487 by_cases h_small : (Fintype.card α : ℝ) ≤ C * r ^ 2 * Real.log r
1488 · -- Small ground set: Y = Finset.univ is already small enough
1489 refine ⟨Finset.univ, isEpsilonApprox_mono (univ_isEpsilonApprox 𝒜) ?_, ?_⟩
1490 · positivity
1491 · simp [Finset.card_univ]; linarith
1492 · -- Large ground set: iterate halving from univ.
1493 push_neg at h_small
1494 -- Obtain the analytic budget.
1495 obtain ⟨threshold, B, ht, hthresh_le, hB_nonneg, hB_top, hB_step⟩ :=
1496 hbudget r hr (Fintype.card α)
1497 -- Universe is non-empty (since |α| ≥ C·r²·log r ≥ 0 — actually we need ≥ 1).
1498 have h_univ_pos : 0 < (Finset.univ : Finset α).card := by
1499 rw [Finset.card_univ]
1500 have hCpos : (0 : ℝ) < C := by positivity
1501 have hlog2_pos : 0 < Real.log 2 := Real.log_pos (by norm_num)
1502 have hlogr_pos : 0 < Real.log r := Real.log_pos (by linarith)
1503 have h_prod_pos : 0 < C * r ^ 2 * Real.log r := by positivity
1504 have : (0 : ℝ) < (Fintype.card α : ℝ) := lt_of_lt_of_le h_prod_pos (le_of_lt h_small)
1505 exact_mod_cast this
1506 -- Apply iterate_halving_approx starting from univ (a 0-approx).
1507 obtain ⟨Z, hZsub, hZpos, hZthresh, hZε⟩ :=
1508 iterate_halving_approx (le_of_lt hc) hstep 𝒜 hd threshold ht B hB_nonneg hB_step
1509 Finset.univ h_univ_pos 0 le_rfl (univ_isEpsilonApprox 𝒜)
1510 refine ⟨Z, ?_, ?_⟩
1511 · -- IsEpsilonApprox 𝒜 (1/r) Z, using B (Fintype.card α) ≤ 1/r
1512 have hbound : (0 : ℝ) + B (Finset.univ : Finset α).card ≤ 1 / r := by
1513 rw [Finset.card_univ]; linarith [hB_top]
1514 exact isEpsilonApprox_mono hZε hbound
1515 · -- Size: Z.card ≤ threshold ≤ C·r²·log r
1516 calc (Z.card : ℝ) ≤ (threshold : ℝ) := by exact_mod_cast hZthresh
1517 _ ≤ C * r ^ 2 * Real.log r := hthresh_le
1518
1519end Catalog.VC.EpsilonApproximationBound
1520