LabeledOneSample.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The one-sample endpoint on arbitrary finite labels

This is supporting transport for thm:main, not a new manuscript target. The enumeration is fixed from the label type before the input distributions. All labels, including loops, and all probability/online-information hypotheses are retained. The probability-space universe is independent of the label universe. No moment assumption on individual loop values is introduced.

lemma OAI.MatroidProphet.Labeling.measurable_finWeights line 22
lemma OAI.MatroidProphet.Labeling.paired_independent_finWeights line 27

theorem OAI.MatroidProphet.Labeling.one_sample_finite_labels line 43

Source documentation

The complete distribution-independent prophet guarantee after a fixed renaming of arbitrary finite labels. The order may depend on the full seed, all samples, all values, and any other randomness in the probability space.

theorem one_sample_finite_labels.{u, v} {E : Type v} [Fintype E]
    [MeasurableSpace E] [MeasurableSingletonClass E]
    (M : Matroid E) (hE : M.E = Set.univ) :
    ∃ (bits : ℕ) (ν : Measure (Seed bits)), IsProbabilityMeasure ν ∧
    ∃ A : LabeledOnlineRule E bits,
      (∀ (r : Seed bits) (s v : E → ℝ) (π : LabeledOrder E) (t : ℕ),
        (∀ e, 0 ≤ s e) → (∀ e, 0 ≤ v e) →
        M.Indep (labeledAcceptedThrough A r s v π t : Set E)) ∧
      ∀ {Ω : Type u} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
        (S V : Ω → E → ℝ) (R : Ω → Seed bits),
        Measurable S → Measurable V → Measurable R →
        (∀ᵐ ω ∂μ, ∀ e, 0 ≤ S ω e) →
…

Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.Labeling.LabeledOnlineRule, OAI.MatroidProphet.Labeling.LabeledOrder, OAI.MatroidProphet.Labeling.labeledAcceptedThrough