LabeledTransportOneSample.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The indexed endpoint transported to any finite labeled ground type. The encoding is fixed from the labels alone, before distributions and randomness. No representability, positive-rank, atomlessness, or per-label moment premise is introduced. This is optional source-correspondence support.

def OAI.MatroidProphet.LabeledTransport.pairedCoordinates line 17

theorem OAI.MatroidProphet.LabeledTransport.one_sample line 22

Source documentation

The main guarantee on arbitrary finite physical labels, with a measurable history-only rule and the same all-prefix feasibility and arbitrary-law bound.

theorem one_sample.{u} (M : Matroid α) (hE : M.E = Set.univ) :
    ∃ (bits : ℕ) (ν : Measure (Seed bits)), IsProbabilityMeasure ν ∧
    ∃ (A : OnlineRule α (Fintype.card α) bits),
      (∀ (r : Seed bits) (s v : α → ℝ) (π : ArrivalOrder α (Fintype.card α)) (t : ℕ),
        (∀ a, 0 ≤ s a) → (∀ a, 0 ≤ v a) →
        M.Indep (acceptedThrough A r s v π t : Set α)) ∧
      ∀ {Ω : Type u} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
        (S V : Ω → α → ℝ) (R : Ω → Seed bits),
        Measurable S → Measurable V → Measurable R →
        (∀ᵐ ω ∂μ, ∀ a, 0 ≤ S ω a) →
        (∀ᵐ ω ∂μ, ∀ a, 0 ≤ V ω a) →
        iIndepFun (pairedCoordinates S V) μ →
…

Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.LabeledTransport.OnlineRule, OAI.MatroidProphet.LabeledTransport.ArrivalOrder, OAI.MatroidProphet.LabeledTransport.acceptedThrough, OAI.MatroidProphet.LabeledTransport.pairedCoordinates