SieveGoldbachDenominator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The dimension-two denominator bound for the finite Goldbach sieve.

lemma OAI.TwoPointCorrelations.sieve_goldbach_denominator_two_scale line 13

theorem OAI.TwoPointCorrelations.sieve_goldbach_denominator_log_square line 37

Source documentation

A single explicit logarithmic lower threshold gives the usual log(z)^2 / singularFactor(N) denominator.

theorem sieve_goldbach_denominator_log_square :
    ∃ c : ℝ, 0 < c ∧ ∀ N z : ℕ, 2 ∣ N → N ≠ 0 → 2 ≤ z →
      8 * (halaszMertensConstant + Real.log 2) ≤ Real.log z →
      c * Real.log z ^ 2 / sieveSingularFactor N ≤
        GoldbachSelberg.denominator N (primorial z) z := by
…

Mentions: OAI.TwoPointCorrelations.halaszMertensConstant, OAI.TwoPointCorrelations.sieveSingularFactor