Documentation

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

↑↑f ≤ᵐ[μ] ↑↑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 : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ }) :

0 ≤ᵐ[μ] ↑↑f ↔ 0 ≤ f

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 μ }) :

↑↑(f ⊔ g) =ᵐ[μ] ↑↑f ⊔ ↑↑g

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 μ }) :

↑↑(f ⊓ g) =ᵐ[μ] ↑↑f ⊓ ↑↑g

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 μ }) :

↑↑|f| =ᵐ[μ] 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 : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E p μ }

Equations

MeasureTheory.Lp.instNormedLatticeAddCommGroup = NormedLatticeAddCommGroup.mk ⋯