OAI/Combinatorics/KMedianRecovery/Recovery/RowInput.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.columns_source line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rowInput line 17
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rowInput_computes line 18
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rowCoefficients line 21
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rowCoefficients_computes line 23
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rowCoefficients_pack line 27
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rowWord line 33
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rowWord_computes line 35
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rowWord_pack line 37
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rows line 42
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rows_computes line 43
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.rows_pack line 47
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.bound line 52
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.bound_computes line 54
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.bound_pack line 57
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.prepared line 61
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.prepared_computes line 63
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.prepared_pack line 66
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.run line 72
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.run_computes line 73
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.run_pack line 74
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.nil_iff line 78
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRawOpening.witness line 86
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.natEq line 102
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.natEq_computes line 103
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.contains line 116
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.contains_computes line 117
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.contains_indices line 123
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.context line 133
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.query line 138
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.query_computes line 140
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.query_context line 146
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.answer line 152
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.answer_computes line 153
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.eligible line 154
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.eligible_computes line 157
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.contains_finset line 167
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.eligible_context line 173
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.chosen line 186
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.chosen_computes line 187
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.chosenQuery line 188
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.chosenQuery_computes line 189
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.bids line 192
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.bids_computes line 194
  45. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.enum_bid line 200
  46. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.bids_context line 203
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.eventBits line 223
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.resultBits line 225
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.run line 228
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.run_computes line 230
  51. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFirst.run_pack line 238