FormalConjectures/GreensOpenProblems/22.lean

GitHub source file

7 declarations, 4 contain sorry, 0 declared as axioms

1. def Green22.HasMonochromaticSumProduct The monochromatic sum-product property: a colouring line 50 source

   Source documentation

   The monochromatic sum-product property: a colouring $c$ of $\{1, \ldots, N\}$ has a pair $(x, y)$ with $x, y \geq 3$ such that $x + y$ and $xy$ are both in $\{1, \ldots, N\}$ and receive the same colour.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Fin

   Proof uses: Exists, And, LE.le, HAdd.hAdd, HMul.hMul, Eq, Subtype.mk

   15 instances, coercions and auxiliary constants left out.

   def HasMonochromaticSumProduct (N : ℕ) (r : ℕ) (coloring : Icc 1 N → Fin r) : Prop :=
   …

2. def Green22.N₀ $N_0(r)$ is the smallest $N$ such that every $r$-colouring of $\{1, \ldots, N\}$ has the monochromatic sum-product property line 59 source

   Source documentation

   $N_0(r)$ is the smallest $N$ such that every $r$-colouring of $\{1, \ldots, N\}$ has the monochromatic sum-product property.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat

   Proof uses: InfSet.sInf, Set.ofPred, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Fin, Green22.HasMonochromaticSumProduct

   6 instances, coercions and auxiliary constants left out.

   noncomputable def N₀ (r : ℕ) : ℕ :=
   …

3. def Green22.GreenSawhneyBound The upper bound function from [GrSa25] line 65 source

   Source documentation

   The upper bound function from [GrSa25].

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Real

   Proof uses: Real.exp, HPow.hPow, OfNat.ofNat

   7 instances, coercions and auxiliary constants left out.

   noncomputable def GreenSawhneyBound (r : ℕ) : ℝ := Real.exp (Real.exp (r ^ 50))
   …

4. theorem Green22.green_22 If $\{1, \ldots, N\}$ is $r$-coloured then, for $N \geqslant N_0(r)$, there are integers $x, y \geqslant 3$ such that $x + y, xy$ have the same colour sorry line 74 source

   Source documentation

   If $\{1, \ldots, N\}$ is $r$-coloured then, for $N \geqslant N_0(r)$, there are integers $x, y \geqslant 3$ such that $x + y, xy$ have the same colour.

   Find reasonable bounds for $N_0(r)$. The goal is to improve upon the Green-Sawhney bound.

   depends on sorry what this means

   Statement uses: Nat, Real, sorryAx, Bool.false, Filter.Eventually, And, LE.le, Green22.N₀, Asymptotics.IsLittleO, Filter.atTop, Green22.GreenSawhneyBound

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

   11 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem green_22 :
       let ans := (answer(sorry) : ℕ → ℝ)
   …

5. theorem Green22.green_22.variants.green_sawhney_bound [GrSa25, Theorem 1.1] found a permissible upper bound sorry line 84 source

   Source documentation

   [GrSa25, Theorem 1.1] found a permissible upper bound.

   depends on sorry what this means

   Statement uses: Filter.Eventually, Nat, LE.le, Real, Green22.N₀, Green22.GreenSawhneyBound, Filter.atTop

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

   9 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem green_22.variants.green_sawhney_bound :
       ∀ᶠ r in atTop, N₀ r ≤ GreenSawhneyBound r := by
   …

   Mentions: Green22.N₀, Green22.GreenSawhneyBound

6. theorem Green22.green_22.variants.moreira_infinite [Mo17, Corollary 1.5] For any finite coloring of $\mathbb{N}$ there exist (infinitely many) $x, y \in \mathbb{N}$ such that $\{xy, x + y\}$ is monochromatic sorry line 97 source

   Source documentation

   [Mo17, Corollary 1.5] For any finite coloring of $\mathbb{N}$ there exist (infinitely many) $x, y \in \mathbb{N}$ such that $\{xy, x + y\}$ is monochromatic.

   This guarantees that $N_0(r)$ is well-defined.

   Note: [Mo17] also establishes that $x$ is of the same colour.

   depends on sorry what this means

   Statement uses: Nat, Fin, Set.Infinite, Prod, Set.ofPred, And, LT.lt, OfNat.ofNat, Prod.fst, Prod.snd, Eq, HMul.hMul, HAdd.hAdd

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

   12 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem green_22.variants.moreira_infinite :
       ∀ (r : ℕ) (coloring : ℕ → Fin r),
       Set.Infinite { p : ℕ × ℕ |
         0 < p.1 ∧ 0 < p.2 ∧
         coloring p.1 = coloring (p.1 * p.2) ∧
         coloring p.1 = coloring (p.1 + p.2) } := by
   …

7. theorem Green22.green_22.variants.lower_nine Since $x, y \geq 3$, we must have $xy \geq 9$, so $N_0(r) \geq 9$ (assuming $N_0(r)$ is well-defined, which follows from [Mo17]) sorry line 110 source

   Source documentation

   Since $x, y \geq 3$, we must have $xy \geq 9$, so $N_0(r) \geq 9$ (assuming $N_0(r)$ is well-defined, which follows from [Mo17]).

   depends on sorry what this means

   Statement uses: Nat, Ne, OfNat.ofNat, LE.le, Green22.N₀

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

   4 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem green_22.variants.lower_nine : ∀ r : ℕ, r ≠ 0 → 9 ≤ N₀ r := by
   …

   Mentions: Green22.N₀