Structure ProbabilityTheory.HasSubgaussianMGF

Modification history

2025-03-11 17:38

Mathlib/Probability/Moments/SubGaussian.lean

feat(Probability): (conditionally) sub-Gaussian random variables (#22623) …

Added ProbabilityTheory.HasSubgaussianMGF View on Github →