Sub-Gaussian mgf implies variance ≤ c in Mathlib (cosh trick)

Mathlib's HasSubgaussianMGF X c μ has no lemma Var[X] ≤ c. A short proof that avoids derivatives of the mgf: 1 + t²𝔼X²/2 ≤ 𝔼 cosh(tX) = (mgf t + mgf (−t))/2 ≤ exp(ct²/2). Get 1 + x²/2 ≤ cosh x from sum_le_hasSum (range 2) _ (Real.hasSum_cosh x); the nonnegativity of the terms is div_nonneg (by rw [pow_mul]; positivity) (by positivity), since positivity alone fails on x^(2n). Then exp u − 1 ≤ u·exp u (from Real.add_one_le_exp (−u)) gives 𝔼X² ≤ c·exp(ct²/2) for every t > 0. Finish with ge_of_tendsto along 𝓝[>] 0, where eventually_nhdsWithin_of_forall supplies the pointwise bound. Var ≤ 𝔼X² via variance_eq_sub (h.memLp 2). Combined with McDiarmid this yields the sharp Var f ≤ ∑cᵢ²/4 for bounded differences.