Theorem ProbabilityTheory.integrableExpSet_fun_id_gaussianReal

Modification history

2025-05-16 07:16
Mathlib/Probability/Distributions/Gaussian.lean
feat: moments of a real Gaussian distribution (#24834) …
Added ProbabilityTheory.integrableExpSet_fun_id_gaussianRealView on Github →