Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion_tannery_bound

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:628 to 670

Source documentation

Principal-value reduction with the explicit Tannery majorant expected from the finite-height inversion bound. The only domination input is the eventual uniform estimate by a constant multiple of the absolutely summable von Mangoldt line Λ n / n^(1+a).

Exact Lean statement

theorem kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion_tannery_bound
    {φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ)
    {b : ℝ} (hb : 0 < b)
    (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))
        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))
    (hφ'_decay : (fun x : ℝ ↦ deriv φ x * exp ((x : ℂ) / 2))
        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))
    {a : ℝ} (ha : 0 < a) (hab : a < b) (ha1 : a < 1)
    (hinv : ∀ n : Nat, 1 ≤ n →
      let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume
      Tendsto
        (fun T : ℝ =>
          (1 / (2 * (Real.pi : ℂ))) *
            ∫ t in (-T)..T,
              Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *
                (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))
        atTop (𝓝 (φ (Real.log n))))
    {C : ℝ}
    (hbound :
      ∀ᶠ T in atTop, ∀ n : ℕ,
        ‖(Λ n : ℂ) *
          ((1 / (2 * (Real.pi : ℂ))) *
            ∫ t in (-T)..T,
              (let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume
               Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *
                (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)))‖ ≤
          C * ‖(Λ n : ℂ) / (n : ℂ) ^ ((1 + a : ℝ) : ℂ)‖) :
    let Φ : ℂ → ℂ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion_tannery_bound    {φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ)    {b : ℝ} (hb : 0 < b)    (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))    (hφ'_decay : (fun x : ℝ ↦ deriv φ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))    {a : ℝ} (ha : 0 < a) (hab : a < b) (ha1 : a < 1)    (hinv : ∀ n : Nat, 1 ≤ n →      let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume      Tendsto        (fun T : ℝ =>          (1 / (2 * (Real.pi : ℂ))) *            ∫ t in (-T)..T,              Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *                (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))        atTop (𝓝 (φ (Real.log n))))    {C : ℝ}    (hbound :      ∀ᶠ T in atTop, ∀ n : ℕ,        ‖(Λ n : ℂ) *          ((1 / (2 * (Real.pi : ℂ))) *            ∫ t in (-T)..T,              (let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume               Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *                (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)))‖ ≤          C * ‖(Λ n : ℂ) / (n : ℂ) ^ ((1 + a : ℝ) : ℂ)‖) :    let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume    Tendsto      (fun T : ℝ =>        (1 / (2 * (Real.pi : ℂ))) *          ∫ t in (-T)..T,            (-deriv riemannZeta (((1 + a : ℝ) : ℂ) + (t : ℂ) * I) /                riemannZeta (((1 + a : ℝ) : ℂ) + (t : ℂ) * I)) *              Φ (-(((1 + a : ℝ) : ℂ) + (t : ℂ) * I)))      atTop      (𝓝 (∑' n : ℕ, (Λ n : ℂ) * φ (Real.log n))) := by  exact kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion_bound    (φ := φ) hφ (b := b) hb hφ_decay hφ'_decay    (a := a) ha hab ha1 hinv    (bound := fun n : ℕ => C * ‖(Λ n : ℂ) / (n : ℂ) ^ ((1 + a : ℝ) : ℂ)‖)    ((summable_norm_vonMangoldt_real_line ha).mul_left C)    hbound