Order related properties of Lp spaces #
Results #
Lp E p μ
is anOrderedAddCommGroup
whenE
is aNormedLatticeAddCommGroup
.
TODO #
- move definitions of
Lp.posPart
andLp.negPart
to this file, and define them asPosPart.pos
andNegPart.neg
given by the lattice structure.
instance
MeasureTheory.Lp.instAddLeftMono
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
:
AddLeftMono ↥(Lp E p μ)
instance
MeasureTheory.Lp.instOrderedAddCommGroup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
:
OrderedAddCommGroup ↥(Lp E p μ)
theorem
MeasureTheory.Memℒp.sup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
{f g : α → E}
(hf : Memℒp f p μ)
(hg : Memℒp g p μ)
:
theorem
MeasureTheory.Memℒp.inf
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
{f g : α → E}
(hf : Memℒp f p μ)
(hg : Memℒp g p μ)
:
theorem
MeasureTheory.Memℒp.abs
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
{f : α → E}
(hf : Memℒp f p μ)
:
instance
MeasureTheory.Lp.instLattice
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
:
Equations
noncomputable instance
MeasureTheory.Lp.instNormedLatticeAddCommGroup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
[Fact (1 ≤ p)]
:
NormedLatticeAddCommGroup ↥(Lp E p μ)