divConst_le_inv_dens — Mathlib

English

For any finite A,B in a multiplicative group G, the dense-difference constant δ_m(A,B) is bounded above by the inverse density of A: δ_m(A,B) ≤ dens(A)^{-1}. In particular, since dens(A) = |A|/|G|, one has δ_m(A,B) ≤ |G|/|A|.

Русский

Для любых конечных подмножеств A,B группы G верна оценка плотности различия: δ_m(A,B) ≤ dens(A)^{-1}. При этом dens(A) = |A|/|G|, следовательно δ_m(A,B) ≤ |G|/|A|.

LaTeX

$$$\\delta_m(A,B) \\le \\operatorname{dens}(A)^{-1}$$$

Lean4

/-- Dense sets have small difference constant. -/
@[to_additive subConst_le_inv_dens /-- Dense sets have small difference constant. -/
    ]
theorem divConst_le_inv_dens : δₘ[A, B] ≤ A.dens⁻¹ := by rw [dens, inv_div, divConst]; gcongr; exact card_le_univ _

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