Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-12 08:44 a8fdd990

View on Github →

feat(probability/moments): Chernoff bound on the upper/lower tail of a real random variable (#15129) For t nonnegative such that the cgf exists, ℙ(ε ≤ X) ≤ exp(-t*ε + cgf X ℙ t). We prove a similar result for the lower tail, as well as two corresponding versions using mgf instead of cgf.

Estimated changes

Modified src/analysis/special_functions/log/basic.lean

added theorem real.le_exp_log

Modified src/measure_theory/integral/bochner.lean

added theorem measure_theory.mul_meas_ge_le_integral_of_nonneg

Modified src/probability/moments.lean

modified def probability_theory.cgf

added theorem probability_theory.cgf_neg

modified theorem probability_theory.cgf_undef

modified theorem probability_theory.cgf_zero'

modified theorem probability_theory.cgf_zero_fun

added theorem probability_theory.measure_ge_le_exp_cgf

added theorem probability_theory.measure_ge_le_exp_mul_mgf

added theorem probability_theory.measure_le_le_exp_cgf

added theorem probability_theory.measure_le_le_exp_mul_mgf

modified def probability_theory.mgf

modified theorem probability_theory.mgf_const'

modified theorem probability_theory.mgf_const

added theorem probability_theory.mgf_neg

modified theorem probability_theory.mgf_pos'

modified theorem probability_theory.mgf_pos

modified theorem probability_theory.mgf_undef