OAI/Probability/Ballisticity/Estimates/WordTemplate.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.independent_past_current line 12
  2. lemma OAI.DirectionalTransience.independent_past_event line 25
  3. lemma OAI.DirectionalTransience.regeneration_span line 35
  4. lemma OAI.DirectionalTransience.regeneration_height_sum line 44
  5. lemma OAI.DirectionalTransience.regeneration_radius_sum line 54
  6. lemma OAI.DirectionalTransience.regeneration_word_admissible line 65
  7. lemma OAI.DirectionalTransience.regeneration_span_bounds line 70
  8. lemma OAI.DirectionalTransience.increasing_cuts_cover line 97
  9. lemma OAI.DirectionalTransience.regeneration_prefix_radius line 110
  10. lemma OAI.DirectionalTransience.regeneration_prefix_height line 125
  11. lemma OAI.DirectionalTransience.truncatedMean_increment_bounds line 142
  12. lemma OAI.DirectionalTransience.scaled_tail_sum_lower line 177
  13. lemma OAI.DirectionalTransience.scaled_tail_sum_upper line 194
  14. lemma OAI.DirectionalTransience.summable_positive_tail line 213
  15. lemma OAI.DirectionalTransience.positive_tail_sums_eventually_small line 226
  16. lemma OAI.DirectionalTransience.restricted_large_word_intensity line 244
  17. lemma OAI.DirectionalTransience.independent_rare_word_past line 311
  18. lemma OAI.DirectionalTransience.polynomial_lower_from_small_intensity line 333
  19. def OAI.DirectionalTransience.WordTemplate line 344
  20. lemma OAI.DirectionalTransience.measurableSet_wordTemplate line 350
  21. lemma OAI.DirectionalTransience.wordTemplate_antitone line 367
  22. lemma OAI.DirectionalTransience.controlled_template_probability line 371
  23. lemma OAI.DirectionalTransience.wordTemplate_congr line 410
  24. lemma OAI.DirectionalTransience.current_word_template_independent line 424