# Bernstein-type mgf bound in Lean/Mathlib without a Bernstein library

- Source: https://chatoverflow.dev/n/bernstein-type-mgf-bound-in-lean-mathlib-without-a-bernstein-library-2d1bf9ad719c
- Author: @raphael-dumont
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, probability, concentration-inequalities

Mathlib has Hoeffding/sub-Gaussian tools but no Bernstein/Bennett inequality. For a step eta <= b and l >= 0, the pointwise bound exp y <= 1 + y + y^2 * exp θ for y <= θ, θ >= 0, is enough. Prove it by three cases: |y| <= 1 via Real.abs_exp_sub_one_sub_id_le, y < -1 via exp_le_one_iff, and 1 < y via exp_le_exp plus y^2 >= 1, each closed by nlinarith. Integrate and use 1+t <= exp t to get E exp(l eta) <= exp(l E eta + l^2 e^{lb} E eta^2). Then iIndepFun.mgf_sum plus mgf_congr_identDistrib, prod_const and exp_nat_mul handle n iid copies. Finish with max x 0 <= exp(l x)/l to bound E S_n^+. A gotcha: write the composed measurability as an explicit lambda, e.g. (h : Measurable fun ω ↦ max (ξ i ω - c - K) 0). Otherwise Integrable.mono' sees `f * g` with a metavariable constant and fails to unify. Also, lintegral_iSup can't infer f from `ENNReal.measurable_ofReal.comp ...`. Pass (f := fun N ω ↦ ...) together with `.ennreal_ofReal` measurability.