mathlib documentation

measure_theory.lp_space

ℒp space and Lp space #

This file describes properties of almost everywhere measurable functions with finite seminorm, denoted by snorm f p μ and defined for p:ℝ≥0∞ as 0 if p=0, (∫ ∥f a∥^p ∂μ) ^ (1/p) for 0 < p < ∞ and ess_sup ∥f∥ μ for p=∞.

The Prop-valued mem_ℒp f p μ states that a function f : α → E has finite seminorm. The space Lp E p μ is the subtype of elements of α →ₘ[μ] E (see ae_eq_fun) such that snorm f p μ is finite. For 1 ≤ p, snorm defines a norm and Lp is a complete metric space.

Main definitions #

Lipschitz functions vanishing at zero act by composition on Lp. We define this action, and prove that it is continuous. In particular,

When α is a topological space equipped with a finite Borel measure, there is a bounded linear map from the normed space of bounded continuous functions (α →ᵇ E) to Lp E p μ. We construct this as bounded_continuous_function.to_Lp.

Notations #

Implementation #

Since Lp is defined as an add_subgroup, dot notation does not work. Use Lp.measurable f to say that the coercion of f to a genuine function is measurable, instead of the non-working f.measurable.

To prove that two Lp elements are equal, it suffices to show that their coercions to functions coincide almost everywhere (this is registered as an ext rule). This can often be done using filter_upwards. For instance, a proof from first principles that f + (g + h) = (f + g) + h could read (in the Lp namespace)

example (f g h : Lp E p μ) : (f + g) + h = f + (g + h) :=
begin
  ext1,
  filter_upwards [coe_fn_add (f + g) h, coe_fn_add f g, coe_fn_add f (g + h), coe_fn_add g h],
  assume a ha1 ha2 ha3 ha4,
  simp only [ha1, ha2, ha3, ha4, add_assoc],
end

The lemma coe_fn_add states that the coercion of f + g coincides almost everywhere with the sum of the coercions of f and g. All such lemmas use coe_fn in their name, to distinguish the function coercion from the coercion to almost everywhere defined functions.

ℒp seminorm #

We define the ℒp seminorm, denoted by snorm f p μ. For real p, it is given by an integral formula (for which we use the notation snorm' f p μ), and for p = ∞ it is the essential supremum (for which we use the notation snorm_ess_sup f μ).

We also define a predicate mem_ℒp f p μ, requesting that a function is almost everywhere measurable and has finite snorm f p μ.

This paragraph is devoted to the basic properties of these definitions. It is constructed as follows: for a given property, we prove it for snorm' and snorm_ess_sup when it makes sense, deduce it for snorm, and translate it in terms of mem_ℒp.

def measure_theory.snorm' {α : Type u_1} {F : Type u_3} [measurable_space α] [normed_group F] (f : α → F) (q : ) (μ : measure_theory.measure α) :

(∫ ∥f a∥^q ∂μ) ^ (1/q), which is a seminorm on the space of measurable functions for which this quantity is finite

Equations
def measure_theory.snorm_ess_sup {α : Type u_1} {F : Type u_3} [measurable_space α] [normed_group F] (f : α → F) (μ : measure_theory.measure α) :

seminorm for ℒ∞, equal to the essential supremum of ∥f∥.

Equations
def measure_theory.snorm {α : Type u_1} {F : Type u_3} [measurable_space α] [normed_group F] (f : α → F) (p : ℝ≥0∞) (μ : measure_theory.measure α) :

ℒp seminorm, equal to 0 for p=0, to (∫ ∥f a∥^p ∂μ) ^ (1/p) for 0 < p < ∞ and to ess_sup ∥f∥ μ for p = ∞.

Equations
theorem measure_theory.snorm_eq_snorm' {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] (hp_ne_zero : p 0) (hp_ne_top : p ) {f : α → F} :
@[simp]
theorem measure_theory.snorm_exponent_top {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
def measure_theory.mem_ℒp {α : Type u_1} {E : Type u_2} [measurable_space α] [measurable_space E] [normed_group E] (f : α → E) (p : ℝ≥0∞) (μ : measure_theory.measure α) :
Prop

The property that f:α→E is ae_measurable and (∫ ∥f a∥^p ∂μ)^(1/p) is finite if p < ∞, or ess_sup f < ∞ if p = ∞.

Equations
theorem measure_theory.mem_ℒp.ae_measurable {α : Type u_1} {E : Type u_2} [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {p : ℝ≥0∞} {μ : measure_theory.measure α} (h : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.lintegral_rpow_nnnorm_eq_rpow_snorm' {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] {f : α → F} (hq0_lt : 0 < q) :
∫⁻ (a : α), (nnnorm (f a)) ^ q μ = measure_theory.snorm' f q μ ^ q
theorem measure_theory.mem_ℒp.snorm_lt_top {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {f : α → E} (hfp : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.mem_ℒp.snorm_ne_top {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {f : α → E} (hfp : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] {f : α → F} (hq0_lt : 0 < q) (hfq : measure_theory.snorm' f q μ < ) :
∫⁻ (a : α), (nnnorm (f a)) ^ q μ <
@[simp]
theorem measure_theory.snorm'_exponent_zero {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
@[simp]
theorem measure_theory.snorm_exponent_zero {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
@[simp]
theorem measure_theory.snorm'_zero {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] (hp0_lt : 0 < q) :
@[simp]
theorem measure_theory.snorm'_zero' {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] (hq0_ne : q 0) (hμ : μ 0) :
@[simp]
theorem measure_theory.snorm_ess_sup_zero {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] :
@[simp]
theorem measure_theory.snorm_zero {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] :
theorem measure_theory.snorm'_measure_zero_of_pos {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } [normed_group F] {f : α → F} (hq_pos : 0 < q) :
theorem measure_theory.snorm'_measure_zero_of_exponent_zero {α : Type u_1} {F : Type u_3} [measurable_space α] [normed_group F] {f : α → F} :
theorem measure_theory.snorm'_measure_zero_of_neg {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } [normed_group F] {f : α → F} (hq_neg : q < 0) :
@[simp]
theorem measure_theory.snorm_ess_sup_measure_zero {α : Type u_1} {F : Type u_3} [measurable_space α] [normed_group F] {f : α → F} :
@[simp]
theorem measure_theory.snorm_measure_zero {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} [normed_group F] {f : α → F} :
theorem measure_theory.snorm'_const {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] (c : F) (hq_pos : 0 < q) :
measure_theory.snorm' (λ (x : α), c) q μ = ((nnnorm c)) * μ set.univ ^ (1 / q)
theorem measure_theory.snorm'_const' {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] [measure_theory.finite_measure μ] (c : F) (hc_ne_zero : c 0) (hq_ne_zero : q 0) :
measure_theory.snorm' (λ (x : α), c) q μ = ((nnnorm c)) * μ set.univ ^ (1 / q)
theorem measure_theory.snorm_ess_sup_const {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] (c : F) (hμ : μ 0) :
measure_theory.snorm_ess_sup (λ (x : α), c) μ = (nnnorm c)
theorem measure_theory.snorm'_const_of_probability_measure {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] (c : F) (hq_pos : 0 < q) [measure_theory.probability_measure μ] :
measure_theory.snorm' (λ (x : α), c) q μ = (nnnorm c)
theorem measure_theory.snorm_const {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] (c : F) (h0 : p 0) (hμ : μ 0) :
measure_theory.snorm (λ (x : α), c) p μ = ((nnnorm c)) * μ set.univ ^ (1 / p.to_real)
theorem measure_theory.snorm_const' {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] (c : F) (h0 : p 0) (h_top : p ) :
measure_theory.snorm (λ (x : α), c) p μ = ((nnnorm c)) * μ set.univ ^ (1 / p.to_real)
theorem measure_theory.mem_ℒp_const {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] (c : E) [measure_theory.finite_measure μ] :
measure_theory.mem_ℒp (λ (a : α), c) p μ
theorem measure_theory.snorm'_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] [normed_group G] {f : α → F} {g : α → G} (hq : 0 q) (h : ∀ᵐ (x : α) ∂μ, f x g x) :
theorem measure_theory.snorm'_congr_norm_ae {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] {f g : α → F} (hfg : ∀ᵐ (x : α) ∂μ, f x = g x) :
theorem measure_theory.snorm'_congr_ae {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] {f g : α → F} (hfg : f =ᵐ[μ] g) :
theorem measure_theory.snorm_ess_sup_congr_ae {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {f g : α → F} (hfg : f =ᵐ[μ] g) :
theorem measure_theory.snorm_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] [normed_group G] {f : α → F} {g : α → G} (h : ∀ᵐ (x : α) ∂μ, f x g x) :
theorem measure_theory.snorm_le_of_ae_bound {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] {f : α → F} {C : } (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
theorem measure_theory.snorm_congr_norm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] [normed_group G] {f : α → F} {g : α → G} (hfg : ∀ᵐ (x : α) ∂μ, f x = g x) :
@[simp]
theorem measure_theory.snorm'_norm {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
measure_theory.snorm' (λ (a : α), f a) q μ = measure_theory.snorm' f q μ
@[simp]
theorem measure_theory.snorm_norm {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] (f : α → F) :
measure_theory.snorm (λ (x : α), f x) p μ = measure_theory.snorm f p μ
theorem measure_theory.snorm'_norm_rpow {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] (f : α → F) (p q : ) (hq_pos : 0 < q) :
measure_theory.snorm' (λ (x : α), f x ^ q) p μ = measure_theory.snorm' f (p * q) μ ^ q
theorem measure_theory.snorm_norm_rpow {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {q : } {μ : measure_theory.measure α} [normed_group F] (f : α → F) (hq_pos : 0 < q) :
measure_theory.snorm (λ (x : α), f x ^ q) p μ = measure_theory.snorm f (p * ennreal.of_real q) μ ^ q
theorem measure_theory.snorm_congr_ae {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] {f g : α → F} (hfg : f =ᵐ[μ] g) :
theorem measure_theory.mem_ℒp_congr_ae {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {f g : α → E} (hfg : f =ᵐ[μ] g) :
theorem measure_theory.mem_ℒp.ae_eq {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {f g : α → E} (hfg : f =ᵐ[μ] g) (hf_Lp : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.mem_ℒp.of_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [measurable_space F] {f : α → E} {g : α → F} (hg : measure_theory.mem_ℒp g p μ) (hf : ae_measurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, f x g x) :
theorem measure_theory.mem_ℒp.of_bound {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [measure_theory.finite_measure μ] {f : α → E} (hf : ae_measurable f μ) (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
theorem measure_theory.mem_ℒp.norm {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f : α → E} (h : measure_theory.mem_ℒp f p μ) :
measure_theory.mem_ℒp (λ (x : α), f x) p μ
theorem measure_theory.snorm'_eq_zero_of_ae_zero {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] {f : α → F} (hq0_lt : 0 < q) (hf_zero : f =ᵐ[μ] 0) :
theorem measure_theory.snorm'_eq_zero_of_ae_zero' {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] (hq0_ne : q 0) (hμ : μ 0) {f : α → F} (hf_zero : f =ᵐ[μ] 0) :
theorem measure_theory.ae_eq_zero_of_snorm'_eq_zero {α : Type u_1} {E : Type u_2} [measurable_space α] {q : } {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f : α → E} (hq0 : 0 q) (hf : ae_measurable f μ) (h : measure_theory.snorm' f q μ = 0) :
f =ᵐ[μ] 0
theorem measure_theory.snorm'_eq_zero_iff {α : Type u_1} {E : Type u_2} [measurable_space α] {q : } {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] (hq0_lt : 0 < q) {f : α → E} (hf : ae_measurable f μ) :
theorem measure_theory.coe_nnnorm_ae_le_snorm_ess_sup {α : Type u_1} {F : Type u_3} [measurable_space α] [normed_group F] (f : α → F) (μ : measure_theory.measure α) :
∀ᵐ (x : α) ∂μ, (nnnorm (f x)) measure_theory.snorm_ess_sup f μ
@[simp]
theorem measure_theory.snorm_ess_sup_eq_zero_iff {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
theorem measure_theory.snorm_eq_zero_iff {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [opens_measurable_space E] {f : α → E} (hf : ae_measurable f μ) (h0 : p 0) :
@[simp]
theorem measure_theory.snorm'_neg {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
@[simp]
theorem measure_theory.snorm_neg {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] {f : α → F} :
theorem measure_theory.mem_ℒp.neg {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {f : α → E} (hf : measure_theory.mem_ℒp f p μ) :
theorem measure_theory.snorm'_le_snorm'_mul_rpow_measure_univ {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {p q : } (hp0_lt : 0 < p) (hpq : p q) {f : α → E} (hf : ae_measurable f μ) :
theorem measure_theory.snorm'_le_snorm_ess_sup_mul_rpow_measure_univ {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] (hq_pos : 0 < q) {f : α → F} :
theorem measure_theory.snorm'_le_snorm'_of_exponent_le {α : Type u_1} {E : Type u_2} [measurable_space α] [measurable_space E] [normed_group E] [borel_space E] {p q : } (hp0_lt : 0 < p) (hpq : p q) (μ : measure_theory.measure α) [measure_theory.probability_measure μ] {f : α → E} (hf : ae_measurable f μ) :
theorem measure_theory.snorm'_le_snorm_ess_sup {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] (hq_pos : 0 < q) {f : α → F} [measure_theory.probability_measure μ] :
theorem measure_theory.snorm'_lt_top_of_snorm'_lt_top_of_exponent_le {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {p q : } [measure_theory.finite_measure μ] {f : α → E} (hf : ae_measurable f μ) (hfq_lt_top : measure_theory.snorm' f q μ < ) (hp_nonneg : 0 p) (hpq : p q) :
theorem measure_theory.snorm'_add_le {α : Type u_1} {E : Type u_2} [measurable_space α] {q : } {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hq1 : 1 q) :
theorem measure_theory.snorm_add_le {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hp1 : 1 p) :
theorem measure_theory.snorm'_sum_le {α : Type u_1} {E : Type u_2} [measurable_space α] {q : } {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {ι : Type u_3} {f : ι → α → E} {s : finset ι} (hfs : ∀ (i : ι), i sae_measurable (f i) μ) (hq1 : 1 q) :
measure_theory.snorm' (∑ (i : ι) in s, f i) q μ ∑ (i : ι) in s, measure_theory.snorm' (f i) q μ
theorem measure_theory.snorm_sum_le {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {ι : Type u_3} {f : ι → α → E} {s : finset ι} (hfs : ∀ (i : ι), i sae_measurable (f i) μ) (hp1 : 1 p) :
measure_theory.snorm (∑ (i : ι) in s, f i) p μ ∑ (i : ι) in s, measure_theory.snorm (f i) p μ
theorem measure_theory.snorm_add_lt_top_of_one_le {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {f g : α → E} (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ) (hq1 : 1 p) :
theorem measure_theory.snorm'_add_lt_top_of_le_one {α : Type u_1} {E : Type u_2} [measurable_space α] {q : } {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hf_snorm : measure_theory.snorm' f q μ < ) (hg_snorm : measure_theory.snorm' g q μ < ) (hq_pos : 0 < q) (hq1 : q 1) :
theorem measure_theory.snorm_add_lt_top {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] {f g : α → E} (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ) :
theorem measure_theory.snorm'_const_smul {α : Type u_1} {F : Type u_3} [measurable_space α] {q : } {μ : measure_theory.measure α} [normed_group F] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 F] {f : α → F} (c : 𝕜) (hq0_lt : 0 < q) :
theorem measure_theory.snorm_ess_sup_const_smul {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 F] {f : α → F} (c : 𝕜) :
theorem measure_theory.snorm_const_smul {α : Type u_1} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_group F] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 F] {f : α → F} (c : 𝕜) :
theorem measure_theory.mem_ℒp.const_smul {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] [borel_space E] {f : α → E} (hf : measure_theory.mem_ℒp f p μ) (c : 𝕜) :
theorem measure_theory.mem_ℒp.const_mul {α : Type u_1} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_field 𝕜] [measurable_space 𝕜] [borel_space 𝕜] {f : α → 𝕜} (hf : measure_theory.mem_ℒp f p μ) (c : 𝕜) :
measure_theory.mem_ℒp (λ (x : α), c * f x) p μ
theorem measure_theory.snorm'_smul_le_mul_snorm' {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 E] [opens_measurable_space E] [measurable_space 𝕜] [opens_measurable_space 𝕜] {p q r : } {f : α → E} (hf : ae_measurable f μ) {φ : α → 𝕜} (hφ : ae_measurable φ μ) (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) :
theorem measure_theory.snorm_le_mul_snorm_aux_of_nonneg {α : Type u_1} {F : Type u_3} {G : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] [normed_group G] {f : α → F} {g : α → G} {c : } (h : ∀ᵐ (x : α) ∂μ, f x c * g x) (hc : 0 c) (p : ℝ≥0∞) :
theorem measure_theory.snorm_le_mul_snorm_aux_of_neg {α : Type u_1} {F : Type u_3} {G : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] [normed_group G] {f : α → F} {g : α → G} {c : } (h : ∀ᵐ (x : α) ∂μ, f x c * g x) (hc : c < 0) (p : ℝ≥0∞) :
theorem measure_theory.snorm_le_mul_snorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] [normed_group G] {f : α → F} {g : α → G} {c : } (h : ∀ᵐ (x : α) ∂μ, f x c * g x) (p : ℝ≥0∞) :
theorem measure_theory.mem_ℒp.of_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [measurable_space F] {f : α → E} {g : α → F} {c : } (hg : measure_theory.mem_ℒp g p μ) (hf : ae_measurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, f x c * g x) :

Lp space #

The space of equivalence classes of measurable functions for which snorm f p μ < ∞.

@[simp]
theorem measure_theory.snorm_ae_eq_fun {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : ℝ≥0∞} {f : α → E} (hf : ae_measurable f μ) :

Lp space

Equations

make an element of Lp from a function verifying mem_ℒp

Equations
@[ext]
theorem measure_theory.Lp.ext {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {f g : (measure_theory.Lp E p μ)} (h : f =ᵐ[μ] g) :
f = g
@[simp]
@[simp]
theorem measure_theory.Lp.coe_mk {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {f : α →ₘ[μ] E} (hf : measure_theory.snorm f p μ < ) :
f, hf⟩ = f
theorem measure_theory.Lp.mem_Lp_of_ae_bound {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] [measure_theory.finite_measure μ] {f : α →ₘ[μ] E} (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
@[instance]
Equations

The 𝕜-submodule of elements of α →ₘ[μ] E whose Lp norm is finite. This is Lp E p μ, with extra structure.

Equations
theorem measure_theory.Lp.coe_fn_smul {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] (c : 𝕜) (f : (measure_theory.Lp E p μ)) :
(c f) =ᵐ[μ] c f

Composition on L^p #

We show that Lipschitz functions vanishing at zero act by composition on L^p, and specialize this to the composition with continuous linear maps, and to the definition of the positive part of an L^p function.

theorem lipschitz_with.mem_ℒp_comp_iff_of_antilipschitz {p : ℝ≥0∞} {α : Type u_1} {E : Type u_2} {F : Type u_3} {K K' : ℝ≥0} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [measurable_space F] [normed_group E] [normed_group F] [borel_space E] [borel_space F] [complete_space E] {f : α → E} {g : E → F} (hg : lipschitz_with K g) (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) :

When g is a Lipschitz function sending 0 to 0 and f is in Lp, then g ∘ f is well defined as an element of Lp.

Equations
@[simp]
theorem lipschitz_with.comp_Lp_zero {α : Type u_1} {E : Type u_2} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [topological_space.second_countable_topology E] [borel_space E] [topological_space.second_countable_topology F] [measurable_space F] [borel_space F] {g : E → F} {c : ℝ≥0} (hg : lipschitz_with c g) (g0 : g 0 = 0) :
hg.comp_Lp g0 0 = 0
theorem lipschitz_with.norm_comp_Lp_sub_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [normed_group F] [topological_space.second_countable_topology E] [borel_space E] [topological_space.second_countable_topology F] [measurable_space F] [borel_space F] {g : E → F} {c : ℝ≥0} (hg : lipschitz_with c g) (g0 : g 0 = 0) (f f' : (measure_theory.Lp E p μ)) :
hg.comp_Lp g0 f - hg.comp_Lp g0 f' (c) * f - f'

Composing f : Lp with L : E →L[ℝ] F.

Equations

Composing f : Lp E p μ with L : E →L[ℝ] F, seen as a -linear map on Lp E p μ.

Equations

Composing f : Lp E p μ with L : E →L[ℝ] F, seen as a continuous -linear map on Lp E p μ.

Equations

Positive part of a function in L^p.

Equations

Negative part of a function in L^p.

Equations
theorem measure_theory.Lp.coe_fn_neg_part_eq_max {α : Type u_1} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : (measure_theory.Lp p μ)) :
∀ᵐ (a : α) ∂μ, (measure_theory.Lp.neg_part f) a = max (-f a) 0
theorem measure_theory.Lp.coe_fn_neg_part {α : Type u_1} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : (measure_theory.Lp p μ)) :
∀ᵐ (a : α) ∂μ, (measure_theory.Lp.neg_part f) a = -min (f a) 0

L^p is a complete space #

We show that L^p is a complete space for 1 ≤ p.

theorem measure_theory.Lp.snorm'_lim_eq_lintegral_liminf {α : Type u_1} {G : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [normed_group G] {ι : Type u_2} [nonempty ι] [linear_order ι] {f : ι → α → G} {p : } (hp_nonneg : 0 p) {f_lim : α → G} (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ι), f n x) filter.at_top (𝓝 (f_lim x))) :
measure_theory.snorm' f_lim p μ = (∫⁻ (a : α), filter.at_top.liminf (λ (m : ι), (nnnorm (f m a)) ^ p) μ) ^ (1 / p)
theorem measure_theory.Lp.snorm'_lim_le_liminf_snorm' {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {E : Type u_2} [measurable_space E] [normed_group E] [borel_space E] {f : α → E} {p : } (hp_pos : 0 < p) (hf : ∀ (n : ), ae_measurable (f n) μ) {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 (f_lim x))) :
theorem measure_theory.Lp.snorm_exponent_top_lim_eq_ess_sup_liminf {α : Type u_1} {G : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [normed_group G] {ι : Type u_2} [nonempty ι] [linear_order ι] {f : ι → α → G} {f_lim : α → G} (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ι), f n x) filter.at_top (𝓝 (f_lim x))) :
measure_theory.snorm f_lim μ = ess_sup (λ (x : α), filter.at_top.liminf (λ (m : ι), (nnnorm (f m x)))) μ
theorem measure_theory.Lp.snorm_exponent_top_lim_le_liminf_snorm_exponent_top {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {ι : Type u_2} [nonempty ι] [encodable ι] [linear_order ι] {f : ι → α → F} {f_lim : α → F} (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ι), f n x) filter.at_top (𝓝 (f_lim x))) :
theorem measure_theory.Lp.snorm_lim_le_liminf_snorm {α : Type u_1} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} {E : Type u_2} [measurable_space E] [normed_group E] [borel_space E] {f : α → E} (hf : ∀ (n : ), ae_measurable (f n) μ) (f_lim : α → E) (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 (f_lim x))) :

Lp is complete iff Cauchy sequences of ℒp have limits in ℒp #

theorem measure_theory.Lp.tendsto_Lp_of_tendsto_ℒp {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {ι : Type u_3} [linear_order ι] [hp : fact (1 p)] {f : ι → (measure_theory.Lp E p μ)} (f_lim : α → E) (f_lim_ℒp : measure_theory.mem_ℒp f_lim p μ) (h_tendsto : filter.tendsto (λ (n : ι), measure_theory.snorm ((f n) - f_lim) p μ) filter.at_top (𝓝 0)) :
theorem measure_theory.Lp.complete_space_Lp_of_cauchy_complete_ℒp {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] [hp : fact (1 p)] (H : ∀ (f : α → E), (∀ (n : ), measure_theory.mem_ℒp (f n) p μ)∀ (B : ℝ≥0∞), ∑' (i : ), B i < (∀ (N n m : ), N nN mmeasure_theory.snorm (f n - f m) p μ < B N)(∃ (f_lim : α → E) (hf_lim_meas : measure_theory.mem_ℒp f_lim p μ), filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (𝓝 0))) :

Prove that controlled Cauchy sequences of ℒp have limits in ℒp #

theorem measure_theory.Lp.ae_tendsto_of_cauchy_snorm' {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] {f : α → E} {p : } (hf : ∀ (n : ), ae_measurable (f n) μ) (hp1 : 1 p) {B : ℝ≥0∞} (hB : ∑' (i : ), B i < ) (h_cau : ∀ (N n m : ), N nN mmeasure_theory.snorm' (f n - f m) p μ < B N) :
∀ᵐ (x : α) ∂μ, ∃ (l : E), filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 l)
theorem measure_theory.Lp.ae_tendsto_of_cauchy_snorm {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] {f : α → E} (hf : ∀ (n : ), ae_measurable (f n) μ) (hp : 1 p) {B : ℝ≥0∞} (hB : ∑' (i : ), B i < ) (h_cau : ∀ (N n m : ), N nN mmeasure_theory.snorm (f n - f m) p μ < B N) :
∀ᵐ (x : α) ∂μ, ∃ (l : E), filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 l)
theorem measure_theory.Lp.cauchy_tendsto_of_tendsto {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] {f : α → E} (hf : ∀ (n : ), ae_measurable (f n) μ) (f_lim : α → E) {B : ℝ≥0∞} (hB : ∑' (i : ), B i < ) (h_cau : ∀ (N n m : ), N nN mmeasure_theory.snorm (f n - f m) p μ < B N) (h_lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 (f_lim x))) :
filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (𝓝 0)
theorem measure_theory.Lp.mem_ℒp_of_cauchy_tendsto {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] (hp : 1 p) {f : α → E} (hf : ∀ (n : ), measure_theory.mem_ℒp (f n) p μ) (f_lim : α → E) (h_lim_meas : ae_measurable f_lim μ) (h_tendsto : filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (𝓝 0)) :
theorem measure_theory.Lp.cauchy_complete_ℒp {α : Type u_1} {E : Type u_2} [measurable_space α] {p : ℝ≥0∞} {μ : measure_theory.measure α} [measurable_space E] [normed_group E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] (hp : 1 p) {f : α → E} (hf : ∀ (n : ), measure_theory.mem_ℒp (f n) p μ) {B : ℝ≥0∞} (hB : ∑' (i : ), B i < ) (h_cau : ∀ (N n m : ), N nN mmeasure_theory.snorm (f n - f m) p μ < B N) :
∃ (f_lim : α → E) (hf_lim_meas : measure_theory.mem_ℒp f_lim p μ), filter.tendsto (λ (n : ), measure_theory.snorm (f n - f_lim) p μ) filter.at_top (𝓝 0)

Lp is complete for 1 ≤ p #

The Lp-norm of a bounded continuous function is at most a constant (depending on the measure of the whole space) times its sup-norm.

The bounded linear map of considering a continuous function on a compact finite-measure space α as an element of Lp. By definition, the norm on C(α, E) is the sup-norm, transferred from the space α →ᵇ E of bounded continuous functions, so this construction is just a matter of transferring the structure from bounded_continuous_function.to_Lp along the isometry.

Equations