OAI/Probability/Ballisticity/Estimates/SingleCoverWord.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.singleCoverWord line 146
  2. lemma OAI.DirectionalTransience.measurable_countable_select line 150
  3. lemma OAI.DirectionalTransience.measurable_singleCoverWord line 156
  4. lemma OAI.DirectionalTransience.single_width_positive line 165
  5. theorem OAI.DirectionalTransience.single_cover_event_bound line 171
  6. lemma OAI.DirectionalTransience.single_cover_tail_small line 186
  7. lemma OAI.DirectionalTransience.late_failure_cover_width line 198
  8. lemma OAI.DirectionalTransience.conditionedFrom_recenter line 246
  9. lemma OAI.DirectionalTransience.shared_recenter_marginal_bound line 258
  10. lemma OAI.DirectionalTransience.shared_recenter_marginal_bound_snd line 284
  11. lemma OAI.DirectionalTransience.height_sub line 296
  12. def OAI.DirectionalTransience.LateFailure line 303
  13. lemma OAI.DirectionalTransience.measurableSet_lateFailure line 306
  14. lemma OAI.DirectionalTransience.lateFailure_recenter line 314
  15. lemma OAI.DirectionalTransience.conditioned_late_failure_bound line 328