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

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.