OAI/Combinatorics/PerfectMatching/Ascent.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryMatching.Algorithm.q_pos line 11
  2. lemma OAI.BinaryMatching.Algorithm.Dā‚€_pos line 15
  3. lemma OAI.BinaryMatching.Algorithm.clip_sq_le line 19
  4. lemma OAI.BinaryMatching.Algorithm.update_box line 31
  5. lemma OAI.BinaryMatching.Algorithm.iterate_box line 36
  6. def OAI.BinaryMatching.Algorithm.point line 42
  7. def OAI.BinaryMatching.Algorithm.sampledValue line 45
  8. lemma OAI.BinaryMatching.Algorithm.coordinates_cast line 48
  9. lemma OAI.BinaryMatching.Algorithm.point_box line 52
  10. lemma OAI.BinaryMatching.Algorithm.point_zero line 61
  11. lemma OAI.BinaryMatching.Algorithm.point_succ line 64
  12. lemma OAI.BinaryMatching.Algorithm.sampledValue_correct line 73
  13. lemma OAI.BinaryMatching.Algorithm.best_spec line 77
  14. def OAI.BinaryMatching.Algorithm.squareDistance line 101
  15. lemma OAI.BinaryMatching.Algorithm.squareDistance_nonneg line 104
  16. lemma OAI.BinaryMatching.Algorithm.squareDistance_zero_bound line 107
  17. lemma OAI.BinaryMatching.Algorithm.distance_step line 115
  18. lemma OAI.BinaryMatching.Algorithm.trial_max_bound line 149
  19. theorem OAI.BinaryMatching.Algorithm.R_objective_bracket line 187