OAI/Probability/Ballisticity/Estimates/IndependentPairLaw.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.shared_pair_common_true_unbounded line 12
  2. lemma OAI.DirectionalTransience.pair_record_event_noDrop_lower line 24
  3. lemma OAI.DirectionalTransience.pair_common_true_after_prefix line 72
  4. def OAI.DirectionalTransience.independentPairLaw line 158
  5. instance OAI.DirectionalTransience.independentPairLaw_probability line 161
  6. lemma OAI.DirectionalTransience.independent_pair_record_cylinder_noDrop line 165
  7. lemma OAI.DirectionalTransience.independent_pair_layer_hits line 178
  8. lemma OAI.DirectionalTransience.independent_pair_common_true_unbounded line 193
  9. lemma OAI.DirectionalTransience.commonTrueRecord_time_order line 212
  10. lemma OAI.DirectionalTransience.firstCommonTrueRecord_unique line 231
  11. lemma OAI.DirectionalTransience.firstCommonTrueRecord_exists line 250
  12. def OAI.DirectionalTransience.FirstPairWordEvent line 258
  13. lemma OAI.DirectionalTransience.measurableSet_firstPairWordEvent line 262
  14. lemma OAI.DirectionalTransience.firstPairWordEvent_nil line 267
  15. lemma OAI.DirectionalTransience.firstPairWordEvent_disjoint line 272
  16. lemma OAI.DirectionalTransience.firstPairWordEvent_admissible line 282
  17. def OAI.DirectionalTransience.independentConditionedPairLaw line 288
  18. lemma OAI.DirectionalTransience.independentConditionedPairLaw_probability line 291
  19. lemma OAI.DirectionalTransience.independent_conditioned_firstPairWord_exists line 297
  20. def OAI.DirectionalTransience.firstPairWord line 335
  21. lemma OAI.DirectionalTransience.firstPairWord_eq_iff line 339
  22. lemma OAI.DirectionalTransience.firstPairWord_nil_iff line 355
  23. lemma OAI.DirectionalTransience.measurable_firstPairWord line 367
  24. def OAI.DirectionalTransience.renewPairSuffix line 385
  25. lemma OAI.DirectionalTransience.measurable_renewPairSuffix line 390
  26. lemma OAI.DirectionalTransience.conditioned_record_word_factor line 407