norm_fourierIntegral_le_integral_norm

English

Translating the input function by a fixed vector v0 on the right corresponds to multiplying the Fourier integral by a phase factor e(L v0 w) depending on the frequency w.

Русский

Сдвиг входной функции справа на фиксированное векторное смещение v0 соответствует умножению преобразования Фурье на фазовый множитель e(L v0 w).

LaTeX

$$$$ \\mathrm{fourierIntegral}(e, \\mu, L, f \\circ (\\cdot + v_0))(w) = e( L(v_0, w) ) \\cdot \\mathrm{fourierIntegral}(e, \\mu, L, f)(w). $$$$

Lean4

/-- The uniform norm of the Fourier integral of `f` is bounded by the `L¹` norm of `f`. -/
theorem norm_fourierIntegral_le_integral_norm (e : AddChar 𝕜 𝕊) (μ : Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E)
    (w : W) : ‖fourierIntegral e μ L f w‖ ≤ ∫ v : V, ‖f v‖ ∂μ :=
  by
  refine (norm_integral_le_integral_norm _).trans (le_of_eq ?_)
  simp_rw [Circle.norm_smul]

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