From b974b1579ccee0dfd0ae78fc3f47603e5634090b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Tue, 5 Sep 2023 08:18:19 +0200 Subject: [PATCH] New version --- Mathlib/LinearAlgebra/Basis.lean | 3 ++ .../MeasureTheory/Measure/Haar/OfBasis.lean | 45 +++++++++++++++++++ .../Measure/Lebesgue/Complex.lean | 20 +++++---- Mathlib/Topology/Algebra/Module/Basic.lean | 4 ++ 4 files changed, 63 insertions(+), 9 deletions(-) diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean index 0002ce74f4a1e..713792c8cb02d 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/OfBasis.lean b/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean index e65e6883b7cb3..a558a8fb34e3e 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean index 97c1d1fda2e32..56608e35ffab7 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean +++ b/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 diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index d5a7b0730e93b..321920e3a5112 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/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