theorem
MeasureTheory.superlevelSet_zero_eq_support
{α : Type u_1}
{ε : Type u_12}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
:
theorem
MeasureTheory.nullMeasurableSet_superlevelSet
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{ε : Type u_12}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
:
NullMeasurableSet (superlevelSet f t) μ
theorem
MeasureTheory.measurableSet_superlevelSet
{α : Type u_1}
{m : MeasurableSpace α}
{t : ENNReal}
{ε : Type u_12}
[TopologicalSpace ε]
[ContinuousENorm ε]
[MeasurableSpace ε]
[OpensMeasurableSpace ε]
{f : α → ε}
(hf : Measurable f)
:
MeasurableSet (superlevelSet f t)
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.
Todo: rename to something more Mathlib-appropriate.
Instances For
theorem
MeasureTheory.distribution_eq_measure_superlevelSet
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
[ENorm ε]
{f : α → ε}
:
@[simp]
theorem
MeasureTheory.distibution_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(μ : Measure α)
:
theorem
MeasureTheory.distribution_mono_right
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{t s : ENNReal}
[ENorm ε]
{f : α → ε}
(h : t ≤ s)
:
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}
:
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₀
theorem
MeasureTheory.distribution_pow
{α : Type u_1}
{m : MeasurableSpace α}
(ε : Type u_12)
[SeminormedRing ε]
[NormOneClass ε]
[NormMulClass ε]
(f : α → ε)
(t : ENNReal)
(μ : Measure α)
{n : ℕ}
(hn : n ≠ 0)
:
theorem
MeasureTheory.distribution_eLpNormEssSup
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[ENorm ε]
{f : α → ε}
:
theorem
MeasureTheory.distribution_add_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t s : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f g : α → ε}
:
theorem
MeasureTheory.distribution_eq_zero_of_ae_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
(h : f =ᵐ[μ] 0)
:
@[simp]
theorem
MeasureTheory.distribution_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
:
theorem
MeasureTheory.distribution_zero_eq_measure_support
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_13}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
:
theorem
MeasureTheory.distribution_indicator_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{x : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
{X : Set α}
:
theorem
MeasureTheory.distribution_indicator_le_measure
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{x : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
{X : Set α}
:
theorem
MeasureTheory.distribution_indicator_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{s : Set α}
{a : ε}
:
distribution (s.indicator (Function.const α a)) t μ = (Set.Iio ‖a‖ₑ).indicator (fun (x : ENNReal) => μ s) t
theorem
MeasureTheory.distribution_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{a : ε}
:
distribution (Function.const α a) t μ = (Set.Iio ‖a‖ₑ).indicator (fun (x : ENNReal) => μ Set.univ) t
theorem
MeasureTheory.distribution_indicator_superlevelSet
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{x : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
:
theorem
MeasureTheory.distribution_indicator_superlevelSet_compl
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{x : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
(hf : AEStronglyMeasurable f μ)
{t : ENNReal}
(ht : distribution f t μ ≠ ⊤)
:
theorem
MeasureTheory.distribution_eq_zero_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
:
theorem
MeasureTheory.support_distribution
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_13}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
:
theorem
MeasureTheory.distribution_add
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f g : α → ε}
(h : Disjoint (Function.support f) (Function.support g))
(hg : AEStronglyMeasurable g μ)
:
theorem
MeasureTheory.distribution_indicator_add_of_support_subset
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{ε : Type u_13}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
(enorm_add : ∀ (a b : ε), ‖a + b‖ₑ = ‖a‖ₑ + ‖b‖ₑ)
{f : α → ε}
{c : ε}
(hc : ‖c‖ₑ ≠ ⊤)
{s : Set α}
(hfs : Function.support f ⊆ s)
:
distribution (f + s.indicator (Function.const α c)) t μ = if t < ‖c‖ₑ then μ s else distribution f (t - ‖c‖ₑ) μ
theorem
MeasureTheory.distribution_indicator_add_of_support_subset_ennreal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{f : α → ENNReal}
{c : ENNReal}
(hc : c ≠ ⊤)
{s : Set α}
(hfs : Function.support f ⊆ s)
:
distribution (f + s.indicator (Function.const α c)) t μ = if t < c then μ s else distribution f (t - c) μ
theorem
MeasureTheory.distribution_indicator_add_of_support_subset_nnreal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{f : α → NNReal}
{c : NNReal}
{s : Set α}
(hfs : Function.support f ⊆ s)
:
distribution (f + s.indicator (Function.const α c)) t μ = if t < ↑c then μ s else distribution f (t - ↑c) μ
theorem
MeasureTheory.distribution_eq_distribution_prod
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_14}
[ENorm ε]
{f : α → ε}
{t : ENNReal}
{β : Type u_13}
{m' : MeasurableSpace β}
{ν : Measure β}
[IsProbabilityMeasure ν]
:
theorem
MeasureTheory.distribution_le_mul_pow_eLpNorm_enorm
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε' : Type u_13}
[TopologicalSpace ε']
[ContinuousENorm ε']
{p : ENNReal}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{f : α → ε'}
(hf : AEStronglyMeasurable f μ)
{ε : ENNReal}
(hε : ε ≠ 0)
(hmeas_top : ε = ⊤ → μ {x : α | ‖f x‖ₑ = ⊤} = 0)
:
The constant used in C_distribution_le_of_eLpNorm_le.
Equations
- MeasureTheory.C_distribution_le_of_eLpNorm_le δ ε p = δ * ε ^ (↑p)⁻¹
Instances For
theorem
MeasureTheory.C_distribution_le_of_eLpNorm_le_pos
{δ ε p : NNReal}
(δpos : 0 < δ)
(εpos : 0 < ε)
:
theorem
MeasureTheory.distribution_le_of_eLpNorm_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε' : Type u_13}
[TopologicalSpace ε']
[ContinuousENorm ε']
{δ ε p : NNReal}
(δpos : 0 < δ)
(p_pos : 0 < p)
{f : α → ε'}
(meas_f : AEStronglyMeasurable f μ)
(hf : eLpNorm f (↑p) μ ≤ ↑(C_distribution_le_of_eLpNorm_le δ ε p))
: