English
For a sum over the non-uniform parts, the total weighted size is strictly less than ε times a quadratic expression in |A| and |P.parts|, under suitable assumptions on A, ε and G being equipartition/uniform.
Русский
Для суммы по неоднородным частям суммарный вес строго меньше ε, умноженное на квадратичный выражение от |A| и |P.parts|, при надлежащих предположениях на A, ε и G как на равноправном/однородном.
LaTeX
$$∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) < ε * (#A + #P.parts) ^ 2$$
Lean4
theorem sum_nonUniforms_lt' (hA : A.Nonempty) (hε : 0 < ε) (hP : P.IsEquipartition) (hG : P.IsUniform G ε) :
∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) < ε * (#A + #P.parts) ^ 2 :=
by
calc
_ ≤ #(P.nonUniforms G ε) • (↑(#A / #P.parts + 1) : 𝕜) ^ 2 := sum_le_card_nsmul _ _ _ ?_
_ = _ := (nsmul_eq_mul _ _)
_ ≤ _ := (mul_le_mul_of_nonneg_right hG <| by positivity)
_ < _ := ?_
· simp only [Prod.forall, Finpartition.mk_mem_nonUniforms, and_imp]
rintro U V hU hV - -
rw [sq, ← Nat.cast_mul, ← Nat.cast_mul, Nat.cast_le]
exact Nat.mul_le_mul (hP.card_part_le_average_add_one hU) (hP.card_part_le_average_add_one hV)
· rw [mul_right_comm _ ε, mul_comm ε]
apply mul_lt_mul_of_pos_right _ hε
norm_cast
exact aux (P.parts_nonempty hA.ne_empty).card_pos
