GoldbachSelbergBound.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.GoldbachSelberg.sieve line 13
Source documentation
The actual multiplicity-preserving sieve for an even target.
```
def sieve (N P : ℕ) (hN : 2 ∣ N) (hP : Squarefree P) : BoundingSieve :=
…
```
def OAI.Problem337.GoldbachSelberg.denominator line 20
Source documentation
A concrete finite denominator, independent of proof-valued sieve parameters.
```
def denominator (N P z : ℕ) : ℝ :=
…
```
theorem OAI.Problem337.GoldbachSelberg.normalizer_eq_denominator line 25
theorem OAI.Problem337.GoldbachSelberg.denominator_pos line 33
theorem OAI.Problem337.GoldbachSelberg.rem_bound line 39
Source documentation
The local error of this actual sieve is bounded by its actual root count.
```
theorem rem_bound (N P d : ℕ) (hN : 2 ∣ N) (hP : Squarefree P) [NeZero d] :
    |(sieve N P hN hP).rem d| ≤ goldbachSieveRootCount N d := by
…
```
Mentions: OAI.Problem337.GoldbachSelberg.sieve, OAI.Problem337.goldbachSieveRootCount

theorem OAI.Problem337.GoldbachSelberg.rem_lcm_bound line 47

Source documentation

The polynomial root count yields the dimension-two factorizable remainder bound required by the optimized logarithmic error estimate.

theorem rem_lcm_bound (N P : ℕ) (hN : 2 ∣ N) (hP : Squarefree P)
    (a : ℕ) (ha : a ∈ P.divisors) (b : ℕ) (hb : b ∈ P.divisors) :
    |(sieve N P hN hP).rem (Nat.lcm a b)| ≤
      (2 : ℝ) ^ a.primeFactors.card * (2 : ℝ) ^ b.primeFactors.card := by
…

Mentions: OAI.Problem337.GoldbachSelberg.sieve

theorem OAI.Problem337.GoldbachSelberg.primePairs_le line 68
Source documentation
An unconditional, explicit finite upper sieve for ordered Goldbach pairs. Only evenness, squarefreeness of the chosen sieving product, and z ≥ 1 are assumed. The remaining denominator is an actual finite arithmetic sum; no prime-distribution or unproved remainder estimate is hidden in a premise.
```
theorem primePairs_le (N P : ℕ) (hN : 2 ∣ N) (hP : Squarefree P)
    {z : ℕ} (hz : 1 ≤ z) :
    ((PrimePairSieve.primePairs N).card : ℝ) ≤
      ((N - 1 : ℕ) : ℝ) / denominator N P z +
      (z : ℝ) ^ 2 * (1 + Real.log z) ^ 4 + 2 * P.primeFactors.card := by
…
```
Mentions: OAI.Problem337.PrimePairSieve.primePairs, OAI.Problem337.GoldbachSelberg.denominator
theorem OAI.Problem337.GoldbachSelberg.denominator_primorial line 90
Source documentation
With the primorial cutoff, the denominator is a sum over every squarefree integer up to the cutoff, not an unspecified subset of them.
```
theorem denominator_primorial (N z : ℕ) :
    denominator N (primorial z) z =
      ∑ d ∈ Icc 1 z, if Squarefree d then
        goldbachSieveDensity N d *
          ∏ p ∈ d.primeFactors, (1 - goldbachSieveDensity N p)⁻¹ else 0 := by
…
```
Mentions: OAI.Problem337.GoldbachSelberg.denominator, OAI.Problem337.goldbachSieveDensity

theorem OAI.Problem337.GoldbachSelberg.primePairs_le_primorial line 113

Source documentation

The explicit prime-pair sieve at the canonical primorial product.

theorem primePairs_le_primorial (N : ℕ) (hN : 2 ∣ N) {z : ℕ} (hz : 1 ≤ z) :
    ((PrimePairSieve.primePairs N).card : ℝ) ≤
      ((N - 1 : ℕ) : ℝ) / denominator N (primorial z) z +
      (z : ℝ) ^ 2 * (1 + Real.log z) ^ 4 + 2 * (Nat.primesLE z).card := by
…

Mentions: OAI.Problem337.PrimePairSieve.primePairs, OAI.Problem337.GoldbachSelberg.denominator