OAI/Probability/MatroidProphet/Reverse/Bands.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatroidProphet.bandNonexitCost_budget line 11
  2. def OAI.MatroidProphet.bandExitCost line 34
  3. def OAI.MatroidProphet.bandCountCost line 40
  4. lemma OAI.MatroidProphet.bandCountCost_step_split line 46
  5. lemma OAI.MatroidProphet.bandCountCost_mean_split line 61
  6. lemma OAI.MatroidProphet.bandExitCost_count_le_one line 82
  7. lemma OAI.MatroidProphet.bandExitCost_mean_le_one line 104
  8. lemma OAI.MatroidProphet.bandExitCost_le_upper_count line 119
  9. theorem OAI.MatroidProphet.reverse_exit_band_bound line 150