Documentation

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Borel sigma algebras on spaces with orders #

Main statements #

@[simp]
theorem nhdsWithin_Ici_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a b : α} :
(nhdsWithin a (Set.Ici b)).IsMeasurablyGenerated
theorem nhdsWithin_Iic_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a b : α} :
(nhdsWithin a (Set.Iic b)).IsMeasurablyGenerated
theorem nhdsWithin_Icc_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a b x : α} :
(nhdsWithin x (Set.Icc a b)).IsMeasurablyGenerated
theorem atTop_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] :
Filter.atTop.IsMeasurablyGenerated
theorem atBot_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] :
Filter.atBot.IsMeasurablyGenerated
theorem measurableSet_le {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] {mδ : MeasurableSpace δ} [PartialOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f g : δα} (hf : Measurable f) (hg : Measurable g) :
MeasurableSet {a : δ | f a g a}
theorem nhdsWithin_Ioi_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a b : α} :
(nhdsWithin a (Set.Ioi b)).IsMeasurablyGenerated
theorem nhdsWithin_Iio_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a b : α} :
(nhdsWithin a (Set.Iio b)).IsMeasurablyGenerated
theorem nhdsWithin_uIcc_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a b x : α} :
(nhdsWithin x (Set.uIcc a b)).IsMeasurablyGenerated
theorem measurableSet_lt {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] {mδ : 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 α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure δ} {f g : δα} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
MeasureTheory.NullMeasurableSet {a : δ | f a < g a} μ
theorem nullMeasurableSet_le {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure δ} {f g : δα} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
MeasureTheory.NullMeasurableSet {a : δ | f a g a} μ
theorem generateFrom_Ico_mem_le_borel {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (s t : Set α) :
MeasurableSpace.generateFrom {S : Set α | ls, ut, 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 xx s) (hIoo : ∀ (x y : α), x < ySet.Ioo x y = y s) :
borel α = MeasurableSpace.generateFrom {S : Set α | ls, us, 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 α | ls, us, 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 xx s) (hIoo : ∀ (x y : α), x < ySet.Ioo x y = x s) :
borel α = MeasurableSpace.generateFrom {S : Set α | ls, us, 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 α | ls, us, 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.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.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 α) (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 α) (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.

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

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

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 α] {x✝ : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : 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 Measurable.max {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f g : δα} (hf : Measurable f) (hg : Measurable g) :
Measurable fun (a : δ) => f a g a
theorem AEMeasurable.max {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f g : δα} {μ : MeasureTheory.Measure δ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
AEMeasurable (fun (a : δ) => f a g a) μ
theorem Measurable.min {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f g : δα} (hf : Measurable f) (hg : Measurable g) :
Measurable fun (a : δ) => f a g a
theorem AEMeasurable.min {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f g : δα} {μ : MeasureTheory.Measure δ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
AEMeasurable (fun (a : δ) => f a g a) μ
theorem measurable_of_Iio {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Iio x)) :
theorem measurable_of_Ioi {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Ioi x)) :
theorem measurable_of_Iic {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Iic x)) :
theorem measurable_of_Ici {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Ici x)) :
theorem Measurable.isLUB {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : 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)) :

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

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 α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {f : ιδα} {g g' : δα} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : MeasurableSet s) (hg : bs, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' s) (g'_meas : 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 α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : 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)) :
theorem Monotone.measurable {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] [TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {f : βα} (hf : Monotone f) :
theorem aemeasurable_restrict_of_monotoneOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] [TopologicalSpace β] {mβ : 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 α] {mα : MeasurableSpace α} [BorelSpace α] [TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {f : βα} (hf : Antitone f) :
theorem aemeasurable_restrict_of_antitoneOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] [TopologicalSpace β] {mβ : 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 α] {mα : MeasurableSpace α} [BorelSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (h : xs, s nhdsWithin x (Set.Ioi x)) (h' : xs, ∃ (y : α), x < y) :

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 α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : 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 α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : 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} {mδ : MeasurableSpace δ} {α : Type u_5} {mα : MeasurableSpace α} [ConditionallyCompleteLattice α] (p : Prop) {f : δα} (hf : Measurable f) :
Measurable fun (b : δ) => ⨆ (_ : p), f b
theorem Measurable.iInf_Prop {δ : Type u_4} {mδ : MeasurableSpace δ} {α : Type u_5} {mα : MeasurableSpace α} [ConditionallyCompleteLattice α] (p : Prop) {f : δα} (hf : Measurable f) :
Measurable fun (b : δ) => ⨅ (_ : p), f b
theorem Measurable.iSup {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
Measurable fun (b : δ) => ⨆ (i : ι), f i b
@[deprecated Measurable.iSup]
theorem measurable_iSup {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5} [Countable ι] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
Measurable fun (b : δ) => ⨆ (i : ι), f i b

Alias of Measurable.iSup.

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

Alias of AEMeasurable.iSup.

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

Alias of Measurable.iInf.

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

Alias of AEMeasurable.iInf.

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

Alias of Measurable.sSup.

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

Alias of Measurable.sInf.

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

Alias of Measurable.biSup.

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

Alias of AEMeasurable.biSup.

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

Alias of Measurable.biInf.

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

Alias of AEMeasurable.biInf.

theorem Measurable.liminf' {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : 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 .

@[deprecated Measurable.liminf']
theorem measurable_liminf' {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : 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

Alias of Measurable.liminf'.


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

theorem Measurable.limsup' {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : 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 .

@[deprecated Measurable.limsup']
theorem measurable_limsup' {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : 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

Alias of Measurable.limsup'.


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

theorem Measurable.liminf {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : 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.

@[deprecated Measurable.liminf]
theorem measurable_liminf {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (i : ), Measurable (f i)) :
Measurable fun (x : δ) => Filter.liminf (fun (i : ) => f i x) Filter.atTop

Alias of Measurable.liminf.


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

theorem Measurable.limsup {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : 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.

@[deprecated Measurable.limsup]
theorem measurable_limsup {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δα} (hf : ∀ (i : ), Measurable (f i)) :
Measurable fun (x : δ) => Filter.limsup (fun (i : ) => f i x) Filter.atTop

Alias of Measurable.limsup.


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

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

Convert a Homeomorph to a MeasurableEquiv.

Equations
Instances For
    theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type u_5} {mα : 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.