Commit 2024-03-24 09:17 2b282122

View on Github →

refactor(Analysis/Fourier): use AddChar machinery in FourierTransform (#11417) The file Analysis/Fourier/FourierTransform.lean predates the general approach to additive characters elsewhere in the library; this merges the two (getting rid of the rather kludgy notation e [x] in the process). I also rejigged some slow proofs, to make them compile slightly faster.

Estimated changes

Modified Mathlib/Analysis/Complex/Circle.lean

added theorem norm_circle_smul

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

modified def Fourier.fourierIntegral

modified theorem Fourier.fourierIntegral_comp_add_right

modified theorem Fourier.fourierIntegral_def

modified theorem Fourier.fourierIntegral_smul_const

modified theorem Fourier.norm_fourierIntegral_le_integral_norm

modified def Real.fourierChar

modified theorem Real.fourierChar_apply

modified def VectorFourier.fourierIntegral

modified theorem VectorFourier.fourierIntegral_add

modified theorem VectorFourier.fourierIntegral_comp_add_right

modified theorem VectorFourier.fourierIntegral_smul_const

modified theorem VectorFourier.norm_fourierIntegral_le_integral_norm

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

modified theorem Real.hasDerivAt_fourierChar

Modified Mathlib/Analysis/Fourier/Inversion.lean

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean