OAI/Combinatorics/KMedianRecovery/Recovery/Basic.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.RatOps.le line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.MetricTable.context line 21
  3. def OAI.MetricKMedianRecovery.BitMachine.MetricTable.row line 22
  4. def OAI.MetricKMedianRecovery.BitMachine.MetricTable.col line 23
  5. def OAI.MetricKMedianRecovery.BitMachine.MetricTable.context_computes line 24
  6. def OAI.MetricKMedianRecovery.BitMachine.MetricTable.row_computes line 25
  7. def OAI.MetricKMedianRecovery.BitMachine.MetricTable.col_computes line 26
  8. def OAI.MetricKMedianRecovery.BitMachine.MetricTable.getRow line 27
  9. def OAI.MetricKMedianRecovery.BitMachine.MetricTable.getRow_computes line 28
  10. def OAI.MetricKMedianRecovery.BitMachine.MetricTable.get line 29
  11. def OAI.MetricKMedianRecovery.BitMachine.MetricTable.get_computes line 30
  12. lemma OAI.MetricKMedianRecovery.BitMachine.MetricTable.get_pack line 31
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.context line 41
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.indices line 44
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.table line 46
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.client line 47
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.paramV line 48
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.paramZ line 49
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.table_computes line 50
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.client_computes line 52
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.paramV_computes line 54
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.paramZ_computes line 56
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.distanceWord line 58
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.distanceWord_computes line 60
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.fails line 68
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.fails_computes line 71
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.fails_context line 76
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.run line 83
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.run_computes line 84
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.optionEncode_nil_iff line 85
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.run_pack line 87
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningActivity.run_source line 98
  33. def OAI.MetricKMedianRecovery.BitMachine.RationalMin.choose line 118
  34. def OAI.MetricKMedianRecovery.BitMachine.RationalMin.choose_computes line 121
  35. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.operation_pair line 126
  36. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.fold_encode line 129
  37. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.fold_length line 140
  38. def OAI.MetricKMedianRecovery.BitMachine.RationalMin.seed line 151
  39. def OAI.MetricKMedianRecovery.BitMachine.RationalMin.seed_computes line 152
  40. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.seed_encode line 156
  41. def OAI.MetricKMedianRecovery.BitMachine.RationalMin.run line 161
  42. def OAI.MetricKMedianRecovery.BitMachine.RationalMin.run_computes line 163
  43. def OAI.MetricKMedianRecovery.BitMachine.RationalMin.minimum line 166
  44. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.run_encode line 167
  45. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.fold_lower line 184
  46. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.fold_le_init line 190
  47. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.fold_le_mem line 194
  48. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.minimum_lower line 202
  49. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.minimum_le_mem line 209