English
For a finite group G with a finite set A, IsApproximateSubgroup K A implies #(A^n) ≤ K^(n-1) * #A for all n.
Русский
Для конечного множества A в группе G, если A является K-приближённой подпгруппой, то #(A^n) ≤ K^(n-1) · #A для всех n.
LaTeX
$$$\\#(A^{n}) \\le K^{\\,n-1} \\cdot \\#A\\quad\\text{for all } n$$$
Lean4
@[to_additive]
theorem card_pow_le [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K (A : Set G)) :
∀ {n}, #(A ^ n) ≤ K ^ (n - 1) * #A
| 0 => by simpa using hA.nonempty
| 1 => by simp
| n + 2 => by
obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul
calc
(#(A ^ (n + 2)) : ℝ) ≤ #(F ^ (n + 1) * A) := by gcongr;
exact mod_cast Set.pow_subset_pow_mul_of_sq_subset_mul hSF (by cutsat)
_ ≤ #(F ^ (n + 1)) * #A := (mod_cast Finset.card_mul_le)
_ ≤ #F ^ (n + 1) * #A := by gcongr; exact mod_cast Finset.card_pow_le
_ ≤ K ^ (n + 1) * #A := by gcongr
