Theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_integrable_exp_mul

Modification history

2025-03-11 17:38
Mathlib/Probability/Moments/SubGaussian.lean
feat(Probability): (conditionally) sub-Gaussian random variables (#22623) …
Added ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_integrable_exp_mulView on Github →