mathlib documentation

measure_theory.lp_space

ℒp space

This file describes properties of measurable functions with finite seminorm (∫ ∥f a∥^p ∂μ) ^ (1/p) for p:ℝ with 1 ≤ p.

Main definitions

Notation

def ℒp_space.mem_ℒp {α : Type u_1} {E : Type u_2} [measurable_space α] [measurable_space E] [normed_group E] (f : α → E) (p : ) (μ : measure_theory.measure α) :
Prop

The property that f:α→E is ae_measurable and ∫ ∥f a∥^p ∂μ is finite

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

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

Equations
theorem ℒp_space.lintegral_rpow_nnnorm_eq_rpow_snorm {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } {f : α → F} (hp0_lt : 0 < p) :
∫⁻ (a : α), (nnnorm (f a)) ^ p μ = ℒp_space.snorm f p μ ^ p

theorem ℒp_space.mem_ℒp.snorm_lt_top {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } {f : α → E} (hp0 : 0 p) (hfp : ℒp_space.mem_ℒp f p μ) :

theorem ℒp_space.mem_ℒp.snorm_ne_top {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } {f : α → E} (hp0 : 0 p) (hfp : ℒp_space.mem_ℒp f p μ) :

theorem ℒp_space.lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } {f : α → F} (hp0_lt : 0 < p) (hfp : ℒp_space.snorm f p μ < ) :
∫⁻ (a : α), (nnnorm (f a)) ^ p μ <

theorem ℒp_space.mem_ℒp_of_snorm_lt_top {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } {f : α → E} (hp0_lt : 0 < p) (hfm : ae_measurable f μ) (hfp : ℒp_space.snorm f p μ < ) :

@[simp]
theorem ℒp_space.snorm_exponent_zero {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {f : α → F} :

theorem ℒp_space.zero_mem_ℒp_of_pos {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } (hp_pos : 0 < p) :

@[simp]
theorem ℒp_space.snorm_zero {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } (hp0_lt : 0 < p) :

@[simp]
theorem ℒp_space.snorm_zero' {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } (hp0_ne : p 0) (hμ : μ 0) :

theorem ℒp_space.snorm_measure_zero_of_pos {α : Type u_1} {F : Type u_3} [measurable_space α] [normed_group F] {p : } {f : α → F} (hp_pos : 0 < p) :

When μ = 0, we have ∫ f^p ∂μ = 0. snorm f p μ is then 0, 1 or depending on p.

theorem ℒp_space.snorm_measure_zero_of_exponent_zero {α : Type u_1} {F : Type u_3} [measurable_space α] [normed_group F] {f : α → F} :

When μ = 0, we have ∫ f^p ∂μ = 0. snorm f p μ is then 0, 1 or depending on p.

theorem ℒp_space.snorm_measure_zero_of_neg {α : Type u_1} {F : Type u_3} [measurable_space α] [normed_group F] {p : } {f : α → F} (hp_neg : p < 0) :

When μ = 0, we have ∫ f^p ∂μ = 0. snorm f p μ is then 0, 1 or depending on p.

theorem ℒp_space.snorm_const {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } (c : F) (hp_pos : 0 < p) :
ℒp_space.snorm (λ (x : α), c) p μ = ((nnnorm c)) * μ set.univ ^ (1 / p)

theorem ℒp_space.snorm_const' {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } [measure_theory.finite_measure μ] (c : F) (hc_ne_zero : c 0) (hp_ne_zero : p 0) :
ℒp_space.snorm (λ (x : α), c) p μ = ((nnnorm c)) * μ set.univ ^ (1 / p)

theorem ℒp_space.snorm_const_of_probability_measure {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } (c : F) (hp_pos : 0 < p) [measure_theory.probability_measure μ] :
ℒp_space.snorm (λ (x : α), c) p μ = (nnnorm c)

theorem ℒp_space.mem_ℒp_const {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } (c : E) (h : c 0 0 p) [measure_theory.finite_measure μ] :
ℒp_space.mem_ℒp (λ (a : α), c) p μ

theorem ℒp_space.mem_ℒp_const_of_nonneg {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } (c : E) (hp0 : 0 p) [measure_theory.finite_measure μ] :
ℒp_space.mem_ℒp (λ (a : α), c) p μ

theorem ℒp_space.mem_ℒp_const_of_ne_zero {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } (c : E) (hc : c 0) [measure_theory.finite_measure μ] :
ℒp_space.mem_ℒp (λ (a : α), c) p μ

theorem ℒp_space.snorm_congr_ae {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } {f g : α → F} (hfg : f =ᵐ[μ] g) :

theorem ℒp_space.mem_ℒp.ae_eq {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } {f g : α → E} (hfg : f =ᵐ[μ] g) (hf_Lp : ℒp_space.mem_ℒp f p μ) :

theorem ℒp_space.mem_ℒp_congr_ae {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } {f g : α → E} (hfg : f =ᵐ[μ] g) :

theorem ℒp_space.snorm_eq_zero_of_ae_zero {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } {f : α → F} (hp0_lt : 0 < p) (hf_zero : f =ᵐ[μ] 0) :

theorem ℒp_space.snorm_eq_zero_of_ae_zero' {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } (hp0_ne : p 0) (hμ : μ 0) {f : α → F} (hf_zero : f =ᵐ[μ] 0) :

theorem ℒp_space.ae_eq_zero_of_snorm_eq_zero {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } [opens_measurable_space E] {f : α → E} (hp0 : 0 p) (hf : ae_measurable f μ) (h : ℒp_space.snorm f p μ = 0) :
f =ᵐ[μ] 0

theorem ℒp_space.snorm_eq_zero_iff {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } [opens_measurable_space E] (hp0_lt : 0 < p) {f : α → E} (hf : ae_measurable f μ) :
ℒp_space.snorm f p μ = 0 f =ᵐ[μ] 0

@[simp]
theorem ℒp_space.snorm_neg {α : Type u_1} {F : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group F] {p : } {f : α → F} :

theorem ℒp_space.mem_ℒp.neg {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } [borel_space E] {f : α → E} (hf : ℒp_space.mem_ℒp f p μ) :

theorem ℒp_space.snorm_le_snorm_mul_rpow_measure_univ {α : 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 α) {f : α → E} (hf : ae_measurable f μ) :
ℒp_space.snorm f p μ (ℒp_space.snorm f q μ) * μ set.univ ^ (1 / p - 1 / q)

theorem ℒp_space.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 ℒp_space.mem_ℒp.mem_ℒp_of_exponent_le {α : Type u_1} {E : Type u_2} [measurable_space α] [measurable_space E] [normed_group E] [borel_space E] {p q : } {μ : measure_theory.measure α} [measure_theory.finite_measure μ] {f : α → E} (hfq : ℒp_space.mem_ℒp f q μ) (hp_pos : 0 < p) (hpq : p q) :

theorem ℒp_space.mem_ℒp.integrable {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } [borel_space E] (hp1 : 1 p) {f : α → E} [measure_theory.finite_measure μ] (hfp : ℒp_space.mem_ℒp f p μ) :

theorem ℒp_space.snorm_add_le {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } [borel_space E] {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hp1 : 1 p) :

theorem ℒp_space.mem_ℒp.add {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } [borel_space E] [topological_space.second_countable_topology E] {f g : α → E} (hf : ℒp_space.mem_ℒp f p μ) (hg : ℒp_space.mem_ℒp g p μ) (hp1 : 1 p) :

theorem ℒp_space.mem_ℒp.sub {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } [borel_space E] [topological_space.second_countable_topology E] {f g : α → E} (hf : ℒp_space.mem_ℒp f p μ) (hg : ℒp_space.mem_ℒp g p μ) (hp1 : 1 p) :

theorem ℒp_space.mem_ℒp.const_smul {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } [borel_space E] {𝕜 : Type u_4} [normed_field 𝕜] [normed_space 𝕜 E] {f : α → E} (hfp : ℒp_space.mem_ℒp f p μ) (c : 𝕜) (hp0 : 0 p) :

theorem ℒp_space.snorm_const_smul {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } [borel_space E] {𝕜 : Type u_4} [normed_field 𝕜] [normed_space 𝕜 E] {f : α → E} (hf : ae_measurable f μ) (c : 𝕜) (hp0_lt : 0 < p) :

theorem ℒp_space.snorm_smul_le_mul_snorm {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [normed_group E] {p : } [borel_space E] {𝕜 : Type u_4} [normed_field 𝕜] [normed_space 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] {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) :