OAI/Combinatorics/KMedianRecovery/Branching/BlueMerge.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.listEnc line 10
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.listEnc_append line 11
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.payload line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.payload_computes line 14
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.sum line 15
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.sum_computes line 18
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.output line 21
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.output_computes line 23
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.run line 26
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.run_computes line 28
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueMerge.run_pack line 33
  12. def OAI.MetricKMedianRecovery.BlueDP.score0 line 59
  13. def OAI.MetricKMedianRecovery.BlueDP.atoms line 60
  14. lemma OAI.MetricKMedianRecovery.BlueDP.collect_formula line 61
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.invalid line 75
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.invalid_computes line 76
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.bad line 77
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.bad_computes line 78
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.scoreOp line 79
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.scoreOp_computes line 80
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.scores line 81
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.scores_computes line 83
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.payloadOp line 86
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.payloadOp_computes line 87
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.contents line 88
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.contents_computes line 89
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.result line 90
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.result_computes line 91
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.run line 93
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.run_computes line 94
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.enc_empty line 98
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.bad_empty line 103
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.score_some line 115
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.contents_pack line 120
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueCollect.run_pack line 131