OAI/Computability/MatchingCount/RawOptimizerDataCompiler.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.paramsRepr_poly line 11
  2. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.paramsOfData_poly line 13
  3. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.params_n line 15
  4. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.params_q line 17
  5. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.params_k line 19
  6. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.params_L line 21
  7. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.params_D line 23
  8. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.params_M line 25
  9. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.params_pow line 27
  10. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.params_beta line 29
  11. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.doubleIntSum line 32
  12. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.upperSum_poly line 40
  13. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.rowNumerator_poly line 46
  14. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.indexedSlope_poly line 53
  15. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.pieceNumerator_poly line 57
  16. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.selectedIndex_poly line 63
  17. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.selectedIndex_params_poly line 73
  18. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.scaledPsi_poly line 75
  19. theorem OAI.BinaryMatching.Raw.Optimize.Compiler.scaledSlope_poly line 78