OAI/Combinatorics/KMedianRecovery/Recovery/Values.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningNearest.distanceWord_context line 8
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningNearest.values line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningNearest.values_computes line 15
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningNearest.values_pack line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningNearest.run line 20
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningNearest.run_computes line 21
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningNearest.run_pack line 22
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningNearest.minimum_nearest line 28
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningNearest.run_source line 52
  10. def OAI.MetricKMedianRecovery.BitMachine.RatOps.max line 71
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.pack line 81
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.field line 88
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.field_computes line 89
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.field_encode line 91
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.itemField line 94
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.itemField_computes line 95
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.paramV line 97
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.paramZ line 98
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.paramV_computes line 99
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.paramZ_computes line 101
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.scale line 103
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.scale_computes line 104
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.activityInput line 106
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.activityInput_computes line 109
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.activityInput_pack line 112
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.active line 120
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.active_computes line 122
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.active_pack line 125
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.nearest line 131
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.nearest_computes line 133
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.nearest_pack line 139
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.distanceWords line 144
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.distanceWords_computes line 146
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.distance line 154
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.distance_computes line 155
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.distance_pack line 157
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.summand line 165
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.summand_computes line 170
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.sourceSummand line 179
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.summand_pack line 185
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.input line 194
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.input_computes line 196
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.values line 198
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.values_computes line 199
  45. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.values_pack line 200
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.sumWords line 210
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.sumWords_computes line 211
  48. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.sumWords_pack line 212
  49. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.source_constant line 218
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.run line 228
  51. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.run_computes line 232
  52. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningPayment.run_source line 239