OAI/Combinatorics/KMedianRecovery/Branching/BranchObjective.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.objective_eq_source line 9
2. def OAI.BlueSubsetDP.Plan.reweight line 43
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.rationalScore line 50
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.score_cast line 53
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.favorable_literal_plan line 58
6. def OAI.MetricKMedianRecovery.BitMachine.BinaryObservableBranch.run line 102
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryObservableBranch.run_computes line 106
8. def OAI.MetricKMedianRecovery.BitMachine.BinaryObservableBranch.output line 113
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryObservableBranch.output_none line 132
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryObservableBranch.output_some line 142
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryObservableBranch.best_pack line 165
12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryObservableBranch.run_pack line 172
13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryObservableBranch.output_feasible line 208