OAI/Probability/MatroidProphet/Rounding.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.MatroidProphet.levelMeasurableSpace line 12
  2. instance OAI.MatroidProphet.levelMeasurableSingletonClass line 13
  3. def OAI.MatroidProphet.roundedLevel line 16
  4. def OAI.MatroidProphet.levelWeight line 19
  5. def OAI.MatroidProphet.roundedWeight line 23
  6. theorem OAI.MatroidProphet.measurable_roundedLevel line 25
  7. lemma OAI.MatroidProphet.roundedWeight_nonneg line 32
  8. lemma OAI.MatroidProphet.roundedWeight_le line 39
  9. lemma OAI.MatroidProphet.le_base_mul_roundedWeight line 49
  10. def OAI.MatroidProphet.discreteOnlineRule line 61
  11. lemma OAI.MatroidProphet.optimum_le_of_independent_bound line 86
  12. theorem OAI.MatroidProphet.optimum_mono line 97
  13. theorem OAI.MatroidProphet.optimum_rounding_bound line 103