ℒ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 : ℝ)
(μ : MeasureTheory.Measure α)
:
(∫ ‖f a‖^q ∂μ) ^ (1/q), which is a seminorm on the space of measurable functions for which
this quantity is finite
Instances For
theorem
MeasureTheory.eLpNorm'_eq_lintegral_nnnorm
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
{x✝ : MeasurableSpace α}
(f : α → F)
(q : ℝ)
(μ : MeasureTheory.Measure α)
:
def
MeasureTheory.eLpNormEssSup
{α : Type u_1}
{ε : Type u_2}
[ENorm ε]
{x✝ : MeasurableSpace α}
(f : α → ε)
(μ : MeasureTheory.Measure α)
:
seminorm for ℒ∞, equal to the essential supremum of ‖f‖.
Equations
- MeasureTheory.eLpNormEssSup f μ = essSup (fun (x : α) => ‖f x‖ₑ) μ
Instances For
theorem
MeasureTheory.eLpNormEssSup_eq_essSup_nnnorm
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
{x✝ : MeasurableSpace α}
(f : α → F)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNormEssSup f μ = essSup (fun (x : α) => ↑‖f x‖₊) μ
def
MeasureTheory.eLpNorm
{α : Type u_1}
{ε : Type u_2}
[ENorm ε]
{x✝ : MeasurableSpace α}
(f : α → ε)
(p : ENNReal)
(μ : MeasureTheory.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 = ∞.
Equations
- MeasureTheory.eLpNorm f p μ = if p = 0 then 0 else if p = ⊤ then MeasureTheory.eLpNormEssSup f μ else MeasureTheory.eLpNorm' f p.toReal μ
Instances For
@[deprecated MeasureTheory.eLpNorm (since := "2024-07-26")]
def
MeasureTheory.snorm
{α : Type u_1}
{ε : Type u_2}
[ENorm ε]
{x✝ : MeasurableSpace α}
(f : α → ε)
(p : ENNReal)
(μ : MeasureTheory.Measure α := by volume_tac)
:
Alias of MeasureTheory.eLpNorm.
ℒp seminorm, equal to 0 for p=0, to (∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and to
essSup ‖f‖ μ for p = ∞.
Equations
Instances For
theorem
MeasureTheory.eLpNorm_eq_eLpNorm'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{f : α → F}
:
MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm' f p.toReal μ
@[deprecated MeasureTheory.eLpNorm_eq_eLpNorm' (since := "2024-07-27")]
theorem
MeasureTheory.snorm_eq_snorm'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{f : α → F}
:
MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm' f p.toReal μ
Alias of MeasureTheory.eLpNorm_eq_eLpNorm'.
theorem
MeasureTheory.eLpNorm_nnreal_eq_eLpNorm'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{p : NNReal}
(hp : p ≠ 0)
:
MeasureTheory.eLpNorm f (↑p) μ = MeasureTheory.eLpNorm' f (↑p) μ
@[deprecated MeasureTheory.eLpNorm_nnreal_eq_eLpNorm' (since := "2024-07-27")]
theorem
MeasureTheory.snorm_nnreal_eq_snorm'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{p : NNReal}
(hp : p ≠ 0)
:
MeasureTheory.eLpNorm f (↑p) μ = MeasureTheory.eLpNorm' f (↑p) μ
Alias of MeasureTheory.eLpNorm_nnreal_eq_eLpNorm'.
theorem
MeasureTheory.eLpNorm_eq_lintegral_rpow_nnnorm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{f : α → F}
:
@[deprecated MeasureTheory.eLpNorm_eq_lintegral_rpow_nnnorm (since := "2024-07-27")]
theorem
MeasureTheory.snorm_eq_lintegral_rpow_nnnorm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{f : α → F}
:
theorem
MeasureTheory.eLpNorm_nnreal_eq_lintegral
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{p : NNReal}
(hp : p ≠ 0)
:
@[deprecated MeasureTheory.eLpNorm_nnreal_eq_lintegral (since := "2024-07-27")]
theorem
MeasureTheory.snorm_nnreal_eq_lintegral
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{p : NNReal}
(hp : p ≠ 0)
:
theorem
MeasureTheory.eLpNorm_one_eq_lintegral_nnnorm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNorm f 1 μ = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
@[deprecated MeasureTheory.eLpNorm_one_eq_lintegral_nnnorm (since := "2024-07-27")]
theorem
MeasureTheory.snorm_one_eq_lintegral_nnnorm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNorm f 1 μ = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
@[simp]
theorem
MeasureTheory.eLpNorm_exponent_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
@[deprecated MeasureTheory.eLpNorm_exponent_top (since := "2024-07-27")]
theorem
MeasureTheory.snorm_exponent_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
Alias of MeasureTheory.eLpNorm_exponent_top.
def
MeasureTheory.Memℒp
{ε : Type u_2}
[ENorm ε]
{α : Type u_6}
{x✝ : MeasurableSpace α}
[TopologicalSpace ε]
(f : α → ε)
(p : ENNReal)
(μ : MeasureTheory.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 μ < ⊤)
Instances For
theorem
MeasureTheory.Memℒp.aestronglyMeasurable
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{p : ENNReal}
(h : MeasureTheory.Memℒp f p μ)
:
theorem
MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_eLpNorm'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
:
@[deprecated MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_eLpNorm' (since := "2024-07-27")]
theorem
MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_snorm'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
:
Alias of MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_eLpNorm'.
theorem
MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{p : NNReal}
(hp : p ≠ 0)
:
@[deprecated MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral (since := "2024-07-27")]
theorem
MeasureTheory.snorm_nnreal_pow_eq_lintegral
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{p : NNReal}
(hp : p ≠ 0)
:
theorem
MeasureTheory.Memℒp.eLpNorm_lt_top
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hfp : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.eLpNorm f p μ < ⊤
@[deprecated MeasureTheory.Memℒp.eLpNorm_lt_top (since := "2024-07-27")]
theorem
MeasureTheory.Memℒp.snorm_lt_top
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hfp : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.eLpNorm f p μ < ⊤
Alias of MeasureTheory.Memℒp.eLpNorm_lt_top.
theorem
MeasureTheory.Memℒp.eLpNorm_ne_top
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hfp : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.eLpNorm f p μ ≠ ⊤
@[deprecated MeasureTheory.Memℒp.eLpNorm_ne_top (since := "2024-07-27")]
theorem
MeasureTheory.Memℒp.snorm_ne_top
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hfp : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.eLpNorm f p μ ≠ ⊤
Alias of MeasureTheory.Memℒp.eLpNorm_ne_top.
theorem
MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
(hfq : MeasureTheory.eLpNorm' f q μ < ⊤)
:
@[deprecated MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top (since := "2024-07-27")]
theorem
MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
(hfq : MeasureTheory.eLpNorm' f q μ < ⊤)
:
Alias of MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top.
theorem
MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm_lt_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hfp : MeasureTheory.eLpNorm f p μ < ⊤)
:
@[deprecated MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm_lt_top (since := "2024-07-27")]
theorem
MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hfp : MeasureTheory.eLpNorm f p μ < ⊤)
:
Alias of MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm_lt_top.
theorem
MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
@[deprecated MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top (since := "2024-07-27")]
theorem
MeasureTheory.snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
Alias of MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top.
@[simp]
theorem
MeasureTheory.eLpNorm'_exponent_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNorm' f 0 μ = 1
@[deprecated MeasureTheory.eLpNorm'_exponent_zero (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_exponent_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNorm' f 0 μ = 1
Alias of MeasureTheory.eLpNorm'_exponent_zero.
@[simp]
theorem
MeasureTheory.eLpNorm_exponent_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNorm f 0 μ = 0
@[deprecated MeasureTheory.eLpNorm_exponent_zero (since := "2024-07-27")]
theorem
MeasureTheory.snorm_exponent_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNorm f 0 μ = 0
Alias of MeasureTheory.eLpNorm_exponent_zero.
@[simp]
theorem
MeasureTheory.memℒp_zero_iff_aestronglyMeasurable
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
:
@[simp]
theorem
MeasureTheory.eLpNorm'_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp0_lt : 0 < q)
:
MeasureTheory.eLpNorm' 0 q μ = 0
@[deprecated MeasureTheory.eLpNorm'_zero (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp0_lt : 0 < q)
:
MeasureTheory.eLpNorm' 0 q μ = 0
Alias of MeasureTheory.eLpNorm'_zero.
@[simp]
theorem
MeasureTheory.eLpNorm'_zero'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hq0_ne : q ≠ 0)
(hμ : μ ≠ 0)
:
MeasureTheory.eLpNorm' 0 q μ = 0
@[deprecated MeasureTheory.eLpNorm'_zero' (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_zero'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hq0_ne : q ≠ 0)
(hμ : μ ≠ 0)
:
MeasureTheory.eLpNorm' 0 q μ = 0
Alias of MeasureTheory.eLpNorm'_zero'.
@[simp]
theorem
MeasureTheory.eLpNormEssSup_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
:
MeasureTheory.eLpNormEssSup 0 μ = 0
@[deprecated MeasureTheory.eLpNormEssSup_zero (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
:
MeasureTheory.eLpNormEssSup 0 μ = 0
Alias of MeasureTheory.eLpNormEssSup_zero.
@[simp]
theorem
MeasureTheory.eLpNorm_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
:
MeasureTheory.eLpNorm 0 p μ = 0
@[deprecated MeasureTheory.eLpNorm_zero (since := "2024-07-27")]
theorem
MeasureTheory.snorm_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
:
MeasureTheory.eLpNorm 0 p μ = 0
Alias of MeasureTheory.eLpNorm_zero.
@[simp]
theorem
MeasureTheory.eLpNorm_zero'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
:
MeasureTheory.eLpNorm (fun (x : α) => 0) p μ = 0
@[deprecated MeasureTheory.eLpNorm_zero' (since := "2024-07-27")]
theorem
MeasureTheory.snorm_zero'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
:
MeasureTheory.eLpNorm (fun (x : α) => 0) p μ = 0
Alias of MeasureTheory.eLpNorm_zero'.
theorem
MeasureTheory.zero_memℒp
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
MeasureTheory.Memℒp 0 p μ
theorem
MeasureTheory.zero_mem_ℒp'
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
MeasureTheory.Memℒp (fun (x : α) => 0) p μ
theorem
MeasureTheory.eLpNorm'_measure_zero_of_pos
{α : Type u_1}
{F : Type u_4}
{q : ℝ}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
(hq_pos : 0 < q)
:
MeasureTheory.eLpNorm' f q 0 = 0
@[deprecated MeasureTheory.eLpNorm'_measure_zero_of_pos (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_measure_zero_of_pos
{α : Type u_1}
{F : Type u_4}
{q : ℝ}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
(hq_pos : 0 < q)
:
MeasureTheory.eLpNorm' f q 0 = 0
theorem
MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
MeasureTheory.eLpNorm' f 0 0 = 1
@[deprecated MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_measure_zero_of_exponent_zero
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
MeasureTheory.eLpNorm' f 0 0 = 1
Alias of MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero.
theorem
MeasureTheory.eLpNorm'_measure_zero_of_neg
{α : Type u_1}
{F : Type u_4}
{q : ℝ}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
(hq_neg : q < 0)
:
MeasureTheory.eLpNorm' f q 0 = ⊤
@[deprecated MeasureTheory.eLpNorm'_measure_zero_of_neg (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_measure_zero_of_neg
{α : Type u_1}
{F : Type u_4}
{q : ℝ}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
(hq_neg : q < 0)
:
MeasureTheory.eLpNorm' f q 0 = ⊤
@[simp]
theorem
MeasureTheory.eLpNormEssSup_measure_zero
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
MeasureTheory.eLpNormEssSup f 0 = 0
@[deprecated MeasureTheory.eLpNormEssSup_measure_zero (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_measure_zero
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
MeasureTheory.eLpNormEssSup f 0 = 0
Alias of MeasureTheory.eLpNormEssSup_measure_zero.
@[simp]
theorem
MeasureTheory.eLpNorm_measure_zero
{α : Type u_1}
{F : Type u_4}
{p : ENNReal}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
MeasureTheory.eLpNorm f p 0 = 0
@[deprecated MeasureTheory.eLpNorm_measure_zero (since := "2024-07-27")]
theorem
MeasureTheory.snorm_measure_zero
{α : Type u_1}
{F : Type u_4}
{p : ENNReal}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
MeasureTheory.eLpNorm f p 0 = 0
Alias of MeasureTheory.eLpNorm_measure_zero.
@[simp]
theorem
MeasureTheory.memℒp_measure_zero
{α : Type u_1}
{F : Type u_4}
{p : ENNReal}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
MeasureTheory.Memℒp f p 0
@[simp]
theorem
MeasureTheory.eLpNorm'_neg
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(q : ℝ)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm' (-f) q μ = MeasureTheory.eLpNorm' f q μ
@[deprecated MeasureTheory.eLpNorm'_neg (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_neg
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(q : ℝ)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm' (-f) q μ = MeasureTheory.eLpNorm' f q μ
Alias of MeasureTheory.eLpNorm'_neg.
@[simp]
theorem
MeasureTheory.eLpNorm_neg
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(p : ENNReal)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm (-f) p μ = MeasureTheory.eLpNorm f p μ
theorem
MeasureTheory.eLpNorm_sub_comm
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
(f g : α → E)
(p : ENNReal)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm (f - g) p μ = MeasureTheory.eLpNorm (g - f) p μ
@[deprecated MeasureTheory.eLpNorm_neg (since := "2024-07-27")]
theorem
MeasureTheory.snorm_neg
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(p : ENNReal)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm (-f) p μ = MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_neg.
theorem
MeasureTheory.Memℒp.neg
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (-f) p μ
theorem
MeasureTheory.memℒp_neg_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
:
MeasureTheory.Memℒp (-f) p μ ↔ MeasureTheory.Memℒp f p μ
theorem
MeasureTheory.eLpNorm'_const
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(hq_pos : 0 < q)
:
@[deprecated MeasureTheory.eLpNorm'_const (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_const
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(hq_pos : 0 < q)
:
Alias of MeasureTheory.eLpNorm'_const.
theorem
MeasureTheory.eLpNorm'_const'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[MeasureTheory.IsFiniteMeasure μ]
(c : F)
(hc_ne_zero : c ≠ 0)
(hq_ne_zero : q ≠ 0)
:
@[deprecated MeasureTheory.eLpNorm'_const' (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_const'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[MeasureTheory.IsFiniteMeasure μ]
(c : F)
(hc_ne_zero : c ≠ 0)
(hq_ne_zero : q ≠ 0)
:
Alias of MeasureTheory.eLpNorm'_const'.
theorem
MeasureTheory.eLpNormEssSup_const
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(hμ : μ ≠ 0)
:
MeasureTheory.eLpNormEssSup (fun (x : α) => c) μ = ↑‖c‖₊
@[deprecated MeasureTheory.eLpNormEssSup_const (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_const
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(hμ : μ ≠ 0)
:
MeasureTheory.eLpNormEssSup (fun (x : α) => c) μ = ↑‖c‖₊
Alias of MeasureTheory.eLpNormEssSup_const.
theorem
MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(hq_pos : 0 < q)
[MeasureTheory.IsProbabilityMeasure μ]
:
MeasureTheory.eLpNorm' (fun (x : α) => c) q μ = ↑‖c‖₊
@[deprecated MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_const_of_isProbabilityMeasure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(hq_pos : 0 < q)
[MeasureTheory.IsProbabilityMeasure μ]
:
MeasureTheory.eLpNorm' (fun (x : α) => c) q μ = ↑‖c‖₊
Alias of MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure.
theorem
MeasureTheory.eLpNorm_const
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(h0 : p ≠ 0)
(hμ : μ ≠ 0)
:
@[deprecated MeasureTheory.eLpNorm_const (since := "2024-07-27")]
theorem
MeasureTheory.snorm_const
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(h0 : p ≠ 0)
(hμ : μ ≠ 0)
:
Alias of MeasureTheory.eLpNorm_const.
theorem
MeasureTheory.eLpNorm_const'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(h0 : p ≠ 0)
(h_top : p ≠ ⊤)
:
@[deprecated MeasureTheory.eLpNorm_const' (since := "2024-07-27")]
theorem
MeasureTheory.snorm_const'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(h0 : p ≠ 0)
(h_top : p ≠ ⊤)
:
Alias of MeasureTheory.eLpNorm_const'.
theorem
MeasureTheory.eLpNorm_const_lt_top_iff
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ENNReal}
{c : F}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
@[deprecated MeasureTheory.eLpNorm_const_lt_top_iff (since := "2024-07-27")]
theorem
MeasureTheory.snorm_const_lt_top_iff
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ENNReal}
{c : F}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
Alias of MeasureTheory.eLpNorm_const_lt_top_iff.
theorem
MeasureTheory.memℒp_const
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(c : E)
[MeasureTheory.IsFiniteMeasure μ]
:
MeasureTheory.Memℒp (fun (x : α) => c) p μ
theorem
MeasureTheory.memℒp_top_const
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(c : E)
:
MeasureTheory.Memℒp (fun (x : α) => c) ⊤ μ
theorem
MeasureTheory.memℒp_const_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{c : E}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
theorem
MeasureTheory.eLpNorm'_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hq : 0 ≤ q)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ
@[deprecated MeasureTheory.eLpNorm'_mono_nnnorm_ae (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hq : 0 ≤ q)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ
Alias of MeasureTheory.eLpNorm'_mono_nnnorm_ae.
theorem
MeasureTheory.eLpNorm'_mono_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hq : 0 ≤ q)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ
@[deprecated MeasureTheory.eLpNorm'_mono_ae (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_mono_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hq : 0 ≤ q)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ
Alias of MeasureTheory.eLpNorm'_mono_ae.
theorem
MeasureTheory.eLpNorm'_congr_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊)
:
MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
@[deprecated MeasureTheory.eLpNorm'_congr_nnnorm_ae (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_congr_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊)
:
MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
Alias of MeasureTheory.eLpNorm'_congr_nnnorm_ae.
theorem
MeasureTheory.eLpNorm'_congr_norm_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖)
:
MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
@[deprecated MeasureTheory.eLpNorm'_congr_norm_ae (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_congr_norm_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖)
:
MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
Alias of MeasureTheory.eLpNorm'_congr_norm_ae.
theorem
MeasureTheory.eLpNorm'_congr_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : f =ᵐ[μ] g)
:
MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
@[deprecated MeasureTheory.eLpNorm'_congr_ae (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_congr_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : f =ᵐ[μ] g)
:
MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
Alias of MeasureTheory.eLpNorm'_congr_ae.
theorem
MeasureTheory.eLpNormEssSup_congr_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : f =ᵐ[μ] g)
:
@[deprecated MeasureTheory.eLpNormEssSup_congr_ae (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_congr_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : f =ᵐ[μ] g)
:
Alias of MeasureTheory.eLpNormEssSup_congr_ae.
theorem
MeasureTheory.eLpNormEssSup_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
@[deprecated MeasureTheory.eLpNormEssSup_mono_nnnorm_ae (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_mono_nnnorm_ae (since := "2024-07-27")]
theorem
MeasureTheory.snorm_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_mono_nnnorm_ae.
theorem
MeasureTheory.eLpNorm_mono_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_mono_ae (since := "2024-07-27")]
theorem
MeasureTheory.snorm_mono_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_mono_ae.
theorem
MeasureTheory.eLpNorm_mono_ae_real
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_mono_ae_real (since := "2024-07-27")]
theorem
MeasureTheory.snorm_mono_ae_real
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_mono_ae_real.
theorem
MeasureTheory.eLpNorm_mono_nnnorm
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ (x : α), ‖f x‖₊ ≤ ‖g x‖₊)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_mono_nnnorm (since := "2024-07-27")]
theorem
MeasureTheory.snorm_mono_nnnorm
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ (x : α), ‖f x‖₊ ≤ ‖g x‖₊)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_mono_nnnorm.
theorem
MeasureTheory.eLpNorm_mono
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ (x : α), ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_mono (since := "2024-07-27")]
theorem
MeasureTheory.snorm_mono
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ (x : α), ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_mono.
theorem
MeasureTheory.eLpNorm_mono_real
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → ℝ}
(h : ∀ (x : α), ‖f x‖ ≤ g x)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_mono_real (since := "2024-07-27")]
theorem
MeasureTheory.snorm_mono_real
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → ℝ}
(h : ∀ (x : α), ‖f x‖ ≤ g x)
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_mono_real.
theorem
MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
MeasureTheory.eLpNormEssSup f μ ≤ ↑C
@[deprecated MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_le_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
MeasureTheory.eLpNormEssSup f μ ≤ ↑C
theorem
MeasureTheory.eLpNormEssSup_le_of_ae_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
@[deprecated MeasureTheory.eLpNormEssSup_le_of_ae_bound (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_le_of_ae_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
@[deprecated MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_lt_top_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
Alias of MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound.
theorem
MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
@[deprecated MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_lt_top_of_ae_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
theorem
MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
@[deprecated MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound (since := "2024-07-27")]
theorem
MeasureTheory.snorm_le_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
theorem
MeasureTheory.eLpNorm_le_of_ae_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
MeasureTheory.eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C
@[deprecated MeasureTheory.eLpNorm_le_of_ae_bound (since := "2024-07-27")]
theorem
MeasureTheory.snorm_le_of_ae_bound
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
MeasureTheory.eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C
Alias of MeasureTheory.eLpNorm_le_of_ae_bound.
theorem
MeasureTheory.eLpNorm_congr_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊)
:
MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_congr_nnnorm_ae (since := "2024-07-27")]
theorem
MeasureTheory.snorm_congr_nnnorm_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊)
:
MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_congr_nnnorm_ae.
theorem
MeasureTheory.eLpNorm_congr_norm_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖)
:
MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_congr_norm_ae (since := "2024-07-27")]
theorem
MeasureTheory.snorm_congr_norm_ae
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖)
:
MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_congr_norm_ae.
theorem
MeasureTheory.eLpNorm_indicator_sub_indicator
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(s t : Set α)
(f : α → E)
:
MeasureTheory.eLpNorm (s.indicator f - t.indicator f) p μ = MeasureTheory.eLpNorm ((symmDiff s t).indicator f) p μ
@[deprecated MeasureTheory.eLpNorm_indicator_sub_indicator (since := "2024-07-27")]
theorem
MeasureTheory.snorm_indicator_sub_indicator
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(s t : Set α)
(f : α → E)
:
MeasureTheory.eLpNorm (s.indicator f - t.indicator f) p μ = MeasureTheory.eLpNorm ((symmDiff s t).indicator f) p μ
@[simp]
theorem
MeasureTheory.eLpNorm'_norm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNorm' (fun (a : α) => ‖f a‖) q μ = MeasureTheory.eLpNorm' f q μ
@[deprecated MeasureTheory.eLpNorm'_norm (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_norm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNorm' (fun (a : α) => ‖f a‖) q μ = MeasureTheory.eLpNorm' f q μ
Alias of MeasureTheory.eLpNorm'_norm.
@[simp]
theorem
MeasureTheory.eLpNorm_norm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
:
MeasureTheory.eLpNorm (fun (x : α) => ‖f x‖) p μ = MeasureTheory.eLpNorm f p μ
@[deprecated MeasureTheory.eLpNorm_norm (since := "2024-07-27")]
theorem
MeasureTheory.snorm_norm
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
:
MeasureTheory.eLpNorm (fun (x : α) => ‖f x‖) p μ = MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_norm.
theorem
MeasureTheory.eLpNorm'_norm_rpow
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(p q : ℝ)
(hq_pos : 0 < q)
:
MeasureTheory.eLpNorm' (fun (x : α) => ‖f x‖ ^ q) p μ = MeasureTheory.eLpNorm' f (p * q) μ ^ q
@[deprecated MeasureTheory.eLpNorm'_norm_rpow (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_norm_rpow
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(p q : ℝ)
(hq_pos : 0 < q)
:
MeasureTheory.eLpNorm' (fun (x : α) => ‖f x‖ ^ q) p μ = MeasureTheory.eLpNorm' f (p * q) μ ^ q
Alias of MeasureTheory.eLpNorm'_norm_rpow.
theorem
MeasureTheory.eLpNorm_norm_rpow
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hq_pos : 0 < q)
:
MeasureTheory.eLpNorm (fun (x : α) => ‖f x‖ ^ q) p μ = MeasureTheory.eLpNorm f (p * ENNReal.ofReal q) μ ^ q
@[deprecated MeasureTheory.eLpNorm_norm_rpow (since := "2024-07-27")]
theorem
MeasureTheory.snorm_norm_rpow
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hq_pos : 0 < q)
:
MeasureTheory.eLpNorm (fun (x : α) => ‖f x‖ ^ q) p μ = MeasureTheory.eLpNorm f (p * ENNReal.ofReal q) μ ^ q
Alias of MeasureTheory.eLpNorm_norm_rpow.
theorem
MeasureTheory.eLpNorm_congr_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : f =ᵐ[μ] g)
:
MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_congr_ae (since := "2024-07-27")]
theorem
MeasureTheory.snorm_congr_ae
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : f =ᵐ[μ] g)
:
MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_congr_ae.
theorem
MeasureTheory.memℒp_congr_ae
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f g : α → E}
(hfg : f =ᵐ[μ] g)
:
MeasureTheory.Memℒp f p μ ↔ MeasureTheory.Memℒp g p μ
theorem
MeasureTheory.Memℒp.ae_eq
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f g : α → E}
(hfg : f =ᵐ[μ] g)
(hf_Lp : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.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}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hg : MeasureTheory.Memℒp g p μ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.Memℒp f p μ
theorem
MeasureTheory.Memℒp.mono
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hg : MeasureTheory.Memℒp g p μ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.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}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → ℝ}
(hg : MeasureTheory.Memℒp g p μ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a)
:
MeasureTheory.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}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
MeasureTheory.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}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
MeasureTheory.Memℒp f p μ ↔ MeasureTheory.Memℒp g p μ
theorem
MeasureTheory.memℒp_top_of_bound
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(C : ℝ)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
MeasureTheory.Memℒp f ⊤ μ
theorem
MeasureTheory.Memℒp.of_bound
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(C : ℝ)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
MeasureTheory.Memℒp f p μ
theorem
MeasureTheory.memℒp_of_bounded
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{a b : ℝ}
{f : α → ℝ}
(h : ∀ᵐ (x : α) ∂μ, f x ∈ Set.Icc a b)
(hX : MeasureTheory.AEStronglyMeasurable f μ)
(p : ENNReal)
:
MeasureTheory.Memℒp f p μ
theorem
MeasureTheory.eLpNorm'_mono_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ ν : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν ≤ μ)
(hq : 0 ≤ q)
:
MeasureTheory.eLpNorm' f q ν ≤ MeasureTheory.eLpNorm' f q μ
@[deprecated MeasureTheory.eLpNorm'_mono_measure (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_mono_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ ν : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν ≤ μ)
(hq : 0 ≤ q)
:
MeasureTheory.eLpNorm' f q ν ≤ MeasureTheory.eLpNorm' f q μ
Alias of MeasureTheory.eLpNorm'_mono_measure.
theorem
MeasureTheory.eLpNormEssSup_mono_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν.AbsolutelyContinuous μ)
:
@[deprecated MeasureTheory.eLpNormEssSup_mono_measure (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_mono_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν.AbsolutelyContinuous μ)
:
Alias of MeasureTheory.eLpNormEssSup_mono_measure.
theorem
MeasureTheory.eLpNorm_mono_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν ≤ μ)
:
MeasureTheory.eLpNorm f p ν ≤ MeasureTheory.eLpNorm f p μ
@[deprecated MeasureTheory.eLpNorm_mono_measure (since := "2024-07-27")]
theorem
MeasureTheory.snorm_mono_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν ≤ μ)
:
MeasureTheory.eLpNorm f p ν ≤ MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_mono_measure.
theorem
MeasureTheory.Memℒp.mono_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hμν : ν ≤ μ)
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp f p ν
theorem
MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
:
MeasureTheory.eLpNorm (s.indicator f) p μ = MeasureTheory.eLpNorm f p (μ.restrict s)
@[deprecated MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict (since := "2024-07-27")]
theorem
MeasureTheory.snorm_indicator_eq_restrict
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
:
MeasureTheory.eLpNorm (s.indicator f) p μ = MeasureTheory.eLpNorm f p (μ.restrict s)
Alias of MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict.
@[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}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
:
MeasureTheory.eLpNorm (s.indicator f) p μ = MeasureTheory.eLpNorm f p (μ.restrict 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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
:
MeasureTheory.eLpNormEssSup (s.indicator f) μ = MeasureTheory.eLpNormEssSup f (μ.restrict s)
theorem
MeasureTheory.eLpNorm_restrict_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(p : ENNReal)
(μ : MeasureTheory.Measure α)
(s : Set α)
:
MeasureTheory.eLpNorm f p (μ.restrict s) ≤ MeasureTheory.eLpNorm f p μ
@[deprecated MeasureTheory.eLpNorm_restrict_le (since := "2024-07-27")]
theorem
MeasureTheory.snorm_restrict_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(p : ENNReal)
(μ : MeasureTheory.Measure α)
(s : Set α)
:
MeasureTheory.eLpNorm f p (μ.restrict s) ≤ MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_restrict_le.
theorem
MeasureTheory.eLpNorm_indicator_le
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f : α → E)
:
MeasureTheory.eLpNorm (s.indicator f) p μ ≤ MeasureTheory.eLpNorm f p μ
theorem
MeasureTheory.eLpNormEssSup_indicator_le
{α : Type u_1}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
(s : Set α)
(f : α → G)
:
MeasureTheory.eLpNormEssSup (s.indicator f) μ ≤ MeasureTheory.eLpNormEssSup f μ
theorem
MeasureTheory.eLpNormEssSup_indicator_const_le
{α : Type u_1}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
(s : Set α)
(c : G)
:
MeasureTheory.eLpNormEssSup (s.indicator fun (x : α) => c) μ ≤ ↑‖c‖₊
theorem
MeasureTheory.eLpNormEssSup_indicator_const_eq
{α : Type u_1}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
(s : Set α)
(c : G)
(hμs : μ s ≠ 0)
:
MeasureTheory.eLpNormEssSup (s.indicator fun (x : α) => c) μ = ↑‖c‖₊
theorem
MeasureTheory.eLpNorm_indicator_const₀
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{c : F}
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(hp : p ≠ 0)
(hp_top : p ≠ ⊤)
:
theorem
MeasureTheory.eLpNorm_indicator_const
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.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}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{c : F}
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ 0)
(hp : p ≠ 0)
:
theorem
MeasureTheory.eLpNorm_indicator_const_le
{α : Type u_1}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
{s : Set α}
(c : G)
(p : ENNReal)
:
theorem
MeasureTheory.Memℒp.indicator
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (s.indicator f) p μ
theorem
MeasureTheory.memℒp_indicator_iff_restrict
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
:
MeasureTheory.Memℒp (s.indicator f) p μ ↔ MeasureTheory.Memℒp f p (μ.restrict s)
theorem
MeasureTheory.memℒp_indicator_const
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(p : ENNReal)
(hs : MeasurableSet s)
(c : E)
(hμsc : c = 0 ∨ μ s ≠ ⊤)
:
MeasureTheory.Memℒp (s.indicator fun (x : α) => c) p μ
theorem
MeasureTheory.eLpNormEssSup_piecewise
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f g : α → E)
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
MeasureTheory.eLpNormEssSup (s.piecewise f g) μ = MeasureTheory.eLpNormEssSup f (μ.restrict s) ⊔ MeasureTheory.eLpNormEssSup g (μ.restrict sᶜ)
theorem
MeasureTheory.eLpNorm_top_piecewise
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f g : α → E)
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
MeasureTheory.eLpNorm (s.piecewise f g) ⊤ μ = MeasureTheory.eLpNorm f ⊤ (μ.restrict s) ⊔ MeasureTheory.eLpNorm g ⊤ (μ.restrict sᶜ)
theorem
MeasureTheory.Memℒp.piecewise
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
[DecidablePred fun (x : α) => x ∈ s]
{g : α → F}
(hs : MeasurableSet s)
(hf : MeasureTheory.Memℒp f p (μ.restrict s))
(hg : MeasureTheory.Memℒp g p (μ.restrict sᶜ))
:
MeasureTheory.Memℒp (s.piecewise f g) p μ
theorem
MeasureTheory.eLpNorm_restrict_eq_of_support_subset
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{s : Set α}
{f : α → F}
(hsf : Function.support f ⊆ s)
:
MeasureTheory.eLpNorm f p (μ.restrict s) = MeasureTheory.eLpNorm f p μ
For a function f with support in s, the Lᵖ norms of f with respect to μ and
μ.restrict s are the same.
@[deprecated MeasureTheory.eLpNorm_restrict_eq_of_support_subset (since := "2024-07-27")]
theorem
MeasureTheory.snorm_restrict_eq_of_support_subset
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{s : Set α}
{f : α → F}
(hsf : Function.support f ⊆ s)
:
MeasureTheory.eLpNorm f p (μ.restrict s) = MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_restrict_eq_of_support_subset.
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}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(s : Set α)
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp f p (μ.restrict s)
theorem
MeasureTheory.eLpNorm'_smul_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ℝ}
(hp : 0 ≤ p)
{f : α → F}
(c : ENNReal)
:
MeasureTheory.eLpNorm' f p (c • μ) = c ^ (1 / p) * MeasureTheory.eLpNorm' f p μ
@[deprecated MeasureTheory.eLpNorm'_smul_measure (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_smul_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ℝ}
(hp : 0 ≤ p)
{f : α → F}
(c : ENNReal)
:
MeasureTheory.eLpNorm' f p (c • μ) = c ^ (1 / p) * MeasureTheory.eLpNorm' f p μ
Alias of MeasureTheory.eLpNorm'_smul_measure.
@[simp]
theorem
MeasureTheory.eLpNormEssSup_smul_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.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)
:
MeasureTheory.eLpNormEssSup f (c • μ) = MeasureTheory.eLpNormEssSup f μ
@[deprecated MeasureTheory.eLpNormEssSup_smul_measure (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_smul_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.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)
:
MeasureTheory.eLpNormEssSup f (c • μ) = MeasureTheory.eLpNormEssSup f μ
Alias of MeasureTheory.eLpNormEssSup_smul_measure.
@[deprecated _private.Mathlib.MeasureTheory.Function.LpSeminorm.Basic.0.MeasureTheory.eLpNorm_smul_measure_of_ne_zero_of_ne_top (since := "2024-07-27")]
theorem
MeasureTheory.snorm_smul_measure_of_ne_zero_of_ne_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ENNReal}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{f : α → F}
(c : ENNReal)
:
MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
Use eLpNorm_smul_measure_of_ne_top instead.
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)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
See eLpNorm_smul_measure_of_ne_zero' for a version with scalar multiplication by ℝ≥0.
@[deprecated MeasureTheory.eLpNorm_smul_measure_of_ne_zero (since := "2024-07-27")]
theorem
MeasureTheory.snorm_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)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_smul_measure_of_ne_zero.
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)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • MeasureTheory.eLpNorm f p μ
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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ENNReal}
(hp_ne_top : p ≠ ⊤)
(f : α → F)
(c : ENNReal)
:
MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
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}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp : p ≠ ⊤)
(c : NNReal)
(f : α → F)
:
MeasureTheory.eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • MeasureTheory.eLpNorm f p μ
See eLpNorm_smul_measure_of_ne_top' for a version with scalar multiplication by ℝ≥0∞.
@[deprecated MeasureTheory.eLpNorm_smul_measure_of_ne_top (since := "2024-07-27")]
theorem
MeasureTheory.snorm_smul_measure_of_ne_top
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ENNReal}
(hp_ne_top : p ≠ ⊤)
(f : α → F)
(c : ENNReal)
:
MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_smul_measure_of_ne_top.
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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(c : ENNReal)
:
MeasureTheory.eLpNorm f 1 (c • μ) = c * MeasureTheory.eLpNorm f 1 μ
@[deprecated MeasureTheory.eLpNorm_one_smul_measure (since := "2024-07-27")]
theorem
MeasureTheory.snorm_one_smul_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(c : ENNReal)
:
MeasureTheory.eLpNorm f 1 (c • μ) = c * MeasureTheory.eLpNorm f 1 μ
Alias of MeasureTheory.eLpNorm_one_smul_measure.
theorem
MeasureTheory.Memℒp.of_measure_le_smul
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{μ' : MeasureTheory.Measure α}
(c : ENNReal)
(hc : c ≠ ⊤)
(hμ'_le : μ' ≤ c • μ)
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp f p μ'
theorem
MeasureTheory.Memℒp.smul_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{c : ENNReal}
(hf : MeasureTheory.Memℒp f p μ)
(hc : c ≠ ⊤)
:
MeasureTheory.Memℒp f p (c • μ)
theorem
MeasureTheory.eLpNorm_one_add_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ ν : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm f 1 (μ + ν) = MeasureTheory.eLpNorm f 1 μ + MeasureTheory.eLpNorm f 1 ν
@[deprecated MeasureTheory.eLpNorm_one_add_measure (since := "2024-07-27")]
theorem
MeasureTheory.snorm_one_add_measure
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ ν : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm f 1 (μ + ν) = MeasureTheory.eLpNorm f 1 μ + MeasureTheory.eLpNorm f 1 ν
Alias of MeasureTheory.eLpNorm_one_add_measure.
theorem
MeasureTheory.eLpNorm_le_add_measure_right
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ ν : MeasureTheory.Measure α)
{p : ENNReal}
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f p (μ + ν)
@[deprecated MeasureTheory.eLpNorm_le_add_measure_right (since := "2024-07-27")]
theorem
MeasureTheory.snorm_le_add_measure_right
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ ν : MeasureTheory.Measure α)
{p : ENNReal}
:
MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f p (μ + ν)
theorem
MeasureTheory.eLpNorm_le_add_measure_left
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ ν : MeasureTheory.Measure α)
{p : ENNReal}
:
MeasureTheory.eLpNorm f p ν ≤ MeasureTheory.eLpNorm f p (μ + ν)
@[deprecated MeasureTheory.eLpNorm_le_add_measure_left (since := "2024-07-27")]
theorem
MeasureTheory.snorm_le_add_measure_left
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ ν : MeasureTheory.Measure α)
{p : ENNReal}
:
MeasureTheory.eLpNorm f p ν ≤ MeasureTheory.eLpNorm f p (μ + ν)
theorem
MeasureTheory.eLpNormEssSup_eq_iSup
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hμ : ∀ (a : α), μ {a} ≠ 0)
(f : α → E)
:
MeasureTheory.eLpNormEssSup f μ = ⨆ (a : α), ↑‖f a‖₊
@[simp]
theorem
MeasureTheory.eLpNormEssSup_count
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
[MeasurableSingletonClass α]
(f : α → E)
:
MeasureTheory.eLpNormEssSup f MeasureTheory.Measure.count = ⨆ (a : α), ↑‖f a‖₊
theorem
MeasureTheory.Memℒp.left_of_add_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(h : MeasureTheory.Memℒp f p (μ + ν))
:
MeasureTheory.Memℒp f p μ
theorem
MeasureTheory.Memℒp.right_of_add_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(h : MeasureTheory.Memℒp f p (μ + ν))
:
MeasureTheory.Memℒp f p ν
theorem
MeasureTheory.Memℒp.norm
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(h : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (fun (x : α) => ‖f x‖) p μ
theorem
MeasureTheory.memℒp_norm_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.Memℒp (fun (x : α) => ‖f x‖) p μ ↔ MeasureTheory.Memℒp f p μ
theorem
MeasureTheory.eLpNorm'_eq_zero_of_ae_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
(hf_zero : f =ᵐ[μ] 0)
:
MeasureTheory.eLpNorm' f q μ = 0
@[deprecated MeasureTheory.eLpNorm'_eq_zero_of_ae_zero (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_eq_zero_of_ae_zero
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
(hf_zero : f =ᵐ[μ] 0)
:
MeasureTheory.eLpNorm' f q μ = 0
theorem
MeasureTheory.eLpNorm'_eq_zero_of_ae_zero'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hq0_ne : q ≠ 0)
(hμ : μ ≠ 0)
{f : α → F}
(hf_zero : f =ᵐ[μ] 0)
:
MeasureTheory.eLpNorm' f q μ = 0
@[deprecated MeasureTheory.eLpNorm'_eq_zero_of_ae_zero' (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_eq_zero_of_ae_zero'
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hq0_ne : q ≠ 0)
(hμ : μ ≠ 0)
{f : α → F}
(hf_zero : f =ᵐ[μ] 0)
:
MeasureTheory.eLpNorm' f q μ = 0
theorem
MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hq0 : 0 ≤ q)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h : MeasureTheory.eLpNorm' f q μ = 0)
:
@[deprecated MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero (since := "2024-07-27")]
theorem
MeasureTheory.ae_eq_zero_of_snorm'_eq_zero
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hq0 : 0 ≤ q)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h : MeasureTheory.eLpNorm' f q μ = 0)
:
theorem
MeasureTheory.eLpNorm'_eq_zero_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hq0_lt : 0 < q)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.eLpNorm' f q μ = 0 ↔ f =ᵐ[μ] 0
@[deprecated MeasureTheory.eLpNorm'_eq_zero_iff (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_eq_zero_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hq0_lt : 0 < q)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.eLpNorm' f q μ = 0 ↔ f =ᵐ[μ] 0
Alias of MeasureTheory.eLpNorm'_eq_zero_iff.
theorem
MeasureTheory.coe_nnnorm_ae_le_eLpNormEssSup
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
{x✝ : MeasurableSpace α}
(f : α → F)
(μ : MeasureTheory.Measure α)
:
∀ᵐ (x : α) ∂μ, ↑‖f x‖₊ ≤ MeasureTheory.eLpNormEssSup f μ
@[deprecated MeasureTheory.coe_nnnorm_ae_le_eLpNormEssSup (since := "2024-07-27")]
theorem
MeasureTheory.coe_nnnorm_ae_le_snormEssSup
{α : Type u_1}
{F : Type u_4}
[NormedAddCommGroup F]
{x✝ : MeasurableSpace α}
(f : α → F)
(μ : MeasureTheory.Measure α)
:
∀ᵐ (x : α) ∂μ, ↑‖f x‖₊ ≤ MeasureTheory.eLpNormEssSup f μ
@[simp]
theorem
MeasureTheory.eLpNormEssSup_eq_zero_iff
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNormEssSup f μ = 0 ↔ f =ᵐ[μ] 0
@[deprecated MeasureTheory.eLpNormEssSup_eq_zero_iff (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_eq_zero_iff
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNormEssSup f μ = 0 ↔ f =ᵐ[μ] 0
Alias of MeasureTheory.eLpNormEssSup_eq_zero_iff.
theorem
MeasureTheory.eLpNorm_eq_zero_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h0 : p ≠ 0)
:
MeasureTheory.eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0
@[deprecated MeasureTheory.eLpNorm_eq_zero_iff (since := "2024-07-27")]
theorem
MeasureTheory.snorm_eq_zero_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h0 : p ≠ 0)
:
MeasureTheory.eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0
Alias of MeasureTheory.eLpNorm_eq_zero_iff.
theorem
MeasureTheory.eLpNorm_eq_zero_of_ae_zero
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : f =ᵐ[μ] 0)
:
MeasureTheory.eLpNorm f p μ = 0
theorem
MeasureTheory.ae_le_eLpNormEssSup
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
∀ᵐ (y : α) ∂μ, ↑‖f y‖₊ ≤ MeasureTheory.eLpNormEssSup f μ
@[deprecated MeasureTheory.ae_le_eLpNormEssSup (since := "2024-07-27")]
theorem
MeasureTheory.ae_le_snormEssSup
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
∀ᵐ (y : α) ∂μ, ↑‖f y‖₊ ≤ MeasureTheory.eLpNormEssSup f μ
Alias of MeasureTheory.ae_le_eLpNormEssSup.
theorem
MeasureTheory.eLpNormEssSup_lt_top_iff_isBoundedUnder
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.eLpNormEssSup f μ < ⊤ ↔ Filter.IsBoundedUnder (fun (x1 x2 : NNReal) => x1 ≤ x2) (MeasureTheory.ae μ) fun (x : α) => ‖f x‖₊
theorem
MeasureTheory.meas_eLpNormEssSup_lt
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
μ {y : α | MeasureTheory.eLpNormEssSup f μ < ↑‖f y‖₊} = 0
@[deprecated MeasureTheory.meas_eLpNormEssSup_lt (since := "2024-07-27")]
theorem
MeasureTheory.meas_snormEssSup_lt
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
μ {y : α | MeasureTheory.eLpNormEssSup f μ < ↑‖f y‖₊} = 0
Alias of MeasureTheory.meas_eLpNormEssSup_lt.
theorem
MeasureTheory.eLpNorm_lt_top_of_finite
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
[Finite α]
[MeasureTheory.IsFiniteMeasure μ]
:
MeasureTheory.eLpNorm f p μ < ⊤
@[simp]
theorem
MeasureTheory.Memℒp.of_discrete
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
[DiscreteMeasurableSpace α]
[Finite α]
[MeasureTheory.IsFiniteMeasure μ]
:
MeasureTheory.Memℒp f p μ
@[simp]
theorem
MeasureTheory.eLpNorm_of_isEmpty
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[IsEmpty α]
(f : α → E)
(p : ENNReal)
:
MeasureTheory.eLpNorm f p μ = 0
@[deprecated MeasureTheory.eLpNormEssSup_piecewise (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_piecewise
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f g : α → E)
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
MeasureTheory.eLpNormEssSup (s.piecewise f g) μ = MeasureTheory.eLpNormEssSup f (μ.restrict s) ⊔ MeasureTheory.eLpNormEssSup g (μ.restrict sᶜ)
Alias of MeasureTheory.eLpNormEssSup_piecewise.
@[deprecated MeasureTheory.eLpNorm_top_piecewise (since := "2024-07-27")]
theorem
MeasureTheory.snorm_top_piecewise
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f g : α → E)
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
MeasureTheory.eLpNorm (s.piecewise f g) ⊤ μ = MeasureTheory.eLpNorm f ⊤ (μ.restrict s) ⊔ MeasureTheory.eLpNorm g ⊤ (μ.restrict sᶜ)
Alias of MeasureTheory.eLpNorm_top_piecewise.
theorem
MeasureTheory.eLpNormEssSup_map_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f μ)
:
@[deprecated MeasureTheory.eLpNormEssSup_map_measure (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_map_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f μ)
:
Alias of MeasureTheory.eLpNormEssSup_map_measure.
theorem
MeasureTheory.eLpNorm_map_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f μ)
:
MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ
@[deprecated MeasureTheory.eLpNorm_map_measure (since := "2024-07-27")]
theorem
MeasureTheory.snorm_map_measure
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f μ)
:
MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ
Alias of MeasureTheory.eLpNorm_map_measure.
theorem
MeasureTheory.memℒp_map_measure_iff
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f μ)
:
MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Memℒp (g ∘ f) p μ
theorem
MeasureTheory.Memℒp.comp_of_map
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f μ)
:
MeasureTheory.Memℒp (g ∘ f) p μ
theorem
MeasureTheory.eLpNorm_comp_measurePreserving
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
{ν : MeasureTheory.Measure β}
(hg : MeasureTheory.AEStronglyMeasurable g ν)
(hf : MeasureTheory.MeasurePreserving f μ ν)
:
MeasureTheory.eLpNorm (g ∘ f) p μ = MeasureTheory.eLpNorm g p ν
@[deprecated MeasureTheory.eLpNorm_comp_measurePreserving (since := "2024-07-27")]
theorem
MeasureTheory.snorm_comp_measurePreserving
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
{ν : MeasureTheory.Measure β}
(hg : MeasureTheory.AEStronglyMeasurable g ν)
(hf : MeasureTheory.MeasurePreserving f μ ν)
:
MeasureTheory.eLpNorm (g ∘ f) p μ = MeasureTheory.eLpNorm g p ν
theorem
MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{ν : MeasureTheory.Measure β}
(g : β →ₘ[ν] E)
(hf : MeasureTheory.MeasurePreserving f μ ν)
:
MeasureTheory.eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = MeasureTheory.eLpNorm (↑g) p ν
@[deprecated MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving (since := "2024-07-27")]
theorem
MeasureTheory.AEEqFun.snorm_compMeasurePreserving
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{ν : MeasureTheory.Measure β}
(g : β →ₘ[ν] E)
(hf : MeasureTheory.MeasurePreserving f μ ν)
:
MeasureTheory.eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = MeasureTheory.eLpNorm (↑g) p ν
Alias of MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving.
theorem
MeasureTheory.Memℒp.comp_measurePreserving
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
{ν : MeasureTheory.Measure β}
(hg : MeasureTheory.Memℒp g p ν)
(hf : MeasureTheory.MeasurePreserving f μ ν)
:
MeasureTheory.Memℒp (g ∘ f) p μ
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)
:
@[deprecated MeasurableEmbedding.eLpNormEssSup_map_measure (since := "2024-07-27")]
theorem
MeasurableEmbedding.snormEssSup_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)
:
MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ
@[deprecated MeasurableEmbedding.eLpNorm_map_measure (since := "2024-07-27")]
theorem
MeasurableEmbedding.snorm_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)
:
MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ
Alias of MeasurableEmbedding.eLpNorm_map_measure.
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)
:
MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Memℒp (g ∘ f) p μ
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}
:
MeasureTheory.Memℒp g p (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.Memℒp (g ∘ ⇑f) p μ
theorem
MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
{p : ℝ}
(hp : 0 < p)
:
MeasureTheory.eLpNorm' f p μ ≤ c • MeasureTheory.eLpNorm' g p μ
@[deprecated MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_le_nnreal_smul_snorm'_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
{p : ℝ}
(hp : 0 < p)
:
MeasureTheory.eLpNorm' f p μ ≤ c • MeasureTheory.eLpNorm' g p μ
Alias of MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul.
theorem
MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
:
@[deprecated MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_le_nnreal_smul_snormEssSup_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
:
Alias of MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul.
theorem
MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
(p : ENNReal)
:
MeasureTheory.eLpNorm f p μ ≤ c • MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (since := "2024-07-27")]
theorem
MeasureTheory.snorm_le_nnreal_smul_snorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
(p : ENNReal)
:
MeasureTheory.eLpNorm f p μ ≤ c • MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul.
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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(hc : c < 0)
(p : ENNReal)
:
MeasureTheory.eLpNorm f p μ = 0 ∧ MeasureTheory.eLpNorm g p μ = 0
When c is negative, ‖f x‖ ≤ c * ‖g x‖ is nonsense and forces both f and g to have an
eLpNorm of 0.
@[deprecated MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg (since := "2024-07-27")]
theorem
MeasureTheory.snorm_eq_zero_and_zero_of_ae_le_mul_neg
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(hc : c < 0)
(p : ENNReal)
:
MeasureTheory.eLpNorm f p μ = 0 ∧ MeasureTheory.eLpNorm g p μ = 0
Alias of MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg.
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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(p : ENNReal)
:
MeasureTheory.eLpNorm f p μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul (since := "2024-07-27")]
theorem
MeasureTheory.snorm_le_mul_snorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_4}
{G : Type u_5}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(p : ENNReal)
:
MeasureTheory.eLpNorm f p μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm g p μ
theorem
MeasureTheory.Memℒp.of_nnnorm_le_mul
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
{c : NNReal}
(hg : MeasureTheory.Memℒp g p μ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
:
MeasureTheory.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}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
{c : ℝ}
(hg : MeasureTheory.Memℒp g p μ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
:
MeasureTheory.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 : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
(hq : 0 < q)
:
MeasureTheory.eLpNorm' (c • f) q μ ≤ ‖c‖₊ • MeasureTheory.eLpNorm' f q μ
@[deprecated MeasureTheory.eLpNorm'_const_smul_le (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_const_smul_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
(hq : 0 < q)
:
MeasureTheory.eLpNorm' (c • f) q μ ≤ ‖c‖₊ • MeasureTheory.eLpNorm' f q μ
Alias of MeasureTheory.eLpNorm'_const_smul_le.
theorem
MeasureTheory.eLpNormEssSup_const_smul_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
:
MeasureTheory.eLpNormEssSup (c • f) μ ≤ ‖c‖₊ • MeasureTheory.eLpNormEssSup f μ
@[deprecated MeasureTheory.eLpNormEssSup_const_smul_le (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_const_smul_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
:
MeasureTheory.eLpNormEssSup (c • f) μ ≤ ‖c‖₊ • MeasureTheory.eLpNormEssSup f μ
theorem
MeasureTheory.eLpNorm_const_smul_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
:
MeasureTheory.eLpNorm (c • f) p μ ≤ ‖c‖₊ • MeasureTheory.eLpNorm f p μ
@[deprecated MeasureTheory.eLpNorm_const_smul_le (since := "2024-07-27")]
theorem
MeasureTheory.snorm_const_smul_le
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
:
MeasureTheory.eLpNorm (c • f) p μ ≤ ‖c‖₊ • MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_const_smul_le.
theorem
MeasureTheory.Memℒp.const_smul
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
{f : α → F}
(hf : MeasureTheory.Memℒp f p μ)
(c : 𝕜)
:
MeasureTheory.Memℒp (c • f) p μ
theorem
MeasureTheory.Memℒp.const_mul
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{f : α → 𝕜}
(hf : MeasureTheory.Memℒp f p μ)
(c : 𝕜)
:
MeasureTheory.Memℒp (fun (x : α) => c * f x) p μ
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 : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[BoundedSMul 𝕜 F]
{f : α → F}
(c : 𝕜)
(hq_pos : 0 < q)
:
MeasureTheory.eLpNorm' (c • f) q μ = ‖c‖₊ • MeasureTheory.eLpNorm' f q μ
@[deprecated MeasureTheory.eLpNorm'_const_smul (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_const_smul
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[BoundedSMul 𝕜 F]
{f : α → F}
(c : 𝕜)
(hq_pos : 0 < q)
:
MeasureTheory.eLpNorm' (c • f) q μ = ‖c‖₊ • MeasureTheory.eLpNorm' f q μ
Alias of MeasureTheory.eLpNorm'_const_smul.
theorem
MeasureTheory.eLpNormEssSup_const_smul
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[BoundedSMul 𝕜 F]
(c : 𝕜)
(f : α → F)
:
MeasureTheory.eLpNormEssSup (c • f) μ = ↑‖c‖₊ * MeasureTheory.eLpNormEssSup f μ
@[deprecated MeasureTheory.eLpNormEssSup_const_smul (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_const_smul
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_6}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[BoundedSMul 𝕜 F]
(c : 𝕜)
(f : α → F)
:
MeasureTheory.eLpNormEssSup (c • f) μ = ↑‖c‖₊ * MeasureTheory.eLpNormEssSup f μ
Alias of MeasureTheory.eLpNormEssSup_const_smul.
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)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm (c • f) p μ = ↑‖c‖₊ * MeasureTheory.eLpNorm f p μ
@[deprecated MeasureTheory.eLpNorm_const_smul (since := "2024-07-27")]
theorem
MeasureTheory.snorm_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)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm (c • f) p μ = ↑‖c‖₊ * MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_const_smul.
theorem
MeasureTheory.eLpNorm_nsmul
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(n : ℕ)
(f : α → F)
:
MeasureTheory.eLpNorm (n • f) p μ = ↑n * MeasureTheory.eLpNorm f p μ
theorem
MeasureTheory.le_eLpNorm_of_bddBelow
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp : p ≠ 0)
(hp' : p ≠ ⊤)
{f : α → F}
(C : NNReal)
{s : Set α}
(hs : MeasurableSet s)
(hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊)
:
C • μ s ^ (1 / p.toReal) ≤ MeasureTheory.eLpNorm f p μ
@[deprecated MeasureTheory.le_eLpNorm_of_bddBelow (since := "2024-07-27")]
theorem
MeasureTheory.le_snorm_of_bddBelow
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp : p ≠ 0)
(hp' : p ≠ ⊤)
{f : α → F}
(C : NNReal)
{s : Set α}
(hs : MeasurableSet s)
(hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊)
:
C • μ s ^ (1 / p.toReal) ≤ MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.le_eLpNorm_of_bddBelow.
@[deprecated MeasureTheory.le_snorm_of_bddBelow (since := "2024-06-26")]
theorem
MeasureTheory.snorm_indicator_ge_of_bdd_below
{α : Type u_1}
{F : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp : p ≠ 0)
(hp' : p ≠ ⊤)
{f : α → F}
(C : NNReal)
{s : Set α}
(hs : MeasurableSet s)
(hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊)
:
C • μ s ^ (1 / p.toReal) ≤ MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.le_eLpNorm_of_bddBelow.
Alias of MeasureTheory.le_eLpNorm_of_bddBelow.
@[simp]
theorem
MeasureTheory.eLpNorm_conj
{α : Type u_1}
{m0 : MeasurableSpace α}
{𝕜 : Type u_6}
[RCLike 𝕜]
(f : α → 𝕜)
(p : ENNReal)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.eLpNorm ((starRingEnd (α → 𝕜)) f) p μ = MeasureTheory.eLpNorm f p μ
theorem
MeasureTheory.Memℒp.re
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_6}
[RCLike 𝕜]
{f : α → 𝕜}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (fun (x : α) => RCLike.re (f x)) p μ
theorem
MeasureTheory.Memℒp.im
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_6}
[RCLike 𝕜]
{f : α → 𝕜}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (fun (x : α) => RCLike.im (f x)) p μ
theorem
MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{R : NNReal}
{p : ENNReal}
{f : ℕ → α → E}
(hfmeas : ∀ (n : ℕ), Measurable (f n))
(hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R)
:
∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ℕ) => ↑‖f n x‖₊ ^ p.toReal) Filter.atTop < ⊤
@[deprecated MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd (since := "2024-07-27")]
theorem
MeasureTheory.ae_bdd_liminf_atTop_rpow_of_snorm_bdd
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{R : NNReal}
{p : ENNReal}
{f : ℕ → α → E}
(hfmeas : ∀ (n : ℕ), Measurable (f n))
(hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R)
:
∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ℕ) => ↑‖f n x‖₊ ^ p.toReal) Filter.atTop < ⊤
Alias of MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd.
theorem
MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{R : NNReal}
{p : ENNReal}
(hp : p ≠ 0)
{f : ℕ → α → E}
(hfmeas : ∀ (n : ℕ), Measurable (f n))
(hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R)
:
∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ℕ) => ↑‖f n x‖₊) Filter.atTop < ⊤
@[deprecated MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd (since := "2024-07-27")]
theorem
MeasureTheory.ae_bdd_liminf_atTop_of_snorm_bdd
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{R : NNReal}
{p : ENNReal}
(hp : p ≠ 0)
{f : ℕ → α → E}
(hfmeas : ∀ (n : ℕ), Measurable (f n))
(hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R)
:
∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ℕ) => ↑‖f n x‖₊) Filter.atTop < ⊤
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}
{μ : MeasureTheory.Measure α}
{β : Type u_6}
[NormedAddCommGroup β]
(hp_top : p ≠ ⊤)
{f : α → β}
(hf : MeasureTheory.Memℒp f p μ)
{ε : ENNReal}
(hε : ε ≠ 0)
:
∃ (s : Set α), MeasurableSet s ∧ μ s < ⊤ ∧ MeasureTheory.eLpNorm (sᶜ.indicator f) p μ < ε
A single function that is Memℒp f p μ is tight with respect to μ.
@[deprecated MeasureTheory.Memℒp.exists_eLpNorm_indicator_compl_lt (since := "2024-07-27")]
theorem
MeasureTheory.Memℒp.exists_snorm_indicator_compl_lt
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{β : Type u_6}
[NormedAddCommGroup β]
(hp_top : p ≠ ⊤)
{f : α → β}
(hf : MeasureTheory.Memℒp f p μ)
{ε : ENNReal}
(hε : ε ≠ 0)
:
∃ (s : Set α), MeasurableSet s ∧ μ s < ⊤ ∧ MeasureTheory.eLpNorm (sᶜ.indicator f) p μ < ε
Alias of MeasureTheory.Memℒp.exists_eLpNorm_indicator_compl_lt.
A single function that is Memℒp f p μ is tight with respect to μ.