noncomputable def
MeasureTheory.wnorm'
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(p : ℝ)
(μ : Measure α)
:
The weak L^p norm of a function, for p < ∞
Equations
- MeasureTheory.wnorm' f p μ = ⨆ (t : NNReal), ↑t * MeasureTheory.distribution f (↑t) μ ^ p⁻¹
Instances For
theorem
MeasureTheory.wnorm'_zero
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(μ : Measure α)
:
theorem
MeasureTheory.wnorm'_toReal_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
{p : ℝ}
(hp : 0 ≤ p)
:
noncomputable def
MeasureTheory.wnorm
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(p : ENNReal)
(μ : Measure α)
:
The weak L^p norm of a function.
Equations
- MeasureTheory.wnorm f p μ = if p = ⊤ then MeasureTheory.eLpNormEssSup f μ else MeasureTheory.wnorm' f p.toReal μ
Instances For
@[simp]
theorem
MeasureTheory.wnorm_zero
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
:
@[simp]
theorem
MeasureTheory.wnorm_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
:
theorem
MeasureTheory.wnorm_ofReal
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
{p : ℝ}
(hp : 0 ≤ p)
:
theorem
MeasureTheory.wnorm_toReal_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
{p : ENNReal}
:
theorem
MeasureTheory.wnorm_indicator_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_12}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{a : ε}
{s : Set α}
{p : ENNReal}
(h₀ : ¬p = 0)
(h₁ : ¬p = ⊤)
:
def
MeasureTheory.MemWLp
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
[TopologicalSpace ε]
(f : α → ε)
(p : ENNReal)
(μ : Measure α)
:
A function is in weak-L^p if it is (strongly a.e.)-measurable and has finite weak L^p norm.
Equations
- MeasureTheory.MemWLp f p μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.wnorm f p μ < ⊤)
Instances For
theorem
MeasureTheory.MemWLp_zero
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
[TopologicalSpace ε]
:
theorem
MeasureTheory.MemWLp.aeStronglyMeasurable
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
[TopologicalSpace ε]
(hf : MemWLp f p μ)
:
theorem
MeasureTheory.MemWLp.wnorm_lt_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
[TopologicalSpace ε]
(hf : MemWLp f p μ)
:
theorem
MeasureTheory.MemWLp.ennreal_toReal
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{f : α → ENNReal}
(hf : MemWLp f p μ)
:
MemWLp (ENNReal.toReal ∘ f) p μ
theorem
MeasureTheory.distribution_le
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
[MeasurableSpace ε]
[OpensMeasurableSpace ε]
{c : ENNReal}
(hc : c ≠ 0)
{μ : Measure α}
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.wnorm'_le_eLpNorm'
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(p0 : 0 < p)
:
theorem
MeasureTheory.distribution_lt_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : MemLp f p μ)
(p_pos : 0 < p)
(p_ne_top : p ≠ ⊤)
{t : NNReal}
(ht : 0 < t)
:
theorem
MeasureTheory.wnorm_le_eLpNorm
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ENNReal}
(hp : 0 < p)
:
theorem
MeasureTheory.MemLp.memWLp
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hp : 0 < p)
(hf : MemLp f p μ)
:
MemWLp f p μ
def
MeasureTheory.HasWeakType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
[ENorm ε₁]
[ENorm ε₂]
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
An operator has weak type (p, q) if it is bounded as a map from L^p to weak L^q.
HasWeakType T p p' μ ν c means that T has weak type (p, p') w.r.t. measures μ, ν
and constant c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.HasBoundedWeakType
{ε₁ : Type u_4}
{ε₂ : Type u_5}
[ENorm ε₁]
[ENorm ε₂]
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{α : Type u_12}
{α' : Type u_13}
[Zero ε₁]
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
A weaker version of HasWeakType.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.HasStrongType
{ε₁ : Type u_4}
{ε₂ : Type u_5}
[ENorm ε₁]
[ENorm ε₂]
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{α : Type u_12}
{α' : Type u_13}
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
An operator has strong type (p, q) if it is bounded as an operator on L^p → L^q.
HasStrongType T p p' μ ν c means that T has strong type (p, p') w.r.t. measures μ, ν
and constant c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.HasBoundedStrongType
{ε₁ : Type u_4}
{ε₂ : Type u_5}
[ENorm ε₁]
[ENorm ε₂]
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{α : Type u_12}
{α' : Type u_13}
[Zero ε₁]
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : ENNReal)
:
A weaker version of HasStrongType. This is the same as HasStrongType if T is continuous
w.r.t. the L^2 norm, but weaker in general.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lemmas about HasWeakType #
theorem
MeasureTheory.HasWeakType.memWLp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
{f₁ : α → ε₁}
(h : HasWeakType T p p' μ ν c)
(hf₁ : MemLp f₁ p μ)
(hc : c < ⊤ := by finiteness)
:
MemWLp (T f₁) p' ν
theorem
MeasureTheory.HasWeakType.toReal
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(h : HasWeakType T p p' μ ν c)
:
HasWeakType (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) p p' μ ν c
theorem
MeasureTheory.aestronglyMeasurable_ennreal_toReal_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
(hf : NullMeasurableSet (f ⁻¹' {⊤}) μ)
:
theorem
MeasureTheory.hasWeakType_toReal_iff
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(hT : ∀ (f : α → ε₁), MemLp f p μ → ∀ᵐ (x : α') ∂ν, T f x ≠ ⊤)
:
theorem
MeasureTheory.hasWeakType_iSup_of_monotone
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
{f : ℕ → (α → ε₁) → α' → ENNReal}
(hf : Monotone f)
(hp' : p' ≠ 0)
(hwtf : ∀ (n : ℕ), HasWeakType (f n) p p' μ ν c)
:
HasWeakType (fun (u : α → ε₁) (x : α') => ⨆ (n : ℕ), f n u x) p p' μ ν c
Lemmas about HasBoundedWeakType #
theorem
MeasureTheory.HasBoundedWeakType.memWLp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ENorm ε₂]
{f₁ : α → ε₁}
(h : HasBoundedWeakType T p p' μ ν c)
(hf₁ : BoundedFiniteSupport f₁ μ)
(hc : c < ⊤ := by finiteness)
:
MemWLp (T f₁) p' ν
theorem
MeasureTheory.HasWeakType.hasBoundedWeakType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ENorm ε₂]
(h : HasWeakType T p p' μ ν c)
:
HasBoundedWeakType T p p' μ ν c
Lemmas about HasStrongType #
theorem
MeasureTheory.HasStrongType.memLp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
{f₁ : α → ε₁}
(h : HasStrongType T p p' μ ν c)
(hf₁ : MemLp f₁ p μ)
(hc : c < ⊤ := by finiteness)
:
MemLp (T f₁) p' ν
theorem
MeasureTheory.HasStrongType.hasWeakType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
(hp' : 0 < p')
(h : HasStrongType T p p' μ ν c)
:
HasWeakType T p p' μ ν c
theorem
MeasureTheory.HasStrongType.toReal
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(h : HasStrongType T p p' μ ν c)
:
HasStrongType (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) p p' μ ν c
theorem
MeasureTheory.hasStrongType_toReal_iff
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(hT : ∀ (f : α → ε₁), MemLp f p μ → ∀ᵐ (x : α') ∂ν, T f x ≠ ⊤)
:
HasStrongType (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) p p' μ ν c ↔ HasStrongType T p p' μ ν c
theorem
MeasureTheory.hasStrongType_iSup_of_monotone
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ContinuousENorm ε₁]
{f : ℕ → (α → ε₁) → α' → ENNReal}
(hf : Monotone f)
(hstf : ∀ (n : ℕ), HasStrongType (f n) p p' μ ν c)
:
HasStrongType (fun (u : α → ε₁) (x : α') => ⨆ (n : ℕ), f n u x) p p' μ ν c
Lemmas about HasBoundedStrongType #
theorem
MeasureTheory.HasBoundedStrongType.memLp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
{f₁ : α → ε₁}
(h : HasBoundedStrongType T p p' μ ν c)
(hf₁ : BoundedFiniteSupport f₁ μ)
(hc : c < ⊤ := by finiteness)
:
MemLp (T f₁) p' ν
theorem
MeasureTheory.HasStrongType.hasBoundedStrongType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
(h : HasStrongType T p p' μ ν c)
:
HasBoundedStrongType T p p' μ ν c
theorem
MeasureTheory.HasBoundedStrongType.hasBoundedWeakType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[TopologicalSpace ε₁]
[ESeminormedAddMonoid ε₁]
[TopologicalSpace ε₂]
[ContinuousENorm ε₂]
(hp' : 0 < p')
(h : HasBoundedStrongType T p p' μ ν c)
:
HasBoundedWeakType T p p' μ ν c
theorem
MeasureTheory.HasBoundedStrongType.const_smul
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' c : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[TopologicalSpace ε₁]
[ESeminormedAddMonoid ε₁]
{T : (α → ε₁) → α' → ENNReal}
(h : HasBoundedStrongType T p p' μ ν c)
(r : NNReal)
:
HasBoundedStrongType (r • T) p p' μ ν (r • c)
theorem
MeasureTheory.distribution_smul_left
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{ε' : Type u_13}
[TopologicalSpace ε']
[ENormedSpace ε']
{f : α → ε'}
{c : NNReal}
(hc : c ≠ 0)
:
theorem
MeasureTheory.distribution_smul_left'
{α : Type u_1}
{𝕜 : Type u_7}
{E : Type u_8}
{m : MeasurableSpace α}
{μ : Measure α}
[NontriviallyNormedField 𝕜]
{t : ENNReal}
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[NormSMulClass 𝕜 E]
{f : α → E}
{c : 𝕜}
(hc : c ≠ 0)
:
theorem
MeasureTheory.HasStrongType.const_smul
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
{ε' : Type u_13}
[TopologicalSpace ε]
[ENorm ε]
[TopologicalSpace ε']
[ENormedSpace ε']
[ContinuousConstSMul NNReal ε']
{T : (α → ε) → α' → ε'}
{c : ENNReal}
(h : HasStrongType T p p' μ ν c)
(k : NNReal)
:
HasStrongType (k • T) p p' μ ν (‖k‖ₑ * c)
theorem
MeasureTheory.HasStrongType.const_smul'
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{𝕜 : Type u_15}
{E' : Type u_16}
[NormedRing 𝕜]
[NormedAddCommGroup E']
[MulActionWithZero 𝕜 E']
[IsBoundedSMul 𝕜 E']
{T : (α → ε) → α' → E'}
{c : ENNReal}
(h : HasStrongType T p p' μ ν c)
(k : 𝕜)
:
HasStrongType (k • T) p p' μ ν (‖k‖ₑ * c)
theorem
MeasureTheory.HasStrongType.const_mul
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{T : (α → ε) → α' → ENNReal}
{c : ENNReal}
(h : HasStrongType T p p' μ ν c)
(e : NNReal)
:
HasStrongType (fun (f : α → ε) (x : α') => ↑e * T f x) p p' μ ν (‖e‖ₑ * c)
theorem
MeasureTheory.HasStrongType.const_mul'
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{E' : Type u_15}
[NormedRing E']
{T : (α → ε) → α' → E'}
{c : ENNReal}
(h : HasStrongType T p p' μ ν c)
(e : E')
:
HasStrongType (fun (f : α → ε) (x : α') => e * T f x) p p' μ ν (‖e‖ₑ * c)
theorem
MeasureTheory.wnorm_const_smul_le
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε' : Type u_13}
[TopologicalSpace ε']
[ENormedSpace ε']
(hp : p ≠ 0)
{f : α → ε'}
(k : NNReal)
:
theorem
MeasureTheory.wnorm_const_smul_le'
{α : Type u_1}
{𝕜 : Type u_7}
{E : Type u_8}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[NormSMulClass 𝕜 E]
[IsBoundedSMul 𝕜 E]
(hp : p ≠ 0)
{f : α → E}
(k : 𝕜)
:
theorem
MeasureTheory.HasWeakType.const_smul
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
{ε' : Type u_13}
[TopologicalSpace ε]
[ENorm ε]
[TopologicalSpace ε']
[ENormedSpace ε']
[ContinuousConstSMul NNReal ε']
{T : (α → ε) → α' → ε'}
(hp' : p' ≠ 0)
{c : ENNReal}
(h : HasWeakType T p p' μ ν c)
(k : NNReal)
:
HasWeakType (k • T) p p' μ ν (↑k * c)
theorem
MeasureTheory.HasWeakType.const_smul'
{α : Type u_1}
{α' : Type u_2}
{𝕜 : Type u_7}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[NontriviallyNormedField 𝕜]
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{E' : Type u_14}
[NormedAddCommGroup E']
[MulActionWithZero 𝕜 E']
[NormSMulClass 𝕜 E']
[IsBoundedSMul 𝕜 E']
{T : (α → ε) → α' → E'}
(hp' : p' ≠ 0)
{c : ENNReal}
(h : HasWeakType T p p' μ ν c)
(k : 𝕜)
:
HasWeakType (k • T) p p' μ ν (‖k‖ₑ * c)
theorem
MeasureTheory.HasWeakType.const_mul
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{T : (α → ε) → α' → ENNReal}
(hp' : p' ≠ 0)
{c : ENNReal}
(h : HasWeakType T p p' μ ν c)
(e : NNReal)
:
HasWeakType (fun (f : α → ε) (x : α') => ↑e * T f x) p p' μ ν (↑e * c)
theorem
MeasureTheory.HasWeakType.const_mul'
{α : Type u_1}
{α' : Type u_2}
{𝕜 : Type u_7}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
[NontriviallyNormedField 𝕜]
{ε : Type u_12}
[TopologicalSpace ε]
[ENorm ε]
{T : (α → ε) → α' → 𝕜}
(hp' : p' ≠ 0)
{c : ENNReal}
(h : HasWeakType T p p' μ ν c)
(e : 𝕜)
:
HasWeakType (fun (f : α → ε) (x : α') => e * T f x) p p' μ ν (‖e‖ₑ * c)
theorem
ContinuousLinearMap.distribution_le
{α : Type u_1}
{𝕜 : Type u_7}
{E₁ : Type u_9}
{E₂ : Type u_10}
{E₃ : Type u_11}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NontriviallyNormedField 𝕜]
{t s : ENNReal}
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[NormedAddCommGroup E₃]
[NormedSpace 𝕜 E₃]
{f : α → E₁}
{g : α → E₂}
(L : E₁ →L[𝕜] E₂ →L[𝕜] E₃)
:
MeasureTheory.distribution (fun (x : α) => (L (f x)) (g x)) (‖L‖ₑ * t * s) μ ≤ MeasureTheory.distribution f t μ + MeasureTheory.distribution g s μ
theorem
MeasureTheory.lintegral_norm_pow_eq_distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(hp : 0 < p)
:
The layer-cake theorem, or Cavalieri's principle for functions into a space with a continuous enorm.
theorem
MeasureTheory.eLpNorm_pow_eq_distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : NNReal}
(hp : 0 < p)
:
eLpNorm f (↑p) μ ^ ↑p = ∫⁻ (t : ℝ) in Set.Ioi 0, ↑p * ENNReal.ofReal (t ^ (↑p - 1)) * distribution f (ENNReal.ofReal t) μ
The layer-cake theorem, or Cavalieri's principle, written using eLpNorm.
theorem
MeasureTheory.eLpNorm_eq_distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(hp : 0 < p)
:
eLpNorm f (ENNReal.ofReal p) μ = (ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, distribution f (ENNReal.ofReal t) μ * ENNReal.ofReal (t ^ (p - 1))) ^ p⁻¹
The layer-cake theorem, or Cavalieri's principle, written using eLpNorm, without
taking powers.
theorem
MeasureTheory.lintegral_pow_mul_distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(hp : -1 < p)
: