From 01a1e92a9d0fde739c7c6ad0d8445d5218105bec Mon Sep 17 00:00:00 2001 From: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Tue, 12 Sep 2023 07:58:23 +0000 Subject: [PATCH] feat: add some lemmas for Haar measures (#7034) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We prove some lemmas that will be useful in following PRs #6832 and #7037, mainly: ```lean theorem Basis.addHaar_eq {b : Basis ι ℝ E} {b' : Basis ι' ℝ E} : b.addHaar = b'.addHaar ↔ b.addHaar b'.parallelepiped = 1 theorem Basis.parallelepiped_eq_map (b : Basis ι ℝ E) : b.parallelepiped = (TopologicalSpace.PositiveCompacts.piIcc01 ι).map b.equivFun.symm b.equivFunL.symm.continuous theorem Basis.addHaar_map (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) : map f b.addHaar = (b.map f.toLinearEquiv).addHaar ``` Co-authored-by: Eric Wieser --- Mathlib/LinearAlgebra/Basis.lean | 3 +++ Mathlib/MeasureTheory/Measure/Haar/Basic.lean | 8 +++++++ .../MeasureTheory/Measure/Haar/OfBasis.lean | 17 +++++++++++++ .../Measure/Lebesgue/EqHaar.lean | 24 +++++++++++++++++++ Mathlib/Topology/Algebra/Module/Basic.lean | 3 +++ 5 files changed, 55 insertions(+) diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean index ff47e3092bb25a..a9475c7b5b1a4e 100644 --- a/Mathlib/LinearAlgebra/Basis.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index 82d1c3351ba5ba..49ee1df8791222 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/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 `μ` be a σ-finite left invariant measure on `G`. Then `μ` is equal to the Haar measure +defined by `K₀` iff `μ K₀ = 1`. -/ +@[to_additive] +theorem haarMeasure_eq_iff (K₀ : PositiveCompacts G) (μ : Measure G) [SigmaFinite μ] + [IsMulLeftInvariant μ] : + haarMeasure K₀ = μ ↔ μ K₀ = 1 := + ⟨fun h => h.symm ▸ haarMeasure_self, fun h => by rw [haarMeasure_unique μ K₀, h, one_smul]⟩ + example [LocallyCompactSpace G] (μ : Measure G) [IsHaarMeasure μ] (K₀ : PositiveCompacts G) : μ = μ K₀.1 • haarMeasure K₀ := haarMeasure_unique μ K₀ diff --git a/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean b/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean index e65e6883b7cb39..4bdc299aa5844f 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean @@ -226,6 +226,23 @@ 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 [SecondCountableTopology E] (b : Basis ι ℝ E) : + SigmaFinite b.addHaar := by + rw [Basis.addHaar_def]; exact sigmaFinite_addHaarMeasure + +/-- Let `μ` be a σ-finite left invariant measure on `E`. Then `μ` is equal to the Haar measure +defined by `b` iff the parallelepiped defined by `b` has measure `1` for `μ`. -/ +theorem Basis.addHaar_eq_iff [SecondCountableTopology E] (b : Basis ι ℝ E) (μ : Measure E) + [SigmaFinite μ] [IsAddLeftInvariant μ] : + b.addHaar = μ ↔ μ b.parallelepiped = 1 := by + rw [Basis.addHaar_def] + exact addHaarMeasure_eq_iff b.parallelepiped μ + +@[simp] +theorem Basis.addHaar_reindex (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 diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean index df05ce0845ed32..47862e61cddab2 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean @@ -79,6 +79,30 @@ 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 = (PositiveCompacts.piIcc01 ι).map b.equivFun.symm + b.equivFunL.symm.continuous b.equivFunL.symm.isOpenMap := by + classical + rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map] + congr + 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] [NormedAddCommGroup F] + [NormedSpace ℝ E] [NormedSpace ℝ F] [MeasurableSpace E] [MeasurableSpace F] [BorelSpace E] + [BorelSpace F] [SecondCountableTopology F] [SigmaCompactSpace F] + (b : Basis ι ℝ E) (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 + rw [eq_comm, Basis.addHaar_eq_iff, Measure.map_apply f.continuous.measurable + (PositiveCompacts.isCompact _).measurableSet, Basis.coe_parallelepiped, Basis.coe_map] + erw [← image_parallelepiped, f.toEquiv.preimage_image, addHaar_self] + namespace MeasureTheory open Measure TopologicalSpace.PositiveCompacts FiniteDimensional diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index d5a7b0730e93bc..6e15802c0078f5 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/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