FiniteLabelingModel.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MatroidProphet.Labeling.finiteOptimum line 12
Source documentation
The same offline maximum as MatroidProphet.optimum, on an arbitrary finite ground type. The empty independent set is among the competitors.
```
noncomputable def finiteOptimum {E : Type*} [Fintype E]
    (M : Matroid E) (w : E → ℝ) : ℝ := by
…
```

def OAI.MatroidProphet.Labeling.finMatroid line 19

Source documentation

Relabel all elements, without restricting the matroid or dropping loops.

noncomputable def finMatroid {E : Type*} [Fintype E] (M : Matroid E) :
    Matroid (Fin (Fintype.card E)) := M.mapEquiv (Fintype.equivFin E)

def OAI.MatroidProphet.Labeling.finWeights line 23
Source documentation
Transport each weight along the inverse of the chosen enumeration.
```
noncomputable def finWeights {E : Type*} [Fintype E] (w : E → ℝ) :
    Weights (Fintype.card E) := fun i => w ((Fintype.equivFin E).symm i)
```
Mentions: OAI.MatroidProphet.Weights
abbrev OAI.MatroidProphet.Labeling.LabeledOrder line 28
Source documentation
A labeled arrival order uses arrival times Fin |E| and actual labels E. It is a bijection, so every label arrives exactly once.
```
abbrev LabeledOrder (E : Type*) [Fintype E] := Fin (Fintype.card E) ≃ E
```
instance OAI.MatroidProphet.Labeling.labeledOrderMeasurableSpace line 32
Source documentation
Arrival orders form a finite discrete measurable space, just as in the Fin n information model.
```
instance labeledOrderMeasurableSpace (E : Type*) [Fintype E] :
    MeasurableSpace (LabeledOrder E) := ⊤
```
Mentions: OAI.MatroidProphet.Labeling.LabeledOrder
instance OAI.MatroidProphet.Labeling.labeledOrderMeasurableSingletonClass line 35
def OAI.MatroidProphet.Labeling.encodeHistory line 39
Source documentation
Only the label coordinates of a history are relabeled.
```
def encodeHistory {E : Type*} {n : ℕ} (e : E ≃ Fin n) (k : Fin n)
    (h : Fin (k.val + 1) → E × ℝ) : History n k :=
…
```
Mentions: OAI.MatroidProphet.History
structure OAI.MatroidProphet.Labeling.LabeledOnlineRule line 45
Source documentation
A rule on arbitrary finite labels has exactly the same information restriction as OnlineRule: seed, initial samples, and the observed prefix.
```
structure LabeledOnlineRule (E : Type*) [Fintype E] [MeasurableSpace E]
    (bits : ℕ) where
…
```
def OAI.MatroidProphet.Labeling.labeledHistory line 54
Source documentation
The actual observed history for an arbitrary labeled arrival order.
```
def labeledHistory {E : Type*} [Fintype E] (v : E → ℝ)
    (π : LabeledOrder E) (k : Fin (Fintype.card E)) :
    Fin (k.val + 1) → E × ℝ :=
…
```
Mentions: OAI.MatroidProphet.Labeling.LabeledOrder
def OAI.MatroidProphet.Labeling.labeledAcceptedThrough line 60
Source documentation
Accepted labels after t arrivals in the arbitrary-label model.
```
noncomputable def labeledAcceptedThrough {E : Type*} [Fintype E] [MeasurableSpace E]
    {bits : ℕ} (A : LabeledOnlineRule E bits) (r : Seed bits)
    (s v : E → ℝ) (π : LabeledOrder E) (t : ℕ) : Finset E := by
…
```
Mentions: OAI.MatroidProphet.Labeling.LabeledOnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Labeling.LabeledOrder