Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion_bound

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:565 to 622

Source documentation

Principal-value reduction of Kadiri equation (11) from pointwise PV inversion and an explicit Tannery domination bound. The finite-window sum/integral exchange is proved in this file, and the final vertical-line reflection is the Dirichlet-series identity followed by t ↦ -t.

Exact Lean statement

theorem kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion_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))))
    {bound : ℕ → ℝ} (hbound_sum : Summable bound)
    (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)))‖ ≤ bound n) :
    let Φ : ℂ → ℂ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion_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))))    {bound : ℕ → ℝ} (hbound_sum : Summable bound)    (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)))‖ ≤ bound n) :    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  intro Φ  have hsummed :=    kadiri_thm_3_1_q1_eq_11_summed_pv_of_pointwise_inversion_bound      (φ := φ) (a := a) hinv hbound_sum hbound  have hneg :      Tendsto        (fun T : ℝ =>          (1 / (2 * (Real.pi : ℂ))) *            ∫ t in (-T)..T,              (∑' n : ℕ,                  (Λ n : ℂ) *                    (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) *                Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))        atTop        (𝓝 (∑' n : ℕ, (Λ n : ℂ) * φ (Real.log n))) := by    dsimp only at hsummed    refine hsummed.congr' ?_    filter_upwards with T    exact kadiri_eq11_truncated_mellin_swap      (φ := φ) hφ (b := b) hb hφ_decay (a := a) ha hab T  exact kadiri_eq11_pv_positive_line_of_negative_line_pv    (φ := φ) hφ (b := b) hb hφ_decay hφ'_decay (a := a) ha hab ha1 hneg