OAI/Probability/Ballisticity/Crossings/HitWord.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalTransience.HitWord line 114
  2. lemma OAI.DirectionalTransience.hitWord_prefix line 117
  3. lemma OAI.DirectionalTransience.hitWord_cylinders_disjoint line 123
  4. lemma OAI.DirectionalTransience.hitWord_cover line 134
  5. def OAI.DirectionalTransience.wordTrace line 151
  6. lemma OAI.DirectionalTransience.wordDepartures_subset_trace line 154
  7. lemma OAI.DirectionalTransience.hitWords_contact_iff line 160
  8. lemma OAI.DirectionalTransience.annealedFrom_wordCylinder line 183
  9. lemma OAI.DirectionalTransience.disjoint_word_pair_weight line 190
  10. def OAI.DirectionalTransience.hitWordsEvent line 210
  11. lemma OAI.DirectionalTransience.measurableSet_hitWordsEvent line 214
  12. lemma OAI.DirectionalTransience.hitWordsEvent_diff_contact line 222
  13. lemma OAI.DirectionalTransience.hitWords_pair_cylinders_disjoint line 239
  14. lemma OAI.DirectionalTransience.hitWordsEvent_measure line 251
  15. theorem OAI.DirectionalTransience.raw_prefix_off_contact_equal line 267