OAI/Analysis/KadisonKastler/BaireMeasurableBranch.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Measurable successive choices of Baire digits

  1. instance OAI.KadisonKastler.(instance at line 17) line 17
  2. instance OAI.KadisonKastler.(instance at line 18) line 18
  3. def OAI.KadisonKastler.baireNextPredicate line 20
  4. theorem OAI.KadisonKastler.baireNextPredicate_exists line 26
  5. def OAI.KadisonKastler.baireNextDigit line 34
  6. theorem OAI.KadisonKastler.baireNextDigit_mem line 39
  7. theorem OAI.KadisonKastler.measurable_baireNextDigit line 47
  8. def OAI.KadisonKastler.baireChosenWord line 63
  9. theorem OAI.KadisonKastler.baireChosenWord_length line 68
  10. theorem OAI.KadisonKastler.measurable_baireChosenWord line 74
  11. def OAI.KadisonKastler.baireChosenBranch line 84
  12. theorem OAI.KadisonKastler.measurable_baireChosenDigit line 87
  13. theorem OAI.KadisonKastler.measurable_baireChosenBranch line 93
  14. theorem OAI.KadisonKastler.baireChosenBranch_res line 98
  15. theorem OAI.KadisonKastler.baireChosenBranch_hull line 105