OAI/Combinatorics/KMedianRecovery/Branching/ObservableCapacity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryObservableBranch.source_run line 8
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedBranch.run line 35
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedBranch.run_computes line 37
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedBranch.source_run line 40
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.pack line 61
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.rhs line 64
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.rhs_computes line 66
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.check line 70
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.check_computes line 73
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.completion line 80
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.completion_computes line 82
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.run line 88
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.run_computes line 92
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.output line 98
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.check_pack line 110
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.completion_pack line 123
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryZeroBranch.run_pack line 142