RoughHarmonicLaw.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The harmonic rough coefficient law

Partial summation of the proved moving-cutoff expansion gives the weighted interval law needed for the independent prime-product model.

theorem OAI.JointDickman.finiteCountingFunction_rough line 18
theorem OAI.JointDickman.roughDensityPolynomial_continuousAt line 24

theorem OAI.JointDickman.rough_harmonic_interval_law line 35

Source documentation

Uniformity includes arbitrarily short intervals: the error is absolute.

theorem rough_harmonic_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 : ℝ,
        9 ≤ a → a ≤ b → (B : ℝ) ^ (89 / 100 : ℝ) ≤ Real.log a →
        |(∑ n ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, roughSquarefreeWeight (Nat.primesLE (auxiliaryCutoff B)) z n / (n : ℝ)) -
          ∫ t in a..b, roughDensityPolynomial c (Nat.primesLE (auxiliaryCutoff B)) z H (Real.log t) / t| ≤
          K * (B : ℝ) ^ (-D) * (2 + Real.log (b / a)) := by
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.squarefreeLeadingConstant, OAI.JointDickman.roughSquarefreeWeight, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.roughDensityPolynomial