Formalizing Structural Graph Theory in Lean 4

Catalog/VC/ShortEdgeLemma/Full.lean
1import Catalog.VC.DualShatterFunction.Full
2import Catalog.VC.PackingLemma.Full
3import Catalog.VC.ShatterFunction.Full
4import Mathlib.Analysis.SpecialFunctions.Pow.Real
5import Mathlib.Data.Finset.Card
6
7namespace Catalog.VC.ShortEdgeLemma
8
9universe u
10
11section
12
13variable {α : Type*} [DecidableEq α]
14
15/-- The crossing number of an edge `{x, y}` by a subfamily `Q`: the number
16 of sets in `Q` that contain exactly one of `x, y`. -/
17abbrev crossingNumber (Q : Finset (Finset α)) (x y : α) : ℕ :=
18 (Q.filter (fun S => (x ∈ S ∧ y ∉ S) ∨ (x ∉ S ∧ y ∈ S))).card
19
20private lemma symmDiff_atomMap_card_eq_crossingNumber
21 (Q : Finset (Finset α)) (x y : α) :
22 (symmDiff (Catalog.VC.DualShatterFunction.atomMap Q x)
23 (Catalog.VC.DualShatterFunction.atomMap Q y)).card = crossingNumber Q x y := by
24 unfold Catalog.VC.DualShatterFunction.atomMap crossingNumber
25 congr
26 ext S
27 by_cases hS : S ∈ Q
28 · simp [hS, Finset.mem_symmDiff, and_comm]
29 · simp [hS, Finset.mem_symmDiff]
30
31private lemma exists_atomMap_collision [Fintype α] (Q : Finset (Finset α))
32 (hcard : (Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap Q)).card < Fintype.card α) :
33 ∃ x y : α, x ≠ y ∧
34 Catalog.VC.DualShatterFunction.atomMap Q x = Catalog.VC.DualShatterFunction.atomMap Q y := by
35 simpa using
36 (Finset.exists_ne_map_eq_of_card_image_lt (s := (Finset.univ : Finset α))
37 (f := Catalog.VC.DualShatterFunction.atomMap Q) hcard)
38
39private lemma crossingNumber_eq_zero_of_atomMap_eq
40 (Q : Finset (Finset α)) {x y : α}
41 (hxy : Catalog.VC.DualShatterFunction.atomMap Q x = Catalog.VC.DualShatterFunction.atomMap Q y) :
42 crossingNumber Q x y = 0 := by
43 rw [← symmDiff_atomMap_card_eq_crossingNumber]
44 rw [hxy]
45 simp
46
47private def atomMapOn (Q : Finset (Finset α)) (x : α) :
48 Finset {S // S ∈ Q} :=
49 Q.attach.filter (fun S => x ∈ S.1)
50
51private lemma image_val_atomMapOn (Q : Finset (Finset α)) (x : α) :
52 (atomMapOn Q x).image Subtype.val = Catalog.VC.DualShatterFunction.atomMap Q x := by
53 ext S
54 simp [atomMapOn, Catalog.VC.DualShatterFunction.atomMap, and_comm]
55
56private lemma atomMapOn_eq_iff (Q : Finset (Finset α)) {x y : α} :
57 atomMapOn Q x = atomMapOn Q y ↔
58 Catalog.VC.DualShatterFunction.atomMap Q x = Catalog.VC.DualShatterFunction.atomMap Q y := by
59 constructor
60 · intro h
61 simpa [image_val_atomMapOn] using congrArg (fun T => T.image Subtype.val) h
62 · intro h
63 ext S
64 have hmem := congrArg (fun T => S.1 ∈ T) h
65 simp [Catalog.VC.DualShatterFunction.atomMap] at hmem
66 simpa [atomMapOn] using hmem
67
68private lemma atomMapOn_inter_image_val
69 (Q : Finset (Finset α)) (Y : Finset {S // S ∈ Q}) (x : α) :
70 ((atomMapOn Q x ∩ Y).image Subtype.val) =
71 Catalog.VC.DualShatterFunction.atomMap (Y.image Subtype.val) x := by
72 ext S
73 simp [atomMapOn, Catalog.VC.DualShatterFunction.atomMap, and_comm]
74
75private lemma image_val_injective (Q : Finset (Finset α)) :
76 Function.Injective (fun T : Finset {S // S ∈ Q} => T.image Subtype.val) := by
77 intro T₁ T₂ h
78 ext S
79 constructor
80 · intro hS
81 have hmem₁ : S.1 ∈ T₁.image Subtype.val := Finset.mem_image.mpr ⟨S, hS, rfl⟩
82 have hmem : S.1 ∈ T₂.image Subtype.val := by simpa [h] using hmem₁
83 rcases Finset.mem_image.mp hmem with ⟨S', hS', hEq⟩
84 exact Subtype.val_injective hEq ▸ hS'
85 · intro hS
86 have hmem₂ : S.1 ∈ T₂.image Subtype.val := Finset.mem_image.mpr ⟨S, hS, rfl⟩
87 have hmem : S.1 ∈ T₁.image Subtype.val := by simpa [h] using hmem₂
88 rcases Finset.mem_image.mp hmem with ⟨S', hS', hEq⟩
89 exact Subtype.val_injective hEq ▸ hS'
90
91private lemma dualFamilyOn_card_eq [Fintype α] (Q : Finset (Finset α)) :
92 (Finset.univ.image (atomMapOn Q)).card =
93 (Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap Q)).card := by
94 let e : Finset {S // S ∈ Q} → Finset (Finset α) := fun T => T.image Subtype.val
95 have hEq :
96 (Finset.univ.image (atomMapOn Q)).image e =
97 Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap Q) := by
98 ext T
99 simp only [e, Finset.mem_image]
100 constructor
101 · rintro ⟨U, hU, rfl⟩
102 rcases hU with ⟨x, -, rfl⟩
103 exact ⟨x, Finset.mem_univ _, (image_val_atomMapOn Q x).symm⟩
104 · rintro ⟨x, -, hT⟩
105 exact ⟨atomMapOn Q x, ⟨x, Finset.mem_univ _, rfl⟩, by simpa [e] using (image_val_atomMapOn Q x).trans hT⟩
106 calc
107 (Finset.univ.image (atomMapOn Q)).card
108 = ((Finset.univ.image (atomMapOn Q)).image e).card := by
109 symm
110 exact Finset.card_image_of_injective _ (image_val_injective Q)
111 _ = (Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap Q)).card := by rw [hEq]
112
113private lemma atomMapOn_sep_card_eq_crossingNumber
114 (Q : Finset (Finset α)) (x y : α) :
115 ((atomMapOn Q x \ atomMapOn Q y) ∪ (atomMapOn Q y \ atomMapOn Q x)).card =
116 crossingNumber Q x y := by
117 have hEq :
118 (((atomMapOn Q x \ atomMapOn Q y) ∪ (atomMapOn Q y \ atomMapOn Q x)).image Subtype.val) =
119 symmDiff (Catalog.VC.DualShatterFunction.atomMap Q x) (Catalog.VC.DualShatterFunction.atomMap Q y) := by
120 ext S
121 by_cases hS : S ∈ Q
122 · simp [hS, atomMapOn, Catalog.VC.DualShatterFunction.atomMap, Finset.mem_symmDiff, and_comm]
123 · simp [hS, atomMapOn, Catalog.VC.DualShatterFunction.atomMap, Finset.mem_symmDiff]
124 calc
125 ((atomMapOn Q x \ atomMapOn Q y) ∪ (atomMapOn Q y \ atomMapOn Q x)).card
126 = ((((atomMapOn Q x \ atomMapOn Q y) ∪ (atomMapOn Q y \ atomMapOn Q x)).image
127 Subtype.val)).card := by
128 symm
129 exact Finset.card_image_of_injective _ Subtype.val_injective
130 _ = (symmDiff (Catalog.VC.DualShatterFunction.atomMap Q x)
131 (Catalog.VC.DualShatterFunction.atomMap Q y)).card := by rw [hEq]
132 _ = crossingNumber Q x y := symmDiff_atomMap_card_eq_crossingNumber Q x y
133
134private lemma crossingNumber_le_card (Q : Finset (Finset α)) (x y : α) :
135 crossingNumber Q x y ≤ Q.card := by
136 unfold crossingNumber
137 exact Finset.card_filter_le _ _
138
139private theorem le_floor_double {x : ℝ} (hx : 1 ≤ x) :
140 x ≤ Nat.floor (2 * x) := by
141 have hlt : 2 * x < Nat.floor (2 * x) + 1 := Nat.lt_floor_add_one (2 * x)
142 have hx2 : x ≤ 2 * x - 1 := by linarith
143 have hle : 2 * x - 1 < Nat.floor (2 * x) := by linarith
144 linarith
145
146private lemma card_image_atomMap_le_dualShatterFun
147 [Fintype α] (𝒜 Q : Finset (Finset α)) (hQ : Q ⊆ 𝒜) :
148 (Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap Q)).card ≤
149 Catalog.VC.DualShatterFunction.dualShatterFun 𝒜 Q.card := by
150 unfold Catalog.VC.DualShatterFunction.dualShatterFun
151 exact Finset.le_sup (f := fun 𝒴 => (Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap 𝒴)).card)
152 (Finset.mem_filter.mpr ⟨Finset.mem_powerset.mpr hQ, rfl⟩)
153
154private lemma trace_dualFamily_card_le_dualShatterFun
155 [Fintype α] (𝒜 Q : Finset (Finset α)) (hQ : Q ⊆ 𝒜)
156 (Y : Finset {S // S ∈ Q}) :
157 (Catalog.VC.ShatterFunction.trace (Finset.univ.image (atomMapOn Q)) Y).card ≤
158 Catalog.VC.DualShatterFunction.dualShatterFun 𝒜 Y.card := by
159 let e : Finset {S // S ∈ Q} → Finset (Finset α) := fun T => T.image Subtype.val
160 have he_inj : Function.Injective e := image_val_injective Q
161 have hYsub : Y.image Subtype.val ⊆ 𝒜 := by
162 intro S hS
163 rcases Finset.mem_image.mp hS with ⟨T, hT, rfl⟩
164 exact hQ T.2
165 have hYcard : (Y.image Subtype.val).card = Y.card := by
166 rw [Finset.card_image_of_injective _ Subtype.val_injective]
167 calc
168 (Catalog.VC.ShatterFunction.trace (Finset.univ.image (atomMapOn Q)) Y).card
169 = ((Catalog.VC.ShatterFunction.trace (Finset.univ.image (atomMapOn Q)) Y).image e).card := by
170 symm
171 exact Finset.card_image_of_injective _ he_inj
172 _ ≤ (Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap (Y.image Subtype.val))).card := by
173 apply Finset.card_le_card
174 intro T hT
175 rcases Finset.mem_image.mp hT with ⟨U, hU, rfl⟩
176 simp only [Catalog.VC.ShatterFunction.trace, Finset.mem_image] at hU
177 rcases hU with ⟨A, hA, rfl⟩
178 rcases hA with ⟨x, -, rfl⟩
179 exact Finset.mem_image.mpr ⟨x, Finset.mem_univ _, (atomMapOn_inter_image_val Q Y x).symm⟩
180 _ ≤ Catalog.VC.DualShatterFunction.dualShatterFun 𝒜 Y.card := by
181 rw [← hYcard]
182 exact card_image_atomMap_le_dualShatterFun 𝒜 (Y.image Subtype.val) hYsub
183
184end
185
186/-- Short edge lemma: if the dual shatter function satisfies
187 `π*_𝒜(m) ≤ C · m^d` with `d > 1`, then for any subfamily `Q ⊆ 𝒜`
188 there exist distinct points `x, y` with crossing number at most
189 `C₂ · |Q| / n^{1/d}`. (Lemma 5.18) -/
190theorem shortEdgeLemma (d : ℕ) (C : ℝ) (hd : 1 < d) (hC : 0 < C) :
191 ∃ C₂ : ℝ, 0 < C₂ ∧
192 ∀ (α : Type u) [DecidableEq α] [Fintype α] (𝒜 : Finset (Finset α)),
193 (∀ m : ℕ, (Catalog.VC.DualShatterFunction.dualShatterFun 𝒜 m : ℝ) ≤ C * (m : ℝ) ^ d) →
194 2 ≤ Fintype.card α →
195 ∀ (Q : Finset (Finset α)), Q ⊆ 𝒜 →
196 ∃ x y : α, x ≠ y ∧
197 ((Q.filter (fun S => (x ∈ S ∧ y ∉ S) ∨ (x ∉ S ∧ y ∈ S))).card : ℝ) ≤
198 C₂ * (Q.card : ℝ) /
199 (Fintype.card α : ℝ) ^ ((1 : ℝ) / d) := by
200 obtain ⟨C', hC'pos, hpack⟩ := Catalog.VC.PackingLemma.packingLemma d C hC
201 let A : ℝ := C + 2 * C' + 2
202 refine ⟨2 * A, by positivity, ?_⟩
203 intro α _ _ 𝒜 hdual hn Q hQ
204 change ∃ x y : α, x ≠ y ∧
205 (crossingNumber Q x y : ℝ) ≤ (2 * A) * (Q.card : ℝ) /
206 (Fintype.card α : ℝ) ^ ((1 : ℝ) / d)
207 by_cases hlt : (Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap Q)).card < Fintype.card α
208 · obtain ⟨x, y, hxy, hatom⟩ := exists_atomMap_collision Q hlt
209 refine ⟨x, y, hxy, ?_⟩
210 rw [crossingNumber_eq_zero_of_atomMap_eq Q hatom]
211 have hnonneg :
212 0 ≤ (2 * A) * (Q.card : ℝ) / (Fintype.card α : ℝ) ^ ((1 : ℝ) / d) := by
213 positivity
214 linarith
215 · have himg_ge : Fintype.card α ≤
216 (Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap Q)).card := by
217 exact Nat.le_of_not_lt hlt
218 have himg_le : (Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap Q)).card ≤
219 Fintype.card α := Finset.card_image_le
220 have himg_eq : (Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap Q)).card =
221 Fintype.card α := le_antisymm himg_le himg_ge
222 let nroot : ℝ := (Fintype.card α : ℝ) ^ ((1 : ℝ) / d)
223 let R : ℝ := (2 * A) * (Q.card : ℝ) / nroot
224 by_cases hRbig : (Q.card : ℝ) ≤ R
225 · have huniv : 1 < (Finset.univ : Finset α).card := by simpa using hn
226 obtain ⟨x, hx, y, hy, hxy⟩ := Finset.one_lt_card.mp huniv
227 refine ⟨x, y, hxy, ?_⟩
228 have hcross : (crossingNumber Q x y : ℝ) ≤ Q.card := by
229 exact_mod_cast crossingNumber_le_card Q x y
230 calc
231 (crossingNumber Q x y : ℝ) ≤ Q.card := hcross
232 _ ≤ R := hRbig
233 _ = (2 * A) * (Q.card : ℝ) / nroot := rfl
234 · by_contra hshort
235 push_neg at hshort
236 let P : Finset (Finset {S // S ∈ Q}) := Finset.univ.image (atomMapOn Q)
237 let δ : ℕ := Nat.floor R
238 have hPcard : P.card = Fintype.card α := by
239 simp [P, dualFamilyOn_card_eq, himg_eq]
240 have hαle : (Fintype.card α : ℝ) ≤ C * (Q.card : ℝ) ^ d := by
241 calc
242 (Fintype.card α : ℝ)
243 = ((Finset.univ.image (Catalog.VC.DualShatterFunction.atomMap Q)).card : ℝ) := by
244 norm_num [himg_eq]
245 _ ≤ Catalog.VC.DualShatterFunction.dualShatterFun 𝒜 Q.card := by
246 exact_mod_cast card_image_atomMap_le_dualShatterFun 𝒜 Q hQ
247 _ ≤ C * (Q.card : ℝ) ^ d := hdual Q.card
248 have hAone : 1 ≤ A := by
249 dsimp [A]
250 linarith
251 have hAle : C ≤ A := by
252 dsimp [A]
253 linarith
254 have hQnonneg : 0 ≤ (Q.card : ℝ) ^ d := by positivity
255 have hApow : A ≤ A ^ d := by
256 exact le_self_pow₀ hAone (by omega)
257 have hnroot_pos : 0 < nroot := by
258 dsimp [nroot]
259 positivity
260 have hRlt : R < (Q.card : ℝ) := lt_of_not_ge hRbig
261 have hnroot_le : nroot ≤ A * (Q.card : ℝ) := by
262 have hpow :
263 (Fintype.card α : ℝ) ≤ (A * (Q.card : ℝ)) ^ d := by
264 calc
265 (Fintype.card α : ℝ) ≤ C * (Q.card : ℝ) ^ d := hαle
266 _ ≤ A * (Q.card : ℝ) ^ d := by gcongr
267 _ ≤ A ^ d * (Q.card : ℝ) ^ d := by
268 gcongr
269 _ = (A * (Q.card : ℝ)) ^ d := by rw [mul_pow]
270 have hroot :=
271 Real.rpow_le_rpow (by positivity : 0 ≤ (Fintype.card α : ℝ)) hpow
272 (by positivity : (0 : ℝ) ≤ (1 : ℝ) / d)
273 calc
274 nroot = (Fintype.card α : ℝ) ^ ((1 : ℝ) / d) := rfl
275 _ ≤ ((A * (Q.card : ℝ)) ^ d) ^ ((1 : ℝ) / d) := hroot
276 _ = A * (Q.card : ℝ) := by
277 calc
278 ((A * (Q.card : ℝ)) ^ d) ^ ((1 : ℝ) / d)
279 = (A * (Q.card : ℝ)) ^ ((d : ℝ) * ((1 : ℝ) / d)) := by
280 simpa [Real.rpow_natCast] using
281 (Real.rpow_mul (by positivity : 0 ≤ A * (Q.card : ℝ))
282 (d : ℝ) ((1 : ℝ) / d)).symm
283 _ = (A * (Q.card : ℝ)) ^ (1 : ℝ) := by
284 field_simp [show (d : ℝ) ≠ 0 by exact_mod_cast (show (d : ℕ) ≠ 0 by omega)]
285 _ = A * (Q.card : ℝ) := by simp
286 have hxone : 1 ≤ A * (Q.card : ℝ) / nroot := by
287 rw [le_div_iff₀ hnroot_pos]
288 simpa [mul_comm] using hnroot_le
289 have hδge : A * (Q.card : ℝ) / nroot ≤ δ := by
290 have hfloor := le_floor_double hxone
291 have hR_eq : 2 * (A * (Q.card : ℝ) / nroot) = R := by
292 dsimp [R]
293 ring
294 simpa [δ, hR_eq] using hfloor
295 have hδpos : 0 < δ := by
296 have hδge1 : (1 : ℝ) ≤ δ := le_trans hxone hδge
297 exact_mod_cast hδge1
298 have hδleQ : δ ≤ Q.card := by
299 have hδleR : (δ : ℝ) ≤ R := Nat.floor_le (by positivity : 0 ≤ R)
300 have hδltQ : (δ : ℝ) < Q.card := by linarith
301 exact_mod_cast hδltQ.le
302 have hsep : Catalog.VC.PackingLemma.IsSeparated P δ := by
303 intro S hS S' hS' hSS'
304 rcases Finset.mem_image.mp hS with ⟨x, -, rfl⟩
305 rcases Finset.mem_image.mp hS' with ⟨y, -, rfl⟩
306 have hxy : x ≠ y := by
307 intro hxy
308 apply hSS'
309 simp [hxy]
310 have hltcross :
311 R < (crossingNumber Q x y : ℝ) := by
312 have hnot : ¬ ((crossingNumber Q x y : ℝ) ≤ R) := by
313 simpa [R, nroot] using hshort x y hxy
314 exact lt_of_not_ge hnot
315 have hδltcross : (δ : ℝ) < (crossingNumber Q x y : ℝ) := by
316 have hδleR : (δ : ℝ) ≤ R := Nat.floor_le (by positivity : 0 ≤ R)
317 linarith
318 have hδltcross_nat : δ < crossingNumber Q x y := by
319 exact_mod_cast hδltcross
320 simpa [P, atomMapOn_sep_card_eq_crossingNumber] using hδltcross_nat
321 have hshatter : ∀ m : ℕ, (Catalog.VC.ShatterFunction.shatterFun P m : ℝ) ≤ C * (m : ℝ) ^ d := by
322 intro m
323 have hsf : Catalog.VC.ShatterFunction.shatterFun P m ≤ Catalog.VC.DualShatterFunction.dualShatterFun 𝒜 m := by
324 unfold Catalog.VC.ShatterFunction.shatterFun
325 refine Finset.sup_le ?_
326 intro Y hY
327 have hYm : Y.card = m := by
328 simpa using (Finset.mem_filter.mp hY).2
329 calc
330 (Catalog.VC.ShatterFunction.trace P Y).card ≤ Catalog.VC.DualShatterFunction.dualShatterFun 𝒜 Y.card :=
331 trace_dualFamily_card_le_dualShatterFun 𝒜 Q hQ Y
332 _ = Catalog.VC.DualShatterFunction.dualShatterFun 𝒜 m := by rw [hYm]
333 have hsf' : (Catalog.VC.ShatterFunction.shatterFun P m : ℝ) ≤ Catalog.VC.DualShatterFunction.dualShatterFun 𝒜 m := by
334 exact_mod_cast hsf
335 exact hsf'.trans (hdual m)
336 have hpack_bound :=
337 hpack {S // S ∈ Q} P P (by intro T hT; exact hT) hshatter δ hδpos
338 (by simpa [Fintype.card_coe] using hδleQ) hsep
339 have hpack_bound' : (Fintype.card α : ℝ) ≤ C' * ((Q.card : ℝ) / δ) ^ d := by
340 simpa [P, hPcard, Fintype.card_coe] using hpack_bound
341 have hq_div : (Q.card : ℝ) / δ ≤ nroot / A := by
342 have hδpos' : (0 : ℝ) < δ := by exact_mod_cast hδpos
343 have hApos : 0 < A := by linarith
344 have hδge' : A * (Q.card : ℝ) ≤ δ * nroot := by
345 have htemp := hδge
346 rw [div_le_iff₀ hnroot_pos] at htemp
347 simpa [mul_comm, mul_left_comm, mul_assoc] using htemp
348 field_simp [hApos.ne', hδpos'.ne']
349 nlinarith [hδge']
350 have hpow_div : ((Q.card : ℝ) / δ) ^ d ≤ (nroot / A) ^ d := by
351 gcongr
352 have hpack_bound'' : (Fintype.card α : ℝ) ≤ C' * (nroot / A) ^ d := by
353 exact le_trans hpack_bound' (by gcongr)
354 have hnroot_pow : nroot ^ d = Fintype.card α := by
355 calc
356 nroot ^ d = nroot ^ (d : ℝ) := by rw [Real.rpow_natCast]
357 _ = (Fintype.card α : ℝ) ^ (((1 : ℝ) / d) * d) := by
358 dsimp [nroot]
359 rw [Real.rpow_mul (by positivity : 0 ≤ (Fintype.card α : ℝ))]
360 _ = (Fintype.card α : ℝ) ^ (1 : ℝ) := by
361 field_simp [show (d : ℝ) ≠ 0 by exact_mod_cast (show (d : ℕ) ≠ 0 by omega)]
362 _ = Fintype.card α := by simp
363 have hratio : (nroot / A) ^ d = (Fintype.card α : ℝ) / A ^ d := by
364 rw [div_pow, hnroot_pow]
365 have hC'ltA : C' < A := by
366 dsimp [A]
367 linarith
368 have hC'ltApow : C' < A ^ d := lt_of_lt_of_le hC'ltA hApow
369 have hαpos : 0 < (Fintype.card α : ℝ) := by
370 exact_mod_cast (lt_of_lt_of_le (by decide : 0 < 2) hn)
371 have hfinal_lt : C' * (nroot / A) ^ d < (Fintype.card α : ℝ) := by
372 rw [hratio]
373 have hApow_pos : 0 < A ^ d := by positivity
374 have hfrac_lt_one : C' / A ^ d < 1 := by
375 rw [div_lt_iff₀ hApow_pos]
376 simpa using hC'ltApow
377 have hmul := mul_lt_mul_of_pos_right hfrac_lt_one hαpos
378 have hrewrite : C' * ((Fintype.card α : ℝ) / A ^ d) = (C' / A ^ d) * (Fintype.card α : ℝ) := by
379 field_simp
380 rw [hrewrite]
381 simpa [one_mul] using hmul
382 exact (not_lt_of_ge hpack_bound'') hfinal_lt
383
384end Catalog.VC.ShortEdgeLemma
385