OAI/Combinatorics/KMedianRecovery/Machines/CoupledPrimitives.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.makeLeaf line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.makeLeaf_computes line 11
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.makeLeaf_pack line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.advance line 26
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.advance_computes line 29
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.advance_pack line 42
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.leafPack line 48
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.endLeaf line 52
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.endLeaf_computes line 53
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.endLeaf_pack line 55
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.leafBank line 60
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.leafBank_computes line 61
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.leafPrefix line 62
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.leafPrefix_computes line 63
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.leafResult line 65
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.leafResult_computes line 67
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.leafResult_pack line 76