OAI/Probability/DirectionalWalk/HittingWords.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.wordCylinder line 12
  2. def OAI.DirectionalZeroOne.wordEnd line 14
  3. def OAI.DirectionalZeroOne.wordDepartures line 16
  4. def OAI.DirectionalZeroOne.PrefixFreeWords line 19
  5. def OAI.DirectionalZeroOne.firstHitWord line 22
  6. lemma OAI.DirectionalZeroOne.firstHitWords_prefixFree line 25
  7. lemma OAI.DirectionalZeroOne.PrefixFreeWords.mono line 48
  8. lemma OAI.DirectionalZeroOne.quenched_restart_word line 54
  9. lemma OAI.DirectionalZeroOne.quenched_prefix_family line 61
  10. lemma OAI.DirectionalZeroOne.quenched_prefix_family_bound line 72
  11. lemma OAI.DirectionalZeroOne.word_contact_transfer line 92
  12. lemma OAI.DirectionalZeroOne.annealed_ae_quenched line 103
  13. lemma OAI.DirectionalZeroOne.annealed_exit_band line 117
  14. lemma OAI.DirectionalZeroOne.measurableSet_exit_band line 128
  15. lemma OAI.DirectionalZeroOne.quenched_exit_all_integer_bands line 134
  16. def OAI.DirectionalZeroOne.hitBefore line 143
  17. lemma OAI.DirectionalZeroOne.measurableSet_hitBefore line 146
  18. lemma OAI.DirectionalZeroOne.hitBefore_disjoint line 154
  19. lemma OAI.DirectionalZeroOne.hitBefore_union_eq_eventual line 161
  20. lemma OAI.DirectionalZeroOne.hitBefore_tail_subset line 184
  21. lemma OAI.DirectionalZeroOne.prefixWord_of_wordCylinder line 195
  22. def OAI.DirectionalZeroOne.firstPrefixWord line 203
  23. lemma OAI.DirectionalZeroOne.firstPrefixWords_prefixFree line 206
  24. lemma OAI.DirectionalZeroOne.firstPrefixWords_union line 229
  25. def OAI.DirectionalZeroOne.visitAfterWord line 253
  26. def OAI.DirectionalZeroOne.visitAfter line 256
  27. lemma OAI.DirectionalZeroOne.visitAfter_eq_firstPrefix line 259
  28. lemma OAI.DirectionalZeroOne.measurableSet_visitAfter line 281
  29. lemma OAI.DirectionalZeroOne.quenched_visitAfter_bound line 285