OAI/Probability/MatroidSecretary/Transport/GeneralSimulationModel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MatroidProphet.General.OnlineRule line 13

    Source documentation

    A decision uses only the entire initial seed, the initially observed vector, and the label/value history through the current arrival.

    structure OnlineRule (n : ℕ) (R : Type*) [MeasurableSpace R] where
…
  2. def OAI.MatroidProphet.General.decisionAt line 18
  3. def OAI.MatroidProphet.General.acceptedThrough line 23
  4. def OAI.MatroidProphet.General.reward line 30
  5. def OAI.MatroidProphet.General.Feasible line 34
  6. structure OAI.MatroidProphet.General.HiddenRule line 41

    Source documentation

    The observation mask is a measurable function of the seed alone.

    structure HiddenRule (n : ℕ) (R : Type*) [MeasurableSpace R] where
…
  7. def OAI.MatroidProphet.General.observed line 46
  8. def OAI.MatroidProphet.General.hiddenAcceptedThrough line 51
  9. def OAI.MatroidProphet.General.hiddenReward line 56
  10. def OAI.MatroidProphet.General.hiddenWorstReward line 60
  11. def OAI.MatroidProphet.General.HiddenFeasible line 65
  12. def OAI.MatroidProphet.General.glue line 72

    Source documentation

    Sample values on the sacrificed mask, and realized values elsewhere.

    noncomputable def glue {n : ℕ} (mask : Finset (Fin n)) (s v : Weights n) : Weights n := by
…

    Mentions: OAI.MatroidProphet.Weights

  13. def OAI.MatroidProphet.General.simulationHistory line 76
  14. def OAI.MatroidProphet.General.simulationDecision line 84
  15. def OAI.MatroidProphet.General.SimulationContract line 96

    Source documentation

    Full source contract for lem:simulation, with arbitrary measurable seed and probability spaces. The simulator is constructed before the distributions and adversary are supplied. Its decision function is specified concretely; the conjunction includes exact execution, feasibility, the seed/glued-vector joint law, integrability, and preservation of the same competitive ratio.

    def SimulationContract.{u, v} : Prop :=
…