English
The Fourier integral converges for an L¹ input if and only if the input function is integrable; more generally, the equivalence holds under suitable continuity of the character and bilinear form.
Русский
Пределение Фурье сходится для функции в L¹ тогда и только тогда, когда функция интегрируема; более общо эквивалентно при существующих условиях непрерывности характеров и билинейной формы.
LaTeX
$$$$ \\text{Integrable}(f, \\mu) \\iff \\text{Integrable}(\\mathrm{fourierIntegral}(e,\\mu,L,f), \\text{...}). $$$$
Lean4
/-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint. -/
theorem integral_fourierIntegral_smul_eq_flip {f : V → ℂ} {g : W → F} (he : Continuous e)
(hL : Continuous fun p : V × W ↦ L p.1 p.2) (hf : Integrable f μ) (hg : Integrable g ν) :
∫ ξ, (fourierIntegral e μ L f ξ) • (g ξ) ∂ν = ∫ x, (f x) • (fourierIntegral e ν L.flip g x) ∂μ :=
integral_bilin_fourierIntegral_eq_flip (ContinuousLinearMap.lsmul ℂ ℂ) he hL hf hg
