PrimeIntervalSums.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal primes on fixed logarithmic intervals

Mertens' second theorem supplies the fixed-power interval limit. Together with Chebyshev's estimate, it bounds the error in the marginal tuple count.

def OAI.JointDickman.primeReciprocalSum line 18
theorem OAI.JointDickman.primesLE_eq_filter line 21
theorem OAI.JointDickman.primeReciprocalSum_remainder_tendsto line 33
Source documentation
The Mertens remainder tends to its additive constant.
```
theorem primeReciprocalSum_remainder_tendsto
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ M : ℝ, Tendsto (fun x : ℝ => primeReciprocalSum x - Real.log (Real.log x))
      atTop (𝓝 M) := by
…
```
Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.primeReciprocalSum
theorem OAI.JointDickman.largePrimeSet_eq_sdiff line 45
theorem OAI.JointDickman.largePrimeSet_reciprocal_eq line 61
theorem OAI.JointDickman.largePrimeSet_reciprocal_tendsto line 72
Source documentation
Mertens' logarithmic interval mass, at the exact powers used in the smooth-number inclusion-exclusion.
```
theorem largePrimeSet_reciprocal_tendsto
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {c : ℝ}
    (hc : 0 < c) (hc1 : c ≤ 1) :
    Tendsto (fun N : ℝ => ∑ p ∈ largePrimeSet N (N ^ c), 1 / (p : ℝ))
      atTop (𝓝 (-Real.log c)) := by
…
```
Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.largePrimeSet
def OAI.JointDickman.PublishedInputs.ChebyshevPrimeCountingInput line 98
Source documentation
The large-argument Chebyshev upper bound; Montgomery–Vaughan, Multiplicative Number Theory I, Corollary 2.6.
```
def ChebyshevPrimeCountingInput : Prop :=
…
```
theorem OAI.JointDickman.largePrimeTupleCount_tendsto_of_published line 105
Source documentation
Mertens and Chebyshev estimates bound the marginal tuple error.
```
theorem largePrimeTupleCount_tendsto_of_published
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hCheb : PublishedInputs.ChebyshevPrimeCountingInput)
    (h : ℕ) {c : ℝ} (hc : 0 < c) (hc1 : c ≤ 1) :
    Tendsto (fun N : ℝ =>
      (primeTupleCount (largePrimeSet N (N ^ c)) (h + 1) N : ℝ) / N)
      atTop (𝓝 0) := by
…
```
Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.ChebyshevPrimeCountingInput, OAI.JointDickman.primeTupleCount, OAI.JointDickman.largePrimeSet