OAI/Probability/MatroidProphet/LayerOnline.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.assignedEligible line 9
  2. def OAI.MatroidProphet.assignedLayer line 14
  3. def OAI.MatroidProphet.layerKeyDecision line 18
  4. def OAI.MatroidProphet.keyHistory line 30
  5. lemma OAI.MatroidProphet.keyHistory_current line 34
  6. lemma OAI.MatroidProphet.keyHistory_prior line 39
  7. theorem OAI.MatroidProphet.layerKeyDecision_eq_greedy line 66
  8. def OAI.MatroidProphet.layerOnlineRule line 84
  9. theorem OAI.MatroidProphet.layerOnlineRule_accepted line 92
  10. lemma OAI.MatroidProphet.acceptedThrough_subset_accepted line 113
  11. theorem OAI.MatroidProphet.layerOnlineRule_feasible line 121