OAI/Combinatorics/KMedianRecovery/Encoding/ColorLabelMachine.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.colorWord line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.colorWord_computes line 14
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.colorWord_bits line 19
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.colors line 23
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.colors_computes line 25
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.colors_tensor line 28
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.labelOp line 42
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.labelOp_computes line 43
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.labels line 44
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.labels_computes line 46
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryColorLabel.labels_tensor line 48
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.op line 62
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.op_computes line 64
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.op_pack line 66
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.capPoly line 69
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.cap line 70
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.pack line 71
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.items line 72
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.items_computes line 73
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.prepared line 74
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.prepared_computes line 76
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.run line 78
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.run_computes line 79
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.fold_mul line 80
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalPower.run_pack line 84
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalMinKey.run line 108
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalMinKey.run_computes line 109
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalMinKey.head_encode line 110
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalMinKey.run_pack line 115