LabeledHiddenVector.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The full hidden-vector endpoint on arbitrary finite labels

The enumeration is fixed before weights. These exact transport identities preserve observation, sacrifice, every prefix, and the order minimum before integration; they do not merely rename an expected fixed-order reward.

def OAI.MatroidProphet.Labeling.relabelHiddenRule line 22
theorem OAI.MatroidProphet.Labeling.relabelHiddenRule_observed line 27
theorem OAI.MatroidProphet.Labeling.relabelHiddenRule_acceptedThrough line 35
theorem OAI.MatroidProphet.Labeling.relabelHiddenRule_reward line 55
theorem OAI.MatroidProphet.Labeling.relabelHiddenRule_worstReward line 65
Source documentation
The set of labeled orders is transported bijectively, so the exact seedwise adversarial minimum, not just any one order, is preserved.
```
theorem relabelHiddenRule_worstReward (A : HiddenRule (Fintype.card E) bits)
    (w : E → ℝ) (r : Seed bits) :
    labeledHiddenWorstReward (relabelHiddenRule A) w r =
      hiddenWorstReward A (finWeights w) r := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Labeling.labeledHiddenWorstReward, OAI.MatroidProphet.Labeling.relabelHiddenRule, OAI.MatroidProphet.hiddenWorstReward, OAI.MatroidProphet.Labeling.finWeights
theorem OAI.MatroidProphet.Labeling.relabelHiddenRule_feasible line 83
theorem OAI.MatroidProphet.Labeling.labeledHiddenAcceptedThrough_disjoint_mask line 99
Source documentation
A hidden label remains sacrificed for every order and every prefix, irrespective of what the online core would have decided.
```
theorem labeledHiddenAcceptedThrough_disjoint_mask
    (A : LabeledHiddenRule E bits) (r : Seed bits) (w : E → ℝ)
    (π : LabeledOrder E) (t : ℕ) :
    Disjoint (labeledHiddenAcceptedThrough A r w π t) (A.mask r) := by
…
```
Mentions: OAI.MatroidProphet.Labeling.LabeledHiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Labeling.LabeledOrder, OAI.MatroidProphet.Labeling.labeledHiddenAcceptedThrough

theorem OAI.MatroidProphet.Labeling.hidden_vector_finite_labels line 108

Source documentation

Literal arbitrary-finite-label version of the hidden-vector result. All masked labels, loops, empty types, ties and zero weights are retained.

theorem hidden_vector_finite_labels (M : Matroid E) (hE : M.E = Set.univ) :
    ∃ (bits : ℕ) (ν : Measure (Seed bits)), IsProbabilityMeasure ν ∧
    ∃ A : LabeledHiddenRule E bits,
      (∀ (w : E → ℝ), (∀ e, 0 ≤ w e) →
        ∀ (r : Seed bits) (π : LabeledOrder E) (t : ℕ),
          M.Indep (labeledHiddenAcceptedThrough A r w π t : Set E)) ∧
      ∀ (w : E → ℝ), (∀ e, 0 ≤ w e) →
        ((2 : ℝ) ^ 293)⁻¹ * finiteOptimum M w ≤
          ∫ r, labeledHiddenWorstReward A w r ∂ν := by
…

Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.Labeling.LabeledHiddenRule, OAI.MatroidProphet.Labeling.LabeledOrder, OAI.MatroidProphet.Labeling.labeledHiddenAcceptedThrough, OAI.MatroidProphet.Labeling.finiteOptimum, OAI.MatroidProphet.Labeling.labeledHiddenWorstReward