ℒp space #
This file describes properties of almost everywhere strongly measurable functions with finite
p-seminorm, denoted by snorm f p μ and defined for p:ℝ≥0∞ as 0 if p=0,
(∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and 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 #
-
snorm' f p μ:(∫ ‖f a‖^p ∂μ) ^ (1/p)forf : α → Fandp : ℝ, whereαis a measurable space andFis a normed group. -
snormEssSup f μ: seminorm inℒ∞, equal to the essential supremumess_sup ‖f‖ μ. -
snorm f p μ: forp : ℝ≥0∞, seminorm inℒp, equal to0forp=0, tosnorm' f p μfor0 < p < ∞and tosnormEssSup f μforp = ∞. -
Memℒp f p μ: property that the functionfis almost everywhere strongly measurable and has finitep-seminorm for the measureμ(snorm f p μ < ∞)
ℒp seminorm #
We define the ℒp seminorm, denoted by snorm f p μ. For real p, it is given by an integral
formula (for which we use the notation snorm' f p μ), and for p = ∞ it is the essential
supremum (for which we use the notation snormEssSup f μ).
We also define a predicate Memℒp f p μ, requesting that a function is almost everywhere
measurable and has finite snorm f p μ.
This paragraph is devoted to the basic properties of these definitions. It is constructed as
follows: for a given property, we prove it for snorm' and snormEssSup when it makes sense,
deduce it for snorm, and translate it in terms of Memℒp.
def
MeasureTheory.snorm'
{α : Type u_1}
{F : Type u_3}
[NormedAddCommGroup F]
:
{x : MeasurableSpace α} → (α → F) → ℝ → MeasureTheory.Measure α → ENNReal
(∫ ‖f a‖^q ∂μ) ^ (1/q), which is a seminorm on the space of measurable functions for which
this quantity is finite
Instances For
def
MeasureTheory.snormEssSup
{α : Type u_1}
{F : Type u_3}
[NormedAddCommGroup F]
:
{x : MeasurableSpace α} → (α → F) → MeasureTheory.Measure α → ENNReal
seminorm for ℒ∞, equal to the essential supremum of ‖f‖.
Equations
- MeasureTheory.snormEssSup f μ = essSup (fun x => ↑‖f x‖₊) μ
Instances For
def
MeasureTheory.snorm
{α : Type u_1}
{F : Type u_3}
[NormedAddCommGroup F]
:
{x : MeasurableSpace α} → (α → F) → ENNReal → MeasureTheory.Measure α → ENNReal
ℒ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.snorm f p μ = if p = 0 then 0 else if p = ⊤ then MeasureTheory.snormEssSup f μ else MeasureTheory.snorm' f (ENNReal.toReal p) μ
Instances For
theorem
MeasureTheory.snorm_eq_snorm'
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{f : α → F}
:
MeasureTheory.snorm f p μ = MeasureTheory.snorm' f (ENNReal.toReal p) μ
theorem
MeasureTheory.snorm_eq_lintegral_rpow_nnnorm
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{f : α → F}
:
MeasureTheory.snorm f p μ = (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
theorem
MeasureTheory.snorm_one_eq_lintegral_nnnorm
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.snorm f 1 μ = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
@[simp]
theorem
MeasureTheory.snorm_exponent_top
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
def
MeasureTheory.Memℒp
{E : Type u_2}
[NormedAddCommGroup E]
{α : Type u_5}
:
{x : MeasurableSpace α} → (α → E) → ENNReal → autoParam (MeasureTheory.Measure α) _auto✝ → Prop
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.snorm f p μ < ⊤)
Instances For
theorem
MeasureTheory.memℒp_def
{E : Type u_2}
[NormedAddCommGroup E]
{α : Type u_5}
:
∀ {x : MeasurableSpace α} (f : α → E) (p : ENNReal) (μ : MeasureTheory.Measure α),
MeasureTheory.Memℒp f p ↔ MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.snorm f p μ < ⊤
theorem
MeasureTheory.Memℒp.aestronglyMeasurable
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{p : ENNReal}
(h : MeasureTheory.Memℒp f p)
:
theorem
MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_snorm'
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
:
theorem
MeasureTheory.Memℒp.snorm_lt_top
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hfp : MeasureTheory.Memℒp f p)
:
MeasureTheory.snorm f p μ < ⊤
theorem
MeasureTheory.Memℒp.snorm_ne_top
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hfp : MeasureTheory.Memℒp f p)
:
MeasureTheory.snorm f p μ ≠ ⊤
theorem
MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
(hfq : MeasureTheory.snorm' f q μ < ⊤)
:
theorem
MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hfp : MeasureTheory.snorm f p μ < ⊤)
:
theorem
MeasureTheory.snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
MeasureTheory.snorm f p μ < ⊤ ↔ ∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ < ⊤
@[simp]
theorem
MeasureTheory.snorm'_exponent_zero
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.snorm' f 0 μ = 1
@[simp]
theorem
MeasureTheory.snorm_exponent_zero
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.snorm f 0 μ = 0
theorem
MeasureTheory.memℒp_zero_iff_aestronglyMeasurable
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
:
@[simp]
theorem
MeasureTheory.snorm'_zero
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hp0_lt : 0 < q)
:
MeasureTheory.snorm' 0 q μ = 0
@[simp]
theorem
MeasureTheory.snorm'_zero'
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hq0_ne : q ≠ 0)
(hμ : μ ≠ 0)
:
MeasureTheory.snorm' 0 q μ = 0
@[simp]
theorem
MeasureTheory.snormEssSup_zero
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
:
MeasureTheory.snormEssSup 0 μ = 0
@[simp]
theorem
MeasureTheory.snorm_zero
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
:
MeasureTheory.snorm 0 p μ = 0
@[simp]
theorem
MeasureTheory.snorm_zero'
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
:
MeasureTheory.snorm (fun x => 0) p μ = 0
theorem
MeasureTheory.zero_memℒp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
theorem
MeasureTheory.zero_mem_ℒp'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
MeasureTheory.Memℒp (fun x => 0) p
theorem
MeasureTheory.snorm'_measure_zero_of_pos
{α : Type u_1}
{F : Type u_3}
{q : ℝ}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
(hq_pos : 0 < q)
:
MeasureTheory.snorm' f q 0 = 0
theorem
MeasureTheory.snorm'_measure_zero_of_exponent_zero
{α : Type u_1}
{F : Type u_3}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
MeasureTheory.snorm' f 0 0 = 1
theorem
MeasureTheory.snorm'_measure_zero_of_neg
{α : Type u_1}
{F : Type u_3}
{q : ℝ}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
(hq_neg : q < 0)
:
MeasureTheory.snorm' f q 0 = ⊤
@[simp]
theorem
MeasureTheory.snormEssSup_measure_zero
{α : Type u_1}
{F : Type u_3}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
MeasureTheory.snormEssSup f 0 = 0
@[simp]
theorem
MeasureTheory.snorm_measure_zero
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
[MeasurableSpace α]
{f : α → F}
:
MeasureTheory.snorm f p 0 = 0
@[simp]
theorem
MeasureTheory.snorm'_neg
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.snorm' (-f) q μ = MeasureTheory.snorm' f q μ
@[simp]
theorem
MeasureTheory.snorm_neg
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.snorm (-f) p μ = MeasureTheory.snorm f p μ
theorem
MeasureTheory.Memℒp.neg
{α : Type u_1}
{E : Type u_2}
{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_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
:
MeasureTheory.Memℒp (-f) p ↔ MeasureTheory.Memℒp f p
theorem
MeasureTheory.snorm'_const
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(hq_pos : 0 < q)
:
theorem
MeasureTheory.snorm'_const'
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[MeasureTheory.IsFiniteMeasure μ]
(c : F)
(hc_ne_zero : c ≠ 0)
(hq_ne_zero : q ≠ 0)
:
theorem
MeasureTheory.snormEssSup_const
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(hμ : μ ≠ 0)
:
MeasureTheory.snormEssSup (fun x => c) μ = ↑‖c‖₊
theorem
MeasureTheory.snorm'_const_of_isProbabilityMeasure
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(hq_pos : 0 < q)
[MeasureTheory.IsProbabilityMeasure μ]
:
MeasureTheory.snorm' (fun x => c) q μ = ↑‖c‖₊
theorem
MeasureTheory.snorm_const
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(h0 : p ≠ 0)
(hμ : μ ≠ 0)
:
MeasureTheory.snorm (fun x => c) p μ = ↑‖c‖₊ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p)
theorem
MeasureTheory.snorm_const'
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(c : F)
(h0 : p ≠ 0)
(h_top : p ≠ ⊤)
:
MeasureTheory.snorm (fun x => c) p μ = ↑‖c‖₊ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p)
theorem
MeasureTheory.snorm_const_lt_top_iff
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ENNReal}
{c : F}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
theorem
MeasureTheory.memℒp_const
{α : Type u_1}
{E : Type u_2}
{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_2}
{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_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{c : E}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
theorem
MeasureTheory.snorm'_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hq : 0 ≤ q)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
MeasureTheory.snorm' f q μ ≤ MeasureTheory.snorm' g q μ
theorem
MeasureTheory.snorm'_mono_ae
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hq : 0 ≤ q)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.snorm' f q μ ≤ MeasureTheory.snorm' g q μ
theorem
MeasureTheory.snorm'_congr_nnnorm_ae
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊)
:
MeasureTheory.snorm' f q μ = MeasureTheory.snorm' g q μ
theorem
MeasureTheory.snorm'_congr_norm_ae
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖)
:
MeasureTheory.snorm' f q μ = MeasureTheory.snorm' g q μ
theorem
MeasureTheory.snorm'_congr_ae
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → F}
(hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g)
:
MeasureTheory.snorm' f q μ = MeasureTheory.snorm' g q μ
theorem
MeasureTheory.snormEssSup_congr_ae
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → F}
(hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g)
:
theorem
MeasureTheory.snormEssSup_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
theorem
MeasureTheory.snorm_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_mono_ae
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_mono_ae_real
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x)
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_mono_nnnorm
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ (x : α), ‖f x‖₊ ≤ ‖g x‖₊)
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_mono
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ (x : α), ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_mono_real
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → ℝ}
(h : ∀ (x : α), ‖f x‖ ≤ g x)
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm g p μ
theorem
MeasureTheory.snormEssSup_le_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
MeasureTheory.snormEssSup f μ ≤ ↑C
theorem
MeasureTheory.snormEssSup_le_of_ae_bound
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
theorem
MeasureTheory.snormEssSup_lt_top_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
theorem
MeasureTheory.snormEssSup_lt_top_of_ae_bound
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
theorem
MeasureTheory.snorm_le_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
MeasureTheory.snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
theorem
MeasureTheory.snorm_le_of_ae_bound
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
MeasureTheory.snorm f p μ ≤ ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹ * ENNReal.ofReal C
theorem
MeasureTheory.snorm_congr_nnnorm_ae
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊)
:
MeasureTheory.snorm f p μ = MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_congr_norm_ae
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖)
:
MeasureTheory.snorm f p μ = MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_indicator_sub_indicator
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(s : Set α)
(t : Set α)
(f : α → E)
:
MeasureTheory.snorm (Set.indicator s f - Set.indicator t f) p μ = MeasureTheory.snorm (Set.indicator (s ∆ t) f) p μ
@[simp]
theorem
MeasureTheory.snorm'_norm
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.snorm' (fun a => ‖f a‖) q μ = MeasureTheory.snorm' f q μ
@[simp]
theorem
MeasureTheory.snorm_norm
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
:
MeasureTheory.snorm (fun x => ‖f x‖) p μ = MeasureTheory.snorm f p μ
theorem
MeasureTheory.snorm'_norm_rpow
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(p : ℝ)
(q : ℝ)
(hq_pos : 0 < q)
:
MeasureTheory.snorm' (fun x => ‖f x‖ ^ q) p μ = MeasureTheory.snorm' f (p * q) μ ^ q
theorem
MeasureTheory.snorm_norm_rpow
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hq_pos : 0 < q)
:
MeasureTheory.snorm (fun x => ‖f x‖ ^ q) p μ = MeasureTheory.snorm f (p * ENNReal.ofReal q) μ ^ q
theorem
MeasureTheory.snorm_congr_ae
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → F}
(hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g)
:
MeasureTheory.snorm f p μ = MeasureTheory.snorm g p μ
theorem
MeasureTheory.memℒp_congr_ae
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g)
:
MeasureTheory.Memℒp f p ↔ MeasureTheory.Memℒp g p
theorem
MeasureTheory.Memℒp.ae_eq
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g)
(hf_Lp : MeasureTheory.Memℒp f p)
:
theorem
MeasureTheory.Memℒp.of_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{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‖)
:
theorem
MeasureTheory.Memℒp.mono
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{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‖)
:
Alias of MeasureTheory.Memℒp.of_le.
theorem
MeasureTheory.Memℒp.mono'
{α : Type u_1}
{E : Type u_2}
{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)
:
theorem
MeasureTheory.Memℒp.congr_norm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{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‖)
:
theorem
MeasureTheory.memℒp_congr_norm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{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_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(C : ℝ)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
theorem
MeasureTheory.Memℒp.of_bound
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(C : ℝ)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
theorem
MeasureTheory.snorm'_mono_measure
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν ≤ μ)
(hq : 0 ≤ q)
:
MeasureTheory.snorm' f q ν ≤ MeasureTheory.snorm' f q μ
theorem
MeasureTheory.snormEssSup_mono_measure
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : MeasureTheory.Measure.AbsolutelyContinuous ν μ)
:
theorem
MeasureTheory.snorm_mono_measure
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hμν : ν ≤ μ)
:
MeasureTheory.snorm f p ν ≤ MeasureTheory.snorm f p μ
theorem
MeasureTheory.Memℒp.mono_measure
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hμν : ν ≤ μ)
(hf : MeasureTheory.Memℒp f p)
:
theorem
MeasureTheory.Memℒp.restrict
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(s : Set α)
{f : α → E}
(hf : MeasureTheory.Memℒp f p)
:
theorem
MeasureTheory.snorm'_smul_measure
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ℝ}
(hp : 0 ≤ p)
{f : α → F}
(c : ENNReal)
:
MeasureTheory.snorm' f p (c • μ) = c ^ (1 / p) * MeasureTheory.snorm' f p μ
theorem
MeasureTheory.snormEssSup_smul_measure
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{c : ENNReal}
(hc : c ≠ 0)
:
MeasureTheory.snormEssSup f (c • μ) = MeasureTheory.snormEssSup f μ
theorem
MeasureTheory.snorm_smul_measure_of_ne_zero
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ENNReal}
{f : α → F}
{c : ENNReal}
(hc : c ≠ 0)
:
MeasureTheory.snorm f p (c • μ) = c ^ ENNReal.toReal (1 / p) • MeasureTheory.snorm f p μ
theorem
MeasureTheory.snorm_smul_measure_of_ne_top
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{p : ENNReal}
(hp_ne_top : p ≠ ⊤)
{f : α → F}
(c : ENNReal)
:
MeasureTheory.snorm f p (c • μ) = c ^ ENNReal.toReal (1 / p) • MeasureTheory.snorm f p μ
theorem
MeasureTheory.snorm_one_smul_measure
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(c : ENNReal)
:
MeasureTheory.snorm f 1 (c • μ) = c * MeasureTheory.snorm f 1 μ
theorem
MeasureTheory.Memℒp.of_measure_le_smul
{α : Type u_1}
{E : Type u_2}
{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)
:
theorem
MeasureTheory.Memℒp.smul_measure
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{c : ENNReal}
(hf : MeasureTheory.Memℒp f p)
(hc : c ≠ ⊤)
:
theorem
MeasureTheory.snorm_one_add_measure
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
:
MeasureTheory.snorm f 1 (μ + ν) = MeasureTheory.snorm f 1 μ + MeasureTheory.snorm f 1 ν
theorem
MeasureTheory.snorm_le_add_measure_right
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
{p : ENNReal}
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm f p (μ + ν)
theorem
MeasureTheory.snorm_le_add_measure_left
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
{p : ENNReal}
:
MeasureTheory.snorm f p ν ≤ MeasureTheory.snorm f p (μ + ν)
theorem
MeasureTheory.Memℒp.left_of_add_measure
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(h : MeasureTheory.Memℒp f p)
:
theorem
MeasureTheory.Memℒp.right_of_add_measure
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(h : MeasureTheory.Memℒp f p)
:
theorem
MeasureTheory.Memℒp.norm
{α : Type u_1}
{E : Type u_2}
{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_2}
{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.snorm'_eq_zero_of_ae_zero
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hq0_lt : 0 < q)
(hf_zero : f =ᶠ[MeasureTheory.Measure.ae μ] 0)
:
MeasureTheory.snorm' f q μ = 0
theorem
MeasureTheory.snorm'_eq_zero_of_ae_zero'
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hq0_ne : q ≠ 0)
(hμ : μ ≠ 0)
{f : α → F}
(hf_zero : f =ᶠ[MeasureTheory.Measure.ae μ] 0)
:
MeasureTheory.snorm' f q μ = 0
theorem
MeasureTheory.ae_eq_zero_of_snorm'_eq_zero
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hq0 : 0 ≤ q)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h : MeasureTheory.snorm' f q μ = 0)
:
theorem
MeasureTheory.snorm'_eq_zero_iff
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hq0_lt : 0 < q)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.snorm' f q μ = 0 ↔ f =ᶠ[MeasureTheory.Measure.ae μ] 0
theorem
MeasureTheory.coe_nnnorm_ae_le_snormEssSup
{α : Type u_1}
{F : Type u_3}
[NormedAddCommGroup F]
:
∀ {x : MeasurableSpace α} (f : α → F) (μ : MeasureTheory.Measure α),
∀ᵐ (x_1 : α) ∂μ, ↑‖f x_1‖₊ ≤ MeasureTheory.snormEssSup f μ
@[simp]
theorem
MeasureTheory.snormEssSup_eq_zero_iff
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
MeasureTheory.snormEssSup f μ = 0 ↔ f =ᶠ[MeasureTheory.Measure.ae μ] 0
theorem
MeasureTheory.snorm_eq_zero_iff
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h0 : p ≠ 0)
:
MeasureTheory.snorm f p μ = 0 ↔ f =ᶠ[MeasureTheory.Measure.ae μ] 0
theorem
MeasureTheory.snorm'_add_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hq1 : 1 ≤ q)
:
MeasureTheory.snorm' (f + g) q μ ≤ MeasureTheory.snorm' f q μ + MeasureTheory.snorm' g q μ
theorem
MeasureTheory.snorm'_add_le_of_le_one
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hq0 : 0 ≤ q)
(hq1 : q ≤ 1)
:
MeasureTheory.snorm' (f + g) q μ ≤ 2 ^ (1 / q - 1) * (MeasureTheory.snorm' f q μ + MeasureTheory.snorm' g q μ)
theorem
MeasureTheory.snormEssSup_add_le
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → F}
:
MeasureTheory.snormEssSup (f + g) μ ≤ MeasureTheory.snormEssSup f μ + MeasureTheory.snormEssSup g μ
theorem
MeasureTheory.snorm_add_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hp1 : 1 ≤ p)
:
MeasureTheory.snorm (f + g) p μ ≤ MeasureTheory.snorm f p μ + MeasureTheory.snorm g p μ
A constant for the inequality ‖f + g‖_{L^p} ≤ C * (‖f‖_{L^p} + ‖g‖_{L^p}). It is equal to 1
for p ≥ 1 or p = 0, and 2^(1/p-1) in the more tricky interval (0, 1).
Equations
- MeasureTheory.LpAddConst p = if p ∈ Set.Ioo 0 1 then 2 ^ (1 / ENNReal.toReal p - 1) else 1
Instances For
theorem
MeasureTheory.snorm_add_le'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(p : ENNReal)
:
MeasureTheory.snorm (f + g) p μ ≤ MeasureTheory.LpAddConst p * (MeasureTheory.snorm f p μ + MeasureTheory.snorm g p μ)
theorem
MeasureTheory.exists_Lp_half
{α : Type u_1}
(E : Type u_2)
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
(p : ENNReal)
{δ : ENNReal}
(hδ : δ ≠ 0)
:
∃ η,
0 < η ∧ ∀ (f g : α → E),
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ →
MeasureTheory.snorm f p μ ≤ η → MeasureTheory.snorm g p μ ≤ η → MeasureTheory.snorm (f + g) p μ < δ
Technical lemma to control the addition of functions in L^p even for p < 1: Given δ > 0,
there exists η such that two functions bounded by η in L^p have a sum bounded by δ. One
could take η = δ / 2 for p ≥ 1, but the point of the lemma is that it works also for p < 1.
theorem
MeasureTheory.snorm_sub_le'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(p : ENNReal)
:
MeasureTheory.snorm (f - g) p μ ≤ MeasureTheory.LpAddConst p * (MeasureTheory.snorm f p μ + MeasureTheory.snorm g p μ)
theorem
MeasureTheory.snorm_sub_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hp : 1 ≤ p)
:
MeasureTheory.snorm (f - g) p μ ≤ MeasureTheory.snorm f p μ + MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_add_lt_top
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Memℒp f p)
(hg : MeasureTheory.Memℒp g p)
:
MeasureTheory.snorm (f + g) p μ < ⊤
theorem
MeasureTheory.ae_le_snormEssSup
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
∀ᵐ (y : α) ∂μ, ↑‖f y‖₊ ≤ MeasureTheory.snormEssSup f μ
theorem
MeasureTheory.meas_snormEssSup_lt
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
↑↑μ {y | MeasureTheory.snormEssSup f μ < ↑‖f y‖₊} = 0
theorem
MeasureTheory.snormEssSup_map_measure
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f)
:
MeasureTheory.snormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.snormEssSup (g ∘ f) μ
theorem
MeasureTheory.snorm_map_measure
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f)
:
MeasureTheory.snorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.snorm (g ∘ f) p μ
theorem
MeasureTheory.memℒp_map_measure_iff
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f)
:
MeasureTheory.Memℒp g p ↔ MeasureTheory.Memℒp (g ∘ f) p
theorem
MeasureTheory.Memℒp.comp_of_map
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
(hg : MeasureTheory.Memℒp g p)
(hf : AEMeasurable f)
:
MeasureTheory.Memℒp (g ∘ f) p
theorem
MeasureTheory.snorm_comp_measurePreserving
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
{ν : MeasureTheory.Measure β}
(hg : MeasureTheory.AEStronglyMeasurable g ν)
(hf : MeasureTheory.MeasurePreserving f)
:
MeasureTheory.snorm (g ∘ f) p μ = MeasureTheory.snorm g p ν
theorem
MeasureTheory.AEEqFun.snorm_compMeasurePreserving
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
{mβ : MeasurableSpace β}
{f : α → β}
{ν : MeasureTheory.Measure β}
(g : β →ₘ[ν] E)
(hf : MeasureTheory.MeasurePreserving f)
:
MeasureTheory.snorm (↑(MeasureTheory.AEEqFun.compMeasurePreserving g f hf)) p μ = MeasureTheory.snorm (↑g) p ν
theorem
MeasureTheory.Memℒp.comp_measurePreserving
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
{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.snormEssSup_map_measure
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{β : Type u_5}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → F}
(hf : MeasurableEmbedding f)
:
MeasureTheory.snormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.snormEssSup (g ∘ f) μ
theorem
MeasurableEmbedding.snorm_map_measure
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{β : Type u_5}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → F}
(hf : MeasurableEmbedding f)
:
MeasureTheory.snorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.snorm (g ∘ f) p μ
theorem
MeasurableEmbedding.memℒp_map_measure_iff
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{β : Type u_5}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → F}
(hf : MeasurableEmbedding f)
:
MeasureTheory.Memℒp g p ↔ MeasureTheory.Memℒp (g ∘ f) p
theorem
MeasurableEquiv.memℒp_map_measure_iff
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{β : Type u_5}
{mβ : MeasurableSpace β}
(f : α ≃ᵐ β)
{g : β → F}
:
MeasureTheory.Memℒp g p ↔ MeasureTheory.Memℒp (g ∘ ↑f) p
theorem
MeasureTheory.snorm'_trim
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{q : ℝ}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.snorm' f q (MeasureTheory.Measure.trim ν hm) = MeasureTheory.snorm' f q ν
theorem
MeasureTheory.limsup_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{ν : MeasureTheory.Measure α}
(hm : m ≤ m0)
{f : α → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.essSup_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{ν : MeasureTheory.Measure α}
(hm : m ≤ m0)
{f : α → ENNReal}
(hf : Measurable f)
:
essSup f (MeasureTheory.Measure.trim ν hm) = essSup f ν
theorem
MeasureTheory.snormEssSup_trim
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
theorem
MeasureTheory.snorm_trim
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{p : ENNReal}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.snorm f p (MeasureTheory.Measure.trim ν hm) = MeasureTheory.snorm f p ν
theorem
MeasureTheory.snorm_trim_ae
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{p : ENNReal}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.trim ν hm))
:
MeasureTheory.snorm f p (MeasureTheory.Measure.trim ν hm) = MeasureTheory.snorm f p ν
theorem
MeasureTheory.memℒp_of_memℒp_trim
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{p : ENNReal}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.Memℒp f p)
:
theorem
MeasureTheory.snorm'_le_snorm'_mul_rpow_measure_univ
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p : ℝ}
{q : ℝ}
(hp0_lt : 0 < p)
(hpq : p ≤ q)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.snorm' f p μ ≤ MeasureTheory.snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
theorem
MeasureTheory.snorm'_le_snormEssSup_mul_rpow_measure_univ
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hq_pos : 0 < q)
{f : α → F}
:
MeasureTheory.snorm' f q μ ≤ MeasureTheory.snormEssSup f μ * ↑↑μ Set.univ ^ (1 / q)
theorem
MeasureTheory.snorm_le_snorm_mul_rpow_measure_univ
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{q : ENNReal}
(hpq : p ≤ q)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
theorem
MeasureTheory.snorm'_le_snorm'_of_exponent_le
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
{m : MeasurableSpace α}
{p : ℝ}
{q : ℝ}
(hp0_lt : 0 < p)
(hpq : p ≤ q)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure μ]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.snorm' f p μ ≤ MeasureTheory.snorm' f q μ
theorem
MeasureTheory.snorm'_le_snormEssSup
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(hq_pos : 0 < q)
{f : α → F}
[MeasureTheory.IsProbabilityMeasure μ]
:
MeasureTheory.snorm' f q μ ≤ MeasureTheory.snormEssSup f μ
theorem
MeasureTheory.snorm_le_snorm_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{q : ENNReal}
(hpq : p ≤ q)
[MeasureTheory.IsProbabilityMeasure μ]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm f q μ
theorem
MeasureTheory.snorm'_lt_top_of_snorm'_lt_top_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p : ℝ}
{q : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hfq_lt_top : MeasureTheory.snorm' f q μ < ⊤)
(hp_nonneg : 0 ≤ p)
(hpq : p ≤ q)
:
MeasureTheory.snorm' f p μ < ⊤
theorem
MeasureTheory.pow_mul_meas_ge_le_snorm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
{f : α → E}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(ε : ENNReal)
:
(ε * ↑↑μ {x | ε ≤ ↑‖f x‖₊ ^ ENNReal.toReal p}) ^ (1 / ENNReal.toReal p) ≤ MeasureTheory.snorm f p μ
theorem
MeasureTheory.mul_meas_ge_le_pow_snorm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
{f : α → E}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(ε : ENNReal)
:
ε * ↑↑μ {x | ε ≤ ↑‖f x‖₊ ^ ENNReal.toReal p} ≤ MeasureTheory.snorm f p μ ^ ENNReal.toReal p
theorem
MeasureTheory.mul_meas_ge_le_pow_snorm'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
{f : α → E}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(ε : ENNReal)
:
ε ^ ENNReal.toReal p * ↑↑μ {x | ε ≤ ↑‖f x‖₊} ≤ MeasureTheory.snorm f p μ ^ ENNReal.toReal p
A version of Markov's inequality using Lp-norms.
theorem
MeasureTheory.meas_ge_le_mul_pow_snorm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
{f : α → E}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{ε : ENNReal}
(hε : ε ≠ 0)
:
↑↑μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ ENNReal.toReal p * MeasureTheory.snorm f p μ ^ ENNReal.toReal p
theorem
MeasureTheory.Memℒp.memℒp_of_exponent_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{q : ENNReal}
[MeasureTheory.IsFiniteMeasure μ]
{f : α → E}
(hfq : MeasureTheory.Memℒp f q)
(hpq : p ≤ q)
:
theorem
MeasureTheory.snorm'_sum_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_5}
{f : ι → α → E}
{s : Finset ι}
(hfs : ∀ (i : ι), i ∈ s → MeasureTheory.AEStronglyMeasurable (f i) μ)
(hq1 : 1 ≤ q)
:
MeasureTheory.snorm' (Finset.sum s fun i => f i) q μ ≤ Finset.sum s fun i => MeasureTheory.snorm' (f i) q μ
theorem
MeasureTheory.snorm_sum_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_5}
{f : ι → α → E}
{s : Finset ι}
(hfs : ∀ (i : ι), i ∈ s → MeasureTheory.AEStronglyMeasurable (f i) μ)
(hp1 : 1 ≤ p)
:
MeasureTheory.snorm (Finset.sum s fun i => f i) p μ ≤ Finset.sum s fun i => MeasureTheory.snorm (f i) p μ
theorem
MeasureTheory.Memℒp.add
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Memℒp f p)
(hg : MeasureTheory.Memℒp g p)
:
MeasureTheory.Memℒp (f + g) p
theorem
MeasureTheory.Memℒp.sub
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Memℒp f p)
(hg : MeasureTheory.Memℒp g p)
:
MeasureTheory.Memℒp (f - g) p
theorem
MeasureTheory.memℒp_finset_sum
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_5}
(s : Finset ι)
{f : ι → α → E}
(hf : ∀ (i : ι), i ∈ s → MeasureTheory.Memℒp (f i) p)
:
MeasureTheory.Memℒp (fun a => Finset.sum s fun i => f i a) p
theorem
MeasureTheory.memℒp_finset_sum'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_5}
(s : Finset ι)
{f : ι → α → E}
(hf : ∀ (i : ι), i ∈ s → MeasureTheory.Memℒp (f i) p)
:
MeasureTheory.Memℒp (Finset.sum s fun i => f i) p
theorem
MeasureTheory.snorm'_le_nnreal_smul_snorm'_of_ae_le_mul
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{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.snorm' f p μ ≤ c • MeasureTheory.snorm' g p μ
theorem
MeasureTheory.snormEssSup_le_nnreal_smul_snormEssSup_of_ae_le_mul
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
:
MeasureTheory.snormEssSup f μ ≤ c • MeasureTheory.snormEssSup g μ
theorem
MeasureTheory.snorm_le_nnreal_smul_snorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
(p : ENNReal)
:
MeasureTheory.snorm f p μ ≤ c • MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_eq_zero_and_zero_of_ae_le_mul_neg
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{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.snorm f p μ = 0 ∧ MeasureTheory.snorm g p μ = 0
When c is negative, ‖f x‖ ≤ c * ‖g x‖ is nonsense and forces both f and g to have an
snorm of 0.
theorem
MeasureTheory.snorm_le_mul_snorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(p : ENNReal)
:
MeasureTheory.snorm f p μ ≤ ENNReal.ofReal c * MeasureTheory.snorm g p μ
theorem
MeasureTheory.Memℒp.of_nnnorm_le_mul
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{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‖₊)
:
theorem
MeasureTheory.Memℒp.of_le_mul
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{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‖)
:
theorem
MeasureTheory.snorm'_le_snorm'_mul_snorm'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{p : ℝ}
{q : ℝ}
{r : ℝ}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{g : α → F}
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(b : E → F → G)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊)
(hp0_lt : 0 < p)
(hpq : p < q)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.snorm' (fun x => b (f x) (g x)) p μ ≤ MeasureTheory.snorm' f q μ * MeasureTheory.snorm' g r μ
theorem
MeasureTheory.snorm_le_snorm_top_mul_snorm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
(p : ENNReal)
(f : α → E)
{g : α → F}
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(b : E → F → G)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊)
:
MeasureTheory.snorm (fun x => b (f x) (g x)) p μ ≤ MeasureTheory.snorm f ⊤ μ * MeasureTheory.snorm g p μ
theorem
MeasureTheory.snorm_le_snorm_mul_snorm_top
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
(p : ENNReal)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(g : α → F)
(b : E → F → G)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊)
:
MeasureTheory.snorm (fun x => b (f x) (g x)) p μ ≤ MeasureTheory.snorm f p μ * MeasureTheory.snorm g ⊤ μ
theorem
MeasureTheory.snorm_le_snorm_mul_snorm_of_nnnorm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{p : ENNReal}
{q : ENNReal}
{r : ENNReal}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{g : α → F}
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(b : E → F → G)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.snorm (fun x => b (f x) (g x)) p μ ≤ MeasureTheory.snorm f q μ * MeasureTheory.snorm g r μ
Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation
fun x => b (f x) (g x).
theorem
MeasureTheory.snorm_le_snorm_mul_snorm'_of_norm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{p : ENNReal}
{q : ENNReal}
{r : ENNReal}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{g : α → F}
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(b : E → F → G)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ‖f x‖ * ‖g x‖)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.snorm (fun x => b (f x) (g x)) p μ ≤ MeasureTheory.snorm f q μ * MeasureTheory.snorm g r μ
Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation
fun x => b (f x) (g x).
Bounded actions by normed rings #
In this section we show inequalities on the norm.
theorem
MeasureTheory.snorm'_const_smul_le
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
(c : 𝕜)
(f : α → F)
(hq_pos : 0 < q)
:
MeasureTheory.snorm' (c • f) q μ ≤ ‖c‖₊ • MeasureTheory.snorm' f q μ
theorem
MeasureTheory.snormEssSup_const_smul_le
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
(c : 𝕜)
(f : α → F)
:
MeasureTheory.snormEssSup (c • f) μ ≤ ‖c‖₊ • MeasureTheory.snormEssSup f μ
theorem
MeasureTheory.snorm_const_smul_le
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[BoundedSMul 𝕜 F]
(c : 𝕜)
(f : α → F)
:
MeasureTheory.snorm (c • f) p μ ≤ ‖c‖₊ • MeasureTheory.snorm f p μ
theorem
MeasureTheory.Memℒp.const_smul
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{f : α → E}
(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 α}
{R : Type u_6}
[NormedRing R]
{f : α → R}
(hf : MeasureTheory.Memℒp f p)
(c : R)
:
MeasureTheory.Memℒp (fun x => c * f x) p
theorem
MeasureTheory.snorm'_smul_le_mul_snorm'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p : ℝ}
{q : ℝ}
{r : ℝ}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{φ : α → 𝕜}
(hφ : MeasureTheory.AEStronglyMeasurable φ μ)
(hp0_lt : 0 < p)
(hpq : p < q)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.snorm' (φ • f) p μ ≤ MeasureTheory.snorm' φ q μ * MeasureTheory.snorm' f r μ
theorem
MeasureTheory.snorm_smul_le_snorm_top_mul_snorm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
(p : ENNReal)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(φ : α → 𝕜)
:
MeasureTheory.snorm (φ • f) p μ ≤ MeasureTheory.snorm φ ⊤ μ * MeasureTheory.snorm f p μ
theorem
MeasureTheory.snorm_smul_le_snorm_mul_snorm_top
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
(p : ENNReal)
(f : α → E)
{φ : α → 𝕜}
(hφ : MeasureTheory.AEStronglyMeasurable φ μ)
:
MeasureTheory.snorm (φ • f) p μ ≤ MeasureTheory.snorm φ p μ * MeasureTheory.snorm f ⊤ μ
theorem
MeasureTheory.snorm_smul_le_mul_snorm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p : ENNReal}
{q : ENNReal}
{r : ENNReal}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{φ : α → 𝕜}
(hφ : MeasureTheory.AEStronglyMeasurable φ μ)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.snorm (φ • f) p μ ≤ MeasureTheory.snorm φ q μ * MeasureTheory.snorm f r μ
Hölder's inequality, as an inequality on the ℒp seminorm of a scalar product φ • f.
theorem
MeasureTheory.Memℒp.smul
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p : ENNReal}
{q : ENNReal}
{r : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f r)
(hφ : MeasureTheory.Memℒp φ q)
(hpqr : 1 / p = 1 / q + 1 / r)
:
MeasureTheory.Memℒp (φ • f) p
theorem
MeasureTheory.Memℒp.smul_of_top_right
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f p)
(hφ : MeasureTheory.Memℒp φ ⊤)
:
MeasureTheory.Memℒp (φ • f) p
theorem
MeasureTheory.Memℒp.smul_of_top_left
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 E]
[BoundedSMul 𝕜 E]
{p : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MeasureTheory.Memℒp f ⊤)
(hφ : MeasureTheory.Memℒp φ p)
:
MeasureTheory.Memℒp (φ • f) p
Bounded actions by normed division rings #
The inequalities in the previous section are now tight.
theorem
MeasureTheory.snorm'_const_smul
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[BoundedSMul 𝕜 F]
{f : α → F}
(c : 𝕜)
(hq_pos : 0 < q)
:
MeasureTheory.snorm' (c • f) q μ = ‖c‖₊ • MeasureTheory.snorm' f q μ
theorem
MeasureTheory.snormEssSup_const_smul
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[BoundedSMul 𝕜 F]
(c : 𝕜)
(f : α → F)
:
MeasureTheory.snormEssSup (c • f) μ = ↑‖c‖₊ * MeasureTheory.snormEssSup f μ
theorem
MeasureTheory.snorm_const_smul
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[BoundedSMul 𝕜 F]
(c : 𝕜)
(f : α → F)
:
MeasureTheory.snorm (c • f) p μ = ↑‖c‖₊ * MeasureTheory.snorm f p μ
theorem
MeasureTheory.snorm_indicator_ge_of_bdd_below
{α : Type u_1}
{F : Type u_3}
{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 ≤ ‖Set.indicator s f x‖₊)
:
C • ↑↑μ s ^ (1 / ENNReal.toReal p) ≤ MeasureTheory.snorm (Set.indicator s f) p μ
theorem
MeasureTheory.Memℒp.re
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[IsROrC 𝕜]
{f : α → 𝕜}
(hf : MeasureTheory.Memℒp f p)
:
MeasureTheory.Memℒp (fun x => ↑IsROrC.re (f x)) p
theorem
MeasureTheory.Memℒp.im
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[IsROrC 𝕜]
{f : α → 𝕜}
(hf : MeasureTheory.Memℒp f p)
:
MeasureTheory.Memℒp (fun x => ↑IsROrC.im (f x)) p
theorem
MeasureTheory.ae_bdd_liminf_atTop_rpow_of_snorm_bdd
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{R : NNReal}
{p : ENNReal}
{f : ℕ → α → E}
(hfmeas : ∀ (n : ℕ), Measurable (f n))
(hbdd : ∀ (n : ℕ), MeasureTheory.snorm (f n) p μ ≤ ↑R)
:
∀ᵐ (x : α) ∂μ, Filter.liminf (fun n => ↑‖f n x‖₊ ^ ENNReal.toReal p) Filter.atTop < ⊤
theorem
MeasureTheory.ae_bdd_liminf_atTop_of_snorm_bdd
{α : Type u_1}
{E : Type u_2}
{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.snorm (f n) p μ ≤ ↑R)
:
∀ᵐ (x : α) ∂μ, Filter.liminf (fun n => ↑‖f n x‖₊) Filter.atTop < ⊤
theorem
Continuous.memℒp_top_of_hasCompactSupport
{E : Type u_2}
[NormedAddCommGroup E]
{X : Type u_5}
[TopologicalSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
{f : X → E}
(hf : Continuous f)
(h'f : HasCompactSupport f)
(μ : MeasureTheory.Measure X)
:
A continuous function with compact support belongs to L^∞.