Commit 2024-03-04 21:27 99969936

View on Github →

feat: Fourier integral of Gaussians on inner product spaces (#11035) Also rename (and deprecate) a few statements by changing fourierTransform to fourierIntegral: the Fourier transform for general L^2 functions is not given by the Fourier integral, so we should separate cleanly the two of them.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Gaussian.lean

added theorem GaussianFourier.integrable_cexp_neg_mul_sq_norm_add

added theorem GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace

added theorem GaussianFourier.integrable_cexp_neg_mul_sum_add

added theorem GaussianFourier.integrable_cexp_neg_sum_mul_add

added theorem GaussianFourier.integral_cexp_neg_mul_sq_norm

added theorem GaussianFourier.integral_cexp_neg_mul_sq_norm_add

added theorem GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace

added theorem GaussianFourier.integral_cexp_neg_mul_sum_add

added theorem GaussianFourier.integral_cexp_neg_sum_mul_add

added theorem GaussianFourier.integral_rexp_neg_mul_sq_norm

added theorem fourierIntegral_gaussian

added theorem fourierIntegral_gaussian_innerProductSpace'

added theorem fourierIntegral_gaussian_innerProductSpace

added theorem fourierIntegral_gaussian_pi'

added theorem fourierIntegral_gaussian_pi

deleted theorem fourier_transform_gaussian

deleted theorem fourier_transform_gaussian_pi'

deleted theorem fourier_transform_gaussian_pi

added theorem integrable_cexp_quadratic'

added theorem integrable_cexp_quadratic

Modified Mathlib/MeasureTheory/Integral/Pi.lean

added theorem MeasureTheory.Integrable.fin_nat_prod

added theorem MeasureTheory.Integrable.fintype_prod

added theorem MeasureTheory.Integrable.fintype_prod_dep

modified theorem MeasureTheory.integral_fin_nat_prod_eq_prod

modified theorem MeasureTheory.integral_fintype_prod_eq_pow

modified theorem MeasureTheory.integral_fintype_prod_eq_prod

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

added theorem MeasureTheory.Measure.ContinuousLinearMap.quasiMeasurePreserving

added theorem MeasureTheory.Measure.LinearMap.quasiMeasurePreserving

added theorem MeasureTheory.Measure.quasiMeasurePreserving_smul