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.

@[instance_reducible]

instance DomMulAct.instSMulSubtypeAEEqFunMemAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] : SMul Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)

Equations

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

@[instance_reducible]

instance DomAddAct.instVAddSubtypeAEEqFunMemAddAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] : VAdd Mᵈᵃᵃ ↥(MeasureTheory.Lp E p μ)

Equations

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

@[simp]

theorem DomMulAct.smul_Lp_val {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ↑(c • f) = c • ↑f

@[simp]

theorem DomAddAct.vadd_Lp_val {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ↑(c +ᵥ f) = c +ᵥ ↑f

theorem DomMulAct.smul_Lp_ae_eq {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑(c • f) =ᵐ[μ] fun (x : α) => ↑↑f (mk.symm c • x)

theorem DomAddAct.vadd_Lp_ae_eq {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑(c +ᵥ f) =ᵐ[μ] fun (x : α) => ↑↑f (mk.symm c +ᵥ x)

theorem DomMulAct.mk_smul_toLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : M) {f : α → E} (hf : MeasureTheory.MemLp f p μ) : mk c • MeasureTheory.MemLp.toLp f hf = MeasureTheory.MemLp.toLp (fun (x : α) => f (c • x)) ⋯

theorem DomAddAct.mk_vadd_toLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : M) {f : α → E} (hf : MeasureTheory.MemLp f p μ) : mk c +ᵥ MeasureTheory.MemLp.toLp f hf = MeasureTheory.MemLp.toLp (fun (x : α) => f (c +ᵥ x)) ⋯

@[simp]

theorem DomMulAct.smul_Lp_const {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] [MeasureTheory.IsFiniteMeasure μ] (c : Mᵈᵐᵃ) (a : E) : c • (MeasureTheory.Lp.const p μ) a = (MeasureTheory.Lp.const p μ) a

@[simp]

theorem DomAddAct.vadd_Lp_const {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] [MeasureTheory.IsFiniteMeasure μ] (c : Mᵈᵃᵃ) (a : E) : c +ᵥ (MeasureTheory.Lp.const p μ) a = (MeasureTheory.Lp.const p μ) a

theorem DomMulAct.mk_smul_indicatorConstLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : M) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (b : E) : mk c • MeasureTheory.indicatorConstLp p hs hμs b = MeasureTheory.indicatorConstLp p ⋯ ⋯ b

theorem DomAddAct.mk_vadd_indicatorConstLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : M) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (b : E) : mk c +ᵥ MeasureTheory.indicatorConstLp p hs hμs b = MeasureTheory.indicatorConstLp p ⋯ ⋯ b

instance DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp {M : Type u_1} {N : Type u_2} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] [SMul N α] [SMulCommClass M N α] [MeasureTheory.SMulInvariantMeasure N α μ] [MeasurableConstSMul N α] : SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)

instance DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_1 {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : SMulCommClass Mᵈᵐᵃ 𝕜 ↥(MeasureTheory.Lp E p μ)

instance DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_2 {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : SMulCommClass 𝕜 Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)

theorem DomMulAct.smul_Lp_add {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f g : ↥(MeasureTheory.Lp E p μ)) : c • (f + g) = c • f + c • g

@[simp]

theorem DomAddAct.vadd_Lp_add {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f g : ↥(MeasureTheory.Lp E p μ)) : c +ᵥ f + g = (c +ᵥ f) + (c +ᵥ g)

@[simp]

theorem DomMulAct.smul_Lp_zero {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) : c • 0 = 0

@[simp]

theorem DomAddAct.vadd_Lp_zero {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) : c +ᵥ 0 = 0

theorem DomMulAct.smul_Lp_neg {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : c • -f = -(c • f)

theorem DomAddAct.vadd_Lp_neg {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : c +ᵥ -f = -(c +ᵥ f)

theorem DomMulAct.smul_Lp_sub {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f g : ↥(MeasureTheory.Lp E p μ)) : c • (f - g) = c • f - c • g

theorem DomAddAct.vadd_Lp_sub {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f g : ↥(MeasureTheory.Lp E p μ)) : c +ᵥ f - g = (c +ᵥ f) - (c +ᵥ g)

@[instance_reducible]

instance DomMulAct.instDistribSMulSubtypeAEEqFunMemAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] : DistribSMul Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)

Equations

• DomMulAct.instDistribSMulSubtypeAEEqFunMemAddSubgroupLp = { toSMul := DomMulAct.instSMulSubtypeAEEqFunMemAddSubgroupLp, smul_zero := ⋯, smul_add := ⋯ }

@[simp]

theorem DomMulAct.norm_smul_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ‖c • f‖ = ‖f‖

@[simp]

theorem DomAddAct.norm_vadd_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ‖c +ᵥ f‖ = ‖f‖

@[simp]

theorem DomMulAct.nnNorm_smul_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ‖c • f‖₊ = ‖f‖₊

@[simp]

theorem DomAddAct.nnNorm_vadd_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ‖c +ᵥ f‖₊ = ‖f‖₊

@[deprecated DomMulAct.nnNorm_smul_Lp (since := "2026-10-31")]

theorem DomMulAct.nnnorm_smul_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ‖c • f‖₊ = ‖f‖₊

Alias of DomMulAct.nnNorm_smul_Lp.

@[deprecated DomAddAct.nnNorm_vadd_Lp (since := "2026-10-31")]

theorem DomAddAct.nnnorm_vadd_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ‖c +ᵥ f‖₊ = ‖f‖₊

Alias of DomAddAct.nnNorm_vadd_Lp.

@[simp]

theorem DomMulAct.dist_smul_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f g : ↥(MeasureTheory.Lp E p μ)) : dist (c • f) (c • g) = dist f g

@[simp]

theorem DomAddAct.dist_vadd_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f g : ↥(MeasureTheory.Lp E p μ)) : dist (c +ᵥ f) (c +ᵥ g) = dist f g

@[simp]

theorem DomMulAct.edist_smul_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f g : ↥(MeasureTheory.Lp E p μ)) : edist (c • f) (c • g) = edist f g

@[simp]

theorem DomAddAct.edist_vadd_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f g : ↥(MeasureTheory.Lp E p μ)) : edist (c +ᵥ f) (c +ᵥ g) = edist f g

instance DomMulAct.instIsIsometricSMulSubtypeAEEqFunMemAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] [Fact (1 ≤ p)] : IsIsometricSMul Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)

instance DomAddAct.instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] [Fact (1 ≤ p)] : IsIsometricVAdd Mᵈᵃᵃ ↥(MeasureTheory.Lp E p μ)

@[instance_reducible]

instance DomMulAct.instMulActionSubtypeAEEqFunMemAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [Monoid M] [MulAction M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] : MulAction Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)

Equations

• DomMulAct.instMulActionSubtypeAEEqFunMemAddSubgroupLp = Function.Injective.mulAction Subtype.val ⋯ ⋯

@[instance_reducible]

instance DomAddAct.instAddActionSubtypeAEEqFunMemAddAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [AddMonoid M] [AddAction M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableConstVAdd M α] : AddAction Mᵈᵃᵃ ↥(MeasureTheory.Lp E p μ)

Equations

• DomAddAct.instAddActionSubtypeAEEqFunMemAddAddSubgroupLp = Function.Injective.addAction Subtype.val ⋯ ⋯

@[instance_reducible]

instance DomMulAct.instDistribMulActionSubtypeAEEqFunMemAddSubgroupLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [Monoid M] [MulAction M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableConstSMul M α] : DistribMulAction Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)

Equations

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