OAI/Computability/MatchingCount/RawOptimizerCompiler.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.value_poly line 11
  2. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.gradient_poly line 19
  3. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.update_poly line 21
  4. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.step_poly line 29
  5. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.initial_poly line 42
  6. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.operandBound_poly line 46
  7. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.budget_poly line 47
  8. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.run_poly line 48
  9. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.result_poly line 52