OAI/Combinatorics/KMedianRecovery/Branching/SuccessfulFavorableProbability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedianRecovery.Sampling.Comparison.successful_favorable_probability line 14
2. def OAI.MetricKMedianRecovery.Sampling.branchScore line 53
3. structure OAI.MetricKMedianRecovery.Sampling.BranchReady line 56
4. def OAI.MetricKMedianRecovery.Sampling.branchObjective line 64
5. lemma OAI.MetricKMedianRecovery.Sampling.observable_branch_exists line 78
6. def OAI.MetricKMedianRecovery.Sampling.acceptedOutput line 133
7. lemma OAI.MetricKMedianRecovery.Sampling.acceptedOutput_spec line 142
8. def OAI.MetricKMedianRecovery.Sampling.observableOutput line 157
9. lemma OAI.MetricKMedianRecovery.Sampling.observableOutput_feasible line 169