Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_thm_3_1_q1_eq_14_of_windowed_fourier_source_bounds

PrimeNumberTheoremAnd.IEANTN.KadiriEq14 · PrimeNumberTheoremAnd/IEANTN/KadiriEq14.lean:618 to 665

Source documentation

Kadiri-side bridge from windowed Fourier bounds to equation (14). It leaves only a source bound and a local principal-value window bound as application inputs; the mass and far-field tail are handled by LaplaceInversion.

Exact Lean statement

lemma kadiri_thm_3_1_q1_eq_14_of_windowed_fourier_source_bounds
    {φ : ℝ → ℂ} (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|))
    {a R B L M : ℝ} (ha : 0 < a) (hab : a < b) (ha1 : a < 1) (hR : 0 < R)
    (hsource : ∀ n : ℕ, n ≠ 0 → n ≠ 1 →
      ‖(fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) • φ y) (-Real.log n)‖ ≤ B)
    (hmass : ∀ᶠ T in Filter.atTop,
      ‖∫ u in (-R)..R,
        if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)‖ ≤ M)
    (hlocal : ∀ᶠ T in Filter.atTop, ∀ n : ℕ, n ≠ 0 → n ≠ 1 →
      ‖∫ u in (-R)..R,
          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) •
            ((fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) • φ y) (-Real.log n - u) -
              (fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) • φ y) (-Real.log n))‖ ≤ L) :
    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

lemma kadiri_thm_3_1_q1_eq_14_of_windowed_fourier_source_bounds    {φ : ℝ → ℂ} (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|))    {a R B L M : ℝ} (ha : 0 < a) (hab : a < b) (ha1 : a < 1) (hR : 0 < R)    (hsource : ∀ n : ℕ, n ≠ 0 → n ≠ 1 →      ‖(fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) • φ y) (-Real.log n)‖ ≤ B)    (hmass : ∀ᶠ T in Filter.atTop,      ‖∫ u in (-R)..R,        if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)‖ ≤ M)    (hlocal : ∀ᶠ T in Filter.atTop, ∀ n : ℕ, n ≠ 0 → n ≠ 1 →      ‖∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) •            ((fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) • φ y) (-Real.log n - u) -              (fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) • φ y) (-Real.log n))‖ ≤ L) :    Filter.Tendsto (fun T : ℝ ↦ kadiri_thm_3_1_q1_I_2 φ a T)      Filter.atTop      (nhds (-∑' n : ℕ, ((Λ n : ℂ) / (n : ℂ)) * φ (-Real.log n))) := by  let F : ℝ → ℂ := fun y => exp (-((a : ℂ) * (y : ℂ))) • φ y  have hF_int : Integrable F := by    have hF_mul :        Integrable (fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) * φ y) :=      kadiri_laplace_positive_line_weight_integrable hφ hφ_decay ha hab    simpa [F, smul_eq_mul] using hF_mul  refine kadiri_thm_3_1_q1_eq_14_of_uniform_fourier_inv_trunc_bound    hφ hb hφ_decay ha hab ha1    (M * B + L + (1 / (Real.pi * R)) * ∫ u : ℝ, ‖F u‖) ?_  filter_upwards [Filter.eventually_ge_atTop (0 : ℝ), hmass, hlocal] with    T hT hmassT hlocalT n hn h1  have hq : IntervalIntegrable      (fun u : ℝ =>        if u = 0 then 0 else (1 / (Real.pi * u) : ℂ) • (F (-Real.log n - u) -          F (-Real.log n)))      volume (-R) R := by    have hq0 := kadiri_laplace_line_local_quotient_integrable      (φ := φ) hφ a (-Real.log n) hR    simpa [F, smul_eq_mul] using hq0  have herr : IntervalIntegrable      (fun u : ℝ =>        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) •          (F (-Real.log n - u) - F (-Real.log n)))      volume (-R) R :=    intervalIntegrable_sin_div_kernel_error_of_intervalIntegrable_quotient      (E := ℂ) hq T  simpa [F] using    norm_fourierInvTrunc_le_of_windowed_sin_div_bounds (E := ℂ) hF_int hT hR      (hsource n hn h1) hmassT herr (hlocalT n hn h1)