Formalizing Structural Graph Theory in Lean 4

Catalog/VC/UnitDistanceGraphEdges/Full.lean
1import Catalog.VC.VCDimension.Full
2import Mathlib.Order.SymmDiff
3import Mathlib.Tactic
4
5namespace Catalog.VC.UnitDistanceGraphEdges
6
7variable {α : Type*} [DecidableEq α] [Fintype α]
8
9private def shadow (a : α) (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
10 𝒜.filter (fun S => a ∉ S ∧ insert a S ∈ 𝒜)
11
12omit [Fintype α] in
13private theorem shadow_eq_inter (a : α) (𝒜 : Finset (Finset α)) :
14 shadow a 𝒜 = 𝒜.memberSubfamily a ∩ 𝒜.nonMemberSubfamily a := by
15 ext S
16 simp only [shadow, Finset.mem_filter, Finset.mem_inter,
17 Finset.mem_memberSubfamily, Finset.mem_nonMemberSubfamily]
18 tauto
19
20omit [Fintype α] in
21private theorem card_eq (a : α) (𝒜 : Finset (Finset α)) :
22 𝒜.card = (𝒜.image (·.erase a)).card + (shadow a 𝒜).card := by
23 rw [shadow_eq_inter, ← Finset.memberSubfamily_union_nonMemberSubfamily a 𝒜]
24 have h1 := Finset.card_union_add_card_inter (𝒜.memberSubfamily a) (𝒜.nonMemberSubfamily a)
25 have h2 := Finset.card_memberSubfamily_add_card_nonMemberSubfamily a 𝒜
26 omega
27
28omit [Fintype α] in
29private theorem vcDim_eraseImage_le (a : α) (𝒜 : Finset (Finset α)) :
30 (𝒜.image (·.erase a)).vcDim ≤ 𝒜.vcDim := by
31 simp only [Finset.vcDim]
32 apply Finset.sup_le
33 intro T hT
34 rw [Finset.mem_shatterer] at hT
35 have ha : a ∉ T := by
36 obtain ⟨S', hS', hTS'⟩ := hT Finset.Subset.rfl
37 rw [Finset.mem_image] at hS'
38 obtain ⟨S, _, rfl⟩ := hS'
39 exact fun haT => Finset.notMem_erase a S (Finset.inter_eq_left.mp hTS' haT)
40 have : 𝒜.Shatters T := by
41 intro U hU
42 obtain ⟨S', hS', hTS'⟩ := hT hU
43 rw [Finset.mem_image] at hS'
44 obtain ⟨S, hS, rfl⟩ := hS'
45 refine ⟨S, hS, ?_⟩
46 have : T ∩ S = T ∩ S.erase a := by
47 ext x; simp only [Finset.mem_inter, Finset.mem_erase]
48 exact ⟨fun ⟨hxT, hxS⟩ => ⟨hxT, ne_of_mem_of_not_mem hxT ha, hxS⟩,
49 fun ⟨hxT, _, hxS⟩ => ⟨hxT, hxS⟩⟩
50 rw [this]; exact hTS'
51 exact this.card_le_vcDim
52
53omit [Fintype α] in
54private theorem vcDim_shadow_succ_le (a : α) (𝒜 : Finset (Finset α))
55 (hne : (shadow a 𝒜).Nonempty) :
56 (shadow a 𝒜).vcDim + 1 ≤ 𝒜.vcDim := by
57 -- Shadow membership: a ∉ S and insert a S ∈ 𝒜
58 have hmem : ∀ S ∈ shadow a 𝒜, a ∉ S ∧ insert a S ∈ 𝒜 :=
59 fun S hS => (Finset.mem_filter.mp hS).2
60 have hsub_fam : shadow a 𝒜 ⊆ 𝒜 := fun S hS => (Finset.mem_filter.mp hS).1
61 -- If shadow shatters T, then a ∉ T
62 have ha_not : ∀ T, (shadow a 𝒜).Shatters T → a ∉ T := by
63 intro T hT haT
64 obtain ⟨S, hS, hle⟩ := hT.exists_superset
65 exact (hmem S hS).1 (hle haT)
66 -- Key: shadow shatters T → 𝒜 shatters (insert a T)
67 have lift : ∀ T, (shadow a 𝒜).Shatters T → 𝒜.Shatters (insert a T) := by
68 intro T hT V hV
69 by_cases haV : a ∈ V
70 · -- a ∈ V: witness is insert a S where T ∩ S = V \ {a}
71 have hVe : V.erase a ⊆ T := fun x hx => by
72 rw [Finset.mem_erase] at hx
73 exact (Finset.mem_insert.mp (hV hx.2)).resolve_left hx.1
74 obtain ⟨S, hS, hTS⟩ := hT hVe
75 exact ⟨insert a S, (hmem S hS).2, by
76 rw [← Finset.insert_inter_distrib, hTS, Finset.insert_erase haV]⟩
77 · -- a ∉ V: witness is S itself
78 have hVT : V ⊆ T := fun x hx =>
79 (Finset.mem_insert.mp (hV hx)).resolve_left (fun h => haV (h ▸ hx))
80 obtain ⟨S, hS, hTS⟩ := hT hVT
81 exact ⟨S, hsub_fam hS, by
82 rw [Finset.insert_inter_of_notMem (hmem S hS).1, hTS]⟩
83 -- Get T achieving shadow.vcDim
84 have hne' : (shadow a 𝒜).shatterer.Nonempty :=
85 ⟨∅, Finset.mem_shatterer.mpr (Finset.shatters_empty.mpr hne)⟩
86 obtain ⟨T, hT_mem, hT_max⟩ := (shadow a 𝒜).shatterer.exists_max_image Finset.card hne'
87 rw [Finset.mem_shatterer] at hT_mem
88 have hT_eq : (shadow a 𝒜).vcDim = T.card := by
89 unfold Finset.vcDim
90 exact le_antisymm (Finset.sup_le fun S hS => hT_max S hS)
91 (Finset.le_sup (Finset.mem_shatterer.mpr hT_mem))
92 calc (shadow a 𝒜).vcDim + 1 = T.card + 1 := by rw [hT_eq]
93 _ = (insert a T).card := (Finset.card_insert_of_notMem (ha_not T hT_mem)).symm
94 _ ≤ 𝒜.vcDim := (lift T hT_mem).card_le_vcDim
95
96omit [Fintype α] in
97private theorem support_eraseImage (a : α) (𝒜 : Finset (Finset α)) (X : Finset α)
98 (hsub : ∀ S ∈ 𝒜, S ⊆ X) :
99 ∀ S ∈ 𝒜.image (·.erase a), S ⊆ X.erase a := by
100 intro S hS x hx
101 rw [Finset.mem_image] at hS
102 obtain ⟨T, hT, rfl⟩ := hS
103 rw [Finset.mem_erase] at hx ⊢
104 exact ⟨hx.1, hsub T hT hx.2⟩
105
106omit [Fintype α] in
107private theorem support_shadow (a : α) (𝒜 : Finset (Finset α)) (X : Finset α)
108 (hsub : ∀ S ∈ 𝒜, S ⊆ X) :
109 ∀ S ∈ shadow a 𝒜, S ⊆ X.erase a := by
110 intro S hS x hx
111 rw [shadow, Finset.mem_filter] at hS
112 rw [Finset.mem_erase]
113 exact ⟨fun h => hS.2.1 (h ▸ hx), hsub S hS.1 hx⟩
114
115-- Inclusion-exclusion for filtered offDiag
116omit [Fintype α] in
117private lemma offDiag_filter_ie (M NM : Finset (Finset α)) :
118 (M.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card +
119 (NM.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card ≤
120 ((M ∪ NM).offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card +
121 ((M ∩ NM).offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card := by
122 set F := fun p : Finset α × Finset α => (symmDiff p.1 p.2).card = 1
123 have h := Finset.card_union_add_card_inter (M.offDiag.filter F) (NM.offDiag.filter F)
124 have hsub : M.offDiag.filter F ∪ NM.offDiag.filter F ⊆
125 (M ∪ NM).offDiag.filter F := by
126 rw [← Finset.filter_union]
127 exact Finset.filter_subset_filter _
128 (Finset.union_subset (Finset.offDiag_mono Finset.subset_union_left)
129 (Finset.offDiag_mono Finset.subset_union_right))
130 rw [← Finset.filter_inter_distrib, ← Finset.offDiag_inter] at h
131 change (M.offDiag.filter F).card + (NM.offDiag.filter F).card ≤
132 ((M ∪ NM).offDiag.filter F).card + ((M ∩ NM).offDiag.filter F).card
133 linarith [Finset.card_le_card hsub]
134
135-- symmDiff is preserved by erase when a is in both sets
136private lemma symmDiff_erase_of_mem (S S' : Finset α) (a : α)
137 (hS : a ∈ S) (hS' : a ∈ S') :
138 symmDiff (S.erase a) (S'.erase a) = symmDiff S S' := by
139 have ha_not : a ∉ symmDiff S S' := by
140 intro h
141 have := symmDiff_def S S' ▸ h
142 rcases Finset.mem_union.mp this with h | h
143 · exact (Finset.mem_sdiff.mp h).2 hS'
144 · exact (Finset.mem_sdiff.mp h).2 hS
145 simp only [← Finset.sdiff_singleton_eq_erase]
146 calc symmDiff (S \ {a}) (S' \ {a})
147 = symmDiff ({a}ᶜ ⊓ S) ({a}ᶜ ⊓ S') := by congr 1 <;> rw [sdiff_eq, inf_comm]
148 _ = {a}ᶜ ⊓ symmDiff S S' := (inf_symmDiff_distrib_left _ _ _).symm
149 _ = symmDiff S S' ⊓ {a}ᶜ := inf_comm _ _
150 _ = symmDiff S S' \ {a} := sdiff_eq.symm
151 _ = symmDiff S S' := by
152 rw [Finset.sdiff_singleton_eq_erase, Finset.erase_eq_of_notMem ha_not]
153
154private theorem udPairs_bound (a : α) (𝒜 : Finset (Finset α)) :
155 (𝒜.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card ≤
156 2 * (shadow a 𝒜).card +
157 ((𝒜.image (·.erase a)).offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card +
158 ((shadow a 𝒜).offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card := by
159 set M := 𝒜.memberSubfamily a
160 set NM := 𝒜.nonMemberSubfamily a
161 -- Reduce to: udP(𝒜) ≤ 2|Sh| + udP(M) + udP(NM) via inclusion-exclusion
162 suffices key : (𝒜.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card ≤
163 2 * (shadow a 𝒜).card +
164 (M.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card +
165 (NM.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card by
166 have h_ie := offDiag_filter_ie M NM
167 have h1 : M ∪ NM = 𝒜.image (·.erase a) :=
168 Finset.memberSubfamily_union_nonMemberSubfamily a 𝒜
169 have h2 : M ∩ NM = shadow a 𝒜 := (shadow_eq_inter a 𝒜).symm
170 rw [h1, h2] at h_ie
171 linarith
172 -- Prove key: udP(𝒜) ≤ 2|Sh| + udP(M) + udP(NM)
173 -- Partition pairs by membership of a
174 set Ap := 𝒜.filter (a ∈ ·)
175 -- 𝒜 = Ap ∪ NM
176 have h𝒜_split : 𝒜 = Ap ∪ NM := by
177 ext S
178 simp only [Finset.mem_union, Ap, Finset.mem_filter, NM, Finset.mem_nonMemberSubfamily]
179 tauto
180 -- Ap and NM are disjoint
181 have h_disj : Disjoint Ap NM := by
182 rw [Finset.disjoint_left]
183 intro S hS hS'
184 exact (Finset.mem_nonMemberSubfamily.mp hS').2 (Finset.mem_filter.mp hS).2
185 -- Helper: if a ∈ S, a ∉ T, |S △ T| = 1, then T = S.erase a
186 have hT_det : ∀ S T : Finset α, a ∈ S → a ∉ T →
187 (symmDiff S T).card = 1 → T = S.erase a := by
188 intro S T haS haT hsd
189 have h_sd : symmDiff S T = {a} := by
190 rw [Finset.card_eq_one] at hsd
191 obtain ⟨b, hb⟩ := hsd
192 have : a ∈ symmDiff S T := by
193 rw [symmDiff_def, Finset.sup_eq_union, Finset.mem_union, Finset.mem_sdiff]
194 left; exact ⟨haS, haT⟩
195 rw [hb, Finset.mem_singleton] at this; rw [hb, this]
196 calc T = symmDiff S (symmDiff S T) := (symmDiff_symmDiff_cancel_left S T).symm
197 _ = symmDiff S {a} := by rw [h_sd]
198 _ = S.erase a := by
199 ext x; simp [symmDiff_def, Finset.sup_eq_union, Finset.mem_union, Finset.mem_sdiff,
200 Finset.mem_erase, Finset.mem_singleton]
201 constructor
202 · rintro (⟨hx, h⟩ | ⟨rfl, _⟩) <;> [exact ⟨h, hx⟩; exact absurd haS ‹_›]
203 · rintro ⟨hxa, hxS⟩; left; exact ⟨hxS, fun h => hxa h⟩
204 -- BOUND 1: cross pairs ≤ 2|Sh|
205 -- Map (S, T) ↦ T sends Ap×NM cross pairs to shadow, injectively (S = insert a T)
206 have h_cross : ((Ap ×ˢ NM).filter (fun p => (symmDiff p.1 p.2).card = 1)).card ≤
207 (shadow a 𝒜).card := by
208 have h_to_sh : ∀ p ∈ (Ap ×ˢ NM).filter (fun p => (symmDiff p.1 p.2).card = 1),
209 Prod.snd p ∈ shadow a 𝒜 := by
210 intro ⟨S, T⟩ hp
211 simp only [Finset.mem_filter, Finset.mem_product] at hp
212 obtain ⟨⟨hSap, hT_nm⟩, hsd⟩ := hp
213 have haS := (Finset.mem_filter.mp hSap).2
214 have haT := (Finset.mem_nonMemberSubfamily.mp hT_nm).2
215 rw [shadow, Finset.mem_filter]
216 refine ⟨(Finset.mem_nonMemberSubfamily.mp hT_nm).1, haT, ?_⟩
217 rw [hT_det S T haS haT hsd, Finset.insert_erase haS]
218 exact (Finset.mem_filter.mp hSap).1
219 have h_inj : Set.InjOn (Prod.snd : Finset α × Finset α → Finset α)
220 ((Ap ×ˢ NM).filter (fun p => (symmDiff p.1 p.2).card = 1)) := by
221 intro ⟨S₁, T₁⟩ h₁ ⟨S₂, T₂⟩ h₂ (heq : T₁ = T₂)
222 simp only [Finset.mem_coe, Finset.mem_filter, Finset.mem_product] at h₁ h₂
223 have haS₁ := (Finset.mem_filter.mp h₁.1.1).2
224 have haT₁ := (Finset.mem_nonMemberSubfamily.mp h₁.1.2).2
225 have haS₂ := (Finset.mem_filter.mp h₂.1.1).2
226 have haT₂ := (Finset.mem_nonMemberSubfamily.mp h₂.1.2).2
227 have : S₁ = S₂ := by
228 calc S₁ = insert a (S₁.erase a) := (Finset.insert_erase haS₁).symm
229 _ = insert a T₁ := by rw [← hT_det S₁ T₁ haS₁ haT₁ h₁.2]
230 _ = insert a T₂ := by rw [heq]
231 _ = insert a (S₂.erase a) := by rw [hT_det S₂ T₂ haS₂ haT₂ h₂.2]
232 _ = S₂ := Finset.insert_erase haS₂
233 exact Prod.ext this heq
234 exact le_trans (Finset.card_image_of_injOn h_inj).symm.le
235 (Finset.card_le_card (Finset.image_subset_iff.mpr h_to_sh))
236 -- Similarly for cross in the other direction (NM × Ap)
237 have h_cross' : ((NM ×ˢ Ap).filter (fun p => (symmDiff p.1 p.2).card = 1)).card ≤
238 (shadow a 𝒜).card := by
239 have h_to_sh : ∀ p ∈ (NM ×ˢ Ap).filter (fun p => (symmDiff p.1 p.2).card = 1),
240 Prod.fst p ∈ shadow a 𝒜 := by
241 intro ⟨T, S⟩ hp
242 simp only [Finset.mem_filter, Finset.mem_product] at hp
243 obtain ⟨⟨hT_nm, hSap⟩, hsd⟩ := hp
244 have haS := (Finset.mem_filter.mp hSap).2
245 have haT := (Finset.mem_nonMemberSubfamily.mp hT_nm).2
246 rw [shadow, Finset.mem_filter]
247 refine ⟨(Finset.mem_nonMemberSubfamily.mp hT_nm).1, haT, ?_⟩
248 rw [hT_det S T haS haT (symmDiff_comm T S ▸ hsd), Finset.insert_erase haS]
249 exact (Finset.mem_filter.mp hSap).1
250 have h_inj : Set.InjOn (Prod.fst : Finset α × Finset α → Finset α)
251 ((NM ×ˢ Ap).filter (fun p => (symmDiff p.1 p.2).card = 1)) := by
252 intro ⟨T₁, S₁⟩ h₁ ⟨T₂, S₂⟩ h₂ (heq : T₁ = T₂)
253 simp only [Finset.mem_coe, Finset.mem_filter, Finset.mem_product] at h₁ h₂
254 have haS₁ := (Finset.mem_filter.mp h₁.1.2).2
255 have haT₁ := (Finset.mem_nonMemberSubfamily.mp h₁.1.1).2
256 have haS₂ := (Finset.mem_filter.mp h₂.1.2).2
257 have haT₂ := (Finset.mem_nonMemberSubfamily.mp h₂.1.1).2
258 have : S₁ = S₂ := by
259 calc S₁ = insert a (S₁.erase a) := (Finset.insert_erase haS₁).symm
260 _ = insert a T₁ := by rw [← hT_det S₁ T₁ haS₁ haT₁ (symmDiff_comm T₁ S₁ ▸ h₁.2)]
261 _ = insert a T₂ := by rw [heq]
262 _ = insert a (S₂.erase a) := by
263 rw [hT_det S₂ T₂ haS₂ haT₂ (symmDiff_comm T₂ S₂ ▸ h₂.2)]
264 _ = S₂ := Finset.insert_erase haS₂
265 exact Prod.ext heq this
266 exact le_trans (Finset.card_image_of_injOn h_inj).symm.le
267 (Finset.card_le_card (Finset.image_subset_iff.mpr h_to_sh))
268 -- BOUND 2: udP(Ap) ≤ udP(M) via erase-a injection
269 have h_erase : (Ap.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card ≤
270 (M.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card := by
271 -- Map (S, S') ↦ (S.erase a, S'.erase a) is injective into M.offDiag.filter P
272 let φ := fun p : Finset α × Finset α => (p.1.erase a, p.2.erase a)
273 have h_inj : Set.InjOn φ (Ap.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)) := by
274 intro ⟨S₁, S₁'⟩ h₁ ⟨S₂, S₂'⟩ h₂ heq
275 simp only [Finset.mem_coe, Finset.mem_filter, Finset.mem_offDiag] at h₁ h₂
276 have ha₁ : a ∈ S₁ := (Finset.mem_filter.mp h₁.1.1).2
277 have ha₁' : a ∈ S₁' := (Finset.mem_filter.mp h₁.1.2.1).2
278 have ha₂ : a ∈ S₂ := (Finset.mem_filter.mp h₂.1.1).2
279 have ha₂' : a ∈ S₂' := (Finset.mem_filter.mp h₂.1.2.1).2
280 have heq1 : S₁.erase a = S₂.erase a := congr_arg Prod.fst heq
281 have heq2 : S₁'.erase a = S₂'.erase a := congr_arg Prod.snd heq
282 exact Prod.ext
283 (calc S₁ = insert a (S₁.erase a) := (Finset.insert_erase ha₁).symm
284 _ = insert a (S₂.erase a) := by rw [heq1]
285 _ = S₂ := Finset.insert_erase ha₂)
286 (calc S₁' = insert a (S₁'.erase a) := (Finset.insert_erase ha₁').symm
287 _ = insert a (S₂'.erase a) := by rw [heq2]
288 _ = S₂' := Finset.insert_erase ha₂')
289 have h_maps : (Ap.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).image φ ⊆
290 M.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1) := by
291 intro p hp
292 rw [Finset.mem_image] at hp
293 obtain ⟨⟨S, S'⟩, hSS', rfl⟩ := hp
294 show (S.erase a, S'.erase a) ∈ M.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)
295 simp only [Finset.mem_filter, Finset.mem_offDiag] at hSS'
296 have haS : a ∈ S := (Finset.mem_filter.mp hSS'.1.1).2
297 have haS' : a ∈ S' := (Finset.mem_filter.mp hSS'.1.2.1).2
298 refine Finset.mem_filter.mpr ⟨Finset.mem_offDiag.mpr ⟨?_, ?_, ?_⟩, ?_⟩
299 · exact Finset.mem_memberSubfamily.mpr
300 ⟨by rw [Finset.insert_erase haS]; exact (Finset.mem_filter.mp hSS'.1.1).1,
301 Finset.notMem_erase a S⟩
302 · exact Finset.mem_memberSubfamily.mpr
303 ⟨by rw [Finset.insert_erase haS']; exact (Finset.mem_filter.mp hSS'.1.2.1).1,
304 Finset.notMem_erase a S'⟩
305 · intro heq
306 change S.erase a = S'.erase a at heq
307 exact hSS'.1.2.2 (by
308 calc S = insert a (S.erase a) := (Finset.insert_erase haS).symm
309 _ = insert a (S'.erase a) := by rw [heq]
310 _ = S' := Finset.insert_erase haS')
311 · rw [symmDiff_erase_of_mem S S' a haS haS']; exact hSS'.2
312 exact le_trans (Finset.card_image_of_injOn h_inj).symm.le
313 (Finset.card_le_card h_maps)
314 -- COMBINE: udP(𝒜) ≤ cross + cross' + udP(NM) + udP(Ap) ≤ 2|Sh| + udP(NM) + udP(M)
315 -- Need: 𝒜.offDiag.filter P ⊆ (Ap ×ˢ NM ∪ NM ×ˢ Ap).filter P ∪ NM.offDiag.filter P ∪ Ap.offDiag.filter P
316 have h_decomp : 𝒜.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1) ⊆
317 (Ap ×ˢ NM ∪ NM ×ˢ Ap).filter (fun p => (symmDiff p.1 p.2).card = 1) ∪
318 NM.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1) ∪
319 Ap.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1) := by
320 intro ⟨S, T⟩ hp
321 simp only [Finset.mem_filter, Finset.mem_offDiag, Finset.mem_union,
322 Finset.mem_product] at hp ⊢
323 obtain ⟨⟨hS, hT, hne⟩, hsd⟩ := hp
324 by_cases haS : a ∈ S <;> by_cases haT : a ∈ T
325 · -- a ∈ S, a ∈ T: internal to Ap
326 right; exact ⟨⟨Finset.mem_filter.mpr ⟨hS, haS⟩,
327 Finset.mem_filter.mpr ⟨hT, haT⟩, hne⟩, hsd⟩
328 · -- a ∈ S, a ∉ T: cross Ap × NM
329 left; left
330 exact ⟨Or.inl ⟨Finset.mem_filter.mpr ⟨hS, haS⟩,
331 Finset.mem_nonMemberSubfamily.mpr ⟨hT, haT⟩⟩, hsd⟩
332 · -- a ∉ S, a ∈ T: cross NM × Ap
333 left; left
334 exact ⟨Or.inr ⟨Finset.mem_nonMemberSubfamily.mpr ⟨hS, haS⟩,
335 Finset.mem_filter.mpr ⟨hT, haT⟩⟩, hsd⟩
336 · -- a ∉ S, a ∉ T: internal to NM
337 left; right
338 exact ⟨⟨Finset.mem_nonMemberSubfamily.mpr ⟨hS, haS⟩,
339 Finset.mem_nonMemberSubfamily.mpr ⟨hT, haT⟩, hne⟩, hsd⟩
340 -- Final combination
341 have hfu : ((Ap ×ˢ NM ∪ NM ×ˢ Ap).filter (fun p => (symmDiff p.1 p.2).card = 1)).card ≤
342 ((Ap ×ˢ NM).filter (fun p => (symmDiff p.1 p.2).card = 1)).card +
343 ((NM ×ˢ Ap).filter (fun p => (symmDiff p.1 p.2).card = 1)).card := by
344 rw [Finset.filter_union]; exact Finset.card_union_le _ _
345 linarith [Finset.card_le_card h_decomp,
346 Finset.card_union_le
347 ((Ap ×ˢ NM ∪ NM ×ˢ Ap).filter (fun p => (symmDiff p.1 p.2).card = 1) ∪
348 NM.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1))
349 (Ap.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)),
350 Finset.card_union_le
351 ((Ap ×ˢ NM ∪ NM ×ˢ Ap).filter (fun p => (symmDiff p.1 p.2).card = 1))
352 (NM.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)),
353 hfu, h_cross, h_cross', h_erase]
354
355theorem unitDistEdgeBound (𝒜 : Finset (Finset α)) :
356 (𝒜.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card
357 ≤ 2 * 𝒜.vcDim * 𝒜.card := by
358 suffices h : ∀ (X : Finset α) (𝒜 : Finset (Finset α)),
359 (∀ S ∈ 𝒜, S ⊆ X) →
360 (𝒜.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card
361 ≤ 2 * 𝒜.vcDim * 𝒜.card from
362 h Finset.univ 𝒜 (fun S _ => Finset.subset_univ S)
363 exact Finset.strongInduction fun X ih 𝒜 hsub => by
364 rcases X.eq_empty_or_nonempty with rfl | ⟨a, haX⟩
365 · -- Base: X = ∅ → |𝒜| ≤ 1 → no pairs
366 have h𝒜 : 𝒜 ⊆ {∅} := fun S hS =>
367 Finset.mem_singleton.mpr (Finset.subset_empty.mp (hsub S hS))
368 have hcard : 𝒜.card ≤ 1 :=
369 (Finset.card_le_card h𝒜).trans (Finset.card_singleton ∅).le
370 have : 𝒜.offDiag = ∅ := by
371 rw [← Finset.card_eq_zero, Finset.offDiag_card]
372 rcases Nat.le_one_iff_eq_zero_or_eq_one.mp hcard with h | h <;> simp [h]
373 simp [this]
374 · -- Step: pick a ∈ X
375 have hXea := Finset.erase_ssubset haX
376 have ih₁ := ih _ hXea _ (support_eraseImage a 𝒜 X hsub)
377 have ihSh := ih _ hXea _ (support_shadow a 𝒜 X hsub)
378 have hcharge := udPairs_bound a 𝒜
379 have hcard := card_eq a 𝒜
380 have hvc₁ := vcDim_eraseImage_le a 𝒜
381 rcases (shadow a 𝒜).eq_empty_or_nonempty with hShe | hShne
382 · -- Shadow empty: 2|Sh| = 0 and UD(Sh) = 0
383 have hSh0 : (shadow a 𝒜).card = 0 := Finset.card_eq_zero.mpr hShe
384 have hSh_off : ((shadow a 𝒜).offDiag.filter
385 (fun p => (symmDiff p.1 p.2).card = 1)).card = 0 := by simp [hShe]
386 have h1 := Nat.mul_le_mul_right (𝒜.image (·.erase a)).card
387 (Nat.mul_le_mul_left 2 hvc₁)
388 nlinarith [hcharge, ih₁]
389 · -- Shadow nonempty: vcDim(Sh) + 1 ≤ d
390 have hvc₂ := vcDim_shadow_succ_le a 𝒜 hShne
391 have h1 := Nat.mul_le_mul_right (𝒜.image (·.erase a)).card
392 (Nat.mul_le_mul_left 2 hvc₁)
393 have h2 := Nat.mul_le_mul_right (shadow a 𝒜).card
394 (Nat.mul_le_mul_left 2 hvc₂)
395 have h3 : 2 * 𝒜.vcDim * 𝒜.card =
396 2 * 𝒜.vcDim * (𝒜.image (·.erase a)).card +
397 2 * 𝒜.vcDim * (shadow a 𝒜).card := by rw [hcard]; ring
398 nlinarith [hcharge, ih₁, ihSh]
399
400end Catalog.VC.UnitDistanceGraphEdges
401