Commit 2025-06-23 11:31 f609d634

View on Github →

feat(Probability): sum of sub-Gaussian random variables is sub-Gaussian (#26164) This PR continues the work from #25620. Original PR: https://github.com/leanprover-community/mathlib4/pull/25620

Estimated changes

Modified Mathlib/Probability/Kernel/Composition/MeasureComp.lean

added theorem MeasureTheory.Measure.ae_comp_iff

added theorem MeasureTheory.Measure.ae_comp_of_ae_ae

Modified Mathlib/Probability/Moments/SubGaussian.lean

added theorem ProbabilityTheory.HasSubgaussianMGF.add

added theorem ProbabilityTheory.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero

added theorem ProbabilityTheory.HasSubgaussianMGF.neg

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.add

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero'

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_memLp_exp_mul

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_pos_eq_zero_of_hasSubGaussianMGF_zero

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.neg