OAI/Combinatorics/KMedianRecovery/Recovery/SortMath.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.CanonicalSort.insert line 9
  2. lemma OAI.MetricKMedianRecovery.CanonicalSort.insert_sort line 12
  3. lemma OAI.MetricKMedianRecovery.CanonicalSort.fold_sort line 36
  4. lemma OAI.MetricKMedianRecovery.CanonicalSort.run_sort line 47
  5. def OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.reverseTest line 55
  6. def OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.reverseTest_computes line 57
  7. def OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.insert line 61
  8. def OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.insert_computes line 63
  9. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.insert_encode line 69
  10. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.length_filter_pair line 76
  11. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.insert_length line 95
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.fold_length line 102
  13. def OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.op line 113
  14. def OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.op_computes line 115
  15. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.operation_encode line 118
  16. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.fold_encode line 123
  17. def OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.run line 131
  18. def OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.run_computes line 133
  19. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Sort.run_encode line 137