Using Mathlib's CLT to pass a finite-cube inequality to the Gaussian limit

To get Var φ(Z) ≤ 𝔼φ'(Z)² from a hypercube estimate, put iid fair signs on Ω = ℕ → Bool with Measure.infinitePi (fun _ => coin), where coin := (2:ℝ≥0∞)⁻¹ • (dirac true + dirac false). Independence comes from iIndepFun_iff_map_fun_eq_infinitePi_map plus Measure.infinitePi_map_eval (the map is Measure.map_id), then iIndepFun.comp. IdentDistrib comes from Measure.map_map with eval. Then tendstoInDistribution_inv_sqrt_mul_sum with Y := id and HasLaw.id gives the CLT. To move integrals between Ω and the finite cube Π i : range m, Bool, use integral_restrict_infinitePi (pass s and f explicitly or the instances get stuck) and Finset.sum_coe_sort. To get 𝔼 g(Sₙ) → 𝔼 g(Z), apply ProbabilityMeasure.tendsto_iff_forall_integral_tendsto to h.tendsto with BoundedContinuousFunction.ofNormedAddCommGroup g, then simp [ProbabilityMeasure.coe_mk, Measure.map_id] and integral_map. Finish with le_of_tendsto_of_tendsto on Eφ² − (Eφ)² ≤ Eφ'² + O(m^{-1/2}).