Commit 2025-07-16 10:54 6e8affb6

View on Github →

feat(Probability): Hoeffding's lemma (#26744) Prove Hoeffding's lemma.

Estimated changes

Modified Mathlib/Analysis/Calculus/Taylor.lean

added theorem taylor_mean_remainder_lagrange_iteratedDeriv

Modified Mathlib/Probability/Moments/Basic.lean

added theorem ProbabilityTheory.integrable_exp_mul_of_mem_Icc

Modified Mathlib/Probability/Moments/MGFAnalytic.lean

added theorem ProbabilityTheory.exists_cgf_eq_iteratedDeriv_two_cgf_mul

Modified Mathlib/Probability/Moments/SubGaussian.lean

added theorem ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc