card_interedges_sparsePairs_le — Mathlib

English

For an equipartition P, the total number of interedges between sparse pairs is bounded by a linear function of |A| and |P.parts|, with a factor depending on ε.

Русский

Для равноправного разбиения P общее число межкраев между разреженными парами ограничено линейной функцией от |A| и |P.parts| с коэффициентом, зависящим от ε.

LaTeX

$$#((P.sparsePairs G ε).biUnion (fun (U, V) ↦ G.interedges U V)).card.cast ≤ ε * (#A + #P.parts) ^ 2$$

Lean4

theorem card_interedges_sparsePairs_le (hP : P.IsEquipartition) (hε : 0 ≤ ε) :
    #((P.sparsePairs G ε).biUnion fun (U, V) ↦ G.interedges U V) ≤ 4 * ε * #A ^ 2 := by
  calc
    _ ≤ _ := hP.card_interedges_sparsePairs_le' hε
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring

Похожие утверждения