WeightedRewardModel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A separate score vector evaluates the actual accepted labels without changing the observations or decisions. In particular, rounded analysis scores need not be substituted for the arriving weights.

def OAI.MatroidProphet.hiddenScore line 13
def OAI.MatroidProphet.hiddenWorstScore line 18
Source documentation
The order minimum is taken separately for each complete seed.
```
noncomputable def hiddenWorstScore {n bits : ℕ} (A : HiddenRule n bits)
    (w score : Weights n) (r : Seed bits) : ℝ := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed