OAI/Computability/MinUncut/Graphs/HonestBudgets.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Inner.secondError_evaluation_le line 15
  2. lemma OAI.MinUncut.Inner.honest_first_budget line 38
  3. lemma OAI.MinUncut.Inner.honest_second_budget line 46
  4. lemma OAI.MinUncut.Inner.labelCode_pullback line 62
  5. lemma OAI.MinUncut.Inner.fourthError_evaluation line 69
  6. lemma OAI.MinUncut.Inner.fourthError_le_one line 74
  7. def OAI.MinUncut.Outer.honestProof line 88
  8. lemma OAI.MinUncut.Outer.honest_fourth_point line 92
  9. lemma OAI.MinUncut.Outer.failure_fraction line 107
  10. lemma OAI.MinUncut.Outer.honest_fourth_mean line 114
  11. lemma OAI.MinUncut.Outer.honest_errors_le line 129
  12. lemma OAI.MinUncut.Outer.honest_cost_le line 147