Mathlib.MeasureTheory.Function.LpOrder

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 : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [PartialOrder E] (f g : ↥(Lp E p μ)) :

↑↑f ≤ᶠ[ae μ] ↑↑g ↔ f ≤ g

source

theorem MeasureTheory.Lp.coeFn_nonneg {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [PartialOrder E] (f : ↥(Lp E p μ)) :

0 ≤ᶠ[ae μ] ↑↑f ↔ 0 ≤ f

source

instance MeasureTheory.Lp.instAddLeftMono {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] :

AddLeftMono ↥(Lp E p μ)

source

instance MeasureTheory.Lp.instIsOrderedAddMonoid {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] :

IsOrderedAddMonoid ↥(Lp E p μ)

source

instance MeasureTheory.Lp.instOrderClosedTopologySubtypeAEEqFunMemAddSubgroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [PartialOrder E] [OrderClosedTopology E] [IsOrderedAddMonoid E] [Fact (1 ≤ p)] :

OrderClosedTopology ↥(Lp E p μ)

source

theorem MeasureTheory.MemLp.sup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) :

MemLp (f ⊔ g) p μ

source

@[deprecated MeasureTheory.MemLp.sup (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.sup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) :

MemLp (f ⊔ g) p μ

Alias of MeasureTheory.MemLp.sup.

source

theorem MeasureTheory.MemLp.inf {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) :

MemLp (f ⊓ g) p μ

source

@[deprecated MeasureTheory.MemLp.inf (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.inf {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) :

MemLp (f ⊓ g) p μ

Alias of MeasureTheory.MemLp.inf.

source

theorem MeasureTheory.MemLp.abs {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] {f : α → E} (hf : MemLp f p μ) :

MemLp |f| p μ

source

@[deprecated MeasureTheory.MemLp.abs (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.abs {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] {f : α → E} (hf : MemLp f p μ) :

MemLp |f| p μ

Alias of MeasureTheory.MemLp.abs.

source

instance MeasureTheory.Lp.instLattice {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] :

Lattice ↥(Lp E p μ)

Equations

MeasureTheory.Lp.instLattice = Subtype.lattice ⋯ ⋯

source

theorem MeasureTheory.Lp.coeFn_sup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] (f g : ↥(Lp E p μ)) :

↑↑(f ⊔ g) =ᶠ[ae μ] ↑↑f ⊔ ↑↑g

source

theorem MeasureTheory.Lp.coeFn_inf {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] (f g : ↥(Lp E p μ)) :

↑↑(f ⊓ g) =ᶠ[ae μ] ↑↑f ⊓ ↑↑g

source

theorem MeasureTheory.Lp.coeFn_abs {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] (f : ↥(Lp E p μ)) :

↑↑|f| =ᶠ[ae μ] fun (x : α) => |↑↑f x|

source

instance MeasureTheory.Lp.instHasSolidNorm {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] [Fact (1 ≤ p)] :

HasSolidNorm ↥(Lp E p μ)

Order related properties of Lp spaces #

Results #

TODO #