Commit 2024-02-28 07:04 e059984c

View on Github →

feat: the Fourier transform is self-adjoint (#10833) Also extend the notation 𝓕 for the Fourier transform to inner product spaces, introduce a notation 𝓕⁻ for the inverse Fourier transform, and generalize a few results from the real line to inner product spaces.

Estimated changes

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

modified theorem Real.continuous_fourierChar

modified theorem Real.fourierChar_apply

modified def Real.fourierIntegral

added def Real.fourierIntegralInv

added theorem Real.fourierIntegralInv_comp_linearIsometry

added theorem Real.fourierIntegralInv_eq'

added theorem Real.fourierIntegralInv_eq

added theorem Real.fourierIntegralInv_eq_fourierIntegral_neg

added theorem Real.fourierIntegral_comp_linearIsometry

deleted theorem Real.fourierIntegral_def

added theorem Real.fourierIntegral_eq'

added theorem Real.fourierIntegral_eq

deleted theorem Real.fourierIntegral_eq_integral_exp_smul

added theorem Real.fourierIntegral_real_eq

added theorem Real.fourierIntegral_real_eq_integral_exp_smul

added theorem VectorFourier.integral_bilin_fourierIntegral_eq_flip

added theorem VectorFourier.integral_fourierIntegral_smul_eq_flip

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

added theorem LinearIsometryEquiv.inner_map_eq_flip

added theorem flip_innerₗ

added def innerₗ

added theorem innerₗ_apply

Modified Mathlib/Analysis/SpecialFunctions/Gaussian.lean