MaskModel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Concrete sacrificed-mask data for the secretary transport.

The branch and every mask coordinate are functions of the complete source seed. The test mask is deliberately not part of the sacrificed mask.

def OAI.MatroidProphet.Secretary.sourceMask line 14
Source documentation
The observation mask of the concrete source rule, before any values are seen.
```
noncomputable def sourceMask {n : ℕ} (r : Seed (mainSeedBits n)) : Finset (Fin n) :=
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits
def OAI.MatroidProphet.Secretary.branchRate line 21
Source documentation
Literal branchwise Bernoulli rates from sections/secretary.tex. false is the maximum branch and true is the main branch.
```
noncomputable def branchRate (j : Bool) : ℝ :=
…
```