OAI/Probability/LatticePassage/LocalSelection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CompanionFPP.encodable_lattice_walk line 9
  2. def OAI.CompanionFPP.enumerateWalk line 12
  3. lemma OAI.CompanionFPP.enumerateWalk_surjective line 15
  4. def OAI.CompanionFPP.minimizesLocally line 19
  5. lemma OAI.CompanionFPP.exists_minimizesLocally line 23
  6. lemma OAI.CompanionFPP.measurableSet_minimizesLocally line 29
  7. def OAI.CompanionFPP.localSelectionIndex line 39
  8. theorem OAI.CompanionFPP.measurable_localSelectionIndex line 44
  9. def OAI.CompanionFPP.selectedLocalPath line 49
  10. theorem OAI.CompanionFPP.selectedLocalPath_spec line 53
  11. theorem OAI.CompanionFPP.measurable_selectedLocalPath_observation line 61
  12. theorem OAI.CompanionFPP.selectedLocalPath_eq_of_agree line 67