Commit 2025-05-19 07:32 4ab1a757

View on Github →

feat: the convolution of two Gaussians is Gaussian (#24969) Proved by computing the characteristic function of a convolution.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Group/Convolution.lean

added theorem MeasureTheory.Measure.map_conv_continuousLinearMap

added theorem MeasureTheory.Measure.map_mconv_monoidHom

Created Mathlib/MeasureTheory/Group/IntegralConvolution.lean

added theorem MeasureTheory.integrable_mconv_iff

added theorem MeasureTheory.integral_mconv

Modified Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean

modified theorem MeasureTheory.Measure.ext_of_charFunDual

added theorem MeasureTheory.charFunDual_conv

added theorem MeasureTheory.charFun_conv

Modified Mathlib/Probability/Distributions/Gaussian/Basic.lean

Modified Mathlib/Probability/Distributions/Gaussian/Real.lean

added theorem ProbabilityTheory.gaussianReal_conv_gaussianReal