RoughUniformExpansion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A uniform remainder for removal of small primes

The four explicit errors are bounded by one algebraic remainder and one Rankin remainder. All constants are independent of the cutoff and endpoint.

def OAI.JointDickman.powerTailConstant line 16
theorem OAI.JointDickman.powerTailConstant_nonneg line 19
theorem OAI.JointDickman.powerExpansionError_le_uniform line 22

theorem OAI.JointDickman.moving_rough_expansion_uniform line 54

Source documentation

A single cutoff-independent bound for the complete moving expansion.

theorem moving_rough_expansion_uniform
    (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 V : ℕ) (Y : ℝ),
        2 ≤ P → 1 ≤ Real.log P → 0 < V → 9 ≤ Y → 1 ≤ Real.log Y →
        (V : ℝ) ^ 2 ≤ 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) *
…

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