PrimeCellBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform interval upper bounds for the actual prime-site law

theorem OAI.JointDickman.scaledRoughDensity_integral_le line 13

theorem OAI.JointDickman.primeSite_interval_upper line 28

Source documentation

The absolute local-law error is retained, so arbitrarily short cells are included. The two exponents are exactly those needed downstream.

theorem primeSite_interval_upper
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput) {z : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) :
    ∃ M C : ℝ, 0 ≤ M ∧ 0 < C ∧ ∀ᶠ B : ℕ in atTop,
      ∀ a b : ℝ, 1 / 4 ≤ a → a ≤ b → b ≤ 16 / 5 →
      ∀ (q : ℕ) [NeZero q], (q : ℝ) ≤ (B : ℝ) ^ (100 : ℝ) →
      ∀ r : (ZMod q)ˣ,
      (∑ x : auxiliaryPrimes B → Bool,
        if Real.log (retainedPrimeProduct (auxiliaryPrimes B) x) / B ∈ Set.Ioc a b ∧
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.retainedPrimeProduct