OAI/Probability/Ballisticity/Estimates/FirstWordEvent.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.exists_nextRecordAfter line 12
  2. lemma OAI.DirectionalTransience.annealed_trueRecords_unbounded line 21
  3. lemma OAI.DirectionalTransience.annealed_firstTrueRecord_exists line 83
  4. lemma OAI.DirectionalTransience.annealed_ae_of_quenched line 92
  5. lemma OAI.DirectionalTransience.annealed_initial line 102
  6. lemma OAI.DirectionalTransience.annealed_nearest_neighbor line 107
  7. lemma OAI.DirectionalTransience.exists_word_prefix line 116
  8. lemma OAI.DirectionalTransience.word_eq_of_paths line 137
  9. lemma OAI.DirectionalTransience.word_eq_of_cylinders line 159
  10. def OAI.DirectionalTransience.FirstWordEvent line 166
  11. lemma OAI.DirectionalTransience.measurableSet_firstWordEvent line 169
  12. lemma OAI.DirectionalTransience.firstWordEvent_nil line 174
  13. lemma OAI.DirectionalTransience.firstWordEvent_disjoint line 178
  14. lemma OAI.DirectionalTransience.firstWordEvent_eq line 186
  15. lemma OAI.DirectionalTransience.conditionedLaw_absolutelyContinuous line 198
  16. lemma OAI.DirectionalTransience.conditionedLaw_noDrop line 202
  17. lemma OAI.DirectionalTransience.conditioned_firstWord_exists line 206
  18. instance OAI.DirectionalTransience.wordMeasurableSpace line 217
  19. instance OAI.DirectionalTransience.wordDiscreteMeasurable line 219
  20. def OAI.DirectionalTransience.firstWord line 222
  21. lemma OAI.DirectionalTransience.firstWord_eq_iff line 225
  22. lemma OAI.DirectionalTransience.firstWord_nil_iff line 239
  23. lemma OAI.DirectionalTransience.measurable_firstWord line 251
  24. lemma OAI.DirectionalTransience.conditionedLaw_inter_noDrop line 269
  25. lemma OAI.DirectionalTransience.conditionedLaw_noDrop_mass line 276
  26. lemma OAI.DirectionalTransience.conditioned_firstWordEvent_mass line 283
  27. lemma OAI.DirectionalTransience.firstWordEvent_empty_of_not_admissible line 290
  28. lemma OAI.DirectionalTransience.conditioned_firstWordEvent_factor line 295
  29. def OAI.DirectionalTransience.renewSuffix line 317
  30. lemma OAI.DirectionalTransience.measurable_renewSuffix line 320
  31. lemma OAI.DirectionalTransience.renewSuffix_on_firstWordEvent line 330
  32. lemma OAI.DirectionalTransience.conditioned_firstWord_fiber_ae line 340
  33. lemma OAI.DirectionalTransience.conditioned_firstWord_fiber_factor line 353
  34. lemma OAI.DirectionalTransience.renewSuffix_preserves_conditioned line 375
  35. lemma OAI.DirectionalTransience.measure_preimage_partition line 402
  36. lemma OAI.DirectionalTransience.firstWord_indep_renewSuffix line 411
  37. lemma OAI.DirectionalTransience.independent_iterated_symbols line 425