Theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable

Modification history

2025-06-23 11:31
Mathlib/Probability/Moments/SubGaussian.lean
feat(Probability): sum of sub-Gaussian random variables is sub-Gaussian (#26164) …
Added ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurableView on Github →