RoughCutoffTruncation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Choosing the roughness truncation

An integer square-root truncation turns the remaining Rankin error into an explicit exponential in the endpoint logarithm.

def OAI.JointDickman.roughTruncation line 18
theorem OAI.JointDickman.roughTruncation_bounds line 20
theorem OAI.JointDickman.roughTruncation_rankin line 47

theorem OAI.JointDickman.moving_rough_expansion_exponential line 63

Source documentation

The complete roughness expansion before substituting P = B^1000.

theorem moving_rough_expansion_exponential
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {z : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) :
    ∃ c : ℕ → ℝ, c 0 = squarefreeLeadingConstant z ∧ 0 < c 0 ∧
      ∀ H : ℕ, ∃ K : ℝ, 0 ≤ K ∧ ∀ (P : ℕ) (Y : ℝ),
        2 ≤ P → 1 ≤ Real.log P → 9 ≤ Y → 16 ≤ Real.log Y →
        |roughSquarefreeSummatory (Nat.primesLE P) z Y -
          Y * ∑ ν ∈ range (H + 1), roughCoefficient c (Nat.primesLE P) z ν *
            (Real.log Y) ^ (z - 1 - ν)| ≤
          Y * K * ((Real.log Y) ^ (z - 2 - H) *
            (Real.log P) ^ (Real.exp 1 + (H + 1 : ℕ)) +
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.squarefreeLeadingConstant, OAI.JointDickman.roughSquarefreeSummatory, OAI.JointDickman.roughCoefficient