Commit 2025-03-23 16:04 ff7c9298

View on Github →

feat: remove measurable assumptions in Azuma-Hoeffding inequality (#23070)

Estimated changes

Modified Mathlib/InformationTheory/KullbackLeibler/KLFun.lean

Modified Mathlib/MeasureTheory/Decomposition/IntegralRNDeriv.lean

added theorem MeasureTheory.Measure.integrable_toReal_rnDeriv

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

deleted theorem MeasureTheory.Measure.integrable_toReal_rnDeriv

Modified Mathlib/Probability/Independence/Basic.lean

deleted theorem ProbabilityTheory.IndepFun.ae_eq

added theorem ProbabilityTheory.IndepFun.comp₀

added theorem ProbabilityTheory.IndepFun.congr

added theorem ProbabilityTheory.iIndepFun.congr

added theorem ProbabilityTheory.iIndepFun.indepFun_div_div₀

added theorem ProbabilityTheory.iIndepFun.indepFun_div_left₀

added theorem ProbabilityTheory.iIndepFun.indepFun_div_right₀

added theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_not_mem₀

added theorem ProbabilityTheory.iIndepFun.indepFun_finset₀

added theorem ProbabilityTheory.iIndepFun.indepFun_mul_left₀

added theorem ProbabilityTheory.iIndepFun.indepFun_mul_mul₀

added theorem ProbabilityTheory.iIndepFun.indepFun_mul_right₀

added theorem ProbabilityTheory.iIndepFun.indepFun_prodMk_prodMk₀

added theorem ProbabilityTheory.iIndepFun.indepFun_prodMk₀

added theorem ProbabilityTheory.iIndepFun.indepFun_prod_range_succ₀

Modified Mathlib/Probability/Independence/Kernel.lean

deleted theorem ProbabilityTheory.Kernel.IndepFun.ae_eq

added theorem ProbabilityTheory.Kernel.IndepFun.comp₀

added theorem ProbabilityTheory.Kernel.IndepFun.congr'

added theorem ProbabilityTheory.Kernel.iIndepFun.comp₀

added theorem ProbabilityTheory.Kernel.iIndepFun.congr'

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div₀

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left₀

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right₀

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_not_mem₀

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset₀

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left₀

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul₀

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right₀

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk₀

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk₀

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ₀

Modified Mathlib/Probability/Integration.lean

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

added theorem MeasureTheory.AEStronglyMeasurable.ae_of_compProd

added theorem MeasureTheory.Measure.ae_integrable_of_integrable_comp

added theorem MeasureTheory.Measure.integrable_compProd_iff

added theorem MeasureTheory.Measure.integrable_compProd_snd_iff

added theorem MeasureTheory.Measure.integrable_integral_norm_of_integrable_comp

added theorem MeasureTheory.Measure.integral_compProd

added theorem MeasureTheory.Measure.setIntegral_compProd

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

deleted theorem MeasureTheory.Measure.ae_integrable_of_integrable_comp

deleted theorem MeasureTheory.Measure.integrable_compProd_snd_iff

deleted theorem MeasureTheory.Measure.integrable_integral_norm_of_integrable_comp

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

deleted theorem MeasureTheory.AEStronglyMeasurable.ae_of_compProd

deleted theorem MeasureTheory.Measure.integrable_compProd_iff

deleted theorem MeasureTheory.Measure.integral_compProd

deleted theorem MeasureTheory.Measure.setIntegral_compProd

Modified Mathlib/Probability/Kernel/Disintegration/Integral.lean

Modified Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean

Modified Mathlib/Probability/Moments/SubGaussian.lean

added theorem ProbabilityTheory.HasSubgaussianMGF.aemeasurable

added theorem ProbabilityTheory.HasSubgaussianMGF.congr

Modified Mathlib/Probability/StrongLaw.lean