PrimeProductLogLaw.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Prime-product intervals in logarithmic coordinates

The logarithmic density is the exact change of variables in the harmonic interval formula, not an independent smoothness assumption.

theorem OAI.JointDickman.scaledRoughDensity_integral line 18

theorem OAI.JointDickman.primeProduct_log_interval_law line 57

Source documentation

The actual prime-product probability of a log-coordinate interval.

theorem primeProduct_log_interval_law
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {z : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) (D : ℝ) :
    ∃ c : ℕ → ℝ, c 0 = squarefreeLeadingConstant z ∧ 0 < c 0 ∧
      ∃ H : ℕ, ∃ K : ℝ, 0 ≤ K ∧ ∀ᶠ B : ℕ in atTop, ∀ a b : ℝ,
        0 < a → a ≤ b → b ≤ 4 →
        9 ≤ Real.exp (B * a) → (B : ℝ) ^ (89 / 100 : ℝ) ≤ B * a →
        |(∑ 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| ≤
          z ^ 2 / (auxiliaryCutoff B : ℝ) + K * (B : ℝ) ^ (-D) * (2 + B * (b - a)) := by
…

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