OAI/Probability/DirectionalWalk/Escape.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.height line 10
  2. lemma OAI.DirectionalZeroOne.height_zero line 12
  3. lemma OAI.DirectionalZeroOne.height_add line 14
  4. lemma OAI.DirectionalZeroOne.height_neg line 18
  5. def OAI.DirectionalZeroOne.neverBelow line 21
  6. def OAI.DirectionalZeroOne.nonBacktracking line 24
  7. lemma OAI.DirectionalZeroOne.measurableSet_neverBelow line 26
  8. lemma OAI.DirectionalZeroOne.measurableSet_nonBacktracking line 32
  9. lemma OAI.DirectionalZeroOne.shiftPath_preimage_neverBelow line 35
  10. lemma OAI.DirectionalZeroOne.annealed_neverBelow_start line 41
  11. lemma OAI.DirectionalZeroOne.annealed_prefix_tail_null line 50
  12. def OAI.DirectionalZeroOne.extendPrefix line 68
  13. lemma OAI.DirectionalZeroOne.extendPrefix_apply line 71
  14. lemma OAI.DirectionalZeroOne.restrict_extendPrefix line 75
  15. lemma OAI.DirectionalZeroOne.set_eq_iUnion_prefix_inter line 80
  16. lemma OAI.DirectionalZeroOne.measure_zero_of_prefix_inter line 92
  17. lemma OAI.DirectionalZeroOne.annealed_tail_start_null line 98
  18. lemma OAI.DirectionalZeroOne.escape_subset_globalMinimum_suffix line 116
  19. lemma OAI.DirectionalZeroOne.positive_nonBacktracking line 128
  20. lemma OAI.DirectionalZeroOne.annealed_record_tail line 144
  21. lemma OAI.DirectionalZeroOne.annealed_record_relative_tail line 158
  22. def OAI.DirectionalZeroOne.pathFiltration line 187
  23. lemma OAI.DirectionalZeroOne.pathFiltration_eq line 190
  24. lemma OAI.DirectionalZeroOne.pathCylinder_eq_fiber line 194
  25. lemma OAI.DirectionalZeroOne.measurableSet_pathCylinder_filtration line 205
  26. lemma OAI.DirectionalZeroOne.pathFiltration_iSup line 210
  27. lemma OAI.DirectionalZeroOne.ae_pathCylinder_ne_zero line 224
  28. lemma OAI.DirectionalZeroOne.condExp_indicator_cylinder line 242
  29. lemma OAI.DirectionalZeroOne.null_of_prefix_contraction line 263
  30. lemma OAI.DirectionalZeroOne.real_contraction_of_disjoint_success line 290