OAI/Computability/MatchingCount/RawOptimizer.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.Raw.Optimize.value line 11
  2. lemma OAI.BinaryMatching.Raw.Optimize.value_rep line 14
  3. def OAI.BinaryMatching.Raw.Optimize.gradient line 25
  4. lemma OAI.BinaryMatching.Raw.Optimize.gradient_rep line 27
  5. def OAI.BinaryMatching.Raw.Optimize.update line 33
  6. lemma OAI.BinaryMatching.Raw.Optimize.update_rep line 35
  7. def OAI.BinaryMatching.Raw.Optimize.step line 46
  8. def OAI.BinaryMatching.Raw.Optimize.initial line 51
  9. lemma OAI.BinaryMatching.Raw.Optimize.initial_rep line 52
  10. lemma OAI.BinaryMatching.Raw.Optimize.step_rep line 58
  11. lemma OAI.BinaryMatching.Raw.Optimize.step_iterate_rep line 64
  12. lemma OAI.BinaryMatching.Raw.Optimize.integralIterate_lower line 70
  13. lemma OAI.BinaryMatching.Raw.Optimize.integralIterate_all_abs line 75
  14. def OAI.BinaryMatching.Raw.Optimize.operandBound line 82
  15. def OAI.BinaryMatching.Raw.Optimize.budget line 83
  16. lemma OAI.BinaryMatching.Raw.Optimize.state_code_bound line 86
  17. def OAI.BinaryMatching.Raw.Optimize.run line 111
  18. lemma OAI.BinaryMatching.Raw.Optimize.run_rep line 113
  19. def OAI.BinaryMatching.Raw.Optimize.result line 122
  20. lemma OAI.BinaryMatching.Raw.Optimize.result_rep line 123