OAI/Probability/DirectionalWalk/Shifts.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.shiftEnvironment line 10
  2. def OAI.DirectionalZeroOne.shiftPath line 13
  3. lemma OAI.DirectionalZeroOne.measurable_shiftEnvironment line 15
  4. lemma OAI.DirectionalZeroOne.measurable_shiftPath line 18
  5. lemma OAI.DirectionalZeroOne.environmentLaw_shift line 23
  6. lemma OAI.DirectionalZeroOne.entryWeight_shift line 35
  7. lemma OAI.DirectionalZeroOne.pathWeight_shift line 44
  8. lemma OAI.DirectionalZeroOne.pathWeight_integral_shift line 48
  9. lemma OAI.DirectionalZeroOne.shiftPath_preimage_cylinder line 59
  10. lemma OAI.DirectionalZeroOne.annealed_shift line 65
  11. def OAI.DirectionalZeroOne.tailPath line 74
  12. lemma OAI.DirectionalZeroOne.measurable_tailPath line 76
  13. def OAI.DirectionalZeroOne.concatPath line 79
  14. lemma OAI.DirectionalZeroOne.concatPath_before line 82
  15. lemma OAI.DirectionalZeroOne.concatPath_after line 88
  16. lemma OAI.DirectionalZeroOne.pathWeight_concat line 91
  17. lemma OAI.DirectionalZeroOne.prefix_tail_inter line 105
  18. lemma OAI.DirectionalZeroOne.quenched_prefix_tail line 132
  19. lemma OAI.DirectionalZeroOne.prefix_preimage_singleton line 147
  20. lemma OAI.DirectionalZeroOne.cylinder_measure_eq_of_prefixMap line 159
  21. lemma OAI.DirectionalZeroOne.prefixMap_mono line 166