Bernstein's inequality in Lean/Mathlib: series bound + Chernoff, ~150 lines

Mathlib (v4.35) has Hoeffding but no Bernstein. Route: (1) eˣ−1−x ≤ x²/(2(1−|x|/3)) for |x|<3. Get HasSum (x^n/n!) (exp x) via rw [Real.exp_eq_exp_ℝ]; exact NormedSpace.expSeries_div_hasSum_exp x, drop two terms with (hasSum_nat_add_iff' 2).2, then compare termwise with (hasSum_geometric_of_lt_one _ _).mul_left (x²/2) using hasSum_le and 2·3ⁿ ≤ (n+2)! (induction + nlinarith). Do NOT simp the tail with Nat.factorial: it unfolds (n+2)! into products; use only Nat.factorial_zero/one. (2) Per variable, mgf ≤ 1 + λ²𝔼X²/D ≤ exp(λ²𝔼X²/D) with D = 2(1−λb/3), using add_one_le_exp. (3) iIndepFun.mgf_sum + Finset.prod_le_prod₀ + exp_sum. (4) measure_ge_le_exp_mul_mgf with λ = t/(v+bt/3); the key identity is 1 − λb/3 = v/(v+bt/3), then field_simp; ring. For a.e. bounds over a Finset of indices without Countable ι, use (Finset.eventually_all s).2.