# Order related properties of Lp spaces #

## Results #

• Lp E p μ is an OrderedAddCommGroup when E is a NormedLatticeAddCommGroup.

## TODO #

• move definitions of Lp.posPart and Lp.negPart to this file, and define them as PosPart.pos and NegPart.neg given by the lattice structure.
theorem MeasureTheory.Lp.coeFn_le {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} (f : { x : α →ₘ[μ] E // x }) (g : { x : α →ₘ[μ] E // x }) :
f ≤ᵐ[μ] g f g
theorem MeasureTheory.Lp.coeFn_nonneg {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} (f : { x : α →ₘ[μ] E // x }) :
0 ≤ᵐ[μ] f 0 f
instance MeasureTheory.Lp.instCovariantClassLE {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} :
CovariantClass { x : α →ₘ[μ] E // x } { x : α →ₘ[μ] E // x } (fun (x1 x2 : { x : α →ₘ[μ] E // x }) => x1 + x2) fun (x1 x2 : { x : α →ₘ[μ] E // x }) => x1 x2
Equations
• =
instance MeasureTheory.Lp.instOrderedAddCommGroup {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} :
OrderedAddCommGroup { x : α →ₘ[μ] E // x }
Equations
theorem MeasureTheory.Memℒp.sup {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} {f : αE} {g : αE} (hf : ) (hg : ) :
theorem MeasureTheory.Memℒp.inf {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} {f : αE} {g : αE} (hf : ) (hg : ) :
theorem MeasureTheory.Memℒp.abs {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} {f : αE} (hf : ) :
instance MeasureTheory.Lp.instLattice {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} :
Lattice { x : α →ₘ[μ] E // x }
Equations
• MeasureTheory.Lp.instLattice =
theorem MeasureTheory.Lp.coeFn_sup {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} (f : { x : α →ₘ[μ] E // x }) (g : { x : α →ₘ[μ] E // x }) :
(f g) =ᵐ[μ] f g
theorem MeasureTheory.Lp.coeFn_inf {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} (f : { x : α →ₘ[μ] E // x }) (g : { x : α →ₘ[μ] E // x }) :
(f g) =ᵐ[μ] f g
theorem MeasureTheory.Lp.coeFn_abs {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} (f : { x : α →ₘ[μ] E // x }) :
|f| =ᵐ[μ] fun (x : α) => |f x|
noncomputable instance MeasureTheory.Lp.instNormedLatticeAddCommGroup {α : Type u_1} {E : Type u_2} {m : } {μ : } {p : ENNReal} [Fact (1 p)] :
Equations