OAI/Probability/MatroidProphet/Reverse/Hazard.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.reverseHazard line 10
  2. lemma OAI.MatroidProphet.reverseHazard_eq line 15
  3. lemma OAI.MatroidProphet.reverseHazard_nonneg line 26
  4. lemma OAI.MatroidProphet.reverseHazard_le_one line 32
  5. lemma OAI.MatroidProphet.reverseHazard_mono line 38
  6. lemma OAI.MatroidProphet.reverseHazard_step_mono line 53
  7. lemma OAI.MatroidProphet.reverseHazard_eq_step line 62
  8. def OAI.MatroidProphet.bandNonexitCost line 73
  9. lemma OAI.MatroidProphet.bandNonexitCost_zero_above line 79
  10. lemma OAI.MatroidProphet.bandNonexitCost_eq_count line 93
  11. theorem OAI.MatroidProphet.bandNonexitCost_budget_after_entry line 114