Theorem ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc

Modification history

2025-07-16 10:54
Mathlib/Probability/Moments/SubGaussian.lean
feat(Probability): Hoeffding's lemma (#26744) …
Added ProbabilityTheory.hasSubgaussianMGF_of_mem_IccView on Github →