OAI/Probability/Ballisticity/Estimates/CommonLayer.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.CommonLayer line 151
  2. lemma OAI.DirectionalTransience.measurableSet_commonLayer line 156
  3. lemma OAI.DirectionalTransience.failure_visible_or_late line 165
  4. lemma OAI.DirectionalTransience.commonLayer_failure_cover line 179
  5. lemma OAI.DirectionalTransience.shared_conditioned_raw_bound line 200
  6. def OAI.DirectionalTransience.singleWidthTail line 215
  7. lemma OAI.DirectionalTransience.singleWidthTail_nonneg line 219
  8. lemma OAI.DirectionalTransience.singleWidthTail_tendsto line 227
  9. def OAI.DirectionalTransience.NoCommonGrid line 251
  10. lemma OAI.DirectionalTransience.measurableSet_noCommonGrid line 254
  11. theorem OAI.DirectionalTransience.shared_no_common_grid_bound line 260
  12. def OAI.DirectionalTransience.NoCommonInterval line 348
  13. lemma OAI.DirectionalTransience.measurableSet_noCommonInterval line 351
  14. theorem OAI.DirectionalTransience.shared_common_overshoot_tight line 357