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.instVAddDomAddActAEEqFun.proof_1 {M : Type u_2} {α : Type u_1} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [VAdd M α] [MeasurableVAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] (c : Mᵈᵃᵃ) : MeasureTheory.MeasurePreserving (fun (x : α) => DomAddAct.mk.symm c +ᵥ x) μ μ

instance DomAddAct.instVAddDomAddActAEEqFun {M : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [VAdd M α] [MeasurableVAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] : VAdd Mᵈᵃᵃ (α →ₘ[μ] β)

Equations

• DomAddAct.instVAddDomAddActAEEqFun = { vadd := fun (c : Mᵈᵃᵃ) (f : α →ₘ[μ] β) => MeasureTheory.AEEqFun.compMeasurePreserving f (fun (x : α) => DomAddAct.mk.symm c +ᵥ x) ⋯ }

instance DomMulAct.instSMulDomMulActAEEqFun {M : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SMul M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] : SMul Mᵈᵐᵃ (α →ₘ[μ] β)

Equations

• DomMulAct.instSMulDomMulActAEEqFun = { smul := fun (c : Mᵈᵐᵃ) (f : α →ₘ[μ] β) => MeasureTheory.AEEqFun.compMeasurePreserving f (fun (x : α) => DomMulAct.mk.symm c • x) ⋯ }

theorem DomAddAct.vadd_aeeqFun_aeeq {M : Type u_1} {α : Type u_3} {β : Type u_2} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [VAdd M α] [MeasurableVAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] (c : Mᵈᵃᵃ) (f : α →ₘ[μ] β) : ↑(c +ᵥ f) =ᶠ[MeasureTheory.Measure.ae μ] fun (x : α) => ↑f (DomAddAct.mk.symm c +ᵥ x)

theorem DomMulAct.smul_aeeqFun_aeeq {M : Type u_1} {α : Type u_3} {β : Type u_2} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SMul M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] (c : Mᵈᵐᵃ) (f : α →ₘ[μ] β) : ↑(c • f) =ᶠ[MeasureTheory.Measure.ae μ] 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} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [VAdd M α] [MeasurableVAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] (c : M) (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ) : DomAddAct.mk c +ᵥ MeasureTheory.AEEqFun.mk f hf = 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} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SMul M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] (c : M) (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ) : DomMulAct.mk c • MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk (fun (x : α) => f (c • x)) ⋯

@[simp]

theorem DomAddAct.vadd_aeeqFun_const {M : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [VAdd M α] [MeasurableVAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] (c : Mᵈᵃᵃ) (b : β) : c +ᵥ MeasureTheory.AEEqFun.const α b = MeasureTheory.AEEqFun.const α b

@[simp]

theorem DomMulAct.smul_aeeqFun_const {M : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SMul M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] (c : Mᵈᵐᵃ) (b : β) : c • MeasureTheory.AEEqFun.const α b = MeasureTheory.AEEqFun.const α b

instance DomMulAct.instSMulCommClassDomMulActAEEqFunInstSMulDomMulActAEEqFunInstSMul {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SMul M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [SMul N β] [ContinuousConstSMul N β] : SMulCommClass Mᵈᵐᵃ N (α →ₘ[μ] β)

Equations

• ⋯ = ⋯

instance DomMulAct.instSMulCommClassDomMulActAEEqFunInstSMulInstSMulDomMulActAEEqFun {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SMul M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [SMul N β] [ContinuousConstSMul N β] : SMulCommClass N Mᵈᵐᵃ (α →ₘ[μ] β)

Equations

• ⋯ = ⋯

instance DomAddAct.instVAddCommClassDomAddActDomAddActAEEqFunInstVAddDomAddActAEEqFunInstVAddDomAddActAEEqFun {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [MeasurableSpace M] [MeasurableSpace N] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [VAdd M α] [MeasurableVAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [VAdd N α] [MeasurableVAdd N α] [MeasureTheory.VAddInvariantMeasure N α μ] [VAddCommClass M N α] : VAddCommClass Mᵈᵃᵃ Nᵈᵃᵃ (α →ₘ[μ] β)

Equations

• ⋯ = ⋯

instance DomMulAct.instSMulCommClassDomMulActDomMulActAEEqFunInstSMulDomMulActAEEqFunInstSMulDomMulActAEEqFun {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [MeasurableSpace M] [MeasurableSpace N] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SMul M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [SMul N α] [MeasurableSMul N α] [MeasureTheory.SMulInvariantMeasure N α μ] [SMulCommClass M N α] : SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (α →ₘ[μ] β)

Equations

• ⋯ = ⋯

instance DomMulAct.instSMulZeroClassDomMulActAEEqFunInstZero {M : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SMul M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [Zero β] : SMulZeroClass Mᵈᵐᵃ (α →ₘ[μ] β)

Equations

• DomMulAct.instSMulZeroClassDomMulActAEEqFunInstZero = SMulZeroClass.mk ⋯

instance DomMulAct.instDistribSMulDomMulActAEEqFunToAddZeroClassInstAddMonoid {M : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [SMul M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [AddMonoid β] [ContinuousAdd β] : DistribSMul Mᵈᵐᵃ (α →ₘ[μ] β)

Equations

• DomMulAct.instDistribSMulDomMulActAEEqFunToAddZeroClassInstAddMonoid = DistribSMul.mk ⋯

theorem DomAddAct.instAddActionDomAddActAEEqFunInstAddMonoidDomAddActInstAddMonoid.proof_2 {M : Type u_1} {α : Type u_3} {β : Type u_2} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [AddMonoid M] [AddAction M α] [MeasurableVAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] (y : Mᵈᵃᵃ) (y : Mᵈᵃᵃ) (b : α →ₘ[μ] β) : y✝ + y +ᵥ b = y✝ +ᵥ (y +ᵥ b)

instance DomAddAct.instAddActionDomAddActAEEqFunInstAddMonoidDomAddActInstAddMonoid {M : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [AddMonoid M] [AddAction M α] [MeasurableVAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] : AddAction Mᵈᵃᵃ (α →ₘ[μ] β)

Equations

• DomAddAct.instAddActionDomAddActAEEqFunInstAddMonoidDomAddActInstAddMonoid = AddAction.mk ⋯ ⋯

theorem DomAddAct.instAddActionDomAddActAEEqFunInstAddMonoidDomAddActInstAddMonoid.proof_1 {M : Type u_3} {α : Type u_2} {β : Type u_1} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [AddMonoid M] [AddAction M α] [MeasurableVAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] : ∀ (x : α →ₘ[μ] β), 0 +ᵥ x = x

instance DomMulAct.instMulActionDomMulActAEEqFunInstMonoidDomMulActInstMonoid {M : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Monoid M] [MulAction M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] : MulAction Mᵈᵐᵃ (α →ₘ[μ] β)

Equations

• DomMulAct.instMulActionDomMulActAEEqFunInstMonoidDomMulActInstMonoid = MulAction.mk ⋯ ⋯

instance DomMulAct.instMulDistribMulActionDomMulActAEEqFunInstMonoidDomMulActInstMonoidInstMonoid {M : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Monoid M] [MulAction M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [Monoid β] [ContinuousMul β] : MulDistribMulAction Mᵈᵐᵃ (α →ₘ[μ] β)

Equations

• DomMulAct.instMulDistribMulActionDomMulActAEEqFunInstMonoidDomMulActInstMonoidInstMonoid = MulDistribMulAction.mk ⋯ ⋯

instance DomMulAct.instDistribMulActionDomMulActAEEqFunInstMonoidDomMulActInstMonoidInstAddMonoid {M : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Monoid M] [MulAction M α] [MeasurableSMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [AddMonoid β] [ContinuousAdd β] : DistribMulAction Mᵈᵐᵃ (α →ₘ[μ] β)

Equations

• DomMulAct.instDistribMulActionDomMulActAEEqFunInstMonoidDomMulActInstMonoidInstAddMonoid = DistribMulAction.mk ⋯ ⋯