English
For an equipartition P, the total number of interedges across sparse pairs is bounded by ε times (#A + #P.parts) squared.
Русский
Для равноправного разбиения 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) ≤ ε * (#A + #P.parts) ^ 2 :=
by
calc
_ ≤ ∑ UV ∈ P.sparsePairs G ε, (#(G.interedges UV.1 UV.2) : 𝕜) := mod_cast card_biUnion_le
_ ≤ ∑ UV ∈ P.sparsePairs G ε, ε * (#UV.1 * #UV.2) := ?_
_ ≤ ∑ UV ∈ P.parts.offDiag, ε * (#UV.1 * #UV.2) := by gcongr; apply filter_subset
_ = ε * ∑ UV ∈ P.parts.offDiag, (#UV.1 * #UV.2 : 𝕜) := (mul_sum _ _ _).symm
_ ≤ _ := ?_
· gcongr with UV hUV
obtain ⟨U, V⟩ := UV
simp [mk_mem_sparsePairs, ← card_interedges_div_card] at hUV
refine ((div_lt_iff₀ ?_).1 hUV.2.2.2).le
exact
mul_pos (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.1).card_pos)
(Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.2.1).card_pos)
norm_cast
gcongr
calc
(_ : ℕ) ≤ _ := sum_le_card_nsmul P.parts.offDiag (fun i ↦ #i.1 * #i.2) ((#A / #P.parts + 1) ^ 2 : ℕ) ?_
_ ≤ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2 := ?_
_ ≤ _ := by gcongr; apply Nat.mul_div_le
· simp only [Prod.forall, and_imp, mem_offDiag, sq]
rintro U V hU hV -
exact_mod_cast Nat.mul_le_mul (hP.card_part_le_average_add_one hU) (hP.card_part_le_average_add_one hV)
· rw [smul_eq_mul, offDiag_card, Nat.mul_sub_right_distrib, ← sq, ← mul_pow, mul_add_one (α := ℕ)]
exact Nat.sub_le _ _
