OAI/Analysis/KadisonKastler/BaireSelectionHulls.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Measurable hulls of finite-prefix images

For a continuous Baire-space parametrization, measurable hulls permit successive prefix choices outside one null set. This is the measure-specific selection construction needed for the published unitary selector.

  1. def OAI.KadisonKastler.bairePrefixCylinder line 22
  2. theorem OAI.KadisonKastler.bairePrefixCylinder_nil line 25
  3. theorem OAI.KadisonKastler.bairePrefixCylinder_children line 29
  4. theorem OAI.KadisonKastler.bairePrefixCylinder_eq line 40
  5. theorem OAI.KadisonKastler.measurableHull_subset_ae line 49

    Source documentation

    A measurable envelope is minimal modulo null sets among measurable supersets.

    theorem measurableHull_subset_ae (μ : Measure X) [IsFiniteMeasure μ]
    {A B : Set X} (hB : MeasurableSet B) (hAB : A ⊆ B) :
    ∀ᵐ x ∂μ, x ∈ toMeasurable μ A → x ∈ B := by
…
  6. def OAI.KadisonKastler.baireImageHull line 63
  7. theorem OAI.KadisonKastler.measurableSet_baireImageHull line 66
  8. theorem OAI.KadisonKastler.image_subset_baireImageHull line 71
  9. theorem OAI.KadisonKastler.baireImageHull_children_ae line 75
  10. theorem OAI.KadisonKastler.baireImageHull_all_children_ae line 86