OAI/Combinatorics/KMedianRecovery/Recovery/BoundOp.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boundOp line 14
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boundOp_computes line 15
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boundOp_pair line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boxShape line 19
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boxShape_computes line 21
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boxShape_pack line 29
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boxWords line 41
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boxWords_computes line 43
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boxWords_pack line 51
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boundedWords line 55
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boundedWords_computes line 56
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.boundedWords_pack line 58
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.relaxedOp line 63
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.relaxedOp_computes line 66
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.relaxedOp_pair line 70
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.relaxedWords line 74
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.relaxedWords_computes line 75
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.relaxedWords_pack line 81
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.prepared line 85
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.prepared_computes line 87
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.prepared_pack line 89
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.solved line 94
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.solved_computes line 95
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.run line 96
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.run_computes line 97
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.run_pack line 103
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDecision.run_correct line 110
  28. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.signedOp line 122
  29. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.signedOp_computes line 123
  30. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.sumWords line 124
  31. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.sumWords_computes line 126
  32. lemma OAI.MetricKMedianRecovery.BitMachine.NaturalArray.sumWords_encode line 135