OAI/Combinatorics/KMedianRecovery/Machines/DeleteSize.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.capacityPoly line 14
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.accBits_bound line 18
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.capacity line 38
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.run line 39
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.run_computes line 40
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.pack line 43
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.pack_bounds line 47
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDelete.run_pack line 65
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.pack line 117
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.deletionInput line 119
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.deletionInput_computes line 121
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.deleted line 133
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.deleted_computes line 134
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.suffix line 135
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.suffix_computes line 136
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.firstVertex line 137
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.firstVertex_computes line 138
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.lastVertex line 140
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.lastVertex_computes line 141
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.vertices line 143
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.vertices_computes line 145
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.run line 148
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.run_computes line 149
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.deleted_pack line 156
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryAdvance.run_pack line 166