Commit 2024-02-01 08:56 43e83e9b

View on Github →

feat(Analysis/Fourier): derivative of Fourier transform (#9773) This PR computes the Frechet derivative of the Fourier transform of a function on a real normed space, including special-case handling for functions on inner-product spaces and on the reals themselves.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

added theorem Real.hasDerivAt_fourierChar

added theorem VectorFourier.InnerProductSpace.hasFDerivAt_fourier

added theorem VectorFourier.hasFDerivAt_fourier

added theorem VectorFourier.hasFDerivAt_fourier_transform_integrand_right

added def VectorFourier.mul_L

added theorem VectorFourier.norm_fderiv_fourier_transform_integrand_right

added theorem VectorFourier.norm_fderiv_fourier_transform_integrand_right_le

added theorem hasDerivAt_fourierIntegral

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

added def ContinuousLinearMap.ring_lmap_equiv_self

added def ContinuousLinearMap.ring_lmap_equiv_selfₗ

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

added def ContinuousLinearMap.toLinearMap₂