OAI/Probability/Ballisticity/Renewal/RegenerationWords.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.identDistrib_iterated_symbol line 12
  2. def OAI.DirectionalTransience.regenerationWords line 20
  3. lemma OAI.DirectionalTransience.measurable_regenerationWord line 23
  4. lemma OAI.DirectionalTransience.regenerationWords_independent line 27
  5. lemma OAI.DirectionalTransience.regenerationWords_identDistrib line 35
  6. lemma OAI.DirectionalTransience.firstWordEvent_self line 42
  7. def OAI.DirectionalTransience.regenerationTimes line 47
  8. lemma OAI.DirectionalTransience.regenerationTimes_zero line 50
  9. lemma OAI.DirectionalTransience.regenerationTimes_succ line 53
  10. lemma OAI.DirectionalTransience.measurable_regenerationTime line 57
  11. lemma OAI.DirectionalTransience.iterate_renewSuffix_eq line 62
  12. lemma OAI.DirectionalTransience.strictRecord_suffix_iff line 75
  13. lemma OAI.DirectionalTransience.trueRecord_suffix_iff line 88
  14. lemma OAI.DirectionalTransience.conditioned_all_firstWords line 94
  15. lemma OAI.DirectionalTransience.regenerationTimes_strictMono line 105
  16. lemma OAI.DirectionalTransience.regenerationTimes_true line 113
  17. lemma OAI.DirectionalTransience.regenerationTimes_no_true_between line 131
  18. def OAI.DirectionalTransience.recordCount line 147
  19. def OAI.DirectionalTransience.wordRecordCount line 150
  20. lemma OAI.DirectionalTransience.recordCount_congr_prefix line 153
  21. lemma OAI.DirectionalTransience.recordCount_add line 160
  22. lemma OAI.DirectionalTransience.recordCount_regenerationTimes line 171
  23. lemma OAI.DirectionalTransience.wordRecordCount_positive line 185
  24. lemma OAI.DirectionalTransience.recordCount_zero line 199
  25. lemma OAI.DirectionalTransience.recordCount_succ line 203
  26. lemma OAI.DirectionalTransience.recordCount_mono line 209
  27. lemma OAI.DirectionalTransience.recordCount_lt_of_strictRecord line 216
  28. lemma OAI.DirectionalTransience.recordCount_unbounded line 223
  29. lemma OAI.DirectionalTransience.exists_record_at_index line 234
  30. lemma OAI.DirectionalTransience.measurable_recordCount line 257
  31. def OAI.DirectionalTransience.RecordIndexPrefix line 264
  32. lemma OAI.DirectionalTransience.recordIndexPrefix_prefix line 268
  33. lemma OAI.DirectionalTransience.measurableSet_recordIndexPrefix line 279
  34. lemma OAI.DirectionalTransience.recordIndexPrefix_disjoint line 289
  35. lemma OAI.DirectionalTransience.recordIndexPrefix_noDrop line 302
  36. lemma OAI.DirectionalTransience.conditioned_recordIndexPrefix_true line 313
  37. lemma OAI.DirectionalTransience.conditioned_true_at_index_lower line 329
  38. lemma OAI.DirectionalTransience.renewal_truncated_sum_le line 353
  39. lemma OAI.DirectionalTransience.renewal_wald_bound line 369