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.
theorem
MeasureTheory.Lp.coeFn_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
(f g : ↥(Lp E p μ))
:
theorem
MeasureTheory.Lp.coeFn_nonneg
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
(f : ↥(Lp E p μ))
:
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 μ)
:
Memℒp |f| p μ
instance
MeasureTheory.Lp.instLattice
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
:
Equations
theorem
MeasureTheory.Lp.coeFn_sup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
(f g : ↥(Lp E p μ))
:
theorem
MeasureTheory.Lp.coeFn_inf
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
(f g : ↥(Lp E p μ))
:
theorem
MeasureTheory.Lp.coeFn_abs
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
(f : ↥(Lp E p μ))
:
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 μ)