OAI/Probability/MatroidProphet/Reverse/Hybrid.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.sourceReverseTree line 10
  2. lemma OAI.MatroidProphet.sourceReverseTree_fresh line 16
  3. lemma OAI.MatroidProphet.sourceReverseTree_queried line 26
  4. lemma OAI.MatroidProphet.sourceReverseTree_queried_coordinate line 35
  5. lemma OAI.MatroidProphet.sourceReverseTree_hybrid_coordinate line 50
  6. def OAI.MatroidProphet.transitionHybrid line 64
  7. lemma OAI.MatroidProphet.sourceReverseTree_hybrid_guard line 71
  8. lemma OAI.MatroidProphet.reversePrefix_congr_guard_inter line 89
  9. lemma OAI.MatroidProphet.sourceReverseTree_hybrid_output line 98
  10. theorem OAI.MatroidProphet.reverse_double_exit line 111
  11. lemma OAI.MatroidProphet.sourceReverseTree_queried_coordinate_full line 147
  12. lemma OAI.MatroidProphet.sourceReverseTree_positive_guards line 162
  13. lemma OAI.MatroidProphet.sourceReverseTree_positive_nominal line 175
  14. def OAI.MatroidProphet.reverseStateTree line 191
  15. lemma OAI.MatroidProphet.reverseStateTree_run line 197
  16. lemma OAI.MatroidProphet.reverseStateTree_fresh line 206
  17. lemma OAI.MatroidProphet.reverseStateTree_queried line 214