OAI/Probability/Ballisticity/Estimates/SuccessfulWords.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.hitWordEvent line 12
  2. lemma OAI.DirectionalTransience.measurableSet_hitWordEvent line 16
  3. lemma OAI.DirectionalTransience.hitWordEvent_mass line 20
  4. lemma OAI.DirectionalTransience.hitWordEvent_univ_ae line 30
  5. def OAI.DirectionalTransience.successfulWordLaw line 38
  6. lemma OAI.DirectionalTransience.successfulWordLaw_apply line 42
  7. lemma OAI.DirectionalTransience.successfulWordLaw_event line 54
  8. lemma OAI.DirectionalTransience.successfulWordLaw_univ line 59
  9. lemma OAI.DirectionalTransience.successfulWordLaw_le_one line 65
  10. lemma OAI.DirectionalTransience.successfulWordLaw_finite line 71
  11. lemma OAI.DirectionalTransience.successfulWordLaw_endpoint line 76
  12. lemma OAI.DirectionalTransience.successfulWordLaw_singleton line 109
  13. def OAI.DirectionalTransience.rawWordLaw line 115
  14. instance OAI.DirectionalTransience.rawWordLaw_finite line 119
  15. lemma OAI.DirectionalTransience.rawWordLaw_singleton line 124
  16. lemma OAI.DirectionalTransience.rawWordLaw_univ line 142
  17. lemma OAI.DirectionalTransience.rawWordLaw_endpoint line 150
  18. lemma OAI.DirectionalTransience.measurable_rawWordLaw_rows line 156
  19. lemma OAI.DirectionalTransience.measurable_rawWordLaw line 172
  20. def OAI.DirectionalTransience.rawTupleWordLaw line 178
  21. instance OAI.DirectionalTransience.rawTupleWordLaw_finite line 182
  22. lemma OAI.DirectionalTransience.rawTupleWordLaw_endpoint line 187
  23. lemma OAI.DirectionalTransience.rawTupleWordLaw_singleton line 197
  24. lemma OAI.DirectionalTransience.measurable_rawWordLaw_tuple_component line 202
  25. lemma OAI.DirectionalTransience.measurable_rawTupleWordLaw_singleton line 210
  26. lemma OAI.DirectionalTransience.measurable_rawTupleWordLaw line 220