OAI/Probability/DirectionalWalk/BridgeWords.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.appendWord line 12
  2. lemma OAI.DirectionalZeroOne.appendWord_length line 16
  3. lemma OAI.DirectionalZeroOne.appendWord_before line 18
  4. lemma OAI.DirectionalZeroOne.appendWord_after line 24
  5. lemma OAI.DirectionalZeroOne.appendWord_prefixWord line 29
  6. def OAI.DirectionalZeroOne.concatenateWords line 48
  7. def OAI.DirectionalZeroOne.concatenateList line 52
  8. lemma OAI.DirectionalZeroOne.concatenateWords_length line 54
  9. lemma OAI.DirectionalZeroOne.concatenateList_prefix_slabs line 60
  10. lemma OAI.DirectionalZeroOne.concatenateList_length line 80
  11. def OAI.DirectionalZeroOne.recordWord line 83
  12. lemma OAI.DirectionalZeroOne.recordWord_eq line 87
  13. lemma OAI.DirectionalZeroOne.recordWord_atom line 94
  14. lemma OAI.DirectionalZeroOne.measurable_recordWord line 108
  15. lemma OAI.DirectionalZeroOne.conditioned_recordWord_atom line 134
  16. def OAI.DirectionalZeroOne.rawBridgeMeasure line 172
  17. lemma OAI.DirectionalZeroOne.rawBridgeMeasure_conditioned line 176
  18. lemma OAI.DirectionalZeroOne.concatenate_cutList_slabs line 186
  19. lemma OAI.DirectionalZeroOne.bridgeListMeasure_concatenate line 200