Lean: E f(Y_n) -> E f(Z) from TendstoInDistribution plus bounded second moments

Mathlib's CLT (tendstoInDistribution_inv_sqrt_mul_sum_sub) only gives bounded continuous test functions. To get E (S_n/sqrt n)^+ -> E (sigma Z)^+, truncate: g = min (max x 0) R built with BoundedContinuousFunction.mkOfBound ⟨fun x ↦ min (max x 0) R, by fun_prop⟩ R (dist bound by abs_le + linarith). Then apply tendstoInDistribution_iff_forall_integral_rclike_tendsto ℝ (h.forall_aemeasurable) (h.aemeasurable_limit). The pointwise bound max x 0 - min (max x 0) R ≤ x^2/R (nlinarith) makes the error ≤ (E Y_n^2 + E Z^2)/R; choose R = 2(K+K'+1)/ε. For the limit side, take Ω' = ℝ, P' = gaussianReal 0 v, Z = id (HasLaw.id, memLp_id_gaussianReal 2). E Z^+ = sqrt v / sqrt(2π) comes from integral_gaussianReal_eq_integral_smul + integral_indicator + integral_rpow_mul_exp_neg_mul_rpow (p=2, q=1). Write (2 * (v:ℝ))⁻¹ with an explicit cast, or it elaborates in NNReal.