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 α]
:
theorem
borel_eq_generateFrom_Ioi
(α : Type u_1)
[TopologicalSpace α]
[SecondCountableTopology α]
[LinearOrder α]
[OrderTopology α]
:
theorem
borel_eq_generateFrom_Iic
(α : Type u_1)
[TopologicalSpace α]
[SecondCountableTopology α]
[LinearOrder α]
[OrderTopology α]
:
theorem
borel_eq_generateFrom_Ici
(α : Type u_1)
[TopologicalSpace α]
[SecondCountableTopology α]
[LinearOrder α]
[OrderTopology α]
:
@[simp]
theorem
measurableSet_Ici
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
{a : α}
:
MeasurableSet (Set.Ici a)
theorem
nullMeasurableSet_Ici
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
{a : α}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
measurableSet_Iic
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
{a : α}
:
MeasurableSet (Set.Iic a)
theorem
nullMeasurableSet_Iic
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
{a : α}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
measurableSet_Icc
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
{a b : α}
:
MeasurableSet (Set.Icc a b)
theorem
nullMeasurableSet_Icc
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
{a b : α}
{μ : MeasureTheory.Measure α}
:
instance
nhdsWithin_Ici_isMeasurablyGenerated
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
{a b : α}
:
(nhdsWithin a (Set.Ici b)).IsMeasurablyGenerated
instance
nhdsWithin_Iic_isMeasurablyGenerated
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
{a b : α}
:
(nhdsWithin a (Set.Iic b)).IsMeasurablyGenerated
instance
nhdsWithin_Icc_isMeasurablyGenerated
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
{a b x : α}
:
(nhdsWithin x (Set.Icc a b)).IsMeasurablyGenerated
instance
atTop_isMeasurablyGenerated
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
:
instance
atBot_isMeasurablyGenerated
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[Preorder α]
[OrderClosedTopology α]
:
instance
instIsMeasurablyGeneratedCocompactOfR1Space
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[R1Space α]
:
theorem
measurableSet_le'
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[PartialOrder α]
[OrderClosedTopology α]
[SecondCountableTopology α]
:
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)
:
@[simp]
theorem
measurableSet_Iio
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a : α}
:
MeasurableSet (Set.Iio a)
theorem
nullMeasurableSet_Iio
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a : α}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
measurableSet_Ioi
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a : α}
:
MeasurableSet (Set.Ioi a)
theorem
nullMeasurableSet_Ioi
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a : α}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
measurableSet_Ioo
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a b : α}
:
MeasurableSet (Set.Ioo a b)
theorem
nullMeasurableSet_Ioo
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a b : α}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
measurableSet_Ioc
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a b : α}
:
MeasurableSet (Set.Ioc a b)
theorem
nullMeasurableSet_Ioc
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a b : α}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
measurableSet_Ico
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a b : α}
:
MeasurableSet (Set.Ico a b)
theorem
nullMeasurableSet_Ico
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a b : α}
{μ : MeasureTheory.Measure α}
:
instance
nhdsWithin_Ioi_isMeasurablyGenerated
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a b : α}
:
(nhdsWithin a (Set.Ioi b)).IsMeasurablyGenerated
instance
nhdsWithin_Iio_isMeasurablyGenerated
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a b : α}
:
(nhdsWithin a (Set.Iio b)).IsMeasurablyGenerated
instance
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}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
[SecondCountableTopology α]
:
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)
:
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 μ)
:
theorem
nullMeasurableSet_lt'
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
[SecondCountableTopology α]
{μ : MeasureTheory.Measure (α × α)}
:
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 μ)
:
theorem
Set.OrdConnected.measurableSet
{α : Type u_1}
{s : Set α}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
(h : s.OrdConnected)
:
theorem
IsPreconnected.measurableSet
{α : Type u_1}
{s : Set α}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
(h : IsPreconnected s)
:
theorem
generateFrom_Ico_mem_le_borel
{α : Type u_5}
[TopologicalSpace α]
[LinearOrder α]
[OrderClosedTopology α]
(s t : Set α)
:
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)
:
theorem
Dense.borel_eq_generateFrom_Ico_mem
{α : Type u_5}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[SecondCountableTopology α]
[DenselyOrdered α]
[NoMinOrder α]
{s : Set α}
(hd : Dense s)
:
theorem
borel_eq_generateFrom_Ico
(α : Type u_5)
[TopologicalSpace α]
[SecondCountableTopology α]
[LinearOrder α]
[OrderTopology α]
:
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)
:
theorem
Dense.borel_eq_generateFrom_Ioc_mem
{α : Type u_5}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[SecondCountableTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
{s : Set α}
(hd : Dense s)
:
theorem
borel_eq_generateFrom_Ioc
(α : Type u_5)
[TopologicalSpace α]
[SecondCountableTopology α]
[LinearOrder α]
[OrderTopology α]
:
theorem
MeasureTheory.Measure.ext_of_Ico_finite
{α : Type u_5}
[TopologicalSpace α]
{m : MeasurableSpace α}
[SecondCountableTopology α]
[LinearOrder α]
[OrderTopology α]
[BorelSpace α]
(μ ν : Measure α)
[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 α]
(μ ν : Measure α)
[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 α]
(μ ν : 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 α]
(μ ν : 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 α]
(μ ν : Measure α)
[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 α]
(μ ν : Measure α)
[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 α]
(μ ν : Measure α)
[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 α]
{x✝ : MeasurableSpace α}
[SecondCountableTopology α]
[LinearOrder α]
[OrderTopology α]
[BorelSpace α]
(μ ν : Measure α)
[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 α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a b : α}
:
MeasurableSet (Set.uIcc a b)
theorem
measurableSet_uIoc
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[OpensMeasurableSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{a b : α}
:
MeasurableSet (Set.uIoc a b)
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 : δ) => Max.max (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 : δ) => Max.max (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 : δ) => Min.min (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 : δ) => Min.min (f a) (g a)) μ
@[instance 100]
instance
ContinuousSup.measurableSup
{γ : Type u_3}
[TopologicalSpace γ]
{mγ : MeasurableSpace γ}
[BorelSpace γ]
[Max γ]
[ContinuousSup γ]
:
@[instance 100]
instance
ContinuousSup.measurableSup₂
{γ : Type u_3}
[TopologicalSpace γ]
{mγ : MeasurableSpace γ}
[BorelSpace γ]
[SecondCountableTopology γ]
[Max γ]
[ContinuousSup γ]
:
@[instance 100]
instance
ContinuousInf.measurableInf
{γ : Type u_3}
[TopologicalSpace γ]
{mγ : MeasurableSpace γ}
[BorelSpace γ]
[Min γ]
[ContinuousInf γ]
:
@[instance 100]
instance
ContinuousInf.measurableInf₂
{γ : Type u_3}
[TopologicalSpace γ]
{mγ : MeasurableSpace γ}
[BorelSpace γ]
[SecondCountableTopology γ]
[Min γ]
[ContinuousInf γ]
:
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
UpperSemicontinuous.measurable
{α : Type u_1}
{δ : Type u_4}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[BorelSpace α]
{mδ : MeasurableSpace δ}
[LinearOrder α]
[OrderTopology α]
[SecondCountableTopology α]
[TopologicalSpace δ]
[OpensMeasurableSpace δ]
{f : δ → α}
(hf : UpperSemicontinuous f)
:
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
LowerSemicontinuous.measurable
{α : Type u_1}
{δ : Type u_4}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[BorelSpace α]
{mδ : MeasurableSpace δ}
[LinearOrder α]
[OrderTopology α]
[SecondCountableTopology α]
[TopologicalSpace δ]
[OpensMeasurableSpace δ]
{f : δ → α}
(hf : LowerSemicontinuous f)
:
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 : ∀ b ∈ s, 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))
:
AEMeasurable g μ
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 : ∀ b ∈ s, 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))
:
AEMeasurable g μ
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_nhdsGT_aux
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[BorelSpace α]
[LinearOrder α]
[OrderTopology α]
[SecondCountableTopology α]
{s : Set α}
(h : ∀ x ∈ s, s ∈ nhdsWithin x (Set.Ioi x))
(h' : ∀ x ∈ s, ∃ (y : α), x < y)
:
theorem
MeasurableSet.of_mem_nhdsGT
{α : Type u_1}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[BorelSpace α]
[LinearOrder α]
[OrderTopology α]
[SecondCountableTopology α]
{s : Set α}
(h : ∀ x ∈ s, s ∈ nhdsWithin x (Set.Ioi 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}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[BorelSpace α]
{mδ : MeasurableSpace δ}
[LinearOrder α]
[OrderTopology α]
[SecondCountableTopology α]
{ι : Sort u_5}
[Countable ι]
{f : ι → δ → α}
(hf : ∀ (i : ι), Measurable (f i))
:
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))
:
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
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) μ
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
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) μ
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 : ∀ 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 α]
{mα : MeasurableSpace α}
[BorelSpace α]
{mδ : 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 α]
{mα : MeasurableSpace α}
[BorelSpace α]
{mδ : 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 α]
{mα : MeasurableSpace α}
[BorelSpace α]
{mδ : 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 α]
{mα : MeasurableSpace α}
[BorelSpace α]
{mδ : 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 α]
{mα : MeasurableSpace α}
[BorelSpace α]
{mδ : 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 α]
{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 ℕ.
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 ℕ.
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.
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 Homeomorph.toMeasurableEquiv (since := "2025-05-30")]
def
Homemorph.toMeasurableEquiv
{γ : Type u_3}
{γ₂ : Type u_4}
[TopologicalSpace γ]
[MeasurableSpace γ]
[BorelSpace γ]
[TopologicalSpace γ₂]
[MeasurableSpace γ₂]
[BorelSpace γ₂]
(h : γ ≃ₜ γ₂)
:
Alias of Homeomorph.toMeasurableEquiv.
A homeomorphism between two Borel spaces is a measurable equivalence.
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)
:
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.