RoughCoefficients.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Coefficients after removal of the small prime factors

Each coefficient is a finite combination of the published fixed-order Selberg–Delange coefficients and the actual correction moments. The definition has no dependence on a subsequently chosen truncation order.

def OAI.JointDickman.roughCoefficient line 18
theorem OAI.JointDickman.roughCoefficient_zero line 22

theorem OAI.JointDickman.roughCoefficient_expansion line 29

Source documentation

Grouping the Taylor terms by their total degree gives the actual rough coefficients, with no discarded cross terms.

theorem roughCoefficient_expansion (c : ℕ → ℝ) (E : Finset ℕ)
    (z L : ℝ) (H : ℕ) :
    (∑ ν ∈ range (H + 1), roughCoefficient c E z ν * L ^ (z - 1 - ν)) =
      ∑ j ∈ range (H + 1), c j *
        ∑ k ∈ range (H - j + 1), rpowShiftCoeff (z - 1 - j) k *
          correctionLogMoment E z k * L ^ (z - 1 - j - k) := by
…

Mentions: OAI.JointDickman.roughCoefficient, OAI.JointDickman.rpowShiftCoeff, OAI.JointDickman.correctionLogMoment

theorem OAI.JointDickman.roughCoefficient_bound line 64

Source documentation

Uniform coefficient bound with the absolute exponent supplied by the correction moment estimate.

theorem roughCoefficient_bound
    (hM : PublishedInputs.PrimeReciprocalMertensInput) (c : ℕ → ℝ)
    {z : ℝ} (hz : 0 ≤ z) (hzhalf : z ≤ 1 / 2) (ν : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ P : ℕ, 2 ≤ P → 1 ≤ Real.log P →
      |roughCoefficient c (Nat.primesLE P) z ν| ≤
        C * (Real.log P) ^ (Real.exp 1 + ν) := by
…

Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.roughCoefficient