Commit 2024-02-12 10:30 e2abe9f3

View on Github →

feat: the Fourier transform of a Schwartz function is differentiable (#10268)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Distribution/FourierSchwartz.lean

added theorem SchwartzMap.hasFDerivAt_fourier

added theorem SchwartzMap.integrable

added theorem SchwartzMap.integrable_pow_mul

added def VectorFourier.mul_L_schwartz

added theorem VectorFourier.mul_L_schwartz_apply

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

added theorem ContinuousLinearMap.hasTemperateGrowth

added theorem Function.HasTemperateGrowth.const

added theorem Function.HasTemperateGrowth.of_fderiv

added theorem Function.HasTemperateGrowth.zero

Modified Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

modified theorem finite_integral_one_add_norm

modified theorem integrable_one_add_norm

modified theorem integrable_rpow_neg_one_add_norm_sq