OAI/Probability/DirectionalWalk/Columns.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.axialRay line 10
  2. lemma OAI.DirectionalZeroOne.axialRay_zero line 13
  3. lemma OAI.DirectionalZeroOne.axialRay_succ line 16
  4. lemma OAI.DirectionalZeroOne.axialRay_injective line 20
  5. lemma OAI.DirectionalZeroOne.height_nsmul line 26
  6. lemma OAI.DirectionalZeroOne.height_axialRay line 32
  7. lemma OAI.DirectionalZeroOne.pathWeight_axialRay line 36
  8. lemma OAI.DirectionalZeroOne.quenched_axialRay_pos line 42
  9. lemma OAI.DirectionalZeroOne.annealed_axialRay line 51
  10. lemma OAI.DirectionalZeroOne.quenched_prefix_tail_factor line 61
  11. lemma OAI.DirectionalZeroOne.annealed_disjoint_prefix_tail line 67
  12. def OAI.DirectionalZeroOne.alwaysBelow line 83
  13. lemma OAI.DirectionalZeroOne.measurableSet_alwaysBelow line 86
  14. def OAI.DirectionalZeroOne.infiniteVisits line 92
  15. lemma OAI.DirectionalZeroOne.measurableSet_infiniteVisits line 95
  16. lemma OAI.DirectionalZeroOne.quenched_bounded_infiniteVisits_null line 100
  17. lemma OAI.DirectionalZeroOne.annealed_bounded_infiniteVisits_null line 133
  18. def OAI.DirectionalZeroOne.column line 142
  19. lemma OAI.DirectionalZeroOne.column_axialRay line 144
  20. lemma OAI.DirectionalZeroOne.height_eq_column line 151
  21. lemma OAI.DirectionalZeroOne.finite_column_band line 161
  22. def OAI.DirectionalZeroOne.freshColumnTime line 197
  23. lemma OAI.DirectionalZeroOne.measurableSet_freshColumnTime line 200
  24. lemma OAI.DirectionalZeroOne.measurableSet_frequently_nat line 216
  25. lemma OAI.DirectionalZeroOne.annealed_bounded_freshColumns_null line 223
  26. lemma OAI.DirectionalZeroOne.recurrent_or_freshColumns line 264
  27. lemma OAI.DirectionalZeroOne.height_stepVector line 292
  28. lemma OAI.DirectionalZeroOne.annealed_bounded_band_null line 297
  29. lemma OAI.DirectionalZeroOne.exists_positive_step line 315
  30. lemma OAI.DirectionalZeroOne.finite_supremum line 326