Borel (measurable) spaces ℝ, ℝ≥0, ℝ≥0∞ #
Main statements #
borel_eq_generateFrom_Ixx_rat(where Ixx is one of {Ioo, Ioi, Iio, Ici, Iic): the Borel sigma algebra on ℝ is generated by intervals with rational endpoints;isPiSystem_Ixx_rat(where Ixx is one of {Ioo, Ioi, Iio, Ici, Iic): intervals with rational endpoints form a pi system on ℝ;measurable_real_toNNReal,measurable_coe_nnreal_real,measurable_coe_nnreal_ennreal,ENNReal.measurable_ofReal,ENNReal.measurable_toReal: measurability of various coercions between ℝ, ℝ≥0, and ℝ≥0∞;Measurable.real_toNNReal,Measurable.coe_nnreal_real,Measurable.coe_nnreal_ennreal,Measurable.ennreal_ofReal,Measurable.ennreal_toNNReal,Measurable.ennreal_toReal: measurability of functions composed with various coercions between ℝ, ℝ≥0, and ℝ≥0∞ (also similar results for a.e.-measurability);Measurable.ennreal*: measurability of special cases for arithmetic operations onℝ≥0∞.
def
Real.finiteSpanningSetsInIooRat
(μ : MeasureTheory.Measure ℝ)
[MeasureTheory.IsLocallyFiniteMeasure μ]
:
The intervals (-(n + 1), (n + 1)) form a finite spanning sets in the set of open intervals
with rational endpoints for a locally finite measure μ on ℝ.
Equations
Instances For
theorem
Real.measure_ext_Ioo_rat
{μ ν : MeasureTheory.Measure ℝ}
[MeasureTheory.IsLocallyFiniteMeasure μ]
(h : ∀ (a b : ℚ), μ (Set.Ioo ↑a ↑b) = ν (Set.Ioo ↑a ↑b))
:
theorem
Measurable.real_toNNReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℝ}
(hf : Measurable f)
:
Measurable fun (x : α) => (f x).toNNReal
theorem
AEMeasurable.real_toNNReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℝ}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => (f x).toNNReal) μ
theorem
Measurable.coe_nnreal_real
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → NNReal}
(hf : Measurable f)
:
Measurable fun (x : α) => ↑(f x)
theorem
AEMeasurable.coe_nnreal_real
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → NNReal}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => ↑(f x)) μ
theorem
Measurable.coe_nnreal_ennreal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → NNReal}
(hf : Measurable f)
:
Measurable fun (x : α) => ↑(f x)
theorem
AEMeasurable.coe_nnreal_ennreal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → NNReal}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => ↑(f x)) μ
theorem
Measurable.ennreal_ofReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℝ}
(hf : Measurable f)
:
Measurable fun (x : α) => ENNReal.ofReal (f x)
theorem
AEMeasurable.ennreal_ofReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℝ}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => ENNReal.ofReal (f x)) μ
@[simp]
@[simp]
theorem
aemeasurable_coe_nnreal_real_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → NNReal}
{μ : MeasureTheory.Measure α}
:
theorem
ENNReal.measurable_of_measurable_nnreal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : ENNReal → α}
(h : Measurable fun (p : NNReal) => f ↑p)
:
theorem
ENNReal.measurable_of_measurable_nnreal_prod
{β : Type u_2}
{γ : Type u_3}
{x✝ : MeasurableSpace β}
{x✝¹ : MeasurableSpace γ}
{f : ENNReal × β → γ}
(H₁ : Measurable fun (p : NNReal × β) => f (↑p.1, p.2))
(H₂ : Measurable fun (x : β) => f (⊤, x))
:
theorem
ENNReal.measurable_of_measurable_nnreal_nnreal
{β : Type u_2}
{x✝ : MeasurableSpace β}
{f : ENNReal × ENNReal → β}
(h₁ : Measurable fun (p : NNReal × NNReal) => f (↑p.1, ↑p.2))
(h₂ : Measurable fun (r : NNReal) => f (⊤, ↑r))
(h₃ : Measurable fun (r : NNReal) => f (↑r, ⊤))
:
theorem
ENNReal.measurable_of_tendsto'
{α : Type u_1}
{mα : MeasurableSpace α}
{ι : Type u_5}
{f : ι → α → ENNReal}
{g : α → ENNReal}
(u : Filter ι)
[u.NeBot]
[u.IsCountablyGenerated]
(hf : ∀ (i : ι), Measurable (f i))
(lim : Filter.Tendsto f u (nhds g))
:
A limit (over a general filter) of measurable ℝ≥0∞ valued functions is measurable.
theorem
ENNReal.measurable_of_tendsto
{α : Type u_1}
{mα : MeasurableSpace α}
{f : ℕ → α → ENNReal}
{g : α → ENNReal}
(hf : ∀ (i : ℕ), Measurable (f i))
(lim : Filter.Tendsto f Filter.atTop (nhds g))
:
A sequential limit of measurable ℝ≥0∞ valued functions is measurable.
theorem
ENNReal.aemeasurable_of_tendsto'
{α : Type u_1}
{mα : MeasurableSpace α}
{ι : Type u_5}
{f : ι → α → ENNReal}
{g : α → ENNReal}
{μ : MeasureTheory.Measure α}
(u : Filter ι)
[u.NeBot]
[u.IsCountablyGenerated]
(hf : ∀ (i : ι), AEMeasurable (f i) μ)
(hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ι) => f i a) u (nhds (g a)))
:
AEMeasurable g μ
A limit (over a general filter) of a.e.-measurable ℝ≥0∞ valued functions is
a.e.-measurable.
theorem
ENNReal.aemeasurable_of_tendsto
{α : Type u_1}
{mα : MeasurableSpace α}
{f : ℕ → α → ENNReal}
{g : α → ENNReal}
{μ : MeasureTheory.Measure α}
(hf : ∀ (i : ℕ), AEMeasurable (f i) μ)
(hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ℕ) => f i a) Filter.atTop (nhds (g a)))
:
AEMeasurable g μ
A limit of a.e.-measurable ℝ≥0∞ valued functions is a.e.-measurable.
theorem
Measurable.ennreal_toNNReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ENNReal}
(hf : Measurable f)
:
Measurable fun (x : α) => (f x).toNNReal
theorem
AEMeasurable.ennreal_toNNReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ENNReal}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => (f x).toNNReal) μ
@[simp]
theorem
measurable_coe_nnreal_ennreal_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → NNReal}
:
@[simp]
theorem
aemeasurable_coe_nnreal_ennreal_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → NNReal}
{μ : MeasureTheory.Measure α}
:
theorem
Measurable.ennreal_toReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ENNReal}
(hf : Measurable f)
:
Measurable fun (x : α) => (f x).toReal
theorem
AEMeasurable.ennreal_toReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ENNReal}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => (f x).toReal) μ
theorem
Measurable.ennreal_tsum
{α : Type u_1}
{mα : MeasurableSpace α}
{ι : Type u_5}
[Countable ι]
{f : ι → α → ENNReal}
(h : ∀ (i : ι), Measurable (f i))
:
Measurable fun (x : α) => ∑' (i : ι), f i x
note: ℝ≥0∞ can probably be generalized in a future version of this lemma.
theorem
Measurable.ennreal_tsum'
{α : Type u_1}
{mα : MeasurableSpace α}
{ι : Type u_5}
[Countable ι]
{f : ι → α → ENNReal}
(h : ∀ (i : ι), Measurable (f i))
:
Measurable (∑' (i : ι), f i)
theorem
Measurable.nnreal_tsum
{α : Type u_1}
{mα : MeasurableSpace α}
{ι : Type u_5}
[Countable ι]
{f : ι → α → NNReal}
(h : ∀ (i : ι), Measurable (f i))
:
Measurable fun (x : α) => ∑' (i : ι), f i x
theorem
AEMeasurable.ennreal_tsum
{α : Type u_1}
{mα : MeasurableSpace α}
{ι : Type u_5}
[Countable ι]
{f : ι → α → ENNReal}
{μ : MeasureTheory.Measure α}
(h : ∀ (i : ι), AEMeasurable (f i) μ)
:
AEMeasurable (fun (x : α) => ∑' (i : ι), f i x) μ
theorem
AEMeasurable.nnreal_tsum
{α : Type u_5}
{x✝ : MeasurableSpace α}
{ι : Type u_6}
[Countable ι]
{f : ι → α → NNReal}
{μ : MeasureTheory.Measure α}
(h : ∀ (i : ι), AEMeasurable (f i) μ)
:
AEMeasurable (fun (x : α) => ∑' (i : ι), f i x) μ
theorem
Measurable.coe_real_ereal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℝ}
(hf : Measurable f)
:
Measurable fun (x : α) => ↑(f x)
theorem
AEMeasurable.coe_real_ereal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℝ}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => ↑(f x)) μ
theorem
EReal.measurable_of_measurable_real
{α : Type u_1}
{mα : MeasurableSpace α}
{f : EReal → α}
(h : Measurable fun (p : ℝ) => f ↑p)
:
theorem
Measurable.ereal_toReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → EReal}
(hf : Measurable f)
:
Measurable fun (x : α) => (f x).toReal
theorem
AEMeasurable.ereal_toReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → EReal}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => (f x).toReal) μ
theorem
Measurable.coe_ereal_ennreal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ENNReal}
(hf : Measurable f)
:
Measurable fun (x : α) => ↑(f x)
theorem
AEMeasurable.coe_ereal_ennreal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ENNReal}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => ↑(f x)) μ
theorem
Measurable.ereal_toENNReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → EReal}
(hf : Measurable f)
:
Measurable fun (x : α) => (f x).toENNReal
theorem
AEMeasurable.ereal_toENNReal
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → EReal}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => (f x).toENNReal) μ
theorem
NNReal.measurable_of_tendsto'
{α : Type u_1}
{mα : MeasurableSpace α}
{ι : Type u_5}
{f : ι → α → NNReal}
{g : α → NNReal}
(u : Filter ι)
[u.NeBot]
[u.IsCountablyGenerated]
(hf : ∀ (i : ι), Measurable (f i))
(lim : Filter.Tendsto f u (nhds g))
:
A limit (over a general filter) of measurable ℝ≥0 valued functions is measurable.
theorem
NNReal.measurable_of_tendsto
{α : Type u_1}
{mα : MeasurableSpace α}
{f : ℕ → α → NNReal}
{g : α → NNReal}
(hf : ∀ (i : ℕ), Measurable (f i))
(lim : Filter.Tendsto f Filter.atTop (nhds g))
:
A sequential limit of measurable ℝ≥0 valued functions is measurable.
theorem
EReal.measurable_of_real_prod
{β : Type u_6}
{γ : Type u_7}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{f : EReal × β → γ}
(h_real : Measurable fun (p : ℝ × β) => f (↑p.1, p.2))
(h_bot : Measurable fun (x : β) => f (⊥, x))
(h_top : Measurable fun (x : β) => f (⊤, x))
:
theorem
EReal.measurable_of_real_real
{β : Type u_6}
{mβ : MeasurableSpace β}
{f : EReal × EReal → β}
(h_real : Measurable fun (p : ℝ × ℝ) => f (↑p.1, ↑p.2))
(h_bot_left : Measurable fun (r : ℝ) => f (⊥, ↑r))
(h_top_left : Measurable fun (r : ℝ) => f (⊤, ↑r))
(h_bot_right : Measurable fun (r : ℝ) => f (↑r, ⊥))
(h_top_right : Measurable fun (r : ℝ) => f (↑r, ⊤))
:
theorem
exists_spanning_measurableSet_le
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → NNReal}
(hf : Measurable f)
(μ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
:
If a function f : α → ℝ≥0 is measurable and the measure is σ-finite, then there exists
spanning measurable sets with finite measure on which f is bounded.
See also StronglyMeasurable.exists_spanning_measurableSet_norm_le for functions into normed
groups.
theorem
tendsto_measure_Icc_nhdsWithin_right'
(μ : MeasureTheory.Measure ℝ)
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
(b : ℝ)
:
Filter.Tendsto (fun (δ : ℝ) => μ (Set.Icc (b - δ) (b + δ))) (nhdsWithin 0 (Set.Ioi 0)) (nhds (μ {b}))
theorem
tendsto_measure_Icc_nhdsWithin_right
(μ : MeasureTheory.Measure ℝ)
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
(b : ℝ)
:
Filter.Tendsto (fun (δ : ℝ) => μ (Set.Icc (b - δ) (b + δ))) (nhdsWithin 0 (Set.Ici 0)) (nhds (μ {b}))
theorem
tendsto_measure_Icc
(μ : MeasureTheory.Measure ℝ)
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
[MeasureTheory.NoAtoms μ]
(b : ℝ)
: