OAI/Probability/MatroidSecretary/Secretary/Assembly.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatroidProphet.SecretaryReplay.prefix_set_eq line 10
2. theorem OAI.MatroidProphet.SecretaryReplay.reconstructed_product_lower line 30

   Source documentation

   A finite product coupling supplies the entire arbitrary-ambient-space lower bound. In particular nothing here requires independence of the executed order.

   theorem reconstructed_product_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)
       (νQ : Measure Q) (η : Measure (ArrivalOrder n)) (ν : Measure (Seed bits))
       (hproductLaw : (νQ.prod η).map
         (fun z => decode z.1 (orderPrefix z.2 (K z.1).val)) = ν)
       (hproductMask : ∀ᵐ z ∂νQ.prod η,
         A.mask (decode z.1 (orderPrefix z.2 (K z.1).val)) =
           orderPrefix z.2 (K z.1).val)
       (w : Weights n) {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ]
   …

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