English
If A has small doubling, then the difference between A and B is controlled by the square of the doubling constant: δ_m[A,B] ≤ (σ_m[A,B])^2.
Русский
Если A имеет малое удвоение, то разница между A и B контролируется квадратом константы удвоения: δ_m[A,B] ≤ (σ_m[A,B])^2.
LaTeX
$$\\delta_m[A,B] \\le (\\sigma_m[A,B])^2$$
Lean4
/-- If `A` has small difference, then it has small doubling, with the constant squared.
This is a consequence of the Ruzsa triangle inequality. -/
@[to_additive /-- If `A` has small difference, then it has small doubling, with the constant squared.
This is a consequence of the Ruzsa triangle inequality. -/
]
theorem mulConst_le_divConst_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, mulConst_mul_card]
_ ≤ #(A / A) * #(A / A) := by norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..
_ = _ := by rw [← divConst_mul_card]; ring
