OAI/Probability/MatroidProphet/BranchMix.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.branchOnlineRule line 12
  2. def OAI.MatroidProphet.branchHiddenRule line 21
  3. lemma OAI.MatroidProphet.branchOnlineRule_acceptedThrough line 26
  4. lemma OAI.MatroidProphet.branchHiddenRule_observed line 33
  5. lemma OAI.MatroidProphet.branchHiddenRule_acceptedThrough line 41
  6. lemma OAI.MatroidProphet.branchHiddenRule_reward line 50
  7. lemma OAI.MatroidProphet.branchHiddenRule_worst line 56
  8. instance OAI.MatroidProphet.withBotIntMeasurableSpace line 63
  9. instance OAI.MatroidProphet.withBotIntMeasurableSingletonClass line 64
  10. def OAI.MatroidProphet.roundedMaximumHidden line 67
  11. def OAI.MatroidProphet.completeHiddenRule line 73
  12. lemma OAI.MatroidProphet.branchHiddenRule_feasible line 78
  13. lemma OAI.MatroidProphet.roundedMaximumHidden_feasible line 93
  14. lemma OAI.MatroidProphet.completeHiddenRule_feasible line 99