OAI/Computability/MinUncut/Estimates/ComparisonSoundness.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Inner.firstError_nonneg line 14
  2. lemma OAI.MinUncut.Inner.secondError_nonneg line 16
  3. lemma OAI.MinUncut.Inner.thirdError_nonneg line 21
  4. inductive OAI.MinUncut.Outer.Test line 32
  5. instance OAI.MinUncut.Outer.(instance at line 33) line 33
  6. def OAI.MinUncut.Outer.ProofFamily.testErrors line 37
  7. def OAI.MinUncut.Outer.budgets line 48
  8. lemma OAI.MinUncut.Outer.budgets_pos line 54
  9. lemma OAI.MinUncut.Outer.edgeMean_nonneg line 66
  10. lemma OAI.MinUncut.Outer.fourthError_nonneg line 71
  11. lemma OAI.MinUncut.Outer.ProofFamily.testErrors_nonneg line 82
  12. def OAI.MinUncut.Outer.ProofFamily.cost line 94
  13. lemma OAI.MinUncut.Outer.ProofFamily.error_le_of_cost line 99
  14. lemma OAI.MinUncut.Outer.ProofFamily.cost_atom_lower line 108
  15. lemma OAI.MinUncut.Outer.ProofFamily.cost_atom_upper line 119
  16. theorem OAI.MinUncut.Outer.ProofFamily.cost_gt line 135