OAI/Computability/MatchingCount/ScaledAlgorithm.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryMatching.Algorithm.argmin_map line 11
  2. lemma OAI.BinaryMatching.Algorithm.argmin_congr_on line 21
  3. lemma OAI.BinaryMatching.Algorithm.argmax_congr_on line 36
  4. def OAI.BinaryMatching.Algorithm.indexedPiece line 41
  5. def OAI.BinaryMatching.Algorithm.pieceNumerator line 44
  6. lemma OAI.BinaryMatching.Algorithm.pieces_indexed line 47
  7. lemma OAI.BinaryMatching.Algorithm.pieceNumerator_cast line 57
  8. def OAI.BinaryMatching.Algorithm.selectedIndex line 71
  9. lemma OAI.BinaryMatching.Algorithm.selectedIndex_mem line 74
  10. lemma OAI.BinaryMatching.Algorithm.selectedIndex_le line 81
  11. lemma OAI.BinaryMatching.Algorithm.selectedPiece_index line 85
  12. def OAI.BinaryMatching.Algorithm.scaledPsi line 105
  13. def OAI.BinaryMatching.Algorithm.scaledSlope line 106
  14. lemma OAI.BinaryMatching.Algorithm.scaledPsi_cast line 108
  15. lemma OAI.BinaryMatching.Algorithm.scaledSlope_eq line 114
  16. def OAI.BinaryMatching.Algorithm.rowNumerator line 121
  17. lemma OAI.BinaryMatching.Algorithm.rowNumerator_cast line 124
  18. def OAI.BinaryMatching.Algorithm.integralRows line 135
  19. lemma OAI.BinaryMatching.Algorithm.integralRows_eq line 139
  20. def OAI.BinaryMatching.Algorithm.integralRow line 142
  21. lemma OAI.BinaryMatching.Algorithm.integralRow_eq line 145
  22. def OAI.BinaryMatching.Algorithm.integralValue line 155
  23. def OAI.BinaryMatching.Algorithm.integralGradient line 159
  24. def OAI.BinaryMatching.Algorithm.integralUpdate line 162
  25. lemma OAI.BinaryMatching.Algorithm.integralGradient_eq line 165
  26. lemma OAI.BinaryMatching.Algorithm.integralUpdate_eq line 170
  27. lemma OAI.BinaryMatching.Algorithm.integralValue_cast line 174
  28. structure OAI.BinaryMatching.Algorithm.IntegralState line 187
  29. def OAI.BinaryMatching.Algorithm.integralStep line 191
  30. def OAI.BinaryMatching.Algorithm.integralInitial line 196
  31. def OAI.BinaryMatching.Algorithm.integralIterate line 198