RoughSelbergDelange.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Applying the published expansion inside the roughness convolution

The expansion is inserted only below the truncation, where its endpoint and logarithmic hypotheses hold. The complementary terms remain the actual convolution tail, already controlled by Rankin's bound.

def OAI.JointDickman.sdPolynomial line 19
def OAI.JointDickman.roughSquarefreeSummatory line 22

theorem OAI.JointDickman.square_root_truncation_conditions line 26

Source documentation

The usual square-root truncation meets both local expansion conditions.

theorem square_root_truncation_conditions {Y : ℝ} {V : ℕ}
    (hY : 9 ≤ Y) (hV : (V : ℝ) ^ 2 ≤ Y) :
    V ≤ ⌊Y⌋₊ ∧ ∀ v ∈ Ioc 0 V,
      3 ≤ Y / (v : ℝ) ∧ Real.log Y / 2 ≤ Real.log (Y / (v : ℝ)) := by
…

theorem OAI.JointDickman.roughSquarefreeSummatory_split line 45
theorem OAI.JointDickman.smallConvolution_SD_error line 58

theorem OAI.JointDickman.roughSelbergDelange_truncated line 101

Source documentation

Direct consequence of the published fixed-order expansion, with an explicit remaining tail and no assumed moving-cutoff estimate.

theorem roughSelbergDelange_truncated
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput) {z : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) :
    ∃ c : ℕ → ℝ, c 0 = squarefreeLeadingConstant z ∧ 0 < c 0 ∧
      ∀ H : ℕ, ∃ C : ℝ, 0 ≤ C ∧ ∀ (E : Finset ℕ) (Y : ℝ) (V : ℕ),
        1 < Y → V ≤ ⌊Y⌋₊ →
        (∀ v ∈ Ioc 0 V, 3 ≤ Y / (v : ℝ)) →
        (∀ v ∈ Ioc 0 V, Real.log Y / 2 ≤ Real.log (Y / (v : ℝ))) →
        |roughSquarefreeSummatory E z Y -
          Y * ∑ v ∈ Ioc 0 V, smoothCorrection E z v / (v : ℝ) *
            sdPolynomial c z H (Real.log (Y / v))| ≤
          C * Y * (Real.log Y / 2) ^ (z - 2 - H) *
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.squarefreeLeadingConstant, OAI.JointDickman.roughSquarefreeSummatory, OAI.JointDickman.smoothCorrection, OAI.JointDickman.sdPolynomial