OAI/Probability/Ballisticity/Geometry/FiniteWordGeometry.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.wordPath_append_prefix line 13
  2. lemma OAI.DirectionalTransience.wordPath_append_suffix line 25
  3. lemma OAI.DirectionalTransience.wordPath_after_end line 32
  4. lemma OAI.DirectionalTransience.wordWeight_append line 42
  5. lemma OAI.DirectionalTransience.wordPath_height_step line 49
  6. lemma OAI.DirectionalTransience.wordPath_hit_exact line 56
  7. def OAI.DirectionalTransience.wordFirstHitTime line 77
  8. def OAI.DirectionalTransience.wordFirstHitPosition line 81
  9. lemma OAI.DirectionalTransience.wordFirstHitTime_spec line 85
  10. lemma OAI.DirectionalTransience.wordFirstHitTime_le line 92
  11. lemma OAI.DirectionalTransience.wordFirstHitTime_min line 99
  12. lemma OAI.DirectionalTransience.wordFirstHitTime_zero line 105
  13. lemma OAI.DirectionalTransience.wordFirstHitTime_endpoint line 111
  14. lemma OAI.DirectionalTransience.coordinate_mem_strip_iff line 126
  15. lemma OAI.DirectionalTransience.coordinate_mem_upper_iff line 140
  16. lemma OAI.DirectionalTransience.wordPath_hit_append line 145
  17. lemma OAI.DirectionalTransience.wordFirstHitTime_eq line 172
  18. lemma OAI.DirectionalTransience.wordFirstHitTime_append_prefix line 182
  19. lemma OAI.DirectionalTransience.wordFirstHitPosition_append_prefix line 197
  20. lemma OAI.DirectionalTransience.wordFirstHitTime_append_suffix line 208
  21. lemma OAI.DirectionalTransience.wordFirstHitPosition_append_suffix line 233