OAI/Combinatorics/KMedianRecovery/Encoding/FinSets.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.values line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.encode line 12
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.values_card line 13
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.values_union line 14
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.values_diff line 15
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.values_sort line 17
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.encode_eq line 21
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.values_bottom line 24
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.values_pad line 30
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.union_pack line 33
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.diff_pack line 35
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.pad_pack line 37
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryMaskParser.member line 45
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryMaskParser.member_computes line 47
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryMaskParser.run line 49
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryMaskParser.run_computes line 51
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMaskParser.member_mask line 54
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMaskParser.run_mask line 59
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryIndexMap.item line 89
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryIndexMap.item_computes line 90
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryIndexMap.run line 91
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryIndexMap.run_computes line 92
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIndexMap.run_pack line 93
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.ranking_injective line 102
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.rank_value_mono line 105
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.bottomValues line 108
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.bottom_sum_cast line 110
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.sumBottom line 142
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.sumBottom_computes line 145
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.sumBottom_pack line 149
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.sumBottom_correct line 155