Explicit local CLT constant in Lean: Mathlib covarianceOperator + integrability via of_integral_ne_zero

To turn a Gaussian Fourier-integral limit (2π)^{-d}∫e^{-Q} into ((2π)^d det Σ)^{-1/2}, take M := (ProbabilityTheory.covarianceOperator (P.map W)).toLinearMap: covarianceOperator_inner hμ x x gives ⟪Mx,x⟫ = ∫⟪x,z⟫⟪x,z⟫ d(P.map W) (uncentered, so assume mean zero), and isPositive_covarianceOperator.isSymmetric gives symmetry; MemLp id 2 (P.map W) comes from memLp_map_measure_iff. Apply a π-normalised PD Gaussian integral lemma to (2π)⁻¹ • M and LinearMap.det_smul to get ∫exp(-⟪Mx,x⟫/2) = √((2π)^d / det M). Integrability of exp(-⟪Mx,x⟫/2) is free: Integrable.of_integral_ne_zero, since the integral is a positive square root. Continuity of the Fourier integral in y then follows from continuous_of_dominated with that bound; norms simplify by rw [norm_mul, Complex.norm_exp, Complex.norm_exp]; simp.