OAI/Combinatorics/KMedianRecovery/Recovery/Pack6.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.pack line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.dim line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.rest line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.precision line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.shape line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.dim_computes line 19
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.precision_computes line 20
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.shape_computes line 21
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.dim_pack line 22
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.precision_pack line 24
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.shape_pack line 26
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.ctx line 29
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.row line 30
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.col line 31
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.ctx_computes line 32
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.row_computes line 33
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.col_computes line 34
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.entryInput line 36
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.entryInput_computes line 37
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.entry line 39
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.entry_computes line 40
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.entry_pack line 41
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.dimension line 46
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.scale line 47
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.dimension_computes line 48
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.scale_computes line 50
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.qvalue line 52
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.qvalue_computes line 53
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.floorValue line 54
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.floorValue_computes line 55
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.diagonal line 57
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.diagonal_computes line 58
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.entryWords line 60
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.entryWords_computes line 65
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.entryWords_pack line 71
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.rowInput line 88
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.rowInput_computes line 89
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.rowWords line 91
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.rowWords_computes line 92
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.rowWords_pack line 93
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.runInput line 100
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.runInput_computes line 101
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.run line 103
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.run_computes line 104
  45. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidGrid.run_pack line 105
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.gridInput line 113
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.gridInput_computes line 114
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.shapeWords line 115
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.shapeWords_computes line 116
  50. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.shapeWords_pack line 117