OAI/Probability/Ballisticity/Estimates/StrictRecord.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.StrictRecord line 12
  2. def OAI.DirectionalTransience.TrueRecord line 15
  3. def OAI.DirectionalTransience.FirstTrueRecord line 18
  4. lemma OAI.DirectionalTransience.measurableSet_strictRecord line 21
  5. lemma OAI.DirectionalTransience.measurableSet_trueRecord line 31
  6. lemma OAI.DirectionalTransience.measurableSet_firstTrueRecord line 35
  7. lemma OAI.DirectionalTransience.wordDepartures_mem_iff line 42
  8. lemma OAI.DirectionalTransience.strictRecord_congr_prefix line 57
  9. def OAI.DirectionalTransience.AdmissibleTrueWord line 65
  10. lemma OAI.DirectionalTransience.admissibleTrueWord_record line 74
  11. lemma OAI.DirectionalTransience.suffix_noDrop_iff line 82
  12. lemma OAI.DirectionalTransience.firstTrueWord_characterization line 90
  13. lemma OAI.DirectionalTransience.firstTrueRecord_unique line 153
  14. def OAI.DirectionalTransience.conditionedLaw line 160
  15. lemma OAI.DirectionalTransience.conditionedLaw_probability line 164
  16. lemma OAI.DirectionalTransience.conditionedLaw_apply_of_subset line 172
  17. lemma OAI.DirectionalTransience.conditioned_true_word_factor line 178
  18. lemma OAI.DirectionalTransience.piLE_iSup_eq line 196
  19. lemma OAI.DirectionalTransience.prefix_probability_lower line 213
  20. lemma OAI.DirectionalTransience.ae_of_prefix_probability_lower line 250
  21. lemma OAI.DirectionalTransience.annealed_record_cylinder_noDrop line 282
  22. def OAI.DirectionalTransience.PrefixDetermined line 317
  23. lemma OAI.DirectionalTransience.prefixDetermined_mono line 320
  24. lemma OAI.DirectionalTransience.prefixDetermined_inter line 324
  25. lemma OAI.DirectionalTransience.prefixDetermined_cylinder line 328
  26. lemma OAI.DirectionalTransience.prefixDetermined_inter_cylinder line 334
  27. lemma OAI.DirectionalTransience.annealed_record_event_noDrop line 344
  28. def OAI.DirectionalTransience.NextRecordAfter line 382
  29. lemma OAI.DirectionalTransience.nextRecordAfter_prefix line 385
  30. lemma OAI.DirectionalTransience.measurableSet_nextRecordAfter line 394
  31. lemma OAI.DirectionalTransience.nextRecordAfter_disjoint line 401
  32. lemma OAI.DirectionalTransience.exists_strictRecord_gt line 410