Commit 2024-04-06 17:15 85cbf2d0

View on Github →

feat: the Fourier transform a function with fast enough decay is smooth (#11776)

Estimated changes

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

added theorem ContDiff.fourierPowSMulRight

added theorem Continuous.fourierPowSMulRight

added theorem MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight

added theorem Real.contDiff_fourierIntegral

added theorem Real.iteratedDeriv_fourierIntegral

added theorem Real.iteratedFDeriv_fourierIntegral

added theorem VectorFourier.contDiff_fourierIntegral

added def VectorFourier.fourierPowSMulRight

added theorem VectorFourier.fourierPowSMulRight_apply

added theorem VectorFourier.fourierPowSMulRight_eq_comp

added theorem VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral

added theorem VectorFourier.integrable_fourierPowSMulRight

added theorem VectorFourier.iteratedFDeriv_fourierIntegral

added theorem VectorFourier.norm_fourierPowSMulRight_le