OAI/Computability/MinUncut/Graphs/HonestComparisons.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Inner.score_query line 18
  2. lemma OAI.MinUncut.Inner.score_add_noise line 23
  3. lemma OAI.MinUncut.Inner.firstFailure_evaluation line 33
  4. lemma OAI.MinUncut.Inner.firstRejection_evaluation_le line 42
  5. lemma OAI.MinUncut.Inner.firstError_evaluation_le line 48
  6. lemma OAI.MinUncut.Inner.secondFailure_evaluation line 54
  7. lemma OAI.MinUncut.Inner.secondRejection_evaluation_le line 63
  8. lemma OAI.MinUncut.Inner.thirdFailure_evaluation line 84
  9. lemma OAI.MinUncut.Inner.thirdRejection_evaluation line 93
  10. lemma OAI.MinUncut.Inner.thirdError_evaluation line 99
  11. lemma OAI.MinUncut.Inner.codeVector_distance_sq line 113
  12. lemma OAI.MinUncut.Inner.noise_vector_sq line 119
  13. lemma OAI.MinUncut.Inner.noise_vector_sq_le line 125
  14. lemma OAI.MinUncut.Inner.weighted_expect_sq line 143
  15. lemma OAI.MinUncut.Inner.noise_vector_le line 155