# Action of DomMulAct and DomAddAct on α →ₘ[μ] β#

If M acts on α by measure-preserving transformations, then Mᵈᵐᵃ acts on α →ₘ[μ] β by sending each function f to f ∘ (DomMulAct.mk.symm c • ·). We define this action and basic instances about it.

## Implementation notes #

In fact, it suffices to require that (c • ·) is only quasi measure-preserving but we don't have a typeclass for quasi measure-preserving actions yet.

## Keywords #

theorem DomAddAct.instVAddAEEqFun.proof_1 {M : Type u_2} {α : Type u_1} [] [] {μ : } [VAdd M α] [] (c : Mᵈᵃᵃ) :
MeasureTheory.MeasurePreserving (fun (x : α) => DomAddAct.mk.symm c +ᵥ x) μ μ
instance DomAddAct.instVAddAEEqFun {M : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {μ : } [] [VAdd M α] [] :
Equations
• DomAddAct.instVAddAEEqFun = { vadd := fun (c : Mᵈᵃᵃ) (f : α →ₘ[μ] β) => f.compMeasurePreserving (fun (x : α) => DomAddAct.mk.symm c +ᵥ x) }
instance DomMulAct.instSMulAEEqFun {M : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {μ : } [] [SMul M α] [] :
Equations
• DomMulAct.instSMulAEEqFun = { smul := fun (c : Mᵈᵐᵃ) (f : α →ₘ[μ] β) => f.compMeasurePreserving (fun (x : α) => DomMulAct.mk.symm c x) }
theorem DomAddAct.vadd_aeeqFun_aeeq {M : Type u_1} {α : Type u_3} {β : Type u_2} [] [] {μ : } [] [VAdd M α] [] (c : Mᵈᵃᵃ) (f : α →ₘ[μ] β) :
(c +ᵥ f) =ᵐ[μ] fun (x : α) => f (DomAddAct.mk.symm c +ᵥ x)
theorem DomMulAct.smul_aeeqFun_aeeq {M : Type u_1} {α : Type u_3} {β : Type u_2} [] [] {μ : } [] [SMul M α] [] (c : Mᵈᵐᵃ) (f : α →ₘ[μ] β) :
(c f) =ᵐ[μ] fun (x : α) => f (DomMulAct.mk.symm c x)
@[simp]
theorem DomAddAct.mk_vadd_mk_aeeqFun {M : Type u_3} {α : Type u_2} {β : Type u_1} [] [] {μ : } [] [VAdd M α] [] (c : M) (f : αβ) (hf : ) :
DomAddAct.mk c +ᵥ = MeasureTheory.AEEqFun.mk (fun (x : α) => f (c +ᵥ x))
@[simp]
theorem DomMulAct.mk_smul_mk_aeeqFun {M : Type u_3} {α : Type u_2} {β : Type u_1} [] [] {μ : } [] [SMul M α] [] (c : M) (f : αβ) (hf : ) :
DomMulAct.mk c = MeasureTheory.AEEqFun.mk (fun (x : α) => f (c x))
@[simp]
theorem DomAddAct.vadd_aeeqFun_const {M : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {μ : } [] [VAdd M α] [] (c : Mᵈᵃᵃ) (b : β) :
@[simp]
theorem DomMulAct.smul_aeeqFun_const {M : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {μ : } [] [SMul M α] [] (c : Mᵈᵐᵃ) (b : β) :
instance DomMulAct.instSMulCommClassAEEqFun {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [] [] {μ : } [] [SMul M α] [] [SMul N β] [] :
Equations
• =
instance DomMulAct.instSMulCommClassAEEqFun_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [] [] {μ : } [] [SMul M α] [] [SMul N β] [] :
Equations
• =
instance DomAddAct.instVAddCommClassAEEqFun_2 {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [] [] [] {μ : } [] [VAdd M α] [] [VAdd N α] [] [] :
Equations
• =
instance DomMulAct.instSMulCommClassAEEqFun_2 {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [] [] [] {μ : } [] [SMul M α] [] [SMul N α] [] [] :
Equations
• =
instance DomMulAct.instSMulZeroClassAEEqFun {M : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {μ : } [] [SMul M α] [] [Zero β] :
Equations
• DomMulAct.instSMulZeroClassAEEqFun =
instance DomMulAct.instDistribSMulAEEqFun {M : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {μ : } [] [SMul M α] [] [] [] :
Equations
• DomMulAct.instDistribSMulAEEqFun =
theorem DomAddAct.instAddActionAEEqFun.proof_1 {M : Type u_3} {α : Type u_2} {β : Type u_1} [] [] {μ : } [] [] [] [] :
∀ (x : α →ₘ[μ] β), 0 +ᵥ x = x
instance DomAddAct.instAddActionAEEqFun {M : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {μ : } [] [] [] [] :
Equations