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 α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : (MeasureTheory.Lp E p μ)) (g : (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 : (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 ((MeasureTheory.Lp E p μ)) ((MeasureTheory.Lp E p μ)) (fun (x x_1 : (MeasureTheory.Lp E p μ)) => x + x_1) fun (x x_1 : (MeasureTheory.Lp E p μ)) => x x_1
Equations
  • =
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 μ) :
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 μ) :
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 μ) :
Equations
theorem MeasureTheory.Lp.coeFn_sup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedLatticeAddCommGroup E] (f : (MeasureTheory.Lp E p μ)) (g : (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 : (MeasureTheory.Lp E p μ)) (g : (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 : (MeasureTheory.Lp E p μ)) :
|f| =ᵐ[μ] fun (x : α) => |f x|
Equations
  • MeasureTheory.Lp.instNormedLatticeAddCommGroup = let __src := MeasureTheory.Lp.instLattice; let __src_1 := MeasureTheory.Lp.instNormedAddCommGroup; NormedLatticeAddCommGroup.mk