Order related properties of Lp spaces #
Results #
Lp E p μ
is anOrderedAddCommGroup
whenE
is aNormedLatticeAddCommGroup
.
TODO #
theorem
MeasureTheory.Lp.coeFn_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ })
(g : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ })
:
theorem
MeasureTheory.Lp.coeFn_nonneg
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ })
:
instance
MeasureTheory.Lp.instCovariantClassLE
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
:
CovariantClass { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ } { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ }
(fun (x1 x2 : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ }) => x1 + x2)
fun (x1 x2 : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ }) => x1 ≤ x2
Equations
- ⋯ = ⋯
instance
MeasureTheory.Lp.instOrderedAddCommGroup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
:
OrderedAddCommGroup { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ }
Equations
- MeasureTheory.Lp.instOrderedAddCommGroup = OrderedAddCommGroup.mk ⋯
theorem
MeasureTheory.Memℒp.sup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.Memℒp (f ⊔ g) p μ
theorem
MeasureTheory.Memℒp.inf
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.Memℒp (f ⊓ g) p μ
theorem
MeasureTheory.Memℒp.abs
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp |f| p μ
instance
MeasureTheory.Lp.instLattice
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
:
Lattice { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ }
Equations
- MeasureTheory.Lp.instLattice = Subtype.lattice ⋯ ⋯
theorem
MeasureTheory.Lp.coeFn_sup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ })
(g : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ })
:
theorem
MeasureTheory.Lp.coeFn_inf
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ })
(g : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ })
:
theorem
MeasureTheory.Lp.coeFn_abs
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ })
:
noncomputable instance
MeasureTheory.Lp.instNormedLatticeAddCommGroup
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[NormedLatticeAddCommGroup E]
[Fact (1 ≤ p)]
:
NormedLatticeAddCommGroup { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ }
Equations
- MeasureTheory.Lp.instNormedLatticeAddCommGroup = NormedLatticeAddCommGroup.mk ⋯