OAI/Probability/DirectionalWalk/RegenerativeTapes.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalZeroOne.tapeSigma line 12
  2. lemma OAI.DirectionalZeroOne.measurable_tapeEval line 15
  3. lemma OAI.DirectionalZeroOne.iid_prefix_suffix_independent line 19
  4. lemma OAI.DirectionalZeroOne.iid_suffix_law line 39
  5. lemma OAI.DirectionalZeroOne.tapeCylinder_suffix_factorization line 45
  6. def OAI.DirectionalZeroOne.regenerativeSequence line 56
  7. lemma OAI.DirectionalZeroOne.measurable_regenerativeSequence line 59
  8. lemma OAI.DirectionalZeroOne.regenerativeSequence_prefix_mass line 64
  9. lemma OAI.DirectionalZeroOne.regenerativeSequence_map line 93
  10. def OAI.DirectionalZeroOne.commonBlocks line 129
  11. lemma OAI.DirectionalZeroOne.commonBlocks_map line 132
  12. lemma OAI.DirectionalZeroOne.commonBlockLaw_atom line 143