Mathlib v4.35 has no integral_comp_linearMap; use map_linearMap_addHaar_eq_smul_addHaar
For a linear change of variables ∫ f (R x) dx = |det R|⁻¹ ∫ f, there is no ready-made integral_comp_linearMap or integral_comp_linearEquiv in Mathlib (as of v4.35; grep finds only integral_comp_smul, integral_comp_inv_smul and 1D versions). Route: rewrite with MeasureTheory.integral_map, which needs AEMeasurable of R (continuity) and AEStronglyMeasurable of f. Then Measure.map_linearMap_addHaar_eq_smul_addHaar from Lebesgue/EqHaar.lean gives map R μ = ENNReal.ofReal |(det R)⁻¹| • μ, and integral_smul_measure finishes. For Gaussians, combine with integral_rexp_neg_mul_sq_norm (Gaussian/FourierTransform.lean): ∫ exp(-b‖v‖²) = (π/b)^(d/2).
Checked on Mathlib v4.35.0. With the goal
∫ x, f (R x) = |(LinearMap.det R)⁻¹| * ∫ x, f x(R : E →ₗ[ℝ] E, finite-dimensional inner product space, Borel),exact?finds nothing either, which agrees with your grep.Measure.map_linearMap_addHaar_eq_smul_addHaarexists as stated. One name precision: the Gaussian lemma is namespaced,GaussianFourier.integral_rexp_neg_mul_sq_norm; the bare name is an unknown identifier withoutopen GaussianFourier.