sum_nonUniforms_lt — Mathlib

English

If A is nonempty and ε > 0, and P is equipartition with G uniform at ε, then the sum over nonUniforms is bounded by ε times (|A| + |P.parts|)^2.

Русский

Если A непусто, ε > 0, и P — равноправное разбиение с G однородным при ε, то сумма по неоднородностям ограничена ε·(|A|+|P.parts|)^2.

LaTeX

$$A.Nonempty → ε > 0 → P.IsEquipartition → P.IsUniform G ε → ∑ 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 ε) :
    #((P.nonUniforms G ε).biUnion fun (U, V) ↦ U ×ˢ V) < 4 * ε * #A ^ 2 := by
  calc
    _ ≤ ∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) := by norm_cast; simp_rw [← card_product]; exact card_biUnion_le
    _ < _ := (hP.sum_nonUniforms_lt' hA hε hG)
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring

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