OAI/Probability/MatroidProphet/GreedyOptimal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.Candidates.prefixCount line 14
2. def OAI.MatroidProphet.Candidates.timeCount line 17
3. lemma OAI.MatroidProphet.Candidates.sum_timeCount line 20
4. lemma OAI.MatroidProphet.Candidates.sum_weight_timeCount line 28
5. lemma OAI.MatroidProphet.Candidates.sum_weight_le_of_prefixCount line 39
6. lemma OAI.MatroidProphet.Candidates.greedy_univ_prefix_closure line 56
7. lemma OAI.MatroidProphet.Candidates.prefixCount_le_greedy line 65
8. def OAI.MatroidProphet.Candidates.orderedWeights line 97
9. def OAI.MatroidProphet.Candidates.priorityTime line 100
10. lemma OAI.MatroidProphet.Candidates.priorityTime_injective line 102
11. lemma OAI.MatroidProphet.Candidates.orderedWeights_priorityTime line 106
12. lemma OAI.MatroidProphet.Candidates.greedy_dominates_independent line 110
13. theorem OAI.MatroidProphet.Candidates.greedy_weight_eq_optimum line 131