SeedModel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Reindexing a secretary rule's complete initial seed

An arbitrary finite predrawn kernel table is represented by a single finite index. This is a measurable bijection of the complete seed, not a statistic of it. The rule continues to read only its initial seed and the available history.

def OAI.MatroidProphet.reindexSecretarySeed line 20

Source documentation

Reindex a secretary rule through any measurable decoding map.

def reindexSecretarySeed {n : ℕ} {Q Q' : Type*}
    [MeasurableSpace Q] [MeasurableSpace Q']
    (A : SecretaryRule n Q) (f : Q' → Q) (hf : Measurable f) : SecretaryRule n Q' where
…

Mentions: OAI.MatroidProphet.SecretaryRule

def OAI.MatroidProphet.secretaryFinSeed line 30
Source documentation
Canonical finite-index representation, with no nonemptiness restriction.
```
noncomputable def secretaryFinSeed {n : ℕ} {Q : Type*}
    [Fintype Q] [MeasurableSpace Q] (A : SecretaryRule n Q) :
    SecretaryRule n (Fin (Fintype.card Q)) :=
…
```
Mentions: OAI.MatroidProphet.SecretaryRule
def OAI.MatroidProphet.secretaryFinSeedLaw line 36
Source documentation
Push the complete finite seed law forward along the same canonical bijection.
```
noncomputable def secretaryFinSeedLaw {Q : Type*} [Fintype Q] [MeasurableSpace Q]
    (ν : Measure Q) : Measure (Fin (Fintype.card Q)) :=
…
```
def OAI.MatroidProphet.SecretaryGuarantee line 42
Source documentation
Performance against every full-seed-aware suffix adversary, on an arbitrary ambient probability space. The seed law is fixed before the weight vector.
```
def SecretaryGuarantee.{u} {n : ℕ} {Q : Type*} [MeasurableSpace Q]
    (M : Matroid (Fin n)) (A : SecretaryRule n Q) (ν : Measure Q) (c : ℝ) : Prop :=
…
```
Mentions: OAI.MatroidProphet.SecretaryRule