The distribution function d_f #
def
MeasureTheory.distribution
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
[NNNorm E]
(f : α → E)
(t : ENNReal)
(μ : MeasureTheory.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_left
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f g : α → E}
{t : ENNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.distribution f t μ ≤ MeasureTheory.distribution g t μ
theorem
MeasureTheory.distribution_mono_right
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{t s : ENNReal}
(h : t ≤ s)
:
MeasureTheory.distribution f s μ ≤ MeasureTheory.distribution f t μ
theorem
MeasureTheory.distribution_mono_right'
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
:
Antitone fun (t : ENNReal) => MeasureTheory.distribution f t μ
theorem
MeasureTheory.distribution_mono
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f g : α → E}
{t s : ENNReal}
(h₁ : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
(h₂ : t ≤ s)
:
MeasureTheory.distribution f s μ ≤ MeasureTheory.distribution g t μ
theorem
MeasureTheory.ENNNorm_absolute_homogeneous
{𝕜 : Type u_3}
{E : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{c : 𝕜}
(z : E)
:
theorem
MeasureTheory.distribution_snormEssSup
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
:
MeasureTheory.distribution f (MeasureTheory.eLpNormEssSup f μ) μ = 0
theorem
MeasureTheory.distribution_measurable₀
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
:
Measurable fun (t : ENNReal) => MeasureTheory.distribution f t μ
theorem
MeasureTheory.distribution_measurable
{α : Type u_1}
{α' : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α' → ENNReal}
(hg : Measurable g)
:
Measurable fun (y : α') => MeasureTheory.distribution f (g y) μ
theorem
MeasureTheory.distribution_smul_left
{α : Type u_1}
{𝕜 : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{f : α → E}
{t : ENNReal}
{c : 𝕜}
(hc : c ≠ 0)
:
MeasureTheory.distribution (c • f) t μ = MeasureTheory.distribution f (t / ↑‖c‖₊) μ
theorem
MeasureTheory.measure_mono_ae'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{A B : Set α}
(h : μ (B \ A) = 0)
:
μ B ≤ μ A
theorem
MeasureTheory.distribution_add_le'
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{t s : ENNReal}
{A : ℝ}
(hA : A ≥ 0)
(g₁ g₂ : α → E)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ A * (‖g₁ x‖ + ‖g₂ x‖))
:
MeasureTheory.distribution f (ENNReal.ofReal A * (t + s)) μ ≤ MeasureTheory.distribution g₁ t μ + MeasureTheory.distribution g₂ s μ
theorem
MeasureTheory.distribution_add_le
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f g : α → E}
{t s : ENNReal}
:
MeasureTheory.distribution (f + g) (t + s) μ ≤ MeasureTheory.distribution f t μ + MeasureTheory.distribution g s μ
theorem
MeasureTheory.tendsto_measure_iUnion_distribution
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(t₀ : ENNReal)
:
theorem
MeasureTheory.select_neighborhood_distribution
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(t₀ l : ENNReal)
(hu : l < MeasureTheory.distribution f t₀ μ)
:
∃ (n : ℕ), l < MeasureTheory.distribution f (t₀ + (↑n)⁻¹) μ
theorem
MeasureTheory.continuousWithinAt_distribution
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(t₀ : ENNReal)
:
ContinuousWithinAt (fun (x : ENNReal) => MeasureTheory.distribution f x μ) (Set.Ioi t₀) t₀
theorem
ContinuousLinearMap.distribution_le
{α : Type u_1}
{𝕜 : Type u_3}
{E₁ : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
{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_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
[MeasurableSpace E]
[BorelSpace E]
(hf : AEMeasurable f μ)
{p : ℝ}
(hp : 0 < p)
:
∫⁻ (x : α), ↑‖f x‖₊ ^ p ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (p * t ^ (p - 1)) * MeasureTheory.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_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
[MeasurableSpace E]
[BorelSpace E]
(hf : AEMeasurable f μ)
{p : NNReal}
(hp : 0 < p)
:
MeasureTheory.eLpNorm f (↑p) μ ^ ↑p = ∫⁻ (t : ℝ) in Set.Ioi 0, ↑p * ENNReal.ofReal (t ^ (↑p - 1)) * MeasureTheory.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_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
[MeasurableSpace E]
[BorelSpace E]
(hf : AEMeasurable f μ)
{p : ℝ}
(hp : 0 < p)
:
MeasureTheory.eLpNorm f (ENNReal.ofReal p) μ = (ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, MeasureTheory.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_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
[MeasurableSpace E]
[BorelSpace E]
(hf : AEMeasurable f μ)
{p : ℝ}
(hp : -1 < p)
:
∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (t ^ p) * MeasureTheory.distribution f (ENNReal.ofReal t) μ = ENNReal.ofReal (p + 1)⁻¹ * ∫⁻ (x : α), ↑‖f x‖₊ ^ (p + 1) ∂μ
def
MeasureTheory.wnorm'
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
[NNNorm E]
(f : α → E)
(p : ℝ)
(μ : MeasureTheory.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'_le_eLpNorm'
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{p : ℝ}
(hp : 1 ≤ p)
:
MeasureTheory.wnorm' f p μ ≤ MeasureTheory.eLpNorm' f p μ
def
MeasureTheory.wnorm
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NNNorm E]
(f : α → E)
(p : ENNReal)
(μ : MeasureTheory.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_le_eLpNorm
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{p : ENNReal}
(hp : 1 ≤ p)
:
MeasureTheory.wnorm f p μ ≤ MeasureTheory.eLpNorm f p μ
def
MeasureTheory.MemWℒp
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NNNorm E]
(f : α → E)
(p : ENNReal)
(μ : MeasureTheory.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}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{p : ENNReal}
(hp : 1 ≤ p)
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.MemWℒp f p μ
def
MeasureTheory.HasWeakType
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_5}
{E₂ : Type u_6}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
(T : (α → E₁) → α' → E₂)
(p p' : ENNReal)
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.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.HasStrongType
{E : Type u_8}
{E' : Type u_9}
{α : Type u_10}
{α' : Type u_11}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → E) → α' → E')
(p p' : ENNReal)
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.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
{E : Type u_8}
{E' : Type u_9}
{α : Type u_10}
{α' : Type u_11}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
(T : (α → E) → α' → E')
(p p' : ENNReal)
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.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
theorem
MeasureTheory.HasStrongType.hasWeakType
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_5}
{E₂ : Type u_6}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{c : NNReal}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α'}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
{T : (α → E₁) → α' → E₂}
(hp' : 1 ≤ p')
(h : MeasureTheory.HasStrongType T p p' μ ν c)
:
MeasureTheory.HasWeakType T p p' μ ν c
theorem
MeasureTheory.HasStrongType.hasBoundedStrongType
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_5}
{E₂ : Type u_6}
{m : MeasurableSpace α}
{m✝ : MeasurableSpace α'}
{p p' : ENNReal}
{c : NNReal}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α'}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
{T : (α → E₁) → α' → E₂}
(h : MeasureTheory.HasStrongType T p p' μ ν c)
:
MeasureTheory.HasBoundedStrongType T p p' μ ν c
theorem
MeasureTheory.HasStrongType.const_smul
{𝕜 : Type u_8}
{E : Type u_9}
{E' : Type u_10}
{α : Type u_11}
{α' : Type u_12}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
{T : (α → E) → α' → E'}
{p p' : ENNReal}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α'}
{c : NNReal}
(h : MeasureTheory.HasStrongType T p p' μ ν c)
[NormedRing 𝕜]
[MulActionWithZero 𝕜 E']
[BoundedSMul 𝕜 E']
(k : 𝕜)
:
MeasureTheory.HasStrongType (k • T) p p' μ ν (‖k‖₊ * c)
theorem
MeasureTheory.HasStrongType.const_mul
{E : Type u_8}
{E' : Type u_9}
{α : Type u_10}
{α' : Type u_11}
[NormedAddCommGroup E]
[NormedRing E']
{_x : MeasurableSpace α}
{_x' : MeasurableSpace α'}
{T : (α → E) → α' → E'}
{p p' : ENNReal}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α'}
{c : NNReal}
(h : MeasureTheory.HasStrongType T p p' μ ν c)
(e : E')
:
MeasureTheory.HasStrongType (fun (f : α → E) (x : α') => e * T f x) p p' μ ν (‖e‖₊ * c)