OAI/Probability/MatroidProphet/Residual/Timeline.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatroidProphet.Pivots.IntWindow line 12
2. instance OAI.MatroidProphet.Pivots.(instance at line 14) line 14
3. abbrev OAI.MatroidProphet.Pivots.ParityWindow line 16
4. instance OAI.MatroidProphet.Pivots.(instance at line 18) line 18
5. def OAI.MatroidProphet.Pivots.roundParity line 20
6. lemma OAI.MatroidProphet.Pivots.roundParity_bounds line 22
7. lemma OAI.MatroidProphet.Pivots.roundParity_mod line 26
8. lemma OAI.MatroidProphet.Pivots.roundParity_le_iff line 31
9. lemma OAI.MatroidProphet.Pivots.roundParity_lt_iff line 37
10. def OAI.MatroidProphet.Pivots.windowPlacement line 45
11. def OAI.MatroidProphet.Pivots.parityPlacement line 48
12. def OAI.MatroidProphet.Pivots.generatedPath line 55
13. lemma OAI.MatroidProphet.Pivots.window_prefix line 58
14. lemma OAI.MatroidProphet.Pivots.parity_upperPath line 65
15. lemma OAI.MatroidProphet.Pivots.parity_lowerPath line 77
16. lemma OAI.MatroidProphet.Pivots.window_before line 118