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.

theorem borel_eq_generateFrom_Iio (α : Type u_1) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom (Set.range Set.Iio)

theorem borel_eq_generateFrom_Ioi (α : Type u_1) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom (Set.range Set.Ioi)

theorem borel_eq_generateFrom_Iic (α : Type u_1) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom (Set.range Set.Iic)

theorem borel_eq_generateFrom_Ici (α : Type u_1) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom (Set.range Set.Ici)

@[simp]

theorem measurableSet_Ici {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} : MeasurableSet (Set.Ici a)

@[simp]

theorem measurableSet_Iic {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} : MeasurableSet (Set.Iic a)

@[simp]

theorem measurableSet_Icc {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Set.Icc a b)

instance nhdsWithin_Ici_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} {b : α} : (nhdsWithin a (Set.Ici b)).IsMeasurablyGenerated

Equations

• ⋯ = ⋯

instance nhdsWithin_Iic_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} {b : α} : (nhdsWithin a (Set.Iic b)).IsMeasurablyGenerated

Equations

• ⋯ = ⋯

instance nhdsWithin_Icc_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} : (nhdsWithin x (Set.Icc a b)).IsMeasurablyGenerated

Equations

• ⋯ = ⋯

instance atTop_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] : Filter.atTop.IsMeasurablyGenerated

Equations

• ⋯ = ⋯

instance atBot_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] : Filter.atBot.IsMeasurablyGenerated

Equations

• ⋯ = ⋯

instance instIsMeasurablyGeneratedCocompactOfR1Space {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [R1Space α] : (Filter.cocompact α).IsMeasurablyGenerated

Equations

• ⋯ = ⋯

theorem measurableSet_le' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [PartialOrder α] [OrderClosedTopology α] [SecondCountableTopology α] : MeasurableSet {p : α × α | p.1 ≤ p.2}

theorem measurableSet_le {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [PartialOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} (hf : Measurable f) (hg : Measurable g) : MeasurableSet {a : δ | f a ≤ g a}

@[simp]

theorem measurableSet_Iio {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} : MeasurableSet (Set.Iio a)

@[simp]

theorem measurableSet_Ioi {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} : MeasurableSet (Set.Ioi a)

@[simp]

theorem measurableSet_Ioo {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Set.Ioo a b)

@[simp]

theorem measurableSet_Ioc {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Set.Ioc a b)

@[simp]

theorem measurableSet_Ico {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Set.Ico a b)

instance nhdsWithin_Ioi_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : (nhdsWithin a (Set.Ioi b)).IsMeasurablyGenerated

Equations

• ⋯ = ⋯

instance nhdsWithin_Iio_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : (nhdsWithin a (Set.Iio b)).IsMeasurablyGenerated

Equations

• ⋯ = ⋯

instance nhdsWithin_uIcc_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} : (nhdsWithin x (Set.uIcc a b)).IsMeasurablyGenerated

Equations

• ⋯ = ⋯

theorem measurableSet_lt' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] : MeasurableSet {p : α × α | p.1 < p.2}

theorem measurableSet_lt {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} (hf : Measurable f) (hg : Measurable g) : MeasurableSet {a : δ | f a < g a}

theorem nullMeasurableSet_lt {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure δ} {f : δ → α} {g : δ → α} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : MeasureTheory.NullMeasurableSet {a : δ | f a < g a} μ

theorem nullMeasurableSet_lt' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure (α × α)} : MeasureTheory.NullMeasurableSet {p : α × α | p.1 < p.2} μ

theorem nullMeasurableSet_le {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure δ} {f : δ → α} {g : δ → α} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : MeasureTheory.NullMeasurableSet {a : δ | f a ≤ g a} μ

theorem Set.OrdConnected.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] (h : s.OrdConnected) : MeasurableSet s

theorem IsPreconnected.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] (h : IsPreconnected s) : MeasurableSet s

theorem generateFrom_Ico_mem_le_borel {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (s : Set α) (t : Set α) : MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ico l u = S} ≤ borel α

theorem Dense.borel_eq_generateFrom_Ico_mem_aux {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ (x : α), IsBot x → x ∈ s) (hIoo : ∀ (x y : α), x < y → Set.Ioo x y = ∅ → y ∈ s) : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ico l u = S}

theorem Dense.borel_eq_generateFrom_Ico_mem {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMinOrder α] {s : Set α} (hd : Dense s) : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ico l u = S}

theorem borel_eq_generateFrom_Ico (α : Type u_5) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u ∧ Set.Ico l u = S}

theorem Dense.borel_eq_generateFrom_Ioc_mem_aux {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ (x : α), IsTop x → x ∈ s) (hIoo : ∀ (x y : α), x < y → Set.Ioo x y = ∅ → x ∈ s) : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ioc l u = S}

theorem Dense.borel_eq_generateFrom_Ioc_mem {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMaxOrder α] {s : Set α} (hd : Dense s) : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ioc l u = S}

theorem borel_eq_generateFrom_Ioc (α : Type u_5) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u ∧ Set.Ioc l u = S}

theorem MeasureTheory.Measure.ext_of_Ico_finite {α : Type u_5} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (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} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (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} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] [NoMaxOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (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} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (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} [TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [BorelSpace α] [NoMaxOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (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} [TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (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} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (a : α), μ (Set.Iic a) = ν (Set.Iic 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} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (a : α), μ (Set.Ici a) = ν (Set.Ici 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} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Set.uIcc a b)

theorem measurableSet_uIoc {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Ι a b)

theorem Measurable.max {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} (hf : Measurable f) (hg : Measurable g) : Measurable fun (a : δ) => max (f a) (g a)

theorem AEMeasurable.max {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} {μ : MeasureTheory.Measure δ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun (a : δ) => max (f a) (g a)) μ

theorem Measurable.min {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} (hf : Measurable f) (hg : Measurable g) : Measurable fun (a : δ) => min (f a) (g a)

theorem AEMeasurable.min {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} {μ : MeasureTheory.Measure δ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun (a : δ) => min (f a) (g a)) μ

@[instance 100]

instance ContinuousSup.measurableSup {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Sup γ] [ContinuousSup γ] : MeasurableSup γ

Equations

• ⋯ = ⋯

@[instance 100]

instance ContinuousSup.measurableSup₂ {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ] [Sup γ] [ContinuousSup γ] : MeasurableSup₂ γ

Equations

• ⋯ = ⋯

@[instance 100]

instance ContinuousInf.measurableInf {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Inf γ] [ContinuousInf γ] : MeasurableInf γ

Equations

• ⋯ = ⋯

@[instance 100]

instance ContinuousInf.measurableInf₂ {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ] [Inf γ] [ContinuousInf γ] : MeasurableInf₂ γ

Equations

• ⋯ = ⋯

theorem measurable_of_Iio {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Iio x)) : Measurable f

theorem UpperSemicontinuous.measurable {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [TopologicalSpace δ] [OpensMeasurableSpace δ] {f : δ → α} (hf : UpperSemicontinuous f) : Measurable f

theorem measurable_of_Ioi {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Ioi x)) : Measurable f

theorem LowerSemicontinuous.measurable {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [TopologicalSpace δ] [OpensMeasurableSpace δ] {f : δ → α} (hf : LowerSemicontinuous f) : Measurable f

theorem measurable_of_Iic {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Iic x)) : Measurable f

theorem measurable_of_Ici {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Ici x)) : Measurable f

theorem Measurable.isLUB {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), Measurable (f i)) (hg : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) : Measurable g

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {f : ι → δ → α} {g : δ → α} {g' : δ → α} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : MeasurableSet s) (hg : ∀ b ∈ s, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' sᶜ) (g'_meas : Measurable g') : Measurable g

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) : AEMeasurable g μ

theorem Measurable.isGLB {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), Measurable (f i)) (hg : ∀ (b : δ), IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) : Measurable g

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {f : ι → δ → α} {g : δ → α} {g' : δ → α} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : MeasurableSet s) (hg : ∀ b ∈ s, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' sᶜ) (g'_meas : Measurable g') : Measurable g

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) : AEMeasurable g μ

theorem Monotone.measurable {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {f : β → α} (hf : Monotone f) : Measurable f

theorem aemeasurable_restrict_of_monotoneOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {μ : MeasureTheory.Measure β} {s : Set β} (hs : MeasurableSet s) {f : β → α} (hf : MonotoneOn f s) : AEMeasurable f (μ.restrict s)

theorem Antitone.measurable {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {f : β → α} (hf : Antitone f) : Measurable f

theorem aemeasurable_restrict_of_antitoneOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {μ : MeasureTheory.Measure β} {s : Set β} (hs : MeasurableSet s) {f : β → α} (hf : AntitoneOn f s) : AEMeasurable f (μ.restrict s)

theorem measurableSet_of_mem_nhdsWithin_Ioi_aux {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (h : ∀ x ∈ s, s ∈ nhdsWithin x (Set.Ioi x)) (h' : ∀ x ∈ s, ∃ (y : α), x < y) : MeasurableSet s

theorem measurableSet_of_mem_nhdsWithin_Ioi {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (h : ∀ x ∈ s, s ∈ nhdsWithin x (Set.Ioi x)) : MeasurableSet s

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), Measurable (f i)) : MeasurableSet {b : δ | BddBelow (Set.range fun (i : ι) => f i b)}

theorem Measurable.iSup_Prop {δ : Type u_4} [MeasurableSpace δ] {α : Type u_5} [MeasurableSpace α] [ConditionallyCompleteLattice α] (p : Prop) {f : δ → α} (hf : Measurable f) : Measurable fun (b : δ) => ⨆ (_ : p), f b

theorem Measurable.iInf_Prop {δ : Type u_4} [MeasurableSpace δ] {α : Type u_5} [MeasurableSpace α] [ConditionallyCompleteLattice α] (p : Prop) {f : δ → α} (hf : Measurable f) : Measurable fun (b : δ) => ⨅ (_ : p), f b

theorem measurable_iSup {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), Measurable (f i)) : Measurable fun (b : δ) => ⨆ (i : ι), f i b

theorem aemeasurable_iSup {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) : AEMeasurable (fun (b : δ) => ⨆ (i : ι), f i b) μ

theorem measurable_iInf {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), Measurable (f i)) : Measurable fun (b : δ) => ⨅ (i : ι), f i b

theorem aemeasurable_iInf {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) : AEMeasurable (fun (b : δ) => ⨅ (i : ι), f i b) μ

theorem measurable_sSup {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_5} {f : ι → δ → α} {s : Set ι} (hs : s.Countable) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun (x : δ) => sSup ((fun (i : ι) => f i x) '' s)

theorem measurable_sInf {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_5} {f : ι → δ → α} {s : Set ι} (hs : s.Countable) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun (x : δ) => sInf ((fun (i : ι) => f i x) '' s)

theorem measurable_biSup {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_5} (s : Set ι) {f : ι → δ → α} (hs : s.Countable) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun (b : δ) => ⨆ i ∈ s, f i b

theorem aemeasurable_biSup {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_5} {μ : MeasureTheory.Measure δ} (s : Set ι) {f : ι → δ → α} (hs : s.Countable) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) : AEMeasurable (fun (b : δ) => ⨆ i ∈ s, f i b) μ

theorem measurable_biInf {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_5} (s : Set ι) {f : ι → δ → α} (hs : s.Countable) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun (b : δ) => ⨅ i ∈ s, f i b

theorem aemeasurable_biInf {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_5} {μ : MeasureTheory.Measure δ} (s : Set ι) {f : ι → δ → α} (hs : s.Countable) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) : AEMeasurable (fun (b : δ) => ⨅ i ∈ s, f i b) μ

theorem measurable_liminf' {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_5} {ι' : Type u_6} {f : ι → δ → α} {v : Filter ι} (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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_5} {ι' : Type u_6} {f : ι → δ → α} {u : Filter ι} (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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] (h : α ≃ₜ β) : α ≃ᵐ β

Convert a Homeomorph to a MeasurableEquiv.

Equations

• Homemorph.toMeasurableEquiv h = { toEquiv := h.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem IsFiniteMeasureOnCompacts.map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : α ≃ₜ β) : MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.map (⇑f) μ)

theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type u_5} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ENNReal} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s) {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.