OAI/Probability/DirectionalWalk/FreshContacts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.wordPairCylinder line 12
  2. lemma OAI.DirectionalZeroOne.measurableSet_wordPairCylinder line 15
  3. lemma OAI.DirectionalZeroOne.wordPair_transfer line 19
  4. def OAI.DirectionalZeroOne.freshPair line 30
  5. instance OAI.DirectionalZeroOne.(instance at line 34) line 34
  6. lemma OAI.DirectionalZeroOne.freshPair_apply line 39
  7. lemma OAI.DirectionalZeroOne.freshPair_first line 46
  8. lemma OAI.DirectionalZeroOne.freshPair_second line 58
  9. lemma OAI.DirectionalZeroOne.wordPairFamily_transfer line 70
  10. lemma OAI.DirectionalZeroOne.wordPairFamily_visit_bound line 99
  11. def OAI.DirectionalZeroOne.firstContactPairs line 114
  12. lemma OAI.DirectionalZeroOne.firstContactPairs_rows line 120
  13. lemma OAI.DirectionalZeroOne.firstContactPairs_disjoint line 127
  14. lemma OAI.DirectionalZeroOne.firstContactPairs_classify line 148
  15. lemma OAI.DirectionalZeroOne.firstContactPairs_visit_bound line 174
  16. lemma OAI.DirectionalZeroOne.freshJoint_visitAfter_bound line 188
  17. lemma OAI.DirectionalZeroOne.firstContactPairs_raw_bound line 202