FormalConjectures/GreensOpenProblems/5.lean

GitHub source file

4 declarations, 4 contain sorry, 0 declared as axioms

1. theorem Green5.green_5 Which finite groups have the smallest biggest product-free sets? sorry line 54 source

   Source documentation

   Which finite groups have the smallest biggest product-free sets?

   We formalise this as: determine the supremum of exponents $\alpha$ such that every nontrivial finite group of order $n$ contains a product-free set of size $\geq c n^{\alpha}$ for some absolute constant $c > 0$. (The trivial group is excluded since its only product-free subset is empty.) Kedlaya [Ke97] showed that $\alpha = 11/14$ is admissible, and Green suggests this exponent may well be sharp; the candidate extremal family is the Ree groups ${}^2G_2(q)$, $q = 3^{2m+1}$.

   depends on sorry what this means

   Statement uses: IsLUB, Real, Set.ofPred, Exists, And, GT.gt, OfNat.ofNat, Group, Fintype, Nontrivial, Finset, IsProductFree, LE.le, HMul.hMul, HPow.hPow, Fintype.card, Finset.card, sorryAx, Bool.false

   Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

   35 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem green_5 :
       IsLUB {α : ℝ | ∃ c > (0 : ℝ), ∀ (G : Type) [Group G] [Fintype G], Nontrivial G →
         ∃ S : Finset G, IsProductFree (S : Set G) ∧
           c * (Fintype.card G : ℝ) ^ α ≤ (S.card : ℝ)}
         answer(sorry) := by
   …

   Mentions: c, IsProductFree

2. theorem Green5.green_5.variants.kedlaya Kedlaya [Ke97] observed, refining some work of Babai and Sós [BaSo85], that it follows from the classification of finite simple groups that every finite group sorry line 67 source

   Source documentation

   Kedlaya [Ke97] observed, refining some work of Babai and Sós [BaSo85], that it follows from the classification of finite simple groups that every finite group $G$ of order $n$ has a product-free subset of size $\gg n^{11/14}$.

   depends on sorry what this means

   Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Group, Fintype, Nontrivial, Finset, IsProductFree, LE.le, HMul.hMul, HPow.hPow, Fintype.card, HDiv.hDiv, Nat, Finset.card

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   48 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem green_5.variants.kedlaya :
       ∃ c > (0 : ℝ), ∀ (G : Type) [Group G] [Fintype G], Nontrivial G →
         ∃ S : Finset G, IsProductFree (S : Set G) ∧
           c * (Fintype.card G : ℝ) ^ ((11 : ℝ) / 14) ≤ (S.card : ℝ) := by
   …

   Mentions: c, IsProductFree

3. theorem Green5.green_5.variants.sl_two A good model problem would be to determine the largest product-free subsets of $\mathrm{SL}_2(\mathbb{F}_p)$ sorry line 80 source

   Source documentation

   A good model problem would be to determine the largest product-free subsets of $\mathrm{SL}_2(\mathbb{F}_p)$.

   depends on sorry what this means

   Statement uses: Nat, Fact, Nat.Prime, Finset, Matrix.SpecialLinearGroup, Fin, OfNat.ofNat, ZMod, sorryAx, Bool.false, MaximalFor, Set, IsProductFree, Set.ncard

   Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   16 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem green_5.variants.sl_two (p : ℕ) [Fact p.Prime] :
       let S : Finset (SL₂ p) := answer(sorry)
   …

4. theorem Green5.green_5.variants.gowers_sl_two For the largest product-free subsets of $\mathrm{SL}_2(\mathbb{F}_p)$ of order $n$, the best-known upper bound is $O(n^{8/9})$, due to Gowers [Go08] sorry line 90 source

   Source documentation

   For the largest product-free subsets of $\mathrm{SL}_2(\mathbb{F}_p)$ of order $n$, the best-known upper bound is $O(n^{8/9})$, due to Gowers [Go08].

   depends on sorry what this means

   Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Nat, Fact, Nat.Prime, Finset, Matrix.SpecialLinearGroup, Fin, ZMod, IsProductFree, LE.le, Finset.card, HMul.hMul, HPow.hPow, Fintype.card, HDiv.hDiv

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   68 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem green_5.variants.gowers_sl_two :
       ∃ C > (0 : ℝ), ∀ (p : ℕ) [Fact p.Prime], ∀ S : Finset (SL₂ p),
         IsProductFree (S : Set (SL₂ p)) →
         (S.card : ℝ) ≤ C * (Fintype.card (SL₂ p) : ℝ) ^ ((8 : ℝ) / 9) := by
   …

   Mentions: IsProductFree