ℒp space #
This file describes properties of almost everywhere strongly measurable functions with finite
p-seminorm, denoted by eLpNorm f p μ and defined for p:ℝ≥0∞ as 0 if p=0,
(∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and essSup ‖f‖ μ for p=∞.
The Prop-valued Memℒp f p μ states that a function f : α → E has finite p-seminorm
and is almost everywhere strongly measurable.
Main definitions #
eLpNorm' f p μ:(∫ ‖f a‖^p ∂μ) ^ (1/p)forf : α → Fandp : ℝ, whereαis a measurable space andFis a normed group.eLpNormEssSup f μ: seminorm inℒ∞, equal to the essential supremumessSup ‖f‖ μ.eLpNorm f p μ: forp : ℝ≥0∞, seminorm inℒp, equal to0forp=0, toeLpNorm' f p μfor0 < p < ∞and toeLpNormEssSup f μforp = ∞.Memℒp f p μ: property that the functionfis almost everywhere strongly measurable and has finitep-seminorm for the measureμ(eLpNorm f p μ < ∞)
ℒp seminorm #
We define the ℒp seminorm, denoted by eLpNorm f p μ. For real p, it is given by an integral
formula (for which we use the notation eLpNorm' f p μ), and for p = ∞ it is the essential
supremum (for which we use the notation eLpNormEssSup f μ).
We also define a predicate Memℒp f p μ, requesting that a function is almost everywhere
measurable and has finite eLpNorm 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 eLpNorm' and eLpNormEssSup when it makes sense,
deduce it for eLpNorm, and translate it in terms of Memℒp.
def
MeasureTheory.eLpNorm'
{α : Type u_1}
{ε : Type u_2}
[ENorm ε]
{x✝ : MeasurableSpace α}
(f : α → ε)
(q : ℝ)
(μ : Measure α)
:
(∫ ‖f a‖^q ∂μ) ^ (1/q), which is a seminorm on the space of measurable functions for which
this quantity is finite
@[deprecated MeasureTheory.eLpNorm'_eq_lintegral_enorm (since := "2025-01-17")]
theorem
MeasureTheory.eLpNorm'_eq_lintegral_nnnorm
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
{x✝ : MeasurableSpace α}
(f : α → F)
(q : ℝ)
(μ : Measure α)
:
def
MeasureTheory.eLpNormEssSup
{α : Type u_1}
{ε : Type u_2}
[ENorm ε]
{x✝ : MeasurableSpace α}
(f : α → ε)
(μ : Measure α)
:
seminorm for ℒ∞, equal to the essential supremum of ‖f‖.
Equations
- MeasureTheory.eLpNormEssSup f μ = essSup (fun (x : α) => ‖f x‖ₑ) μ
theorem
MeasureTheory.eLpNormEssSup_eq_essSup_enorm
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
{x✝ : MeasurableSpace α}
(f : α → F)
(μ : Measure α)
:
@[deprecated MeasureTheory.eLpNormEssSup_eq_essSup_enorm (since := "2025-01-17")]
theorem
MeasureTheory.eLpNormEssSup_eq_essSup_nnnorm
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
{x✝ : MeasurableSpace α}
(f : α → F)
(μ : Measure α)
:
def
MeasureTheory.eLpNorm
{α : Type u_1}
{ε : Type u_2}
[ENorm ε]
{x✝ : MeasurableSpace α}
(f : α → ε)
(p : ENNReal)
(μ : Measure α := by volume_tac)
:
ℒp seminorm, equal to 0 for p=0, to (∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and to
essSup ‖f‖ μ for p = ∞.
theorem
MeasureTheory.eLpNorm_nnreal_eq_eLpNorm'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{p : NNReal}
(hp : p ≠ 0)
:
@[deprecated MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm (since := "2025-01-17")]
theorem
MeasureTheory.eLpNorm_eq_lintegral_rpow_nnnorm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{f : α → F}
:
theorem
MeasureTheory.eLpNorm_one_eq_lintegral_enorm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
@[deprecated MeasureTheory.eLpNorm_one_eq_lintegral_enorm (since := "2025-01-17")]
theorem
MeasureTheory.eLpNorm_one_eq_lintegral_nnnorm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
@[simp]
theorem
MeasureTheory.eLpNorm_exponent_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
def
MeasureTheory.Memℒp
{ε : Type u_2}
[ENorm ε]
{α : Type u_6}
{x✝ : MeasurableSpace α}
[TopologicalSpace ε]
(f : α → ε)
(p : ENNReal)
(μ : Measure α := by volume_tac)
:
The property that f:α→E is ae strongly measurable and (∫ ‖f a‖^p ∂μ)^(1/p) is finite
if p < ∞, or essSup f < ∞ if p = ∞.
Equations
- MeasureTheory.Memℒp f p μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.eLpNorm f p μ < ⊤)
theorem
MeasureTheory.Memℒp.aestronglyMeasurable
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
{p : ENNReal}
(h : Memℒp f p μ)
:
@[deprecated MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm' (since := "2025-01-17")]
theorem
MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_eLpNorm'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
:
Alias of MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm'.
theorem
MeasureTheory.Memℒp.eLpNorm_lt_top
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hfp : Memℒp f p μ)
:
theorem
MeasureTheory.Memℒp.eLpNorm_ne_top
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hfp : Memℒp f p μ)
:
@[deprecated MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top (since := "2025-01-17")]
theorem
MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
(hfq : eLpNorm' f q μ < ⊤)
:
Alias of MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top.
@[deprecated MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top (since := "2025-01-17")]
theorem
MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm_lt_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hfp : eLpNorm f p μ < ⊤)
:
Alias of MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top.
@[simp]
theorem
MeasureTheory.eLpNorm'_exponent_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
@[simp]
theorem
MeasureTheory.eLpNorm_exponent_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
@[simp]
theorem
MeasureTheory.memℒp_zero_iff_aestronglyMeasurable
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
:
@[simp]
theorem
MeasureTheory.eLpNorm'_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
(hp0_lt : 0 < q)
:
@[simp]
theorem
MeasureTheory.eLpNorm'_zero'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
(hq0_ne : q ≠ 0)
(hμ : μ ≠ 0)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
:
@[simp]
theorem
MeasureTheory.eLpNorm_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
:
@[simp]
theorem
MeasureTheory.eLpNorm_zero'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
:
@[simp]
theorem
MeasureTheory.Memℒp.zero
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
:
Memℒp 0 p μ
@[simp]
theorem
MeasureTheory.Memℒp.zero'
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
:
Memℒp (fun (x : α) => 0) p μ
@[deprecated MeasureTheory.Memℒp.zero (since := "2025-01-21")]
theorem
MeasureTheory.zero_memℒp
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
:
Memℒp 0 p μ
Alias of MeasureTheory.Memℒp.zero.
@[deprecated MeasureTheory.Memℒp.zero' (since := "2025-01-21")]
theorem
MeasureTheory.zero_mem_ℒp
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
:
Memℒp (fun (x : α) => 0) p μ
Alias of MeasureTheory.Memℒp.zero'.
theorem
MeasureTheory.eLpNorm'_measure_zero_of_pos
{α : Type u_1}
{F : Type u_4}
{q : ℝ}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
(hq_pos : 0 < q)
:
theorem
MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
theorem
MeasureTheory.eLpNorm'_measure_zero_of_neg
{α : Type u_1}
{F : Type u_4}
{q : ℝ}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
(hq_neg : q < 0)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_measure_zero
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
@[simp]
theorem
MeasureTheory.eLpNorm_measure_zero
{α : Type u_1}
{F : Type u_4}
{p : ENNReal}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
@[simp]
theorem
MeasureTheory.memℒp_measure_zero
{α : Type u_1}
{F : Type u_4}
{p : ENNReal}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
Memℒp f p 0
@[simp]
theorem
MeasureTheory.eLpNorm'_neg
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(q : ℝ)
(μ : Measure α)
:
@[simp]
theorem
MeasureTheory.eLpNorm_neg
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(p : ENNReal)
(μ : Measure α)
:
theorem
MeasureTheory.eLpNorm_sub_comm
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
(f g : α → E)
(p : ENNReal)
(μ : Measure α)
:
theorem
MeasureTheory.Memℒp.neg
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : Memℒp f p μ)
:
theorem
MeasureTheory.memℒp_neg_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
:
theorem
MeasureTheory.eLpNormEssSup_const
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
(c : F)
(hμ : μ ≠ 0)
:
theorem
MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
(c : F)
(hq_pos : 0 < q)
[IsProbabilityMeasure μ]
:
theorem
MeasureTheory.memℒp_const
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
(c : E)
[IsFiniteMeasure μ]
:
Memℒp (fun (x : α) => c) p μ
theorem
MeasureTheory.memℒp_top_const
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
(c : E)
:
theorem
MeasureTheory.eLpNorm'_congr_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.eLpNormEssSup_congr_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.eLpNormEssSup_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm_mono_nnnorm
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ (x : α), ‖f x‖₊ ≤ ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm_mono
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ (x : α), ‖f x‖ ≤ ‖g x‖)
:
theorem
MeasureTheory.eLpNorm_mono_real
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → ℝ}
(h : ∀ (x : α), ‖f x‖ ≤ g x)
:
theorem
MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
theorem
MeasureTheory.eLpNormEssSup_le_of_ae_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
theorem
MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
theorem
MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
@[simp]
theorem
MeasureTheory.eLpNorm'_norm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
@[simp]
theorem
MeasureTheory.eLpNorm_norm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
(f : α → F)
:
theorem
MeasureTheory.eLpNorm_congr_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.memℒp_congr_ae
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f g : α → E}
(hfg : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.Memℒp.ae_eq
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f g : α → E}
(hfg : f =ᶠ[ae μ] g)
(hf_Lp : Memℒp f p μ)
:
Memℒp g p μ
theorem
MeasureTheory.Memℒp.of_le
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hg : Memℒp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
Memℒp f p μ
theorem
MeasureTheory.Memℒp.mono
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hg : Memℒp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
Memℒp f p μ
Alias of MeasureTheory.Memℒp.of_le.
theorem
MeasureTheory.Memℒp.mono'
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → ℝ}
(hg : Memℒp g p μ)
(hf : AEStronglyMeasurable f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a)
:
Memℒp f p μ
theorem
MeasureTheory.Memℒp.congr_norm
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hf : Memℒp f p μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
Memℒp g p μ
theorem
MeasureTheory.memℒp_congr_norm
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
theorem
MeasureTheory.memℒp_top_of_bound
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : AEStronglyMeasurable f μ)
(C : ℝ)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
theorem
MeasureTheory.Memℒp.of_bound
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[IsFiniteMeasure μ]
{f : α → E}
(hf : AEStronglyMeasurable f μ)
(C : ℝ)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
Memℒp f p μ
theorem
MeasureTheory.memℒp_of_bounded
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
{a b : ℝ}
{f : α → ℝ}
(h : ∀ᵐ (x : α) ∂μ, f x ∈ Set.Icc a b)
(hX : AEStronglyMeasurable f μ)
(p : ENNReal)
:
Memℒp f p μ
theorem
MeasureTheory.eLpNorm'_mono_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ ν : Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν ≤ μ)
(hq : 0 ≤ q)
:
theorem
MeasureTheory.eLpNormEssSup_mono_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ ν : Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν.AbsolutelyContinuous μ)
:
theorem
MeasureTheory.eLpNorm_mono_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν ≤ μ)
:
theorem
MeasureTheory.Memℒp.mono_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hμν : ν ≤ μ)
(hf : Memℒp f p μ)
:
Memℒp f p ν
theorem
MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
:
@[deprecated MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict (since := "2025-01-07")]
theorem
MeasureTheory.eLpNorm_indicator_eq_restrict
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
:
Alias of MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict.
theorem
MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.eLpNorm_restrict_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(p : ENNReal)
(μ : Measure α)
(s : Set α)
:
theorem
MeasureTheory.eLpNorm_indicator_le
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f : α → E)
:
theorem
MeasureTheory.eLpNormEssSup_indicator_le
{α : Type u_1}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup G]
(s : Set α)
(f : α → G)
:
theorem
MeasureTheory.eLpNormEssSup_indicator_const_le
{α : Type u_1}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup G]
(s : Set α)
(c : G)
:
theorem
MeasureTheory.eLpNormEssSup_indicator_const_eq
{α : Type u_1}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup G]
(s : Set α)
(c : G)
(hμs : μ s ≠ 0)
:
theorem
MeasureTheory.eLpNorm_indicator_const₀
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{c : F}
{s : Set α}
(hs : NullMeasurableSet s μ)
(hp : p ≠ 0)
(hp_top : p ≠ ⊤)
:
theorem
MeasureTheory.eLpNorm_indicator_const
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{c : F}
{s : Set α}
(hs : MeasurableSet s)
(hp : p ≠ 0)
(hp_top : p ≠ ⊤)
:
theorem
MeasureTheory.eLpNorm_indicator_const'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{c : F}
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ 0)
(hp : p ≠ 0)
:
theorem
MeasureTheory.Memℒp.indicator
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
(hf : Memℒp f p μ)
:
theorem
MeasureTheory.memℒp_indicator_iff_restrict
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.memℒp_indicator_const
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{s : Set α}
(p : ENNReal)
(hs : MeasurableSet s)
(c : E)
(hμsc : c = 0 ∨ μ s ≠ ⊤)
:
theorem
MeasureTheory.eLpNormEssSup_piecewise
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f g : α → E)
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
eLpNormEssSup (s.piecewise f g) μ = eLpNormEssSup f (μ.restrict s) ⊔ eLpNormEssSup g (μ.restrict sᶜ)
theorem
MeasureTheory.eLpNorm_top_piecewise
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f g : α → E)
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Memℒp.piecewise
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
[DecidablePred fun (x : α) => x ∈ s]
{g : α → F}
(hs : MeasurableSet s)
(hf : Memℒp f p (μ.restrict s))
(hg : Memℒp g p (μ.restrict sᶜ))
:
theorem
MeasureTheory.eLpNorm_restrict_eq_of_support_subset
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{s : Set α}
{f : α → F}
(hsf : Function.support f ⊆ s)
:
For a function f with support in s, the Lᵖ norms of f with respect to μ and
μ.restrict s are the same.
theorem
MeasureTheory.Memℒp.restrict
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
(s : Set α)
{f : α → E}
(hf : Memℒp f p μ)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_smul_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{R : Type u_6}
[Zero R]
[SMulWithZero R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[NoZeroSMulDivisors R ENNReal]
{c : R}
(hc : c ≠ 0)
(f : α → F)
:
theorem
MeasureTheory.eLpNorm_smul_measure_of_ne_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
{c : ENNReal}
(hc : c ≠ 0)
(f : α → F)
(p : ENNReal)
(μ : Measure α)
:
See eLpNorm_smul_measure_of_ne_zero' for a version with scalar multiplication by ℝ≥0.
theorem
MeasureTheory.eLpNorm_smul_measure_of_ne_zero'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
{c : NNReal}
(hc : c ≠ 0)
(f : α → F)
(p : ENNReal)
(μ : Measure α)
:
See eLpNorm_smul_measure_of_ne_zero for a version with scalar multiplication by ℝ≥0∞.
theorem
MeasureTheory.eLpNorm_smul_measure_of_ne_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{p : ENNReal}
(hp_ne_top : p ≠ ⊤)
(f : α → F)
(c : ENNReal)
:
See eLpNorm_smul_measure_of_ne_top' for a version with scalar multiplication by ℝ≥0.
theorem
MeasureTheory.eLpNorm_smul_measure_of_ne_top'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
(hp : p ≠ ⊤)
(c : NNReal)
(f : α → F)
:
See eLpNorm_smul_measure_of_ne_top' for a version with scalar multiplication by ℝ≥0∞.
theorem
MeasureTheory.eLpNorm_one_smul_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
(c : ENNReal)
:
theorem
MeasureTheory.eLpNorm_one_add_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ ν : Measure α)
:
theorem
MeasureTheory.eLpNorm_le_add_measure_right
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ ν : Measure α)
{p : ENNReal}
:
theorem
MeasureTheory.eLpNorm_le_add_measure_left
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ ν : Measure α)
{p : ENNReal}
:
theorem
MeasureTheory.eLpNormEssSup_eq_iSup
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
(hμ : ∀ (a : α), μ {a} ≠ 0)
(f : α → E)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_count
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
[MeasurableSingletonClass α]
(f : α → E)
:
theorem
MeasureTheory.Memℒp.left_of_add_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(h : Memℒp f p (μ + ν))
:
Memℒp f p μ
theorem
MeasureTheory.Memℒp.right_of_add_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(h : Memℒp f p (μ + ν))
:
Memℒp f p ν
theorem
MeasureTheory.Memℒp.norm
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(h : Memℒp f p μ)
:
theorem
MeasureTheory.memℒp_norm_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hq0 : 0 ≤ q)
(hf : AEStronglyMeasurable f μ)
(h : eLpNorm' f q μ = 0)
:
theorem
MeasureTheory.eLpNorm'_eq_zero_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup E]
(hq0_lt : 0 < q)
{f : α → E}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.coe_nnnorm_ae_le_eLpNormEssSup
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
{x✝ : MeasurableSpace α}
(f : α → F)
(μ : Measure α)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_eq_zero_iff
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
theorem
MeasureTheory.eLpNorm_eq_zero_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : AEStronglyMeasurable f μ)
(h0 : p ≠ 0)
:
theorem
MeasureTheory.eLpNorm_eq_zero_of_ae_zero
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : f =ᶠ[ae μ] 0)
:
theorem
MeasureTheory.ae_le_eLpNormEssSup
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
theorem
MeasureTheory.eLpNormEssSup_lt_top_iff_isBoundedUnder
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
theorem
MeasureTheory.meas_eLpNormEssSup_lt
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
theorem
MeasureTheory.eLpNorm_lt_top_of_finite
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
[Finite α]
[IsFiniteMeasure μ]
:
@[simp]
theorem
MeasureTheory.Memℒp.of_discrete
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
[DiscreteMeasurableSpace α]
[Finite α]
[IsFiniteMeasure μ]
:
Memℒp f p μ
@[simp]
theorem
MeasureTheory.eLpNorm_of_isEmpty
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[IsEmpty α]
(f : α → E)
(p : ENNReal)
:
theorem
MeasureTheory.eLpNormEssSup_map_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : AEStronglyMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm_map_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : AEStronglyMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.memℒp_map_measure_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : AEStronglyMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.Memℒp.comp_of_map
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : Memℒp g p (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm_comp_measurePreserving
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
{ν : Measure β}
(hg : AEStronglyMeasurable g ν)
(hf : MeasurePreserving f μ ν)
:
theorem
MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{ν : Measure β}
(g : β →ₘ[ν] E)
(hf : MeasurePreserving f μ ν)
:
theorem
MeasureTheory.Memℒp.comp_measurePreserving
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
{ν : Measure β}
(hg : Memℒp g p ν)
(hf : MeasurePreserving f μ ν)
:
theorem
MeasurableEmbedding.eLpNormEssSup_map_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → F}
(hf : MeasurableEmbedding f)
:
theorem
MeasurableEmbedding.eLpNorm_map_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → F}
(hf : MeasurableEmbedding f)
:
theorem
MeasurableEmbedding.memℒp_map_measure_iff
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → F}
(hf : MeasurableEmbedding f)
:
theorem
MeasurableEquiv.memℒp_map_measure_iff
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{β : Type u_6}
{mβ : MeasurableSpace β}
(f : α ≃ᵐ β)
{g : β → F}
:
theorem
MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
{p : ℝ}
(hp : 0 < p)
:
theorem
MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
(p : ENNReal)
:
theorem
MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(hc : c < 0)
(p : ENNReal)
:
When c is negative, ‖f x‖ ≤ c * ‖g x‖ is nonsense and forces both f and g to have an
eLpNorm of 0.
theorem
MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(p : ENNReal)
:
theorem
MeasureTheory.Memℒp.of_nnnorm_le_mul
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
{c : NNReal}
(hg : Memℒp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
:
Memℒp f p μ
theorem
MeasureTheory.Memℒp.of_le_mul
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
{c : ℝ}
(hg : Memℒp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
:
Memℒp f p μ
Bounded actions by normed rings #
In this section we show inequalities on the norm.
theorem
MeasureTheory.eLpNorm'_const_smul_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
(hq : 0 < q)
:
theorem
MeasureTheory.eLpNormEssSup_const_smul_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
:
theorem
MeasureTheory.eLpNorm_const_smul_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
:
theorem
MeasureTheory.Memℒp.const_smul
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{f : α → F}
(hf : Memℒp f p μ)
(c : 𝕜)
:
theorem
MeasureTheory.Memℒp.const_mul
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{f : α → 𝕜}
(hf : Memℒp f p μ)
(c : 𝕜)
:
Bounded actions by normed division rings #
The inequalities in the previous section are now tight.
theorem
MeasureTheory.eLpNorm'_const_smul
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[BoundedSMul 𝕜 F]
{f : α → F}
(c : 𝕜)
(hq_pos : 0 < q)
:
theorem
MeasureTheory.eLpNormEssSup_const_smul
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[BoundedSMul 𝕜 F]
(c : 𝕜)
(f : α → F)
:
theorem
MeasureTheory.eLpNorm_const_smul
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[BoundedSMul 𝕜 F]
(c : 𝕜)
(f : α → F)
(p : ENNReal)
(μ : Measure α)
:
theorem
MeasureTheory.eLpNorm_nsmul
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(n : ℕ)
(f : α → F)
:
@[simp]
theorem
MeasureTheory.eLpNorm_conj
{α : Type u_1}
{m0 : MeasurableSpace α}
{𝕜 : Type u_6}
[RCLike 𝕜]
(f : α → 𝕜)
(p : ENNReal)
(μ : Measure α)
:
theorem
MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{R : NNReal}
{p : ENNReal}
{f : ℕ → α → E}
(hfmeas : ∀ (n : ℕ), Measurable (f n))
(hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R)
:
theorem
MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{R : NNReal}
{p : ENNReal}
(hp : p ≠ 0)
{f : ℕ → α → E}
(hfmeas : ∀ (n : ℕ), Measurable (f n))
(hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R)
:
theorem
Continuous.memℒp_top_of_hasCompactSupport
{E : Type u_3}
[NormedAddCommGroup E]
{X : Type u_6}
[TopologicalSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
{f : X → E}
(hf : Continuous f)
(h'f : HasCompactSupport f)
(μ : MeasureTheory.Measure X)
:
MeasureTheory.Memℒp f ⊤ μ
A continuous function with compact support belongs to L^∞.
See Continuous.memℒp_of_hasCompactSupport for a version for L^p.
theorem
MeasureTheory.Memℒp.exists_eLpNorm_indicator_compl_lt
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{β : Type u_6}
[NormedAddCommGroup β]
(hp_top : p ≠ ⊤)
{f : α → β}
(hf : Memℒp f p μ)
{ε : ENNReal}
(hε : ε ≠ 0)
:
A single function that is Memℒp f p μ is tight with respect to μ.