English
If ε > 0 and P is an equipartition with sufficient parts, then the offDiag union size is bounded by (ε/4) times a quadratic expression in |A| and |P.parts|.
Русский
Если ε > 0 и P является равноправным разбиением с достаточным числом частей, то размер объединения offDiag ограничен (ε/4) умножить на квадратичную функцию от |A| и |P.parts|.
LaTeX
$$ (P.IsEquipartition) ∧ (ε > 0) ∧ (4 / ε ≤ #P.parts) → #(P.parts.biUnion offDiag) ≤ ε / 2 * #A ^ 2$$
Lean4
theorem card_biUnion_offDiag_le (hε : 0 < ε) (hP : P.IsEquipartition) (hP' : 4 / ε ≤ #P.parts) :
#(P.parts.biUnion offDiag) ≤ ε / 2 * #A ^ 2 :=
by
obtain rfl | hA : A = ⊥ ∨ _ := A.eq_empty_or_nonempty
· simp [Subsingleton.elim P ⊥]
apply hP.card_biUnion_offDiag_le'.trans
rw [div_le_iff₀ (Nat.cast_pos.2 (P.parts_nonempty hA.ne_empty).card_pos)]
have : (#A : 𝕜) + #P.parts ≤ 2 * #A := by rw [two_mul]; gcongr; exact P.card_parts_le_card
refine (mul_le_mul_of_nonneg_left this <| by positivity).trans ?_
suffices 1 ≤ ε / 4 * #P.parts by
rw [mul_left_comm, ← sq]
convert mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1 <;> ring
rwa [← div_le_iff₀', one_div_div]
positivity
