SieveGoldbachTruncation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic-moment criterion applied to the actual Goldbach sieve.

lemma OAI.TwoPointCorrelations.sieve_prime_subset_log_cutoff line 13
theorem OAI.TwoPointCorrelations.sieve_goldbach_denominator_half_product line 22
theorem OAI.TwoPointCorrelations.sieve_goldbach_denominator_small_primes line 48
Source documentation
The small-prime cutoff is chosen using a logarithmic inequality, avoiding any rounding assumption on its real value.
```
theorem sieve_goldbach_denominator_small_primes (N z : ℕ) (hN : 2 ∣ N) (hz : 2 ≤ z)
    {y : ℝ} (hy : 1 ≤ y)
    (hscale : 4 * (Real.log y + halaszMertensConstant) ≤ Real.log z) :
    (∏ p ∈ sievePrimesUpTo y, (1 + sieveGoldbachWeight N p)) / 2 ≤
      GoldbachSelberg.denominator N (primorial z) z := by
…
```
Mentions: OAI.TwoPointCorrelations.halaszMertensConstant, OAI.TwoPointCorrelations.sievePrimesUpTo, OAI.TwoPointCorrelations.sieveGoldbachWeight