PrimeTupleBounds.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Prime tuples in the marginal floor error

Fix the first h entries of an ordered prime tuple and count the last entry by a Chebyshev bound. Summing its reciprocal-product weight gives the hth power of the reciprocal-prime sum. Repeated primes are allowed, so this bounds the distinct tuples used in inclusion-exclusion as well. The Chebyshev and reciprocal-sum hypotheses are explicit arithmetic inputs.

def OAI.JointDickman.PrimeCountingUpperBound line 24
Source documentation
Only the range t ≥ y of the usual Chebyshev upper estimate is needed.
```
def PrimeCountingUpperBound (C y : ℝ) : Prop :=
…
```
def OAI.JointDickman.largePrimeSet line 28
Source documentation
Allowed large primes up to the real endpoint N.
```
noncomputable def largePrimeSet (N y : ℝ) : Finset ℕ :=
…
```
def OAI.JointDickman.primeTupleCount line 32
Source documentation
Ordered tuples of h primes from P with product at most N.
```
noncomputable def primeTupleCount (P : Finset ℕ) (h : ℕ) (N : ℝ) : ℕ :=
…
```
theorem OAI.JointDickman.card_filter_product_real line 36

theorem OAI.JointDickman.prime_product_fiber_bound line 46

Source documentation

The one-dimensional final-coordinate estimate.

theorem prime_product_fiber_bound {P : Finset ℕ} {C y N r : ℝ}
    (hP : ∀ p ∈ P, p.Prime ∧ y < (p : ℝ)) (hC : 0 ≤ C)
    (hy : 1 < y) (hN : 0 ≤ N) (hr : 0 < r)
    (hcount : PrimeCountingUpperBound C y) :
    ((P.filter (fun p : ℕ => r * (p : ℝ) ≤ N)).card : ℝ) ≤
      (C * N / Real.log y) * (1 / r) := by
…

Mentions: OAI.JointDickman.PrimeCountingUpperBound

theorem OAI.JointDickman.primeTupleCount_le_fibers line 86

theorem OAI.JointDickman.primeTupleCount_bound line 123

Source documentation

The ordered tuple bound used for the floor error. It is valid without distinctness restrictions on the prime entries.

theorem primeTupleCount_bound {P : Finset ℕ} {C y N : ℝ} (h : ℕ)
    (hP : ∀ p ∈ P, p.Prime ∧ y < (p : ℝ)) (hC : 0 ≤ C)
    (hy : 1 < y) (hN : 0 ≤ N) (hcount : PrimeCountingUpperBound C y) :
    (primeTupleCount P (h + 1) N : ℝ) ≤
      (C * N / Real.log y) * (∑ p ∈ P, 1 / (p : ℝ)) ^ h := by
…

Mentions: OAI.JointDickman.PrimeCountingUpperBound, OAI.JointDickman.primeTupleCount

theorem OAI.JointDickman.largePrimeTupleCount_bound line 149

theorem OAI.JointDickman.largePrimeTupleCount_density_tendsto_zero line 160

Source documentation

For y=N^c, the tuple count is o(N) once the reciprocal-prime sum is bounded. The explicit Chebyshev hypothesis is not discharged here.

theorem largePrimeTupleCount_density_tendsto_zero (h : ℕ) {c C K : ℝ}
    (hc : 0 < c) (hC : 0 ≤ C)
    (hcount : ∀ᶠ N : ℝ in atTop, PrimeCountingUpperBound C (N ^ c))
    (hrecip : ∀ᶠ N : ℝ in atTop,
      (∑ p ∈ largePrimeSet N (N ^ c), 1 / (p : ℝ)) ≤ K) :
    Tendsto (fun N : ℝ =>
      (primeTupleCount (largePrimeSet N (N ^ c)) (h + 1) N : ℝ) / N)
      atTop (𝓝 0) := by
…

Mentions: OAI.JointDickman.PrimeCountingUpperBound, OAI.JointDickman.largePrimeSet, OAI.JointDickman.primeTupleCount