OAI/Combinatorics/KMedianRecovery/Recovery/Pack9.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.pack line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.nword line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.rest₁ line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.mword line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.rest₂ line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.bound line 19
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.rest₃ line 20
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.height line 21
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.rows line 22
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.nword_computes line 23
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.rest₁_computes line 24
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.mword_computes line 25
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.rest₂_computes line 26
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.bound_computes line 27
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.rest₃_computes line 28
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.height_computes line 29
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.rows_computes line 30
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.projections_pack line 31
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.dim line 37
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.count line 38
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.dim_computes line 39
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.count_computes line 40
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.dim_pack line 41
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.count_pack line 43
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.nextDim line 46
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.nextDim_computes line 47
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.nextDim_pack line 48
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.rowFactor line 51
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.rowFactor_computes line 53
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.base line 58
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.base_computes line 59
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.power line 63
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.power_computes line 64
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.factorial line 65
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.factorial_computes line 66
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.gap line 67
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.gap_computes line 68
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.gap_pack line 69
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.doubledGap line 75
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.doubledGap_computes line 76
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.epsilon line 80
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.epsilon_computes line 81
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.epsilon_pack line 82
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.precisionArg line 85
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.precisionArg_computes line 86
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.precision line 87
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.precision_computes line 88
  48. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.precision_pack line 89
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.radius line 93
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.radius_computes line 94
  51. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.radius_pack line 98
  52. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.radiusPrecision line 101
  53. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.radiusPrecision_computes line 102
  54. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.radiusPrecision_pack line 103