Commit 2025-03-11 17:38 246c76f9

View on Github →

feat(Probability): (conditionally) sub-Gaussian random variables (#22623) Definitions of sub-Gaussian and conditionally sub-Gaussian, both as special cases of a definition of sub-Gaussian with respect to a kernel and a measure.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

added theorem MeasureTheory.toReal_prob_le_one

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

added theorem MeasureTheory.Measure.prodMkLeft_comp_compProd

Created Mathlib/Probability/Moments/SubGaussian.lean

added theorem ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_le

added theorem ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le

added theorem ProbabilityTheory.HasCondSubgaussianMGF.cgf_le

added theorem ProbabilityTheory.HasCondSubgaussianMGF.fun_zero

added theorem ProbabilityTheory.HasCondSubgaussianMGF.integrable_exp_mul

added theorem ProbabilityTheory.HasCondSubgaussianMGF.memLp_exp_mul

added theorem ProbabilityTheory.HasCondSubgaussianMGF.mgf_le

added theorem ProbabilityTheory.HasCondSubgaussianMGF.zero

added def ProbabilityTheory.HasCondSubgaussianMGF

added theorem ProbabilityTheory.HasSubgaussianMGF.aestronglyMeasurable

added theorem ProbabilityTheory.HasSubgaussianMGF.cgf_le

added theorem ProbabilityTheory.HasSubgaussianMGF.fun_zero

added theorem ProbabilityTheory.HasSubgaussianMGF.measure_ge_le

added theorem ProbabilityTheory.HasSubgaussianMGF.memLp_exp_mul

added theorem ProbabilityTheory.HasSubgaussianMGF.zero

added structure ProbabilityTheory.HasSubgaussianMGF

added theorem ProbabilityTheory.HasSubgaussianMGF_iff_kernel

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_aestronglyMeasurable

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_integrable_exp_mul

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_integrable_exp_mul

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.aestronglyMeasurable

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.cgf_le

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.congr

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.fun_zero

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.isFiniteMeasure

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le_exp_add

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_univ_le_one

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.memLp_exp_mul

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.zero

added structure ProbabilityTheory.Kernel.HasSubgaussianMGF

added theorem ProbabilityTheory.Kernel.HasSubgaussianMGF_congr

Modified docs/references.bib