Basic theorems about ℒp space #
theorem
MeasureTheory.MemLp.eLpNorm_lt_top
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ENorm ε]
[TopologicalSpace ε]
{f : α → ε}
(hfp : MemLp f p μ)
:
theorem
MeasureTheory.MemLp.eLpNorm_ne_top
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ENorm ε]
[TopologicalSpace ε]
{f : α → ε}
(hfp : MemLp f p μ)
:
@[simp]
theorem
MeasureTheory.eLpNorm'_exponent_zero
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
:
@[simp]
theorem
MeasureTheory.eLpNorm_exponent_zero
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
:
@[simp]
theorem
MeasureTheory.memLp_zero_iff_aestronglyMeasurable
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
[TopologicalSpace ε]
{f : α → ε}
:
@[simp]
theorem
MeasureTheory.eLpNorm'_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
(hp0_lt : 0 < q)
:
@[simp]
theorem
MeasureTheory.eLpNorm'_zero'
{α : Type u_1}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
(hq0_ne : q ≠ 0)
(hμ : μ ≠ 0)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
:
@[simp]
theorem
MeasureTheory.eLpNorm_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
:
@[simp]
theorem
MeasureTheory.eLpNorm_zero'
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
:
@[simp]
theorem
MeasureTheory.MemLp.zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
:
MemLp 0 p μ
@[simp]
theorem
MeasureTheory.MemLp.zero'
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
:
MemLp (fun (x : α) => 0) p μ
theorem
MeasureTheory.eLpNorm'_measure_zero_of_pos
{α : Type u_1}
{q : ℝ}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[MeasurableSpace α]
{f : α → ε}
(hq_pos : 0 < q)
:
theorem
MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero
{α : Type u_1}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[MeasurableSpace α]
{f : α → ε}
:
theorem
MeasureTheory.eLpNorm'_measure_zero_of_neg
{α : Type u_1}
{q : ℝ}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[MeasurableSpace α]
{f : α → ε}
(hq_neg : q < 0)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_measure_zero
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
{f : α → ε}
:
@[simp]
theorem
MeasureTheory.eLpNorm_measure_zero
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
[ENorm ε]
{f : α → ε}
:
@[simp]
theorem
MeasureTheory.memLp_measure_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
:
MemLp f p 0
@[simp]
theorem
MeasureTheory.eLpNorm'_neg
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(q : ℝ)
(μ : Measure α)
:
@[simp]
theorem
MeasureTheory.eLpNorm_neg
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
(f : α → F)
(p : ENNReal)
(μ : Measure α)
:
theorem
MeasureTheory.eLpNorm_sub_comm
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
(f g : α → E)
(p : ENNReal)
(μ : Measure α)
:
theorem
MeasureTheory.MemLp.neg
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MemLp f p μ)
:
theorem
MeasureTheory.memLp_neg_iff
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
:
theorem
MeasureTheory.eLpNorm'_const'
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
[IsFiniteMeasure μ]
(c : F)
(hc_ne_zero : c ≠ 0)
(hq_ne_zero : q ≠ 0)
:
theorem
MeasureTheory.eLpNormEssSup_const
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
(c : ε)
(hμ : μ ≠ 0)
:
theorem
MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[ENorm ε]
(c : ε)
(hq_pos : 0 < q)
[IsProbabilityMeasure μ]
:
theorem
MeasureTheory.eLpNorm_const_lt_top_iff_enorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε'' : Type u_8}
[TopologicalSpace ε'']
[ESeminormedAddMonoid ε'']
{c : ε''}
(hc' : ‖c‖ₑ ≠ ⊤)
{p : ENNReal}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
theorem
MeasureTheory.memLp_const_enorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε' : Type u_7}
[TopologicalSpace ε']
[ContinuousENorm ε']
{c : ε'}
(hc : ‖c‖ₑ ≠ ⊤)
[IsFiniteMeasure μ]
:
MemLp (fun (x : α) => c) p μ
theorem
MeasureTheory.memLp_const
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
(c : E)
[IsFiniteMeasure μ]
:
MemLp (fun (x : α) => c) p μ
theorem
MeasureTheory.memLp_top_const_enorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε' : Type u_7}
[TopologicalSpace ε']
[ContinuousENorm ε']
{c : ε'}
(hc : ‖c‖ₑ ≠ ⊤)
:
theorem
MeasureTheory.memLp_top_const
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
(c : E)
:
theorem
MeasureTheory.memLp_const_iff_enorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε'' : Type u_8}
[TopologicalSpace ε'']
[ESeminormedAddMonoid ε'']
{p : ENNReal}
{c : ε''}
(hc : ‖c‖ₑ ≠ ⊤)
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
theorem
MeasureTheory.eLpNormEssSup_congr_ae
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f g : α → ε}
(hfg : f =ᵐ[μ] g)
:
theorem
MeasureTheory.eLpNormEssSup_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_5}
{G : Type u_6}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
@[deprecated MeasureTheory.eLpNorm_mono_enorm_ae (since := "2026-06-24")]
theorem
MeasureTheory.eLpNorm_mono_ae'
{α : Type u_1}
{ε : Type u_2}
{ε' : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ENorm ε]
[ENorm ε']
{f : α → ε}
{g : α → ε'}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ)
:
Alias of MeasureTheory.eLpNorm_mono_enorm_ae.
theorem
MeasureTheory.eLpNorm_mono_nnnorm
{α : Type u_1}
{F : Type u_5}
{G : Type u_6}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ (x : α), ‖f x‖₊ ≤ ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm_mono
{α : Type u_1}
{F : Type u_5}
{G : Type u_6}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
(h : ∀ (x : α), ‖f x‖ ≤ ‖g x‖)
:
theorem
MeasureTheory.eLpNorm_mono_real
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{g : α → ℝ}
(h : ∀ (x : α), ‖f x‖ ≤ g x)
:
theorem
MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
theorem
MeasureTheory.eLpNormEssSup_le_of_ae_bound
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
theorem
MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C)
:
theorem
MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{C : ℝ}
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
@[simp]
theorem
MeasureTheory.eLpNorm'_norm
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
@[simp]
theorem
MeasureTheory.eLpNorm_norm
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
(f : α → F)
:
theorem
MeasureTheory.eLpNorm_ofReal
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
(f : α → ℝ)
(hf : ∀ᵐ (x : α) ∂μ, 0 ≤ f x)
:
f : α → ℝ and ENNReal.ofReal ∘ f : α → ℝ≥0∞ have the same eLpNorm.
Usually, you should not use this lemma (but use enorms everywhere.)
theorem
MeasureTheory.eLpNorm_norm_rpow
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
(f : α → F)
(hq_pos : 0 < q)
:
theorem
MeasureTheory.memLp_congr_ae
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ENorm ε]
[TopologicalSpace ε]
{f g : α → ε}
(hfg : f =ᵐ[μ] g)
:
theorem
MeasureTheory.MemLp.ae_eq
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ENorm ε]
[TopologicalSpace ε]
{f g : α → ε}
(hfg : f =ᵐ[μ] g)
(hf_Lp : MemLp f p μ)
:
MemLp g p μ
theorem
MeasureTheory.MemLp.of_le_enorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
{ε' : Type u_8}
[TopologicalSpace ε]
[TopologicalSpace ε']
[ContinuousENorm ε]
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.of_le
{α : Type u_1}
{E : Type u_4}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.mono
{α : Type u_1}
{E : Type u_4}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MemLp f p μ
Alias of MeasureTheory.MemLp.of_le.
theorem
MeasureTheory.MemLp.mono'_enorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
{g : α → ENNReal}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ g a)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.mono'
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → ℝ}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.congr_enorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
{ε' : Type u_8}
[TopologicalSpace ε]
[TopologicalSpace ε']
[ContinuousENorm ε]
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
(hf : MemLp f p μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ)
:
MemLp g p μ
theorem
MeasureTheory.MemLp.congr_norm
{α : Type u_1}
{E : Type u_4}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hf : MemLp f p μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
MemLp g p μ
theorem
MeasureTheory.memLp_congr_enorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
{ε' : Type u_8}
[TopologicalSpace ε]
[TopologicalSpace ε']
[ContinuousENorm ε]
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ)
:
theorem
MeasureTheory.memLp_congr_norm
{α : Type u_1}
{E : Type u_4}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
theorem
MeasureTheory.memLp_top_of_bound_enorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
(C : NNReal)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑C)
:
theorem
MeasureTheory.memLp_top_of_bound
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : AEStronglyMeasurable f μ)
(C : ℝ)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
theorem
MeasureTheory.MemLp.of_enorm_bound
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
[IsFiniteMeasure μ]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{C : ENNReal}
(hC : C ≠ ⊤)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.of_bound
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[IsFiniteMeasure μ]
{f : α → E}
(hf : AEStronglyMeasurable f μ)
(C : ℝ)
(hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C)
:
MemLp f p μ
theorem
MeasureTheory.memLp_of_bounded
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
{a b : ℝ}
{f : α → ℝ}
(h : ∀ᵐ (x : α) ∂μ, f x ∈ Set.Icc a b)
(hX : AEStronglyMeasurable f μ)
(p : ENNReal)
:
MemLp f p μ
theorem
MeasureTheory.eLpNorm'_mono_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ ν : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
(f : α → ε)
(hμν : ν ≤ μ)
(hq : 0 ≤ q)
:
theorem
MeasureTheory.eLpNormEssSup_mono_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
(f : α → ε)
(hμν : ν.AbsolutelyContinuous μ)
:
theorem
MeasureTheory.eLpNorm_mono_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
(f : α → ε)
(hμν : ν ≤ μ)
:
theorem
MeasureTheory.MemLp.mono_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hμν : ν ≤ μ)
(hf : MemLp f p μ)
:
MemLp f p ν
theorem
MeasureTheory.eLpNorm_restrict_eq_of_support_subset
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{s : Set α}
{f : α → ε}
(hsf : Function.support f ⊆ s)
:
For a function f with support in s, the Lᵖ norms of f with respect to μ and
μ.restrict s are the same.
theorem
MeasureTheory.MemLp.restrict
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
(s : Set α)
{f : α → ε}
(hf : MemLp f p μ)
:
theorem
MeasureTheory.eLpNorm'_smul_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{p : ℝ}
(hp : 0 ≤ p)
{f : α → ε}
(c : ENNReal)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_smul_measure
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{R : Type u_7}
[Semiring R]
[IsDomain R]
[Module R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[Module.IsTorsionFree R ENNReal]
{c : R}
(hc : c ≠ 0)
(f : α → ε)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_ennreal_smul_measure
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{c : ENNReal}
(hc : c ≠ 0)
(f : α → ε)
:
theorem
MeasureTheory.eLpNorm_smul_measure_of_ne_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{c : ENNReal}
(hc : c ≠ 0)
(f : α → ε)
(p : ENNReal)
(μ : Measure α)
:
See eLpNorm_smul_measure_of_ne_zero' for a version with scalar multiplication by ℝ≥0.
theorem
MeasureTheory.eLpNorm_smul_measure_of_ne_zero'
{α : Type u_1}
{m0 : MeasurableSpace α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{c : NNReal}
(hc : c ≠ 0)
(f : α → ε)
(p : ENNReal)
(μ : Measure α)
:
See eLpNorm_smul_measure_of_ne_zero for a version with scalar multiplication by ℝ≥0∞.
theorem
MeasureTheory.eLpNorm_smul_measure_of_ne_top
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{p : ENNReal}
(hp_ne_top : p ≠ ⊤)
(f : α → ε)
(c : ENNReal)
:
See eLpNorm_smul_measure_of_ne_top' for a version with scalar multiplication by ℝ≥0.
theorem
MeasureTheory.eLpNorm_smul_measure_of_ne_top'
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
(hp : p ≠ ⊤)
(c : NNReal)
(f : α → ε)
:
See eLpNorm_smul_measure_of_ne_top' for a version with scalar multiplication by ℝ≥0∞.
theorem
MeasureTheory.eLpNorm_one_smul_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(c : ENNReal)
:
theorem
MeasureTheory.MemLp.of_measure_le_smul
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{μ' : Measure α}
{c : ENNReal}
(hc : c ≠ ⊤)
(hμ'_le : μ' ≤ c • μ)
{f : α → ε}
(hf : MemLp f p μ)
:
MemLp f p μ'
theorem
MeasureTheory.MemLp.smul_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
{c : ENNReal}
(hf : MemLp f p μ)
(hc : c ≠ ⊤)
:
theorem
MeasureTheory.eLpNorm_le_add_measure_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
(f : α → ε)
(μ ν : Measure α)
{p : ENNReal}
:
theorem
MeasureTheory.eLpNorm_le_add_measure_left
{α : Type u_1}
{m0 : MeasurableSpace α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
(f : α → ε)
(μ ν : Measure α)
{p : ENNReal}
:
theorem
MeasureTheory.eLpNormEssSup_eq_iSup
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_8}
[ENorm ε]
(hμ : ∀ (a : α), μ {a} ≠ 0)
(f : α → ε)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_count
{α : Type u_1}
{m0 : MeasurableSpace α}
{ε : Type u_8}
[ENorm ε]
[MeasurableSingletonClass α]
(f : α → ε)
:
theorem
MeasureTheory.MemLp.left_of_add_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(h : MemLp f p (μ + ν))
:
MemLp f p μ
theorem
MeasureTheory.MemLp.right_of_add_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ ν : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(h : MemLp f p (μ + ν))
:
MemLp f p ν
theorem
MeasureTheory.MemLp.enorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(h : MemLp f p μ)
:
theorem
MeasureTheory.MemLp.norm
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(h : MemLp f p μ)
:
theorem
MeasureTheory.memLp_enorm_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.memLp_norm_iff
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm'_eq_zero_of_ae_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
(hq0_lt : 0 < q)
(hf_zero : f =ᵐ[μ] 0)
:
theorem
MeasureTheory.eLpNorm'_eq_zero_of_ae_zero'
{α : Type u_1}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
(hq0_ne : q ≠ 0)
(hμ : μ ≠ 0)
{f : α → ε}
(hf_zero : f =ᵐ[μ] 0)
:
theorem
MeasureTheory.eLpNorm_eq_zero_of_ae_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
(hf : f =ᵐ[μ] 0)
:
theorem
MeasureTheory.eLpNorm'_eq_zero_of_ae_eq_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
{p : ℝ}
(hp : 0 < p)
(hf : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0)
:
theorem
MeasureTheory.ae_le_eLpNormEssSup
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_8}
[ENorm ε]
{f : α → ε}
:
theorem
MeasureTheory.eLpNormEssSup_lt_top_iff_isBoundedUnder
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
:
eLpNormEssSup f μ < ⊤ ↔ Filter.IsBoundedUnder (fun (x1 x2 : NNReal) => x1 ≤ x2) (ae μ) fun (x : α) => ‖f x‖₊
theorem
MeasureTheory.eLpNorm_lt_top_of_finite
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
[Finite α]
[IsFiniteMeasure μ]
:
@[simp]
theorem
MeasureTheory.MemLp.of_discrete
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
[DiscreteMeasurableSpace α]
[Finite α]
[IsFiniteMeasure μ]
:
MemLp f p μ
@[simp]
theorem
MeasureTheory.eLpNorm_of_isEmpty
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[IsEmpty α]
(f : α → ε)
(p : ENNReal)
:
theorem
MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
(hq0 : 0 ≤ q)
(hf : AEStronglyMeasurable f μ)
(h : eLpNorm' f q μ = 0)
:
theorem
MeasureTheory.eLpNorm'_eq_zero_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
(hq0_lt : 0 < q)
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.enorm_ae_le_eLpNormEssSup
{α : Type u_1}
{ε : Type u_8}
[ENorm ε]
{x✝ : MeasurableSpace α}
(f : α → ε)
(μ : Measure α)
:
@[simp]
theorem
MeasureTheory.eLpNormEssSup_eq_zero_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
:
theorem
MeasureTheory.eLpNorm_eq_zero_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
(h0 : p ≠ 0)
:
theorem
MeasureTheory.eLpNormEssSup_map_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_8}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → ε}
(hg : AEStronglyMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm_map_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_8}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → ε}
(hg : AEStronglyMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.memLp_map_measure_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_8}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → ε}
(hg : AEStronglyMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.MemLp.comp_of_map
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_8}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → ε}
(hg : MemLp g p (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm_comp_measurePreserving
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_8}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → ε}
{ν : Measure β}
(hg : AEStronglyMeasurable g ν)
(hf : MeasurePreserving f μ ν)
:
theorem
MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_8}
{mβ : MeasurableSpace β}
{f : α → β}
{ν : Measure β}
(g : β →ₘ[ν] E)
(hf : MeasurePreserving f μ ν)
:
theorem
MeasureTheory.MemLp.comp_measurePreserving
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_8}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → ε}
{ν : Measure β}
(hg : MemLp g p ν)
(hf : MeasurePreserving f μ ν)
:
theorem
MeasurableEmbedding.eLpNormEssSup_map_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_8}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → ε}
(hf : MeasurableEmbedding f)
:
theorem
MeasurableEmbedding.eLpNorm_map_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_8}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → ε}
(hf : MeasurableEmbedding f)
:
theorem
MeasurableEmbedding.memLp_map_measure_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_8}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → ε}
(hf : MeasurableEmbedding f)
:
theorem
MeasurableEquiv.memLp_map_measure_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_8}
{mβ : MeasurableSpace β}
{g : β → ε}
(f : α ≃ᵐ β)
:
theorem
MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{R : NNReal}
{p : ENNReal}
{f : ℕ → α → E}
(hfmeas : ∀ (n : ℕ), Measurable (f n))
(hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R)
:
theorem
MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{R : NNReal}
{p : ENNReal}
(hp : p ≠ 0)
{f : ℕ → α → E}
(hfmeas : ∀ (n : ℕ), Measurable (f n))
(hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R)
:
∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ℕ) => ‖f n x‖ₑ) Filter.atTop < ⊤
theorem
Continuous.memLp_top_of_hasCompactSupport
{E : Type u_4}
[NormedAddCommGroup E]
{X : Type u_7}
[TopologicalSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
{f : X → E}
(hf : Continuous f)
(h'f : HasCompactSupport f)
(μ : MeasureTheory.Measure X)
:
MeasureTheory.MemLp f ⊤ μ
A continuous function with compact support belongs to L^∞.
See Continuous.memLp_of_hasCompactSupport for a version for L^p.