Diff — Fourier transform

Revision #1828 → #2345 · back to history

modifiedFourier transform (integral definition)4471d8abf2f8

Field	From #1828	To #2345
mathlib.decl	Fourier.fourierIntegral	Real.fourierIntegral_eq
note	`Fourier.fourierIntegral` (with the explicit unfolding `Real.fourierIntegral_eq`) defines the Fourier integral on ℝ via the standard additive character `Real.fourierChar`, exactly as in the article.	`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.
provenance	ai	ai-moderated

addedLinearity of the Fourier transform0c3f38f899bf

addedTime-shifting property of the Fourier transform22b1f9aef27a

addedFrequency-shifting (modulation) propertyb90a02e5d2d8

addedTime-scaling property of the Fourier transform513265805225

addedGaussian is its own Fourier transform2b7fa60c5fec

addedSchwartz function space13a9b913b87b

addedConvolution of functionscd4ba074fbc1

addedHaar measure on a locally compact groupba470108303c

addedHermite polynomials3da99d4054ed