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 #
instance
DomAddAct.instVAddAEEqFun
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace M]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
[VAdd M α]
[MeasurableVAdd M α]
[MeasureTheory.VAddInvariantMeasure M α μ]
:
theorem
DomAddAct.instVAddAEEqFun.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
DomMulAct.instSMulAEEqFun
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace M]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
[SMul M α]
[MeasurableSMul M α]
[MeasureTheory.SMulInvariantMeasure M α μ]
:
theorem
DomAddAct.vadd_aeeqFun_aeeq
{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ᵈᵃᵃ)
(f : α →ₘ[μ] β)
:
theorem
DomMulAct.smul_aeeqFun_aeeq
{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ᵈᵐᵃ)
(f : α →ₘ[μ] β)
:
@[simp]
theorem
DomAddAct.mk_vadd_mk_aeeqFun
{M : Type u_3}
{α : Type u_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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 : β)
:
@[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 : β)
:
instance
DomMulAct.instSMulCommClassAEEqFun
{M : Type u_3}
{N : Type u_1}
{α : Type u_4}
{β : Type u_2}
[MeasurableSpace M]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
[SMul M α]
[MeasurableSMul M α]
[MeasureTheory.SMulInvariantMeasure M α μ]
[SMul N β]
[ContinuousConstSMul N β]
:
SMulCommClass Mᵈᵐᵃ N (α →ₘ[μ] β)
Equations
- ⋯ = ⋯
instance
DomMulAct.instSMulCommClassAEEqFun_1
{M : Type u_3}
{N : Type u_1}
{α : Type u_4}
{β : Type u_2}
[MeasurableSpace M]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
[SMul M α]
[MeasurableSMul M α]
[MeasureTheory.SMulInvariantMeasure M α μ]
[SMul N β]
[ContinuousConstSMul N β]
:
SMulCommClass N Mᵈᵐᵃ (α →ₘ[μ] β)
Equations
- ⋯ = ⋯
instance
DomAddAct.instVAddCommClassAEEqFun_2
{M : Type u_3}
{N : Type u_1}
{α : Type u_2}
{β : 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.instSMulCommClassAEEqFun_2
{M : Type u_3}
{N : Type u_1}
{α : Type u_2}
{β : 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.instSMulZeroClassAEEqFun
{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.instSMulZeroClassAEEqFun = SMulZeroClass.mk ⋯
instance
DomMulAct.instDistribSMulAEEqFun
{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.instDistribSMulAEEqFun = DistribSMul.mk ⋯
instance
DomAddAct.instAddActionAEEqFun
{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 α μ]
:
Equations
- DomAddAct.instAddActionAEEqFun = AddAction.mk ⋯ ⋯
theorem
DomAddAct.instAddActionAEEqFun.proof_2
{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 α μ]
(y : Mᵈᵃᵃ)
(y : Mᵈᵃᵃ)
(b : α →ₘ[μ] β)
:
theorem
DomAddAct.instAddActionAEEqFun.proof_1
{M : Type u_3}
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace M]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
[AddMonoid M]
[AddAction M α]
[MeasurableVAdd M α]
[MeasureTheory.VAddInvariantMeasure M α μ]
:
instance
DomMulAct.instMulActionAEEqFun
{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 α μ]
:
Equations
- DomMulAct.instMulActionAEEqFun = MulAction.mk ⋯ ⋯
instance
DomMulAct.instMulDistribMulActionAEEqFun
{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.instMulDistribMulActionAEEqFun = MulDistribMulAction.mk ⋯ ⋯
instance
DomMulAct.instDistribMulActionAEEqFun
{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.instDistribMulActionAEEqFun = DistribMulAction.mk ⋯ ⋯