OAI/Probability/Ballisticity/Estimates/SurvivingLane.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.SurvivingLane line 108
  2. lemma OAI.DirectionalTransience.measurableSet_survivingLane line 111
  3. lemma OAI.DirectionalTransience.future_stay_iff line 115
  4. lemma OAI.DirectionalTransience.future_hit_iff line 127
  5. lemma OAI.DirectionalTransience.hit_survival_factorization line 149
  6. lemma OAI.DirectionalTransience.hit_laneError_factorization line 164
  7. lemma OAI.DirectionalTransience.hitKernel_ae_target line 186
  8. lemma OAI.DirectionalTransience.quenched_lowLane_visit_bound line 194
  9. lemma OAI.DirectionalTransience.survivingLane_disjoint line 218
  10. lemma OAI.DirectionalTransience.measure_low_complement_or line 231
  11. def OAI.DirectionalTransience.PrefixContact line 246
  12. lemma OAI.DirectionalTransience.measurableSet_prefixContact line 249
  13. lemma OAI.DirectionalTransience.prefix_visit_first line 263
  14. lemma OAI.DirectionalTransience.quenched_pair_contact_bound line 274
  15. lemma OAI.DirectionalTransience.shared_pair_contact_bound line 309