OAI/Probability/MatroidProphet/Pivots/Encoding.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.Pivots.oldBefore line 13
2. def OAI.MatroidProphet.Pivots.movableBefore line 16
3. lemma OAI.MatroidProphet.Pivots.oldBefore_mono line 19
4. lemma OAI.MatroidProphet.Pivots.movableBefore_mono line 26
5. lemma OAI.MatroidProphet.Pivots.oldBefore_lt_after line 33
6. lemma OAI.MatroidProphet.Pivots.movableBefore_lt_after line 46
7. lemma OAI.MatroidProphet.Pivots.movableBefore_self_lt line 59
8. lemma OAI.MatroidProphet.Pivots.old_time_lt_iff line 72
9. lemma OAI.MatroidProphet.Pivots.oldBefore_self line 80
10. def OAI.MatroidProphet.Pivots.scoreExponent line 89
11. lemma OAI.MatroidProphet.Pivots.scoreExponent_old line 94
12. lemma OAI.MatroidProphet.Pivots.scoreExponent_preserves_order line 97
13. lemma OAI.MatroidProphet.Pivots.scoreExponent_injective line 134