OAI/Probability/Ballisticity/Estimates/FixedPairSuffix.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.fixedPairSuffix line 12
  2. lemma OAI.DirectionalTransience.measurable_fixedPairSuffix line 17
  3. lemma OAI.DirectionalTransience.firstPairWordEvent_suffix_rectangle line 20
  4. lemma OAI.DirectionalTransience.independent_conditioned_pair_word_rectangle line 49
  5. lemma OAI.DirectionalTransience.independent_conditioned_pair_word_mass line 68
  6. lemma OAI.DirectionalTransience.independent_conditioned_pair_word_factor line 80
  7. lemma OAI.DirectionalTransience.renewPairSuffix_on_firstPairWordEvent line 110
  8. lemma OAI.DirectionalTransience.independent_conditioned_firstPairWord_fiber_ae line 121
  9. lemma OAI.DirectionalTransience.independent_conditioned_firstPairWord_fiber_factor line 138
  10. lemma OAI.DirectionalTransience.measurePreserving_of_countable_fiber_factor line 164
  11. lemma OAI.DirectionalTransience.indepFun_of_countable_fiber_factor line 191
  12. lemma OAI.DirectionalTransience.renewPairSuffix_preserves_independent_conditioned line 206
  13. lemma OAI.DirectionalTransience.firstPairWord_indep_renewPairSuffix line 219
  14. lemma OAI.DirectionalTransience.common_words_independent line 231
  15. lemma OAI.DirectionalTransience.common_words_identDistrib line 244
  16. def OAI.DirectionalTransience.commonWords line 253
  17. def OAI.DirectionalTransience.commonTimes line 256
  18. lemma OAI.DirectionalTransience.commonTimes_zero line 260
  19. lemma OAI.DirectionalTransience.commonTimes_succ line 263
  20. lemma OAI.DirectionalTransience.iterate_renewPairSuffix_eq line 269
  21. lemma OAI.DirectionalTransience.commonTrueRecord_suffix_iff line 296
  22. lemma OAI.DirectionalTransience.independent_conditioned_all_firstPairWords line 304
  23. lemma OAI.DirectionalTransience.commonTimes_strictMono line 316
  24. lemma OAI.DirectionalTransience.commonTimes_true line 323
  25. lemma OAI.DirectionalTransience.commonTimes_no_true_between line 343
  26. lemma OAI.DirectionalTransience.commonTrueRecord_eq_commonTimes line 365
  27. lemma OAI.DirectionalTransience.recordCount_commonTimes line 398
  28. lemma OAI.DirectionalTransience.recordCount_integer_height line 416