OAI/Probability/MatroidSecretary/Secretary/ProbabilityModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reference-side arrival law for the actual random-prefix secretary experiment.

  1. instance OAI.MatroidProphet.Secretary.uniformArrivalLaw_probability line 10
  2. abbrev OAI.MatroidProphet.Secretary.prefixSet line 16

    Source documentation

    Compatibility name for the source prefix set; only the analysis uses a full order.

    abbrev prefixSet {n : ℕ} := @MatroidProphet.orderPrefix n
…

    Mentions: OAI.MatroidProphet.orderPrefix