Source indexedtheorem · leanprover/lean4:v4.32.0

sinc_kernel_tendsto_of_windowed_pv_of_local_quotient

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:2250 to 2289

Source documentation

Windowed principal-value convergence from local quotient integrability and tail control.

Exact Lean statement

theorem sinc_kernel_tendsto_of_windowed_pv_of_local_quotient
    [CompleteSpace E] {f : ℝ → E} {x R : ℝ} (hR : 0 < R)
    (hq : IntervalIntegrable
      (fun u : ℝ =>
        if u = 0 then 0 else (1 / (π * u) : ℂ) • (f (x - u) - f x))
      volume (-R) R)
    (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_local_quotient    [CompleteSpace E] {f : ℝ → E} {x R : ℝ} (hR : 0 < R)    (hq : IntervalIntegrable      (fun u : ℝ =>        if u = 0 then 0 else (1 / (π * u) : ℂ) • (f (x - u) - f x))      volume (-R) R)    (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 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 := by    exact Filter.Eventually.of_forall      (intervalIntegrable_sin_div_kernel_error_of_intervalIntegrable_quotient        (E := E) hq)  have 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) :=    tendsto_intervalIntegral_sin_div_kernel_error_of_intervalIntegrable_quotient      (E := E) hR hq  exact sinc_kernel_tendsto_of_windowed_pv_of_pos_radius (E := E) hR    herrInt herror htail