Source indexedtheorem · leanprover/lean4:v4.32.0

sinc_kernel_tendsto_of_windowed_pv_of_pos_radius

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:2204 to 2246

Source documentation

Windowed principal-value convergence with the finite-window mass discharged by the scalar sinc limit.

Exact Lean statement

theorem sinc_kernel_tendsto_of_windowed_pv_of_pos_radius
    [CompleteSpace E] {f : ℝ → E} {x R : ℝ} (hR : 0 < R)
    (herrInt : ∀ᶠ T in Filter.atTop,
      IntervalIntegrable
        (fun u : ℝ =>
          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
            (f (x - u) - f x))
        volume (-R) R)
    (herror : Filter.Tendsto
      (fun T : ℝ =>
        ∫ u in (-R)..R,
          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
            (f (x - u) - f x))
      Filter.atTop (nhds 0))
    (htail : Filter.Tendsto
      (fun T : ℝ =>
        (∫ u : ℝ,
          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
            f (x - u)) -
          ∫ u in (-R)..R,
            (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
              f (x - u))
      Filter.atTop (nhds 0)) :
    Filter.Tendsto
      (fun T : ℝ =>
        (1 / (2 * π) : ℝ) •
          ∫ y : ℝ, (2 * T * Real.sinc (T * (x - y)) : ℂ) • f y)
      Filter.atTop (nhds (f x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem sinc_kernel_tendsto_of_windowed_pv_of_pos_radius    [CompleteSpace E] {f : ℝ → E} {x R : ℝ} (hR : 0 < R)    (herrInt : ∀ᶠ T in Filter.atTop,      IntervalIntegrable        (fun u : ℝ =>          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            (f (x - u) - f x))        volume (-R) R)    (herror : Filter.Tendsto      (fun T : ℝ =>        ∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            (f (x - u) - f x))      Filter.atTop (nhds 0))    (htail : Filter.Tendsto      (fun T : ℝ =>        (∫ u : ℝ,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            f (x - u)) -          ∫ u in (-R)..R,            (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •              f (x - u))      Filter.atTop (nhds 0)) :    Filter.Tendsto      (fun T : ℝ =>        (1 / (2 * π) : ℝ) •          ∫ y : ℝ, (2 * T * Real.sinc (T * (x - y)) : ℂ) • f y)      Filter.atTop (nhds (f x)) := by  have hmass : Filter.Tendsto      (fun T : ℝ =>        (∫ u in (-R)..R,          if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x)      Filter.atTop (nhds (f x)) :=    tendsto_intervalIntegral_sin_div_kernel_smul_of_scalar_mass (E := E) (f x)      (tendsto_intervalIntegral_sin_div_kernel_scalar_mass hR)  have hconst : ∀ᶠ T in Filter.atTop,      IntervalIntegrable        (fun u : ℝ =>          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x)        volume (-R) R := by    exact Filter.Eventually.of_forall fun T =>      intervalIntegrable_sin_div_kernel_smul_const (E := E) (f x) T (-R) R  exact sinc_kernel_tendsto_of_windowed_pv (E := E) hconst herrInt hmass herror htail