OAI/Probability/Ballisticity/Estimates/FirstHighRecord.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.FirstHighRecord line 74
  2. lemma OAI.DirectionalTransience.measurableSet_firstHighRecord line 78
  3. lemma OAI.DirectionalTransience.firstHighRecord_unique line 88
  4. lemma OAI.DirectionalTransience.annealed_exists_firstHighRecord line 95
  5. def OAI.DirectionalTransience.AdmissibleHighWord line 106
  6. lemma OAI.DirectionalTransience.highWord_characterization line 115
  7. def OAI.DirectionalTransience.HighWordEvent line 153
  8. lemma OAI.DirectionalTransience.measurableSet_highWordEvent line 156
  9. lemma OAI.DirectionalTransience.highWordEvent_disjoint line 161
  10. lemma OAI.DirectionalTransience.highWordEvent_nil line 171
  11. lemma OAI.DirectionalTransience.highWordEvent_eq line 182
  12. lemma OAI.DirectionalTransience.highWordEvent_empty line 194
  13. def OAI.DirectionalTransience.highWord line 200
  14. lemma OAI.DirectionalTransience.highWord_eq_iff line 203
  15. lemma OAI.DirectionalTransience.highWord_nil_iff line 216
  16. lemma OAI.DirectionalTransience.measurable_highWord line 227
  17. def OAI.DirectionalTransience.highSuffix line 245
  18. lemma OAI.DirectionalTransience.measurable_highSuffix line 248
  19. lemma OAI.DirectionalTransience.highSuffix_on_highWordEvent line 259
  20. lemma OAI.DirectionalTransience.conditioned_highWord_exists line 269