OAI/Probability/Ballisticity/Crossings/TailCuts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TailCuts.score line 12
  2. lemma OAI.TailCuts.maximizing_cuts_escape line 14
  3. lemma OAI.TailCuts.exists_maximizing_cut line 62
  4. def OAI.TailCuts.lower line 82
  5. def OAI.TailCuts.upper line 83
  6. lemma OAI.TailCuts.lower_pos line 85
  7. lemma OAI.TailCuts.upper_pos line 89
  8. lemma OAI.TailCuts.lower_strictMono line 93
  9. lemma OAI.TailCuts.upper_strictAnti line 113
  10. lemma OAI.TailCuts.lower_tendsto line 133
  11. lemma OAI.TailCuts.upper_tendsto line 149
  12. theorem OAI.TailCuts.finite_profile_cuts_escape line 165
  13. lemma OAI.TailCuts.measurable_maximizing_cut line 180