English
Let A be a finite subset of a group G with doubling strictly less than 3/2 times its size, i.e. |A A| < (3/2)·|A|. Then there exists a finite subgroup H ≤ G such that A is contained in a left coset aH for every a in A, and H is normalized by every a ∈ A (i.e., a⁻¹Ha = H for all a ∈ A). Moreover, |H| < (3/2)·|A|.
Русский
Пусть A — конечное множество в группе G such that удвоение A A меньше (3/2)·|A|. Тогда существует конечная подпгруппа H ≤ G такая, что A ⊆ aH для каждого a ∈ A, и каждый a ∈ A нормализует H (то есть a⁻¹Ha = H для всех a ∈ A). Кроме того, |H| < (3/2)·|A|.
LaTeX
$$$\exists H \le G,\ |H| < \tfrac{3}{2}\,|A|\ \land\ \forall a \in A:\ A \subseteq aH\ \land\ a^{-1}Ha = H$$$
Lean4
/-- If `A` has doubling strictly less than `3 / 2`, then there exists a subgroup `H` of the
normaliser of `A` of size strictly less than `3 / 2 * #A` such that `A` is a subset of a coset of
`H` (in fact a subset of `a • H` for every `a ∈ A`).
Note that this is sharp: `A = {0, 1}` in `ℤ` has doubling `3 / 2` and can't be covered by a subgroup
of size at most `2`.
This is Theorem 2.2.1 in [tointon2020]. -/
theorem doubling_lt_three_halves (h : #(A * A) < (3 / 2 : ℚ) * #A) :
∃ (H : Subgroup G) (_ : Fintype H),
Fintype.card H < (3 / 2 : ℚ) * #A ∧ ∀ a ∈ A, (A : Set G) ⊆ a • H ∧ a •> (H : Set G) = H <• a :=
by
let H := invMulSubgroup A h
refine ⟨H, inferInstance, ?_, fun a ha ↦ ⟨?_, ?_⟩⟩
· simp [← Nat.card_eq_fintype_card, invMulSubgroup, ← coe_mul, -coe_inv, H]
rwa [Nat.card_eq_finsetCard, card_inv_mul_of_doubling_lt_three_halves h]
· rw [invMulSubgroup_eq_inv_mul]
exact_mod_cast A_subset_aH a ha
·
simpa [H, invMulSubgroup_eq_inv_mul, ← coe_inv, ← coe_mul, ← coe_smul_finset] using
smul_inv_mul_eq_inv_mul_opSMul h ha
