OAI/Probability/MatroidSecretary/Labels/FiniteLabelAgreement.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The two preserved arbitrary-label interfaces describe exactly the same offline benchmark and online execution. These are definitional equalities, not extra model-validity premises or comparisons of surrogate rewards.

  1. theorem OAI.MatroidProphet.FiniteLabelAgreement.optimum_eq line 16
  2. theorem OAI.MatroidProphet.FiniteLabelAgreement.decision_eq line 19
  3. theorem OAI.MatroidProphet.FiniteLabelAgreement.acceptedThrough_eq line 25
  4. theorem OAI.MatroidProphet.FiniteLabelAgreement.reward_eq line 30