OAI/Probability/DirectionalWalk/Avoidance.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.avoidsThrough line 10
  2. def OAI.DirectionalZeroOne.avoids line 13
  3. lemma OAI.DirectionalZeroOne.measurableSet_avoidsThrough line 15
  4. lemma OAI.DirectionalZeroOne.measurableSet_avoids line 22
  5. lemma OAI.DirectionalZeroOne.avoidsThrough_antitone line 28
  6. lemma OAI.DirectionalZeroOne.cylinder_inter_avoidsThrough line 33
  7. lemma OAI.DirectionalZeroOne.pathWeight_congr_rows line 51
  8. lemma OAI.DirectionalZeroOne.quenched_avoid_prefixMap line 57
  9. lemma OAI.DirectionalZeroOne.quenched_restrict_avoids_eq line 79
  10. def OAI.DirectionalZeroOne.maskEnvironment line 118
  11. lemma OAI.DirectionalZeroOne.measurable_maskEnvironment line 123
  12. lemma OAI.DirectionalZeroOne.measurable_quenched_avoids_on_rows line 134
  13. lemma OAI.DirectionalZeroOne.measurable_entryWeight_on_rows line 150
  14. lemma OAI.DirectionalZeroOne.measurable_pathWeight_on_rows line 159
  15. lemma OAI.DirectionalZeroOne.path_departure_transfer line 166
  16. lemma OAI.DirectionalZeroOne.quenched_prefix_tail_apply line 177
  17. lemma OAI.DirectionalZeroOne.annealed_fresh_prefix_tail line 187
  18. lemma OAI.DirectionalZeroOne.path_weights_disjoint line 204