theorem
MeasureTheory.eLpNorm_zero_of_ae_zero'
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_6}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
(h : enorm ∘ f =ᵐ[μ] 0)
:
theorem
MeasureTheory.eLpNormEssSup_map_measure'
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
[MeasurableSpace E]
[OpensMeasurableSpace E]
(hg : AEMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm_map_measure'
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
[MeasurableSpace E]
[OpensMeasurableSpace E]
(hg : AEMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm_comp_measurePreserving'
{α : Type u_1}
{E : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → E}
{ν : Measure β}
[MeasurableSpace E]
[OpensMeasurableSpace E]
(hg : AEMeasurable g ν)
(hf : MeasurePreserving f μ ν)
:
theorem
MeasureTheory.eLpNormEssSup_iSup
{α : Type u_6}
{ι : Type u_7}
[Countable ι]
[MeasurableSpace α]
{μ : Measure α}
(f : ι → α → ENNReal)
:
theorem
MeasureTheory.eLpNorm_iSup'
{α : Type u_6}
[MeasurableSpace α]
{μ : Measure α}
{p : ENNReal}
{f : ℕ → α → ENNReal}
(hf : ∀ (n : ℕ), AEMeasurable (f n) μ)
(h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun (n : ℕ) => f n x)
:
Monotone convergence applied to eLpNorms. AEMeasurable variant.
Possibly imperfect hypotheses, particularly on p. Note that for p = ∞ the stronger
statement in eLpNormEssSup_iSup holds.
theorem
MeasureTheory.eLpNormEssSup_indicator_const_eq'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_6}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{s : Set α}
{c : ε}
(hμs : μ s = 0)
:
theorem
MeasureTheory.eLpNorm'_const_smul_le''
{α : Type u_1}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul NNReal ε]
[ENormSMulClass NNReal ε]
{c : NNReal}
{f : α → ε}
(hq : 0 < q)
:
theorem
MeasureTheory.eLpNormEssSup_const_smul_le''
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul NNReal ε]
[ENormSMulClass NNReal ε]
{c : NNReal}
{f : α → ε}
:
theorem
MeasureTheory.eLpNorm_const_smul_le''
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul NNReal ε]
[ENormSMulClass NNReal ε]
{c : NNReal}
{f : α → ε}
:
theorem
MeasureTheory.MemLp.const_smul''
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul NNReal ε]
[ENormSMulClass NNReal ε]
{c : NNReal}
{f : α → ε}
[ContinuousConstSMul NNReal ε]
(hf : MemLp f p μ)
:
theorem
MeasureTheory.MemLp.const_mul''
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul NNReal ε]
[ENormSMulClass NNReal ε]
{c : NNReal}
{f : α → ε}
[ContinuousConstSMul NNReal ε]
(hf : MemLp f p μ)
:
theorem
MeasureTheory.MemLp.eLpNormEssSup_lt_top
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_6}
[TopologicalSpace ε]
[ENorm ε]
{f : α → ε}
(hu : MemLp f ⊤ μ)
: