Source indexedtheorem · leanprover/lean4:v4.32.0

norm_fourierInvTrunc_le_of_windowed_sin_div_bounds

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1053 to 1112

Source documentation

Windowed bound for finite-height Fourier inversion. The mass term, local principal-value window, and far-field tail are separated so applications can supply uniform bounds for the first two and use the built-in tail estimate.

Exact Lean statement

theorem norm_fourierInvTrunc_le_of_windowed_sin_div_bounds
    [CompleteSpace E]
    {f : ℝ → E} (hf : Integrable f) {x T R B L M : ℝ}
    (hT : 0 ≤ T) (hR : 0 < R)
    (hfx : ‖f x‖ ≤ B)
    (hmass : ‖∫ u in (-R)..R,
      if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)‖ ≤ M)
    (herr : IntervalIntegrable
      (fun u : ℝ =>
        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
          (f (x - u) - f x)) volume (-R) R)
    (hlocal : ‖∫ u in (-R)..R,
        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
          (f (x - u) - f x)‖ ≤ L) :
    ‖fourierInvTrunc (𝓕 f) x T‖ ≤
      M * B + L + (1 / (π * R)) * ∫ u : ℝ, ‖f u‖

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem norm_fourierInvTrunc_le_of_windowed_sin_div_bounds    [CompleteSpace E]    {f : ℝ → E} (hf : Integrable f) {x T R B L M : ℝ}    (hT : 0 ≤ T) (hR : 0 < R)    (hfx : ‖f x‖ ≤ B)    (hmass : ‖∫ u in (-R)..R,      if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)‖ ≤ M)    (herr : IntervalIntegrable      (fun u : ℝ =>        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •          (f (x - u) - f x)) volume (-R) R)    (hlocal : ‖∫ u in (-R)..R,        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •          (f (x - u) - f x)‖ ≤ L) :    ‖fourierInvTrunc (𝓕 f) x T‖ ≤      M * B + L + (1 / (π * R)) * ∫ u : ℝ, ‖f u‖ := by  let K : ℝ → ℂ := fun u =>    if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)  have hwhole : fourierInvTrunc (𝓕 f) x T = ∫ u : ℝ, K u • f (x - u) := by    rw [fourierInvTrunc_fourier_eq_sinc_kernel (E := E) hf x T hT]    simpa [K] using normalized_sinc_kernel_integral_comp_sub_left_sin_div_ae (E := E) f x T  have hconst : IntervalIntegrable (fun u : ℝ => K u • f x) volume (-R) R := by    simpa [K] using intervalIntegrable_sin_div_kernel_smul_const (E := E) (f x) T (-R) R  have hsplit := intervalIntegral_sin_div_kernel_split (E := E) f x T R hconst    (by simpa [K] using herr)  have hwindow_bound : ‖∫ u in (-R)..R, K u • f (x - u)‖ ≤ M * B + L := by    calc      ‖∫ u in (-R)..R, K u • f (x - u)‖          = ‖(∫ u in (-R)..R, K u) • f x +              ∫ u in (-R)..R, K u • (f (x - u) - f x)‖ := by            rw [show (∫ u in (-R)..R, K u • f (x - u)) =                (∫ u in (-R)..R, K u) • f x +                ∫ u in (-R)..R, K u • (f (x - u) - f x) by simpa [K] using hsplit]      _ ≤ ‖(∫ u in (-R)..R, K u) • f x‖ +            ‖∫ u in (-R)..R, K u • (f (x - u) - f x)‖ := norm_add_le _ _      _ ≤ M * B + L := by        have hM_nonneg : 0 ≤ M := le_trans (norm_nonneg _) hmass        have hterm : ‖(∫ u in (-R)..R, K u) • f x‖ ≤ M * B := by          rw [norm_smul]          exact mul_le_mul (by simpa [K] using hmass) hfx (norm_nonneg _) hM_nonneg        have hloc : ‖∫ u in (-R)..R, K u • (f (x - u) - f x)‖ ≤ L := by          simpa [K] using hlocal        linarith  have htail := norm_sin_div_kernel_tail_le_integral_norm (E := E) hf x T hR  rw [hwhole]  let W : E := ∫ u in (-R)..R, K u • f (x - u)  let Tail : E := (∫ u : ℝ, K u • f (x - u)) - W  have hdecomp : (∫ u : ℝ, K u • f (x - u)) = W + Tail := by    dsimp [W, Tail]    abel  calc    ‖∫ u : ℝ, K u • f (x - u)‖ = ‖W + Tail‖ := by rw [hdecomp]    _ ≤ ‖W‖ + ‖Tail‖ := norm_add_le _ _    _ ≤ (M * B + L) + (1 / (π * R)) * ∫ u : ℝ, ‖f u‖ := by      have hW : ‖W‖ ≤ M * B + L := by simpa [W] using hwindow_bound      have hTail : ‖Tail‖ ≤ (1 / (π * R)) * ∫ u : ℝ, ‖f u‖ := by        dsimp [Tail, W, K]        simpa [K] using htail      linarith    _ = M * B + L + (1 / (π * R)) * ∫ u : ℝ, ‖f u‖ := by ring