# Documentation

Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic

# Action of Mᵈᵐᵃ on Lᵖ spaces #

In this file we define action of Mᵈᵐᵃ on MeasureTheory.Lp E p μ If f : α → E is a function representing an equivalence class in Lᵖ(α, E), M acts on α, and c : M, then (.mk c : Mᵈᵐᵃ) • [f] is represented by the function a ↦ f (c • a).

We also prove basic properties of this action.

@[simp]
theorem DomAddAct.vadd_Lp_val {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) (f : { x // x }) :
↑(c +ᵥ f) = c +ᵥ f
@[simp]
theorem DomMulAct.smul_Lp_val {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) (f : { x // x }) :
↑(c f) = c f
theorem DomAddAct.vadd_Lp_ae_eq {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) (f : { x // x }) :
↑(c +ᵥ f) =ᶠ[] fun x => f (DomAddAct.mk.symm c +ᵥ x)
theorem DomMulAct.smul_Lp_ae_eq {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) (f : { x // x }) :
↑(c f) =ᶠ[] fun x => f (DomMulAct.mk.symm c x)
theorem DomAddAct.mk_vadd_toLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : M) {f : αE} (hf : ) :
DomAddAct.mk c +ᵥ = MeasureTheory.Memℒp.toLp (fun x => f (c +ᵥ x)) (_ : MeasureTheory.Memℒp (f fun x => c +ᵥ x) p)
theorem DomMulAct.mk_smul_toLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : M) {f : αE} (hf : ) :
DomMulAct.mk c = MeasureTheory.Memℒp.toLp (fun x => f (c x)) (_ : MeasureTheory.Memℒp (f fun x => c x) p)
@[simp]
theorem DomAddAct.vadd_Lp_const {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) (a : E) :
c +ᵥ ↑() a = ↑() a
@[simp]
theorem DomMulAct.smul_Lp_const {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) (a : E) :
c ↑() a = ↑() a
@[simp]
theorem DomAddAct.vadd_Lp_add {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) (f : { x // x }) (g : { x // x }) :
c +ᵥ (f + g) = c +ᵥ f + (c +ᵥ g)
theorem DomMulAct.smul_Lp_add {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) (f : { x // x }) (g : { x // x }) :
c (f + g) = c f + c g
@[simp]
theorem DomAddAct.vadd_Lp_zero {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) :
c +ᵥ 0 = 0
@[simp]
theorem DomMulAct.smul_Lp_zero {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) :
c 0 = 0
theorem DomAddAct.vadd_Lp_neg {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) (f : { x // x }) :
c +ᵥ -f = -(c +ᵥ f)
theorem DomMulAct.smul_Lp_neg {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) (f : { x // x }) :
c -f = -(c f)
theorem DomAddAct.vadd_Lp_sub {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) (f : { x // x }) (g : { x // x }) :
c +ᵥ (f - g) = c +ᵥ f - (c +ᵥ g)
theorem DomMulAct.smul_Lp_sub {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) (f : { x // x }) (g : { x // x }) :
c (f - g) = c f - c g
@[simp]
theorem DomAddAct.norm_vadd_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) (f : { x // x }) :
@[simp]
theorem DomMulAct.norm_smul_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) (f : { x // x }) :
@[simp]
theorem DomAddAct.nnnorm_vadd_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) (f : { x // x }) :
@[simp]
theorem DomMulAct.nnnorm_smul_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) (f : { x // x }) :
@[simp]
theorem DomAddAct.dist_vadd_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) (f : { x // x }) (g : { x // x }) :
dist (c +ᵥ f) (c +ᵥ g) = dist f g
@[simp]
theorem DomMulAct.dist_smul_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) (f : { x // x }) (g : { x // x }) :
dist (c f) (c g) = dist f g
@[simp]
theorem DomAddAct.edist_vadd_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [VAdd M α] [] (c : Mᵈᵃᵃ) (f : { x // x }) (g : { x // x }) :
edist (c +ᵥ f) (c +ᵥ g) = edist f g
@[simp]
theorem DomMulAct.edist_smul_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [] [] {μ : } {p : ENNReal} [SMul M α] [] (c : Mᵈᵐᵃ) (f : { x // x }) (g : { x // x }) :
edist (c f) (c g) = edist f g