English
Let G be a simple graph on a finite vertex set V with an equipartition P and assume G is uniform with respect to the parts of P up to the error ε/8, and that the partition has at least 4/ε parts. Let G_reg be the regularity-reduced graph obtained from G with parameters (ε/8, ε/4). Then the number of edges removed by passing from G to G_reg is bounded by a multiple of ε times |V|^2; specifically, 2(|E(G)| − |E(G_reg)|) < 2ε|V|^2.
Русский
Пусть G — простый граф на конечном множество вершин V. Пусть P — равноправная разбиение вершин, и граф G является равномерным по частям разбиения с ошибкой ε/8. Пусть число частей разбиения удовлетворяет 4/ε ≤ |P|. Обозначим G_reg как редуцированный граф поREG(P, ε/8, ε/4). Тогда число ребер, удалённых при переходе от G к G_reg, удовлетворяет границе: 2(|E(G)| − |E(G_reg)|) < 2ε|V|^2.
LaTeX
$$$2\\bigl(|E(G)| - |E(G)_{\\mathrm{reg}}|\\bigr) < 2\\varepsilon\\, (|V|)^2,$ where $|E(G)_{\\mathrm{reg}}|$ denotes the edge-set size of the regularity-reduced graph $G_{\\mathrm{reg}} = G.regularityReduced(P, \\varepsilon/8, \\varepsilon/4)$.$$
Lean4
theorem regularityReduced_edges_card_aux [Nonempty α] (hε : 0 < ε) (hP : P.IsEquipartition)
(hPε : P.IsUniform G (ε / 8)) (hP' : 4 / ε ≤ #P.parts) :
2 * (#G.edgeFinset - #(G.regularityReduced P (ε / 8) (ε / 4)).edgeFinset : ℝ) < 2 * ε * (card α ^ 2 : ℕ) :=
by
let A := (P.nonUniforms G (ε / 8)).biUnion fun (U, V) ↦ U ×ˢ V
let B := P.parts.biUnion offDiag
let C := (P.sparsePairs G (ε / 4)).biUnion fun (U, V) ↦ G.interedges U V
calc
_ = (#((univ ×ˢ univ).filter fun (x, y) ↦ G.Adj x y ∧ ¬(G.regularityReduced P (ε / 8) (ε / 4)).Adj x y) : ℝ) :=
by
rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff]
· norm_cast
rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]
· exact monotone_filter_right _ fun xy hxy ↦ regularityReduced_le hxy
_ ≤ #(A ∪ B ∪ C) := by gcongr; exact unreduced_edges_subset
_ ≤ #(A ∪ B) + #C := (mod_cast (card_union_le _ _))
_ ≤ #A + #B + #C := by gcongr; exact mod_cast card_union_le _ _
_ < 4 * (ε / 8) * card α ^ 2 + _ + _ := by gcongr; exact hP.sum_nonUniforms_lt univ_nonempty (by positivity) hPε
_ ≤ _ + ε / 2 * card α ^ 2 + 4 * (ε / 4) * card α ^ 2 :=
by
gcongr
· exact hP.card_biUnion_offDiag_le hε hP'
· exact hP.card_interedges_sparsePairs_le (G := G) (ε := ε / 4) (by positivity)
_ = 2 * ε * (card α ^ 2 : ℕ) := by norm_cast; ring
