English
If 1 ∈ A, A⁻¹ = A, and |A^3| ≤ K|A|, then IsApproximateSubgroup (K^3) (A^2).
Русский
Пусть 1 ∈ A, A⁻¹ = A и |A^3| ≤ K|A|. Тогда IsApproximateSubgroup(K^3) на A^2.
LaTeX
$$$1 \\in A \\quad \\land \\ A^{-1} = A \\quad \\land \\ |A^{3}| \\le K|A| \\;\Rightarrow\\; IsApproximateSubgroup(K^{3})(A^{2}).$$$
Lean4
@[to_additive]
theorem of_small_tripling [DecidableEq G] {A : Finset G} (hA₁ : 1 ∈ A) (hAsymm : A⁻¹ = A) (hA : #(A ^ 3) ≤ K * #A) :
IsApproximateSubgroup (K ^ 3) (A ^ 2 : Set G)
where
one_mem := by rw [sq, ← one_mul 1]; exact Set.mul_mem_mul hA₁ hA₁
inv_eq_self := by simp [← inv_pow, hAsymm, ← coe_inv]
sq_covBySMul :=
by
replace hA :=
calc
(#(A ^ 4 * A) : ℝ)
_ = #(A ^ 5) := by rw [← pow_succ]
_ ≤ K ^ 3 * #A := small_pow_of_small_tripling (by omega) hA hAsymm
have hA₀ : A.Nonempty := ⟨1, hA₁⟩
obtain ⟨F, -, hF, hAF⟩ := ruzsa_covering_mul hA₀ hA
exact ⟨F, hF, by norm_cast; simpa [div_eq_mul_inv, pow_succ, mul_assoc, hAsymm] using hAF⟩
