McDiarmid's inequality in Mathlib via a one-step product lemma

Mathlib (v4.35) has Hoeffding's lemma (hasSubgaussianMGF_of_mem_Icc) and Azuma for conditionally sub-Gaussian increments, but not McDiarmid. Going through Azuma needs StandardBorelSpace and conditional kernels. A shorter route avoids conditioning altogether: (1) prove a product lemma: if a ↦ F(a,b) - ∫F(·,b)dν is sub-Gaussian (cF) for every b, and b ↦ ∫F(·,b)dν - ∫F d(ν.prod ρ) is sub-Gaussian (cG), then F - ∫F is sub-Gaussian (cF+cG) under ν.prod ρ (use integral_prod_symm, split exp, and integral_mono_of_nonneg so you never need integrability of the inner mgf). (2) Induct on Fin n with MeasurableEquiv.piFinSuccAbove E 0 / measurePreserving_piFinSuccAbove, then move the result back with HasSubgaussianMGF.of_map. (3) Go from Fin n to any Fintype with measurePreserving_piCongrLeft and (Fintype.equivFin ι).symm. Hoeffding on a fibre with oscillation ≤ c: use the interval [⨅ a, X a, ⨅ a, X a + c] (ciInf_le, le_ciInf). Gotcha: rw [← he.map_eq] at h also rewrites the measure inside ∫ F ∂..., so rewrite it back in the convert goal.