Source indexedtheorem · leanprover/lean4:v4.32.0

tendsto_intervalIntegral_sin_div_kernel_scalar_mass_of_dirichlet

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1174 to 1195

Source documentation

A normalized symmetric Dirichlet integral limit gives the scalar finite-window mass at every positive radius.

Exact Lean statement

theorem tendsto_intervalIntegral_sin_div_kernel_scalar_mass_of_dirichlet
    {R : ℝ} (hR : 0 < R)
    (hdir : Filter.Tendsto
      (fun A : ℝ =>
        (1 / (π : ℂ)) * ∫ v in (-A)..A,
          if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ))
      Filter.atTop (nhds (1 : ℂ))) :
    Filter.Tendsto
      (fun T : ℝ =>
        ∫ u in (-R)..R,
          if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ))
      Filter.atTop (nhds (1 : ℂ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem tendsto_intervalIntegral_sin_div_kernel_scalar_mass_of_dirichlet    {R : ℝ} (hR : 0 < R)    (hdir : Filter.Tendsto      (fun A : ℝ =>        (1 / (π : ℂ)) * ∫ v in (-A)..A,          if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ))      Filter.atTop (nhds (1 : ℂ))) :    Filter.Tendsto      (fun T : ℝ =>        ∫ u in (-R)..R,          if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ))      Filter.atTop (nhds (1 : ℂ)) := by  have hTR : Filter.Tendsto (fun T : ℝ => T * R) Filter.atTop Filter.atTop := by    simpa [mul_comm] using      ((Filter.tendsto_const_mul_atTop_of_pos (f := fun T : ℝ => T) hR).2        Filter.tendsto_id)  have hcomp := hdir.comp hTR  refine hcomp.congr' ?_  filter_upwards with T  rw [intervalIntegral_sin_div_kernel_scalar_mass_eq_scaled]  rw [show T * (-R) = -(T * R) by ring]  rfl