OAI/Combinatorics/KMedianRecovery/Algorithms/GlobalCall.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.A.run line 11
  2. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.A.pack line 12
  3. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.A.budget line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.pack line 15
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.normInput line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.normInput_computes line 18
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.norm line 19
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.norm_computes line 20
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.src line 21
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.src_computes line 22
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.fcount line 23
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.fcount_computes line 24
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.clamp line 25
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.clamp_computes line 26
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.base line 27
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.base_computes line 29
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.counter line 44
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.demand line 45
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.demand_computes line 46
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.cut line 48
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.cut_computes line 50
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.ready line 52
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.ready_computes line 54
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.call line 69
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.call_computes line 70
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.projectInput line 73
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.projectInput_computes line 75
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.run line 77
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.run_computes line 79
  30. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.matrix line 81
  31. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.integralPack line 84
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.norm_pack line 87
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.right_card line 90
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.clamp_pack line 96
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.base_pack line 101
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.demand_length line 106
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.cut_pack line 109
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.ready_pack line 113
  39. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalCall.run_pack line 119
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.keys line 130
  41. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.keys_nonempty line 132
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.key line 134
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.key_mem line 136
  44. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.key_lt line 139
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.pick line 144
  46. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.pick_mem line 146
  47. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.pick_key line 150
  48. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.pick_min line 155
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.rowRun line 161
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.rowRun_computes line 163
  51. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalZero.rowRun_pack line 165