FiniteLabelTransport.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Finite-label equivalence supporting the scope statement "every finite known labeled matroid". No positivity, nonempty-ground, or nonloop hypothesis occurs in the transport laws. The proof uses mathlib's actual matroid map, not a replacement independence predicate.

theorem OAI.MatroidProphet.Labeling.finiteOptimum_nonneg line 19
theorem OAI.MatroidProphet.Labeling.sum_le_finiteOptimum line 26
theorem OAI.MatroidProphet.Labeling.mapEquiv_finset_indep line 35
theorem OAI.MatroidProphet.Labeling.finiteOptimum_mapEquiv line 39
theorem OAI.MatroidProphet.Labeling.finMatroid_ground line 58
theorem OAI.MatroidProphet.Labeling.finWeights_nonnegative_iff line 62
theorem OAI.MatroidProphet.Labeling.optimum_finMatroid line 70
def OAI.MatroidProphet.Labeling.relabelRule line 80
Source documentation
Conjugate an actual online rule by a fixed label enumeration. In particular, the translated rule does not receive a future order or a future value.
```
noncomputable def relabelRule (A : OnlineRule (Fintype.card E) bits) :
    LabeledOnlineRule E bits where
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Labeling.LabeledOnlineRule
theorem OAI.MatroidProphet.Labeling.encode_labeledHistory line 104
theorem OAI.MatroidProphet.Labeling.relabelRule_acceptedThrough line 111
theorem OAI.MatroidProphet.Labeling.relabelRule_feasible line 126
theorem OAI.MatroidProphet.Labeling.relabelRule_reward line 139
theorem OAI.MatroidProphet.Labeling.relabelRule_ratio_iff line 149
Source documentation
Any pointwise guarantee expressed in the actual Fin n model is unchanged by transporting both the selected reward and the offline benchmark.
```
theorem relabelRule_ratio_iff (M : Matroid E)
    (A : OnlineRule (Fintype.card E) bits) (c : ℝ)
    (r : Seed bits) (s v : E → ℝ) (π : LabeledOrder E) :
    (c * finiteOptimum M v ≤
      ∑ e ∈ labeledAcceptedThrough (relabelRule A) r s v π (Fintype.card E), v e) ↔
    c * MatroidProphet.optimum (finMatroid M) (finWeights v) ≤
      reward A r (finWeights s) (finWeights v) (π.trans (Fintype.equivFin E)) := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Labeling.LabeledOrder, OAI.MatroidProphet.Labeling.finiteOptimum, OAI.MatroidProphet.Labeling.labeledAcceptedThrough, OAI.MatroidProphet.Labeling.relabelRule, OAI.MatroidProphet.optimum, OAI.MatroidProphet.Labeling.finMatroid, OAI.MatroidProphet.Labeling.finWeights, OAI.MatroidProphet.reward