OAI/Probability/Ballisticity/Estimates/StayUntil.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.StayUntil line 12
  2. def OAI.DirectionalTransience.Stay line 15
  3. lemma OAI.DirectionalTransience.measurableSet_stayUntil line 18
  4. lemma OAI.DirectionalTransience.measurableSet_stay line 24
  5. lemma OAI.DirectionalTransience.restrict_prefix_fiber line 30
  6. lemma OAI.DirectionalTransience.quenched_stayUntil_congr line 43
  7. lemma OAI.DirectionalTransience.quenched_stay_congr line 73
  8. lemma OAI.DirectionalTransience.measurable_stay_rows line 89
  9. lemma OAI.DirectionalTransience.measurable_noDropQuenched_rows line 109
  10. lemma OAI.DirectionalTransience.noDropQuenched_lower_step line 115
  11. lemma OAI.DirectionalTransience.dot_realPosition_nsmul line 140
  12. lemma OAI.DirectionalTransience.noDrop_positive_limsup line 148
  13. lemma OAI.DirectionalTransience.noDropQuenched_positive_ae line 208
  14. lemma OAI.DirectionalTransience.annealed_record_noDrop line 241
  15. lemma OAI.DirectionalTransience.quenched_futureNoDrop_zero line 272
  16. lemma OAI.DirectionalTransience.noDrop_positive_of_directionallyTransient line 297
  17. lemma OAI.DirectionalTransience.measure_partition_prefix line 324
  18. lemma OAI.DirectionalTransience.lintegral_partition_prefix line 339
  19. def OAI.DirectionalTransience.FutureEvent line 352
  20. lemma OAI.DirectionalTransience.measurableSet_futureEvent line 355
  21. lemma OAI.DirectionalTransience.quenched_past_future line 372