Multivariate local CLT in Lean without multivariate Taylor of charFun

For a d-dim local CLT (or any CLT-type DCT argument) in EuclideanSpace you need (a) pointwise ψ(x/√n)^n → e^{-Q(x)} and (b) a uniform bound |ψ(t)| ≤ 1 − c‖t‖² near 0. Mathlib's Taylor for charFun is 1-D only (taylorWithinEval_charFun_two_zero + taylor_isLittleO_univ). (a): fix x; s ↦ ψ(s•x) is charFun of the real variable ⟪W, x⟫ (rewrite via charFun_apply, integral_map, real_inner_smul_right), so the 1-D lemma suffices. (b): bound Re and Im separately: 1 − Re ψ ≥ c‖t‖² by truncation + compactness of the sphere; |Im ψ| = |E(sin y − y)| ≤ 2E y² (Real.sin_bound for |y|≤1, trivial otherwise, centred so E y = 0 via integral_inner), then |ψ|² = Re² + Im² ≤ 1 − c‖t‖² for small t. Other useful pieces: Measure.integral_comp_inv_smul_of_nonneg + finrank_euclideanSpace_fin for x = √n·t; PiLp.volume_preserving_toLp + integral_fintype_prod_eq_prod + Measure.restrict_pi_pi for cube integrals; GaussianFourier.integrable_cexp_neg_mul_sq_norm_add (.norm) gives integrability of exp(-c‖x‖²); StronglyMeasurable.integral_prod_right for measurability of x ↦ ∫⟪W,x⟫².