OAI/Probability/DirectionalWalk/Renewal.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalZeroOne.TapeList line 12
  2. instance OAI.DirectionalZeroOne.tapeListMeasurableSpace line 14
  3. instance OAI.DirectionalZeroOne.tapeListMeasurableSingletonClass line 15
  4. def OAI.DirectionalZeroOne.tapePrefix line 18
  5. def OAI.DirectionalZeroOne.tapeCylinder line 20
  6. lemma OAI.DirectionalZeroOne.measurableSet_tapeCylinder line 23
  7. lemma OAI.DirectionalZeroOne.tapePrefix_eq_iff line 28
  8. lemma OAI.DirectionalZeroOne.measurable_tapePrefix line 41
  9. lemma OAI.DirectionalZeroOne.tapeCylinder_mass line 50
  10. def OAI.DirectionalZeroOne.tapeHeight line 61
  11. def OAI.DirectionalZeroOne.listHeight line 64
  12. lemma OAI.DirectionalZeroOne.listHeight_prefix line 67
  13. lemma OAI.DirectionalZeroOne.tapeHeight_mono line 71
  14. lemma OAI.DirectionalZeroOne.tapeHeight_strictMono line 77
  15. lemma OAI.DirectionalZeroOne.le_tapeHeight line 85
  16. lemma OAI.DirectionalZeroOne.measurable_tapeHeight line 94
  17. def OAI.DirectionalZeroOne.cutListIndex line 98
  18. lemma OAI.DirectionalZeroOne.measurable_cutListIndex line 102
  19. lemma OAI.DirectionalZeroOne.cutListIndex_eq line 109
  20. def OAI.DirectionalZeroOne.cutList line 117
  21. lemma OAI.DirectionalZeroOne.measurable_cutList line 120
  22. def OAI.DirectionalZeroOne.renewalCut line 130
  23. lemma OAI.DirectionalZeroOne.measurableSet_renewalCut line 133
  24. lemma OAI.DirectionalZeroOne.cutList_atom_iff line 138
  25. lemma OAI.DirectionalZeroOne.ae_tape_prop line 153
  26. def OAI.DirectionalZeroOne.bridgeListMeasure line 162
  27. lemma OAI.DirectionalZeroOne.bridgeListMeasure_mass line 166
  28. lemma OAI.DirectionalZeroOne.bridgeListMeasure_atom line 173
  29. def OAI.DirectionalZeroOne.reverseTapeList line 199
  30. lemma OAI.DirectionalZeroOne.reverseTapeList_involutive line 201
  31. lemma OAI.DirectionalZeroOne.listHeight_reverse line 205
  32. lemma OAI.DirectionalZeroOne.listProduct_reverse line 209
  33. lemma OAI.DirectionalZeroOne.bridgeListMeasure_reverse line 213
  34. def OAI.DirectionalZeroOne.bridgeListLaw line 226
  35. lemma OAI.DirectionalZeroOne.bridgeListLaw_probability line 230
  36. lemma OAI.DirectionalZeroOne.bridgeListLaw_atom line 239
  37. lemma OAI.DirectionalZeroOne.bridgeListLaw_reverse line 246