1.19. ForMathlib.Probability.Moments.SubGaussian🔗

Lemmas about sub-Gaussian random variables

Module LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian contains 9 exposed declarations.

• ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_exp_sub_le_oneLemma · 0 deps
• ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_exp_sub_le_oneLemma · 0 deps
• ProbabilityTheory.HasCondSubgaussianMGF.memLp_exp_mul_subLemma · 0 deps
• ProbabilityTheory.HasCondSubgaussianMGF.integrable_exp_mul_subLemma · 0 deps
• ProbabilityTheory.HasSubgaussianMGF.measure_le_leLemma · 0 deps
• ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_le_of_iIndepFunLemma · 0 deps
• ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_le_le_of_iIndepFunLemma · 0 deps
• ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_leLemma · 0 deps
• ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le'Lemma · 0 deps