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.

theorem DomAddAct.instVAddSubtypeAEEqFunMemAddAddSubgroupLp.proof_1 {E : Type u_1} [NormedAddCommGroup E] : TopologicalAddGroup E

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

Equations

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

theorem DomAddAct.instVAddSubtypeAEEqFunMemAddAddSubgroupLp.proof_2 {M : Type u_2} {α : Type u_1} [MeasurableSpace M] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableVAdd M α] (c : Mᵈᵃᵃ) : MeasureTheory.MeasurePreserving (fun (x : α) => DomAddAct.mk.symm c +ᵥ x) μ μ

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

Equations

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

@[simp]

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

@[simp]

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

theorem DomAddAct.vadd_Lp_ae_eq {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑(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} [MeasurableSpace M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑(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} [MeasurableSpace M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableVAdd M α] (c : M) {f : α → E} (hf : MeasureTheory.Memℒp f p μ) : DomAddAct.mk c +ᵥ MeasureTheory.Memℒp.toLp f hf = MeasureTheory.Memℒp.toLp (fun (x : α) => f (c +ᵥ x)) ⋯

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

@[simp]

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

@[simp]

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

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

theorem DomMulAct.mk_smul_indicatorConstLp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableSMul M α] (c : M) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (b : E) : DomMulAct.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 M] [MeasurableSpace N] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableSMul M α] [SMul N α] [SMulCommClass M N α] [MeasureTheory.SMulInvariantMeasure N α μ] [MeasurableSMul N α] : SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

Equations

• DomMulAct.instDistribSMulSubtypeAEEqFunMemAddSubgroupLp = DistribSMul.mk ⋯

@[simp]

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

@[simp]

theorem DomMulAct.norm_smul_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableSMul 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 M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableVAdd 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 M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)) : ‖c • f‖₊ = ‖f‖₊

@[simp]

theorem DomAddAct.dist_vadd_Lp {M : Type u_1} {α : Type u_3} {E : Type u_4} [MeasurableSpace M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp E p μ)) : 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} [MeasurableSpace M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp E p μ)) : 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} [MeasurableSpace M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [VAdd M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp E p μ)) : 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} [MeasurableSpace M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [SMul M α] [MeasureTheory.SMulInvariantMeasure M α μ] [MeasurableSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp E p μ)) : edist (c • f) (c • g) = edist f g

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem DomAddAct.instAddActionSubtypeAEEqFunMemAddAddSubgroupLp.proof_3 {M : Type u_1} {α : Type u_2} {E : Type u_3} [MeasurableSpace M] [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [AddMonoid M] [AddAction M α] [MeasureTheory.VAddInvariantMeasure M α μ] [MeasurableVAdd M α] : ∀ (x : Mᵈᵃᵃ) (x_1 : ↥(MeasureTheory.Lp E p μ)), ↑(x +ᵥ x_1) = ↑(x +ᵥ x_1)

theorem DomAddAct.instAddActionSubtypeAEEqFunMemAddAddSubgroupLp.proof_1 {E : Type u_1} [NormedAddCommGroup E] : TopologicalAddGroup E

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

Equations

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

theorem DomAddAct.instAddActionSubtypeAEEqFunMemAddAddSubgroupLp.proof_2 {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} : Function.Injective Subtype.val

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

Equations

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

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

Equations

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