OAI/Probability/Ballisticity/Renewal/Regeneration.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.RegenerationSupport line 12
  2. lemma OAI.DirectionalTransience.measurableSet_regenerationSupport line 16
  3. lemma OAI.DirectionalTransience.conditioned_regenerationSupport line 35
  4. lemma OAI.DirectionalTransience.regenerationSupport_noDrop line 42
  5. lemma OAI.DirectionalTransience.template_span_estimates line 45
  6. lemma OAI.DirectionalTransience.signedCoordinate_nsmul line 59
  7. lemma OAI.DirectionalTransience.tiltedCoordinate_nsmul line 65
  8. lemma OAI.DirectionalTransience.template_tilted_lower line 71
  9. lemma OAI.DirectionalTransience.wordPath_replicate_prefix line 93
  10. def OAI.DirectionalTransience.ForwardTemplate line 108
  11. lemma OAI.DirectionalTransience.measurableSet_forwardTemplate line 114
  12. lemma OAI.DirectionalTransience.forwardTemplate_script line 120
  13. lemma OAI.DirectionalTransience.forwardTemplate_noDrop line 128
  14. lemma OAI.DirectionalTransience.forwardTemplate_control line 142
  15. lemma OAI.DirectionalTransience.annealed_wordCylinder_lower line 229
  16. lemma OAI.DirectionalTransience.annealed_eq_noDrop_mul_conditioned line 241
  17. lemma OAI.DirectionalTransience.forwardTemplate_probability line 248
  18. lemma OAI.DirectionalTransience.tilted_height_avoids_prefix line 279
  19. lemma OAI.DirectionalTransience.controlled_suffix_caps_ratio line 295
  20. lemma OAI.DirectionalTransience.prefix_favourable_gain line 352
  21. lemma OAI.DirectionalTransience.stopping_prefix_favourable_gain line 380
  22. lemma OAI.DirectionalTransience.ratio_threshold_contraction line 399