mathlib documentation

measure_theory.function.lp_order

Order related properties of Lp spaces #

Results #

TODO #

theorem measure_theory.Lp.coe_fn_le {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] (f g : (measure_theory.Lp E p μ)) :
theorem measure_theory.Lp.coe_fn_nonneg {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] (f : (measure_theory.Lp E p μ)) :
0 ≤ᵐ[μ] f 0 f
theorem measure_theory.mem_ℒp.sup {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] {f g : α → E} (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ) :
theorem measure_theory.mem_ℒp.inf {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] {f g : α → E} (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ) :
theorem measure_theory.mem_ℒp.abs {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] {f : α → E} (hf : measure_theory.mem_ℒp f p μ) :
@[protected, instance]
def measure_theory.Lp.lattice {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] :
Equations
theorem measure_theory.Lp.coe_fn_sup {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] (f g : (measure_theory.Lp E p μ)) :
(f g) =ᵐ[μ] f g
theorem measure_theory.Lp.coe_fn_inf {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] (f g : (measure_theory.Lp E p μ)) :
(f g) =ᵐ[μ] f g
theorem measure_theory.Lp.coe_fn_abs {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] (f : (measure_theory.Lp E p μ)) :
|f| =ᵐ[μ] λ (x : α), |f x|