OAI/Probability/MatroidProphet/Candidates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.Candidates.prior line 14
2. def OAI.MatroidProphet.Candidates.greedy line 17
3. def OAI.MatroidProphet.Candidates.candidates line 22
4. lemma OAI.MatroidProphet.Candidates.prior_insert_self line 27
5. lemma OAI.MatroidProphet.Candidates.prior_mono line 38
6. lemma OAI.MatroidProphet.Candidates.greedy_indep line 42
7. lemma OAI.MatroidProphet.Candidates.greedy_sdiff_subset_candidates line 66
8. lemma OAI.MatroidProphet.Candidates.expectation_sum line 77
9. lemma OAI.MatroidProphet.Candidates.expectation_not_mem line 84
10. lemma OAI.MatroidProphet.Candidates.expectation_sdiff_fair line 105
11. lemma OAI.MatroidProphet.Candidates.greedy_sdiff_indep line 125
12. lemma OAI.MatroidProphet.Candidates.expectation_greedy_sdiff_fair line 133
13. lemma OAI.MatroidProphet.Candidates.expectation_fair_balance line 141
14. lemma OAI.MatroidProphet.Candidates.expectation_candidates_eq_greedy line 185
15. theorem OAI.MatroidProphet.Candidates.expectation_candidates_le_optimum line 235