OAI/Combinatorics/KMedianRecovery/Recovery/Pack4.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.pack line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.target line 11
  3. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.replacement line 12
  4. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.oldInput line 13
  5. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.oldValue line 14
  6. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.target_computes line 15
  7. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.replacement_computes line 17
  8. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.oldInput_computes line 19
  9. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.oldValue_computes line 21
  10. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.op line 23
  11. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.op_computes line 27
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Set.op_ofFn line 33
  13. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.input line 41
  14. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.input_computes line 42
  15. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.run line 44
  16. def OAI.MetricKMedianRecovery.BitMachine.WordList.Set.run_computes line 45
  17. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Set.run_ofFn line 49
  18. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.updateInput line 62
  19. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.updateInput_computes line 65
  20. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.updateColWords line 72
  21. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.updateColWords_computes line 74
  22. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.updateColWords_encode line 80
  23. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.cramerOpInput line 102
  24. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.cramerOpInput_computes line 104
  25. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.cramerOp line 107
  26. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.cramerOp_computes line 109
  27. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.cramerOp_encode line 115
  28. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.cramerInput line 120
  29. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.cramerInput_computes line 121
  30. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.cramerWords line 123
  31. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.cramerWords_computes line 124
  32. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.cramerWords_encode line 129
  33. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.firstDet line 136
  34. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.firstDet_computes line 137
  35. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.inverseDet line 139
  36. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.inverseDet_computes line 140
  37. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.solveInput line 142
  38. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.solveInput_computes line 143
  39. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.solveWords line 144
  40. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.solveWords_computes line 145
  41. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.solveWords_encode line 150
  42. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.solveWords_correct line 157
  43. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.solveWords_bird line 161
  44. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.solve line 182