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