Product growth in special linear groups over finite fields
DefinitionProduct set of a finite set#✓fully proved
For a finite subset \(A\) of a type with a multiplication, the product set \(A \cdot A\) is the finite set \(\{ab : a, b \in A\}\) of all products of two elements of \(A\).
@[nolint defsWithUnderscore]
def AIMCombinatorics0241_prodSet {G : Type*} [Mul G] [DecidableEq G] (A : Finset G) : Finset G :=
Finset.image₂ (· * ·) A ASources
- AIM-COMBINATORICS-0241, Problem 3.4, aim-combinatorics-notes.json notes[240].
DefinitionTwo-step product growth in \(\mathrm{SL}_2(\mathbb{F}_p)\) (AIM Problem 3.4)#✓fully proved
The statement that for every real \(C \ge 1\) there are a real \(\delta > 0\) and a natural number \(P_0\) such that for every prime \(p \ge P_0\) and every finite subset \(A\) of \(\mathrm{SL}_2(\mathbb{F}_p)\), where \(\mathbb{F}_p = \mathbb{Z}/p\mathbb{Z}\), with \(C^{-1} p^{5/2} \le |A| \le C p^{5/2}\), the product set \(A \cdot A = \{ab : a, b \in A\}\) satisfies \(|A \cdot A| > p^{5/2 + \delta}\).
This is a large-\(p\) reading of the question of Green, after Venkatesh: if \(A \subseteq \mathrm{SL}_2(\mathbb{F}_p)\) satisfies \(|A| \sim p^{5/2}\), does it follow that \(|A \cdot A| > p^{5/2 + \delta}\)?
noncomputable def conjecture : Prop :=
∀ C : ℝ, 1 ≤ C →
∃ δ : ℝ, 0 < δ ∧
∃ P0 : ℕ, ∀ p : ℕ, P0 ≤ p → Nat.Prime p →
∀ A : Finset (Matrix.SpecialLinearGroup (Fin 2) (ZMod p)),
(((1 / C) * Real.rpow (p : ℝ) (5 / 2 : ℝ) ≤ (A.card : ℝ)) ∧
((A.card : ℝ) ≤ C * Real.rpow (p : ℝ) (5 / 2 : ℝ)) →
Real.rpow (p : ℝ) (5 / 2 + δ) < ((AIMCombinatorics0241_prodSet A).card : ℝ))@[nolint defsWithUnderscore]
def AIMCombinatorics0241_prodSet {G : Type*} [Mul G] [DecidableEq G] (A : Finset G) : Finset G :=
Finset.image₂ (· * ·) A AWantedExt/Combinatorics/SL2TwoStepProductGrowthWanted.lean:49
Sources
- AIM-COMBINATORICS-0241, Problem 3.4, aim-combinatorics-notes.json notes[240], https://aimath.org/WWN/additivecomb/additivecomb.pdf.
Uses 1 · Used by 1
TheoremSets of size about \(p^{5/2}\) in \(\mathrm{SL}_2(\mathbb{F}_p)\) grow under multiplication#●ready to prove
For every real \(C \ge 1\) there are a real \(\delta > 0\) and a natural number \(P_0\) such that for every prime \(p \ge P_0\) and every finite subset \(A\) of \(\mathrm{SL}_2(\mathbb{F}_p)\), where \(\mathbb{F}_p = \mathbb{Z}/p\mathbb{Z}\), with \(C^{-1} p^{5/2} \le |A| \le C p^{5/2}\), the product set \(A \cdot A = \{ab : a, b \in A\}\) satisfies \(|A \cdot A| > p^{5/2 + \delta}\).
Every nontrivial representation of \(\mathrm{SL}_2(\mathbb{F}_p)\) has dimension at least \((p-1)/2\), and the product-mixing bound of Gowers and Babai–Nikolov–Pyber then gives \(|A \cdot A| \gg p^3\) for such \(A\), so every \(\delta < 1/2\) works. This answers AIM additive-combinatorics Problem 3.4 (Green, after Venkatesh).
public theorem_wanted conjecture_holds : conjecturenoncomputable def conjecture : Prop :=
∀ C : ℝ, 1 ≤ C →
∃ δ : ℝ, 0 < δ ∧
∃ P0 : ℕ, ∀ p : ℕ, P0 ≤ p → Nat.Prime p →
∀ A : Finset (Matrix.SpecialLinearGroup (Fin 2) (ZMod p)),
(((1 / C) * Real.rpow (p : ℝ) (5 / 2 : ℝ) ≤ (A.card : ℝ)) ∧
((A.card : ℝ) ≤ C * Real.rpow (p : ℝ) (5 / 2 : ℝ)) →
Real.rpow (p : ℝ) (5 / 2 + δ) < ((AIMCombinatorics0241_prodSet A).card : ℝ))WantedExt/Combinatorics/SL2TwoStepProductGrowthWanted.lean:53
Sources
- N. Nikolov and L. Pyber, Product decompositions of quasirandom groups and a Jordan type theorem, arXiv:math/0703343, https://arxiv.org/abs/math/0703343.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.