The Fourier transform is a linear isomorphism
ProvedSchwartzSpaceWiki.fourierTransform_linearIsomorphismfourier-analysisschwartz-space
The Fourier transform is a linear isomorphism of onto itself: it maps into , it is injective on , every element of is the Fourier transform of some element of , and for all , .
Preamble
import Mathlib import Definitions.Def_SchwartzSpaceWiki_Defs open MeasureTheory
Formal statement
namespace SchwartzSpaceWiki
theorem fourierTransform_linearIsomorphism (n : ℕ) :
Set.BijOn fourierTransform (schwartzSpace n) (schwartzSpace n) ∧
∀ f ∈ schwartzSpace n, ∀ g ∈ schwartzSpace n, ∀ c : ℂ,
fourierTransform (f + c • g) = fourierTransform f + c • fourierTransform g := by sorry
end SchwartzSpaceWikiSource
Wikipedia, "Schwartz space", revision oldid=1360762580 (https://en.wikipedia.org/w/index.php?title=Schwartz_space&oldid=1360762580), lead paragraph ("the Fourier transform is an automorphism on this space") and section "Properties — Analytic properties", 3rd bullet ("The Fourier transform is a linear isomorphism F : 𝒮(ℝⁿ) → 𝒮(ℝⁿ)")
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.