OAI/Probability/MatroidProphet/BatchReveal.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.RevealTree.map line 9
2. lemma OAI.MatroidProphet.RevealTree.fresh_map line 13
3. lemma OAI.MatroidProphet.RevealTree.run_map line 19
4. def OAI.MatroidProphet.revealBatch line 27
5. lemma OAI.MatroidProphet.erase_sdiff_eq_sdiff_insert line 32
6. lemma OAI.MatroidProphet.revealBatch_fresh line 38
7. lemma OAI.MatroidProphet.revealBatch_run line 62
8. lemma OAI.MatroidProphet.revealBatch_queried line 93
9. lemma OAI.MatroidProphet.RevealTree.queried_map line 125
10. lemma OAI.MatroidProphet.RevealTree.hybrid_map line 133
11. structure OAI.MatroidProphet.RevealRecord line 140
12. def OAI.MatroidProphet.RevealTree.record line 145
13. lemma OAI.MatroidProphet.RevealTree.record_fresh line 151
14. lemma OAI.MatroidProphet.RevealTree.record_run line 157
15. lemma OAI.MatroidProphet.RevealTree.record_hybrid line 176
16. lemma OAI.MatroidProphet.RevealTree.transcript_hybrid_independent line 182
17. lemma OAI.MatroidProphet.RevealTree.transcript_freshness line 192
18. lemma OAI.MatroidProphet.RevealTree.record_queried line 221