OAI/Probability/MatroidSecretary/Transport/GeneralSimulation.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

One-sample simulation for an arbitrary measurable complete seed.

  1. lemma OAI.MatroidProphet.General.measurable_mask_membership line 15
  2. lemma OAI.MatroidProphet.General.measurable_observed line 19
  3. lemma OAI.MatroidProphet.General.measurable_simulationHistory line 28
  4. lemma OAI.MatroidProphet.General.measurable_simulationDecision line 45
  5. def OAI.MatroidProphet.General.sampleSimulation line 64
  6. lemma OAI.MatroidProphet.General.observed_glue line 68
  7. lemma OAI.MatroidProphet.General.simulationHistory_eq line 74
  8. theorem OAI.MatroidProphet.General.sampleSimulation_acceptedThrough line 78
  9. theorem OAI.MatroidProphet.General.sampleSimulation_reward line 88
  10. theorem OAI.MatroidProphet.General.sampleSimulation_feasible line 99
  11. lemma OAI.MatroidProphet.General.reward_nonneg line 110
  12. lemma OAI.MatroidProphet.General.reward_le_optimum line 114
  13. lemma OAI.MatroidProphet.General.hiddenWorstReward_le line 120
  14. lemma OAI.MatroidProphet.General.hiddenWorstReward_nonneg line 126
  15. lemma OAI.MatroidProphet.General.hiddenWorstReward_le_optimum line 133
  16. lemma OAI.MatroidProphet.General.measurable_decisionAt line 139
  17. lemma OAI.MatroidProphet.General.reward_eq_sum line 147
  18. lemma OAI.MatroidProphet.General.measurable_reward_fixed_order line 158
  19. theorem OAI.MatroidProphet.General.measurable_reward line 174

    Source documentation

    The realized reward remains measurable for arbitrary measurable adversarial permutations.

    theorem measurable_reward {n : ℕ} {R : Type*} [MeasurableSpace R] (A : OnlineRule n R) :
    Measurable (fun x : ArrivalOrder n × (R × (Weights n × Weights n)) =>
      reward A x.2.1 x.2.2.1 x.2.2.2 x.1) :=
…

    Mentions: OAI.MatroidProphet.General.OnlineRule, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.Weights, OAI.MatroidProphet.General.reward

  20. lemma OAI.MatroidProphet.General.glue_self line 179
  21. lemma OAI.MatroidProphet.General.measurable_hiddenReward line 185
  22. lemma OAI.MatroidProphet.General.measurable_hiddenWorstReward line 191
  23. lemma OAI.MatroidProphet.General.measurable_glue line 202
  24. lemma OAI.MatroidProphet.General.measurable_glue_seed line 206
  25. theorem OAI.MatroidProphet.General.glue_fixed_law line 213
  26. theorem OAI.MatroidProphet.General.glue_seed_joint_law line 223

    Source documentation

    Joint gluing law with an arbitrary measurable complete seed; in particular, the observation mask may depend on all of that seed.

    theorem glue_seed_joint_law {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ]
    (ν : Measure R) [IsProbabilityMeasure ν]
    (S V : Ω → Weights n) (seed : Ω → R)
    (hS : Measurable S) (hV : Measurable V) (hseedM : Measurable seed)
    (hi : iIndepFun (pairedCoordinates S V) μ)
    (hlaw : ∀ e, μ.map (fun ω => S ω e) = μ.map (fun ω => V ω e))
    (hseed : IndepFun (fun ω => (S ω, V ω)) seed μ)
    (hseedLaw : μ.map seed = ν) (mask : R → Finset (Fin n)) (hmask : Measurable mask) :
    MeasurePreserving (fun ω => (seed ω, glue (mask (seed ω)) (S ω) (V ω)))
      μ (ν.prod (μ.map V)) := by
…

    Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.pairedCoordinates, OAI.MatroidProphet.General.glue

  27. lemma OAI.MatroidProphet.General.measurableSet_nonnegative line 249

    Source documentation

    Nonnegativity of a finite vector is a Borel condition.

    lemma measurableSet_nonnegative (n : ℕ) :
    MeasurableSet {w : Weights n | ∀ e, 0 ≤ w e} := by
…

    Mentions: OAI.MatroidProphet.Weights

  28. lemma OAI.MatroidProphet.General.integrable_hidden_product line 254
  29. lemma OAI.MatroidProphet.General.hidden_product_integral_bound line 267
  30. lemma OAI.MatroidProphet.General.integrable_feasible_reward line 287
  31. theorem OAI.MatroidProphet.General.oneSample_of_hidden line 303

    Source documentation

    The full one-sample integration step preserves the expected minimum over all orders.

    theorem oneSample_of_hidden {n : ℕ} {Ξ : Type*} [MeasurableSpace Ξ] (M : Matroid (Fin n)) (A : HiddenRule n Ξ)
    (ν : Measure (Ξ)) [IsProbabilityMeasure ν] (c : ℝ)
    (hA : ∀ (w : Weights n), (∀ e, 0 ≤ w e) →
      ∀ (r : Ξ) (π : ArrivalOrder n) (t : ℕ),
        M.Indep (hiddenAcceptedThrough A r w π t : Set (Fin n)))
    (hbound : ∀ (w : Weights n), (∀ e, 0 ≤ w e) →
      c * optimum M w ≤ ∫ r, hiddenWorstReward A w r ∂ν)
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (S V : Ω → Weights n) (R : Ω → Ξ)
    (hS : Measurable S) (hV : Measurable V) (hR : Measurable R)
    (hSN : ∀ᵐ ω ∂μ, ∀ e, 0 ≤ S ω e) (hVN : ∀ᵐ ω ∂μ, ∀ e, 0 ≤ V ω e)
    (hi : iIndepFun (pairedCoordinates S V) μ)
…

    Mentions: OAI.MatroidProphet.General.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.General.hiddenAcceptedThrough, OAI.MatroidProphet.optimum, OAI.MatroidProphet.General.hiddenWorstReward, OAI.MatroidProphet.pairedCoordinates

  32. theorem OAI.MatroidProphet.General.simulation_contract line 347

    Source documentation

    The manuscript's simulation lemma without any finite-seed restriction.

    theorem simulation_contract.{u, v} : SimulationContract.{u, v} := by
…
  33. def OAI.MatroidProphet.General.OnlineRule.ofFinite line 362

    Source documentation

    The concrete finite-seed information model is a special case, with exactly the same decisions rather than an unrelated replacement rule.

    def OnlineRule.ofFinite {bits : ℕ} (A : MatroidProphet.OnlineRule n bits) :
    OnlineRule n (Seed bits) where
…

    Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.General.OnlineRule, OAI.MatroidProphet.Seed

  34. def OAI.MatroidProphet.General.HiddenRule.ofFinite line 367
  35. lemma OAI.MatroidProphet.General.acceptedThrough_ofFinite line 373
  36. lemma OAI.MatroidProphet.General.hiddenAcceptedThrough_ofFinite line 379
  37. lemma OAI.MatroidProphet.General.hiddenWorstReward_ofFinite line 385