OAI/Probability/SKBarriers/Coverage/HighProbability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.high_probability_inter line 14
  2. def OAI.SK.Analytic.finiteGoodEvent line 30
  3. theorem OAI.SK.Analytic.finiteGoodEvent_mem line 34
  4. theorem OAI.SK.Analytic.finiteGoodEvent_measurable line 47
  5. theorem OAI.SK.Analytic.finiteGoodEvent_tendsto line 53
  6. theorem OAI.SK.Analytic.real_markov_bound line 61
  7. theorem OAI.SK.Analytic.stretched_exp_decay line 74
  8. theorem OAI.SK.Analytic.faster_stretched_decay line 78
  9. theorem OAI.SK.Analytic.high_probability_small_replica line 91