PrimeProductIntervalLower.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Positive local mass for the selected coefficient product

theorem OAI.JointDickman.half_density_compact_lower line 13

theorem OAI.JointDickman.half_primeProduct_interval_lower line 46

Source documentation

Uniform lower mass on every logarithmic interval inside [1,3]. The fixed B⁻⁸⁰ error is retained so the theorem also applies to intervals of length comparable to 1/B.

theorem half_primeProduct_interval_lower
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput) :
    ∃ d E : ℝ, 0 < d ∧ 0 < E ∧ ∀ᶠ B : ℕ in atTop, ∀ a b : ℝ,
      1 ≤ a → a ≤ b → b ≤ 3 →
      d * (b - a) - E * (B : ℝ)^(-(80 : ℝ)) ≤
        ∑ n ∈ Ioc ⌊Real.exp (B * a)⌋₊ ⌊Real.exp (B * b)⌋₊,
          primeProductMass (auxiliaryPrimes B) (1 / 2) n := by
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.primeProductMass, OAI.JointDickman.auxiliaryPrimes

theorem OAI.JointDickman.half_primeProduct_short_interval_lower line 77

Source documentation

Positive mass persists at the multiplicative-window scale: an interval of logarithmic width at least h/B has mass at least a fixed multiple of 1/B.

theorem half_primeProduct_short_interval_lower
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput) {h : ℝ} (hh : 0 < h) :
    ∃ d : ℝ, 0 < d ∧ ∀ᶠ B : ℕ in atTop, ∀ a b : ℝ,
      1 ≤ a → a ≤ b → b ≤ 3 → h / B ≤ b - a →
      d / B ≤ ∑ n ∈ Ioc ⌊Real.exp (B * a)⌋₊ ⌊Real.exp (B * b)⌋₊,
        primeProductMass (auxiliaryPrimes B) (1 / 2) n := by
…