Theorem ProbabilityTheory.HasSubgaussianMGF.integrable

Modification history

2025-12-02 17:23

Mathlib/Probability/Moments/SubGaussian.lean

feat: properties of sub-Gaussian random variables (#31550) …

Added ProbabilityTheory.HasSubgaussianMGF.integrable View on Github →