Theorem ProbabilityTheory.HasSubgaussianMGF.integrableExpSet_eq_univ

Modification history

2025-12-02 17:23
Mathlib/Probability/Moments/SubGaussian.lean
feat: properties of sub-Gaussian random variables (#31550) …
Added ProbabilityTheory.HasSubgaussianMGF.integrableExpSet_eq_univView on Github →