OAI/Probability/MatroidSecretary/Secretary/Execution.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatroidProphet.secretaryDecisionAt_congr line 13
2. lemma OAI.MatroidProphet.secretaryAcceptedThrough_mono line 19
3. lemma OAI.MatroidProphet.secretaryAcceptedThrough_arrived line 26
4. lemma OAI.MatroidProphet.secretaryAcceptedThrough_not_prefix line 31
5. lemma OAI.MatroidProphet.secretaryAcceptedThrough_prefix_empty line 40
6. lemma OAI.MatroidProphet.secretaryReward_nonneg line 49
7. lemma OAI.MatroidProphet.secretaryReward_le_optimum line 54
8. lemma OAI.MatroidProphet.measurable_secretaryDecisionAt line 60
9. lemma OAI.MatroidProphet.secretaryReward_eq_sum line 71
10. lemma OAI.MatroidProphet.measurable_secretaryReward_fixed_order line 82
11. lemma OAI.MatroidProphet.measurable_secretaryReward line 96

    Source documentation

    No independence from the entire seed is imposed on the measurable arrival order.

    lemma measurable_secretaryReward (A : SecretaryRule n Q) :
        Measurable (fun x : ArrivalOrder n × (Q × Weights n) =>
          secretaryReward A x.2.1 x.2.2 x.1) :=
    …

    Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.Weights, OAI.MatroidProphet.secretaryReward

12. lemma OAI.MatroidProphet.integrable_secretaryReward line 101