English
The Fourier transform CLE is a continuous linear equivalence (isomorphism) of the Schwartz space.
Русский
Четверть преобразование CLE является непрерывным линейным эквивалентом пространства Шварца (изоморфизм).
LaTeX
$$$ \mathrm{fourierTransformCLE}_{\mathbb{K}}: \mathcal{S}(V,E) \simeq_{\mathrm{CLM}} \mathcal{S}(V,E) $$$
Lean4
/-- The Fourier transform on a real inner product space, as a continuous linear equiv on the
Schwartz space. -/
noncomputable def fourierTransformCLE : 𝓢(V, E) ≃L[𝕜] 𝓢(V, E)
where
__ := fourierTransformCLM 𝕜
invFun := (compCLMOfContinuousLinearEquiv 𝕜 (LinearIsometryEquiv.neg ℝ (E := V))) ∘L (fourierTransformCLM 𝕜)
left_inv := by
intro f
ext x
change 𝓕 (𝓕 f) (-x) = f x
rw [← fourierIntegralInv_eq_fourierIntegral_neg,
Continuous.fourier_inversion f.continuous f.integrable (fourierTransformCLM 𝕜 f).integrable]
right_inv := by
intro f
ext x
change 𝓕 (fun x ↦ (𝓕 f) (-x)) x = f x
simp_rw [← fourierIntegralInv_eq_fourierIntegral_neg,
Continuous.fourier_inversion_inv f.continuous f.integrable (fourierTransformCLM 𝕜 f).integrable]
continuous_invFun := ContinuousLinearMap.continuous _
