# Borel sigma algebras on spaces with orders #

## Main statements #

• borel_eq_generateFrom_Ixx (where Ixx is one of {Iio, Ioi, Iic, Ici, Ico, Ioc}): The Borel sigma algebra of a linear order topology is generated by intervals of the given kind.
• Dense.borel_eq_generateFrom_Ico_mem, Dense.borel_eq_generateFrom_Ioc_mem: The Borel sigma algebra of a dense linear order topology is generated by intervals of a given kind, with endpoints from dense subsets.
• ext_of_Ico, ext_of_Ioc: A locally finite Borel measure on a second countable conditionally complete linear order is characterized by the measures of intervals of the given kind.
• ext_of_Iic, ext_of_Ici: A finite Borel measure on a second countable linear order is characterized by the measures of intervals of the given kind.
• UpperSemicontinuous.measurable, LowerSemicontinuous.measurable: Semicontinuous functions are measurable.
• measurable_iSup, measurable_iInf, measurable_sSup, measurable_sInf: Countable supremums and infimums of measurable functions to conditionally complete linear orders are measurable.
• measurable_liminf, measurable_limsup: Countable liminfs and limsups of measurable functions to conditionally complete linear orders are measurable.
@[simp]
theorem measurableSet_Ici {α : Type u_1} [] [] [] {a : α} :
@[simp]
theorem measurableSet_Iic {α : Type u_1} [] [] [] {a : α} :
@[simp]
theorem measurableSet_Icc {α : Type u_1} [] [] [] {a : α} {b : α} :
instance nhdsWithin_Ici_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} :
(nhdsWithin a ()).IsMeasurablyGenerated
Equations
• =
instance nhdsWithin_Iic_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} :
(nhdsWithin a ()).IsMeasurablyGenerated
Equations
• =
instance nhdsWithin_Icc_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} {x : α} :
(nhdsWithin x (Set.Icc a b)).IsMeasurablyGenerated
Equations
• =
instance atTop_isMeasurablyGenerated {α : Type u_1} [] [] [] :
Filter.atTop.IsMeasurablyGenerated
Equations
• =
instance atBot_isMeasurablyGenerated {α : Type u_1} [] [] [] :
Filter.atBot.IsMeasurablyGenerated
Equations
• =
instance instIsMeasurablyGeneratedCocompactOfR1Space {α : Type u_1} [] [] [] :
().IsMeasurablyGenerated
Equations
• =
theorem measurableSet_le' {α : Type u_1} [] [] [] :
MeasurableSet {p : α × α | p.1 p.2}
theorem measurableSet_le {α : Type u_1} {δ : Type u_4} [] [] [] [] {f : δα} {g : δα} (hf : ) (hg : ) :
MeasurableSet {a : δ | f a g a}
@[simp]
theorem measurableSet_Iio {α : Type u_1} [] [] [] {a : α} :
@[simp]
theorem measurableSet_Ioi {α : Type u_1} [] [] [] {a : α} :
@[simp]
theorem measurableSet_Ioo {α : Type u_1} [] [] [] {a : α} {b : α} :
@[simp]
theorem measurableSet_Ioc {α : Type u_1} [] [] [] {a : α} {b : α} :
@[simp]
theorem measurableSet_Ico {α : Type u_1} [] [] [] {a : α} {b : α} :
instance nhdsWithin_Ioi_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} :
(nhdsWithin a ()).IsMeasurablyGenerated
Equations
• =
instance nhdsWithin_Iio_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} :
(nhdsWithin a ()).IsMeasurablyGenerated
Equations
• =
instance nhdsWithin_uIcc_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} {x : α} :
(nhdsWithin x (Set.uIcc a b)).IsMeasurablyGenerated
Equations
• =
theorem measurableSet_lt' {α : Type u_1} [] [] [] :
MeasurableSet {p : α × α | p.1 < p.2}
theorem measurableSet_lt {α : Type u_1} {δ : Type u_4} [] [] [] [] {f : δα} {g : δα} (hf : ) (hg : ) :
MeasurableSet {a : δ | f a < g a}
theorem nullMeasurableSet_lt {α : Type u_1} {δ : Type u_4} [] [] [] [] {μ : } {f : δα} {g : δα} (hf : ) (hg : ) :
MeasureTheory.NullMeasurableSet {a : δ | f a < g a} μ
theorem nullMeasurableSet_lt' {α : Type u_1} [] [] [] {μ : MeasureTheory.Measure (α × α)} :
MeasureTheory.NullMeasurableSet {p : α × α | p.1 < p.2} μ
theorem nullMeasurableSet_le {α : Type u_1} {δ : Type u_4} [] [] [] [] {μ : } {f : δα} {g : δα} (hf : ) (hg : ) :
MeasureTheory.NullMeasurableSet {a : δ | f a g a} μ
theorem Set.OrdConnected.measurableSet {α : Type u_1} {s : Set α} [] [] [] (h : s.OrdConnected) :
theorem IsPreconnected.measurableSet {α : Type u_1} {s : Set α} [] [] [] (h : ) :
theorem generateFrom_Ico_mem_le_borel {α : Type u_5} [] [] (s : Set α) (t : Set α) :
MeasurableSpace.generateFrom {S : Set α | ls, ut, l < u Set.Ico l u = S}
theorem Dense.borel_eq_generateFrom_Ico_mem_aux {α : Type u_5} [] [] [] {s : Set α} (hd : ) (hbot : ∀ (x : α), x s) (hIoo : ∀ (x y : α), x < ySet.Ioo x y = y s) :
= MeasurableSpace.generateFrom {S : Set α | ls, us, l < u Set.Ico l u = S}
theorem Dense.borel_eq_generateFrom_Ico_mem {α : Type u_5} [] [] [] [] [] {s : Set α} (hd : ) :
= MeasurableSpace.generateFrom {S : Set α | ls, us, l < u Set.Ico l u = S}
theorem borel_eq_generateFrom_Ico (α : Type u_5) [] [] [] :
= MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u Set.Ico l u = S}
theorem Dense.borel_eq_generateFrom_Ioc_mem_aux {α : Type u_5} [] [] [] {s : Set α} (hd : ) (hbot : ∀ (x : α), x s) (hIoo : ∀ (x y : α), x < ySet.Ioo x y = x s) :
= MeasurableSpace.generateFrom {S : Set α | ls, us, l < u Set.Ioc l u = S}
theorem Dense.borel_eq_generateFrom_Ioc_mem {α : Type u_5} [] [] [] [] [] {s : Set α} (hd : ) :
= MeasurableSpace.generateFrom {S : Set α | ls, us, l < u Set.Ioc l u = S}
theorem borel_eq_generateFrom_Ioc (α : Type u_5) [] [] [] :
= MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u Set.Ioc l u = S}
theorem MeasureTheory.Measure.ext_of_Ico_finite {α : Type u_5} [] {m : } [] [] [] (μ : ) (ν : ) (hμν : μ Set.univ = ν Set.univ) (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ico a b) = ν (Set.Ico a b)) :
μ = ν

Two finite measures on a Borel space are equal if they agree on all closed-open intervals. If α is a conditionally complete linear order with no top element, MeasureTheory.Measure.ext_of_Ico is an extensionality lemma with weaker assumptions on μ and ν.

theorem MeasureTheory.Measure.ext_of_Ioc_finite {α : Type u_5} [] {m : } [] [] [] (μ : ) (ν : ) (hμν : μ Set.univ = ν Set.univ) (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ioc a b) = ν (Set.Ioc a b)) :
μ = ν

Two finite measures on a Borel space are equal if they agree on all open-closed intervals. If α is a conditionally complete linear order with no top element, MeasureTheory.Measure.ext_of_Ioc is an extensionality lemma with weaker assumptions on μ and ν.

theorem MeasureTheory.Measure.ext_of_Ico' {α : Type u_5} [] {m : } [] [] [] [] (μ : ) (ν : ) (hμ : ∀ ⦃a b : α⦄, a < bμ (Set.Ico a b) ) (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ico a b) = ν (Set.Ico a b)) :
μ = ν

Two measures which are finite on closed-open intervals are equal if they agree on all closed-open intervals.

theorem MeasureTheory.Measure.ext_of_Ioc' {α : Type u_5} [] {m : } [] [] [] [] (μ : ) (ν : ) (hμ : ∀ ⦃a b : α⦄, a < bμ (Set.Ioc a b) ) (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ioc a b) = ν (Set.Ioc a b)) :
μ = ν

Two measures which are finite on closed-open intervals are equal if they agree on all open-closed intervals.

theorem MeasureTheory.Measure.ext_of_Ico {α : Type u_5} [] {_m : } [] [] [] (μ : ) (ν : ) (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ico a b) = ν (Set.Ico a b)) :
μ = ν

Two measures which are finite on closed-open intervals are equal if they agree on all closed-open intervals.

theorem MeasureTheory.Measure.ext_of_Ioc {α : Type u_5} [] {_m : } [] [] [] (μ : ) (ν : ) (h : ∀ ⦃a b : α⦄, a < bμ (Set.Ioc a b) = ν (Set.Ioc a b)) :
μ = ν

Two measures which are finite on closed-open intervals are equal if they agree on all open-closed intervals.

theorem MeasureTheory.Measure.ext_of_Iic {α : Type u_5} [] {m : } [] [] [] (μ : ) (ν : ) (h : ∀ (a : α), μ () = ν ()) :
μ = ν

Two finite measures on a Borel space are equal if they agree on all left-infinite right-closed intervals.

theorem MeasureTheory.Measure.ext_of_Ici {α : Type u_5} [] {m : } [] [] [] (μ : ) (ν : ) (h : ∀ (a : α), μ () = ν ()) :
μ = ν

Two finite measures on a Borel space are equal if they agree on all left-closed right-infinite intervals.

theorem measurableSet_uIcc {α : Type u_1} [] [] [] {a : α} {b : α} :
theorem measurableSet_uIoc {α : Type u_1} [] [] [] {a : α} {b : α} :
theorem Measurable.max {α : Type u_1} {δ : Type u_4} [] [] [] [] {f : δα} {g : δα} (hf : ) (hg : ) :
Measurable fun (a : δ) => max (f a) (g a)
theorem AEMeasurable.max {α : Type u_1} {δ : Type u_4} [] [] [] [] {f : δα} {g : δα} {μ : } (hf : ) (hg : ) :
AEMeasurable (fun (a : δ) => max (f a) (g a)) μ
theorem Measurable.min {α : Type u_1} {δ : Type u_4} [] [] [] [] {f : δα} {g : δα} (hf : ) (hg : ) :
Measurable fun (a : δ) => min (f a) (g a)
theorem AEMeasurable.min {α : Type u_1} {δ : Type u_4} [] [] [] [] {f : δα} {g : δα} {μ : } (hf : ) (hg : ) :
AEMeasurable (fun (a : δ) => min (f a) (g a)) μ
@[instance 100]
instance ContinuousSup.measurableSup {γ : Type u_3} [] [] [] [Sup γ] [] :
Equations
• =
@[instance 100]
instance ContinuousSup.measurableSup₂ {γ : Type u_3} [] [] [] [Sup γ] [] :
Equations
• =
@[instance 100]
instance ContinuousInf.measurableInf {γ : Type u_3} [] [] [] [Inf γ] [] :
Equations
• =
@[instance 100]
instance ContinuousInf.measurableInf₂ {γ : Type u_3} [] [] [] [Inf γ] [] :
Equations
• =
theorem measurable_of_Iio {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' )) :
theorem UpperSemicontinuous.measurable {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] [] {f : δα} (hf : ) :
theorem measurable_of_Ioi {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' )) :
theorem LowerSemicontinuous.measurable {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] [] {f : δα} (hf : ) :
theorem measurable_of_Iic {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' )) :
theorem measurable_of_Ici {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' )) :
theorem Measurable.isLUB {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {ι : Sort u_5} [] {f : ιδα} {g : δα} (hf : ∀ (i : ι), Measurable (f i)) (hg : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) :

If a function is the least upper bound of countably many measurable functions, then it is measurable.

theorem Measurable.isLUB_of_mem {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {ι : Sort u_5} [] {f : ιδα} {g : δα} {g' : δα} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : ) (hg : bs, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' s) (g'_meas : ) :

If a function is the least upper bound of countably many measurable functions on a measurable set s, and coincides with a measurable function outside of s, then it is measurable.

theorem AEMeasurable.isLUB {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {ι : Sort u_5} {μ : } [] {f : ιδα} {g : δα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) :
theorem Measurable.isGLB {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {ι : Sort u_5} [] {f : ιδα} {g : δα} (hf : ∀ (i : ι), Measurable (f i)) (hg : ∀ (b : δ), IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) :

If a function is the greatest lower bound of countably many measurable functions, then it is measurable.

theorem Measurable.isGLB_of_mem {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {ι : Sort u_5} [] {f : ιδα} {g : δα} {g' : δα} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : ) (hg : bs, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' s) (g'_meas : ) :

If a function is the greatest lower bound of countably many measurable functions on a measurable set s, and coincides with a measurable function outside of s, then it is measurable.

theorem AEMeasurable.isGLB {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {ι : Sort u_5} {μ : } [] {f : ιδα} {g : δα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) :
theorem Monotone.measurable {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] [] [] [] {f : βα} (hf : ) :
theorem aemeasurable_restrict_of_monotoneOn {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] [] [] [] {μ : } {s : Set β} (hs : ) {f : βα} (hf : ) :
AEMeasurable f (μ.restrict s)
theorem Antitone.measurable {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] [] [] [] {f : βα} (hf : ) :
theorem aemeasurable_restrict_of_antitoneOn {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] [] [] [] {μ : } {s : Set β} (hs : ) {f : βα} (hf : ) :
AEMeasurable f (μ.restrict s)
theorem measurableSet_of_mem_nhdsWithin_Ioi_aux {α : Type u_1} [] [] [] [] [] {s : Set α} (h : xs, s nhdsWithin x ()) (h' : xs, ∃ (y : α), x < y) :
theorem measurableSet_of_mem_nhdsWithin_Ioi {α : Type u_1} [] [] [] [] [] {s : Set α} (h : xs, s nhdsWithin x ()) :

If a set is a right-neighborhood of all of its points, then it is measurable.

theorem measurableSet_bddAbove_range {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {ι : Sort u_5} [] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
MeasurableSet {b : δ | BddAbove (Set.range fun (i : ι) => f i b)}
theorem measurableSet_bddBelow_range {α : Type u_1} {δ : Type u_4} [] [] [] [] [] [] {ι : Sort u_5} [] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
MeasurableSet {b : δ | BddBelow (Set.range fun (i : ι) => f i b)}
theorem Measurable.iSup_Prop {δ : Type u_4} [] {α : Type u_5} [] (p : Prop) {f : δα} (hf : ) :
Measurable fun (b : δ) => ⨆ (_ : p), f b
theorem Measurable.iInf_Prop {δ : Type u_4} [] {α : Type u_5} [] (p : Prop) {f : δα} (hf : ) :
Measurable fun (b : δ) => ⨅ (_ : p), f b
theorem measurable_iSup {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Sort u_5} [] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
Measurable fun (b : δ) => ⨆ (i : ι), f i b
theorem aemeasurable_iSup {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Sort u_5} {μ : } [] {f : ιδα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) :
AEMeasurable (fun (b : δ) => ⨆ (i : ι), f i b) μ
theorem measurable_iInf {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Sort u_5} [] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
Measurable fun (b : δ) => ⨅ (i : ι), f i b
theorem aemeasurable_iInf {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Sort u_5} {μ : } [] {f : ιδα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) :
AEMeasurable (fun (b : δ) => ⨅ (i : ι), f i b) μ
theorem measurable_sSup {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Type u_5} {f : ιδα} {s : Set ι} (hs : s.Countable) (hf : is, Measurable (f i)) :
Measurable fun (x : δ) => sSup ((fun (i : ι) => f i x) '' s)
theorem measurable_sInf {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Type u_5} {f : ιδα} {s : Set ι} (hs : s.Countable) (hf : is, Measurable (f i)) :
Measurable fun (x : δ) => sInf ((fun (i : ι) => f i x) '' s)
theorem measurable_biSup {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Type u_5} (s : Set ι) {f : ιδα} (hs : s.Countable) (hf : is, Measurable (f i)) :
Measurable fun (b : δ) => is, f i b
theorem aemeasurable_biSup {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Type u_5} {μ : } (s : Set ι) {f : ιδα} (hs : s.Countable) (hf : is, AEMeasurable (f i) μ) :
AEMeasurable (fun (b : δ) => is, f i b) μ
theorem measurable_biInf {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Type u_5} (s : Set ι) {f : ιδα} (hs : s.Countable) (hf : is, Measurable (f i)) :
Measurable fun (b : δ) => is, f i b
theorem aemeasurable_biInf {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Type u_5} {μ : } (s : Set ι) {f : ιδα} (hs : s.Countable) (hf : is, AEMeasurable (f i) μ) :
AEMeasurable (fun (b : δ) => is, f i b) μ
theorem measurable_liminf' {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Type u_5} {ι' : Type u_6} {f : ιδα} {v : } (hf : ∀ (i : ι), Measurable (f i)) {p : ι'Prop} {s : ι'Set ι} (hv : v.HasCountableBasis p s) (hs : ∀ (j : ι'), (s j).Countable) :
Measurable fun (x : δ) => Filter.liminf (fun (x_1 : ι) => f x_1 x) v

liminf over a general filter is measurable. See measurable_liminf for the version over ℕ.

theorem measurable_limsup' {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {ι : Type u_5} {ι' : Type u_6} {f : ιδα} {u : } (hf : ∀ (i : ι), Measurable (f i)) {p : ι'Prop} {s : ι'Set ι} (hu : u.HasCountableBasis p s) (hs : ∀ (i : ι'), (s i).Countable) :
Measurable fun (x : δ) => Filter.limsup (fun (i : ι) => f i x) u

limsup over a general filter is measurable. See measurable_limsup for the version over ℕ.

theorem measurable_liminf {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {f : δα} (hf : ∀ (i : ), Measurable (f i)) :
Measurable fun (x : δ) => Filter.liminf (fun (i : ) => f i x) Filter.atTop

liminf over ℕ is measurable. See measurable_liminf' for a version with a general filter.

theorem measurable_limsup {α : Type u_1} {δ : Type u_4} [] [] [] [] [] {f : δα} (hf : ∀ (i : ), Measurable (f i)) :
Measurable fun (x : δ) => Filter.limsup (fun (i : ) => f i x) Filter.atTop

limsup over ℕ is measurable. See measurable_limsup' for a version with a general filter.

def Homemorph.toMeasurableEquiv {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] (h : α ≃ₜ β) :
α ≃ᵐ β

Convert a Homeomorph to a MeasurableEquiv.

Equations
• = { toEquiv := h.toEquiv, measurable_toFun := , measurable_invFun := }
Instances For
theorem IsFiniteMeasureOnCompacts.map {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] (μ : ) (f : α ≃ₜ β) :
theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type u_5} [] (μ : ) {f : αENNReal} (hf : ) {s : Set α} (hs : ) {t : NNReal} (ht : 1 < t) :
μ s = μ (s f ⁻¹' {0}) + μ (s f ⁻¹' {}) + ∑' (n : ), μ (s f ⁻¹' Set.Ico (t ^ n) (t ^ (n + 1)))

One can cut out ℝ≥0∞ into the sets {0}, Ico (t^n) (t^(n+1)) for n : ℤ and {∞}. This gives a way to compute the measure of a set in terms of sets on which a given function f does not fluctuate by more than t.