OAI/Combinatorics/KMedianRecovery/Machines/GridMachine.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.cf line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.gf line 11
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.cf_computes line 12
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.gf_computes line 13
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.num line 14
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.den line 15
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.num_computes line 16
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.den_computes line 17
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.pointWords line 18
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.pointWords_computes line 21
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.pointWords_pack line 25
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.doubled line 29
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.doubled_computes line 30
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.summed line 33
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.summed_computes line 34
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.midpoint line 35
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.midpoint_computes line 36
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.queryInput line 38
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.queryInput_computes line 39
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.chooseLeft line 40
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.chooseLeft_computes line 42
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.upLeft line 44
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.upRight line 45
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.upLeft_computes line 46
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.upRight_computes line 53
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.step line 60
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.step_computes line 62
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.stateBits line 64
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.count line 65
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.boundK line 67
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.lower line 68
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.upper line 69
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.step_pack line 70
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.iterate_pack line 78
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.bits_of_le_pow line 84
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.iterate_length line 90
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.capacity line 100
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.initial line 101
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.initial_computes line 102
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.runInput line 103
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.runInput_computes line 104
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.stateRun line 105
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.stateRun_computes line 106
  44. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.stateRun_pack line 108
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.endpoint line 117
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.endpoint_computes line 118
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.finish line 120
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.finish_computes line 121
  49. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.finish_pack line 122
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.run line 128
  51. def OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.run_computes line 129
  52. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGrid.run_pack line 131