OAI/Probability/DirectionalWalk/TwoTapes.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalZeroOne.TwoTape line 12
  2. abbrev OAI.DirectionalZeroOne.TwoTapeList line 13
  3. def OAI.DirectionalZeroOne.twoTapeLaw line 15
  4. def OAI.DirectionalZeroOne.twoPrefix line 19
  5. def OAI.DirectionalZeroOne.twoCylinder line 22
  6. lemma OAI.DirectionalZeroOne.measurableSet_twoCylinder line 25
  7. lemma OAI.DirectionalZeroOne.measurable_twoPrefix line 31
  8. def OAI.DirectionalZeroOne.twoShift line 35
  9. lemma OAI.DirectionalZeroOne.measurable_twoShift line 38
  10. lemma OAI.DirectionalZeroOne.twoShift_law line 42
  11. lemma OAI.DirectionalZeroOne.twoExtract_law line 55
  12. lemma OAI.DirectionalZeroOne.ae_twoTape_prop line 60
  13. abbrev OAI.DirectionalZeroOne.coordSigma line 72
  14. lemma OAI.DirectionalZeroOne.measurable_coordEval line 75
  15. lemma OAI.DirectionalZeroOne.two_prefix_suffix_independent line 79
  16. lemma OAI.DirectionalZeroOne.twoCylinder_mass line 99
  17. lemma OAI.DirectionalZeroOne.twoCylinder_suffix_factorization line 121
  18. lemma OAI.DirectionalZeroOne.tapeHeight_add line 135
  19. lemma OAI.DirectionalZeroOne.renewalCut_add_iff line 139
  20. def OAI.DirectionalZeroOne.commonCut line 152
  21. lemma OAI.DirectionalZeroOne.measurableSet_commonCut line 155
  22. lemma OAI.DirectionalZeroOne.commonCut_zero line 160
  23. def OAI.DirectionalZeroOne.commonCutIndices line 165
  24. def OAI.DirectionalZeroOne.commonCutList line 168
  25. def OAI.DirectionalZeroOne.afterCommonCut line 171
  26. lemma OAI.DirectionalZeroOne.measurable_commonCutIndices line 174
  27. lemma OAI.DirectionalZeroOne.measurable_commonCutList line 178
  28. lemma OAI.DirectionalZeroOne.measurable_afterCommonCut line 182
  29. lemma OAI.DirectionalZeroOne.commonCutList_atom_iff line 188
  30. lemma OAI.DirectionalZeroOne.commonCutIndices_eq_lengths line 202
  31. lemma OAI.DirectionalZeroOne.commonCut_add_iff line 208
  32. lemma OAI.DirectionalZeroOne.commonCut_fibre_tail line 219
  33. lemma OAI.DirectionalZeroOne.commonCut_tail_factorization line 261
  34. instance OAI.DirectionalZeroOne.twoTapeLaw_probability line 273
  35. lemma OAI.DirectionalZeroOne.twoExtract_independent line 278
  36. lemma OAI.DirectionalZeroOne.commonCut_mass line 297
  37. def OAI.DirectionalZeroOne.noCommonThrough line 314
  38. lemma OAI.DirectionalZeroOne.measurableSet_noCommonThrough line 317
  39. def OAI.DirectionalZeroOne.lastCommonEvent line 323
  40. lemma OAI.DirectionalZeroOne.measurableSet_lastCommonEvent line 326
  41. lemma OAI.DirectionalZeroOne.lastCommonEvent_disjoint line 334
  42. lemma OAI.DirectionalZeroOne.lastCommonEvent_partition line 345
  43. lemma OAI.DirectionalZeroOne.lastCommonEvent_tail line 360
  44. lemma OAI.DirectionalZeroOne.lastCommonEvent_mass line 374
  45. lemma OAI.DirectionalZeroOne.common_renewal_tail_identity line 385
  46. lemma OAI.DirectionalZeroOne.common_renewal_tail_sum_bound line 400