English
The difference constant is bounded above by the square of the doubling constant: δ_m[A] ≤ σ_m[A]^2.
Русский
Константа различий ограничена сверху квадратом константы удвоения: δ_m[A] ≤ σ_m[A]^2.
LaTeX
$$\\delta_m[A] \\le \\sigma_m[A]^2$$
Lean4
/-- If `A` has small doubling, then it has small difference, with the constant squared.
This is a consequence of the Ruzsa triangle inequality. -/
@[to_additive /-- If `A` has small doubling, then it has small difference, with the constant squared.
This is a consequence of the Ruzsa triangle inequality. -/
]
theorem divConst_le_mulConst_sq : δₘ[A] ≤ σₘ[A] ^ 2 :=
by
obtain rfl | hA' := A.eq_empty_or_nonempty
· simp
refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)
calc
_ = #(A / A) * (#A : ℚ≥0) := by rw [← mul_assoc, divConst_mul_card]
_ ≤ #(A * A) * #(A * A) := by norm_cast; exact ruzsa_triangle_inequality_div_mul_mul ..
_ = _ := by rw [← mulConst_mul_card]; ring
