OAI/Computability/MatchingCount/BinaryAlgorithm.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryMatching.Algorithm.Table line 11
  2. def OAI.BinaryMatching.Algorithm.tabulate line 13
  3. def OAI.BinaryMatching.Algorithm.entry line 16
  4. theorem OAI.BinaryMatching.Algorithm.at_tabulate line 18
  5. def OAI.BinaryMatching.Algorithm.toTable line 21
  6. theorem OAI.BinaryMatching.Algorithm.at_toTable line 24
  7. def OAI.BinaryMatching.Algorithm.capacities line 27
  8. def OAI.BinaryMatching.Algorithm.q line 30
  9. def OAI.BinaryMatching.Algorithm.K line 31
  10. def OAI.BinaryMatching.Algorithm.B line 32
  11. def OAI.BinaryMatching.Algorithm.L line 33
  12. def OAI.BinaryMatching.Algorithm.Aâ‚€ line 34
  13. def OAI.BinaryMatching.Algorithm.Mâ‚€ line 35
  14. def OAI.BinaryMatching.Algorithm.Dâ‚€ line 36
  15. def OAI.BinaryMatching.Algorithm.beta line 38
  16. structure OAI.BinaryMatching.Algorithm.Piece line 41
  17. def OAI.BinaryMatching.Algorithm.Piece.eval line 46
  18. def OAI.BinaryMatching.Algorithm.pieces line 48
  19. def OAI.BinaryMatching.Algorithm.selectedPiece line 51
  20. def OAI.BinaryMatching.Algorithm.psi line 54
  21. def OAI.BinaryMatching.Algorithm.slope line 56
  22. structure OAI.BinaryMatching.Algorithm.Affine line 58
  23. def OAI.BinaryMatching.Algorithm.Affine.eval line 62
  24. def OAI.BinaryMatching.Algorithm.zeroRow line 65
  25. def OAI.BinaryMatching.Algorithm.degreeRow line 66
  26. def OAI.BinaryMatching.Algorithm.cutRow line 69
  27. def OAI.BinaryMatching.Algorithm.activeRows line 72
  28. def OAI.BinaryMatching.Algorithm.coordinates line 76
  29. def OAI.BinaryMatching.Algorithm.activeRow line 78
  30. def OAI.BinaryMatching.Algorithm.trialValue line 81
  31. def OAI.BinaryMatching.Algorithm.gradient line 85
  32. def OAI.BinaryMatching.Algorithm.update line 88
  33. structure OAI.BinaryMatching.Algorithm.State line 91
  34. def OAI.BinaryMatching.Algorithm.step line 95
  35. def OAI.BinaryMatching.Algorithm.initial line 100
  36. def OAI.BinaryMatching.Algorithm.iterate line 102
  37. def OAI.BinaryMatching.Algorithm.R line 106
  38. def OAI.BinaryMatching.Algorithm.estimate line 108
  39. def OAI.BinaryMatching.Algorithm.covered line 112
  40. def OAI.BinaryMatching.Algorithm.rawMultiplicity line 115
  41. def OAI.BinaryMatching.Algorithm.approximate line 118