New version

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/OfBasis.lean

@@ -203,6 +203,15 @@ theorem Basis.parallelepiped_reindex (b : Basis ι ℝ E) (e : ι ≃ ι') :
     (congr_arg _root_.parallelepiped (b.coe_reindex e)).trans (parallelepiped_comp_equiv b e.symm)
 #align basis.parallelepiped_reindex Basis.parallelepiped_reindex
 
+theorem Basis.mem_parallelepiped [DecidableEq ι] {b : Basis ι ℝ E} {a : E} :
+    a ∈ (b.parallelepiped : Set E) ↔ ∀ i, b.repr a i ∈ Set.Icc 0 1 := by
+  simp_rw [coe_parallelepiped, mem_parallelepiped_iff, Set.mem_Icc, Pi.le_def, ← forall_and]
+  refine ⟨?_, fun h => ⟨b.repr a, fun i => h i, (b.sum_repr a).symm⟩⟩
+  rintro ⟨_, h, rfl⟩ i
+  simpa only [LinearEquiv.map_sum, SMulHomClass.map_smul, repr_self, Finsupp.smul_single,
+    smul_eq_mul, mul_one, Finset.sum_apply', Finsupp.single_apply, Finset.sum_ite_eq',
+    Finset.mem_univ, ite_true] using h i
+
 theorem Basis.parallelepiped_map (b : Basis ι ℝ E) (e : E ≃ₗ[ℝ] F) :
     (b.map e).parallelepiped = b.parallelepiped.map e
     (have := FiniteDimensional.of_fintype_basis b
@@ -226,10 +235,46 @@ 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
+
 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
 
+theorem Basis.parallelepiped_measurable [DecidableEq ι] (b : Basis ι ℝ E) :
+    MeasurableSet (b.parallelepiped : Set E) := by
+  have : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b
+  rw [show b.parallelepiped = b.equivFun.toLinearMap ⁻¹'
+      (Set.pi Set.univ fun _ : ι => Set.Icc (0 : ℝ) 1) by
+    ext; simp only [Basis.mem_parallelepiped, Set.mem_Icc, forall_and, LinearEquiv.coe_coe,
+      Pi.le_def, Set.pi_univ_Icc, Set.mem_preimage, equivFun_apply]]
+  refine measurableSet_preimage (LinearMap.continuous_of_finiteDimensional _).measurable ?_
+  exact MeasurableSet.pi Set.countable_univ fun _ _ => measurableSet_Icc
+
+theorem Basis.addHaar_eq  {ι' : Type*} [Fintype ι'] [TopologicalSpace.SecondCountableTopology E]
+    {b : Basis ι ℝ E} {b' : Basis ι' ℝ E} :
+    b.addHaar = b'.addHaar ↔ b.addHaar b'.parallelepiped = 1 :=
+  ⟨fun h => h ▸ Basis.addHaar_self b',
+    fun h => by rw [addHaarMeasure_unique b.addHaar b'.parallelepiped, h, one_smul, addHaar]⟩
+
+theorem Basis.addHaar_map {F : Type*} [DecidableEq ι] (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 _
+  convert (map f b.addHaar).addHaarMeasure_unique (b.map f.toLinearEquiv).parallelepiped
+  suffices (map f b.addHaar) ((b.map f.toLinearEquiv)).parallelepiped = 1 by
+    rw [this, one_smul, Basis.addHaar]
+  rw [Measure.map_apply f.continuous.measurable (parallelepiped_measurable (b.map f.toLinearEquiv)),
+    Basis.coe_parallelepiped, Basis.coe_map]
+  erw [← image_parallelepiped f.toLinearMap b, Equiv.preimage_image f.toEquiv _]
+  exact addHaar_self b
+
 end NormedSpace
 
 /-- A finite dimensional inner product space has a canonical measure, the Lebesgue measure giving

Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
 import Mathlib.MeasureTheory.Measure.Haar.NormedSpace
 
 #align_import measure_theory.measure.lebesgue.complex from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
@@ -24,11 +25,6 @@ noncomputable section
 
 namespace Complex
 
-/-- Lebesgue measure on `ℂ`. -/
-instance measureSpace : MeasureSpace ℂ :=
-  ⟨Measure.map basisOneI.equivFun.symm volume⟩
-#align complex.measure_space Complex.measureSpace
-
 /-- Measurable equivalence between `ℂ` and `ℝ² = Fin 2 → ℝ`. -/
 def measurableEquivPi : ℂ ≃ᵐ (Fin 2 → ℝ) :=
   basisOneI.equivFun.toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv
@@ -39,14 +35,20 @@ def measurableEquivRealProd : ℂ ≃ᵐ ℝ × ℝ :=
   equivRealProdClm.toHomeomorph.toMeasurableEquiv
 #align complex.measurable_equiv_real_prod Complex.measurableEquivRealProd
 
-theorem volume_preserving_equiv_pi : MeasurePreserving measurableEquivPi :=
-  (measurableEquivPi.symm.measurable.measurePreserving _).symm _
+@[simp]
+theorem measurableEquivRealProd_apply (a : ℂ) : measurableEquivRealProd a = (a.re, a.im) := rfl
+
+theorem volume_preserving_equiv_pi : MeasurePreserving measurableEquivPi := by
+  convert (measurableEquivPi.symm.measurable.measurePreserving volume).symm
+  rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar,
+    measurableEquivPi, Homeomorph.toMeasurableEquiv_symm_coe,
+    ContinuousLinearEquiv.coe_toHomeomorph_symm, ← LinearEquiv.coe_toContinuousLinearEquiv_symm',
+    Basis.addHaar_map]
+  exact Basis.addHaar_eq.mpr Complex.orthonormalBasisOneI.volume_parallelepiped
 #align complex.volume_preserving_equiv_pi Complex.volume_preserving_equiv_pi
 
 theorem volume_preserving_equiv_real_prod : MeasurePreserving measurableEquivRealProd :=
   (volume_preserving_finTwoArrow ℝ).comp volume_preserving_equiv_pi
 #align complex.volume_preserving_equiv_real_prod Complex.volume_preserving_equiv_real_prod
 
-instance : Measure.IsAddHaarMeasure (@volume ℂ _) := Measure.MapLinearEquiv.isAddHaarMeasure _ _
-
 end Complex

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -1890,6 +1890,10 @@ theorem coe_toHomeomorph (e : M₁ ≃SL[σ₁₂] M₂) : ⇑e.toHomeomorph = e
   rfl
 #align continuous_linear_equiv.coe_to_homeomorph ContinuousLinearEquiv.coe_toHomeomorph
 
+@[simp]
+theorem coe_toHomeomorph_symm (e : M₁ ≃SL[σ₁₂] M₂) : ⇑e.toHomeomorph.symm = e.symm :=
+  rfl
+
 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