ℒp space
This file describes properties of measurable functions with finite seminorm (∫ ∥f a∥^p ∂μ) ^ (1/p)
for p:ℝ with 1 ≤ p.
Main definitions
mem_ℒp f p μ: the functionfhas finite p-seminorm for measureμ, forp:ℝsuch thathp1 : 1 ≤ p,
Notation
snorm f p μ:(∫ ∥f a∥^p ∂μ) ^ (1/p)forf : α → F, whereαis a measurable space andFis a normed group.
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
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
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) :
theorem
ℒp_space.mem_ℒp_one_iff_integrable
{α : Type u_1}
{E : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space E]
[normed_group E]
{f : α → E} :
ℒp_space.mem_ℒp f 1 μ ↔ measure_theory.integrable f μ
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 μ) :
ℒp_space.snorm 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 μ) :
ℒp_space.snorm 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 μ < ⊤) :
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 μ < ⊤) :
ℒp_space.mem_ℒp 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} :
ℒp_space.snorm f 0 μ = 1
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) :
ℒp_space.mem_ℒp 0 p μ
theorem
ℒp_space.zero_mem_ℒp_of_nonneg
{α : Type u_1}
{E : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space E]
[normed_group E]
{p : ℝ}
[measure_theory.finite_measure μ]
(hp0 : 0 ≤ p) :
ℒp_space.mem_ℒp 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) :
ℒp_space.snorm 0 p μ = 0
@[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) :
ℒp_space.snorm 0 p μ = 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) :
ℒp_space.snorm f p 0 = 0
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} :
ℒp_space.snorm f 0 0 = 1
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) :
ℒp_space.snorm f 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) :
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) :
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) :
ℒp_space.snorm f p μ = ℒp_space.snorm g p μ
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 μ) :
ℒp_space.mem_ℒp g 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) :
ℒp_space.mem_ℒp f p μ ↔ ℒp_space.mem_ℒp g p μ
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) :
ℒp_space.snorm f p μ = 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) :
ℒp_space.snorm f p μ = 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) :
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} :
ℒp_space.snorm (-f) p μ = ℒp_space.snorm f p μ
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 μ) :
ℒ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 μ) :
ℒp_space.snorm f p μ ≤ ℒp_space.snorm f q μ
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) :
ℒp_space.mem_ℒp f p μ
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) :
ℒp_space.snorm (f + g) p μ ≤ ℒp_space.snorm f p μ + ℒp_space.snorm g 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) :
ℒp_space.mem_ℒp (f + g) 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) :
ℒp_space.mem_ℒp (f - g) 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) :
ℒp_space.mem_ℒp (c • f) 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) :
ℒp_space.snorm (c • f) p μ = (↑(nnnorm c)) * ℒp_space.snorm f 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) :
ℒp_space.snorm (φ • f) p μ ≤ (ℒp_space.snorm φ q μ) * ℒp_space.snorm f r μ