OAI/Combinatorics/KMedianRecovery/Branching/BlueBlocksMachine.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.labelsEnc line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.itemCall line 10
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.itemCall_computes line 12
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.atCenter line 15
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.at_computes line 16
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.at_pack line 17
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.atCall line 25
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.atCall_computes line 27
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.run line 30
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.run_computes line 31
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueBlocks.run_pack line 32