Commit 2025-11-14 11:51 952587cf

View on Github →

feat(Analysis): use new notation for Fourier transform on Schwartz functions and simplify presentation (#31114) Use the new notation for the Fourier transform and its inverse to clean up FourierSchwartz.

Use notation type class and Prop-type classes.
State all lemmas for the Fourier transform on SchwartzMap and not on the coercion to functions.
Add coercion lemmas.
Move FourierTransformCLE up in the file and use FourierEquiv from the abstract notation file.
Use the notation for the Fourier transform and the Schwartz functions in PoissonSummation.
Add my name to the authors list for this PR and the PR for Plancherel's theorem.
Some golfing

Estimated changes

Modified Mathlib/Analysis/Distribution/FourierSchwartz.lean

added theorem SchwartzMap.fourierInv_coe

added def SchwartzMap.fourierTransformCLE

modified theorem SchwartzMap.fourierTransformCLE_apply

modified theorem SchwartzMap.fourierTransformCLE_symm_apply

added def SchwartzMap.fourierTransformCLM

modified theorem SchwartzMap.fourierTransformCLM_apply

added theorem SchwartzMap.fourier_coe

deleted theorem SchwartzMap.fourier_inversion

deleted theorem SchwartzMap.fourier_inversion_inv

deleted theorem SchwartzMap.inner_fourierTransformCLM_toL2_eq

added theorem SchwartzMap.inner_fourier_toL2_eq

deleted theorem SchwartzMap.norm_fourierTransformCLM_toL2_eq

added theorem SchwartzMap.norm_fourier_toL2_eq

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

modified theorem SchwartzMap.tsum_eq_tsum_fourierIntegral