feat: multiplication on the right preserves left invariant measures (#…

…6071)

The image of a left invariant measure under right addition is left invariant, and if the measure was a Haar measure it is
stays a Haar measure.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/MeasureTheory/Group/Action.lean

@@ -7,6 +7,7 @@ import Mathlib.MeasureTheory.Group.MeasurableEquiv
 import Mathlib.MeasureTheory.Measure.Regular
 import Mathlib.Dynamics.Ergodic.MeasurePreserving
 import Mathlib.Dynamics.Minimal
+import Mathlib.Algebra.Hom.GroupAction
 
 #align_import measure_theory.group.action from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 
@@ -103,6 +104,36 @@ theorem map_smul : map (c • ·) μ = μ :=
 
 end MeasurableSMul
 
+section SMulHomClass
+
+universe uM uN uα uβ
+variable {M : Type uM} {N : Type uN}  {α : Type uα} {β : Type uβ}
+  [MeasurableSpace M] [MeasurableSpace N] [MeasurableSpace α] [MeasurableSpace β]
+
+@[to_additive]
+theorem smulInvariantMeasure_map [SMul M α] [SMul M β]
+    [MeasurableSMul M β]
+    (μ : Measure α) [SMulInvariantMeasure M α μ] (f : α → β)
+    (hsmul : ∀ (m : M) a, f (m • a) = m • f a) (hf : Measurable f) :
+    SMulInvariantMeasure M β (map f μ) where
+  measure_preimage_smul m S hS := calc
+    map f μ ((m • ·) ⁻¹' S)
+    _ = μ (f ⁻¹' ((m • ·) ⁻¹' S)) := map_apply hf <| hS.preimage (measurable_const_smul _)
+    _ = μ ((m • f ·) ⁻¹' S) := by rw [preimage_preimage]
+    _ = μ ((f <| m • ·) ⁻¹' S) := by simp_rw [hsmul]
+    _ = μ ((m • ·) ⁻¹' (f ⁻¹' S)) := by rw [←preimage_preimage]
+    _ = μ (f ⁻¹' S) := by rw [SMulInvariantMeasure.measure_preimage_smul m (hS.preimage hf)]
+    _ = map f μ S  := (map_apply hf hS).symm
+
+@[to_additive]
+instance smulInvariantMeasure_map_smul [SMul M α] [SMul N α] [SMulCommClass N M α]
+    [MeasurableSMul M α] [MeasurableSMul N α]
+    (μ : Measure α) [SMulInvariantMeasure M α μ] (n : N) :
+    SMulInvariantMeasure M α (map (n • ·) μ) :=
+  smulInvariantMeasure_map μ _ (smul_comm n) <| measurable_const_smul _
+
+end SMulHomClass
+
 variable (G) {m : MeasurableSpace α} [Group G] [MulAction G α] [MeasurableSpace G]
   [MeasurableSMul G α] (c : G) (μ : Measure α)
 

Mathlib/MeasureTheory/Group/Measure.lean

@@ -3,13 +3,15 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
+import Mathlib.Algebra.Hom.GroupAction
 import Mathlib.Dynamics.Ergodic.MeasurePreserving
 import Mathlib.MeasureTheory.Measure.Regular
 import Mathlib.MeasureTheory.Group.MeasurableEquiv
 import Mathlib.MeasureTheory.Measure.OpenPos
 import Mathlib.MeasureTheory.Group.Action
 import Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.Topology.ContinuousFunction.CocompactMap
+import Mathlib.Topology.Homeomorph
 
 #align_import measure_theory.group.measure from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
 
@@ -246,6 +248,48 @@ end MeasurableMul
 
 end Mul
 
+section Semigroup
+
+variable [Semigroup G] [MeasurableMul G] {μ : Measure G}
+
+/-- The image of a left invariant measure under a left action is left invariant, assuming that
+the action preserves multiplication. -/
+@[to_additive "The image of a left invariant measure under a left additive action is left invariant,
+assuming that the action preserves addition."]
+theorem isMulLeftInvariant_map_smul
+    {α} [SMul α G] [SMulCommClass α G G] [MeasurableSpace α] [MeasurableSMul α G]
+    [IsMulLeftInvariant μ] (a : α) :
+    IsMulLeftInvariant (map (a • · : G → G) μ) :=
+  (forall_measure_preimage_mul_iff _).1 <| fun x _ hs =>
+    (smulInvariantMeasure_map_smul μ a).measure_preimage_smul x hs
+
+/-- The image of a right invariant measure under a left action is right invariant, assuming that
+the action preserves multiplication. -/
+@[to_additive "The image of a right invariant measure under a left additive action is right
+ invariant, assuming that the action preserves addition."]
+theorem isMulRightInvariant_map_smul
+    {α} [SMul α G] [SMulCommClass α Gᵐᵒᵖ G] [MeasurableSpace α] [MeasurableSMul α G]
+    [IsMulRightInvariant μ] (a : α) :
+    IsMulRightInvariant (map (a • · : G → G) μ) :=
+  (forall_measure_preimage_mul_right_iff _).1 <| fun x _ hs =>
+    (smulInvariantMeasure_map_smul μ a).measure_preimage_smul (MulOpposite.op x) hs
+
+/-- The image of a left invariant measure under right multiplication is left invariant. -/
+@[to_additive isMulLeftInvariant_map_add_right
+"The image of a left invariant measure under right addition is left invariant."]
+instance isMulLeftInvariant_map_mul_right [IsMulLeftInvariant μ] (g : G) :
+    IsMulLeftInvariant (map (· * g) μ) :=
+  isMulLeftInvariant_map_smul (MulOpposite.op g)
+
+/-- The image of a right invariant measure under left multiplication is right invariant. -/
+@[to_additive isMulRightInvariant_map_add_left
+"The image of a right invariant measure under left addition is right invariant."]
+instance isMulRightInvariant_map_mul_left [IsMulRightInvariant μ] (g : G) :
+    IsMulRightInvariant (map (g * ·) μ) :=
+  isMulRightInvariant_map_smul g
+
+end Semigroup
+
 section DivInvMonoid
 
 variable [DivInvMonoid G]
@@ -759,6 +803,26 @@ theorem isHaarMeasure_map [BorelSpace G] [TopologicalGroup G] {H : Type*} [Group
 #align measure_theory.measure.is_haar_measure_map MeasureTheory.Measure.isHaarMeasure_map
 #align measure_theory.measure.is_add_haar_measure_map MeasureTheory.Measure.isAddHaarMeasure_map
 
+/-- The image of a Haar measure under map of a left action is again a Haar measure. -/
+@[to_additive
+   "The image of a Haar measure under map of a left additive action is again a Haar measure"]
+instance isHaarMeasure_map_smul {α} [BorelSpace G] [TopologicalGroup G] [T2Space G]
+    [Group α] [MulAction α G] [SMulCommClass α G G] [MeasurableSpace α] [MeasurableSMul α G]
+    [ContinuousConstSMul α G] (a : α) : IsHaarMeasure (Measure.map (a • · : G → G) μ) where
+  toIsMulLeftInvariant := isMulLeftInvariant_map_smul _
+  lt_top_of_isCompact K hK := by
+    rw [map_apply (measurable_const_smul _) hK.measurableSet]
+    exact IsCompact.measure_lt_top <| (Homeomorph.isCompact_preimage (Homeomorph.smul a)).2 hK
+  toIsOpenPosMeasure :=
+    (continuous_const_smul a).isOpenPosMeasure_map (MulAction.surjective a)
+
+/-- The image of a Haar measure under right multiplication is again a Haar measure. -/
+@[to_additive isHaarMeasure_map_add_right
+  "The image of a Haar measure under right addition is again a Haar measure."]
+instance isHaarMeasure_map_mul_right [BorelSpace G] [TopologicalGroup G] [T2Space G] (g : G) :
+    IsHaarMeasure (Measure.map (· * g) μ) :=
+  isHaarMeasure_map_smul μ (MulOpposite.op g)
+
 /-- A convenience wrapper for `MeasureTheory.Measure.isHaarMeasure_map`. -/
 @[to_additive "A convenience wrapper for `MeasureTheory.Measure.isAddHaarMeasure_map`."]
 nonrec theorem _root_.MulEquiv.isHaarMeasure_map [BorelSpace G] [TopologicalGroup G] {H : Type*}