Documentation

Mathlib.MeasureTheory.Function.LpOrder

Order related properties of Lp spaces #

Results #

TODO #

theorem MeasureTheory.Lp.coeFn_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f g : (Lp E p μ)) :
f ≤ᶠ[ae μ] g f g
theorem MeasureTheory.Lp.coeFn_nonneg {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : (Lp E p μ)) :
0 ≤ᶠ[ae μ] f 0 f
instance MeasureTheory.Lp.instAddLeftMono {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] :
AddLeftMono (Lp E p μ)
theorem MeasureTheory.Memℒp.sup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] {f g : αE} (hf : Memℒp f p μ) (hg : Memℒp g p μ) :
Memℒp (f g) p μ
theorem MeasureTheory.Memℒp.inf {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] {f g : αE} (hf : Memℒp f p μ) (hg : Memℒp g p μ) :
Memℒp (f g) p μ
theorem MeasureTheory.Memℒp.abs {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] {f : αE} (hf : Memℒp f p μ) :
Memℒp |f| p μ
theorem MeasureTheory.Lp.coeFn_sup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f g : (Lp E p μ)) :
(f g) =ᶠ[ae μ] f g
theorem MeasureTheory.Lp.coeFn_inf {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f g : (Lp E p μ)) :
(f g) =ᶠ[ae μ] f g
theorem MeasureTheory.Lp.coeFn_abs {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : (Lp E p μ)) :
|f| =ᶠ[ae μ] fun (x : α) => |f x|