OAI/Combinatorics/KMedianRecovery/Recovery/Pack11.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.event_length line 9
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.finish_event_length line 30
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.finish_count line 46
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.pack line 54
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.answer line 57
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.answer_computes line 58
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.step line 59
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.step_computes line 62
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.step_pack line 69
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.iterate_pack line 83
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.traceCapPoly line 94
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.iterate_length line 95
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.resource line 121
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.loop line 122
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.loop_computes line 124
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.run line 128
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.run_computes line 130
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseTrace.run_pack line 132