Formalizing Structural Graph Theory in Lean 4

Catalog/VC/PackingLemma/Full.lean
1import Catalog.VC.ShatterFunction.Full
2import Catalog.VC.ShatterFunctionLemma.Full
3import Catalog.VC.UnitDistanceGraphEdges.Full
4import Mathlib.Analysis.SpecialFunctions.Pow.Real
5
6namespace Catalog.VC.PackingLemma
7
8variable {α : Type*} [DecidableEq α]
9
10/-- A subfamily `𝒫` is `δ`-separated if any two distinct members have
11 symmetric difference of size strictly greater than `δ`. -/
12def IsSeparated (P : Finset (Finset α)) (δ : ℕ) : Prop :=
13 ∀ S ∈ P, ∀ S' ∈ P, S ≠ S' → δ < (S \ S' ∪ (S' \ S)).card
14
15/-! ### Helper lemmas -/
16
17/-- If `vcDim(P) = 0` then no singleton is shattered, so all elements of `P`
18 agree on every ground-set element, hence `|P| ≤ 1`. -/
19private theorem vcDim_zero_card_le_one [Fintype α]
20 (P : Finset (Finset α)) (hvc : P.vcDim = 0) :
21 P.card ≤ 1 := by
22 rw [Finset.card_le_one]
23 intro S hS S' hS'
24 by_contra hne
25 push_neg at hne
26 obtain ⟨a, ha⟩ := Finset.symmDiff_nonempty.mpr hne
27 have hshatter : P.Shatters {a} := by
28 rw [Finset.shatters_iff]
29 ext t
30 simp only [Finset.mem_image, Finset.mem_powerset, Finset.subset_singleton_iff]
31 rw [Finset.mem_symmDiff] at ha
32 constructor
33 · rintro ⟨T, _, rfl⟩
34 simp only [Finset.singleton_inter]
35 split_ifs <;> simp
36 · rintro (rfl | rfl)
37 · rcases ha with ⟨_, h⟩ | ⟨_, h⟩
38 · exact ⟨S', hS', by simp [h]⟩
39 · exact ⟨S, hS, by simp [h]⟩
40 · rcases ha with ⟨h, _⟩ | ⟨h, _⟩
41 · exact ⟨S, hS, by simp [h]⟩
42 · exact ⟨S', hS', by simp [h]⟩
43 have h1 := hshatter.card_le_vcDim
44 simp at h1
45 omega
46
47/-- If `shatterFun F m ≤ C · m^d` for all `m`, then `vcDim` of any subfamily
48 `P ⊆ F` is bounded by a constant depending only on `C` and `d`.
49 (Because `2^k ≤ shatterFun(F, k) ≤ C · k^d` forces `k` to be bounded,
50 since exponentials dominate polynomials.) -/
51private theorem vcDim_bounded (d : ℕ) (C : ℝ) (hC : 0 < C) :
52 ∃ K : ℕ, ∀ (β : Type*) [DecidableEq β] [Fintype β]
53 (F P : Finset (Finset β)),
54 P ⊆ F →
55 (∀ m : ℕ, (Catalog.VC.ShatterFunction.shatterFun F m : ℝ) ≤ C * (m : ℝ) ^ d) →
56 P.vcDim ≤ K := by
57 -- Step 1: From little-o, extract N such that ∀ n ≥ N, C * n^d < 2^n
58 have ho := @isLittleO_pow_const_const_pow_of_one_lt ℝ _ d 2 (by norm_num : (1:ℝ) < 2)
59 have hev : ∀ᶠ (n : ℕ) in Filter.atTop, C * (n : ℝ) ^ d < (2 : ℝ) ^ n := by
60 have h1 := ho.bound (show (0:ℝ) < C⁻¹ / 2 by positivity)
61 filter_upwards [h1] with n hn
62 have hnd : (0 : ℝ) ≤ (↑n) ^ d := by positivity
63 have h2n : (0 : ℝ) < (2 : ℝ) ^ (n : ℕ) := by positivity
64 rw [Real.norm_of_nonneg hnd, Real.norm_of_nonneg h2n.le] at hn
65 calc C * (↑n) ^ d
66 ≤ C * (C⁻¹ / 2 * (2:ℝ) ^ n) := mul_le_mul_of_nonneg_left hn hC.le
67 _ = (2:ℝ) ^ n / 2 := by field_simp
68 _ < (2:ℝ) ^ n := by linarith
69 rw [Filter.eventually_atTop] at hev
70 obtain ⟨N, hN⟩ := hev
71 -- Step 2: K = N works
72 use N
73 intro β _ _ F P hPF hπ
74 -- P.vcDim ≤ F.vcDim by monotonicity, so suffices to bound F.vcDim
75 calc P.vcDim ≤ F.vcDim := Finset.vcDim_mono hPF
76 _ ≤ N := by
77 by_contra hlt
78 push_neg at hlt
79 -- Extract a shattered set with card > N
80 have hlt' : ¬ (F.shatterer.sup Finset.card ≤ N) := not_le.mpr hlt
81 rw [Finset.sup_le_iff] at hlt'
82 push_neg at hlt'
83 obtain ⟨s, hs_mem, hs_card⟩ := hlt'
84 rw [Finset.mem_shatterer] at hs_mem
85 -- hs_mem : F.Shatters s, hs_card : N < s.card
86 -- Show 2^(s.card) ≤ shatterFun F (s.card) via trace
87 have h_trace : (Catalog.VC.ShatterFunction.trace F s) = s.powerset := by
88 show F.image (· ∩ s) = s.powerset
89 have : F.image (· ∩ s) = F.image (s ∩ ·) :=
90 Finset.image_congr (fun x _ => Finset.inter_comm x s)
91 rw [this]
92 exact Finset.shatters_iff.mp hs_mem
93 have h_le_sf : (Catalog.VC.ShatterFunction.trace F s).card ≤
94 Catalog.VC.ShatterFunction.shatterFun F s.card :=
95 Finset.le_sup (f := fun Y => (Catalog.VC.ShatterFunction.trace F Y).card)
96 (Finset.mem_filter.mpr ⟨Finset.mem_univ s, rfl⟩)
97 -- Chain: 2^(s.card) ≤ shatterFun ≤ C * (s.card)^d < 2^(s.card)
98 have h1 : (2:ℝ) ^ s.card ≤ C * (s.card : ℝ) ^ d := by
99 have : (2 ^ s.card : ℕ) ≤ Catalog.VC.ShatterFunction.shatterFun F s.card := by
100 calc 2 ^ s.card = s.powerset.card := (Finset.card_powerset s).symm
101 _ = (Catalog.VC.ShatterFunction.trace F s).card := by rw [h_trace]
102 _ ≤ _ := h_le_sf
103 calc (2:ℝ) ^ s.card = ((2 ^ s.card : ℕ) : ℝ) := by push_cast; ring
104 _ ≤ ↑(Catalog.VC.ShatterFunction.shatterFun F s.card) := by exact_mod_cast this
105 _ ≤ C * (s.card : ℝ) ^ d := hπ s.card
106 linarith [hN s.card hs_card.le]
107
108/-- `|P| ≤ shatterFun F n` when `P ⊆ F`, since the trace of `F` on the full
109 ground set is `F` itself. -/
110private theorem card_le_shatterFun [Fintype α] (F P : Finset (Finset α))
111 (hPF : P ⊆ F) :
112 (P.card : ℝ) ≤ (Catalog.VC.ShatterFunction.shatterFun F (Fintype.card α) : ℝ) := by
113 have h1 : P.card ≤ F.card := Finset.card_le_card hPF
114 have h2 : (Catalog.VC.ShatterFunction.trace F Finset.univ) = F := by
115 show F.image (· ∩ Finset.univ) = F
116 simp [Finset.inter_univ]
117 have h3 : F.card ≤ Catalog.VC.ShatterFunction.shatterFun F (Fintype.card α) := by
118 calc F.card = (Catalog.VC.ShatterFunction.trace F Finset.univ).card := by rw [h2]
119 _ ≤ Catalog.VC.ShatterFunction.shatterFun F (Fintype.card α) :=
120 Finset.le_sup (f := fun Y => (Catalog.VC.ShatterFunction.trace F Y).card)
121 (Finset.mem_filter.mpr ⟨Finset.mem_univ _, Finset.card_univ⟩)
122 exact_mod_cast Nat.le_trans h1 h3
123
124/-- The VC dimension of the trace (restriction) of `P` on `A` is at most
125 the VC dimension of `P`.
126 If `trace P A` shatters `S`, then `S ⊆ A` (all trace elements are subsets
127 of `A`), so `P` also shatters `S` (since `S ∩ (T ∩ A) = S ∩ T`). -/
128private theorem trace_vcDim_le (P : Finset (Finset α)) (A : Finset α) :
129 (Catalog.VC.ShatterFunction.trace P A).vcDim ≤ P.vcDim := by
130 -- Suffices to show shatterer inclusion, then use sup_mono
131 show (Catalog.VC.ShatterFunction.trace P A).shatterer.sup Finset.card ≤
132 P.shatterer.sup Finset.card
133 apply Finset.sup_mono
134 intro s hs
135 rw [Finset.mem_shatterer] at hs ⊢
136 unfold Catalog.VC.ShatterFunction.trace at hs
137 -- Step 1: s ⊆ A (since s ⊆ some element of P.image (· ∩ A), and all such ⊆ A)
138 have hsA : s ⊆ A := by
139 obtain ⟨u, hu, hsu⟩ := hs.subset_iff.mp Finset.Subset.rfl
140 rw [Finset.mem_image] at hu
141 obtain ⟨T, _, rfl⟩ := hu
142 exact (Finset.inter_eq_left.mp hsu).trans Finset.inter_subset_right
143 -- Step 2: (P.image (· ∩ A)).image (s ∩ ·) = P.image (s ∩ ·)
144 rw [Finset.shatters_iff] at hs ⊢
145 have : Finset.image (s ∩ ·) (Finset.image (· ∩ A) P) = Finset.image (s ∩ ·) P := by
146 rw [Finset.image_image]
147 exact Finset.image_congr (fun T _ => by
148 show s ∩ (T ∩ A) = s ∩ T
149 rw [← Finset.inter_assoc, Finset.inter_eq_left.mpr
150 (Finset.inter_subset_left.trans hsA)])
151 rwa [this] at hs
152
153/-! ### Auxiliary definitions for combined_inequality -/
154
155/-- Weight of a trace element `q` in the trace of `P` on `A`:
156 the number of sets `S ∈ P` with `S ∩ A = q`. -/
157private def traceWeight (P : Finset (Finset α)) (A q : Finset α) : ℕ :=
158 (P.filter (fun S => S ∩ A = q)).card
159
160/-- Weighted ordered unit-distance sum: for each ordered pair `(q₁, q₂)` in `Q`
161 with `|symmDiff(q₁, q₂)| = 1`, sum `min(w(q₁), w(q₂))`. -/
162private def weightedUDSum (Q : Finset (Finset α)) (w : Finset α → ℕ) : ℕ :=
163 (Q.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).sum
164 (fun p => min (w p.1) (w p.2))
165
166/-! ### Sub-lemmas for combined_inequality -/
167
168/-- The sum of trace weights over trace elements equals `|P|`.
169 This is the fiber decomposition: `P` is partitioned by the map `S ↦ S ∩ A`
170 into fibers indexed by `trace P A`, and the sizes sum to `|P|`. -/
171private theorem sum_traceWeight (P : Finset (Finset α)) (A : Finset α) :
172 (Catalog.VC.ShatterFunction.trace P A).sum (traceWeight P A) = P.card :=
173 (Finset.card_eq_sum_card_image (· ∩ A) P).symm
174
175/-- **Greedy peeling bound**: the weighted ordered UD sum is at most
176 `4 · vcDim(Q) · Σ w(q)`.
177
178 Proof sketch (by strong induction on `|Q|`):
179 - Find `q₀ ∈ Q` with minimum degree `d₀ ≤ 2 · vcDim(Q)`
180 (since average degree ≤ `2 · vcDim` from `unitDistEdgeBound`).
181 - Ordered pairs involving `q₀` contribute ≤ `2 · d₀ · w(q₀) ≤ 4 · vcDim · w(q₀)`.
182 - Apply induction to `Q \ {q₀}` for the remaining pairs.
183 - Total: `4 · vcDim · w(q₀) + 4 · vcDim · Σ_{Q\{q₀}} w = 4 · vcDim · Σ w`. -/
184private theorem greedy_peeling [Fintype α] (Q : Finset (Finset α)) (w : Finset α → ℕ) :
185 weightedUDSum Q w ≤ 4 * Q.vcDim * Q.sum w := by
186 -- Strong induction on |Q|
187 suffices ∀ (n : ℕ) (Q : Finset (Finset α)), Q.card = n →
188 weightedUDSum Q w ≤ 4 * Q.vcDim * Q.sum w from this _ Q rfl
189 intro n
190 induction n with
191 | zero =>
192 intro Q hQ
193 simp [Finset.card_eq_zero.mp hQ, weightedUDSum, Finset.offDiag_empty]
194 | succ n ih =>
195 intro Q hQ
196 have hne : Q.Nonempty := Finset.card_pos.mp (by omega)
197 -- Define UD-degree: number of UD neighbors for each vertex
198 let udDeg : Finset α → ℕ := fun q =>
199 (Q.filter (fun q' => q' ≠ q ∧ (symmDiff q q').card = 1)).card
200 -- Find vertex q₀ with minimum UD-degree
201 obtain ⟨q₀, hq₀, hmin⟩ := Finset.exists_min_image Q udDeg hne
202 -- Key: deg(q₀) ≤ 2 * vcDim(Q)
203 -- Proof: Σ_q deg(q) = # ordered UD pairs ≤ 2·vcDim·|Q|
204 -- Since q₀ minimizes degree: deg(q₀) · |Q| ≤ Σ deg ≤ 2·vcDim·|Q|
205 have hdeg : udDeg q₀ ≤ 2 * Q.vcDim := by
206 have hcard_pos : 0 < Q.card := Finset.card_pos.mpr hne
207 set UDE := Q.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1) with hUDE_def
208 have hub : UDE.card ≤ 2 * Q.vcDim * Q.card :=
209 Catalog.VC.UnitDistanceGraphEdges.unitDistEdgeBound Q
210 -- Each fiber of UDE over Prod.fst has card = udDeg
211 have hfib : ∀ q ∈ Q, udDeg q = (UDE.filter (fun p => p.1 = q)).card := by
212 intro q hq
213 simp only [udDeg, hUDE_def, Finset.filter_filter]
214 apply Finset.card_nbij (fun q' => (q, q'))
215 · intro q' hq'
216 simp only [Finset.mem_coe, Finset.mem_filter, Finset.mem_offDiag] at hq' ⊢
217 exact ⟨⟨hq, hq'.1, Ne.symm hq'.2.1⟩, hq'.2.2, trivial⟩
218 · intro q1 _ q2 _ h; exact congr_arg Prod.snd h
219 · intro ⟨a, b⟩ hab
220 simp only [Set.mem_image, Finset.mem_coe, Finset.mem_filter,
221 Finset.mem_offDiag] at hab ⊢
222 exact ⟨b, ⟨hab.1.2.1, Ne.symm (hab.2.2 ▸ hab.1.2.2),
223 hab.2.2 ▸ hab.2.1⟩, Prod.ext hab.2.2.symm rfl⟩
224 -- Q.sum udDeg = UDE.card via fiberwise counting
225 have hsum : Q.sum udDeg = UDE.card := by
226 have heq : Q.sum udDeg = Q.sum (fun q => (UDE.filter (fun p => p.1 = q)).card) :=
227 Finset.sum_congr rfl (fun q hq => hfib q hq)
228 rw [heq]
229 symm
230 apply Finset.card_eq_sum_card_fiberwise
231 intro p hp
232 have hmem : p ∈ Q.offDiag.filter (fun q => (symmDiff q.1 q.2).card = 1) :=
233 hUDE_def ▸ hp
234 exact (Finset.mem_offDiag.mp (Finset.mem_filter.mp hmem).1).1
235 -- min element times card ≤ sum (since q₀ minimizes udDeg)
236 have hmin_avg : Q.card * udDeg q₀ ≤ Q.sum udDeg := by
237 have h := Finset.card_nsmul_le_sum Q udDeg (udDeg q₀) (fun q hq => hmin q hq)
238 simpa [nsmul_eq_mul, mul_comm] using h
239 -- Combine: udDeg q₀ * Q.card ≤ 2 * Q.vcDim * Q.card
240 have hprod : udDeg q₀ * Q.card ≤ 2 * Q.vcDim * Q.card :=
241 calc udDeg q₀ * Q.card = Q.card * udDeg q₀ := Nat.mul_comm _ _
242 _ ≤ Q.sum udDeg := hmin_avg
243 _ = UDE.card := hsum
244 _ ≤ 2 * Q.vcDim * Q.card := hub
245 exact Nat.le_of_mul_le_mul_right hprod hcard_pos
246 -- Q' = Q \ {q₀}, has card = n
247 set Q' := Q.erase q₀ with hQ'_def
248 have hQ'card : Q'.card = n := by
249 simp [hQ'_def, Finset.card_erase_of_mem hq₀]; omega
250 have hQ'sub : Q' ⊆ Q := Finset.erase_subset q₀ Q
251 -- IH for Q'
252 have hih := ih Q' hQ'card
253 -- vcDim(Q') ≤ vcDim(Q) by monotonicity
254 have hvc : Q'.vcDim ≤ Q.vcDim := Finset.vcDim_mono hQ'sub
255 -- Sum decomposition: Q.sum w = Q'.sum w + w q₀
256 have hq₀_not_mem : q₀ ∉ Q' := Finset.notMem_erase q₀ Q
257 have hsum_split : Q.sum w = Q'.sum w + w q₀ :=
258 (Finset.add_sum_erase Q w hq₀).symm.trans (Nat.add_comm _ _)
259 -- Split weightedUDSum into Q'-internal pairs and pairs involving q₀
260 -- weightedUDSum Q w = weightedUDSum Q' w + (border terms involving q₀)
261 -- border terms ≤ 2 · udDeg(q₀) · w(q₀)
262 have hUD_split : weightedUDSum Q w ≤
263 weightedUDSum Q' w + 2 * udDeg q₀ * w q₀ := by
264 unfold weightedUDSum
265 have hQ_eq : Q = insert q₀ Q' := (Finset.insert_erase hq₀).symm
266 rw [hQ_eq, Finset.offDiag_insert hq₀_not_mem,
267 Finset.filter_union, Finset.filter_union]
268 -- Disjointness: A = Q'.offDiag.filter ud, B = {q₀}×Q').filter ud, C = Q'×{q₀}).filter ud
269 have hd1 : Disjoint
270 (Q'.offDiag.filter (fun p : Finset α × Finset α => (symmDiff p.1 p.2).card = 1))
271 (({q₀} ×ˢ Q').filter (fun p : Finset α × Finset α => (symmDiff p.1 p.2).card = 1)) := by
272 rw [Finset.disjoint_left]
273 intro p hp1 hp2
274 simp only [Finset.mem_filter, Finset.mem_offDiag] at hp1
275 simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_singleton] at hp2
276 exact hq₀_not_mem (hp2.1.1 ▸ hp1.1.1)
277 have hd2 : Disjoint
278 (Q'.offDiag.filter (fun p : Finset α × Finset α => (symmDiff p.1 p.2).card = 1) ∪
279 ({q₀} ×ˢ Q').filter (fun p : Finset α × Finset α => (symmDiff p.1 p.2).card = 1))
280 ((Q' ×ˢ {q₀}).filter (fun p : Finset α × Finset α => (symmDiff p.1 p.2).card = 1)) := by
281 rw [Finset.disjoint_left]
282 intro p hp1 hp2
283 simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_singleton] at hp2
284 have hp2_mem : p.2 ∈ Q' := by
285 rcases Finset.mem_union.mp hp1 with h | h
286 · simp only [Finset.mem_filter, Finset.mem_offDiag] at h; exact h.1.2.1
287 · simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_singleton] at h
288 exact h.1.2
289 exact hq₀_not_mem (hp2.1.2 ▸ hp2_mem)
290 rw [Finset.sum_union hd2, Finset.sum_union hd1]
291 -- Bound B.sum ≤ udDeg q₀ * w q₀
292 have hB : (({q₀} ×ˢ Q').filter (fun p : Finset α × Finset α =>
293 (symmDiff p.1 p.2).card = 1)).sum (fun p => min (w p.1) (w p.2)) ≤
294 udDeg q₀ * w q₀ := by
295 calc (({q₀} ×ˢ Q').filter (fun p : Finset α × Finset α =>
296 (symmDiff p.1 p.2).card = 1)).sum (fun p => min (w p.1) (w p.2))
297 ≤ (({q₀} ×ˢ Q').filter (fun p : Finset α × Finset α =>
298 (symmDiff p.1 p.2).card = 1)).card • w q₀ := by
299 apply Finset.sum_le_card_nsmul
300 intro p hp
301 simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_singleton] at hp
302 rw [hp.1.1]; exact Nat.min_le_left _ _
303 _ ≤ udDeg q₀ • w q₀ := by
304 apply nsmul_le_nsmul_left (Nat.zero_le _)
305 apply Finset.card_le_card_of_injOn Prod.snd
306 · intro p hp
307 simp only [Finset.mem_coe, Finset.mem_filter, Finset.mem_product,
308 Finset.mem_singleton] at hp
309 simp only [Finset.mem_coe, Finset.mem_filter]
310 exact ⟨hQ'sub hp.1.2, ne_of_mem_of_not_mem hp.1.2 hq₀_not_mem,
311 by rw [← hp.1.1]; exact hp.2⟩
312 · intro p hp q hq h
313 simp only [Finset.mem_coe, Finset.mem_filter, Finset.mem_product,
314 Finset.mem_singleton] at hp hq
315 exact Prod.ext (hp.1.1.trans hq.1.1.symm) h
316 _ = udDeg q₀ * w q₀ := nsmul_eq_mul _ _
317 -- Bound C.sum ≤ udDeg q₀ * w q₀
318 have hC : ((Q' ×ˢ {q₀}).filter (fun p : Finset α × Finset α =>
319 (symmDiff p.1 p.2).card = 1)).sum (fun p => min (w p.1) (w p.2)) ≤
320 udDeg q₀ * w q₀ := by
321 calc ((Q' ×ˢ {q₀}).filter (fun p : Finset α × Finset α =>
322 (symmDiff p.1 p.2).card = 1)).sum (fun p => min (w p.1) (w p.2))
323 ≤ ((Q' ×ˢ {q₀}).filter (fun p : Finset α × Finset α =>
324 (symmDiff p.1 p.2).card = 1)).card • w q₀ := by
325 apply Finset.sum_le_card_nsmul
326 intro p hp
327 simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_singleton] at hp
328 rw [hp.1.2]; exact Nat.min_le_right _ _
329 _ ≤ udDeg q₀ • w q₀ := by
330 apply nsmul_le_nsmul_left (Nat.zero_le _)
331 apply Finset.card_le_card_of_injOn Prod.fst
332 · intro p hp
333 simp only [Finset.mem_coe, Finset.mem_filter, Finset.mem_product,
334 Finset.mem_singleton] at hp
335 simp only [Finset.mem_coe, Finset.mem_filter]
336 exact ⟨hQ'sub hp.1.1, ne_of_mem_of_not_mem hp.1.1 hq₀_not_mem,
337 by have h := hp.2; rw [hp.1.2] at h; rwa [symmDiff_comm]⟩
338 · intro p hp q hq h
339 simp only [Finset.mem_coe, Finset.mem_filter, Finset.mem_product,
340 Finset.mem_singleton] at hp hq
341 exact Prod.ext h (hp.1.2.trans hq.1.2.symm)
342 _ = udDeg q₀ * w q₀ := nsmul_eq_mul _ _
343 linarith
344 -- Combine: IH + degree bound + sum split
345 calc weightedUDSum Q w
346 ≤ weightedUDSum Q' w + 2 * udDeg q₀ * w q₀ := hUD_split
347 _ ≤ 4 * Q'.vcDim * Q'.sum w + 2 * udDeg q₀ * w q₀ := by linarith [hih]
348 _ ≤ 4 * Q.vcDim * Q'.sum w + 2 * (2 * Q.vcDim) * w q₀ := by
349 have h1 : 4 * Q'.vcDim * Q'.sum w ≤ 4 * Q.vcDim * Q'.sum w :=
350 Nat.mul_le_mul_right _ (Nat.mul_le_mul_left 4 hvc)
351 have h2 : 2 * udDeg q₀ ≤ 2 * (2 * Q.vcDim) :=
352 Nat.mul_le_mul_left 2 hdeg
353 have h3 : 2 * udDeg q₀ * w q₀ ≤ 2 * (2 * Q.vcDim) * w q₀ :=
354 Nat.mul_le_mul_right _ h2
355 omega
356 _ = 4 * Q.vcDim * Q'.sum w + 4 * Q.vcDim * w q₀ := by ring
357 _ = 4 * Q.vcDim * (Q'.sum w + w q₀) := by ring
358 _ = 4 * Q.vcDim * Q.sum w := by rw [← hsum_split]
359
360/-- For fixed `A'` and `a ∉ A'`, sum over trace classes on `A'` the weight of
361 the edge created when we refine by membership of `a`.
362
363 If a trace class `q` splits into `b₁` sets containing `a` and `b₂` sets
364 omitting `a`, its contribution is `min b₁ b₂`, matching the lower-bound
365 step in the source proof. -/
366private def splitWeight (P : Finset (Finset α)) (A' : Finset α) (a : α) : ℕ :=
367 (Catalog.VC.ShatterFunction.trace P A').sum fun q =>
368 min
369 ((P.filter (fun S => S ∩ A' = q ∧ a ∈ S)).card)
370 ((P.filter (fun S => S ∩ A' = q ∧ a ∉ S)).card)
371
372private lemma subset_of_mem_trace (P : Finset (Finset α)) {A q : Finset α}
373 (hq : q ∈ Catalog.VC.ShatterFunction.trace P A) :
374 q ⊆ A := by
375 rw [Catalog.VC.ShatterFunction.trace, Finset.mem_image] at hq
376 obtain ⟨S, _, rfl⟩ := hq
377 exact Finset.inter_subset_right
378
379private lemma inter_erase_eq_of_not_mem {A S : Finset α} {a : α}
380 (haA : a ∈ A) (haS : a ∉ S) :
381 S ∩ A = S ∩ (A.erase a) := by
382 ext x
383 by_cases hx : x = a
384 · subst hx
385 simp [haA, haS]
386 · simp [hx]
387
388private lemma inter_erase_eq_of_mem {A S : Finset α} {a : α}
389 (haA : a ∈ A) (haS : a ∈ S) :
390 S ∩ A = insert a (S ∩ (A.erase a)) := by
391 ext x
392 by_cases hx : x = a
393 · subst hx
394 simp [haA, haS]
395 · simp [hx]
396
397private lemma symmDiff_insert_of_not_mem {q : Finset α} {a : α}
398 (haq : a ∉ q) :
399 symmDiff q (insert a q) = {a} := by
400 ext x
401 by_cases hx : x = a
402 · subst hx
403 simp [symmDiff_def, haq]
404 · simp [symmDiff_def, hx, haq]
405
406private lemma traceWeight_eq_filter_not_mem (P : Finset (Finset α)) {A q : Finset α} {a : α}
407 (haA : a ∈ A) (hq : q ∈ Catalog.VC.ShatterFunction.trace P (A.erase a)) :
408 traceWeight P A q =
409 (P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∉ S)).card := by
410 have haq : a ∉ q := by
411 intro haq
412 exact Finset.notMem_erase a A ((subset_of_mem_trace P hq) haq)
413 unfold traceWeight
414 congr
415 ext S
416 constructor
417 · intro h
418 have haS : a ∉ S := by
419 intro haS
420 have : a ∈ S ∩ A := by simp [haS, haA]
421 rw [h] at this
422 exact haq this
423 exact ⟨by
424 calc
425 S ∩ (A.erase a) = S ∩ A := (inter_erase_eq_of_not_mem haA haS).symm
426 _ = q := h, haS⟩
427 · rintro ⟨hSA, haS⟩
428 calc
429 S ∩ A = S ∩ (A.erase a) := inter_erase_eq_of_not_mem haA haS
430 _ = q := hSA
431
432private lemma traceWeight_eq_filter_mem (P : Finset (Finset α)) {A q : Finset α} {a : α}
433 (haA : a ∈ A) (hq : q ∈ Catalog.VC.ShatterFunction.trace P (A.erase a)) :
434 traceWeight P A (insert a q) =
435 (P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∈ S)).card := by
436 have haq : a ∉ q := by
437 intro haq
438 exact Finset.notMem_erase a A ((subset_of_mem_trace P hq) haq)
439 unfold traceWeight
440 congr
441 ext S
442 constructor
443 · intro h
444 have haS : a ∈ S := by
445 have : a ∈ S ∩ A := by
446 rw [h]
447 simp [haq]
448 exact (Finset.mem_inter.mp this).1
449 exact ⟨by
450 have h' : insert a (S ∩ (A.erase a)) = insert a q := by
451 simpa [inter_erase_eq_of_mem haA haS] using h
452 have := congrArg (fun t : Finset α => t.erase a) h'
453 simpa [haq] using this, haS⟩
454 · rintro ⟨hSA, haS⟩
455 rw [inter_erase_eq_of_mem haA haS, hSA]
456
457private lemma mem_trace_of_filter_not_mem_pos (P : Finset (Finset α)) {A q : Finset α} {a : α}
458 (haA : a ∈ A)
459 (hpos : 0 < (P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∉ S)).card) :
460 q ∈ Catalog.VC.ShatterFunction.trace P A := by
461 rcases Finset.card_pos.mp hpos with ⟨S, hS⟩
462 rw [Finset.mem_filter] at hS
463 rw [Catalog.VC.ShatterFunction.trace, Finset.mem_image]
464 refine ⟨S, hS.1, ?_⟩
465 calc
466 S ∩ A = S ∩ (A.erase a) := inter_erase_eq_of_not_mem haA hS.2.2
467 _ = q := hS.2.1
468
469private lemma mem_trace_of_filter_mem_pos (P : Finset (Finset α)) {A q : Finset α} {a : α}
470 (haA : a ∈ A)
471 (hpos : 0 < (P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∈ S)).card) :
472 insert a q ∈ Catalog.VC.ShatterFunction.trace P A := by
473 rcases Finset.card_pos.mp hpos with ⟨S, hS⟩
474 rw [Finset.mem_filter] at hS
475 rw [Catalog.VC.ShatterFunction.trace, Finset.mem_image]
476 refine ⟨S, hS.1, ?_⟩
477 calc
478 S ∩ A = insert a (S ∩ (A.erase a)) := inter_erase_eq_of_mem haA hS.2.2
479 _ = insert a q := by rw [hS.2.1]
480
481private lemma offDiag_mem_from_split (P : Finset (Finset α)) {A q : Finset α} {a : α}
482 (haA : a ∈ A)
483 (hq : q ∈ Catalog.VC.ShatterFunction.trace P (A.erase a))
484 (hpos :
485 0 < min
486 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∈ S)).card)
487 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∉ S)).card)) :
488 (insert a q, q) ∈
489 (Catalog.VC.ShatterFunction.trace P A).offDiag.filter
490 (fun p => (symmDiff p.1 p.2).card = 1) ∧
491 (q, insert a q) ∈
492 (Catalog.VC.ShatterFunction.trace P A).offDiag.filter
493 (fun p => (symmDiff p.1 p.2).card = 1) := by
494 have hmem : 0 < (P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∈ S)).card := by
495 exact lt_of_lt_of_le hpos (Nat.min_le_left _ _)
496 have hnot : 0 < (P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∉ S)).card := by
497 exact lt_of_lt_of_le hpos (Nat.min_le_right _ _)
498 have hqA : q ∈ Catalog.VC.ShatterFunction.trace P A := mem_trace_of_filter_not_mem_pos P haA hnot
499 have hqA' : insert a q ∈ Catalog.VC.ShatterFunction.trace P A := mem_trace_of_filter_mem_pos P haA hmem
500 have haq : a ∉ q := by
501 intro haq
502 exact Finset.notMem_erase a A ((subset_of_mem_trace P hq) haq)
503 constructor <;>
504 refine Finset.mem_filter.mpr ⟨Finset.mem_offDiag.mpr ⟨?_, ?_, ?_⟩, ?_⟩
505 · exact hqA'
506 · exact hqA
507 · intro hEq
508 have : a ∈ insert a q := by simp
509 have hEq' : insert a q = q := by simpa using hEq
510 exact haq (by rwa [hEq'] at this)
511 · simpa using (by
512 rw [symmDiff_comm, symmDiff_insert_of_not_mem haq]
513 simp : (symmDiff (insert a q) q).card = 1)
514 · exact hqA
515 · exact hqA'
516 · intro hEq
517 have : a ∈ insert a q := by simp
518 have hEq' : insert a q = q := by simpa using hEq.symm
519 exact haq (by rwa [hEq'] at this)
520 · simpa using (by
521 rw [symmDiff_insert_of_not_mem haq]
522 simp : (symmDiff q (insert a q)).card = 1)
523
524private lemma pairWeight_eq_split (P : Finset (Finset α)) {A q : Finset α} {a : α}
525 (haA : a ∈ A)
526 (hq : q ∈ Catalog.VC.ShatterFunction.trace P (A.erase a)) :
527 min (traceWeight P A (insert a q)) (traceWeight P A q) =
528 min
529 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∈ S)).card)
530 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∉ S)).card) := by
531 rw [traceWeight_eq_filter_mem P haA hq, traceWeight_eq_filter_not_mem P haA hq]
532
533private lemma splitWeight_eq_sum_pos (P : Finset (Finset α)) (A : Finset α) (a : α) :
534 splitWeight P (A.erase a) a =
535 ((Catalog.VC.ShatterFunction.trace P (A.erase a)).filter
536 (fun q =>
537 0 <
538 min
539 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∈ S)).card)
540 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∉ S)).card))).sum
541 (fun q =>
542 min
543 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∈ S)).card)
544 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∉ S)).card)) := by
545 unfold splitWeight
546 symm
547 apply Finset.sum_subset
548 · exact Finset.filter_subset _ _
549 · intro q hq hqf
550 have hzero :
551 ¬ 0 <
552 min
553 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∈ S)).card)
554 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∉ S)).card) := by
555 simpa [Finset.mem_filter, hq] using hqf
556 exact Nat.eq_zero_of_not_pos hzero
557
558private lemma symmDiff_mem_of_ne {S T : Finset α} {a : α}
559 (hmem : a ∈ symmDiff S T) :
560 (a ∈ S) ≠ (a ∈ T) := by
561 by_cases hS : a ∈ S <;> by_cases hT : a ∈ T <;> simp [Finset.mem_symmDiff, hS, hT] at hmem ⊢
562
563private lemma not_mem_of_mem_symmDiff_of_same_trace
564 {A' q S T : Finset α} {a : α}
565 (hS : S ∩ A' = q) (hT : T ∩ A' = q)
566 (hmem : a ∈ symmDiff S T) :
567 a ∉ A' := by
568 intro haA'
569 have hneq := symmDiff_mem_of_ne hmem
570 have hSa : a ∈ S ↔ a ∈ T := by
571 constructor
572 · intro haS
573 have hq : a ∈ q := by
574 rw [← hS]
575 simp [haS, haA']
576 have hTA : a ∈ T ∩ A' := by rw [hT]; exact hq
577 exact (Finset.mem_inter.mp hTA).1
578 · intro haT
579 have hq : a ∈ q := by
580 rw [← hT]
581 simp [haT, haA']
582 have hSA : a ∈ S ∩ A' := by rw [hS]; exact hq
583 exact (Finset.mem_inter.mp hSA).1
584 exact hneq (propext hSa)
585
586private lemma split_pairs_card (T : Finset (Finset α)) (a : α) :
587 (((T ×ˢ T).filter (fun p : Finset α × Finset α => (a ∈ p.1) ≠ (a ∈ p.2))).card) =
588 2 * (T.filter (fun S => a ∈ S)).card * (T.filter (fun S => a ∉ S)).card := by
589 let U1 := (T ×ˢ T).filter (fun p : Finset α × Finset α => a ∈ p.1 ∧ a ∉ p.2)
590 let U2 := (T ×ˢ T).filter (fun p : Finset α × Finset α => a ∉ p.1 ∧ a ∈ p.2)
591 have hsplit :
592 ((T ×ˢ T).filter (fun p : Finset α × Finset α => (a ∈ p.1) ≠ (a ∈ p.2))) =
593 U1 ∪ U2 := by
594 ext p
595 by_cases h1 : a ∈ p.1 <;> by_cases h2 : a ∈ p.2 <;> simp [U1, U2, h1, h2]
596 have hdisj : Disjoint U1 U2 := by
597 rw [Finset.disjoint_left]
598 intro p hp1 hp2
599 simp only [U1, U2, Finset.mem_filter, Finset.mem_product] at hp1 hp2
600 exact hp2.2.1 hp1.2.1
601 rw [hsplit, Finset.card_union_of_disjoint hdisj]
602 have hU1 :
603 U1.card = (T.filter (fun S => a ∈ S)).card * (T.filter (fun S => a ∉ S)).card := by
604 dsimp [U1]
605 rw [show ((T ×ˢ T).filter (fun p : Finset α × Finset α => a ∈ p.1 ∧ a ∉ p.2)) =
606 (T.filter (fun S => a ∈ S)) ×ˢ (T.filter (fun S => a ∉ S)) by
607 simpa using
608 (Finset.filter_product (s := T) (t := T) (p := fun S : Finset α => a ∈ S)
609 (q := fun S : Finset α => a ∉ S))]
610 exact Finset.card_product _ _
611 have hU2 :
612 U2.card = (T.filter (fun S => a ∉ S)).card * (T.filter (fun S => a ∈ S)).card := by
613 dsimp [U2]
614 rw [show ((T ×ˢ T).filter (fun p : Finset α × Finset α => a ∉ p.1 ∧ a ∈ p.2)) =
615 (T.filter (fun S => a ∉ S)) ×ˢ (T.filter (fun S => a ∈ S)) by
616 simpa using
617 (Finset.filter_product (s := T) (t := T) (p := fun S : Finset α => a ∉ S)
618 (q := fun S : Finset α => a ∈ S))]
619 exact Finset.card_product _ _
620 rw [hU1, hU2]
621 ring
622
623private lemma trace_class_lower_bound [Fintype α]
624 (P : Finset (Finset α)) (A' q : Finset α) (δ : ℕ)
625 (hsep : IsSeparated P δ)
626 (hq : q ∈ Catalog.VC.ShatterFunction.trace P A') :
627 δ * ((P.filter (fun S => S ∩ A' = q)).card - 1) ≤
628 2 * (Finset.univ \ A').sum (fun a =>
629 min
630 ((P.filter (fun S => S ∩ A' = q ∧ a ∈ S)).card)
631 ((P.filter (fun S => S ∩ A' = q ∧ a ∉ S)).card)) := by
632 let T : Finset (Finset α) := P.filter (fun S => S ∩ A' = q)
633 have hTpos : 0 < T.card := by
634 rw [Catalog.VC.ShatterFunction.trace, Finset.mem_image] at hq
635 obtain ⟨S, hS, hSq⟩ := hq
636 have hST : S ∈ T := by simpa [T, hSq] using hS
637 exact Finset.card_pos.mpr ⟨S, hST⟩
638 let D := T.offDiag.sigma (fun p => symmDiff p.1 p.2)
639 let C := (Finset.univ \ A').sigma
640 (fun a => (T ×ˢ T).filter (fun p : Finset α × Finset α => (a ∈ p.1) ≠ (a ∈ p.2)))
641 have hD_le_C : D.card ≤ C.card := by
642 apply Finset.card_le_card_of_injOn (f := fun x => ⟨x.2, x.1⟩)
643 · intro x hx
644 dsimp [D, C] at hx ⊢
645 simp only [Finset.mem_coe, Finset.mem_sigma] at hx ⊢
646 rcases Finset.mem_offDiag.mp hx.1 with ⟨hS, hT, hne⟩
647 have hS_mem : x.1.1 ∈ P ∧ x.1.1 ∩ A' = q := by
648 simpa [T, Finset.mem_filter] using hS
649 have hT_mem : x.1.2 ∈ P ∧ x.1.2 ∩ A' = q := by
650 simpa [T, Finset.mem_filter] using hT
651 have hS' : x.1.1 ∩ A' = q := hS_mem.2
652 have hT' : x.1.2 ∩ A' = q := hT_mem.2
653 refine ⟨Finset.mem_sdiff.mpr ⟨Finset.mem_univ _, ?_⟩, ?_⟩
654 · exact not_mem_of_mem_symmDiff_of_same_trace hS' hT' hx.2
655 · simp only [Finset.mem_filter, Finset.mem_product]
656 exact ⟨⟨hS, hT⟩, symmDiff_mem_of_ne hx.2⟩
657 · intro x hx y hy hxy
658 cases x
659 cases y
660 cases hxy
661 rfl
662 have hD_lower : δ * T.offDiag.card ≤ D.card := by
663 dsimp [D]
664 rw [Finset.card_sigma]
665 calc
666 δ * T.offDiag.card = ∑ _ ∈ T.offDiag, δ := by
667 simpa [Nat.mul_comm] using (Finset.sum_const_nat (s := T.offDiag) (m := δ))
668 _ ≤ ∑ p ∈ T.offDiag, (symmDiff p.1 p.2).card := by
669 apply Finset.sum_le_sum
670 intro p hp
671 rcases Finset.mem_offDiag.mp hp with ⟨hp1, hp2, hpne⟩
672 have hp1P : p.1 ∈ P := (Finset.mem_filter.mp hp1).1
673 have hp2P : p.2 ∈ P := (Finset.mem_filter.mp hp2).1
674 exact le_of_lt (hsep _ hp1P _ hp2P hpne)
675 have hC_upper :
676 C.card ≤ 2 * T.card * (Finset.univ \ A').sum (fun a =>
677 min ((T.filter (fun S => a ∈ S)).card) ((T.filter (fun S => a ∉ S)).card)) := by
678 dsimp [C]
679 rw [Finset.card_sigma]
680 calc
681 ∑ a ∈ Finset.univ \ A',
682 ((T ×ˢ T).filter (fun p : Finset α × Finset α => (a ∈ p.1) ≠ (a ∈ p.2))).card
683 = ∑ a ∈ Finset.univ \ A',
684 2 * (T.filter (fun S => a ∈ S)).card * (T.filter (fun S => a ∉ S)).card := by
685 apply Finset.sum_congr rfl
686 intro a ha
687 exact split_pairs_card T a
688 _ ≤ ∑ a ∈ Finset.univ \ A',
689 2 * T.card * min ((T.filter (fun S => a ∈ S)).card) ((T.filter (fun S => a ∉ S)).card) := by
690 apply Finset.sum_le_sum
691 intro a ha
692 have hpart :
693 (T.filter (fun S => a ∈ S)).card + (T.filter (fun S => a ∉ S)).card = T.card := by
694 simpa using (Finset.card_filter_add_card_filter_not (s := T) (p := fun S => a ∈ S))
695 by_cases hmn : (T.filter (fun S => a ∈ S)).card ≤ (T.filter (fun S => a ∉ S)).card
696 · have hmin :
697 min ((T.filter (fun S => a ∈ S)).card) ((T.filter (fun S => a ∉ S)).card) =
698 (T.filter (fun S => a ∈ S)).card := Nat.min_eq_left hmn
699 rw [hmin]
700 have hnle : (T.filter (fun S => a ∉ S)).card ≤ T.card := by omega
701 calc
702 2 * (T.filter (fun S => a ∈ S)).card * (T.filter (fun S => a ∉ S)).card
703 = (2 * (T.filter (fun S => a ∈ S)).card) * (T.filter (fun S => a ∉ S)).card := by ring
704 _ ≤ (2 * (T.filter (fun S => a ∈ S)).card) * T.card :=
705 Nat.mul_le_mul_left _ hnle
706 _ = 2 * T.card * (T.filter (fun S => a ∈ S)).card := by ring
707 · have hnm :
708 (T.filter (fun S => a ∉ S)).card ≤ (T.filter (fun S => a ∈ S)).card :=
709 le_of_not_ge hmn
710 have hmin :
711 min ((T.filter (fun S => a ∈ S)).card) ((T.filter (fun S => a ∉ S)).card) =
712 (T.filter (fun S => a ∉ S)).card := Nat.min_eq_right hnm
713 rw [hmin]
714 have hmle : (T.filter (fun S => a ∈ S)).card ≤ T.card := by omega
715 calc
716 2 * (T.filter (fun S => a ∈ S)).card * (T.filter (fun S => a ∉ S)).card
717 = (2 * (T.filter (fun S => a ∉ S)).card) * (T.filter (fun S => a ∈ S)).card := by ring
718 _ ≤ (2 * (T.filter (fun S => a ∉ S)).card) * T.card :=
719 Nat.mul_le_mul_left _ hmle
720 _ = 2 * T.card * (T.filter (fun S => a ∉ S)).card := by ring
721 _ = 2 * T.card * (Finset.univ \ A').sum (fun a =>
722 min ((T.filter (fun S => a ∈ S)).card) ((T.filter (fun S => a ∉ S)).card)) := by
723 rw [← Finset.mul_sum]
724 have hmain0 :
725 δ * T.offDiag.card ≤
726 2 * T.card * (Finset.univ \ A').sum (fun a =>
727 min ((T.filter (fun S => a ∈ S)).card) ((T.filter (fun S => a ∉ S)).card)) := by
728 exact le_trans hD_lower (le_trans hD_le_C hC_upper)
729 have hleft :
730 δ * (T.card * T.card - T.card) = T.card * (δ * (T.card - 1)) := by
731 calc
732 δ * (T.card * T.card - T.card) = δ * (T.card * T.card - T.card * 1) := by rw [Nat.mul_one]
733 _ = δ * (T.card * (T.card - 1)) := by rw [← Nat.mul_sub_left_distrib]
734 _ = T.card * (δ * (T.card - 1)) := by ac_rfl
735 have hright :
736 2 * T.card * (Finset.univ \ A').sum (fun a =>
737 min ((T.filter (fun S => a ∈ S)).card) ((T.filter (fun S => a ∉ S)).card)) =
738 T.card * (2 * (Finset.univ \ A').sum (fun a =>
739 min ((T.filter (fun S => a ∈ S)).card) ((T.filter (fun S => a ∉ S)).card))) := by
740 ac_rfl
741 have hmain :
742 T.card * (δ * (T.card - 1)) ≤
743 T.card * (2 * (Finset.univ \ A').sum (fun a =>
744 min ((T.filter (fun S => a ∈ S)).card) ((T.filter (fun S => a ∉ S)).card))) := by
745 have htmp : δ * (T.card * T.card - T.card) ≤
746 2 * T.card * (Finset.univ \ A').sum (fun a =>
747 min ((T.filter (fun S => a ∈ S)).card) ((T.filter (fun S => a ∉ S)).card)) := by
748 simpa [Finset.offDiag_card] using hmain0
749 rwa [hleft, hright] at htmp
750 have hcancel := Nat.le_of_mul_le_mul_left hmain hTpos
751 simpa [T, Finset.mem_filter, Finset.filter_filter, and_left_comm, and_assoc] using hcancel
752
753/-- **Averaging lower bound**: there exists an `s`-element subset `A` such that
754 the weighted UD sum on `trace P A` is at least
755 `(s · δ / n) · (|P| - C · (s-1)^d)`.
756
757 Proof: Global averaging over all `s`-element subsets. For each `A`,
758 sub-lemma D gives `W(A) ≥ 2·Σ_{a∈A} splitWeight(A\{a}, a)`.
759 Reindexing `(A, a∈A) ↔ (A', a∉A')` and applying sub-lemma C to each
760 `(s-1)`-element `A'` yields
761 `Σ_A W(A) ≥ 2·C(n,s-1)·δ·(|P|-SF(s-1))`.
762 Pigeonhole extracts a single `A` with the required bound. -/
763private theorem averaging_lower_bound [Fintype α] (d : ℕ) (C : ℝ) (hC : 0 < C)
764 (F P : Finset (Finset α))
765 (hPF : P ⊆ F)
766 (hπ : ∀ m : ℕ, (Catalog.VC.ShatterFunction.shatterFun F m : ℝ) ≤ C * (m : ℝ) ^ d)
767 (δ : ℕ) (hδ : 0 < δ) (hδn : δ ≤ Fintype.card α)
768 (hsep : IsSeparated P δ)
769 (s : ℕ) (hs : 0 < s) (hsn : s ≤ Fintype.card α) :
770 ∃ A : Finset α, A.card = s ∧
771 ((s : ℝ) * (δ : ℝ) / (Fintype.card α : ℝ) *
772 ((P.card : ℝ) - C * ((s : ℝ) - 1) ^ d)) ≤
773 (weightedUDSum (Catalog.VC.ShatterFunction.trace P A) (traceWeight P A) : ℝ) := by
774 set n := Fintype.card α with hn_def
775 -- ══════════════════════════════════════════════════════════════════
776 -- Trivial case: if |P| ≤ C·(s-1)^d, LHS ≤ 0 and any A of size s works
777 -- ══════════════════════════════════════════════════════════════════
778 by_cases htriv : (P.card : ℝ) ≤ C * ((s : ℝ) - 1) ^ d
779 · obtain ⟨A, -, hAcard⟩ := Finset.exists_subset_card_eq
780 (show s ≤ (Finset.univ : Finset α).card by rwa [Finset.card_univ])
781 exact ⟨A, hAcard, by
782 have h1 : (0 : ℝ) ≤ ↑(weightedUDSum (Catalog.VC.ShatterFunction.trace P A)
783 (traceWeight P A)) := Nat.cast_nonneg _
784 have h2 : (P.card : ℝ) - C * ((s : ℝ) - 1) ^ d ≤ 0 := by linarith
785 have h3 : 0 ≤ (s : ℝ) * (δ : ℝ) / (n : ℝ) := by positivity
786 nlinarith [mul_nonpos_of_nonneg_of_nonpos h3 h2]⟩
787 · push_neg at htriv -- htriv : C * (↑s - 1) ^ d < ↑P.card
788 -- ══════════════════════════════════════════════════════════════════
789 -- Main case: global averaging argument
790 -- ══════════════════════════════════════════════════════════════════
791 -- Sub-lemma A: |trace P A'| ≤ shatterFun(F, |A'|)
792 have hA_lem : ∀ A' : Finset α,
793 (Catalog.VC.ShatterFunction.trace P A').card ≤
794 Catalog.VC.ShatterFunction.shatterFun F A'.card := by
795 intro A'
796 calc (Catalog.VC.ShatterFunction.trace P A').card
797 ≤ (Catalog.VC.ShatterFunction.trace F A').card :=
798 Finset.card_le_card (Finset.image_mono _ hPF)
799 _ ≤ Catalog.VC.ShatterFunction.shatterFun F A'.card :=
800 Finset.le_sup (f := fun Y => (Catalog.VC.ShatterFunction.trace F Y).card)
801 (Finset.mem_filter.mpr ⟨Finset.mem_univ _, rfl⟩)
802 -- Sub-lemma C: the fixed-`A'` lower bound from the source proof.
803 -- For each trace class of size `b`, summing over `a ∉ A'` contributes at
804 -- least `δ * (b - 1)` by counting ordered differing pairs and using
805 -- `min(b₁,b₂) ≥ b₁b₂ / b`.
806 have hC_lem : ∀ A' : Finset α,
807 δ * (P.card - (Catalog.VC.ShatterFunction.trace P A').card) ≤
808 2 * (Finset.univ \ A').sum (fun a => splitWeight P A' a) := by
809 intro A'
810 have htrace_pos : ∀ q ∈ Catalog.VC.ShatterFunction.trace P A', 1 ≤ traceWeight P A' q := by
811 intro q hq
812 rw [traceWeight]
813 rw [Catalog.VC.ShatterFunction.trace, Finset.mem_image] at hq
814 obtain ⟨S, hS, hSq⟩ := hq
815 exact Finset.one_le_card.mpr ⟨S, by simpa [hSq, Finset.mem_filter] using hS⟩
816 have hsum_tsub :
817 (Catalog.VC.ShatterFunction.trace P A').sum (fun q => traceWeight P A' q - 1) =
818 P.card - (Catalog.VC.ShatterFunction.trace P A').card := by
819 have hsum_add :
820 (Catalog.VC.ShatterFunction.trace P A').sum (fun q => traceWeight P A' q - 1) +
821 (Catalog.VC.ShatterFunction.trace P A').card = P.card := by
822 calc
823 (Catalog.VC.ShatterFunction.trace P A').sum (fun q => traceWeight P A' q - 1) +
824 (Catalog.VC.ShatterFunction.trace P A').card
825 =
826 (Catalog.VC.ShatterFunction.trace P A').sum
827 (fun q => (traceWeight P A' q - 1) + 1) := by
828 rw [Finset.card_eq_sum_ones, ← Finset.sum_add_distrib]
829 _ = (Catalog.VC.ShatterFunction.trace P A').sum (traceWeight P A') := by
830 apply Finset.sum_congr rfl
831 intro q hq
832 exact Nat.sub_add_cancel (htrace_pos q hq)
833 _ = P.card := sum_traceWeight P A'
834 omega
835 have hsum_classes :
836 (Catalog.VC.ShatterFunction.trace P A').sum (fun q => δ * (traceWeight P A' q - 1)) ≤
837 (Catalog.VC.ShatterFunction.trace P A').sum (fun q =>
838 2 * (Finset.univ \ A').sum (fun a =>
839 min
840 ((P.filter (fun S => S ∩ A' = q ∧ a ∈ S)).card)
841 ((P.filter (fun S => S ∩ A' = q ∧ a ∉ S)).card))) := by
842 apply Finset.sum_le_sum
843 intro q hq
844 simpa [traceWeight] using trace_class_lower_bound P A' q δ hsep hq
845 calc
846 δ * (P.card - (Catalog.VC.ShatterFunction.trace P A').card)
847 = δ * (Catalog.VC.ShatterFunction.trace P A').sum
848 (fun q => traceWeight P A' q - 1) := by rw [hsum_tsub]
849 _ = (Catalog.VC.ShatterFunction.trace P A').sum (fun q => δ * (traceWeight P A' q - 1)) := by
850 rw [Finset.mul_sum]
851 _ ≤ (Catalog.VC.ShatterFunction.trace P A').sum (fun q =>
852 2 * (Finset.univ \ A').sum (fun a =>
853 min
854 ((P.filter (fun S => S ∩ A' = q ∧ a ∈ S)).card)
855 ((P.filter (fun S => S ∩ A' = q ∧ a ∉ S)).card))) := hsum_classes
856 _ = 2 * (Finset.univ \ A').sum (fun a => splitWeight P A' a) := by
857 rw [← Finset.mul_sum, Finset.sum_comm]
858 rfl
859 -- Sub-lemma D: for fixed `A`, each `a ∈ A` contributes the weight of the
860 -- edges whose difference element is `a`, and the ordered UD sum counts both
861 -- orientations.
862 have hD_lem : ∀ A : Finset α,
863 2 * A.sum (fun a => splitWeight P (A.erase a) a) ≤
864 weightedUDSum (Catalog.VC.ShatterFunction.trace P A) (traceWeight P A) := by
865 intro A
866 let U : Finset (Finset α × Finset α) :=
867 (Catalog.VC.ShatterFunction.trace P A).offDiag.filter
868 (fun p => (symmDiff p.1 p.2).card = 1)
869 let wt : Finset α × Finset α → ℕ :=
870 fun p => min (traceWeight P A p.1) (traceWeight P A p.2)
871 let Qpos : α → Finset (Finset α) := fun a =>
872 (Catalog.VC.ShatterFunction.trace P (A.erase a)).filter
873 (fun q =>
874 0 <
875 min
876 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∈ S)).card)
877 ((P.filter (fun S => S ∩ (A.erase a) = q ∧ a ∉ S)).card))
878 let Src := A.sigma Qpos
879 have hsplit :
880 A.sum (fun a => splitWeight P (A.erase a) a) =
881 Src.sum (fun x =>
882 min
883 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∈ S)).card)
884 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∉ S)).card)) := by
885 rw [Finset.sum_sigma]
886 apply Finset.sum_congr rfl
887 intro a ha
888 simp only [Qpos]
889 exact splitWeight_eq_sum_pos P A a
890 have hmem_src :
891 ∀ x ∈ Src,
892 x.1 ∈ A ∧
893 x.2 ∈ Catalog.VC.ShatterFunction.trace P (A.erase x.1) ∧
894 0 <
895 min
896 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∈ S)).card)
897 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∉ S)).card) := by
898 intro x hx
899 simp only [Src, Qpos, Finset.mem_sigma, Finset.mem_filter] at hx
900 exact ⟨hx.1, hx.2.1, hx.2.2⟩
901 have himg1_mem : ∀ x ∈ Src, (insert x.1 x.2, x.2) ∈ U := by
902 intro x hx
903 rcases hmem_src x hx with ⟨ha, hq, hpos⟩
904 exact (offDiag_mem_from_split P ha hq hpos).1
905 have himg2_mem : ∀ x ∈ Src, (x.2, insert x.1 x.2) ∈ U := by
906 intro x hx
907 rcases hmem_src x hx with ⟨ha, hq, hpos⟩
908 exact (offDiag_mem_from_split P ha hq hpos).2
909 have himg1_inj :
910 Set.InjOn (fun x : ((a : α) × Finset α) => (insert x.1 x.2, x.2))
911 (↑Src : Set ((a : α) × Finset α)) := by
912 intro x hx y hy hxy
913 have hx' := hmem_src x hx
914 have hy' := hmem_src y hy
915 have hq : x.2 = y.2 := by
916 exact Prod.mk.inj hxy |>.2
917 have hxa : x.1 ∉ x.2 := by
918 intro h
919 exact Finset.notMem_erase x.1 A ((subset_of_mem_trace P hx'.2.1) h)
920 have hya : y.1 ∉ y.2 := by
921 intro h
922 exact Finset.notMem_erase y.1 A ((subset_of_mem_trace P hy'.2.1) h)
923 have hins : insert x.1 x.2 = insert y.1 y.2 := by
924 exact Prod.mk.inj hxy |>.1
925 have hxy1 : x.1 = y.1 := by
926 have hins' : insert x.1 x.2 = insert y.1 x.2 := by
927 simpa [hq] using hins
928 have : x.1 ∈ insert y.1 x.2 := by
929 rw [← hins']
930 simp
931 simp [hxa] at this
932 exact this
933 cases x
934 cases y
935 simp at hq hxy1
936 simp [hxy1, hq]
937 have himg2_inj :
938 Set.InjOn (fun x : ((a : α) × Finset α) => (x.2, insert x.1 x.2))
939 (↑Src : Set ((a : α) × Finset α)) := by
940 intro x hx y hy hxy
941 have hx' := hmem_src x hx
942 have hy' := hmem_src y hy
943 have hq : x.2 = y.2 := by
944 exact Prod.mk.inj hxy |>.1
945 have hxa : x.1 ∉ x.2 := by
946 intro h
947 exact Finset.notMem_erase x.1 A ((subset_of_mem_trace P hx'.2.1) h)
948 have hya : y.1 ∉ y.2 := by
949 intro h
950 exact Finset.notMem_erase y.1 A ((subset_of_mem_trace P hy'.2.1) h)
951 have hins : insert x.1 x.2 = insert y.1 y.2 := by
952 exact Prod.mk.inj hxy |>.2
953 have hxy1 : x.1 = y.1 := by
954 have hins' : insert x.1 x.2 = insert y.1 x.2 := by
955 simpa [hq] using hins
956 have : x.1 ∈ insert y.1 x.2 := by
957 rw [← hins']
958 simp
959 simp [hxa] at this
960 exact this
961 cases x
962 cases y
963 simp at hq hxy1
964 simp [hxy1, hq]
965 have hsum_img1 :
966 (Finset.image (fun x : ((a : α) × Finset α) => (insert x.1 x.2, x.2)) Src).sum wt =
967 Src.sum (fun x =>
968 min
969 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∈ S)).card)
970 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∉ S)).card)) := by
971 rw [Finset.sum_image himg1_inj]
972 apply Finset.sum_congr rfl
973 intro x hx
974 rcases hmem_src x hx with ⟨ha, hq, _⟩
975 simpa [wt] using pairWeight_eq_split P ha hq
976 have hsum_img2 :
977 (Finset.image (fun x : ((a : α) × Finset α) => (x.2, insert x.1 x.2)) Src).sum wt =
978 Src.sum (fun x =>
979 min
980 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∈ S)).card)
981 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∉ S)).card)) := by
982 rw [Finset.sum_image himg2_inj]
983 apply Finset.sum_congr rfl
984 intro x hx
985 rcases hmem_src x hx with ⟨ha, hq, _⟩
986 simpa [wt, Nat.min_comm] using pairWeight_eq_split P ha hq
987 have hdisj :
988 Disjoint
989 (Finset.image (fun x : ((a : α) × Finset α) => (insert x.1 x.2, x.2)) Src)
990 (Finset.image (fun x : ((a : α) × Finset α) => (x.2, insert x.1 x.2)) Src) := by
991 rw [Finset.disjoint_left]
992 intro p hp1 hp2
993 rcases Finset.mem_image.mp hp1 with ⟨x, hx, rfl⟩
994 rcases Finset.mem_image.mp hp2 with ⟨y, hy, hxy⟩
995 rcases hmem_src x hx with ⟨_, hxq, _⟩
996 rcases hmem_src y hy with ⟨_, hyq, _⟩
997 have hxa : x.1 ∉ x.2 := by
998 intro h
999 exact Finset.notMem_erase x.1 A ((subset_of_mem_trace P hxq) h)
1000 have hya : y.1 ∉ y.2 := by
1001 intro h
1002 exact Finset.notMem_erase y.1 A ((subset_of_mem_trace P hyq) h)
1003 have h1 : y.2 = insert x.1 x.2 := Prod.mk.inj hxy |>.1
1004 have h2 : insert y.1 y.2 = x.2 := Prod.mk.inj hxy |>.2
1005 have hx1_not_insert : x.1 ∉ insert y.1 y.2 := by
1006 simpa [h2] using hxa
1007 have hx1_not_y2 : x.1 ∉ y.2 := by
1008 intro hx1_in_y2
1009 exact hx1_not_insert (by simp [hx1_in_y2])
1010 have hx1_in_y2 : x.1 ∈ y.2 := by
1011 rw [h1]
1012 simp
1013 exact hx1_not_y2 hx1_in_y2
1014 have hsubset :
1015 Finset.image (fun x : ((a : α) × Finset α) => (insert x.1 x.2, x.2)) Src ∪
1016 Finset.image (fun x : ((a : α) × Finset α) => (x.2, insert x.1 x.2)) Src ⊆ U := by
1017 intro p hp
1018 rcases Finset.mem_union.mp hp with hp | hp
1019 · rcases Finset.mem_image.mp hp with ⟨x, hx, rfl⟩
1020 exact himg1_mem x hx
1021 · rcases Finset.mem_image.mp hp with ⟨x, hx, rfl⟩
1022 exact himg2_mem x hx
1023 calc
1024 2 * A.sum (fun a => splitWeight P (A.erase a) a)
1025 = A.sum (fun a => splitWeight P (A.erase a) a) +
1026 A.sum (fun a => splitWeight P (A.erase a) a) := by ring
1027 _ = Src.sum (fun x =>
1028 min
1029 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∈ S)).card)
1030 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∉ S)).card)) +
1031 Src.sum (fun x =>
1032 min
1033 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∈ S)).card)
1034 ((P.filter (fun S => S ∩ (A.erase x.1) = x.2 ∧ x.1 ∉ S)).card)) := by
1035 rw [hsplit]
1036 _ = (Finset.image (fun x : ((a : α) × Finset α) => (insert x.1 x.2, x.2)) Src).sum wt +
1037 (Finset.image (fun x : ((a : α) × Finset α) => (x.2, insert x.1 x.2)) Src).sum wt := by
1038 rw [hsum_img1, hsum_img2]
1039 _ = (Finset.image (fun x : ((a : α) × Finset α) => (insert x.1 x.2, x.2)) Src ∪
1040 Finset.image (fun x : ((a : α) × Finset α) => (x.2, insert x.1 x.2)) Src).sum wt := by
1041 rw [Finset.sum_union hdisj]
1042 _ ≤ U.sum wt := by
1043 exact Finset.sum_le_sum_of_subset_of_nonneg hsubset (by intro p hp hpnot; exact Nat.zero_le _)
1044 -- Reindexing: Σ_A Σ_{a∈A} f(A\{a}, a) = Σ_{A'∈binom(s-1)} Σ_{a∉A'} f(A', a)
1045 have hreindex :
1046 ((Finset.univ : Finset α).powersetCard s).sum
1047 (fun A => A.sum (fun a => splitWeight P (A.erase a) a)) =
1048 ((Finset.univ : Finset α).powersetCard (s - 1)).sum
1049 (fun A' => (Finset.univ \ A').sum (fun a => splitWeight P A' a)) := by
1050 set S_s := (Finset.univ : Finset α).powersetCard s
1051 set S_s1 := (Finset.univ : Finset α).powersetCard (s - 1)
1052 -- Work with sigma-type sums; convert back via Finset.sum_sigma
1053 suffices h : ∑ x ∈ S_s.sigma (fun A => A),
1054 splitWeight P (x.1.erase x.2) x.2 =
1055 ∑ x ∈ S_s1.sigma (fun A' => Finset.univ \ A'),
1056 splitWeight P x.1 x.2 by
1057 rwa [Finset.sum_sigma, Finset.sum_sigma] at h
1058 apply Finset.sum_nbij (fun p => ⟨p.1.erase p.2, p.2⟩)
1059 · -- Maps into target
1060 intro ⟨A, a⟩ hmem
1061 simp only [Finset.mem_sigma] at hmem ⊢
1062 exact ⟨Finset.mem_powersetCard.mpr ⟨Finset.subset_univ _,
1063 by rw [Finset.card_erase_of_mem hmem.2,
1064 (Finset.mem_powersetCard.mp hmem.1).2]⟩,
1065 Finset.mem_sdiff.mpr ⟨Finset.mem_univ _, Finset.notMem_erase _ _⟩⟩
1066 · -- Injective
1067 intro ⟨A₁, a₁⟩ h₁ ⟨A₂, a₂⟩ h₂ heq
1068 simp only [Sigma.mk.inj_iff] at heq
1069 obtain ⟨h_fst, h_snd⟩ := heq
1070 have h_a : a₁ = a₂ := eq_of_heq h_snd
1071 subst h_a
1072 have ha₁ : a₁ ∈ A₁ := (Finset.mem_sigma.mp h₁).2
1073 have ha₂ : a₁ ∈ A₂ := (Finset.mem_sigma.mp h₂).2
1074 rw [← Finset.insert_erase ha₁, ← Finset.insert_erase ha₂, h_fst]
1075 · -- Surjective
1076 intro ⟨A', a⟩ hmem
1077 simp only [Finset.mem_coe, Finset.mem_sigma] at hmem
1078 have hA' := Finset.mem_powersetCard.mp hmem.1
1079 have ha := Finset.mem_sdiff.mp hmem.2
1080 refine ⟨⟨insert a A', a⟩,
1081 Finset.mem_coe.mpr (Finset.mem_sigma.mpr ⟨Finset.mem_powersetCard.mpr
1082 ⟨Finset.subset_univ _,
1083 by rw [Finset.card_insert_of_notMem ha.2, hA'.2]; omega⟩,
1084 Finset.mem_insert_self _ _⟩),
1085 ?_⟩
1086 simp only [Sigma.mk.inj_iff, heq_eq_eq, and_true]
1087 exact Finset.erase_insert ha.2
1088 · -- Function values match
1089 intro ⟨_, _⟩ _; rfl
1090 -- ── Combine sub-lemmas to get total lower bound on Σ W(A) ──
1091 set S := (Finset.univ : Finset α).powersetCard s with hS_def
1092 set S' := (Finset.univ : Finset α).powersetCard (s - 1) with hS'_def
1093 set sf := Catalog.VC.ShatterFunction.shatterFun F (s - 1) with hsf_def
1094 -- sf ≤ C·(s-1)^d and P.card > sf
1095 have hsf_le_C : (sf : ℝ) ≤ C * ((s : ℝ) - 1) ^ d := by
1096 calc (sf : ℝ) ≤ C * ((s - 1 : ℕ) : ℝ) ^ d := hπ (s - 1)
1097 _ = C * ((s : ℝ) - 1) ^ d := by
1098 congr 1; push_cast [Nat.cast_sub (by omega : 1 ≤ s)]; ring
1099 have hP_gt_sf : sf < P.card := by exact_mod_cast (hsf_le_C.trans_lt htriv)
1100 -- Each (s-1)-element A': twice the inner sum bounds δ·(P.card - sf)
1101 have hinner_bound : ∀ A' ∈ S',
1102 δ * (P.card - sf) ≤
1103 2 * (Finset.univ \ A').sum (fun a => splitWeight P A' a) := by
1104 intro A' hA'
1105 have hmem := Finset.mem_powersetCard.mp hA'
1106 calc δ * (P.card - sf)
1107 ≤ δ * (P.card - (Catalog.VC.ShatterFunction.trace P A').card) := by
1108 apply Nat.mul_le_mul_left
1109 apply Nat.sub_le_sub_left
1110 calc (Catalog.VC.ShatterFunction.trace P A').card
1111 ≤ Catalog.VC.ShatterFunction.shatterFun F A'.card := hA_lem A'
1112 _ = sf := by rw [hmem.2]
1113 _ ≤ _ := hC_lem A'
1114 -- Total over S': Σ_{A'∈S'} inner ≥ |S'|·δ·(P.card - sf)
1115 have htotal_S' : S'.card * (δ * (P.card - sf)) ≤
1116 S'.sum (fun A' => 2 * (Finset.univ \ A').sum (fun a => splitWeight P A' a)) := by
1117 calc S'.card * (δ * (P.card - sf))
1118 = S'.sum (fun _ => δ * (P.card - sf)) := by
1119 rw [Finset.sum_const, smul_eq_mul]
1120 _ ≤ _ := Finset.sum_le_sum hinner_bound
1121 -- Combine: Σ_A W(A) ≥ |S'|·δ·(P.card - sf) via D + reindex + C
1122 have hW_sum : S'.card * (δ * (P.card - sf)) ≤
1123 S.sum (fun A => weightedUDSum (Catalog.VC.ShatterFunction.trace P A)
1124 (traceWeight P A)) := by
1125 calc S'.card * (δ * (P.card - sf))
1126 ≤ S'.sum (fun A' => 2 * (Finset.univ \ A').sum (fun a => splitWeight P A' a)) :=
1127 htotal_S'
1128 _ = 2 * S'.sum (fun A' => (Finset.univ \ A').sum (fun a => splitWeight P A' a)) := by
1129 rw [← Finset.mul_sum]
1130 _ = 2 * S.sum (fun A => A.sum (fun a => splitWeight P (A.erase a) a)) := by
1131 rw [hreindex]
1132 _ ≤ S.sum (fun A => weightedUDSum (Catalog.VC.ShatterFunction.trace P A)
1133 (traceWeight P A)) := by
1134 rw [Finset.mul_sum]
1135 exact Finset.sum_le_sum (fun A _ => hD_lem A)
1136 -- ── Pigeonhole in ℕ: ∃ A ∈ S with S.card · W(A) ≥ total ──
1137 set L := S'.card * (δ * (P.card - sf)) with hL_def
1138 have hSne : S.Nonempty :=
1139 Finset.powersetCard_nonempty.mpr (by rwa [Finset.card_univ])
1140 have hS_pos : 0 < S.card := Finset.card_pos.mpr hSne
1141 -- Pigeonhole: if L ≤ Σ f and 0 < S.card, then ∃ A with L ≤ S.card * f(A)
1142 have hpigeonhole : ∃ A ∈ S, L ≤ S.card *
1143 weightedUDSum (Catalog.VC.ShatterFunction.trace P A) (traceWeight P A) := by
1144 by_contra h
1145 push_neg at h
1146 -- h : ∀ A ∈ S, S.card * W(A) < L
1147 have hlt : ∑ A ∈ S, S.card * weightedUDSum (Catalog.VC.ShatterFunction.trace P A)
1148 (traceWeight P A) < S.card * L := by
1149 calc ∑ A ∈ S, S.card * weightedUDSum (Catalog.VC.ShatterFunction.trace P A) (traceWeight P A)
1150 < ∑ _ ∈ S, L := Finset.sum_lt_sum_of_nonempty hSne h
1151 _ = S.card * L := by simp [Finset.sum_const, smul_eq_mul]
1152 rw [← Finset.mul_sum] at hlt
1153 linarith [Nat.mul_le_mul_left S.card hW_sum]
1154 obtain ⟨A, hA_mem, hA_bound⟩ := hpigeonhole
1155 have hAcard : A.card = s := (Finset.mem_powersetCard.mp hA_mem).2
1156 -- ── Cast to ℝ and simplify ──
1157 refine ⟨A, hAcard, ?_⟩
1158 -- The ℝ arithmetic: from L ≤ S.card * W(A), derive the desired ℝ bound
1159 -- L = C(n,s-1)·δ·(P.card-sf), S.card = C(n,s)
1160 -- W(A) ≥ L/S.card = s/(n-s+1)·δ·(P.card-sf) [choose identity]
1161 -- ≥ s·δ/n·(|P|-C·(s-1)^d)
1162 -- Let W_r be the real cast of the weighted UD sum
1163 set W_r : ℝ := ↑(weightedUDSum (Catalog.VC.ShatterFunction.trace P A) (traceWeight P A)) with hWr_def
1164 have hW_nn : (0 : ℝ) ≤ W_r := Nat.cast_nonneg _
1165 have hn_pos : (0 : ℝ) < n := by exact_mod_cast Nat.lt_of_lt_of_le hδ hδn
1166 -- S.card and S'.card as choose coefficients
1167 have hS_card : S.card = n.choose s := by
1168 simp [hS_def, Finset.card_powersetCard, Finset.card_univ, hn_def]
1169 have hS'_card : S'.card = n.choose (s - 1) := by
1170 simp [hS'_def, Finset.card_powersetCard, Finset.card_univ, hn_def]
1171 -- S'.card > 0 (since s-1 ≤ n)
1172 have hS'_pos : (0 : ℝ) < S'.card := by
1173 have : 0 < S'.card := by rw [hS'_card]; exact Nat.choose_pos (by omega)
1174 exact_mod_cast this
1175 -- Choose identity in ℕ: n.choose s * s = n.choose (s-1) * (n-s+1)
1176 have hident_N : n.choose s * s = n.choose (s - 1) * (n - s + 1) := by
1177 have h := Nat.choose_succ_right_eq n (s - 1)
1178 simp only [Nat.sub_add_cancel hs] at h
1179 have h2 : n - (s - 1) = n - s + 1 := by omega
1180 rw [h2] at h; exact h
1181 -- Cast identity to ℝ
1182 have hident : (S.card : ℝ) * ↑s = (S'.card : ℝ) * (↑n - ↑s + 1) := by
1183 rw [hS_card, hS'_card]
1184 have cast_rhs : ((n - s + 1 : ℕ) : ℝ) = (n : ℝ) - ↑s + 1 := by
1185 push_cast [Nat.cast_sub hsn]; ring
1186 rw [← cast_rhs]; exact_mod_cast hident_N
1187 -- Cast hA_bound to ℝ
1188 have hPsf : sf ≤ P.card := Nat.le_of_lt hP_gt_sf
1189 have hA_R : (L : ℝ) ≤ (S.card : ℝ) * W_r := by
1190 rw [hWr_def]; exact_mod_cast hA_bound
1191 -- Cast L to ℝ
1192 have hL_R : (L : ℝ) = ↑(S'.card) * ↑δ * (↑P.card - ↑sf) := by
1193 push_cast [hL_def, Nat.cast_sub hPsf]; ring
1194 -- Step 1: S'.card * δ * (P.card - sf) ≤ S.card * W_r
1195 have hstep1 : (S'.card : ℝ) * ↑δ * (↑P.card - ↑sf) ≤ (S.card : ℝ) * W_r := by
1196 linarith [hL_R ▸ hA_R]
1197 -- Step 2: S'.card * s * δ * (P.card-sf) ≤ S'.card * (n-s+1) * W_r
1198 have hstep2 : (S'.card : ℝ) * ↑s * ↑δ * (↑P.card - ↑sf) ≤
1199 (S'.card : ℝ) * (↑n - ↑s + 1) * W_r := by
1200 have h1 : ((S'.card : ℝ) * ↑δ * (↑P.card - ↑sf)) * ↑s ≤
1201 (S.card : ℝ) * W_r * ↑s :=
1202 mul_le_mul_of_nonneg_right hstep1 (Nat.cast_nonneg _)
1203 calc (S'.card : ℝ) * ↑s * ↑δ * (↑P.card - ↑sf)
1204 = ((S'.card : ℝ) * ↑δ * (↑P.card - ↑sf)) * ↑s := by ring
1205 _ ≤ (S.card : ℝ) * W_r * ↑s := h1
1206 _ = (S'.card : ℝ) * (↑n - ↑s + 1) * W_r := by linear_combination W_r * hident
1207 -- Step 3: divide by S'.card to get s*δ*(P.card-sf) ≤ (n-s+1)*W_r
1208 have hstep3 : (s : ℝ) * ↑δ * (↑P.card - ↑sf) ≤ (↑n - ↑s + 1) * W_r := by
1209 have key : (S'.card : ℝ) * (↑s * ↑δ * (↑P.card - ↑sf)) ≤
1210 (S'.card : ℝ) * ((↑n - ↑s + 1) * W_r) := by nlinarith [hstep2]
1211 exact le_of_mul_le_mul_left key hS'_pos
1212 -- Step 4: W_r * n ≥ s*δ*(P.card-sf) (since n ≥ n-s+1 and W_r ≥ 0)
1213 have hns_le_n : (↑n : ℝ) - ↑s + 1 ≤ ↑n := by
1214 linarith [show (1 : ℝ) ≤ ↑s from by exact_mod_cast hs]
1215 have hstep4 : (s : ℝ) * ↑δ * (↑P.card - ↑sf) ≤ W_r * ↑n := by
1216 nlinarith [hstep3]
1217 -- Step 5: compare `sf` with the polynomial bound
1218 have hsf_le2 : (↑P.card : ℝ) - C * (↑s - 1) ^ d ≤ ↑P.card - ↑sf := by linarith [hsf_le_C]
1219 have hPCnn : (0 : ℝ) ≤ ↑P.card - C * (↑s - 1) ^ d := by linarith [htriv.le]
1220 have hPsf_nn : (0 : ℝ) ≤ ↑P.card - ↑sf := by
1221 linarith [show (sf : ℝ) ≤ ↑P.card from by exact_mod_cast hPsf]
1222 have h_main : (s : ℝ) * ↑δ * (↑P.card - C * (↑s - 1) ^ d) ≤ W_r * ↑n := by
1223 have h1 : (s : ℝ) * ↑δ * (↑P.card - C * (↑s - 1) ^ d)
1224 ≤ (s : ℝ) * ↑δ * (↑P.card - ↑sf) :=
1225 mul_le_mul_of_nonneg_left hsf_le2 (by positivity)
1226 linarith [hstep4]
1227 -- Conclude: (s * δ / n * (P.card - C*(s-1)^d)) ≤ W_r
1228 have hrearrange :
1229 ↑s * ↑δ / ↑n * (↑P.card - C * (↑s - 1) ^ d) =
1230 ↑s * ↑δ * (↑P.card - C * (↑s - 1) ^ d) / ↑n := by ring
1231 rw [hrearrange]
1232 rw [div_le_iff₀ hn_pos]
1233 linarith [h_main]
1234
1235/-- **Upper bound on weighted UD sum**: for any `A`, the weighted UD sum on
1236 `trace P A` with trace weights is at most `4 · vcDim(P) · |P|`.
1237 Combines `greedy_peeling`, `trace_vcDim_le`, and `sum_traceWeight`. -/
1238private theorem upper_bound_weightedUDSum [Fintype α] (P : Finset (Finset α)) (A : Finset α) :
1239 (weightedUDSum (Catalog.VC.ShatterFunction.trace P A) (traceWeight P A) : ℝ) ≤
1240 4 * (P.vcDim : ℝ) * (P.card : ℝ) := by
1241 have h1 := greedy_peeling (Catalog.VC.ShatterFunction.trace P A) (traceWeight P A)
1242 have h2 := trace_vcDim_le P A
1243 have h3 := sum_traceWeight P A
1244 calc (weightedUDSum (Catalog.VC.ShatterFunction.trace P A) (traceWeight P A) : ℝ)
1245 ≤ ↑(4 * (Catalog.VC.ShatterFunction.trace P A).vcDim *
1246 (Catalog.VC.ShatterFunction.trace P A).sum (traceWeight P A)) := by exact_mod_cast h1
1247 _ = 4 * ↑(Catalog.VC.ShatterFunction.trace P A).vcDim *
1248 ↑((Catalog.VC.ShatterFunction.trace P A).sum (traceWeight P A)) := by push_cast; ring
1249 _ = 4 * ↑(Catalog.VC.ShatterFunction.trace P A).vcDim * ↑P.card := by rw [h3]
1250 _ ≤ 4 * ↑P.vcDim * ↑P.card := by gcongr
1251
1252/-- Core double-counting inequality: for any `s`-element sample `A`,
1253 the greedy-peeling upper bound on weighted edge sums and the
1254 double-counting lower bound combine to give
1255 `4 · vcDim · |P| ≥ (s · δ / n) · (|P| - C · (s-1)^d)`.
1256
1257 This encapsulates the full probabilistic/combinatorial argument
1258 (Matousek pp 156–159). Proved from `greedy_peeling`, `averaging_lower_bound`,
1259 and `upper_bound_weightedUDSum`. -/
1260private theorem combined_inequality [Fintype α] (d : ℕ) (C : ℝ) (hC : 0 < C)
1261 (F P : Finset (Finset α))
1262 (hPF : P ⊆ F)
1263 (hπ : ∀ m : ℕ, (Catalog.VC.ShatterFunction.shatterFun F m : ℝ) ≤ C * (m : ℝ) ^ d)
1264 (δ : ℕ) (hδ : 0 < δ) (hδn : δ ≤ Fintype.card α)
1265 (hsep : IsSeparated P δ) (hvc : 1 ≤ P.vcDim)
1266 (s : ℕ) (hs : 0 < s) (hsn : s ≤ Fintype.card α) :
1267 4 * (P.vcDim : ℝ) * (P.card : ℝ) ≥
1268 (s : ℝ) * (δ : ℝ) / (Fintype.card α : ℝ) *
1269 ((P.card : ℝ) - C * ((s : ℝ) - 1) ^ d) := by
1270 -- Obtain A witnessing the averaging lower bound
1271 obtain ⟨A, _, hlow⟩ := averaging_lower_bound d C hC F P hPF hπ δ hδ hδn hsep s hs hsn
1272 -- Upper bound holds for this A
1273 have hupp := upper_bound_weightedUDSum P A
1274 -- Combine: R ≤ W ≤ 4·vcDim·|P|, so R ≤ 4·vcDim·|P|
1275 linarith
1276
1277/-- Core packing bound: when `vcDim(P) ≥ 1`, the averaging argument gives
1278 `|P| ≤ 2C · (8 · vcDim P)^d · (n/δ)^d`.
1279 Proved by case split:
1280 - If `8 · vcDim ≤ δ`: apply `combined_inequality` with `s = ⌈8d₀n/δ⌉`
1281 - If `8 · vcDim > δ`: direct bound via `card_le_shatterFun` -/
1282private theorem core_packing_bound [Fintype α] (d : ℕ) (C : ℝ) (hC : 0 < C)
1283 (F P : Finset (Finset α))
1284 (hPF : P ⊆ F)
1285 (hπ : ∀ m : ℕ, (Catalog.VC.ShatterFunction.shatterFun F m : ℝ) ≤ C * (m : ℝ) ^ d)
1286 (δ : ℕ) (hδ : 0 < δ) (hδn : δ ≤ Fintype.card α)
1287 (hsep : IsSeparated P δ) (hvc : 1 ≤ P.vcDim) :
1288 (P.card : ℝ) ≤ 2 * C * ((8 : ℝ) * P.vcDim) ^ d *
1289 ((Fintype.card α : ℝ) / δ) ^ d := by
1290 set n := Fintype.card α with hn_def
1291 set d₀ := P.vcDim with hd₀_def
1292 have hn_pos : (0 : ℝ) < n := Nat.cast_pos.mpr (Nat.lt_of_lt_of_le hδ hδn)
1293 have hδR : (0 : ℝ) < (δ : ℝ) := Nat.cast_pos.mpr hδ
1294 have hd₀_pos : (0 : ℝ) < (d₀ : ℝ) := Nat.cast_pos.mpr (by omega : 0 < d₀)
1295 by_cases h4d : 8 * d₀ ≤ δ
1296 · -- Case 1: 8d₀ ≤ δ. Apply combined_inequality with s = ⌈8d₀n/δ⌉.
1297 set s := (8 * d₀ * n + (δ - 1)) / δ with hs_def
1298 -- ℕ ceiling division properties:
1299 have hsn : s ≤ n := by
1300 calc s ≤ (δ * n + (δ - 1)) / δ :=
1301 Nat.div_le_div_right (Nat.add_le_add_right (Nat.mul_le_mul_right n h4d) _)
1302 _ = n := by
1303 rw [show δ * n + (δ - 1) = (δ - 1) + n * δ from by ring,
1304 Nat.add_mul_div_right _ _ hδ,
1305 Nat.div_eq_of_lt (by omega : δ - 1 < δ), zero_add]
1306 have hs_pos : 0 < s := by
1307 apply Nat.div_pos _ hδ
1308 have : 0 < n := by omega
1309 calc δ ≤ 8 * d₀ * n := by nlinarith
1310 _ ≤ 8 * d₀ * n + (δ - 1) := Nat.le_add_right _ _
1311 have hsδ : 8 * d₀ * n ≤ s * δ := by
1312 have h := Nat.div_add_mod (8 * d₀ * n + (δ - 1)) δ
1313 rw [show δ * s = s * δ from mul_comm δ s] at h
1314 have hmod := Nat.mod_lt (8 * d₀ * n + (δ - 1)) hδ
1315 omega
1316 have hsδ_upper : s * δ ≤ 8 * d₀ * n + (δ - 1) :=
1317 show ((8 * d₀ * n + (δ - 1)) / δ) * δ ≤ _ from Nat.div_mul_le_self _ _
1318 -- Apply the combined inequality
1319 have hci := combined_inequality d C hC F P hPF hπ δ hδ hδn hsep hvc s hs_pos hsn
1320 -- sδ/n ≥ 8d₀ (from ceiling property)
1321 have h_sdn : 8 * (d₀ : ℝ) ≤ (s : ℝ) * δ / n := by
1322 rw [le_div_iff₀ hn_pos]; exact_mod_cast hsδ
1323 -- s - 1 ≤ 8d₀n/δ (from hsδ_upper: s*δ ≤ 8d₀n + δ - 1)
1324 have hs1 : (s : ℝ) - 1 ≤ 8 * d₀ * n / δ := by
1325 rw [sub_le_iff_le_add, div_add_one (ne_of_gt hδR), le_div_iff₀ hδR]
1326 have : (s * δ : ℕ) ≤ 8 * d₀ * n + δ :=
1327 Nat.le_trans hsδ_upper (Nat.add_le_add_left (Nat.sub_le δ 1) _)
1328 exact_mod_cast this
1329 -- Reduce to |P| ≤ 2C(s-1)^d via (s-1)^d ≤ (8d₀n/δ)^d = (8d₀)^d(n/δ)^d
1330 have hs1_nn : 0 ≤ (s : ℝ) - 1 := sub_nonneg.mpr (by exact_mod_cast hs_pos)
1331 suffices h_key : (P.card : ℝ) ≤ 2 * C * ((s : ℝ) - 1) ^ d by
1332 calc (P.card : ℝ) ≤ 2 * C * ((s : ℝ) - 1) ^ d := h_key
1333 _ ≤ 2 * C * (8 * ↑d₀ * ↑n / ↑δ) ^ d := by
1334 apply mul_le_mul_of_nonneg_left _ (by positivity)
1335 exact pow_le_pow_left₀ hs1_nn hs1 d
1336 _ = 2 * C * (8 * ↑d₀) ^ d * (↑n / ↑δ) ^ d := by
1337 rw [mul_div_assoc, mul_pow, ← mul_assoc]
1338 -- Prove |P| ≤ 2C(s-1)^d from the combined inequality + algebra
1339 -- From hci: 4d₀|P| ≥ (sδ/n)(|P| - C(s-1)^d)
1340 -- From h_sdn: sδ/n ≥ 8d₀
1341 set t := C * ((s : ℝ) - 1) ^ d
1342 have ht_nn : 0 ≤ t := mul_nonneg hC.le (pow_nonneg hs1_nn d)
1343 by_cases hp_le : (P.card : ℝ) ≤ t
1344 · linarith -- |P| ≤ t ≤ 2t
1345 · push_neg at hp_le
1346 have h1 : 0 < (P.card : ℝ) - t := by linarith
1347 have h2 : 8 * (d₀ : ℝ) * ((P.card : ℝ) - t) ≤
1348 (s : ℝ) * δ / n * ((P.card : ℝ) - t) :=
1349 mul_le_mul_of_nonneg_right h_sdn h1.le
1350 -- 4d₀|P| ≥ (sδ/n)(|P|-t) ≥ 8d₀(|P|-t), so 8d₀t ≥ 4d₀|P|, so 2t ≥ |P|
1351 nlinarith
1352 · -- Case 2: 8d₀ > δ. Direct bound: |P| ≤ C·n^d ≤ 2C(8d₀)^d(n/δ)^d
1353 push_neg at h4d
1354 have hPbound : (P.card : ℝ) ≤ C * n ^ d := by
1355 calc (P.card : ℝ) ≤ ↑(Catalog.VC.ShatterFunction.shatterFun F n) := card_le_shatterFun F P hPF
1356 _ ≤ C * n ^ d := hπ n
1357 -- n ≤ 8d₀ * n / δ since 1 ≤ 8d₀/δ
1358 have h_nd : (n : ℝ) ≤ 8 * d₀ * n / δ := by
1359 rw [le_div_iff₀ hδR]
1360 calc (n : ℝ) * δ = δ * n := by ring
1361 _ ≤ (8 * d₀) * n := by
1362 apply mul_le_mul_of_nonneg_right _ (by positivity)
1363 exact le_of_lt (by exact_mod_cast h4d)
1364 _ = 8 * d₀ * n := by ring
1365 calc (P.card : ℝ) ≤ C * n ^ d := hPbound
1366 _ ≤ C * (8 * d₀ * n / δ) ^ d := by gcongr
1367 _ = C * ((8 * ↑d₀) ^ d * (↑n / ↑δ) ^ d) := by rw [mul_div_assoc]; ring_nf
1368 _ ≤ 2 * C * (8 * ↑d₀) ^ d * (↑n / ↑δ) ^ d := by
1369 have hx : (0 : ℝ) ≤ (8 * ↑d₀) ^ d * (↑n / ↑δ) ^ d := by positivity
1370 nlinarith
1371
1372/-! ### Main theorem -/
1373
1374/-- **Packing lemma** (Matousek Lemma 5.14, Haussler's packing lemma).
1375 If the shatter function satisfies `π_𝒜(m) ≤ C · m^d` and `𝒫 ⊆ 𝒜` is
1376 `δ`-separated, then `|𝒫| ≤ C' · (n/δ)^d` where `C'` depends only on
1377 `C` and `d`. -/
1378theorem packingLemma (d : ℕ) (C : ℝ) (hC : 0 < C) : ∃ C' : ℝ, 0 < C' ∧
1379 ∀ (α : Type*) [DecidableEq α] [Fintype α] (F P : Finset (Finset α)),
1380 P ⊆ F →
1381 (∀ m : ℕ, (Catalog.VC.ShatterFunction.shatterFun F m : ℝ) ≤ C * (m : ℝ) ^ d) →
1382 ∀ (δ : ℕ), 0 < δ → δ ≤ Fintype.card α →
1383 IsSeparated P δ →
1384 (P.card : ℝ) ≤ C' * ((Fintype.card α : ℝ) / δ) ^ d := by
1385 -- Step 1: Bound vcDim by a universal constant K(C, d)
1386 obtain ⟨K, hK⟩ := vcDim_bounded d C hC
1387 -- Step 2: Choose C' = 2C(8K)^d + 1
1388 refine ⟨2 * C * ((8 : ℝ) * K) ^ d + 1, by positivity, ?_⟩
1389 intro α _ _ F P hPF hπ δ hδ hδn hsep
1390 have hd₀ := hK α F P hPF hπ
1391 by_cases hvc : P.vcDim = 0
1392 · -- Case vcDim = 0: P has at most 1 element
1393 have hP1 := vcDim_zero_card_le_one P hvc
1394 have hnd : (1 : ℝ) ≤ (Fintype.card α : ℝ) / (δ : ℝ) := by
1395 rw [le_div_iff₀ (Nat.cast_pos.mpr hδ)]
1396 simp only [one_mul]
1397 exact Nat.cast_le.mpr hδn
1398 have hpow : (1 : ℝ) ≤ ((Fintype.card α : ℝ) / δ) ^ d := by
1399 calc (1 : ℝ) = 1 ^ d := (one_pow d).symm
1400 _ ≤ ((Fintype.card α : ℝ) / δ) ^ d := by gcongr
1401 have hP1R : (P.card : ℝ) ≤ 1 := by exact_mod_cast hP1
1402 calc (P.card : ℝ) ≤ 1 := hP1R
1403 _ ≤ 1 * ((Fintype.card α : ℝ) / δ) ^ d := by linarith
1404 _ ≤ (2 * C * ((8 : ℝ) * K) ^ d + 1) *
1405 ((Fintype.card α : ℝ) / δ) ^ d := by
1406 apply mul_le_mul_of_nonneg_right _ (by positivity)
1407 have : 0 ≤ 2 * C * ((8 : ℝ) * K) ^ d := by positivity
1408 linarith
1409 · -- Case vcDim ≥ 1: apply the core averaging argument
1410 have hvc1 : 1 ≤ P.vcDim := Nat.one_le_iff_ne_zero.mpr hvc
1411 have hcore := core_packing_bound d C hC F P hPF hπ δ hδ hδn hsep hvc1
1412 have h_mono : ((8 : ℝ) * P.vcDim) ^ d ≤ ((8 : ℝ) * K) ^ d := by gcongr
1413 have h_nonneg : (0 : ℝ) ≤ ((Fintype.card α : ℝ) / δ) ^ d := by positivity
1414 have h_Cpos : 0 < 2 * C := by positivity
1415 calc (P.card : ℝ)
1416 ≤ 2 * C * ((8 : ℝ) * P.vcDim) ^ d *
1417 ((Fintype.card α : ℝ) / δ) ^ d := hcore
1418 _ ≤ 2 * C * ((8 : ℝ) * K) ^ d *
1419 ((Fintype.card α : ℝ) / δ) ^ d := by
1420 apply mul_le_mul_of_nonneg_right _ h_nonneg
1421 exact mul_le_mul_of_nonneg_left h_mono h_Cpos.le
1422 _ ≤ (2 * C * ((8 : ℝ) * K) ^ d + 1) *
1423 ((Fintype.card α : ℝ) / δ) ^ d := by
1424 have : 0 ≤ 1 * ((Fintype.card α : ℝ) / δ) ^ d := by positivity
1425 linarith [mul_nonneg (by positivity : (0:ℝ) ≤ 1) h_nonneg]
1426
1427end Catalog.VC.PackingLemma
1428