OAI/Combinatorics/KMedianRecovery/Recovery/Rectangular.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.Rectangular.encode line 15
  2. lemma OAI.MetricKMedianRecovery.BitMachine.Rectangular.columnOp_encode line 17
  3. def OAI.MetricKMedianRecovery.BitMachine.Rectangular.transpose line 21
  4. def OAI.MetricKMedianRecovery.BitMachine.Rectangular.transpose_computes line 23
  5. lemma OAI.MetricKMedianRecovery.BitMachine.Rectangular.transpose_encode line 31
  6. lemma OAI.MetricKMedianRecovery.BitMachine.Rectangular.rightRowOp_encode line 36
  7. lemma OAI.MetricKMedianRecovery.BitMachine.Rectangular.gram_encode line 43
  8. lemma OAI.MetricKMedianRecovery.BitMachine.Rectangular.mulVec_encode line 50
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.coeffs line 63
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.coeffs_computes line 64
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.coeffs_encode line 69
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.bounds line 75
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.bounds_computes line 76
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.bounds_encode line 81
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.transposed line 86
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.transposed_computes line 88
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.transposed_pack line 96
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.gram line 99
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.gram_computes line 100
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.gram_pack line 105
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.rhs line 108
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.rhs_computes line 110
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.rhs_pack line 118
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.point line 121
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.point_computes line 122
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.point_pack line 127
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.run line 141
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.run_computes line 143
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.resultBits line 146
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.run_pack line 149
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.computation line 158
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.sound line 162
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryExactSolve.complete line 165