theorem
ENNNorm_absolute_homogeneous
{𝕜 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{c : 𝕜}
(z : E)
:
theorem
measure_mono_ae'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{A B : Set α}
(h : μ (B \ A) = 0)
:
μ B ≤ μ A
theorem
eLpNormEssSup_toReal_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
:
theorem
eLpNormEssSup_toReal_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤)
:
theorem
eLpNorm'_toReal_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
{p : ℝ}
(hp : 0 ≤ p)
:
MeasureTheory.eLpNorm' (ENNReal.toReal ∘ f) p μ ≤ MeasureTheory.eLpNorm' f p μ
theorem
eLpNorm'_toReal_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
{p : ℝ}
(hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤)
:
MeasureTheory.eLpNorm' (ENNReal.toReal ∘ f) p μ = MeasureTheory.eLpNorm' f p μ
theorem
eLpNorm_toReal_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{f : α → ENNReal}
:
MeasureTheory.eLpNorm (ENNReal.toReal ∘ f) p μ ≤ MeasureTheory.eLpNorm f p μ
theorem
eLpNorm_toReal_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{f : α → ENNReal}
(hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤)
:
MeasureTheory.eLpNorm (ENNReal.toReal ∘ f) p μ = MeasureTheory.eLpNorm f p μ
The distribution function d_f #
def
MeasureTheory.distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(t : ENNReal)
(μ : Measure α)
:
The distribution function of a function f.
Note that unlike the notes, we also define this for t = ∞.
Note: we also want to use this for functions with codomain ℝ≥0∞, but for those we just write
μ { x | t < f x }
Equations
- MeasureTheory.distribution f t μ = μ {x : α | t < ‖f x‖ₑ}
Instances For
theorem
MeasureTheory.distribution_mono_right
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t s : ENNReal}
[ENorm ε]
{f : α → ε}
(h : t ≤ s)
:
distribution f s μ ≤ distribution f t μ
theorem
MeasureTheory.distribution_mono_right'
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
:
Antitone fun (t : ENNReal) => distribution f t μ
theorem
MeasureTheory.distribution_measurable₀
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
:
Measurable fun (t : ENNReal) => distribution f t μ
theorem
MeasureTheory.distribution_measurable
{α : Type u_1}
{α' : Type u_2}
{ε : Type u_3}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
{g : α' → ENNReal}
(hg : Measurable g)
:
Measurable fun (y : α') => distribution f (g y) μ
theorem
MeasureTheory.distribution_toReal_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{f : α → ENNReal}
:
distribution (ENNReal.toReal ∘ f) t μ ≤ distribution f t μ
theorem
MeasureTheory.distribution_toReal_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{f : α → ENNReal}
(hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤)
:
distribution (ENNReal.toReal ∘ f) t μ = distribution f t μ
theorem
MeasureTheory.distribution_add_le_of_enorm
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t s : ENNReal}
[ENorm ε]
{f g₁ g₂ : α → ε}
{A : ENNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ A * (‖g₁ x‖ₑ + ‖g₂ x‖ₑ))
:
distribution f (A * (t + s)) μ ≤ distribution g₁ t μ + distribution g₂ s μ
theorem
MeasureTheory.select_neighborhood_distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
(t₀ l : ENNReal)
(hu : l < distribution f t₀ μ)
:
∃ (n : ℕ), l < distribution f (t₀ + (↑n)⁻¹) μ
theorem
MeasureTheory.continuousWithinAt_distribution
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
(t₀ : ENNReal)
:
ContinuousWithinAt (fun (x : ENNReal) => distribution f x μ) (Set.Ioi t₀) t₀
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)
:
wnorm' (ENNReal.toReal ∘ f) p μ ≤ wnorm' f p μ
theorem
MeasureTheory.wnorm'_toReal_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
{p : ℝ}
(hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤)
:
wnorm' (ENNReal.toReal ∘ f) p μ = wnorm' f p μ
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
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 : α → ε}
:
wnorm f ⊤ μ = eLpNormEssSup f μ
theorem
MeasureTheory.wnorm_ofReal
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
{p : ℝ}
(hp : 0 ≤ p)
:
wnorm f (ENNReal.ofReal p) μ = wnorm' f p μ
theorem
MeasureTheory.wnorm_toReal_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
{p : ENNReal}
:
wnorm (ENNReal.toReal ∘ f) p μ ≤ wnorm f p μ
theorem
MeasureTheory.wnorm_toReal_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
{p : ENNReal}
(hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤)
:
wnorm (ENNReal.toReal ∘ f) p μ = wnorm f p μ
theorem
MeasureTheory.wnorm'_le_eLpNorm'
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ℝ}
(hp : 1 ≤ p)
:
theorem
MeasureTheory.wnorm_le_eLpNorm
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{p : ENNReal}
(hp : 1 ≤ p)
:
def
MeasureTheory.MemWℒp
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ContinuousENorm ε]
(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.MemWℒp f p μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.wnorm f p μ < ⊤)
Instances For
theorem
MeasureTheory.Memℒp.memWℒp
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ContinuousENorm ε]
{f : α → ε}
(hp : 1 ≤ p)
(hf : Memℒp f p μ)
:
MemWℒp f p μ
theorem
MeasureTheory.MemWℒp_zero
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ContinuousENorm ε]
{f : α → ε}
:
theorem
MeasureTheory.MemWℒp.aeStronglyMeasurable
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ContinuousENorm ε]
{f : α → ε}
(hf : MemWℒp f p μ)
:
theorem
MeasureTheory.MemWℒp.wnorm_lt_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[ContinuousENorm ε]
{f : α → ε}
(hf : MemWℒp f p μ)
:
theorem
MeasureTheory.MemWℒp.ennreal_toReal
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{f : α → ENNReal}
(hf : MemWℒp f p μ)
:
MemWℒp (ENNReal.toReal ∘ f) p μ
theorem
MeasureTheory.MemWℒp.ae_ne_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ContinuousENorm ε]
{f : α → ε}
{p : ENNReal}
{μ : Measure α}
(hf : MemWℒp f p μ)
:
If a function f is MemWℒp, then its norm is almost everywhere finite.
def
MeasureTheory.HasWeakType
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : NNReal)
:
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}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
{α : Type u_12}
{α' : Type u_13}
[Zero ε₁]
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : NNReal)
:
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}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
{α : Type u_12}
{α' : Type u_13}
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : NNReal)
:
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}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
{α : Type u_12}
{α' : Type u_13}
[Zero ε₁]
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → ε₁) → α' → ε₂)
(p p' : ENNReal)
(μ : Measure α)
(ν : Measure α')
(c : NNReal)
:
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.memWℒp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
{f₁ : α → ε₁}
(h : HasWeakType T p p' μ ν c)
(hf₁ : Memℒp f₁ p μ)
:
MemWℒp (T f₁) p' ν
theorem
MeasureTheory.HasWeakType.toReal
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(h : HasWeakType T p p' μ ν c)
:
HasWeakType (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) p p' μ ν c
theorem
MeasureTheory.toReal_ofReal_preimage
{s : Set ENNReal}
:
s = if ⊤ ∈ s ↔ 0 ∈ s then ENNReal.toReal ⁻¹' (ENNReal.ofReal ⁻¹' s)
else
if 0 ∈ s then ENNReal.toReal ⁻¹' (ENNReal.ofReal ⁻¹' s) \ {⊤} else ENNReal.toReal ⁻¹' (ENNReal.ofReal ⁻¹' s) ∪ {⊤}
theorem
MeasureTheory.aestronglyMeasurable_ennreal_toReal_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
(hf : NullMeasurableSet (f ⁻¹' {⊤}) μ)
:
AEStronglyMeasurable (ENNReal.toReal ∘ f) μ ↔ AEStronglyMeasurable f μ
theorem
MeasureTheory.hasWeakType_toReal_iff
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(hT : ∀ (f : α → ε₁), Memℒp f p μ → ∀ᵐ (x : α') ∂ν, T f x ≠ ⊤)
:
HasWeakType (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) p p' μ ν c ↔ HasWeakType T p p' μ ν c
Lemmas about HasBoundedWeakType #
theorem
MeasureTheory.HasBoundedWeakType.memWℒp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
{f₁ : α → ε₁}
[Zero ε₁]
(h : HasBoundedWeakType T p p' μ ν c)
(hf₁ : Memℒp f₁ p μ)
(h2f₁ : eLpNorm f₁ ⊤ μ < ⊤)
(h3f₁ : μ (Function.support f₁) < ⊤)
:
MemWℒp (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' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
[Zero ε₁]
(h : HasWeakType T p p' μ ν c)
:
HasBoundedWeakType T p p' μ ν c
Lemmas about HasStrongType #
theorem
MeasureTheory.HasStrongType.memℒp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
{f₁ : α → ε₁}
(h : HasStrongType T p p' μ ν c)
(hf₁ : Memℒp f₁ p μ)
:
Memℒp (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' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
(hp' : 1 ≤ 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' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
[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' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
[ContinuousENorm ε₁]
{T : (α → ε₁) → α' → ENNReal}
(hT : ∀ (f : α → ε₁), Memℒp f p μ → ∀ᵐ (x : α') ∂ν, T f x ≠ ⊤)
:
HasStrongType (fun (x1 : α → ε₁) (x2 : α') => (T x1 x2).toReal) p p' μ ν c ↔ HasStrongType T p p' μ ν c
Lemmas about HasBoundedStrongType #
theorem
MeasureTheory.HasBoundedStrongType.memℒp
{α : Type u_1}
{α' : Type u_2}
{ε₁ : Type u_4}
{ε₂ : Type u_5}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
{f₁ : α → ε₁}
[Zero ε₁]
(h : HasBoundedStrongType T p p' μ ν c)
(hf₁ : Memℒp f₁ p μ)
(h2f₁ : eLpNorm f₁ ⊤ μ < ⊤)
(h3f₁ : μ (Function.support f₁) < ⊤)
:
Memℒp (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' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
[Zero ε₁]
(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' : ENNReal}
{c : NNReal}
{μ : Measure α}
{ν : Measure α'}
{T : (α → ε₁) → α' → ε₂}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
[Zero ε₁]
(hp' : 1 ≤ p')
(h : HasBoundedStrongType T p p' μ ν c)
:
HasBoundedWeakType T p p' μ ν c
theorem
MeasureTheory.distribution_eq_nnnorm
{α : Type u_1}
{E : Type u_8}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{t : ENNReal}
{f : α → E}
:
distribution f t μ = μ {x : α | t < ↑‖f x‖₊}
theorem
MeasureTheory.distribution_mono_left
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{f g : α → ε}
[ContinuousENorm ε]
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ)
:
distribution f t μ ≤ distribution g t μ
theorem
MeasureTheory.distribution_mono
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t s : ENNReal}
{f g : α → ε}
[ContinuousENorm ε]
(h₁ : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ)
(h₂ : t ≤ s)
:
distribution f s μ ≤ distribution g t μ
theorem
MeasureTheory.distribution_snormEssSup
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ε}
[ContinuousENorm ε]
:
distribution f (eLpNormEssSup f μ) μ = 0
theorem
MeasureTheory.distribution_smul_left
{α : Type u_1}
{𝕜 : Type u_7}
{E : Type u_8}
{m : MeasurableSpace α}
{μ : Measure α}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{t : ENNReal}
{f : α → E}
{c : 𝕜}
(hc : c ≠ 0)
:
distribution (c • f) t μ = distribution f (t / ↑‖c‖₊) μ
theorem
MeasureTheory.distribution_add_le'
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t s : ENNReal}
{f : α → ε}
[ContinuousENorm ε]
{A : ENNReal}
{g₁ g₂ : α → ε}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ A * (‖g₁ x‖ₑ + ‖g₂ x‖ₑ))
:
distribution f (A * (t + s)) μ ≤ distribution g₁ t μ + distribution g₂ s μ
theorem
MeasureTheory.HasStrongType.const_smul
{ε : Type u_3}
[ContinuousENorm ε]
{𝕜 : Type u_12}
{E' : Type u_13}
{α : Type u_14}
{α' : Type u_15}
[NormedAddCommGroup E']
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
{T : (α → ε) → α' → E'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{c : NNReal}
(h : HasStrongType T p p' μ ν c)
[NormedRing 𝕜]
[MulActionWithZero 𝕜 E']
[BoundedSMul 𝕜 E']
(k : 𝕜)
:
HasStrongType (k • T) p p' μ ν (‖k‖₊ * c)
theorem
MeasureTheory.HasStrongType.const_mul
{ε : Type u_3}
[ContinuousENorm ε]
{E' : Type u_12}
{α : Type u_13}
{α' : Type u_14}
[NormedRing E']
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
{T : (α → ε) → α' → E'}
{p p' : ENNReal}
{μ : Measure α}
{ν : Measure α'}
{c : NNReal}
(h : HasStrongType T p p' μ ν c)
(e : E')
:
HasStrongType (fun (f : α → ε) (x : α') => e * T f x) p p' μ ν (‖e‖₊ * c)
theorem
MeasureTheory.distribution_add_le
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t s : ENNReal}
{f g : α → ε}
[ENormedAddMonoid ε]
:
distribution (f + g) (t + s) μ ≤ distribution f t μ + distribution g s μ
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 𝕜]
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[NormedAddCommGroup E₃]
[NormedSpace 𝕜 E₃]
(L : E₁ →L[𝕜] E₂ →L[𝕜] E₃)
{t s : ENNReal}
{f : α → E₁}
{g : α → 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}
{E : Type u_8}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{f : α → E}
(hf : AEMeasurable f μ)
{p : ℝ}
(hp : 0 < p)
:
∫⁻ (x : α), ‖f x‖ₑ ^ p ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (p * t ^ (p - 1)) * distribution f (ENNReal.ofReal t) μ
The layer-cake theorem, or Cavalieri's principle for functions into a normed group.
theorem
MeasureTheory.eLpNorm_pow_eq_distribution
{α : Type u_1}
{E : Type u_8}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{f : α → E}
(hf : AEMeasurable 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}
{E : Type u_8}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{f : α → E}
(hf : AEMeasurable 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}
{E : Type u_8}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{f : α → E}
(hf : AEMeasurable f μ)
{p : ℝ}
(hp : -1 < p)
:
∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (t ^ p) * distribution f (ENNReal.ofReal t) μ = ENNReal.ofReal (p + 1)⁻¹ * ∫⁻ (x : α), ‖f x‖ₑ ^ (p + 1) ∂μ