mathlib3 documentation

measure_theory.function.lp_order

Order related properties of Lp spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Results #

TODO #

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 μ) :
@[protected, instance]
Equations
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|