fourierIntegral_convergent_iff — Mathlib

English

For any w, the integrability of the weighted function v ↦ e^{-⟪v,w⟫} f(v) is equivalent to the integrability of f itself.

Русский

Для любого w корректно: Integrable (v ↦ e^{-⟪v,w⟫} • f(v)) μ ↔ Integrable f μ.

LaTeX

$$$\\operatorname{Integrable}\\big(v \\mapsto 𝐞^{-\\langle v,w\\rangle} \\cdot f(v)\\big)\\,\\mu \\quad\\Longleftrightarrow\\quad \\operatorname{Integrable}\\big(f\\big)\\,\\mu$$$

Lean4

@[simp]
theorem fourierIntegral_convergent_iff {μ : Measure V} {f : V → E} (w : V) :
    Integrable (fun v : V ↦ 𝐞 (-⟪v, w⟫) • f v) μ ↔ Integrable f μ :=
  fourierIntegral_convergent_iff' (innerSL ℝ) w

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