OAI/Combinatorics/KMedianRecovery/Branching/BlueItem.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BlueDP.choose_none line 9
  2. lemma OAI.MetricKMedianRecovery.BlueDP.select_cond line 10
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.select_map line 22
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.atomEnc line 29
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.record line 31
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.records line 33
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.targetL line 35
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.targetY line 36
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.sourceR line 37
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.sourceL line 38
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.sourceRow line 39
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.targetL_computes line 40
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.targetY_computes line 41
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.sourceR_computes line 42
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.sourceL_computes line 43
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.sourceRow_computes line 44
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.price line 45
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.price_computes line 46
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.response line 47
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.response_computes line 49
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.op line 51
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.op_computes line 52
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.op_pack line 55
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.run line 64
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.run_computes line 65
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueItem.run_pack line 66
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.pack line 85
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.oracleInput line 88
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.oracleInput_computes line 89
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.row line 91
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.row_computes line 92
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.weight line 96
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.weight_computes line 98
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.scaled line 103
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.scaled_computes line 104
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.tag line 108
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.tag_computes line 109
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.op line 111
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.op_computes line 112
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.op_pack line 113
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.run line 132
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.run_computes line 133
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueRecords.run_pack line 137