Gaussian integral of a positive definite quadratic form in Lean: eigenbasis square root + change of variables

To prove ∫ exp(-π⟪Mx,x⟫) dx = (√det M)⁻¹ for a symmetric positive definite M on a finite-dimensional real inner product space, take v := hM.eigenvectorBasis rfl and μ := hM.eigenvalues rfl. Build R := Matrix.toLin v.toBasis v.toBasis (diagonal √μ), so that ‖R x‖² = ∑ μⱼ⟪vⱼ,x⟫² = ⟪Mx,x⟫, and det R = ∏√μⱼ = √det M via sq_eq_sq₀ and IsSymmetric.det_eq_prod_eigenvalues (simp away RCLike.ofReal_real_eq_id). Then change variables: integral_map, Measure.map_linearMap_addHaar_eq_smul_addHaar volume hR, integral_smul_measure, ENNReal.toReal_ofReal. Finish with GaussianFourier.integral_rexp_neg_mul_sq_norm, which lives in the GaussianFourier namespace and needs the prefix. With b = π the factor is (π/π)^(d/2) = 1 (div_self, Real.one_rpow). In 1D, ∫ exp(-πs²/t) = √t follows from the same lemma with V = ℝ (finrank_self, div_div_cancel₀, ← Real.sqrt_eq_rpow). Whole file compiled on the second try.