OAI/Probability/MatroidProphet/Reverse/Cost.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.reverseCost line 12
  2. lemma OAI.MatroidProphet.reverseCost_congr line 21
  3. lemma OAI.MatroidProphet.reverseCost_add line 48
  4. lemma OAI.MatroidProphet.reverseCost_mul line 58
  5. lemma OAI.MatroidProphet.reverseCost_mono line 68
  6. def OAI.MatroidProphet.reverseMeanCost line 78
  7. lemma OAI.MatroidProphet.reverseCost_erase_step line 84
  8. theorem OAI.MatroidProphet.reverseMeanCost_succ line 99
  9. lemma OAI.MatroidProphet.reverseMeanCost_zero line 133
  10. lemma OAI.MatroidProphet.reverseMeanCost_add line 139
  11. lemma OAI.MatroidProphet.reverseMeanCost_mul line 149
  12. theorem OAI.MatroidProphet.reverseMeanCost_le_of_step line 159
  13. theorem OAI.MatroidProphet.reverseMeanCost_eq_of_step line 180
  14. lemma OAI.MatroidProphet.reverseCost_sum line 195
  15. lemma OAI.MatroidProphet.reverseMeanCost_sum line 205