OAI/Probability/Ballisticity/Estimates/AdaptiveFailureWeights.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.successes line 14
  2. def OAI.DirectionalTransience.failureWeight line 16
  3. lemma OAI.DirectionalTransience.successes_nonneg line 19
  4. lemma OAI.DirectionalTransience.successes_succ line 23
  5. lemma OAI.DirectionalTransience.measurable_successes line 26
  6. lemma OAI.DirectionalTransience.measurable_failureWeight line 31
  7. lemma OAI.DirectionalTransience.failureWeight_integrable line 34
  8. lemma OAI.DirectionalTransience.failureWeight_step line 44
  9. lemma OAI.DirectionalTransience.failureWeight_contraction line 58
  10. lemma OAI.DirectionalTransience.adaptive_failureWeight_mean line 75
  11. def OAI.DirectionalTransience.failureSeries line 122
  12. lemma OAI.DirectionalTransience.measurable_failureSeries line 125
  13. lemma OAI.DirectionalTransience.failureSeries_mean line 129
  14. theorem OAI.DirectionalTransience.adaptive_failure_excess line 152