OAI/Probability/MatroidProphet/AdaptiveResampling.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatroidProphet.bitsExpectation_mul_left line 9
2. lemma OAI.MatroidProphet.bitsExpectation_mul_right line 16
3. inductive OAI.MatroidProphet.RevealTree line 23
4. def OAI.MatroidProphet.RevealTree.Fresh line 27
5. def OAI.MatroidProphet.RevealTree.run line 31
6. def OAI.MatroidProphet.RevealTree.queried line 35
7. def OAI.MatroidProphet.RevealTree.hybrid line 39
8. lemma OAI.MatroidProphet.RevealTree.queried_subset line 46
9. lemma OAI.MatroidProphet.RevealTree.run_query_no line 57
10. lemma OAI.MatroidProphet.RevealTree.run_query_yes line 60
11. lemma OAI.MatroidProphet.RevealTree.hybrid_query line 63
12. lemma OAI.MatroidProphet.RevealTree.mean_run_query line 71
13. theorem OAI.MatroidProphet.RevealTree.hybrid_independent line 90
14. lemma OAI.MatroidProphet.RevealTree.hybrid_eq_resample line 166
15. lemma OAI.MatroidProphet.RevealTree.double_event line 207