Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:675 to 707

Source documentation

Principal-value reduction of Kadiri equation (11) from pointwise PV inversion. The Tannery domination bound is discharged from the Kadiri decay hypotheses via the finite-window Fourier/Laplace estimate.

Exact Lean statement

theorem kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion
    {φ : ℝ → ℂ} (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)))) :
    let Φ : ℂ → ℂ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion    {φ : ℝ → ℂ} (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)))) :    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  obtain ⟨C, hC⟩ :=    kadiri_eq11_tannery_bound      (φ := φ) hφ (b := b) hb hφ_decay hφ'_decay (a := a) ha hab  exact kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion_tannery_bound    (φ := φ) hφ (b := b) hb hφ_decay hφ'_decay    (a := a) ha hab ha1 hinv (C := C) hC