Commit 2026-01-15 11:10 4d6755cb

View on Github →

feat(Analysis/FourierSchwartz): the derivative of the Fourier transform (#33752) Calculate the derivative (fderiv and lineDerivOp) of the (inverse) Fourier transform. We also generalize evalCLM slightly and make it's arguments explicit.

Estimated changes

Modified Mathlib/Analysis/Distribution/FourierSchwartz.lean

added theorem SchwartzMap.fderivCLM_fourier_eq

added theorem SchwartzMap.fourierInv_apply_eq

added theorem SchwartzMap.fourierInv_lineDerivOp_eq

added theorem SchwartzMap.fourier_evalCLM_eq

added theorem SchwartzMap.fourier_fderivCLM_eq

added theorem SchwartzMap.fourier_lineDerivOp_eq

added theorem SchwartzMap.lineDerivOp_fourierInv_eq

added theorem SchwartzMap.lineDerivOp_fourier_eq

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

added theorem SchwartzMap.evalCLM_apply_apply

added theorem SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv

added theorem SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv

added theorem SchwartzMap.smulLeftCLM_fun_neg

Modified Mathlib/Analysis/Distribution/TemperateGrowth.lean

added theorem ContinuousLinearEquiv.hasTemperateGrowth