OAI/Combinatorics/KMedianRecovery/Branching/BlueLookup.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLookup.encode line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLookup.matchKey line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLookup.matchKey_computes line 14
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLookup.run line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLookup.run_computes line 17
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLookup.run_pack line 18
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.encode_injective line 35
  8. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.atomEnc line 52
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.ctxPack line 53
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.ctx line 57
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.ctx_computes line 58
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.whole line 59
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.whole_computes line 60
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.block line 61
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.block_computes line 63
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.old line 66
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.old_computes line 68
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.op line 71
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.op_computes line 72
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.finValBits_injective line 76
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.op_pack line 80
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.run line 91
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.run_computes line 93
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.subset_capacity line 97
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCell.run_pack line 112