ℒ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 p.toReal μ
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 p.toReal μ
theorem
MeasureTheory.snorm_nnreal_eq_snorm'
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{p : NNReal}
(hp : p ≠ 0)
:
MeasureTheory.snorm f (↑p) μ = MeasureTheory.snorm' f (↑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}
:
theorem
MeasureTheory.snorm_nnreal_eq_lintegral
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{p : NNReal}
(hp : p ≠ 0)
:
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.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.snorm_nnreal_pow_eq_lintegral
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
{p : NNReal}
(hp : p ≠ 0)
:
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 ≠ ⊤)
:
@[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
@[simp]
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]
:
MeasureTheory.Memℒp 0 p μ
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)
:
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 ≠ ⊤)
:
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 =ᵐ[μ] 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 =ᵐ[μ] 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 ^ p.toReal⁻¹
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 ^ p.toReal⁻¹ * 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 (s.indicator f - t.indicator f) p μ = MeasureTheory.snorm ((symmDiff s t).indicator 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 =ᵐ[μ] 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 =ᵐ[μ] 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 =ᵐ[μ] 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_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‖)
:
MeasureTheory.Memℒp f p μ
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‖)
:
MeasureTheory.Memℒp f p μ
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)
:
MeasureTheory.Memℒp f p μ
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‖)
:
MeasureTheory.Memℒp g p μ
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)
:
MeasureTheory.Memℒp f ⊤ μ
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)
:
MeasureTheory.Memℒp f p μ
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μν : ν.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 μ)
:
MeasureTheory.Memℒp f p ν
theorem
MeasureTheory.snorm_restrict_le
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(p : ENNReal)
(μ : MeasureTheory.Measure α)
(s : Set α)
:
MeasureTheory.snorm f p (μ.restrict s) ≤ MeasureTheory.snorm f p μ
theorem
MeasureTheory.snorm_restrict_eq_of_support_subset
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{s : Set α}
{f : α → F}
(hsf : Function.support f ⊆ s)
:
MeasureTheory.snorm f p (μ.restrict s) = MeasureTheory.snorm f p μ
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_2}
{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.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 ^ (1 / p).toReal • 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 ^ (1 / p).toReal • 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 μ)
:
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 ≠ ⊤)
:
MeasureTheory.Memℒp f p (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 (μ + ν))
:
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 (μ + ν))
:
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 =ᵐ[μ] 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 =ᵐ[μ] 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 =ᵐ[μ] 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 =ᵐ[μ] 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 =ᵐ[μ] 0
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_piecewise
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f : α → E)
(g : α → E)
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
MeasureTheory.snormEssSup (s.piecewise f g) μ = max (MeasureTheory.snormEssSup f (μ.restrict s)) (MeasureTheory.snormEssSup g (μ.restrict sᶜ))
theorem
MeasureTheory.snorm_top_piecewise
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f : α → E)
(g : α → E)
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
MeasureTheory.snorm (s.piecewise f g) ⊤ μ = max (MeasureTheory.snorm f ⊤ (μ.restrict s)) (MeasureTheory.snorm g ⊤ (μ.restrict sᶜ))
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.Measure.map f μ) ↔ 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 (MeasureTheory.Measure.map f μ))
(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 (↑(g.compMeasurePreserving 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.Measure.map f μ) ↔ 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.Measure.map (⇑f) μ) ↔ MeasureTheory.Memℒp (g ∘ ⇑f) 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‖₊)
:
MeasureTheory.Memℒp f p μ
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‖)
:
MeasureTheory.Memℒp f p μ
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 μ
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.le_snorm_of_bddBelow
{α : 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 ≤ ‖f x‖₊)
:
C • μ s ^ (1 / p.toReal) ≤ MeasureTheory.snorm f p μ
@[deprecated MeasureTheory.le_snorm_of_bddBelow]
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 ≤ ‖f x‖₊)
:
C • μ s ^ (1 / p.toReal) ≤ MeasureTheory.snorm f p μ
Alias of MeasureTheory.le_snorm_of_bddBelow.
theorem
MeasureTheory.Memℒp.re
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[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_5}
[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_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)
:
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)
:
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)
:
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.