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 =ᶠ[ae μ] g)
:
theorem
MeasureTheory.eLpNormEssSup_mono_nnnorm_ae
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f g : α → F}
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm_mono_nnnorm
{α : Type u_1}
{F : Type u_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 =ᶠ[ae μ] g)
:
theorem
MeasureTheory.MemLp.ae_eq
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ENorm ε]
[TopologicalSpace ε]
{f g : α → ε}
(hfg : f =ᶠ[ae μ] 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_indicator_eq_eLpNorm_restrict
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
{s : Set α}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{s : Set α}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.eLpNorm_restrict_le
{α : Type u_1}
{m0 : MeasurableSpace α}
{ε' : Type u_8}
[TopologicalSpace ε']
[ContinuousENorm ε']
(f : α → ε')
(p : ENNReal)
(μ : Measure α)
(s : Set α)
:
theorem
MeasureTheory.eLpNorm_indicator_le
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{s : Set α}
(f : α → ε)
:
theorem
MeasureTheory.eLpNormEssSup_indicator_le
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
(s : Set α)
(f : α → ε)
:
theorem
MeasureTheory.eLpNormEssSup_indicator_const_le
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
(s : Set α)
(c : ε)
:
theorem
MeasureTheory.eLpNormEssSup_indicator_const_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
(s : Set α)
(c : ε)
(hμs : μ s ≠ 0)
:
theorem
MeasureTheory.eLpNorm_indicator_const₀
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{c : ε}
{s : Set α}
(hs : NullMeasurableSet s μ)
(hp : p ≠ 0)
(hp_top : p ≠ ⊤)
:
theorem
MeasureTheory.eLpNorm_indicator_const
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{c : ε}
{s : Set α}
(hs : MeasurableSet s)
(hp : p ≠ 0)
(hp_top : p ≠ ⊤)
:
theorem
MeasureTheory.eLpNorm_indicator_const'
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{c : ε}
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ 0)
(hp : p ≠ 0)
:
theorem
MeasureTheory.eLpNorm_indicator_const_le
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
(c : ε)
{s : Set α}
(p : ENNReal)
:
theorem
MeasureTheory.MemLp.indicator
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{s : Set α}
{f : α → ε}
(hs : MeasurableSet s)
(hf : MemLp f p μ)
:
theorem
MeasureTheory.memLp_indicator_iff_restrict
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{s : Set α}
{f : α → ε}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.memLp_indicator_const
{α : Type u_1}
{E : Type u_4}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{s : Set α}
(p : ENNReal)
(hs : MeasurableSet s)
(c : E)
(hμsc : c = 0 ∨ μ s ≠ ⊤)
:
theorem
MeasureTheory.eLpNormEssSup_piecewise
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{s : Set α}
(f g : α → ε)
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
eLpNormEssSup (s.piecewise f g) μ = max (eLpNormEssSup f (μ.restrict s)) (eLpNormEssSup g (μ.restrict sᶜ))
theorem
MeasureTheory.eLpNorm_top_piecewise
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{s : Set α}
(f g : α → ε)
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
theorem
MeasureTheory.MemLp.piecewise
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{s : Set α}
{f : α → ε}
[DecidablePred fun (x : α) => x ∈ s]
{g : α → ε}
(hs : MeasurableSet s)
(hf : MemLp f p (μ.restrict s))
(hg : MemLp g p (μ.restrict sᶜ))
:
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}
[Zero R]
[SMulWithZero R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[NoZeroSMulDivisors R ENNReal]
{c : R}
(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 =ᶠ[ae μ] 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 =ᶠ[ae μ] 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 =ᶠ[ae μ] 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 α)
:
@[deprecated MeasureTheory.enorm_ae_le_eLpNormEssSup (since := "2025-03-05")]
theorem
MeasureTheory.coe_nnnorm_ae_le_eLpNormEssSup
{α : Type u_1}
{ε : Type u_8}
[ENorm ε]
{x✝ : MeasurableSpace α}
(f : α → ε)
(μ : Measure α)
:
Alias of MeasureTheory.enorm_ae_le_eLpNormEssSup.
@[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.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul
{α : Type u_1}
{F : Type u_5}
{G : Type u_6}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
{p : ℝ}
(hp : 0 < p)
:
theorem
MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
{ε' : Type u_8}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ)
{p : ℝ}
(hp : 0 < p)
:
theorem
MeasureTheory.eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε' : Type u_8}
[TopologicalSpace ε']
[ContinuousENorm ε']
{ε : Type u_9}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
{c : ENNReal}
{g : α → ε'}
{p : ℝ}
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ)
(hp : 0 < p)
:
If ‖f x‖ₑ ≤ c * ‖g x‖ₑ a.e., eLpNorm' f p μ ≤ c * eLpNorm' g p μ for all p ∈ (0, ∞).
theorem
MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
{ε' : Type u_8}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : ENNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ)
:
theorem
MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul
{α : Type u_1}
{F : Type u_5}
{G : Type u_6}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
{ε' : Type u_8}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ)
(p : ENNReal)
:
theorem
MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_5}
{G : Type u_6}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
(p : ENNReal)
:
theorem
MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg
{α : Type u_1}
{F : Type u_5}
{G : Type u_6}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(hc : c < 0)
(p : ENNReal)
:
When c is negative, ‖f x‖ ≤ c * ‖g x‖ is nonsense and forces both f and g to have an
eLpNorm of 0.
theorem
MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_5}
{G : Type u_6}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(p : ENNReal)
:
theorem
MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
{ε' : Type u_8}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ)
(p : ENNReal)
:
If ‖f x‖ₑ ≤ c * ‖g x‖ₑ, then eLpNorm f p μ ≤ c * eLpNorm g p μ.
This version assumes c is finite, but requires no measurability hypothesis on g.
theorem
MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul''
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε' : Type u_8}
[TopologicalSpace ε']
[ContinuousENorm ε']
{ε : Type u_9}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
{c : ENNReal}
{g : α → ε'}
(p : ENNReal)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ)
:
If ‖f x‖ₑ ≤ c * ‖g x‖ₑ, then eLpNorm f p μ ≤ c * eLpNorm g p μ.
This version allows c = ∞, but requires g to be a.e. strongly measurable.
theorem
MeasureTheory.MemLp.of_nnnorm_le_mul
{α : Type u_1}
{E : Type u_4}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
{c : NNReal}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.of_enorm_le_mul
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
{ε' : Type u_8}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : NNReal}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.of_le_mul
{α : Type u_1}
{E : Type u_4}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
{c : ℝ}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.of_le_mul'
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
{ε' : Type u_8}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : NNReal}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ)
:
MemLp f p μ
Bounded actions by normed rings #
In this section we show inequalities on the norm.
theorem
MeasureTheory.eLpNorm'_const_smul_le
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_7}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[IsBoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
(hq : 0 < q)
:
theorem
MeasureTheory.eLpNormEssSup_const_smul_le
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_7}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[IsBoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
:
theorem
MeasureTheory.eLpNorm_const_smul_le
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_7}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[IsBoundedSMul 𝕜 F]
{c : 𝕜}
{f : α → F}
:
theorem
MeasureTheory.MemLp.const_smul
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_7}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[IsBoundedSMul 𝕜 F]
{f : α → F}
(hf : MemLp f p μ)
(c : 𝕜)
:
theorem
MeasureTheory.MemLp.const_mul
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_7}
[NormedRing 𝕜]
{f : α → 𝕜}
(hf : MemLp f p μ)
(c : 𝕜)
:
theorem
MeasureTheory.MemLp.mul_const
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_7}
[NormedRing 𝕜]
{f : α → 𝕜}
(hf : MemLp f p μ)
(c : 𝕜)
:
theorem
MeasureTheory.eLpNorm'_const_smul_le'
{α : Type u_1}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
{𝕜 : Type u_7}
[NormedRing 𝕜]
{ε : Type u_8}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul 𝕜 ε]
[ENormSMulClass 𝕜 ε]
{c : 𝕜}
{f : α → ε}
(hq : 0 < q)
:
theorem
MeasureTheory.eLpNormEssSup_const_smul_le'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_7}
[NormedRing 𝕜]
{ε : Type u_8}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul 𝕜 ε]
[ENormSMulClass 𝕜 ε]
{c : 𝕜}
{f : α → ε}
:
theorem
MeasureTheory.eLpNorm_const_smul_le'
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_7}
[NormedRing 𝕜]
{ε : Type u_8}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul 𝕜 ε]
[ENormSMulClass 𝕜 ε]
{c : 𝕜}
{f : α → ε}
:
theorem
MeasureTheory.MemLp.const_smul'
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_7}
[NormedRing 𝕜]
{ε : Type u_8}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul 𝕜 ε]
[ENormSMulClass 𝕜 ε]
{f : α → ε}
[ContinuousConstSMul 𝕜 ε]
(hf : MemLp f p μ)
(c : 𝕜)
:
theorem
MeasureTheory.MemLp.const_mul'
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_7}
[NormedRing 𝕜]
{f : α → 𝕜}
(hf : MemLp f p μ)
(c : 𝕜)
:
Bounded actions by normed division rings #
The inequalities in the previous section are now tight.
TODO: do these results hold for any NormedRing assuming NormSMulClass?
theorem
MeasureTheory.eLpNorm'_const_smul
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_7}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[NormSMulClass 𝕜 F]
{f : α → F}
(c : 𝕜)
(hq_pos : 0 < q)
:
theorem
MeasureTheory.eLpNormEssSup_const_smul
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_7}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[NormSMulClass 𝕜 F]
(c : 𝕜)
(f : α → F)
:
theorem
MeasureTheory.eLpNorm_const_smul
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
[NormedAddCommGroup F]
{𝕜 : Type u_7}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[NormSMulClass 𝕜 F]
(c : 𝕜)
(f : α → F)
(p : ENNReal)
(μ : Measure α)
:
theorem
MeasureTheory.eLpNorm_nsmul
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(n : ℕ)
(f : α → F)
:
theorem
MeasureTheory.le_eLpNorm_of_bddBelow
{α : Type u_1}
{F : Type u_5}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
(hp : p ≠ 0)
(hp' : p ≠ ⊤)
{f : α → F}
(C : NNReal)
{s : Set α}
(hs : MeasurableSet s)
(hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊)
:
@[simp]
theorem
MeasureTheory.eLpNorm_star
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{R : Type u_7}
[NormedAddCommGroup R]
[StarAddMonoid R]
[NormedStarGroup R]
{p : ENNReal}
{f : α → R}
:
@[simp]
theorem
MeasureTheory.AEEqFun.eLpNorm_star
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{R : Type u_7}
[NormedAddCommGroup R]
[StarAddMonoid R]
[NormedStarGroup R]
{p : ENNReal}
{f : α →ₘ[μ] R}
:
theorem
MeasureTheory.MemLp.star
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{R : Type u_7}
[NormedAddCommGroup R]
[StarAddMonoid R]
[NormedStarGroup R]
{p : ENNReal}
{f : α → R}
(hf : MemLp f p μ)
:
@[simp]
theorem
MeasureTheory.eLpNorm_conj
{α : Type u_1}
{m0 : MeasurableSpace α}
{𝕜 : Type u_7}
[RCLike 𝕜]
(f : α → 𝕜)
(p : ENNReal)
(μ : Measure α)
:
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.
theorem
MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{β : Type u_7}
[NormedAddCommGroup β]
(hp_top : p ≠ ⊤)
{f : α → β}
(hf : MemLp f p μ)
{ε : ENNReal}
(hε : ε ≠ 0)
:
A single function that is MemLp f p μ is tight with respect to μ.