OAI/Combinatorics/KMedianRecovery/Recovery/Pack5.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.pack line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.dim line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.rest line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.shape line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.rest₂ line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.direction line 19
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.rest₃ line 20
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.center line 21
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.precision line 22
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.dim_computes line 23
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.rest_computes line 24
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.shape_computes line 25
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.rest₂_computes line 26
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.direction_computes line 27
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.rest₃_computes line 28
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.center_computes line 29
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.precision_computes line 30
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.dim_pack line 31
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.shape_pack line 33
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.direction_pack line 36
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.center_pack line 39
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.precision_pack line 42
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.haInput line 46
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.haInput_computes line 47
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.haWords line 48
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.haWords_computes line 49
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.quadWords line 50
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.quadWords_computes line 51
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.haWords_pack line 52
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.quadWords_pack line 55
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.dimension line 59
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.dimension_computes line 60
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.qvalue line 61
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.qvalue_computes line 62
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.coefA line 64
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.coefA_computes line 65
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.coefB line 70
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.coefB_computes line 71
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.coefInflate line 73
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.coefInflate_computes line 74
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.rootPrecision line 81
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.rootPrecision_computes line 82
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.root_computes line 86
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.coefCenter line 89
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.coefCenter_computes line 91
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.scaledHaInput line 94
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.scaledHaInput_computes line 95
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.scaledHa line 96
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.scaledHa_computes line 97
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.centerInput line 98
  51. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.centerInput_computes line 99
  52. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.centerWords line 100
  53. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.centerWords_computes line 101
  54. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.centerWords_pack line 102
  55. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.outerInput line 109
  56. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.outerInput_computes line 110
  57. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.outerWords line 111
  58. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.outerWords_computes line 112
  59. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.scaledOuterInput line 113
  60. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.scaledOuterInput_computes line 114
  61. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.scaledOuter line 115
  62. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.scaledOuter_computes line 116
  63. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.differenceInput line 117
  64. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.differenceInput_computes line 118
  65. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.difference line 119
  66. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.difference_computes line 120
  67. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.cutInput line 121
  68. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.cutInput_computes line 122
  69. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.cutWords line 123
  70. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.cutWords_computes line 124
  71. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.inflateInput line 125
  72. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.inflateInput_computes line 126
  73. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.inflateWords line 127
  74. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.inflateWords_computes line 128
  75. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidCut.inflateWords_pack line 129