OAI/Probability/MatroidProphet/Information.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatroidProphet.decisionAt_congr line 10
  2. theorem OAI.MatroidProphet.acceptedThrough_mono line 16
  3. theorem OAI.MatroidProphet.acceptedThrough_arrived line 24
  4. theorem OAI.MatroidProphet.acceptedThrough_iff_decision line 30
  5. theorem OAI.MatroidProphet.sum_le_optimum line 37
  6. theorem OAI.MatroidProphet.measurable_optimum line 47
  7. theorem OAI.MatroidProphet.optimum_nonneg line 61
  8. theorem OAI.MatroidProphet.reward_nonneg line 65
  9. theorem OAI.MatroidProphet.reward_le_optimum line 70
  10. lemma OAI.MatroidProphet.measurable_history line 76
  11. lemma OAI.MatroidProphet.measurable_decisionAt line 82
  12. lemma OAI.MatroidProphet.reward_eq_sum line 90
  13. lemma OAI.MatroidProphet.measurable_reward_fixed_order line 101
  14. theorem OAI.MatroidProphet.measurable_reward line 116