Theorem ProbabilityTheory.isGaussian_iff_charFunDual_eq

Modification history

2025-05-16 10:47
Mathlib/Probability/Distributions/Gaussian/Basic.lean
feat: define Gaussian measures in normed spaces (#24900) …
Added ProbabilityTheory.isGaussian_iff_charFunDual_eqView on Github →