ReplayTransport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the actual reconstructed secretary rule

This is a supporting composition theorem. The correct source marginal and mask-support facts are explicit inputs to be supplied by the concrete finite prefix/table coupling; they are not premises of the final secretary endpoint. The adversarial order may depend on all of the ambient randomness, including unused precommitted table entries.

theorem OAI.MatroidProphet.SecretaryReplay.reconstructed_integral_lower line 23

Source documentation

Replay and the expected-minimum comparison commute with an arbitrary measurable full-information suffix policy. Prefix-set equality follows, in the secretary experiment, from agreement with the sampled ordered prefix.

theorem reconstructed_integral_lower {n bits : ℕ} {Q : Type*}
    [Fintype Q] [MeasurableSpace Q] [MeasurableSingletonClass Q]
    (A : HiddenRule n bits) (K : Q → Fin (n + 1))
    (decode : Q → Finset (Fin n) → Seed bits) (w : Weights n)
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ]
    (ν : Measure (Seed bits)) (q : Ω → Q) (σ π : Ω → ArrivalOrder n)
    (hq : Measurable q) (hσ : Measurable σ) (hπ : Measurable π)
    (hprefix : ∀ᵐ ω ∂μ,
      orderPrefix (π ω) (K (q ω)).val = orderPrefix (σ ω) (K (q ω)).val)
    (hmask : ∀ᵐ ω ∂μ,
      A.mask (decode (q ω) (orderPrefix (σ ω) (K (q ω)).val)) =
        orderPrefix (σ ω) (K (q ω)).val)
…

Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.orderPrefix