Commit 2023-06-09 22:59 708e9902

View on Github →

feat: port Analysis.Fourier.FourierTransform (#4927)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Fourier/FourierTransform.lean

added def Fourier.fourierIntegral

added theorem Fourier.fourierIntegral_comp_add_right

added theorem Fourier.fourierIntegral_def

added theorem Fourier.fourierIntegral_smul_const

added theorem Fourier.norm_fourierIntegral_le_integral_norm

added theorem Real.continuous_fourierChar

added def Real.fourierChar

added theorem Real.fourierChar_apply

added def Real.fourierIntegral

added theorem Real.fourierIntegral_def

added theorem Real.fourierIntegral_eq_integral_exp_smul

added theorem Real.vector_fourierIntegral_eq_integral_exp_smul

added def VectorFourier.fourierIntegral

added theorem VectorFourier.fourierIntegral_add

added theorem VectorFourier.fourierIntegral_comp_add_right

added theorem VectorFourier.fourierIntegral_continuous

added theorem VectorFourier.fourierIntegral_smul_const

added theorem VectorFourier.fourier_integral_convergent_iff

added theorem VectorFourier.norm_fourierIntegral_le_integral_norm