English
Let A be nonempty finite and B a finite subset. Then for m,n ≥ 0,
Русский
Пусть A не пусто, конечно и B конечно. Тогда для любых m,n ≥ 0 выполняется
LaTeX
$$$\#(B^{m}/B^{n}) \le \Big(\frac{\#(A B)}{\#A}\Big)^{m+n} \cdot \#A$$$
Lean4
/-- If `A` has small tripling, say with constant `K`, then `A` has small alternating powers, in the
sense that `|A^±1 * ... * A^±1|` is at most `|A|` times a constant exponential in the number of
terms in the product.
When `A` is symmetric (`A⁻¹ = A`), the base of the exponential can be lowered from `K ^ 3` to `K`,
where `K` is the tripling constant. See `Finset.small_pow_of_small_tripling`. -/
@[to_additive /-- If `A` has small tripling, say with constant `K`, then `A` has small alternating powers, in the
sense that `|±A ± ... ± A|` is at most `|A|` times a constant exponential in the number of
terms in the product.
When `A` is symmetric (`-A = A`), the base of the exponential can be lowered from `K ^ 3` to `K`,
where `K` is the tripling constant. See `Finset.small_nsmul_of_small_tripling`. -/
]
theorem small_alternating_pow_of_small_tripling (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (ε : Fin m → ℤ)
(hε : ∀ i, |ε i| = 1) : #((finRange m).map fun i ↦ A ^ ε i).prod ≤ K ^ (3 * (m - 2)) * #A :=
by
have hm₀ : m ≠ 0 := by positivity
have hε₀ i : ε i ≠ 0 := fun h ↦ by simpa [h] using hε i
obtain rfl | hA₀ := A.eq_empty_or_nonempty
· simp [hm₀, hε₀]
have hK₁ : 1 ≤ K :=
one_le_of_le_mul_right₀ (by positivity) (hA.trans' <| by norm_cast; exact card_le_card_pow (by simp))
rw [pow_mul]
refine inductive_claim_mul hm (fun δ hδ ↦ ?_) ε hε
simp only [finRange_succ_eq_map, Nat.reduceAdd, isValue, finRange_zero, map_nil, List.map_cons, succ_zero_eq_one,
succ_one_eq_two, List.prod_cons, prod_nil, mul_one, ← mul_assoc]
simp only [zero_le_one, abs_eq, Int.reduceNeg, forall_iff_succ, isValue, succ_zero_eq_one, succ_one_eq_two,
IsEmpty.forall_iff, and_true] at hδ
have : K ≤ K ^ 3 := le_self_pow₀ hK₁ (by cutsat)
have : K ^ 2 ≤ K ^ 3 := by
gcongr
· exact hK₁
· simp
obtain ⟨hδ₀ | hδ₀, hδ₁ | hδ₁, hδ₂ | hδ₂⟩ := hδ <;> simp [hδ₀, hδ₁, hδ₂]
· simp [pow_succ] at hA
nlinarith
· nlinarith [small_pos_pos_neg_mul hA]
· nlinarith [small_pos_neg_pos_mul hA]
· nlinarith [small_pos_neg_neg_mul hA]
· nlinarith [small_neg_pos_pos_mul hA]
· nlinarith [small_neg_pos_neg_mul hA]
· nlinarith [small_neg_neg_pos_mul hA]
· simp [*, pow_succ', ← mul_inv_rev] at hA ⊢
nlinarith
