OAI/Combinatorics/KMedianRecovery/Algorithms/CandidateSanitize.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.keep line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.keep_computes line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.clip line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.clip_computes line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.size line 19
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.size_computes line 20
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.run line 21
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.run_computes line 25
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.pack line 32
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.clipped line 34
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.output line 36
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.clip_pack line 38
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.size_pack line 45
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.run_pack line 49
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.output_feasible line 55
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.clipped_encode line 62
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.output_encode line 70
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCandidateSanitize.run_encode line 73
  19. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.metricContext line 81
  20. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.metricContext_computes line 82
  21. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.sanitizeContext line 84
  22. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.sanitizeContext_computes line 85
  23. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.atRawInput line 87
  24. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.atRawInput_computes line 89
  25. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.atRaw line 92
  26. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.atRaw_computes line 93
  27. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.candidates line 94
  28. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.candidates_computes line 95
  29. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.run line 99
  30. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.run_computes line 101
  31. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.pack line 104
  32. def OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.output line 106
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.atRaw_pack line 108
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.candidates_pack line 114
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.run_pack line 118
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.output_feasible line 129
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.realCost_le_self line 137
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySanitizedBest.realCost_le_good line 145