OAI/Probability/MatroidProphet/Certificates/Budget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MatroidProphet.QueryProgram line 15
2. def OAI.MatroidProphet.QueryProgram.Fresh line 20
3. def OAI.MatroidProphet.QueryProgram.expected line 25
4. lemma OAI.MatroidProphet.ratio_resource line 32
5. theorem OAI.MatroidProphet.certificate_budget_of_failure_identities line 51
6. theorem OAI.MatroidProphet.disjoint_query_certificates line 105