PrimeProductLocalLaw.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform local prime-product law without residue restrictions

This is the modulus-one case of the manuscript's local product law, with its stated B^(-80) absolute error on the shrinking lower-endpoint range.

theorem OAI.JointDickman.auxiliary_log_endpoint_conditions line 17

theorem OAI.JointDickman.primeProduct_local_interval_law line 34

Source documentation

All intervals in the range have the same absolute error constant.

theorem primeProduct_local_interval_law
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {z : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) :
    ∃ c : ℕ → ℝ, c 0 = squarefreeLeadingConstant z ∧ 0 < c 0 ∧
      ∃ H : ℕ, ∃ C : ℝ, 0 < C ∧ ∀ᶠ B : ℕ in atTop, ∀ a b : ℝ,
        (B : ℝ) ^ (-(1 / 10 : ℝ)) ≤ a → a ≤ b → b ≤ 16 / 5 →
        |(∑ n ∈ Ioc ⌊Real.exp (B * a)⌋₊ ⌊Real.exp (B * b)⌋₊,
            primeProductMass (auxiliaryPrimes B) z n) -
          ∫ s in a..b, scaledRoughDensity c z H B s| ≤ C * (B : ℝ) ^ (-(80 : ℝ)) := by
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.squarefreeLeadingConstant, OAI.JointDickman.primeProductMass, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.scaledRoughDensity