The distribution function d_f #
def
MeasureTheory.distribution
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
[NNNorm E]
(f : α → E)
(t : ENNReal)
(μ : MeasureTheory.Measure α)
:
The distribution function d_f 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_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{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_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{t : ENNReal}
{s : ENNReal}
(h : t ≤ s)
:
MeasureTheory.distribution f s μ ≤ MeasureTheory.distribution f t μ
theorem
MeasureTheory.distribution_mono
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
{t : ENNReal}
{s : ENNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
(h : t ≤ s)
:
MeasureTheory.distribution f s μ ≤ MeasureTheory.distribution g t μ
theorem
MeasureTheory.distribution_smul_left
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{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.distribution_add_le
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
{t : ENNReal}
{s : ENNReal}
:
MeasureTheory.distribution (f + g) (t + s) μ ≤ MeasureTheory.distribution f t μ + MeasureTheory.distribution g s μ
theorem
ContinuousLinearMap.distribution_le
{α : Type u_1}
{𝕜 : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{E₃ : Type u_6}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[NormedAddCommGroup E₃]
[NormedSpace 𝕜 E₃]
(L : E₁ →L[𝕜] E₂ →L[𝕜] E₃)
{t : ENNReal}
{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
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{p : ℝ}
(hp : 1 ≤ p)
:
∫⁻ (x : α), ↑‖f x‖₊ ^ p ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (p * t ^ (p - 1)) * MeasureTheory.distribution f (ENNReal.ofReal t) μ
Decreasing rearrangements f^# #
def
MeasureTheory.rearrangement
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
[NNNorm E]
(f : α → E)
(x : ENNReal)
(μ : MeasureTheory.Measure α)
:
The decreasing rearrangement function f^#. It equals μ univ for negative x.
Note that unlike the notes, we also define this for x = ∞.
To do: we should also be able to use this for functions with codomain ℝ≥0∞.
Equations
- MeasureTheory.rearrangement f x μ = sInf {s : ENNReal | MeasureTheory.distribution f s μ ≤ x}
Instances For
theorem
MeasureTheory.rearrangement_mono_right
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{x : ENNReal}
{y : ENNReal}
(h : x ≤ y)
:
MeasureTheory.rearrangement f y μ ≤ MeasureTheory.rearrangement f x μ
theorem
MeasureTheory.rearrangement_mono_left
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
{x : ENNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
:
MeasureTheory.rearrangement f x μ ≤ MeasureTheory.rearrangement g x μ
theorem
MeasureTheory.rearrangement_mono
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
{x : ENNReal}
{y : ENNReal}
(h1 : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖)
(h2 : x ≤ y)
:
MeasureTheory.rearrangement f y μ ≤ MeasureTheory.rearrangement g x μ
theorem
MeasureTheory.rearrangement_smul_left
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{f : α → E}
{x : ENNReal}
(c : 𝕜)
:
MeasureTheory.rearrangement (c • f) x μ = ↑‖c‖₊ * MeasureTheory.rearrangement f x μ
theorem
MeasureTheory.rearrangement_distribution_le
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{t : ENNReal}
:
MeasureTheory.rearrangement f (MeasureTheory.distribution f t μ) μ ≤ t
theorem
MeasureTheory.distribution_rearrangement_le
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{x : ENNReal}
:
MeasureTheory.distribution f (MeasureTheory.rearrangement f x μ) μ ≤ x
theorem
MeasureTheory.rearrangement_add_le
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
{x : ENNReal}
{y : ENNReal}
(c : 𝕜)
:
MeasureTheory.rearrangement (f + g) (x + y) μ ≤ MeasureTheory.rearrangement f x μ + MeasureTheory.rearrangement g y μ
theorem
ContinuousLinearMap.rearrangement_le
{α : Type u_1}
{𝕜 : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{E₃ : Type u_6}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E₁]
[NormedSpace 𝕜 E₁]
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₂]
[NormedAddCommGroup E₃]
[NormedSpace 𝕜 E₃]
(L : E₁ →L[𝕜] E₂ →L[𝕜] E₃)
{x : ENNReal}
{y : ENNReal}
{f : α → E₁}
{g : α → E₂}
:
MeasureTheory.rearrangement (fun (x : α) => (L (f x)) (g x)) (↑‖L‖₊ * x * y) μ ≤ MeasureTheory.rearrangement f x μ + MeasureTheory.rearrangement g y μ
theorem
MeasureTheory.lt_rearrangement_iff
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
{s : ENNReal}
{x : ENNReal}
(hf : Measurable f)
:
s < MeasureTheory.rearrangement f x μ ↔ x < MeasureTheory.distribution f s μ
theorem
MeasureTheory.continuousWithinAt_rearrangement
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
(hf : Measurable f)
(x : ENNReal)
:
ContinuousWithinAt (fun (x : ENNReal) => MeasureTheory.rearrangement f x μ) (Set.Ici x) x
theorem
MeasureTheory.volume_lt_rearrangement
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
(hf : Measurable f)
(s : ENNReal)
:
MeasureTheory.volume {x : ℝ | s < MeasureTheory.rearrangement f (ENNReal.ofReal x) μ} = MeasureTheory.distribution f s μ
theorem
MeasureTheory.lintegral_rearrangement_pow
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
(hf : Measurable f)
{p : ℝ}
(hp : 1 ≤ p)
:
∫⁻ (t : ℝ), MeasureTheory.rearrangement f (ENNReal.ofReal t) μ ^ p = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
theorem
MeasureTheory.sSup_rearrangement
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
(hf : Measurable f)
:
⨆ (t : ENNReal), ⨆ (_ : t > 0), MeasureTheory.rearrangement f t μ = MeasureTheory.rearrangement f 0 μ
theorem
MeasureTheory.essSup_nnnorm_eq_rearrangement_zero
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
(hf : Measurable f)
:
↑(essSup (fun (x : α) => ‖f x‖₊) μ) = MeasureTheory.rearrangement f 0 μ
theorem
MeasureTheory.tendsto_rearrangement
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
{s : ℕ → α → E}
(hs : ∀ᶠ (i : ℕ) in Filter.atTop, Measurable (s i))
(hf : Measurable f)
(h2s : ∀ᵐ (x : α) ∂μ, Monotone fun (n : ℕ) => ‖s n x‖)
(h : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (x_1 : ℕ) => ‖s x_1 x‖) Filter.atTop (nhds ‖f x‖))
:
Filter.Tendsto s Filter.atTop (nhds f)
theorem
MeasureTheory.liminf_rearrangement
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
{x : ENNReal}
{s : ℕ → α → E}
(hs : ∀ᶠ (i : ℕ) in Filter.atTop, Measurable (s i))
(hf : Measurable f)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ Filter.liminf (fun (x_1 : ℕ) => ‖s x_1 x‖) Filter.atTop)
:
MeasureTheory.rearrangement f x μ ≤ Filter.liminf (fun (i : ℕ) => MeasureTheory.rearrangement (s i) x μ) Filter.atTop
theorem
MeasureTheory.distribution_indicator_le_distribution
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
(hf : Measurable f)
{X : Set α}
(hX : MeasurableSet X)
(t : ENNReal)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.distribution (X.indicator f) t μ ≤ MeasureTheory.distribution f t μ
theorem
MeasureTheory.distribution_indicator_le_measure
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
(hf : Measurable f)
{X : Set α}
(hX : MeasurableSet X)
(t : ENNReal)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.distribution (X.indicator f) t μ ≤ μ X
theorem
MeasureTheory.rearrangement_indicator_le'
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
(hf : Measurable f)
{X : Set α}
(hX : MeasurableSet X)
(t : ENNReal)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.rearrangement (X.indicator f) t μ ≤ (Set.Iio (μ X)).indicator (fun (x : ENNReal) => MeasureTheory.rearrangement f x μ) t
Version of rearrangement_indicator_le for t : ℝ≥0∞
theorem
MeasureTheory.rearrangement_indicator_le
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
(hf : Measurable f)
{X : Set α}
(hX : MeasurableSet X)
(t : ℝ)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.rearrangement (X.indicator f) (ENNReal.ofReal t) μ ≤ (μ X).Ico.indicator (fun (x : ℝ) => MeasureTheory.rearrangement f (ENNReal.ofReal x) μ) t
theorem
MeasureTheory.integral_norm_le_integral_rearrangement
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[MeasurableSpace E]
{f : α → E}
(hf : Measurable f)
{X : Set α}
(hX : MeasurableSet X)
(μ : MeasureTheory.Measure α)
:
∫⁻ (x : α), ↑‖f x‖₊ ∂μ ≤ ∫⁻ (t : ℝ) in (μ X).Ico, MeasureTheory.rearrangement f (ENNReal.ofReal t) μ
theorem
MeasureTheory.lintegral_norm_mul_le_lintegral_rearrangement_mul
{α : Type u_1}
{𝕜 : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NontriviallyNormedField 𝕜]
{f : α → 𝕜}
{g : α → 𝕜}
:
∫⁻ (x : α), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (t : ℝ), MeasureTheory.rearrangement f (ENNReal.ofReal t) μ * MeasureTheory.rearrangement g (ENNReal.ofReal t) μ
The Hardy-Littlewood rearrangement inequality, for functions into 𝕜
def
MeasureTheory.lnorm'
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
(f : α → E)
(p : ENNReal)
(q : ℝ)
(μ : MeasureTheory.Measure α)
:
The norm corresponding to the Lorentz space L^{p,q} for 1 ≤ p ≤ ∞ and 1 ≤ q < ∞.
Equations
- MeasureTheory.lnorm' f p q μ = ∫⁻ (t : ℝ), (ENNReal.ofReal (t ^ p⁻¹.toReal) * MeasureTheory.rearrangement f (ENNReal.ofReal t) μ) ^ q⁻¹ / ENNReal.ofReal t
Instances For
def
MeasureTheory.lnorm
{α : Type u_1}
{E : Type u_3}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
(f : α → E)
(p : ENNReal)
(q : ENNReal)
(μ : MeasureTheory.Measure α)
:
The norm corresponding to the Lorentz space L^{p,q} for 1 ≤ p ≤ ∞ and 1 ≤ q ≤ ∞.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.Lorentz
{α : Type u_8}
(E : Type u_7)
{m : MeasurableSpace α}
[NormedAddCommGroup E]
(p : ENNReal)
(q : ENNReal)
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
AddSubgroup (α →ₘ[μ] E)
the Lorentz space L^{p,q}
Equations
- MeasureTheory.Lorentz E p q μ = { carrier := {f : α →ₘ[μ] E | MeasureTheory.lnorm (↑f) p q μ < ⊤}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }