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∞.

theorem Real.borel_eq_generateFrom_Ioo_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})

theorem Real.borel_eq_generateFrom_Iio_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Set.Iio ↑a})

theorem Real.borel_eq_generateFrom_Ioi_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Set.Ioi ↑a})

theorem Real.borel_eq_generateFrom_Iic_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Set.Iic ↑a})

theorem Real.borel_eq_generateFrom_Ici_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Set.Ici ↑a})

theorem Real.isPiSystem_Ioo_rat : IsPiSystem (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})

theorem Real.isPiSystem_Iio_rat : IsPiSystem (⋃ (a : ℚ), {Set.Iio ↑a})

theorem Real.isPiSystem_Ioi_rat : IsPiSystem (⋃ (a : ℚ), {Set.Ioi ↑a})

theorem Real.isPiSystem_Iic_rat : IsPiSystem (⋃ (a : ℚ), {Set.Iic ↑a})

theorem Real.isPiSystem_Ici_rat : IsPiSystem (⋃ (a : ℚ), {Set.Ici ↑a})

def Real.finiteSpanningSetsInIooRat (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure μ] : μ.FiniteSpanningSetsIn (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})

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

• One or more equations did not get rendered due to their size.

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 : Measurable Real.toNNReal

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 : Measurable NNReal.toReal

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 : Measurable ENNReal.ofNNReal

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]

theorem measurable_coe_nnreal_real_iff {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal} : (Measurable fun (x : α) => ↑(f x)) ↔ Measurable f

@[simp]

theorem aemeasurable_coe_nnreal_real_iff {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal} {μ : MeasureTheory.Measure α} : AEMeasurable (fun (x : α) => ↑(f x)) μ ↔ AEMeasurable f μ

def MeasurableEquiv.ennrealEquivNNReal : ↑{r : ENNReal | r ≠ ⊤} ≃ᵐ NNReal

The set of finite ℝ≥0∞ numbers is MeasurableEquiv to ℝ≥0.

Equations

• MeasurableEquiv.ennrealEquivNNReal = ENNReal.neTopHomeomorphNNReal.toMeasurableEquiv

theorem ENNReal.measurable_of_measurable_nnreal {α : Type u_1} {mα : MeasurableSpace α} {f : ENNReal → α} (h : Measurable fun (p : NNReal) => f ↑p) : Measurable f

def ENNReal.ennrealEquivSum : ENNReal ≃ᵐ NNReal ⊕ Unit

ℝ≥0∞ is MeasurableEquiv to ℝ≥0 ⊕ Unit.

Equations

• ENNReal.ennrealEquivSum = { toEquiv := Equiv.optionEquivSumPUnit NNReal, measurable_toFun := ENNReal.ennrealEquivSum._proof_1, measurable_invFun := ENNReal.ennrealEquivSum._proof_2 }

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)) : Measurable f

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, ⊤)) : Measurable f

theorem ENNReal.measurable_ofReal : Measurable ENNReal.ofReal

theorem ENNReal.measurable_toReal : Measurable ENNReal.toReal

theorem ENNReal.measurable_toNNReal : Measurable ENNReal.toNNReal

instance ENNReal.instMeasurableMul₂ : MeasurableMul₂ ENNReal

instance ENNReal.instMeasurableSub₂ : MeasurableSub₂ ENNReal

instance ENNReal.instMeasurableInv : MeasurableInv ENNReal

instance ENNReal.instMeasurableSMulNNReal : MeasurableSMul NNReal ENNReal

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)) : Measurable 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)) : Measurable 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} : (Measurable fun (x : α) => ↑(f x)) ↔ Measurable f

@[simp]

theorem aemeasurable_coe_nnreal_ennreal_iff {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal} {μ : MeasureTheory.Measure α} : AEMeasurable (fun (x : α) => ↑(f x)) μ ↔ AEMeasurable f μ

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 : Measurable Real.toEReal

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)) μ

def MeasurableEquiv.erealEquivReal : ↑{⊥, ⊤}ᶜ ≃ᵐ ℝ

The set of finite EReal numbers is MeasurableEquiv to ℝ.

Equations

• MeasurableEquiv.erealEquivReal = EReal.neBotTopHomeomorphReal.toMeasurableEquiv

theorem EReal.measurable_of_measurable_real {α : Type u_1} {mα : MeasurableSpace α} {f : EReal → α} (h : Measurable fun (p : ℝ) => f ↑p) : Measurable f

theorem measurable_ereal_toReal : Measurable EReal.toReal

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_ennreal_ereal : Measurable ENNReal.toEReal

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 : Measurable EReal.toENNReal

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) μ

instance NNReal.instMeasurableSMul₂ENNReal : MeasurableSMul₂ NNReal ENNReal

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)) : Measurable 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)) : Measurable g

A sequential limit of measurable ℝ≥0-valued functions is measurable.

theorem EReal.measurableEmbedding_coe : MeasurableEmbedding Real.toEReal

instance EReal.instMeasurableAdd₂ : MeasurableAdd₂ EReal

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)) : Measurable f

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, ⊤)) : Measurable f

instance EReal.instMeasurableMul₂ : MeasurableMul₂ EReal

theorem exists_spanning_measurableSet_le {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal} (hf : Measurable f) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ∃ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, f x ≤ ↑n) ∧ ⋃ (i : ℕ), s i = Set.univ

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 : ℝ) : Filter.Tendsto (fun (δ : ℝ) => μ (Set.Icc (b - δ) (b + δ))) (nhds 0) (nhds 0)