OAI/Probability/MatroidProphet/RankAccounting.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.conditionalRank line 12
2. lemma OAI.MatroidProphet.conditionalRank_add_base line 15
3. lemma OAI.MatroidProphet.conditionalRank_antitone line 19
4. lemma OAI.MatroidProphet.conditionalRank_exchange line 41
5. lemma OAI.MatroidProphet.conditionalRank_closure line 60
6. lemma OAI.MatroidProphet.conditionalRank_le_rank line 65
7. lemma OAI.MatroidProphet.rankCost_step line 70
8. lemma OAI.MatroidProphet.sum_potential_drop_le line 83
9. lemma OAI.MatroidProphet.rankCost_chain line 95