Documentation

Mathlib.MeasureTheory.Function.AEEqFun.DomAct

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 #

Equations
  • DomMulAct.instSMulAEEqFun = { smul := fun (c : Mᵈᵐᵃ) (f : α →ₘ[μ] β) => f.compMeasurePreserving (fun (x : α) => DomMulAct.mk.symm c x) }
Equations
  • DomAddAct.instVAddAEEqFun = { vadd := fun (c : Mᵈᵃᵃ) (f : α →ₘ[μ] β) => f.compMeasurePreserving (fun (x : α) => DomAddAct.mk.symm c +ᵥ x) }
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 : α →ₘ[μ] β) :
(c f) =ᵐ[μ] fun (x : α) => f (DomMulAct.mk.symm c x)
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 : α →ₘ[μ] β) :
(c +ᵥ f) =ᵐ[μ] fun (x : α) => f (DomAddAct.mk.symm 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.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))
Equations
Equations
Equations
Equations
Equations
Equations