English
Let A be a finite subset of a group G with doubling constants bounded by a parameter K such that 1 < K < φ (the golden ratio). If both A⁻¹A and AA⁻¹ have size at most K|A|, then the product set A A⁻¹ can be covered by finitely many left cosets of a finite subgroup H of G. More precisely, there exist a finite subgroup H ≤ G and a finite set Z ⊆ G with |Z| ≤ c(K) (where c(K) = (2−K)K/((φ−K)(K−ψ))) such that A A⁻¹ = H Z.
Русский
Пусть A — конечное подмножество группы G, и ударная константа двойного множества удовлетворяет 1 < K < φ; если A⁻¹A и AA⁻¹ имеют размер не больший K|A|, тогда произведение AA⁻¹ можно покрыть конечным числом левых косеток конечной подгруппы H. Точно: найдутся конечная подгруппа H и конечная множество Z с |Z| ≤ c(K), такое что AA⁻¹ = H Z.
LaTeX
$$$\exists \text{ finite subgroup } H \le G,\ \exists Z \subseteq G,\ |Z| \le \dfrac{(2-K)K}{(φ-K)(K-ψ)}\ \text{и}\ A A^{-1} = H Z.$$$
Lean4
/-- If `A` has doubling `K` strictly less than `φ`, then `A * A⁻¹` is covered by
at most a constant number of cosets of a finite subgroup of `G`. -/
theorem doubling_lt_golden_ratio (hK₁ : 1 < K) (hKφ : K < φ) (hA₁ : #(A⁻¹ * A) ≤ K * #A) (hA₂ : #(A * A⁻¹) ≤ K * #A) :
∃ (H : Subgroup G) (_ : Fintype H) (Z : Finset G),
#Z ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (H : Set G) * Z = A * A⁻¹ :=
by
classical
-- Some useful initial calculations
have K_pos : 0 < K := by positivity
have hK₀ : 0 < K := by positivity
have hKφ' : 0 < φ - K := by linarith
have hKψ' : 0 < K - ψ := by linarith [Real.goldenConj_neg]
have hK₂' : 0 < 2 - K := by linarith [Real.goldenRatio_lt_two]
have const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ)) := by
positivity
-- We dispatch the trivial case `A = ∅` separately.
obtain rfl | A_nonempty := A.eq_empty_or_nonempty
·
exact
⟨⊥, inferInstance, ∅, by simp; positivity⟩
-- In the case where `A` is non-empty, we consider the set `S := A * A⁻¹` and its stabilizer `H`.
let S := A * A⁻¹
let H := stabilizer G S
have S_nonempty : S.Nonempty := by simpa [S]
have : Finite H := by simpa [H] using stabilizer_finite (by simpa) S.finite_toSet
cases nonempty_fintype H
have H_mul_S : (H : Set G) * S = S := by
simp [H, ← stabilizer_coe_finset]
-- Since `H` is a subgroup, find a finite set `Z ⊆ S` such that `H * Z = S` and `|H| * |Z| = |S|`.
obtain ⟨Z, hZ⟩ := exists_subset_mul_eq_mul_injOn H S
have H_mul_Z : (H : Set G) * Z = S := by simp [hZ.2.1, H_mul_S]
have H_toFinset_mul_Z : Set.toFinset H * Z = S := by simpa [← Finset.coe_inj]
have card_H_mul_card_Z : Fintype.card H * #Z = #S := by
simpa [card_mul_eq_mul_card_of_injOn_opSMul hZ.2.2] using congr_arg _ H_toFinset_mul_Z
refine
⟨H, inferInstance, Z, ?_, mod_cast H_mul_Z⟩
-- This is equivalent to showing that `|H| ≥ c(K)|S|` for some `c(K)` depending only on `K`.
suffices ((φ - K) * (K - ψ)) / ((2 - K) * K) * #S ≤ Fintype.card H by
calc
(#Z : ℝ)
_ = (Fintype.card H / #S : ℝ)⁻¹ := by simp [← card_H_mul_card_Z]
_ ≤ (((φ - K) * (K - ψ) / ((2 - K) * K) * #S) / #S)⁻¹ := by gcongr
_ = (2 - K) * K / ((φ - K) * (K - ψ)) :=
by
have : (#S : ℝ) ≠ 0 := by positivity
simp [this]
-- Write `r(z)` the number of representations of `z ∈ S` as `x * y⁻¹` for `x, y ∈ A`.
let r z : ℕ := A.convolution A⁻¹ z
have r_inv z : r z⁻¹ = r z := by
simp [r, inv_inv]
-- We show that every `z ∈ S` with at least `(K - 1)|A|` representations lies in `H`,
-- and that such `z` make up a proportion of at least `(2 - K) / ((φ - K) * (K - ψ))` of `S`.
calc
(φ - K) * (K - ψ) / ((2 - K) * K) * #S
_ ≤ #({z ∈ S | (K - 1) * #A < r z}) := ?_
_ ≤ #(H : Set G).toFinset := ?_
_ = Fintype.card H := by
simp
-- First, let's show that a large proportion of all `z ∈ S` have many representations.
· -- Let `l` be that number.
set l : ℕ := #({z ∈ S | (K - 1) * #A < r z}) with hk
have ineq : #A * #A ≤ ((2 - K) * l + (K - 1) * #S) * #A := by
calc
(#A : ℝ) * #A
_ = #A * #A⁻¹ := by simp
_ = #(A ×ˢ A⁻¹) := by simp
_ = ∑ z ∈ S, ↑(r z) := by
norm_cast
exact card_eq_sum_card_fiberwise fun xy hxy ↦ mul_mem_mul (mem_product.mp hxy).1 (mem_product.mp hxy).2
_ = ∑ z ∈ S with (K - 1) * #A < r z, ↑(r z) + ∑ z ∈ S with r z ≤ (K - 1) * #A, ↑(r z) := by norm_cast;
simp_rw [← not_lt, sum_filter_add_sum_filter_not]
_ ≤ ∑ z ∈ S with (K - 1) * #A < r z, ↑(#A) + ∑ z ∈ S with r z ≤ (K - 1) * #A, (K - 1) * #A :=
by
gcongr with z hz z hz
· exact convolution_le_card_left
· simp_all
_ = l * #A + (#S - l) * (K - 1) * #A := by
simp [hk, ← not_lt, mul_assoc, ← S.filter_card_add_filter_neg_card_eq_card fun z ↦ (K - 1) * #A < r z]
_ = ((2 - K) * l + (K - 1) * #S) * #A := by
ring
-- By cancelling `|A|` on both sides, we get `|A| ≤ (2 - K)l + (K - 1)|S|`.
-- By composing with `|S| ≤ K|A|`, we get `|S| ≤ (2 - K)Kl + (K - 1)K|S|`.
have : 0 < #A := by positivity
replace ineq :=
calc
(#S : ℝ)
_ ≤ K * #A := ‹_›
_ ≤ K * ((2 - K) * l + (K - 1) * #S) := by gcongr; exact le_of_mul_le_mul_right ineq <| by positivity
_ = (2 - K) * K * l + (K - 1) * K * #S := by
ring
-- Now, we are done.
calc
(φ - K) * (K - ψ) / ((2 - K) * K) * #S
_ = (φ - K) * (K - ψ) * #S / ((2 - K) * K) := div_mul_eq_mul_div ..
_ ≤ (2 - K) * K * l / ((2 - K) * K) :=
by
have := Real.goldenRatio_mul_goldenConj
have := Real.goldenRatio_add_goldenConj
rw [show (φ - K) * (K - ψ) = 1 - (K - 1) * K by grind]
gcongr ?_ / _
linarith [ineq]
_ = l := by
field_simp
-- Second, let's show that the `z ∈ S` with many representations are in `H`.
· gcongr
simp only [subset_iff, mem_filter, Set.mem_toFinset, SetLike.mem_coe, and_imp]
rintro z hz hrz
rw [mem_stabilizer_finset']
rintro w hw
have hrw : (2 - K) * #A ≤ r w := by
simpa [card_mul_inv_eq_convolution_inv] using
le_card_mul_inv_eq hA₁
(by simpa)
-- But also `r(z⁻¹) = r(z) > (K - 1)|A|`.
rw [← r_inv] at hrz
simp only [r, ← card_inter_smul] at hrz hrw
have : (0 : ℝ) < #((z⁻¹ •> A) ∩ (w •> A)) :=
by
have : (#((A ∩ z⁻¹ •> A) ∩ (A ∩ w •> A)) : ℝ) ≤ #(z⁻¹ •> A ∩ w •> A) := by gcongr <;> exact inter_subset_right
have : (#((A ∩ z⁻¹ •> A) ∪ (A ∩ w •> A)) : ℝ) ≤ #A := by gcongr;
exact union_subset inter_subset_left inter_subset_left
have :
(#((A ∩ z⁻¹ •> A) ∩ (A ∩ w •> A)) + #((A ∩ z⁻¹ •> A) ∪ (A ∩ w •> A)) : ℝ) = #(A ∩ z⁻¹ •> A) + #(A ∩ w •> A) :=
mod_cast card_inter_add_card_union ..
linarith
-- This is exactly what we set out to prove.
simpa [S, card_smul_inter_smul, Finset.Nonempty, mem_mul, mem_inv, -mem_inv', and_assoc] using this
