English
Let A,B,C be finite subsets. Then (#(A/C))·|B| ≤ #(A B)·|(B/C)|.
Русский
Пусть A,B,C — конечные подмножества. Тогда #(A/C)·|B| ≤ #(A B)·|(B/C)|.
LaTeX
$$$|(A/C)|\,|B| \le |(A B)|\,|B/C|$$$
Lean4
/-- If `A` is symmetric (`A⁻¹ = A`) and has small tripling, then `A` has small powers,
in the sense that `|A ^ m|` is at most `|A|` times a constant exponential in `m`.
See also `Finset.small_alternating_pow_of_small_tripling` for a version with a weaker constant but
which encompasses non-symmetric sets. -/
@[to_additive /-- If `A` is symmetric (`-A = A`) and has small tripling, then `A` has small powers,
in the sense that `|m • A|` is at most `|A|` times a constant exponential in `m`.
See also `Finset.small_alternating_nsmul_of_small_tripling` for a version with a weaker constant but
which encompasses non-symmetric sets. -/
]
theorem small_pow_of_small_tripling (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (hAsymm : A⁻¹ = A) :
#(A ^ m) ≤ K ^ (m - 2) * #A :=
by
have (ε : ℤ) (hε : |ε| = 1) : A ^ ε = A := by obtain rfl | rfl := eq_or_eq_neg_of_abs_eq hε <;> simp [hAsymm]
calc
(#(A ^ m) : ℝ) = #((finRange m).map fun i ↦ A ^ 1).prod := by simp
_ ≤ K ^ (m - 2) * #A := inductive_claim_mul hm (fun δ hδ ↦ by simpa [this _ (hδ _), pow_succ'] using hA) _ (by simp)
