Revision #3233 → #3835 · back to history
modifiedFourier transform (integral definition)4471d8abf2f8
| Field | From #3233 | To #3835 |
|---|
| mathlib.decl | Real.fourier_real_eq | Fourier.fourierIntegral |
| note | `Real.fourierIntegral_eq` unfolds the real-variable Fourier transform `FourierTransform.fourier f w = ∫ v, Real.fourierChar (-⟪v,w⟫) • f v`, exactly the article's integral definition. | `Fourier.fourierIntegral e μ f w = ∫ v, e (-(v * w)) • f v ∂μ`; specialized with `Real.fourierChar` and Lebesgue measure this is exactly the article's integral formula (corrected: `Real.fourierIntegral` does not exist). |
modifiedFourier transform is an automorphism of the Schwartz space7ebc2bbc555e
| Field | From #3233 | To #3835 |
|---|
| mathlib.decl | SchwartzMap.fourierTransformCLE | SchwartzMap.fourierTransformCLM |
| note | `SchwartzMap.fourierTransformCLE` packages the Fourier transform on `𝓢(E, F)` as a continuous linear equivalence; by duality this gives an automorphism on the space of tempered distributions. | `SchwartzMap.fourierTransformCLM` packages the Fourier transform on `𝓢(V, E)` as a continuous linear map on the Schwartz space (corrected: `fourierTransformCLE` does not exist). |
modifiedPoisson summation formula889794b1eda9
| Field | From #3233 | To #3835 |
|---|
| mathlib.decl | Real.tsum_eq_tsum_fourierIntegral | Real.tsum_eq_tsum_fourier |
| note | Mathlib formalizes classical Poisson summation `∑ f(n) = ∑ 𝓕(f)(n)` under Schwartz-like hypotheses on `f`. | Mathlib formalizes classical Poisson summation `∑ f(n) = ∑ 𝓕(f)(n)` in `Real.tsum_eq_tsum_fourier` (corrected: `Real.tsum_eq_tsum_fourierIntegral` does not exist). |
modifiedRiesz–Thorin interpolation theorem979bc8c8db65
| Field | From #3233 | To #3835 |
|---|
| anchor.snippet | the Fourier transform can be defined on [MATH] by Riesz–Thorin interpolation | the Fourier transform can be defined on |
| provenance | ai | ai-moderated |
addedDiscrete-time Fourier transform (DTFT)0673c1c71d92
addedHeisenberg uncertainty principle (quantum mechanics)4005e97d5c84
addedFourier transform decays to zero on the real line for L¹ functions522be295f8a2