FormalConjectures/ErdosProblems/1141.lean

GitHub source file

9 declarations, 3 contain sorry, 0 declared as axioms

1. def Erdos1141.residuePrimeUpperBound The cutoff $m^{1/4 + \varepsilon}$ of Theorem 1.3 of [Po17] line 50 source

   Source documentation

   The cutoff $m^{1/4 + \varepsilon}$ of Theorem 1.3 of [Po17].

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

   Statement uses: Nat, Real

   Proof uses: HPow.hPow, HAdd.hAdd, HDiv.hDiv, OfNat.ofNat

   13 instances, coercions and auxiliary constants left out.

   noncomputable def residuePrimeUpperBound (m : ℕ) (ε : ℝ) : ℝ := (m : ℝ) ^ ((1 / 4 : ℝ) + ε)

2. def Erdos1141.residuePrimesUpTo The primes $\ell \leq m^{1/4+\varepsilon}$ with $\chi(\ell) = 1$ line 58 source

   Source documentation

   The primes $\ell \leq m^{1/4+\varepsilon}$ with $\chi(\ell) = 1$.

   This does not require $\chi$ to be quadratic. That hypothesis belongs to the theorem below, as it does in the paper.

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

   Statement uses: Nat, DirichletCharacter, Complex, Real, Finset

   Proof uses: Finset.filter, And, Nat.Prime, LE.le, Erdos1141.residuePrimeUpperBound, Eq, ZMod, OfNat.ofNat, Finset.range, HAdd.hAdd, Nat.ceil

   34 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

   noncomputable def residuePrimesUpTo (m : ℕ) (χ : DirichletCharacter ℂ m) (ε : ℝ) : Finset ℕ := by
   …

3. theorem Erdos1141.erdos_1141.variants.pollack_1_3 Theorem 1.3 of [Po17]: for a quadratic character to a large enough modulus, the primes below sorry line 68 source

   Source documentation

   Theorem 1.3 of [Po17]: for a quadratic character to a large enough modulus, the primes below $m^{1/4+\varepsilon}$ on which the character is $1$ outnumber any fixed power of $\log m$.

   depends on sorry what this means

   Statement uses: Real, LT.lt, OfNat.ofNat, Exists, Nat, DirichletCharacter, Complex, MulChar.IsQuadratic, ZMod, LE.le, HPow.hPow, Real.log, Finset.card, Erdos1141.residuePrimesUpTo

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

   33 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1141.variants.pollack_1_3 (ε A : ℝ) (hε : 0 < ε) (hA : 0 < A) :
       ∃ m₀ : ℕ, ∀ m : ℕ, m₀ < m → ∀ χ : DirichletCharacter ℂ m, MulChar.IsQuadratic χ →
         Real.log m ^ A ≤ ((residuePrimesUpTo m χ ε).card : ℝ) := by
   …

   Mentions: Erdos1141.residuePrimesUpTo

4. theorem Erdos1141.erdos_1141.variants.mertens_third Mertens' third theorem [Me1874], in the weakened form the linked proof assumes: the product over the primes up to $n$ of $1 - 1/p$ is at least $1/(3\log n)$ sorry line 81 source

   Source documentation

   Mertens' third theorem [Me1874], in the weakened form the linked proof assumes: the product over the primes up to $n$ of $1 - 1/p$ is at least $1/(3\log n)$.

   The true asymptotic is $e^{-\gamma}/\log n$, and $e^{-\gamma} > 1/3$, so this bound is weaker than the theorem and is what the deduction needs.

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, Real, HDiv.hDiv, HMul.hMul, Real.log, Finset.prod, Finset.filter, Nat.Prime, Finset.range, HAdd.hAdd, HSub.hSub

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

   42 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1141.variants.mertens_third (n : ℕ) (hn : 3 ≤ n) :
       1 / (3 * Real.log n) ≤ ∏ p ∈ (Finset.range (n + 1)).filter Nat.Prime, (1 - 1 / (p : ℝ)) := by
   …

5. def Erdos1141.Erdos1141Prop The property that $n-k^2$ is prime for all $k$ with $(n,k)=1$ and $k^2 < n$ line 88 source

   Source documentation

   The property that $n-k^2$ is prime for all $k$ with $(n,k)=1$ and $k^2 < n$.

   standard axioms: propext what this means

   Statement uses: Nat

   Proof uses: LT.lt, HPow.hPow, OfNat.ofNat, Nat.Coprime, Nat.Prime, HSub.hSub

   8 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

   def Erdos1141Prop (n : ℕ) : Prop :=
   …

6. instance Erdos1141.(instance at line 91) line 91 source
7. theorem Erdos1141.erdos_1141 sorry line 113 source

   depends on sorry what this means

   Statement uses: Iff, False, Infinite, Nat, Set.ofPred, Erdos1141.Erdos1141Prop

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

   3 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

8. example Erdos1141.(example at line 118) line 118 source
9. example Erdos1141.(example at line 122) line 122 source