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 α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : { x // x ∈ MeasureTheory.Lp E p }) (g : { x // x ∈ MeasureTheory.Lp E p }) : ↑↑f ≤ᶠ[MeasureTheory.Measure.ae μ] ↑↑g ↔ f ≤ g

theorem MeasureTheory.Lp.coeFn_nonneg {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : { x // x ∈ MeasureTheory.Lp E p }) : 0 ≤ᶠ[MeasureTheory.Measure.ae μ] ↑↑f ↔ 0 ≤ f

instance MeasureTheory.Lp.instCovariantClassLE {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] : CovariantClass { x // x ∈ MeasureTheory.Lp E p } { x // x ∈ MeasureTheory.Lp E p } (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• @MeasureTheory.Lp.instCovariantClassLE = @MeasureTheory.Lp.instCovariantClassLE.proof_1

instance MeasureTheory.Lp.instOrderedAddCommGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] : OrderedAddCommGroup { x // x ∈ MeasureTheory.Lp E p }

Equations

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

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 // x ∈ MeasureTheory.Lp E p }

Equations

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

theorem MeasureTheory.Lp.coeFn_sup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : { x // x ∈ MeasureTheory.Lp E p }) (g : { x // x ∈ MeasureTheory.Lp E p }) : ↑↑(f ⊔ g) =ᶠ[MeasureTheory.Measure.ae μ] ↑↑f ⊔ ↑↑g

theorem MeasureTheory.Lp.coeFn_inf {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : { x // x ∈ MeasureTheory.Lp E p }) (g : { x // x ∈ MeasureTheory.Lp E p }) : ↑↑(f ⊓ g) =ᶠ[MeasureTheory.Measure.ae μ] ↑↑f ⊓ ↑↑g

theorem MeasureTheory.Lp.coeFn_abs {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : { x // x ∈ MeasureTheory.Lp E p }) : ↑↑|f| =ᶠ[MeasureTheory.Measure.ae μ] fun x => |↑↑f x|

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 // x ∈ MeasureTheory.Lp E p }

Equations

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