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 : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f g : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) : Iff ((ae μ).EventuallyLE f.val.cast g.val.cast) (LE.le f g)

theorem MeasureTheory.Lp.coeFn_nonneg {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) : Iff ((ae μ).EventuallyLE 0 f.val.cast) (LE.le 0 f)

theorem MeasureTheory.Lp.instAddLeftMono {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] : AddLeftMono (Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x)

def MeasureTheory.Lp.instOrderedAddCommGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] : OrderedAddCommGroup (Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x)

Equations

• One or more equations did not get rendered due to their size.

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

@[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} [NormedLatticeAddCommGroup E] {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : MemLp (Max.max f g) p μ

Alias of MeasureTheory.MemLp.sup.

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

@[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} [NormedLatticeAddCommGroup E] {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : MemLp (Min.min f g) p μ

Alias of MeasureTheory.MemLp.inf.

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

@[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} [NormedLatticeAddCommGroup E] {f : α → E} (hf : MemLp f p μ) : MemLp (_root_.abs f) p μ

Alias of MeasureTheory.MemLp.abs.

def MeasureTheory.Lp.instLattice {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] : Lattice (Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x)

Equations

• Eq MeasureTheory.Lp.instLattice (Subtype.lattice ⋯ ⋯)

theorem MeasureTheory.Lp.coeFn_sup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f g : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) : (ae μ).EventuallyEq (Max.max f g).val.cast (Max.max f.val.cast g.val.cast)

theorem MeasureTheory.Lp.coeFn_inf {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f g : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) : (ae μ).EventuallyEq (Min.min f g).val.cast (Min.min f.val.cast g.val.cast)

theorem MeasureTheory.Lp.coeFn_abs {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) : (ae μ).EventuallyEq (abs f).val.cast fun (x : α) => abs (f.val.cast x)

noncomputable def MeasureTheory.Lp.instNormedLatticeAddCommGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] [Fact (LE.le 1 p)] : NormedLatticeAddCommGroup (Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x)

Equations

• One or more equations did not get rendered due to their size.