OAI/Probability/DirectionalWalk/Words.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalZeroOne.Word line 10
  2. instance OAI.DirectionalZeroOne.(instance at line 12) line 12
  3. instance OAI.DirectionalZeroOne.(instance at line 13) line 13
  4. def OAI.DirectionalZeroOne.wordPath line 15
  5. def OAI.DirectionalZeroOne.prefixWord line 17
  6. lemma OAI.DirectionalZeroOne.wordPath_prefixWord line 19
  7. lemma OAI.DirectionalZeroOne.prefixWord_eq_iff line 23
  8. lemma OAI.DirectionalZeroOne.measurable_prefixWord line 42
  9. def OAI.DirectionalZeroOne.RegenerationWord line 51
  10. def OAI.DirectionalZeroOne.annealedWordWeight line 58
  11. def OAI.DirectionalZeroOne.firstCutTime line 61
  12. lemma OAI.DirectionalZeroOne.firstCutTime_spec line 66
  13. lemma OAI.DirectionalZeroOne.firstCutTime_eq_pos_iff line 73
  14. lemma OAI.DirectionalZeroOne.firstCutTime_eq_zero_iff line 89
  15. lemma OAI.DirectionalZeroOne.measurable_firstCutTime line 97
  16. def OAI.DirectionalZeroOne.firstWord line 118
  17. def OAI.DirectionalZeroOne.cutSuffix line 121
  18. lemma OAI.DirectionalZeroOne.measurable_firstWord line 124
  19. lemma OAI.DirectionalZeroOne.measurable_cutSuffix line 129
  20. lemma OAI.DirectionalZeroOne.firstWord_regeneration line 139
  21. lemma OAI.DirectionalZeroOne.firstWord_eq_iff line 186
  22. lemma OAI.DirectionalZeroOne.firstWord_event line 225
  23. lemma OAI.DirectionalZeroOne.firstWord_event_subset_nonBacktracking line 243