OAI/Combinatorics/KMedianRecovery/Machines/LoopSize.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.components line 10
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.base_dimension line 19
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.capPoly line 29
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.capPoly_eval line 30
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.outcome_length_bound line 35
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.pack_length_bound line 54
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.capacity line 71
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.iterationInput line 72
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.iterationInput_computes line 73
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.stateRun line 75
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.stateRun_computes line 76
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.run line 78
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.run_computes line 79
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.run_pack line 86