Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.kadiri_thm_3_1_q1_eq_14_core

PrimeNumberTheoremAnd.IEANTN.KadiriEq14 · PrimeNumberTheoremAnd/IEANTN/KadiriEq14.lean:757 to 772

Mathematical statement

Exact Lean statement

theorem kadiri_thm_3_1_q1_eq_14_core
    {φ : ℝ → ℂ} (_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) :
    Filter.Tendsto (fun T : ℝ ↦ kadiri_thm_3_1_q1_I_2 φ a T)
      Filter.atTop
      (nhds (-∑' n : ℕ, ((Λ n : ℂ) / (n : ℂ)) * φ (-Real.log n)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem kadiri_thm_3_1_q1_eq_14_core    {φ : ℝ → ℂ} (_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) :    Filter.Tendsto (fun T : ℝ ↦ kadiri_thm_3_1_q1_I_2 φ a T)      Filter.atTop      (nhds (-∑' n : ℕ, ((Λ n : ℂ) / (n : ℂ)) * φ (-Real.log n))) := by  obtain ⟨L, hlocal⟩ :=    kadiri_laplace_positive_line_local_window_bound      (φ := φ) _hφ _hφ_decay _hφ'_decay _ha _hab (R := 1) (by norm_num)  exact kadiri_thm_3_1_q1_eq_14_of_windowed_fourier_local_bound    _hφ _hb _hφ_decay _ha _hab _ha1 (R := 1) (L := L) (by norm_num) hlocal