OAI/Combinatorics/KMedianRecovery/Recovery/FaceSelection.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.negEntry line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.negEntry_computes line 12
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.reverse line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.reverse_computes line 15
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFace.reverse_encode line 23
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.reverseOp line 27
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.reverseOp_computes line 28
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.reverseRows line 29
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.reverseRows_computes line 30
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFace.reverseRows_encode line 35
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.proposed line 39
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.proposed_computes line 40
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.faceWords line 41
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.faceWords_computes line 43
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFace.faceWords_pack line 51
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.decisionInput line 59
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.decisionInput_computes line 62
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFace.decisionInput_pack line 66
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.decision line 73
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.decision_computes line 74
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.op line 75
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.op_computes line 76
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFace.operation_pack line 78
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFace.fold_op line 84
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFace.length_selectFace line 93
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.run line 107
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryFace.run_computes line 108
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFace.run_pack line 109
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.shape line 130
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.shape_computes line 132
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.shape_pack line 140
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.box line 151
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.box_computes line 153
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.box_pack line 161
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.allRows line 165
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.allRows_computes line 166
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.allRows_pack line 167
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.context line 171
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.context_computes line 173
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.context_pack line 175
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.run line 178
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.run_computes line 179
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinalFace.run_pack line 181