feat: Fourier integral of Gaussians on inner product spaces (#11035)

Also rename (and deprecate) a few statements by changing `fourierTransform` to `fourierIntegral`: the Fourier transform for general L^2 functions is not given by the Fourier integral, so we should separate cleanly the two of them.

Mathlib/Analysis/SpecialFunctions/Gaussian.lean

@@ -8,6 +8,7 @@ import Mathlib.Analysis.SpecialFunctions.PolarCoord
 import Mathlib.Analysis.Convex.Complex
 import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.Analysis.Fourier.PoissonSummation
+import Mathlib.MeasureTheory.Integral.Pi
 
 #align_import analysis.special_functions.gaussian from "leanprover-community/mathlib"@"7982767093ae38cba236487f9c9dd9cd99f63c16"
 
@@ -24,11 +25,14 @@ We prove various versions of the formula for the Gaussian integral:
 We also prove, more generally, that the Fourier transform of the Gaussian is another Gaussian:
 
 * `integral_cexp_quadratic`: general formula for `∫ (x : ℝ), exp (b * x ^ 2 + c * x + d)`
-* `fourier_transform_gaussian`: for all complex `b` and `t` with `0 < re b`, we have
+* `fourierIntegral_gaussian`: for all complex `b` and `t` with `0 < re b`, we have
   `∫ x:ℝ, exp (I * t * x) * exp (-b * x^2) = (π / b) ^ (1 / 2) * exp (-t ^ 2 / (4 * b))`.
-* `fourier_transform_gaussian_pi`: a variant with `b` and `t` scaled to give a more symmetric
+* `fourierIntegral_gaussian_pi`: a variant with `b` and `t` scaled to give a more symmetric
   statement, and formulated in terms of the Fourier transform operator `𝓕`.
 
+We also give versions of these formulas in finite-dimensional inner product spaces, see
+`integral_cexp_neg_mul_sq_norm_add` and `fourierIntegral_gaussian_innerProductSpace`.
+
 As an application, in `Real.tsum_exp_neg_mul_int_sq` and `Complex.tsum_exp_neg_mul_int_sq`, we use
 Poisson summation to prove the identity
 `∑' (n : ℤ), exp (-π * a * n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), exp (-π / a * n ^ 2)`
@@ -40,7 +44,7 @@ noncomputable section
 
 open Real Set MeasureTheory Filter Asymptotics
 
-open scoped Real Topology FourierTransform
+open scoped Real Topology FourierTransform RealInnerProductSpace BigOperators
 
 open Complex hiding exp continuous_exp abs_of_nonneg sq_abs
 
@@ -394,10 +398,10 @@ set_option linter.uppercaseLean3 false in
 
 namespace GaussianFourier
 
-/-! ## Fourier transform of the Gaussian integral
+/-!
+## Fourier integral of Gaussian functions
 -/
 
-
 open intervalIntegral
 
 open scoped Real
@@ -567,15 +571,30 @@ theorem _root_.integral_cexp_quadratic (hb : b.re < 0) (c d : ℂ) :
   rw [integral_add_right_eq_self fun a : ℝ ↦ cexp (- -b * (↑a + ↑(c / (2 * b)).im * I) ^ 2),
     integral_cexp_neg_mul_sq_add_real_mul_I ((neg_re b).symm ▸ (neg_pos.mpr hb))]
 
-theorem _root_.fourier_transform_gaussian (hb : 0 < b.re) (t : ℂ) :
+lemma _root_.integrable_cexp_quadratic' (hb : b.re < 0) (c d : ℂ) :
+    Integrable (fun (x : ℝ) ↦ cexp (b * x ^ 2 + c * x + d)) := by
+  have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
+  by_contra H
+  simpa [hb', pi_ne_zero, Complex.exp_ne_zero, integral_undef H]
+    using integral_cexp_quadratic hb c d
+
+lemma _root_.integrable_cexp_quadratic (hb : 0 < b.re) (c d : ℂ) :
+    Integrable (fun (x : ℝ) ↦ cexp (-b * x ^ 2 + c * x + d)) := by
+  have : (-b).re < 0 := by simpa using hb
+  exact integrable_cexp_quadratic' this c d
+
+theorem _root_.fourierIntegral_gaussian (hb : 0 < b.re) (t : ℂ) :
     ∫ x : ℝ, cexp (I * t * x) * cexp (-b * x ^ 2) =
     (π / b) ^ (1 / 2 : ℂ) * cexp (-t ^ 2 / (4 * b)) := by
   conv => enter [1, 2, x]; rw [← Complex.exp_add, add_comm, ← add_zero (-b * x ^ 2 + I * t * x)]
   rw [integral_cexp_quadratic (show (-b).re < 0 by rwa [neg_re, neg_lt_zero]), neg_neg, zero_sub,
     mul_neg, div_neg, neg_neg, mul_pow, I_sq, neg_one_mul, mul_comm]
-#align fourier_transform_gaussian fourier_transform_gaussian
+#align fourier_transform_gaussian fourierIntegral_gaussian
 
-theorem _root_.fourier_transform_gaussian_pi' (hb : 0 < b.re) (c : ℂ) :
+@[deprecated] alias _root_.fourier_transform_gaussian :=
+  fourierIntegral_gaussian -- deprecated on 2024-02-21
+
+theorem _root_.fourierIntegral_gaussian_pi' (hb : 0 < b.re) (c : ℂ) :
     (𝓕 fun x : ℝ => cexp (-π * b * x ^ 2 + 2 * π * c * x)) = fun t : ℝ =>
     1 / b ^ (1 / 2 : ℂ) * cexp (-π / b * (t + I * c) ^ 2) := by
   haveI : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
@@ -595,11 +614,148 @@ theorem _root_.fourier_transform_gaussian_pi' (hb : 0 < b.re) (c : ℂ) :
     simp only [I_sq]
     ring
 
-theorem _root_.fourier_transform_gaussian_pi (hb : 0 < b.re) :
+@[deprecated] alias _root_.fourier_transform_gaussian_pi' :=
+  _root_.fourierIntegral_gaussian_pi' -- deprecated on 2024-02-21
+
+theorem _root_.fourierIntegral_gaussian_pi (hb : 0 < b.re) :
     (𝓕 fun (x : ℝ) ↦ cexp (-π * b * x ^ 2)) =
     fun t : ℝ ↦ 1 / b ^ (1 / 2 : ℂ) * cexp (-π / b * t ^ 2) := by
-  simpa only [mul_zero, zero_mul, add_zero] using fourier_transform_gaussian_pi' hb 0
-#align fourier_transform_gaussian_pi fourier_transform_gaussian_pi
+  simpa only [mul_zero, zero_mul, add_zero] using fourierIntegral_gaussian_pi' hb 0
+#align fourier_transform_gaussian_pi fourierIntegral_gaussian_pi
+
+@[deprecated] alias root_.fourier_transform_gaussian_pi :=
+  _root_.fourierIntegral_gaussian_pi   -- deprecated on 2024-02-21
+
+section InnerProductSpace
+
+variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
+  [MeasurableSpace V] [BorelSpace V]
+
+open scoped BigOperators
+
+theorem integrable_cexp_neg_sum_mul_add {ι : Type*} [Fintype ι] {b : ι → ℂ}
+    (hb : ∀ i, 0 < (b i).re) (c : ι → ℂ) :
+    Integrable (fun (v : ι → ℝ) ↦ cexp (- ∑ i, b i * (v i : ℂ) ^ 2 + ∑ i, c i * v i)) := by
+  simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]
+  apply Integrable.fintype_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v^2 + c i * v)) (fun i ↦ ?_)
+  convert integrable_cexp_quadratic (hb i) (c i) 0 using 3 with x
+  simp only [add_zero]
+
+theorem integrable_cexp_neg_mul_sum_add {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ι → ℂ) :
+    Integrable (fun (v : ι → ℝ) ↦ cexp (- b * ∑ i, (v i : ℂ) ^ 2 + ∑ i, c i * v i)) := by
+  simp_rw [neg_mul, Finset.mul_sum]
+  exact integrable_cexp_neg_sum_mul_add (fun _ ↦ hb) c
+
+theorem integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace
+    {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ℂ) (w : EuclideanSpace ℝ ι) :
+    Integrable (fun (v : EuclideanSpace ℝ ι) ↦ cexp (- b * ‖v‖^2 + c * ⟪w, v⟫)) := by
+  have := EuclideanSpace.volume_preserving_measurableEquiv ι
+  rw [← MeasurePreserving.integrable_comp_emb this.symm (MeasurableEquiv.measurableEmbedding _)]
+  simp only [neg_mul, Function.comp_def]
+  convert integrable_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 3 with v
+  simp only [EuclideanSpace.measurableEquiv, MeasurableEquiv.symm_mk, MeasurableEquiv.coe_mk,
+    EuclideanSpace.norm_eq, WithLp.equiv_symm_pi_apply, Real.norm_eq_abs, sq_abs, PiLp.inner_apply,
+    IsROrC.inner_apply, conj_trivial, ofReal_sum, ofReal_mul, Finset.mul_sum, neg_mul,
+    Finset.sum_neg_distrib, mul_assoc, add_left_inj, neg_inj]
+  norm_cast
+  rw [sq_sqrt]
+  · simp [Finset.mul_sum]
+  · exact Finset.sum_nonneg (fun i _hi ↦ by positivity)
+
+/-- In a real inner product space, the complex exponential of minus the square of the norm plus
+a scalar product is integrable. Useful when discussing the Fourier transform of a Gaussian. -/
+theorem integrable_cexp_neg_mul_sq_norm_add (hb : 0 < b.re) (c : ℂ) (w : V) :
+    Integrable (fun (v : V) ↦ cexp (-b * ‖v‖^2 + c * ⟪w, v⟫)) := by
+  let e := (stdOrthonormalBasis ℝ V).repr.symm
+  rw [← e.measurePreserving.integrable_comp_emb e.toHomeomorph.measurableEmbedding]
+  convert integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace
+    hb c (e.symm w) with v
+  simp only [neg_mul, Function.comp_apply, LinearIsometryEquiv.norm_map,
+    LinearIsometryEquiv.symm_symm, conj_trivial, ofReal_sum,
+    ofReal_mul, LinearIsometryEquiv.inner_map_eq_flip]
+
+theorem integral_cexp_neg_sum_mul_add {ι : Type*} [Fintype ι] {b : ι → ℂ}
+    (hb : ∀ i, 0 < (b i).re) (c : ι → ℂ) :
+    ∫ v : ι → ℝ, cexp (- ∑ i, b i * (v i : ℂ) ^ 2 + ∑ i, c i * v i)
+      = ∏ i, (π / b i) ^ (1 / 2 : ℂ) * cexp (c i ^ 2 / (4 * b i)) := by
+  simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]
+  rw [integral_fintype_prod_eq_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v ^ 2 + c i * v))]
+  congr with i
+  have : (-b i).re < 0 := by simpa using hb i
+  convert integral_cexp_quadratic this (c i) 0 using 1 <;> simp [div_neg]
+
+theorem integral_cexp_neg_mul_sum_add {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ι → ℂ) :
+    ∫ v : ι → ℝ, cexp (- b * ∑ i, (v i : ℂ) ^ 2 + ∑ i, c i * v i)
+      = (π / b) ^ (Fintype.card ι / 2 : ℂ) * cexp ((∑ i, c i ^ 2) / (4 * b)) := by
+  simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c]
+  simp only [one_div, Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum,
+    Fintype.card, Finset.sum_div]
+  rfl
+
+theorem integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace
+    {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ℂ) (w : EuclideanSpace ℝ ι) :
+    ∫ v : EuclideanSpace ℝ ι, cexp (- b * ‖v‖^2 + c * ⟪w, v⟫) =
+      (π / b) ^ (Fintype.card ι / 2 : ℂ) * cexp (c ^ 2 * ‖w‖^2 / (4 * b)) := by
+  have := (EuclideanSpace.volume_preserving_measurableEquiv ι).symm
+  rw [← this.integral_comp (MeasurableEquiv.measurableEmbedding _)]
+  simp only [neg_mul, Function.comp_def]
+  convert integral_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 5 with _x y
+  · simp only [EuclideanSpace.measurableEquiv, MeasurableEquiv.symm_mk, MeasurableEquiv.coe_mk,
+      EuclideanSpace.norm_eq, WithLp.equiv_symm_pi_apply, Real.norm_eq_abs, sq_abs, neg_mul,
+      neg_inj, mul_eq_mul_left_iff]
+    norm_cast
+    left
+    rw [sq_sqrt]
+    exact Finset.sum_nonneg (fun i _hi ↦ by positivity)
+  · simp [PiLp.inner_apply, EuclideanSpace.measurableEquiv, Finset.mul_sum, mul_assoc]
+  · simp only [EuclideanSpace.norm_eq, Real.norm_eq_abs, sq_abs, mul_pow, ← Finset.mul_sum]
+    congr
+    norm_cast
+    rw [sq_sqrt]
+    exact Finset.sum_nonneg (fun i _hi ↦ by positivity)
+
+theorem integral_cexp_neg_mul_sq_norm_add
+    (hb : 0 < b.re) (c : ℂ) (w : V) :
+    ∫ v : V, cexp (- b * ‖v‖^2 + c * ⟪w, v⟫) =
+      (π / b) ^ (FiniteDimensional.finrank ℝ V / 2 : ℂ) * cexp (c ^ 2 * ‖w‖^2 / (4 * b)) := by
+  let e := (stdOrthonormalBasis ℝ V).repr.symm
+  rw [← e.measurePreserving.integral_comp e.toHomeomorph.measurableEmbedding]
+  convert integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace
+    hb c (e.symm w) <;> simp [LinearIsometryEquiv.inner_map_eq_flip]
+
+theorem integral_cexp_neg_mul_sq_norm (hb : 0 < b.re) :
+    ∫ v : V, cexp (- b * ‖v‖^2) = (π / b) ^ (FiniteDimensional.finrank ℝ V / 2 : ℂ) := by
+  simpa using integral_cexp_neg_mul_sq_norm_add hb 0 (0 : V)
+
+theorem integral_rexp_neg_mul_sq_norm {b : ℝ} (hb : 0 < b) :
+    ∫ v : V, rexp (- b * ‖v‖^2) = (π / b) ^ (FiniteDimensional.finrank ℝ V / 2 : ℝ) := by
+  rw [← ofReal_inj]
+  convert integral_cexp_neg_mul_sq_norm (show 0 < (b : ℂ).re from hb) (V := V)
+  · change ofRealLI (∫ (v : V), rexp (-b * ‖v‖ ^ 2)) = ∫ (v : V), cexp (-↑b * ↑‖v‖ ^ 2)
+    rw [← ofRealLI.integral_comp_comm]
+    simp [ofRealLI]
+  · rw [← ofReal_div, ofReal_cpow (by positivity)]
+    simp
+
+theorem _root_.fourierIntegral_gaussian_innerProductSpace' (hb : 0 < b.re) (x w : V) :
+    𝓕 (fun v ↦ cexp (- b * ‖v‖^2 + 2 * π * Complex.I * ⟪x, v⟫)) w =
+      (π / b) ^ (FiniteDimensional.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖x - w‖ ^ 2 / b) := by
+  simp only [neg_mul, fourierIntegral_eq', ofReal_neg, ofReal_mul, ofReal_ofNat,
+    smul_eq_mul, ← Complex.exp_add, real_inner_comm w]
+  convert integral_cexp_neg_mul_sq_norm_add hb (2 * π * Complex.I) (x - w) using 3 with v
+  · congr 1
+    simp [inner_sub_left]
+    ring
+  · have : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
+    field_simp [mul_pow]
+    ring
+
+theorem _root_.fourierIntegral_gaussian_innerProductSpace (hb : 0 < b.re) (w : V) :
+    𝓕 (fun v ↦ cexp (- b * ‖v‖^2)) w =
+      (π / b) ^ (FiniteDimensional.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖w‖^2 / b) := by
+  simpa using fourierIntegral_gaussian_innerProductSpace' hb 0 w
+
+end InnerProductSpace
 
 end GaussianFourier
 
@@ -672,7 +828,7 @@ theorem Complex.tsum_exp_neg_quadratic {a : ℂ} (ha : 0 < a.re) (b : ℂ) :
     · exact continuous_const.mul (Complex.continuous_ofReal.pow 2)
     · exact continuous_const.mul Complex.continuous_ofReal
   have hFf : 𝓕 f = fun x : ℝ ↦ 1 / a ^ (1 / 2 : ℂ) * cexp (-π / a * (x + I * b) ^ 2) :=
-    fourier_transform_gaussian_pi' ha b
+    fourierIntegral_gaussian_pi' ha b
   have h1 : 0 < (↑π * a).re := by
     rw [re_ofReal_mul]
     exact mul_pos pi_pos ha

Mathlib/MeasureTheory/Integral/Pi.lean

@@ -8,14 +8,61 @@ import Mathlib.MeasureTheory.Constructions.Prod.Integral
 
 /-!
 # Integration with respect to a finite product of measures
+
+On a finite product of measure spaces, we show that a product of integrable functions each
+depending on a single coordinate is integrable, in `MeasureTheory.integrable_fintype_prod`, and
+that its integral is the product of the individual integrals,
+in `MeasureTheory.integral_fintype_prod_eq_prod`.
 -/
 
 open BigOperators Fintype MeasureTheory MeasureTheory.Measure
 
 variable {𝕜 : Type*} [IsROrC 𝕜]
 
+namespace MeasureTheory
+
+/-- On a finite product space in `n` variables, for a natural number `n`, a product of integrable
+functions depending on each coordinate is integrable. -/
+theorem Integrable.fin_nat_prod {n : ℕ} {E : Fin n → Type*}
+    [∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))]
+    {f : (i : Fin n) → E i → 𝕜} (hf : ∀ i, Integrable (f i)) :
+    Integrable (fun (x : (i : Fin n) → E i) ↦ ∏ i, f i (x i)) := by
+  induction n with
+  | zero => simp only [Nat.zero_eq, Finset.univ_eq_empty, Finset.prod_empty, volume_pi,
+      integrable_const_iff, one_ne_zero, pi_empty_univ, ENNReal.one_lt_top, or_true]
+  | succ n n_ih =>
+      have := ((measurePreserving_piFinSuccAbove (fun i => (volume : Measure (E i))) 0).symm)
+      rw [volume_pi, ← this.integrable_comp_emb (MeasurableEquiv.measurableEmbedding _)]
+      simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply,
+        Fin.prod_univ_succ, Fin.insertNth_zero]
+      simp only [Fin.zero_succAbove, cast_eq, Function.comp_def, Fin.cons_zero, Fin.cons_succ]
+      have : Integrable (fun (x : (j : Fin n) → E (Fin.succ j)) ↦ ∏ j, f (Fin.succ j) (x j)) :=
+        n_ih (fun i ↦ hf _)
+      exact Integrable.prod_mul (hf 0) this
+
+/-- On a finite product space, a product of integrable functions depending on each coordinate is
+integrable. Version with dependent target. -/
+theorem Integrable.fintype_prod_dep {ι : Type*} [Fintype ι] {E : ι → Type*}
+    {f : (i : ι) → E i → 𝕜} [∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))]
+    (hf : ∀ i, Integrable (f i)) :
+    Integrable (fun (x : (i : ι) → E i) ↦ ∏ i, f i (x i)) := by
+  let e := (equivFin ι).symm
+  simp_rw [← (volume_measurePreserving_piCongrLeft _ e).integrable_comp_emb
+    (MeasurableEquiv.measurableEmbedding _),
+    ← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Function.comp_def,
+    Equiv.piCongrLeft_apply_apply]
+  exact .fin_nat_prod (fun i ↦ hf _)
+
+/-- On a finite product space, a product of integrable functions depending on each coordinate is
+integrable. -/
+theorem Integrable.fintype_prod {ι : Type*} [Fintype ι] {E : Type*}
+    {f : ι → E → 𝕜} [MeasureSpace E] [SigmaFinite (volume : Measure E)]
+    (hf : ∀ i, Integrable (f i)) :
+    Integrable (fun (x : ι → E) ↦ ∏ i, f i (x i)) :=
+  Integrable.fintype_prod_dep hf
+
 /-- A version of **Fubini's theorem** in `n` variables, for a natural number `n`. -/
-theorem MeasureTheory.integral_fin_nat_prod_eq_prod {n : ℕ} {E : Fin n → Type*}
+theorem integral_fin_nat_prod_eq_prod {n : ℕ} {E : Fin n → Type*}
     [∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))]
     (f : (i : Fin n) → E i → 𝕜) :
     ∫ x : (i : Fin n) → E i, ∏ i, f i (x i) = ∏ i, ∫ x, f i x := by
@@ -37,15 +84,17 @@ theorem MeasureTheory.integral_fin_nat_prod_eq_prod {n : ℕ} {E : Fin n → Typ
         _ =  ∏ i, ∫ x, f i x := by rw [Fin.prod_univ_succ]
 
 /-- A version of **Fubini's theorem** with the variables indexed by a general finite type. -/
-theorem MeasureTheory.integral_fintype_prod_eq_prod (ι : Type*) [Fintype ι] {E : ι → Type*}
+theorem integral_fintype_prod_eq_prod (ι : Type*) [Fintype ι] {E : ι → Type*}
     (f : (i : ι) → E i → 𝕜) [∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))] :
     ∫ x : (i : ι) → E i, ∏ i, f i (x i) = ∏ i, ∫ x, f i x := by
   let e := (equivFin ι).symm
   rw [← (volume_measurePreserving_piCongrLeft _ e).integral_comp']
   simp_rw [← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Equiv.piCongrLeft_apply_apply,
     MeasureTheory.integral_fin_nat_prod_eq_prod]
 
-theorem MeasureTheory.integral_fintype_prod_eq_pow {E : Type*} (ι : Type*) [Fintype ι] (f : E → 𝕜)
+theorem integral_fintype_prod_eq_pow {E : Type*} (ι : Type*) [Fintype ι] (f : E → 𝕜)
     [MeasureSpace E] [SigmaFinite (volume : Measure E)] :
     ∫ x : ι → E, ∏ i, f (x i) = (∫ x, f x) ^ (card ι) := by
   rw [integral_fintype_prod_eq_prod, Finset.prod_const, card]
+
+end MeasureTheory

Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

@@ -40,6 +40,9 @@ We also show that a Lebesgue density point `x` of a set `s` (with respect to clo
 density one for the rescaled copies `{x} + r • t` of a given set `t` with positive measure, in
 `tendsto_addHaar_inter_smul_one_of_density_one`. In particular, `s` intersects `{x} + r • t` for
 small `r`, see `eventually_nonempty_inter_smul_of_density_one`.
+
+Statements on integrals of functions with respect to an additive Haar measure can be found in
+`MeasureTheory.Measure.Haar.NormedSpace`.
 -/
 
 assert_not_exists MeasureTheory.integral
@@ -335,6 +338,16 @@ theorem addHaar_image_continuousLinearEquiv (f : E ≃L[ℝ] E) (s : Set E) :
   μ.addHaar_image_linearMap (f : E →ₗ[ℝ] E) s
 #align measure_theory.measure.add_haar_image_continuous_linear_equiv MeasureTheory.Measure.addHaar_image_continuousLinearEquiv
 
+theorem LinearMap.quasiMeasurePreserving (f : E →ₗ[ℝ] E) (hf : LinearMap.det f ≠ 0) :
+    QuasiMeasurePreserving f μ μ := by
+  refine ⟨f.continuous_of_finiteDimensional.measurable, ?_⟩
+  rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]
+  exact smul_absolutelyContinuous
+
+theorem ContinuousLinearMap.quasiMeasurePreserving (f : E →L[ℝ] E) (hf : f.det ≠ 0) :
+    QuasiMeasurePreserving f μ μ :=
+  LinearMap.quasiMeasurePreserving μ (f : E →ₗ[ℝ] E) hf
+
 /-!
 ### Basic properties of Haar measures on real vector spaces
 -/
@@ -351,6 +364,12 @@ theorem map_addHaar_smul {r : ℝ} (hr : r ≠ 0) :
   simp only [f, map_linearMap_addHaar_eq_smul_addHaar μ hf, mul_one, LinearMap.det_smul, map_one]
 #align measure_theory.measure.map_add_haar_smul MeasureTheory.Measure.map_addHaar_smul
 
+theorem quasiMeasurePreserving_smul {r : ℝ} (hr : r ≠ 0) :
+    QuasiMeasurePreserving (r • ·) μ μ := by
+  refine ⟨measurable_const_smul r, ?_⟩
+  rw [map_addHaar_smul μ hr]
+  exact smul_absolutelyContinuous
+
 @[simp]
 theorem addHaar_preimage_smul {r : ℝ} (hr : r ≠ 0) (s : Set E) :
     μ ((r • ·) ⁻¹' s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)⁻¹) * μ s :=