feat(MeasureTheory): define DomMulAct action on Lp (#6190)

Mathlib.lean

@@ -2332,6 +2332,7 @@ import Mathlib.MeasureTheory.Function.LocallyIntegrable
 import Mathlib.MeasureTheory.Function.LpOrder
 import Mathlib.MeasureTheory.Function.LpSeminorm
 import Mathlib.MeasureTheory.Function.LpSpace
+import Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
 import Mathlib.MeasureTheory.Function.SimpleFunc
 import Mathlib.MeasureTheory.Function.SimpleFuncDense
 import Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Mathlib/MeasureTheory/Function/AEEqFun/DomAct.lean

@@ -48,6 +48,11 @@ theorem mk_smul_mk_aeeqFun (c : M) (f : α → β) (hf : AEStronglyMeasurable f
       (hf.comp_measurePreserving (measurePreserving_smul _ _)) :=
   rfl
 
+@[to_additive (attr := simp)]
+theorem smul_aeeqFun_const (c : Mᵈᵐᵃ) (b : β) :
+    c • (AEEqFun.const α b : α →ₘ[μ] β) = AEEqFun.const α b :=
+  rfl
+
 instance [SMul N β] [ContinuousConstSMul N β] : SMulCommClass Mᵈᵐᵃ N (α →ₘ[μ] β) where
   smul_comm := by rintro _ _ ⟨_⟩; rfl
 

Mathlib/MeasureTheory/Function/LpSpace.lean

@@ -262,7 +262,7 @@ theorem norm_def (f : Lp E p μ) : ‖f‖ = ENNReal.toReal (snorm f p μ) :=
 #align measure_theory.Lp.norm_def MeasureTheory.Lp.norm_def
 
 theorem nnnorm_def (f : Lp E p μ) : ‖f‖₊ = ENNReal.toNNReal (snorm f p μ) :=
-  Subtype.eta _ _
+  rfl
 #align measure_theory.Lp.nnnorm_def MeasureTheory.Lp.nnnorm_def
 
 @[simp, norm_cast]
@@ -291,6 +291,13 @@ theorem edist_def (f g : Lp E p μ) : edist f g = snorm (⇑f - ⇑g) p μ :=
   rfl
 #align measure_theory.Lp.edist_def MeasureTheory.Lp.edist_def
 
+protected theorem edist_dist (f g : Lp E p μ) : edist f g = .ofReal (dist f g) := by
+  rw [edist_def, dist_def, ← snorm_congr_ae (coeFn_sub _ _),
+    ENNReal.ofReal_toReal (snorm_ne_top (f - g))]
+
+protected theorem dist_edist (f g : Lp E p μ) : dist f g = (edist f g).toReal :=
+  MeasureTheory.Lp.dist_def ..
+
 @[simp]
 theorem edist_toLp_toLp (f g : α → E) (hf : Memℒp f p μ) (hg : Memℒp g p μ) :
     edist (hf.toLp f) (hg.toLp g) = snorm (f - g) p μ := by
@@ -440,12 +447,9 @@ instance instNormedAddCommGroup [hp : Fact (1 ≤ p)] : NormedAddCommGroup (Lp E
           rw [snorm_congr_ae (coeFn_add _ _)]
           exact snorm_add_le (Lp.aestronglyMeasurable f) (Lp.aestronglyMeasurable g) hp.1
         eq_zero_of_map_eq_zero' := fun f =>
-          (norm_eq_zero_iff <|
-              zero_lt_one.trans_le hp.1).1 } with
+          (norm_eq_zero_iff <| zero_lt_one.trans_le hp.1).1 } with
     edist := edist
-    edist_dist := fun f g => by
-      rw [edist_def, dist_def, ← snorm_congr_ae (coeFn_sub _ _),
-        ENNReal.ofReal_toReal (snorm_ne_top (f - g))] }
+    edist_dist := Lp.edist_dist }
 #align measure_theory.Lp.normed_add_comm_group MeasureTheory.Lp.instNormedAddCommGroup
 
 -- check no diamond is created
@@ -940,12 +944,14 @@ theorem norm_compMeasurePreserving (g : Lp E p μb) (hf : MeasurePreserving f μ
 
 variable (𝕜 : Type _) [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E]
 
+/-- `MeasureTheory.Lp.compMeasurePreserving` as a linear map. -/
 @[simps]
 def compMeasurePreservingₗ (f : α → β) (hf : MeasurePreserving f μ μb) :
     Lp E p μb →ₗ[𝕜] Lp E p μ where
   __ := compMeasurePreserving f hf
   map_smul' c g := by rcases g with ⟨⟨_⟩, _⟩; rfl
 
+/-- `MeasureTheory.Lp.compMeasurePreserving` as a linear isometry. -/
 @[simps!]
 def compMeasurePreservingₗᵢ [Fact (1 ≤ p)] (f : α → β) (hf : MeasurePreserving f μ μb) :
     Lp E p μb →ₗᵢ[𝕜] Lp E p μ where

Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2023 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.MeasureTheory.Integral.Bochner
+import Mathlib.MeasureTheory.Function.AEEqFun.DomAct
+
+/-!
+# Action of `Mᵈᵐᵃ` on `Lᵖ` spaces
+
+In this file we define action of `Mᵈᵐᵃ` on `MeasureTheory.Lp E p μ`
+If `f : α → E` is a function representing an equivalence class in `Lᵖ(α, E)`, `M` acts on `α`,
+and `c : M`, then `(.mk c : Mᵈᵐᵃ) • [f]` is represented by the function `a ↦ f (c • a)`.
+
+We also prove basic properties of this action.
+-/
+
+open MeasureTheory Filter
+open scoped ENNReal
+
+namespace DomMulAct
+
+variable {M N α E : Type _} [MeasurableSpace M] [MeasurableSpace N]
+  [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ℝ≥0∞}
+
+section SMul
+
+variable [SMul M α] [SMulInvariantMeasure M α μ] [MeasurableSMul M α]
+
+@[to_additive]
+instance : SMul Mᵈᵐᵃ (Lp E p μ) where
+  smul c f := Lp.compMeasurePreserving (mk.symm c • ·) (measurePreserving_smul _ _) f
+
+@[to_additive (attr := simp)]
+theorem smul_Lp_val (c : Mᵈᵐᵃ) (f : Lp E p μ) : (c • f).1 = c • f.1 := rfl
+
+@[to_additive]
+theorem smul_Lp_ae_eq (c : Mᵈᵐᵃ) (f : Lp E p μ) : c • f =ᵐ[μ] (f <| mk.symm c • ·) :=
+  Lp.coeFn_compMeasurePreserving _ _
+
+@[to_additive]
+theorem mk_smul_toLp (c : M) {f : α → E} (hf : Memℒp f p μ) :
+    mk c • hf.toLp f =
+      (hf.comp_measurePreserving <| measurePreserving_smul c μ).toLp (f <| c • ·) :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem smul_Lp_const [IsFiniteMeasure μ] (c : Mᵈᵐᵃ) (a : E) :
+    c • Lp.const p μ a = Lp.const p μ a :=
+  rfl
+
+instance [SMul N α] [SMulCommClass M N α] [SMulInvariantMeasure N α μ] [MeasurableSMul N α] :
+    SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (Lp E p μ) :=
+  Subtype.val_injective.smulCommClass (fun _ _ ↦ rfl) fun _ _ ↦ rfl
+
+instance [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] : SMulCommClass Mᵈᵐᵃ 𝕜 (Lp E p μ) :=
+  Subtype.val_injective.smulCommClass (fun _ _ ↦ rfl) fun _ _ ↦ rfl
+
+instance [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] : SMulCommClass 𝕜 Mᵈᵐᵃ (Lp E p μ) :=
+  .symm _ _ _
+
+-- We don't have a typeclass for additive versions of the next few lemmas
+-- Should we add `AddDistribAddAction` with `to_additive` both from `MulDistribMulAction`
+-- and `DistribMulAction`?
+
+@[to_additive]
+theorem smul_Lp_add (c : Mᵈᵐᵃ) : ∀ f g : Lp E p μ, c • (f + g) = c • f + c • g := by
+  rintro ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩; rfl
+attribute [simp] DomAddAct.vadd_Lp_add
+
+@[to_additive (attr := simp 1001)]
+theorem smul_Lp_zero (c : Mᵈᵐᵃ) : c • (0 : Lp E p μ) = 0 := rfl
+
+@[to_additive]
+theorem smul_Lp_neg (c : Mᵈᵐᵃ) (f : Lp E p μ) : c • (-f) = -(c • f) := by
+  rcases f with ⟨⟨_⟩, _⟩; rfl
+
+@[to_additive]
+theorem smul_Lp_sub (c : Mᵈᵐᵃ) : ∀ f g : Lp E p μ, c • (f - g) = c • f - c • g := by
+  rintro ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩; rfl
+
+instance : DistribSMul Mᵈᵐᵃ (Lp E p μ) where
+  smul_zero _ := rfl
+  smul_add := by rintro _ ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩; rfl
+
+-- The next few lemmas follow from the `IsometricSMul` instance if `1 ≤ p`
+@[to_additive (attr := simp)]
+theorem norm_smul_Lp (c : Mᵈᵐᵃ) (f : Lp E p μ) : ‖c • f‖ = ‖f‖ :=
+  Lp.norm_compMeasurePreserving _ _
+
+@[to_additive (attr := simp)]
+theorem nnnorm_smul_Lp (c : Mᵈᵐᵃ) (f : Lp E p μ) : ‖c • f‖₊ = ‖f‖₊ :=
+  NNReal.eq <| Lp.norm_compMeasurePreserving _ _
+
+@[to_additive (attr := simp)]
+theorem dist_smul_Lp (c : Mᵈᵐᵃ) (f g : Lp E p μ) : dist (c • f) (c • g) = dist f g := by
+  simp only [dist, ← smul_Lp_sub, norm_smul_Lp]
+
+@[to_additive (attr := simp)]
+theorem edist_smul_Lp (c : Mᵈᵐᵃ) (f g : Lp E p μ) : edist (c • f) (c • g) = edist f g := by
+  simp only [Lp.edist_dist, dist_smul_Lp]
+
+variable [Fact (1 ≤ p)]
+
+instance : IsometricSMul Mᵈᵐᵃ (Lp E p μ) := ⟨edist_smul_Lp⟩
+
+end SMul
+
+section MulAction
+
+variable [Monoid M] [MulAction M α] [SMulInvariantMeasure M α μ] [MeasurableSMul M α]
+
+@[to_additive]
+instance : MulAction Mᵈᵐᵃ (Lp E p μ) := Subtype.val_injective.mulAction _ fun _ _ ↦ rfl
+
+instance : DistribMulAction Mᵈᵐᵃ (Lp E p μ) :=
+  Subtype.val_injective.distribMulAction ⟨⟨_, rfl⟩, fun _ _ ↦ rfl⟩ fun _ _ ↦ rfl
+
+end MulAction
+
+end DomMulAct

Mathlib/MeasureTheory/Group/Integration.lean

@@ -5,7 +5,6 @@ Authors: Floris van Doorn
 -/
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.MeasureTheory.Group.Measure
-import Mathlib.MeasureTheory.Group.Action
 
 #align_import measure_theory.group.integration from "leanprover-community/mathlib"@"ec247d43814751ffceb33b758e8820df2372bf6f"