[Merged by Bors] - feat: add some lemmas for Haar measures

Mathlib/LinearAlgebra/Basis.lean

@@ -356,6 +356,9 @@ theorem map_apply (i) : b.map f i = f (b i) :=
   rfl
 #align basis.map_apply Basis.map_apply
 
+theorem coe_map : (b.map f : ι → M') = f ∘ b :=
+  rfl
+
 end Map
 
 section MapCoeffs

Mathlib/MeasureTheory/Measure/Haar/Basic.lean

@@ -698,6 +698,14 @@ theorem haarMeasure_unique (μ : Measure G) [SigmaFinite μ] [IsMulLeftInvariant
 #align measure_theory.measure.haar_measure_unique MeasureTheory.Measure.haarMeasure_unique
 #align measure_theory.measure.add_haar_measure_unique MeasureTheory.Measure.addHaarMeasure_unique
 
+/-- Let `K₀ K₁ : TopologicalSpace.PositiveCompacts G`, then `K₁` defines the same Haar measure as
+`K₀` iff it has measure `1` for the Haar measure defined by `K₀`. -/
+@[to_additive]
+theorem haarMeasure_eq_iff (K₀ K₁ : TopologicalSpace.PositiveCompacts G) :
+    haarMeasure K₀ = haarMeasure K₁ ↔ (haarMeasure K₀) K₁ = 1 :=
+  ⟨fun h => h.symm ▸ haarMeasure_self,
+    fun h => by rw [haarMeasure_unique (haarMeasure K₀) K₁, h, one_smul]⟩
+
 example [LocallyCompactSpace G] (μ : Measure G) [IsHaarMeasure μ] (K₀ : PositiveCompacts G) :
     μ = μ K₀.1 • haarMeasure K₀ :=
   haarMeasure_unique μ K₀

Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

@@ -226,6 +226,24 @@ instance IsAddHaarMeasure_basis_addHaar (b : Basis ι ℝ E) : IsAddHaarMeasure
   rw [Basis.addHaar]; exact Measure.isAddHaarMeasure_addHaarMeasure _
 #align is_add_haar_measure_basis_add_haar IsAddHaarMeasure_basis_addHaar
 
+instance [TopologicalSpace.SecondCountableTopology E] (b : Basis ι ℝ E) :
+    SigmaFinite b.addHaar := by
+  rw [Basis.addHaar_def]; exact MeasureTheory.Measure.sigmaFinite_addHaarMeasure
+
+/-- Let `b` and `b'` two bases of `E`. The basis `b'` defines the same Haar measure as the basis
+`b` iff the parallelepiped defined by `b'` has measure `1` for the Haar measure defined by `b`. -/
+theorem Basis.addHaar_eq_iff {ι' : Type*} [Fintype ι'] [TopologicalSpace.SecondCountableTopology E]
+    {b : Basis ι ℝ E} {b' : Basis ι' ℝ E} :
+    b.addHaar = b'.addHaar ↔ b.addHaar b'.parallelepiped = 1 := by
+  rw [Basis.addHaar_def, Basis.addHaar_def]
+  exact Measure.addHaarMeasure_eq_iff b.parallelepiped b'.parallelepiped
+
+@[simp]
+theorem Basis.addHaar_reindex {ι ι' E : Type*} [Fintype ι] [Fintype ι'] [NormedAddCommGroup E]
+    [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι ℝ E) (e : ι ≃ ι') :
+    (b.reindex e).addHaar = b.addHaar := by
+  rw [Basis.addHaar, b.parallelepiped_reindex e, ← Basis.addHaar]
+
 theorem Basis.addHaar_self (b : Basis ι ℝ E) : b.addHaar (_root_.parallelepiped b) = 1 := by
   rw [Basis.addHaar]; exact addHaarMeasure_self
 #align basis.add_haar_self Basis.addHaar_self

Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

@@ -79,6 +79,34 @@ theorem Basis.parallelepiped_basisFun (ι : Type*) [Fintype ι] :
     · exact zero_le_one
 #align basis.parallelepiped_basis_fun Basis.parallelepiped_basisFun
 
+ /-- A parallelepiped can be expressed on the standard basis. -/
+ theorem Basis.parallelepiped_eq_map  {ι E : Type*} [Fintype ι] [NormedAddCommGroup E]
+    [NormedSpace ℝ E] (b : Basis ι ℝ E) :
+    b.parallelepiped = (TopologicalSpace.PositiveCompacts.piIcc01 ι).map b.equivFun.symm
+      b.equivFunL.symm.continuous b.equivFunL.symm.isOpenMap := by
+  rw [← Basis.parallelepiped_basisFun]
+  refine (congrArg _ ?_).trans (Basis.parallelepiped_map _ _)
+  classical
+  ext
+  simp only [map_apply, Pi.basisFun_apply, equivFun_symm_apply, LinearMap.stdBasis_apply',
+    Finset.sum_univ_ite]
+
+open MeasureTheory MeasureTheory.Measure
+
+theorem Basis.map_addHaar {ι E F : Type*} [Fintype ι] [NormedAddCommGroup E]
+    [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι ℝ E)
+    [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace.SecondCountableTopology F]
+    [SigmaCompactSpace F] [MeasurableSpace F] [BorelSpace F] (f : E ≃L[ℝ] F) :
+    map f b.addHaar = (b.map f.toLinearEquiv).addHaar := by
+  have : IsAddHaarMeasure (map f b.addHaar) :=
+  AddEquiv.isAddHaarMeasure_map b.addHaar f.toAddEquiv f.continuous f.symm.continuous
+  have : SigmaFinite (map f b.addHaar) := MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite _
+  rw [(map f b.addHaar).addHaarMeasure_unique (b.map f.toLinearEquiv).parallelepiped,
+    Measure.map_apply f.continuous.measurable (PositiveCompacts.isCompact _).measurableSet,
+    Basis.coe_parallelepiped, Basis.coe_map]
+  erw [← image_parallelepiped, f.toEquiv.preimage_image, addHaar_self]
+  rw [one_smul, Basis.addHaar]
+
 namespace MeasureTheory
 
 open Measure TopologicalSpace.PositiveCompacts FiniteDimensional

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -1890,6 +1890,9 @@ theorem coe_toHomeomorph (e : M₁ ≃SL[σ₁₂] M₂) : ⇑e.toHomeomorph = e
   rfl
 #align continuous_linear_equiv.coe_to_homeomorph ContinuousLinearEquiv.coe_toHomeomorph
 
+theorem isOpenMap (e : M₁ ≃SL[σ₁₂] M₂) : IsOpenMap e :=
+  (ContinuousLinearEquiv.toHomeomorph e).isOpenMap
+
 theorem image_closure (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) : e '' closure s = closure (e '' s) :=
   e.toHomeomorph.image_closure s
 #align continuous_linear_equiv.image_closure ContinuousLinearEquiv.image_closure