SmoothCorrectionSeries.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The convergent correction series

The finite Euler factors used in removing the small primes are proved as identities of absolutely convergent series, including at the shifted exponent required by Rankin's bound.

def OAI.JointDickman.smoothDirichletTerm line 20
theorem OAI.JointDickman.smoothDirichletTerm_one line 23
theorem OAI.JointDickman.smoothDirichletTerm_mul line 27
theorem OAI.JointDickman.smoothDirichletTerm_prime_pow line 35
theorem OAI.JointDickman.smoothDirichletTerm_ratio_lt_one line 46
theorem OAI.JointDickman.smoothDirichletTerm_support line 58

theorem OAI.JointDickman.smoothCorrection_hasSum line 72

Source documentation

Absolute convergence and the signed Euler-factor identity.

theorem smoothCorrection_hasSum (E : Finset ℕ) {z s : ℝ}
    (hz : |z| < 1) (hs : 0 ≤ s) :
    Summable (fun n => ‖smoothDirichletTerm E z s n‖) ∧
      HasSum (smoothDirichletTerm E z s)
        (∏ p ∈ E with p.Prime, (1 + z / (p : ℝ) ^ s)⁻¹) := by
…

Mentions: OAI.JointDickman.smoothDirichletTerm

theorem OAI.JointDickman.smoothCorrection_zeroth_moment line 105

Source documentation

The zeroth correction moment is the inverse of the removed local factors.

theorem smoothCorrection_zeroth_moment (E : Finset ℕ) {z : ℝ} (hz : |z| < 1) :
    HasSum (fun n => smoothCorrection E z n / (n : ℝ))
      (∏ p ∈ E with p.Prime, (1 + z / (p : ℝ))⁻¹) := by
…

Mentions: OAI.JointDickman.smoothCorrection

theorem OAI.JointDickman.smoothDirichletTerm_abs line 115

theorem OAI.JointDickman.smoothCorrection_abs_hasSum line 123

Source documentation

The absolute correction moment is a finite product of positive geometric factors.

theorem smoothCorrection_abs_hasSum (E : Finset ℕ) {z s : ℝ}
    (hz : 0 ≤ z) (hz1 : z < 1) (hs : 0 ≤ s) :
    HasSum (fun n => |smoothCorrection E z n| / (n : ℝ) ^ s)
      (∏ p ∈ E with p.Prime, (1 - z / (p : ℝ) ^ s)⁻¹) := by
…

Mentions: OAI.JointDickman.smoothCorrection

theorem OAI.JointDickman.smoothCorrection_abs_sum_le_exp line 139

Source documentation

An exponential bound for every finite truncation of the absolute series.

theorem smoothCorrection_abs_sum_le_exp (E S : Finset ℕ) {z s : ℝ}
    (hz : 0 ≤ z) (hzhalf : z ≤ 1 / 2) (hs : 0 ≤ s) :
    (∑ n ∈ S, |smoothCorrection E z n| / (n : ℝ) ^ s) ≤
      Real.exp (2 * z * ∑ p ∈ E with p.Prime, 1 / (p : ℝ) ^ s) := by
…

Mentions: OAI.JointDickman.smoothCorrection

theorem OAI.JointDickman.roughConvolutionTail_le_exp line 162

Source documentation

Rankin's truncation error with its correction moment explicitly eliminated.

theorem roughConvolutionTail_le_exp (E : Finset ℕ) {z ε : ℝ}
    (hz : 0 ≤ z) (hzhalf : z ≤ 1 / 2) (hε : 0 ≤ ε) (hε1 : ε ≤ 1)
    (N V : ℕ) (hV : 0 < V) :
    |roughConvolutionTail E z N V| ≤
      ((N : ℝ) / (V : ℝ) ^ ε) *
        Real.exp (2 * z * ∑ p ∈ E with p.Prime, 1 / (p : ℝ) ^ (1 - ε)) := by
…

Mentions: OAI.JointDickman.roughConvolutionTail