PrefixObservationModel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MatroidProphet.orderPrefix line 10
Source documentation
The first K labels of a complete order, used only to specify the experiment.
```
def orderPrefix {n : ℕ} (π : ArrivalOrder n) (K : ℕ) : Finset (Fin n) :=
…
```
Mentions: OAI.MatroidProphet.ArrivalOrder
def OAI.MatroidProphet.prefixLabels line 14
Source documentation
Labels visible in the observation prefix of the currently available history.
```
def prefixLabels {n : ℕ} {k : Fin n} (K : ℕ) (h : History n k) : Finset (Fin n) :=
…
```
Mentions: OAI.MatroidProphet.History
def OAI.MatroidProphet.prefixWeights line 19
Source documentation
The observed weights, extended by zero away from the observation prefix. Repeated labels in malformed histories are summed; genuine histories have none.
```
noncomputable def prefixWeights {n : ℕ} {k : Fin n} (K : ℕ)
    (h : History n k) : Weights n :=
…
```
Mentions: OAI.MatroidProphet.History, OAI.MatroidProphet.Weights