feat: MeasurableConstSMul (#24317)

This typeclass will be useful in #23603.

Author: YaelDillies

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -506,11 +506,16 @@ instance (priority := 100) ContinuousInv.measurableInv [Inv γ] [ContinuousInv 
     MeasurableInv γ := ⟨continuous_inv.measurable⟩
 
 @[to_additive]
-instance (priority := 100) ContinuousSMul.measurableSMul {M α} [TopologicalSpace M]
+instance (priority := 100) ContinuousConstSMul.toMeasurableConstSMul {M α} [TopologicalSpace α]
+    [MeasurableSpace α] [BorelSpace α] [SMul M α] [ContinuousConstSMul M α] :
+    MeasurableConstSMul M α where
+  measurable_const_smul _ := (continuous_const_smul _).measurable
+
+@[to_additive]
+instance (priority := 100) ContinuousSMul.toMeasurableSMul {M α} [TopologicalSpace M]
     [TopologicalSpace α] [MeasurableSpace M] [MeasurableSpace α] [OpensMeasurableSpace M]
-    [BorelSpace α] [SMul M α] [ContinuousSMul M α] : MeasurableSMul M α :=
-  ⟨fun _ => (continuous_const_smul _).measurable, fun _ =>
-    (continuous_id.smul continuous_const).measurable⟩
+    [BorelSpace α] [SMul M α] [ContinuousSMul M α] : MeasurableSMul M α where
+  measurable_smul_const _ := (continuous_id.smul continuous_const).measurable
 
 section Homeomorph
 

Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

@@ -262,10 +262,8 @@ instance instMeasurableInv : MeasurableInv ℝ≥0∞ :=
   ⟨continuous_inv.measurable⟩
 
 instance : MeasurableSMul ℝ≥0 ℝ≥0∞ where
-  measurable_const_smul := by
-    simp_rw [ENNReal.smul_def]
-    exact fun _ ↦ MeasurableSMul.measurable_const_smul _
-  measurable_smul_const := fun x ↦ by
+  measurable_const_smul _ := by simp_rw [ENNReal.smul_def]; exact measurable_const_smul _
+  measurable_smul_const _ := by
     simp_rw [ENNReal.smul_def]
     exact measurable_coe_nnreal_ennreal.mul_const _
 

Mathlib/MeasureTheory/Group/Arithmetic.lean

@@ -468,19 +468,28 @@ instance (priority := 100) MeasurableDiv.toMeasurableInv [MeasurableSpace α] [G
     [MeasurableDiv α] : MeasurableInv α where
   measurable_inv := by simpa using measurable_const_div (1 : α)
 
+/-- We say that the action of `M` on `α` has `MeasurableConstVAdd` if for each `c` the map
+`x ↦ c +ᵥ x` is a measurable function. -/
+class MeasurableConstVAdd (M α : Type*) [VAdd M α] [MeasurableSpace α] : Prop where
+  measurable_const_vadd : ∀ c : M, Measurable (c +ᵥ · : α → α)
+
+/-- We say that the action of `M` on `α` has `MeasurableConstSMul` if for each `c` the map
+`x ↦ c • x` is a measurable function. -/
+@[to_additive]
+class MeasurableConstSMul (M α : Type*) [SMul M α] [MeasurableSpace α] : Prop where
+  measurable_const_smul : ∀ c : M, Measurable (c • · : α → α)
+
 /-- We say that the action of `M` on `α` has `MeasurableVAdd` if for each `c` the map `x ↦ c +ᵥ x`
 is a measurable function and for each `x` the map `c ↦ c +ᵥ x` is a measurable function. -/
-class MeasurableVAdd (M α : Type*) [VAdd M α] [MeasurableSpace M] [MeasurableSpace α] :
-    Prop where
-  measurable_const_vadd : ∀ c : M, Measurable (c +ᵥ · : α → α)
+class MeasurableVAdd (M α : Type*) [VAdd M α] [MeasurableSpace M] [MeasurableSpace α]
+    extends MeasurableConstVAdd M α where
   measurable_vadd_const : ∀ x : α, Measurable (· +ᵥ x : M → α)
 
 /-- We say that the action of `M` on `α` has `MeasurableSMul` if for each `c` the map `x ↦ c • x`
 is a measurable function and for each `x` the map `c ↦ c • x` is a measurable function. -/
 @[to_additive]
-class MeasurableSMul (M α : Type*) [SMul M α] [MeasurableSpace M] [MeasurableSpace α] :
-    Prop where
-  measurable_const_smul : ∀ c : M, Measurable (c • · : α → α)
+class MeasurableSMul (M α : Type*) [SMul M α] [MeasurableSpace M] [MeasurableSpace α]
+    extends MeasurableConstSMul M α where
   measurable_smul_const : ∀ x : α, Measurable (· • x : M → α)
 
 /-- We say that the action of `M` on `α` has `MeasurableVAdd₂` if the map
@@ -496,39 +505,89 @@ class MeasurableSMul₂ (M α : Type*) [SMul M α] [MeasurableSpace M] [Measurab
     Prop where
   measurable_smul : Measurable (Function.uncurry (· • ·) : M × α → α)
 
-export MeasurableSMul (measurable_const_smul measurable_smul_const)
-
+export MeasurableConstVAdd (measurable_const_vadd)
+export MeasurableConstSMul (measurable_const_smul)
+export MeasurableVAdd (measurable_vadd_const)
+export MeasurableSMul (measurable_smul_const)
 export MeasurableSMul₂ (measurable_smul)
-
-export MeasurableVAdd (measurable_const_vadd measurable_vadd_const)
-
 export MeasurableVAdd₂ (measurable_vadd)
 
 @[to_additive]
 instance measurableSMul_of_mul (M : Type*) [Mul M] [MeasurableSpace M] [MeasurableMul M] :
-    MeasurableSMul M M :=
-  ⟨measurable_id.const_mul, measurable_id.mul_const⟩
+    MeasurableSMul M M where
+  measurable_const_smul := measurable_id.const_mul
+  measurable_smul_const := measurable_id.mul_const
 
 @[to_additive]
 instance measurableSMul₂_of_mul (M : Type*) [Mul M] [MeasurableSpace M] [MeasurableMul₂ M] :
     MeasurableSMul₂ M M :=
   ⟨measurable_mul⟩
 
 @[to_additive]
-instance Submonoid.measurableSMul {M α} [MeasurableSpace M] [MeasurableSpace α] [Monoid M]
-    [MulAction M α] [MeasurableSMul M α] (s : Submonoid M) : MeasurableSMul s α :=
-  ⟨fun c => by simpa only using measurable_const_smul (c : M), fun x =>
-    (measurable_smul_const x : Measurable fun c : M => c • x).comp measurable_subtype_coe⟩
+instance Submonoid.instMeasurableConstSMul {M α} [MeasurableSpace α] [Monoid M] [MulAction M α]
+    [MeasurableConstSMul M α] (s : Submonoid M) : MeasurableConstSMul s α where
+  measurable_const_smul c := by simpa only using measurable_const_smul (c : M)
+
+@[to_additive]
+instance Submonoid.instMeasurableSMul {M α} [MeasurableSpace M] [MeasurableSpace α] [Monoid M]
+    [MulAction M α] [MeasurableSMul M α] (s : Submonoid M) : MeasurableSMul s α where
+  measurable_smul_const x := (measurable_smul_const (M := M) x).comp measurable_subtype_coe
 
 @[to_additive]
-instance Subgroup.measurableSMul {G α} [MeasurableSpace G] [MeasurableSpace α] [Group G]
+instance Subgroup.instMeasurableConstSMul {G α} [MeasurableSpace α] [Group G] [MulAction G α]
+    [MeasurableConstSMul G α] (s : Subgroup G) : MeasurableConstSMul s α :=
+  s.toSubmonoid.instMeasurableConstSMul
+
+@[to_additive]
+instance Subgroup.instMeasurableSMul {G α} [MeasurableSpace G] [MeasurableSpace α] [Group G]
     [MulAction G α] [MeasurableSMul G α] (s : Subgroup G) : MeasurableSMul s α :=
-  s.toSubmonoid.measurableSMul
+  s.toSubmonoid.instMeasurableSMul
 
 section SMul
+variable {M X α β : Type*} [MeasurableSpace X] [SMul M X]
+  {m : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {f : α → M} {g : α → X}
+
+section MeasurableConstSMul
+variable [MeasurableConstSMul M X]
+
+@[to_additive (attr := fun_prop, measurability)]
+lemma Measurable.const_smul (hg : Measurable g) (c : M) : Measurable (c • g) :=
+  (measurable_const_smul c).comp hg
+
+/-- Compositional version of `Measurable.const_smul` for use by `fun_prop`. -/
+@[to_additive (attr := fun_prop)
+"Compositional version of `Measurable.const_vadd` for use by `fun_prop`."]
+lemma Measurable.fun_const_smul {g : α → β → X} {h : α → β} (hg : Measurable ↿g) (hh : Measurable h)
+    (c : M) : Measurable fun a ↦ (c • g a) (h a) :=
+  (hg.comp <| measurable_id.prodMk hh).const_smul _
+
+@[deprecated (since := "2025-04-23")] alias Measurable.const_smul' := Measurable.fun_const_smul
+
+@[to_additive (attr := fun_prop, measurability)]
+lemma AEMeasurable.fun_const_smul (hg : AEMeasurable g μ) (c : M) : AEMeasurable (c • g ·) μ :=
+  (measurable_const_smul c).comp_aemeasurable hg
+
+@[deprecated (since := "2025-04-23")] alias AEMeasurable.const_smul' := AEMeasurable.fun_const_smul
+
+@[to_additive (attr := fun_prop, measurability)]
+lemma AEMeasurable.const_smul (hf : AEMeasurable g μ) (c : M) : AEMeasurable (c • g) μ :=
+  hf.fun_const_smul c
+
+@[to_additive]
+instance Pi.instMeasurableConstSMul {ι : Type*} {α : ι → Type*} [∀ i, SMul M (α i)]
+    [∀ i, MeasurableSpace (α i)] [∀ i, MeasurableConstSMul M (α i)] :
+    MeasurableConstSMul M (∀ i, α i) where
+  measurable_const_smul _ := measurable_pi_iff.2 fun i ↦ (measurable_pi_apply i).const_smul _
+
+/-- If a scalar is central, then its right action is measurable when its left action is. -/
+@[to_additive]
+nonrec instance MulOpposite.instMeasurableConstSMul [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α]
+    [MeasurableConstSMul M α] : MeasurableConstSMul Mᵐᵒᵖ α where
+  measurable_const_smul := by simpa using measurable_const_smul
+
+end MeasurableConstSMul
 
-variable {M X α β : Type*} [MeasurableSpace M] [MeasurableSpace X] [SMul M X]
-  {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → M} {g : α → X}
+variable [MeasurableSpace M]
 
 @[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
 theorem Measurable.smul [MeasurableSMul₂ M X] (hf : Measurable f) (hg : Measurable g) :
@@ -549,10 +608,11 @@ theorem AEMeasurable.smul [MeasurableSMul₂ M X] {μ : Measure α} (hf : AEMeas
 
 @[to_additive]
 instance (priority := 100) MeasurableSMul₂.toMeasurableSMul [MeasurableSMul₂ M X] :
-    MeasurableSMul M X :=
-  ⟨fun _ => measurable_const.smul measurable_id, fun _ => measurable_id.smul measurable_const⟩
+    MeasurableSMul M X where
+  measurable_const_smul _ := measurable_const.smul measurable_id
+  measurable_smul_const _ := measurable_id.smul measurable_const
 
-variable [MeasurableSMul M X] {μ : Measure α}
+variable [MeasurableSMul M X]
 
 @[to_additive (attr := fun_prop, measurability)]
 theorem Measurable.smul_const (hf : Measurable f) (y : X) : Measurable fun x => f x • y :=
@@ -563,32 +623,11 @@ theorem AEMeasurable.smul_const (hf : AEMeasurable f μ) (y : X) :
     AEMeasurable (fun x => f x • y) μ :=
   (MeasurableSMul.measurable_smul_const y).comp_aemeasurable hf
 
-@[to_additive (attr := fun_prop, measurability)]
-theorem Measurable.const_smul (hg : Measurable g) (c : M) : Measurable (c • g) :=
-  (MeasurableSMul.measurable_const_smul c).comp hg
-
-/-- Compositional version of `Measurable.const_smul` for use by `fun_prop`. -/
-@[to_additive (attr := fun_prop)
-"Compositional version of `Measurable.const_vadd` for use by `fun_prop`."]
-lemma Measurable.const_smul' {g : α → β → X} {h : α → β} (hg : Measurable ↿g) (hh : Measurable h)
-    (c : M) : Measurable fun a ↦ (c • g a) (h a) :=
-  (hg.comp <| measurable_id.prodMk hh).const_smul _
-
-@[to_additive (attr := fun_prop, measurability)]
-theorem AEMeasurable.const_smul' (hg : AEMeasurable g μ) (c : M) :
-    AEMeasurable (fun x => c • g x) μ :=
-  (MeasurableSMul.measurable_const_smul c).comp_aemeasurable hg
-
-@[to_additive (attr := fun_prop, measurability)]
-theorem AEMeasurable.const_smul (hf : AEMeasurable g μ) (c : M) : AEMeasurable (c • g) μ :=
-  hf.const_smul' c
-
 @[to_additive]
 instance Pi.measurableSMul {ι : Type*} {α : ι → Type*} [∀ i, SMul M (α i)]
     [∀ i, MeasurableSpace (α i)] [∀ i, MeasurableSMul M (α i)] :
-    MeasurableSMul M (∀ i, α i) :=
-  ⟨fun _ => measurable_pi_iff.mpr fun i => (measurable_pi_apply i).const_smul _, fun _ =>
-    measurable_pi_iff.mpr fun _ => measurable_smul_const _⟩
+    MeasurableSMul M (∀ i, α i) where
+  measurable_smul_const _ := measurable_pi_iff.2 fun _ ↦ measurable_smul_const _
 
 /-- `AddMonoid.SMul` is measurable. -/
 instance AddMonoid.measurableSMul_nat₂ (M : Type*) [AddMonoid M] [MeasurableSpace M]
@@ -641,11 +680,10 @@ theorem measurableSMul₂_iterateMulAct : MeasurableSMul₂ (IterateMulAct f) α
 end IterateMulAct
 
 section MulAction
+variable {G G₀ M β α : Type*} [MeasurableSpace β] [MeasurableSpace α] {f : α → β} {μ : Measure α}
 
-variable {M β α : Type*} [MeasurableSpace M] [MeasurableSpace β] [Monoid M] [MulAction M β]
-  [MeasurableSMul M β] [MeasurableSpace α] {f : α → β} {μ : Measure α}
-
-variable {G : Type*} [Group G] [MeasurableSpace G] [MulAction G β] [MeasurableSMul G β]
+section Group
+variable {G : Type*} [Group G] [MulAction G β] [MeasurableConstSMul G β]
 
 @[to_additive]
 theorem measurable_const_smul_iff (c : G) : (Measurable fun x => c • f x) ↔ Measurable f :=
@@ -656,14 +694,17 @@ theorem aemeasurable_const_smul_iff (c : G) :
     AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ :=
   ⟨fun h => by simpa [inv_smul_smul, Pi.smul_def] using h.const_smul c⁻¹, fun h => h.const_smul c⟩
 
-@[to_additive]
-instance Units.instMeasurableSpace : MeasurableSpace Mˣ := MeasurableSpace.comap ((↑) : Mˣ → M) ‹_›
+end Group
+
+section Monoid
+variable [Monoid M] [MulAction M β]
+
+section MeasurableConstSMul
+variable [MeasurableConstSMul M β]
 
 @[to_additive]
-instance Units.measurableSMul : MeasurableSMul Mˣ β where
+instance Units.instMeasurableConstSMul : MeasurableConstSMul Mˣ β where
   measurable_const_smul c := measurable_const_smul (c : M)
-  measurable_smul_const x :=
-    (measurable_smul_const x : Measurable fun c : M => c • x).comp MeasurableSpace.le_map_comap
 
 @[to_additive]
 nonrec theorem IsUnit.measurable_const_smul_iff {c : M} (hc : IsUnit c) :
@@ -677,8 +718,24 @@ nonrec theorem IsUnit.aemeasurable_const_smul_iff {c : M} (hc : IsUnit c) :
   let ⟨u, hu⟩ := hc
   hu ▸ aemeasurable_const_smul_iff u
 
-variable {G₀ : Type*} [GroupWithZero G₀] [MeasurableSpace G₀] [MulAction G₀ β]
-  [MeasurableSMul G₀ β]
+end MeasurableConstSMul
+
+section MeasurableSMul
+variable [MeasurableSpace M] [MeasurableSMul M β]
+
+@[to_additive]
+instance Units.instMeasurableSpace : MeasurableSpace Mˣ := .comap Units.val ‹_›
+
+@[to_additive]
+instance Units.measurableSMul : MeasurableSMul Mˣ β where
+  measurable_smul_const x :=
+    (measurable_smul_const x : Measurable fun c : M => c • x).comp MeasurableSpace.le_map_comap
+
+end MeasurableSMul
+end Monoid
+
+section GroupWithZero
+variable [GroupWithZero G₀] [MeasurableSpace G₀] [MulAction G₀ β] [MeasurableSMul G₀ β]
 
 theorem measurable_const_smul_iff₀ {c : G₀} (hc : c ≠ 0) :
     (Measurable fun x => c • f x) ↔ Measurable f :=
@@ -688,6 +745,7 @@ theorem aemeasurable_const_smul_iff₀ {c : G₀} (hc : c ≠ 0) :
     AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ :=
   (IsUnit.mk0 c hc).aemeasurable_const_smul_iff
 
+end GroupWithZero
 end MulAction
 
 /-!
@@ -725,14 +783,12 @@ instance MulOpposite.instMeasurableMul₂ {M : Type*} [Mul M] [MeasurableSpace M
       ((measurable_mul_unop.comp measurable_snd).mul (measurable_mul_unop.comp measurable_fst))⟩
 
 /-- If a scalar is central, then its right action is measurable when its left action is. -/
+@[to_additive]
 nonrec instance MeasurableSMul.op {M α} [MeasurableSpace M] [MeasurableSpace α] [SMul M α]
-    [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [MeasurableSMul M α] : MeasurableSMul Mᵐᵒᵖ α :=
-  ⟨MulOpposite.rec' fun c =>
-      show Measurable fun x => op c • x by
-        simpa only [op_smul_eq_smul] using measurable_const_smul c,
-    fun x =>
+    [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [MeasurableSMul M α] : MeasurableSMul Mᵐᵒᵖ α where
+  measurable_smul_const x :=
     show Measurable fun c => op (unop c) • x by
-      simpa only [op_smul_eq_smul] using (measurable_smul_const x).comp measurable_mul_unop⟩
+      simpa only [op_smul_eq_smul] using (measurable_smul_const x).comp measurable_mul_unop
 
 /-- If a scalar is central, then its right action is measurable when its left action is. -/
 nonrec instance MeasurableSMul₂.op {M α} [MeasurableSpace M] [MeasurableSpace α] [SMul M α]
@@ -743,8 +799,9 @@ nonrec instance MeasurableSMul₂.op {M α} [MeasurableSpace M] [MeasurableSpace
 
 @[to_additive]
 instance measurableSMul_opposite_of_mul {M : Type*} [Mul M] [MeasurableSpace M]
-    [MeasurableMul M] : MeasurableSMul Mᵐᵒᵖ M :=
-  ⟨fun c => measurable_mul_const (unop c), fun x => measurable_mul_unop.const_mul x⟩
+    [MeasurableMul M] : MeasurableSMul Mᵐᵒᵖ M where
+  measurable_const_smul c := measurable_mul_const (unop c)
+  measurable_smul_const x := measurable_mul_unop.const_mul x
 
 @[to_additive]
 instance measurableSMul₂_opposite_of_mul {M : Type*} [Mul M] [MeasurableSpace M]

Mathlib/MeasureTheory/Group/MeasurableEquiv.lean

@@ -38,8 +38,8 @@ open scoped Pointwise NNReal
 
 namespace MeasurableEquiv
 
-variable {G G₀ α : Type*} [MeasurableSpace G] [MeasurableSpace G₀] [MeasurableSpace α] [Group G]
-  [GroupWithZero G₀] [MulAction G α] [MulAction G₀ α] [MeasurableSMul G α] [MeasurableSMul G₀ α]
+variable {G G₀ α : Type*} [MeasurableSpace α] [Group G] [GroupWithZero G₀] [MulAction G α]
+  [MulAction G₀ α] [MeasurableConstSMul G α] [MeasurableConstSMul G₀ α]
 
 /-- If a group `G` acts on `α` by measurable maps, then each element `c : G` defines a measurable
 automorphism of `α`. -/
@@ -75,6 +75,8 @@ theorem _root_.measurableEmbedding_const_smul₀ {c : G₀} (hc : c ≠ 0) :
     MeasurableEmbedding (c • · : α → α) :=
   (smul₀ c hc).measurableEmbedding
 
+variable [MeasurableSpace G] [MeasurableSpace G₀]
+
 section Mul
 
 variable [MeasurableMul G] [MeasurableMul G₀]
@@ -206,10 +208,7 @@ end MeasurableEquiv
 
 namespace MeasureTheory.Measure
 variable {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A] [MeasurableSpace A]
-  -- We only need `MeasurableConstSMul G A` but we don't have this class. So we erroneously must
-  -- assume `MeasurableSpace G` + `MeasurableSMul G A`
-  [MeasurableSpace G] [MeasurableSMul G A]
-variable {μ ν : Measure A} {g : G}
+  [MeasurableConstSMul G A] {μ ν : Measure A} {g : G}
 
 noncomputable instance : DistribMulAction Gᵈᵐᵃ (Measure A) where
   smul g μ := μ.map (DomMulAct.mk.symm g⁻¹ • ·)

Mathlib/MeasureTheory/Group/Measure.lean

@@ -864,11 +864,9 @@ instance (priority := 100) IsHaarMeasure.noAtoms [IsTopologicalGroup G] [BorelSp
       K_compact.measure_lt_top.ne
 
 instance IsAddHaarMeasure.domSMul {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A]
-    -- We only need `MeasurableConstSMul G A` but we don't have this class. So we erroneously must
-    -- assume `MeasurableSpace G` + `MeasurableSMul G A`
-    [MeasurableSpace A] [MeasurableSpace G] [MeasurableSMul G A] [TopologicalSpace A] [BorelSpace A]
-    [IsTopologicalAddGroup A] [ContinuousConstSMul G A] {μ : Measure A} [μ.IsAddHaarMeasure]
-    (g : Gᵈᵐᵃ) : (g • μ).IsAddHaarMeasure :=
+    [MeasurableSpace A] [TopologicalSpace A] [BorelSpace A] [IsTopologicalAddGroup A]
+    [ContinuousConstSMul G A] {μ : Measure A} [μ.IsAddHaarMeasure] (g : Gᵈᵐᵃ) :
+    (g • μ).IsAddHaarMeasure :=
   (DistribMulAction.toAddEquiv _ (DomMulAct.mk.symm g⁻¹)).isAddHaarMeasure_map _
     (continuous_const_smul _) (continuous_const_smul _)
 

Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

@@ -1051,10 +1051,8 @@ theorem integral_map_equiv {β} [MeasurableSpace β] (e : α ≃ᵐ β) (f : β
 
 omit hE in
 lemma integral_domSMul {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A]
-    -- We only need `MeasurableConstSMul G A` but we don't have this class. So we erroneously must
-    -- assume `MeasurableSpace G` + `MeasurableSMul G A`
-    [MeasurableSpace A] [MeasurableSpace G] [MeasurableSMul G A] {μ : Measure A}
-    (g : Gᵈᵐᵃ) (f : A → E) : ∫ x, f x ∂g • μ = ∫ x, f ((DomMulAct.mk.symm g)⁻¹ • x) ∂μ :=
+    [MeasurableSpace A] [MeasurableConstSMul G A] {μ : Measure A} (g : Gᵈᵐᵃ) (f : A → E) :
+    ∫ x, f x ∂g • μ = ∫ x, f ((DomMulAct.mk.symm g)⁻¹ • x) ∂μ :=
   integral_map_equiv (MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)) f
 
 theorem MeasurePreserving.integral_comp {β} {_ : MeasurableSpace β} {f : α → β} {ν}