OAI/Combinatorics/KMedianRecovery/Geometry/RoundingMatrix.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.round line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.pack line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.ctx line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.rowIndex line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.colIndex line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.ctx_computes line 18
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.rowIndex_computes line 19
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.colIndex_computes line 20
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.distance line 21
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.distance_computes line 23
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.entryInput line 27
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.entryInput_computes line 28
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.entry line 36
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.entry_computes line 38
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.entry_pack line 43
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.row line 56
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.row_computes line 58
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.row_pack line 63
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.run line 69
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.run_computes line 71
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRoundingMatrix.run_pack line 75