OAI/Computability/MatchingCount/RawOptimizerData.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryMatching.Raw.Optimize.Row line 11
  2. abbrev OAI.BinaryMatching.Raw.Optimize.IntState line 12
  3. structure OAI.BinaryMatching.Raw.Optimize.Params line 13
  4. abbrev OAI.BinaryMatching.Raw.Optimize.ParamData line 23
  5. def OAI.BinaryMatching.Raw.Optimize.Params.repr line 24
  6. instance OAI.BinaryMatching.Raw.Optimize.(instance at line 25) line 25
  7. def OAI.BinaryMatching.Raw.Optimize.Params.ofData line 26
  8. lemma OAI.BinaryMatching.Raw.Optimize.Params.ofData_repr line 28
  9. def OAI.BinaryMatching.Raw.Optimize.tableRep line 30
  10. def OAI.BinaryMatching.Raw.Optimize.rowRep line 31
  11. def OAI.BinaryMatching.Raw.Optimize.stateRep line 32
  12. def OAI.BinaryMatching.Raw.Optimize.params line 33
  13. def OAI.BinaryMatching.Raw.Optimize.upperSum line 35
  14. lemma OAI.BinaryMatching.Raw.Optimize.upperSum_rep line 38
  15. lemma OAI.BinaryMatching.Raw.Optimize.get_tableRep line 61
  16. lemma OAI.BinaryMatching.Raw.Optimize.get_rowRep line 63
  17. lemma OAI.BinaryMatching.Raw.Optimize.get_beta line 66
  18. def OAI.BinaryMatching.Raw.Optimize.rowNumerator line 71
  19. lemma OAI.BinaryMatching.Raw.Optimize.tableRep_length line 73
  20. lemma OAI.BinaryMatching.Raw.Optimize.rowNumerator_rep line 74
  21. def OAI.BinaryMatching.Raw.Optimize.indexedSlope line 84
  22. def OAI.BinaryMatching.Raw.Optimize.pieceNumerator line 85
  23. lemma OAI.BinaryMatching.Raw.Optimize.pieceNumerator_rep line 87
  24. def OAI.BinaryMatching.Raw.Optimize.selectedIndex line 94
  25. lemma OAI.BinaryMatching.Raw.Optimize.selectedIndex_rep line 96
  26. def OAI.BinaryMatching.Raw.Optimize.scaledPsi line 99
  27. def OAI.BinaryMatching.Raw.Optimize.scaledSlope line 100
  28. lemma OAI.BinaryMatching.Raw.Optimize.scaledPsi_rep line 101
  29. lemma OAI.BinaryMatching.Raw.Optimize.scaledSlope_rep line 103