Order related properties of Lp spaces #
Results #
Lp E p μis anordered_add_comm_groupwhenEis anormed_lattice_add_comm_group.
TODO #
- move definitions of
Lp.pos_partandLp.neg_partto this file, and define them ashas_pos_part.posandhas_pos_part.neggiven by the lattice structure. - show that if
Eis anormed_lattice_add_comm_groupthen so isLp E p μfor1 ≤ p. In particular, this showsorder_closed_topologyforLp.
theorem
measure_theory.Lp.coe_fn_le
{α : Type u_1}
{E : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{p : ℝ≥0∞}
[normed_lattice_add_comm_group E]
[measurable_space E]
[borel_space E]
[topological_space.second_countable_topology 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 : ℝ≥0∞}
[normed_lattice_add_comm_group E]
[measurable_space E]
[borel_space E]
[topological_space.second_countable_topology E]
(f : ↥(measure_theory.Lp E p μ)) :
@[protected, instance]
def
measure_theory.Lp.has_le.le.covariant_class
{α : Type u_1}
{E : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{p : ℝ≥0∞}
[normed_lattice_add_comm_group E]
[measurable_space E]
[borel_space E]
[topological_space.second_countable_topology E] :
covariant_class ↥(measure_theory.Lp E p μ) ↥(measure_theory.Lp E p μ) has_add.add has_le.le
@[protected, instance]
def
measure_theory.Lp.ordered_add_comm_group
{α : Type u_1}
{E : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{p : ℝ≥0∞}
[normed_lattice_add_comm_group E]
[measurable_space E]
[borel_space E]
[topological_space.second_countable_topology E] :
Equations
- measure_theory.Lp.ordered_add_comm_group = {add := add_comm_group.add (measure_theory.Lp E p μ).to_add_comm_group, add_assoc := _, zero := add_comm_group.zero (measure_theory.Lp E p μ).to_add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (measure_theory.Lp E p μ).to_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (measure_theory.Lp E p μ).to_add_comm_group, sub := add_comm_group.sub (measure_theory.Lp E p μ).to_add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (measure_theory.Lp E p μ).to_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le (subtype.partial_order (λ (x : α →ₘ[μ] E), x ∈ measure_theory.Lp E p μ)), lt := partial_order.lt (subtype.partial_order (λ (x : α →ₘ[μ] E), x ∈ measure_theory.Lp E p μ)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}