English
A strengthened bound on the offDiag part for equipartitions with explicit constants.
Русский
Усиленная граница для offDiag при равноправных разбиениях с явными константами.
LaTeX
$$P.IsEquipartition → (ε ≥ 0) → (4 / ε ≤ #P.parts) → #(P.parts.biUnion offDiag) ≤ (ε / 2) * #A ^ 2$$
Lean4
theorem unreduced_edges_subset :
(A ×ˢ A).filter (fun (x, y) ↦ G.Adj x y ∧ ¬(G.regularityReduced P (ε / 8) (ε / 4)).Adj x y) ⊆
(P.nonUniforms G (ε / 8)).biUnion (fun (U, V) ↦ U ×ˢ V) ∪ P.parts.biUnion offDiag ∪
(P.sparsePairs G (ε / 4)).biUnion fun (U, V) ↦ G.interedges U V :=
by
rintro ⟨x, y⟩
simp only [mem_filter, regularityReduced_adj, not_and, not_exists, not_le, mem_biUnion, mem_union, mem_product,
Prod.exists, mem_offDiag, and_imp, or_assoc, and_assoc, P.mk_mem_nonUniforms, Finpartition.mk_mem_sparsePairs,
mem_interedges_iff]
intro hx hy h h'
replace h' := h' h
obtain ⟨U, hU, hx⟩ := P.exists_mem hx
obtain ⟨V, hV, hy⟩ := P.exists_mem hy
obtain rfl | hUV := eq_or_ne U V
· exact Or.inr (Or.inl ⟨U, hU, hx, hy, G.ne_of_adj h⟩)
by_cases h₂ : G.IsUniform (ε / 8) U V
· exact Or.inr <| Or.inr ⟨U, V, hU, hV, hUV, h' _ hU _ hV hx hy hUV h₂, hx, hy, h⟩
· exact Or.inl ⟨U, V, hU, hV, hUV, h₂, hx, hy⟩
