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