measure_theory.function.lp_order

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

Results #

Lp E p μ is an ordered_add_comm_group when E is a normed_lattice_add_comm_group.

TODO #

move definitions of Lp.pos_part and Lp.neg_part to this file, and define them as has_pos_part.pos and has_pos_part.neg given by the lattice structure.

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 μ)) :

⇑f ≤ᵐ[μ] ⇑g ↔ f ≤ g

source

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

source

@[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 : ennreal} [normed_lattice_add_comm_group E] :

covariant_class ↥(measure_theory.Lp E p μ) ↥(measure_theory.Lp E p μ) has_add.add has_le.le

source

@[protected, instance]

def measure_theory.Lp.ordered_add_comm_group {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] :

ordered_add_comm_group ↥(measure_theory.Lp E p μ)

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 := _}

source

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 μ) :

measure_theory.mem_ℒp (f ⊔ g) p μ

source

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 μ) :

measure_theory.mem_ℒp (f ⊓ g) p μ

source

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 μ) :

measure_theory.mem_ℒp |f| p μ

source

@[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] :

lattice ↥(measure_theory.Lp E p μ)

Equations

measure_theory.Lp.lattice = subtype.lattice measure_theory.Lp.lattice._proof_3 measure_theory.Lp.lattice._proof_4

source

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

source

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

source

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|

source

@[protected, instance]

noncomputable def measure_theory.Lp.normed_lattice_add_comm_group {α : Type u_1} {E : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {p : ennreal} [normed_lattice_add_comm_group E] [fact (1 ≤ p)] :

normed_lattice_add_comm_group ↥(measure_theory.Lp E p μ)

Equations

measure_theory.Lp.normed_lattice_add_comm_group = {to_normed_add_comm_group := {to_has_norm := normed_add_comm_group.to_has_norm measure_theory.Lp.normed_add_comm_group, to_add_comm_group := normed_add_comm_group.to_add_comm_group measure_theory.Lp.normed_add_comm_group, to_metric_space := normed_add_comm_group.to_metric_space measure_theory.Lp.normed_add_comm_group, dist_eq := _}, to_lattice := {sup := lattice.sup measure_theory.Lp.lattice, le := lattice.le measure_theory.Lp.lattice, lt := lattice.lt measure_theory.Lp.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf measure_theory.Lp.lattice, inf_le_left := _, inf_le_right := _, le_inf := _}, to_has_solid_norm := _, add_le_add_left := _}

Order related properties of Lp spaces #

Results #

TODO #