OAI/Probability/Ballisticity/Estimates/WordPrefixes.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.wordPath_take line 12
  2. def OAI.DirectionalTransience.wordPrefix line 20
  3. lemma OAI.DirectionalTransience.wordFirstHitTime_le_end line 23
  4. lemma OAI.DirectionalTransience.wordPrefix_length line 29
  5. lemma OAI.DirectionalTransience.wordPrefix_hit line 33
  6. def OAI.DirectionalTransience.coordinateWordPrefix line 53
  7. lemma OAI.DirectionalTransience.wordCylinder_prefix line 57
  8. lemma OAI.DirectionalTransience.successfulWordLaw_prefix_le line 66
  9. lemma OAI.DirectionalTransience.rawWordLaw_prefix_le line 82
  10. def OAI.DirectionalTransience.tupleWordPrefix line 97
  11. lemma OAI.DirectionalTransience.rawTupleWordLaw_prefix_le line 100
  12. lemma OAI.DirectionalTransience.relativeWordDisplacement_prefix line 119
  13. lemma OAI.DirectionalTransience.tupleRelativeBudget_prefix line 129
  14. lemma OAI.DirectionalTransience.tupleRelativeBudget_prefix_separation line 140
  15. lemma OAI.DirectionalTransience.rawTupleWordLaw_valid_ae line 148
  16. lemma OAI.DirectionalTransience.relativeBudgetWordLaw_prefix_separation_ae line 161
  17. theorem OAI.DirectionalTransience.budget_prefix_certificate line 174