OAI/Combinatorics/KMedianRecovery/Branching/BlueChoice.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.BlueDP.Candidate line 9
  2. def OAI.MetricKMedianRecovery.BlueDP.value line 10
  3. def OAI.MetricKMedianRecovery.BlueDP.choose line 13
  4. lemma OAI.MetricKMedianRecovery.BlueDP.value_choose line 17
  5. lemma OAI.MetricKMedianRecovery.BlueDP.choose_mem line 30
  6. lemma OAI.MetricKMedianRecovery.BlueDP.choose_property line 33
  7. def OAI.MetricKMedianRecovery.BlueDP.select line 38
  8. lemma OAI.MetricKMedianRecovery.BlueDP.fold_property line 39
  9. lemma OAI.MetricKMedianRecovery.BlueDP.fold_value line 44
  10. lemma OAI.MetricKMedianRecovery.BlueDP.select_value line 49
  11. lemma OAI.MetricKMedianRecovery.BlueDP.fold_mem line 54
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.encode line 68
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.score line 71
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.score_computes line 72
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.run line 73
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.run_computes line 78
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.run_pack line 85
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.step line 105
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.step_computes line 106
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.select line 107
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.select_computes line 108
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueChoice.select_pack line 110