MovingRoughExpansion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The moving-cutoff expansion with explicit errors

The classical expansion, Taylor approximation, and correction-moment tails are now combined for the actual rough squarefree summatory function. No moving-cutoff asymptotic is used as an input.

def OAI.JointDickman.powerExpansionError line 19

theorem OAI.JointDickman.powerExpansionError_le line 28

Source documentation

For the nonpositive powers occurring here, the moment-tail sum is bounded by a single fixed logarithmic power.

theorem powerExpansionError_le {A C a L : ℝ} {H P V : ℕ}
    (hA : 0 ≤ A) (ha : a ≤ 0) (hL : 1 ≤ L)
    (hlog : 1 ≤ Real.log P) (hV : 0 < V) :
    powerExpansionError A C a H P V L ≤
      C * L ^ (a - (H + 1)) * (Real.log P) ^ (Real.exp 1 + (H + 1 : ℕ)) +
        A * (∑ k ∈ range (H + 1), |rpowShiftCoeff a k| * (k.factorial : ℝ) * 2 ^ k) *
          (Real.log P) ^ (Real.exp 1 + H) / (V : ℝ) ^ ((1 / Real.log P) / 2) := by
…

Mentions: OAI.JointDickman.powerExpansionError, OAI.JointDickman.rpowShiftCoeff

theorem OAI.JointDickman.correction_sdPolynomial_reindex line 72

theorem OAI.JointDickman.moving_rough_expansion_explicit line 91

Source documentation

The actual expansion with separately identified classical, Rankin, Taylor, and moment-tail errors. Its coefficients are the defined moments.

theorem moving_rough_expansion_explicit
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {z : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) :
    ∃ c : ℕ → ℝ, c 0 = squarefreeLeadingConstant z ∧ 0 < c 0 ∧
      ∃ A : ℝ, 0 < A ∧ ∀ H : ℕ, ∃ Csd : ℝ, ∃ C : ℕ → ℝ,
        0 ≤ Csd ∧ (∀ j, 0 ≤ C j) ∧ ∀ (P V : ℕ) (Y : ℝ),
          2 ≤ P → 1 ≤ Real.log P → 0 < V → 9 ≤ 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 - ν)| ≤
            Csd * Y * (Real.log Y / 2) ^ (z - 2 - H) *
…

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