English
For an equipartition P, the off-diagonal parts contribute at most (ε / 2) |A|^2 scaled by #P.parts, with a condition on ε and #P.parts.
Русский
Для равноправного разбиения P вклад диагональных и вне диагонали частей ограничен (ε/2) |A|^2 в масштабе #P.parts, при условии на ε и размер части.
LaTeX
$$P.IsEquipartition → (ε ≥ 0) → #(P.parts.biUnion offDiag) ≤ ε / 2 * #A ^ 2$$
Lean4
theorem card_biUnion_offDiag_le' (hP : P.IsEquipartition) :
(#(P.parts.biUnion offDiag) : 𝕜) ≤ #A * (#A + #P.parts) / #P.parts :=
by
obtain h | h := P.parts.eq_empty_or_nonempty
· simp [h]
calc
_ ≤ (#P.parts : 𝕜) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1)) :=
mod_cast card_biUnion_le_card_mul _ _ _ fun U hU ↦ ?_
_ = #P.parts * ↑(#A / #P.parts) * ↑(#A / #P.parts + 1) := by rw [mul_assoc]
_ ≤ #A * (#A / #P.parts + 1) := (mul_le_mul (mod_cast Nat.mul_div_le _ _) ?_ (by positivity) (by positivity))
_ = _ := by rw [← div_add_same (mod_cast h.card_pos.ne'), mul_div_assoc]
· simpa using Nat.cast_div_le
suffices (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1) by
rwa [Nat.mul_sub_right_distrib, one_mul, ← offDiag_card] at this
have := hP.card_part_le_average_add_one hU
refine Nat.mul_le_mul ((Nat.sub_le_sub_right this 1).trans ?_) this
simp only [Nat.add_succ_sub_one, add_zero, le_rfl]
