Measurable Space

Results named in Tau Ceti's TauCeti.MeasureTheory.MeasurableSpace modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Jankov–von Neumann uniformization theorem#

An analytic relation R ⊆ X × Y, with X a T₁ space, has a uniformization f : X → Y which is measurable for the σ-algebra generated by the analytic subsets of X: (x, f x) ∈ R for every x in the projection of R.

By TauCeti.MeasureTheory.nullMeasurable_of_measurable_generateFrom_analyticSet, such an f is null-measurable for every s-finite measure on a metrizable X; see MeasureTheory.AnalyticSet.exists_measurable_ae_uniformization.

MeasureTheory.AnalyticSet.exists_measurable_uniformization.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] [MeasurableSpace Y] [BorelSpace Y]
  [Nonempty Y] {R : Set (X × Y)} (hR : MeasureTheory.AnalyticSet R) :
  ∃ f, Measurable f ∧ ∀ x ∈ Prod.fst '' R, (x, f x) ∈ R

Lean

Formalized in Tau Ceti as MeasureTheory.AnalyticSet.exists_measurable_uniformization.

Sources

• Tau Ceti documentation: MeasureTheory.AnalyticSet.exists_measurable_uniformization
• Source of MeasureTheory.AnalyticSet.exists_measurable_uniformization in TauCeti/MeasureTheory/MeasurableSpace/Uniformization.lean

LeanMeasureTheory.AnalyticSet.exists_measurable_uniformization

Used by 1

Used byUniqueness of Wasserstein geodesics

TheoremThe Kuratowski–Ryll-Nardzewski measurable selection theorem#

A map M from a measurable space to the nonempty closed subsets of a Polish space, which is weakly measurable in the sense that {z | M z ∩ U ≠ ∅} is measurable for every open U, has a measurable selection.

TauCeti.exists_measurable_forall_mem.{u_1, u_2} {Z : Type u_1} {X : Type u_2} [MeasurableSpace Z]
  [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {M : Z → Set X}
  (hclosed : ∀ (z : Z), IsClosed (M z)) (hne : ∀ (z : Z), (M z).Nonempty)
  (hM : ∀ (U : Set X), IsOpen U → MeasurableSet {z | (M z ∩ U).Nonempty}) :
  ∃ f, Measurable f ∧ ∀ (z : Z), f z ∈ M z

Lean

Formalized in Tau Ceti as TauCeti.exists_measurable_forall_mem.

Sources

• Tau Ceti documentation: TauCeti.exists_measurable_forall_mem
• Source of TauCeti.exists_measurable_forall_mem in TauCeti/MeasureTheory/MeasurableSpace/Selection.lean

LeanTauCeti.exists_measurable_forall_mem

TheoremLusin's universal-measurability theorem#

An analytic subset of a metrizable space is null-measurable with respect to every s-finite measure on a measurable space containing the Borel sets, equivalently measurable in the completion of that measure.

TauCeti.MeasureTheory.AnalyticSet.nullMeasurableSet.{u_1} {X : Type u_1} [TopologicalSpace X]
  [TopologicalSpace.MetrizableSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {S : Set X}
  (hS : MeasureTheory.AnalyticSet S) (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] :
  MeasureTheory.NullMeasurableSet S μ

Lean

Formalized in Tau Ceti as TauCeti.MeasureTheory.AnalyticSet.nullMeasurableSet.

Sources

• Tau Ceti documentation: TauCeti.MeasureTheory.AnalyticSet.nullMeasurableSet
• Source of TauCeti.MeasureTheory.AnalyticSet.nullMeasurableSet in TauCeti/MeasureTheory/MeasurableSpace/Analytic.lean

LeanTauCeti.MeasureTheory.AnalyticSet.nullMeasurableSet

Used by 2

Used byUniqueness of Wasserstein geodesics · The Schachermayer--Teichmann theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.