RoughAuxiliaryExpansion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The moving-cutoff expansion on the manuscript's auxiliary scale

The remainder is uniform once log Y ≥ B^0.89. Its decay is derived from the explicit expansion, rather than assumed as an analytic input.

def OAI.JointDickman.roughErrorEnvelope line 17
theorem OAI.JointDickman.roughErrorEnvelope_tendsto line 23
theorem OAI.JointDickman.rough_error_at_auxiliaryCutoff line 47

theorem OAI.JointDickman.moving_rough_auxiliary_expansion line 75

Source documentation

The full untwisted moving-cutoff estimate, conditional only on the classical fixed-order expansion and the cited reciprocal-prime estimate.

theorem moving_rough_auxiliary_expansion
    (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, ∀ Y : ℝ,
        (B : ℝ) ^ (89 / 100 : ℝ) ≤ Real.log Y → 9 ≤ Y →
        |roughSquarefreeSummatory (Nat.primesLE (auxiliaryCutoff B)) z Y -
          Y * ∑ ν ∈ range (H + 1),
            roughCoefficient c (Nat.primesLE (auxiliaryCutoff B)) z ν *
              (Real.log Y) ^ (z - 1 - ν)| ≤ K * Y * (B : ℝ) ^ (-D) := by
…

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