RelabelingProphet.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An unconditional prophet witness on arbitrary finite labels, reusing the canonical relabeling implementation. This supplies the existential endpoint rather than requiring a hidden-rule performance hypothesis from the caller.

theorem OAI.MatroidProphet.Relabeling.exists_labeled_one_sample line 20

Source documentation

A distribution-independent measurable one-sample rule on the original labels, with exact prefix feasibility and the full almighty-adversary bound. The enumeration is fixed before all probability laws and realizations.

theorem exists_labeled_one_sample.{u} (M : Matroid α) (hE : M.E = Set.univ)
    (e : α ≃ Fin n) :
    ∃ (bits : ℕ) (ν : Measure (Seed bits)), IsProbabilityMeasure ν ∧
    ∃ (A : OnlineRule n bits),
      (∀ k : Fin n, Measurable (fun x : Seed bits × ((α → ℝ) × LabeledHistory α k) =>
        transportedDecision e A k x.1 x.2.1 x.2.2)) ∧
      (∀ (r : Seed bits) (s v : α → ℝ) (π : LabeledOrder α n) (t : ℕ),
        (∀ a, 0 ≤ s a) → (∀ a, 0 ≤ v a) →
        M.Indep (transportedAcceptedThrough e A r s v π t : Set α)) ∧
      ∀ {Ω : Type u} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
        (S V : Ω → α → ℝ) (R : Ω → Seed bits),
        Measurable S → Measurable V → Measurable R →
…

Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Relabeling.LabeledHistory, OAI.MatroidProphet.Relabeling.transportedDecision, OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.Relabeling.transportedAcceptedThrough