norm_fourierIntegral_le_integral_norm

English

The norm of the Fourier integral at frequency w is bounded by the L¹-norm of f.

Русский

Норма преобразования Фурье в частоте w ограничена L¹-нормой функции f.

LaTeX

$$$$ \\| \\mathrm{fourierIntegral}(e, μ, f)(w) \\| \\\\le \\\\int |f(v)| \\, dμ(v). $$$$

Lean4

/-- The uniform norm of the Fourier transform of `f` is bounded by the `L¹` norm of `f`. -/
theorem norm_fourierIntegral_le_integral_norm (e : AddChar 𝕜 𝕊) (μ : Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) :
    ‖fourierIntegral e μ f w‖ ≤ ∫ x : 𝕜, ‖f x‖ ∂μ :=
  VectorFourier.norm_fourierIntegral_le_integral_norm _ _ _ _ _

Похожие утверждения