Source indexedtheorem · leanprover/lean4:v4.32.0

sinc_kernel_tendsto_of_windowed_pv

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:2110 to 2200

Source documentation

Windowed principal-value convergence for the sinc kernel. This avoids treating the non-integrable constant kernel mass as a whole-line Bochner integral: the remaining analytic work is split into a finite-window mass limit, a finite-window local error limit, and a tail-control limit.

Exact Lean statement

theorem sinc_kernel_tendsto_of_windowed_pv
    [CompleteSpace E] {f : ℝ → E} {x R : ℝ}
    (hconst : ∀ᶠ T in Filter.atTop,
      IntervalIntegrable
        (fun u : ℝ =>
          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x)
        volume (-R) 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)
    (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)))
    (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    [CompleteSpace E] {f : ℝ → E} {x R : ℝ}    (hconst : ∀ᶠ T in Filter.atTop,      IntervalIntegrable        (fun u : ℝ =>          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x)        volume (-R) 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)    (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)))    (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 hsplit : (fun T : ℝ =>      ∫ u in (-R)..R,        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •          f (x - u)) =ᶠ[Filter.atTop]      (fun T : ℝ =>        (∫ u in (-R)..R,          if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x +          ∫ u in (-R)..R,            (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •              (f (x - u) - f x)) := by    filter_upwards [hconst, herrInt] with T hconstT herrT    exact intervalIntegral_sin_div_kernel_split (E := E) f x T R hconstT herrT  have hwindowSum : Filter.Tendsto      (fun T : ℝ =>        (∫ u in (-R)..R,          if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x +          ∫ u in (-R)..R,            (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •              (f (x - u) - f x))      Filter.atTop (nhds (f x)) := by    simpa using hmass.add herror  have hwindow : Filter.Tendsto      (fun T : ℝ =>        ∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            f (x - u))      Filter.atTop (nhds (f x)) := by    exact hwindowSum.congr' hsplit.symm  have hwhole : Filter.Tendsto      (fun T : ℝ =>        ∫ u : ℝ,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            f (x - u))      Filter.atTop (nhds (f x)) := by    have hsum : Filter.Tendsto        (fun T : ℝ =>          (∫ u in (-R)..R,            (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •              f (x - u)) +            ((∫ 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 (f x)) := by      simpa using hwindow.add htail    refine hsum.congr' ?_    filter_upwards with T    abel  refine hwhole.congr' ?_  filter_upwards with T  exact (normalized_sinc_kernel_integral_comp_sub_left_sin_div_ae (E := E) f x T).symm