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

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

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)) (_ : MeasureTheory.AEStronglyMeasurable (f ∘ fun (x : α) => 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)) (_ : MeasureTheory.AEStronglyMeasurable (f ∘ fun (x : α) => 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

• (_ : SMulCommClass Mᵈᵐᵃ N (α →ₘ[μ] β)) = (_ : SMulCommClass Mᵈᵐᵃ N (α →ₘ[μ] β))

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

• (_ : SMulCommClass N Mᵈᵐᵃ (α →ₘ[μ] β)) = (_ : SMulCommClass N Mᵈᵐᵃ (α →ₘ[μ] β))

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

• (_ : VAddCommClass Mᵈᵃᵃ Nᵈᵃᵃ (α →ₘ[μ] β)) = (_ : VAddCommClass Mᵈᵃᵃ Nᵈᵃᵃ (α →ₘ[μ] β))

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

• (_ : SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (α →ₘ[μ] β)) = (_ : SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (α →ₘ[μ] β))

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 (_ : ∀ (x : Mᵈᵐᵃ), x • 0 = x • 0)

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 (_ : ∀ (a : Mᵈᵐᵃ) (x y : α →ₘ[μ] β), a • (x + y) = a • x + a • y)

theorem DomAddAct.instAddActionDomAddActAEEqFunInstAddMonoidDomAddActAddMonoid.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)

theorem DomAddAct.instAddActionDomAddActAEEqFunInstAddMonoidDomAddActAddMonoid.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 DomAddAct.instAddActionDomAddActAEEqFunInstAddMonoidDomAddActAddMonoid {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.instAddActionDomAddActAEEqFunInstAddMonoidDomAddActAddMonoid = AddAction.mk (_ : ∀ (x : α →ₘ[μ] β), 0 +ᵥ x = x) (_ : ∀ (y y_1 : Mᵈᵃᵃ) (b : α →ₘ[μ] β), y + y_1 +ᵥ b = y +ᵥ (y_1 +ᵥ b))

instance DomMulAct.instMulActionDomMulActAEEqFunInstMonoidDomMulActMonoid {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.instMulActionDomMulActAEEqFunInstMonoidDomMulActMonoid = MulAction.mk (_ : ∀ (x : α →ₘ[μ] β), 1 • x = x) (_ : ∀ (y y_1 : Mᵈᵐᵃ) (b : α →ₘ[μ] β), (y * y_1) • b = y • y_1 • b)

instance DomMulAct.instMulDistribMulActionDomMulActAEEqFunInstMonoidDomMulActMonoidInstMonoid {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

• One or more equations did not get rendered due to their size.

instance DomMulAct.instDistribMulActionDomMulActAEEqFunInstMonoidDomMulActMonoidInstAddMonoid {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

• One or more equations did not get rendered due to their size.