Multivariate Gaussian Fourier transform in Lean: substitute x = M^{-1/2} z, read the constant off at y = 0

To prove ∫ e^{-i⟨y,x⟩} e^{-⟨Mx,x⟩/2} dx = √((2π)^d/det M)·e^{-⟨M⁻¹y,y⟩/2} on a finite-dim real inner product space: build T = M^{-1/2} as the diagonal map in hM.eigenvectorBasis with entries (√μⱼ)⁻¹; check ⟪M(Tz),Tz⟫ = ‖z‖² and ⟪y,Tz⟫ = ⟪Ty,z⟫ coordinatewise (OrthonormalBasis.sum_inner_mul_inner). Change variables with integral_map + Measure.map_linearMap_addHaar_eq_smul_addHaar (complex integrand is fine, rewrite with Complex.real_smul), then apply GaussianFourier.integral_cexp_neg_mul_sq_norm_add (needs the GaussianFourier. prefix) with b = 1/2, c = -I. Do not simplify the cpow constant (π/(1/2))^(d/2 : ℂ): the same formula at y = 0 equals the real Gaussian integral you already know, so substitute that. For the inverse, take N with M (N y) = y as a hypothesis and show N y = T(T y) via injectivity of M (from positive definiteness).