OAI/Combinatorics/KMedianRecovery/Encoding/LabelOrder.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.RationalLeaves.rationalHeight line 10
  2. lemma OAI.MetricKMedianRecovery.RationalLeaves.label_lt line 14
  3. lemma OAI.MetricKMedianRecovery.RationalLeaves.rows_height line 30
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.encode line 38
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.levelWords line 40
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.parentWords line 41
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.heightWords line 42
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.levelWords_computes line 43
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.parentWords_computes line 44
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.heightWords_computes line 45
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.levelWords_encode line 47
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.parentWords_encode line 49
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.heightWords_encode line 51
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.lt line 54
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.lt_computes line 60
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.lt_pair line 68
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.orderedSort line 74
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.sort line 76
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.sort_computes line 77
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.sort_encode line 78
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.table line 86
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.label line 87
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.col line 88
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.table_computes line 89
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.label_computes line 90
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.col_computes line 91
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.rawRow line 92
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.rawRow_computes line 95
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.row line 97
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.row_computes line 99
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.row_pack line 102
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.table line 113
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.width line 114
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.item line 115
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.col line 116
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.table_computes line 117
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.width_computes line 118
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.item_computes line 119
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.col_computes line 120
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.entry line 121
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.entry_computes line 123
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.entry_pack line 125
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.row line 130
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.row_computes line 132
  45. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.row_pack line 135
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.run line 141
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.run_computes line 142
  48. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabelMatrix.run_pack line 143