Model.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

One-sample matroid selection

The rule and its finite seed law depend only on the known labeled matroid. A decision sees the initial sample vector, the entire seed, and the arriving label/value prefix. Every prefix is feasible, and decisions are irrevocable. The arrival permutation may depend on all samples, values, and seed bits. Only the actual offline optimum is required to be integrable.

abbrev OAI.MatroidProphet.Weights line 24
Also declared: ComparatorChallenges/MatroidProphet.lean:20 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:22 (same declaration text).
abbrev OAI.MatroidProphet.Seed line 25
Also declared: ComparatorChallenges/MatroidProphet.lean:21 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:23 (same declaration text).
abbrev OAI.MatroidProphet.ArrivalOrder line 26
Also declared: ComparatorChallenges/MatroidProphet.lean:22 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:24 (same declaration text).
instance OAI.MatroidProphet.arrivalOrderMeasurableSpace line 27
Also declared: ComparatorChallenges/MatroidProphet.lean:23 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:25 (same declaration text).
abbrev OAI.MatroidProphet.History line 29
Also declared: ComparatorChallenges/MatroidProphet.lean:25 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:27 (same declaration text).
structure OAI.MatroidProphet.OnlineRule line 31
Also declared: ComparatorChallenges/MatroidProphet.lean:27 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:29 (same declaration text).
def OAI.MatroidProphet.prefixIndex line 36
Also declared: ComparatorChallenges/MatroidProphet.lean:32 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:34 (same declaration text).
def OAI.MatroidProphet.history line 39
Also declared: ComparatorChallenges/MatroidProphet.lean:35 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:37 (same declaration text).
def OAI.MatroidProphet.decisionAt line 42
Also declared: ComparatorChallenges/MatroidProphet.lean:38 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:40 (same declaration text).
def OAI.MatroidProphet.acceptedThrough line 46
Also declared: ComparatorChallenges/MatroidProphet.lean:42 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:44 (same declaration text).
def OAI.MatroidProphet.accepted line 52
Also declared: ComparatorChallenges/MatroidProphet.lean:48 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:50 (same declaration text).
def OAI.MatroidProphet.reward line 56
Also declared: ComparatorChallenges/MatroidProphet.lean:52 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:54 (same declaration text).
def OAI.MatroidProphet.optimum line 60
Also declared: ComparatorChallenges/MatroidProphet.lean:56 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:58 (same declaration text).
def OAI.MatroidProphet.Feasible line 65
Also declared: ComparatorChallenges/MatroidProphet.lean:61 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:63 (same declaration text).
def OAI.MatroidProphet.pairedCoordinates line 70
Also declared: ComparatorChallenges/MatroidProphet.lean:66 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:68 (same declaration text).
def OAI.MatroidProphet.OneSampleChallenge line 74
Also declared: ComparatorChallenges/MatroidProphet.lean:70 (same declaration text), ComparatorChallenges/MatroidSecretary.lean:72 (same declaration text).
instance OAI.MatroidProphet.arrivalOrderMeasurableSingletonClass line 104
Also declared: ComparatorChallenges/MatroidSecretary.lean:102 (same declaration text).
structure OAI.MatroidProphet.HiddenRule line 107
Also declared: ComparatorChallenges/MatroidSecretary.lean:105 (same declaration text).
def OAI.MatroidProphet.observed line 111
Also declared: ComparatorChallenges/MatroidSecretary.lean:109 (same declaration text).
def OAI.MatroidProphet.hiddenAcceptedThrough line 116
Also declared: ComparatorChallenges/MatroidSecretary.lean:114 (same declaration text).
def OAI.MatroidProphet.hiddenReward line 120
Also declared: ComparatorChallenges/MatroidSecretary.lean:118 (same declaration text).
def OAI.MatroidProphet.hiddenWorstReward line 124
Also declared: ComparatorChallenges/MatroidSecretary.lean:122 (same declaration text).
def OAI.MatroidProphet.HiddenVectorChallenge line 139
Also declared: ComparatorChallenges/MatroidSecretary.lean:137 (same declaration text).
structure OAI.MatroidProphet.SecretaryRule line 161
Source documentation
A measurable secretary rule with an initially fixed observation-prefix length.
Also declared: ComparatorChallenges/MatroidSecretary.lean:158 (same declaration text).
```
structure SecretaryRule (n : ℕ) (Q : Type*) [MeasurableSpace Q] where
…
```
def OAI.MatroidProphet.SamePrefix line 169
Source documentation
Full permutations describing the same ordered observation prefix.
Also declared: ComparatorChallenges/MatroidSecretary.lean:165 (same declaration text).
```
def SamePrefix {n : ℕ} (K : ℕ) (σ π : ArrivalOrder n) : Prop :=
…
```
Mentions: OAI.MatroidProphet.ArrivalOrder
def OAI.MatroidProphet.secretaryDecisionAt line 173
Source documentation
Execution forces rejection of every observation-prefix arrival.
Also declared: ComparatorChallenges/MatroidSecretary.lean:168 (same declaration text).
```
def secretaryDecisionAt {n : ℕ} {Q : Type*} [MeasurableSpace Q]
    (A : SecretaryRule n Q) (q : Q) (w : Weights n) (π : ArrivalOrder n)
    (k : Fin n) : Bool :=
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder
def OAI.MatroidProphet.secretaryAcceptedThrough line 179
Source documentation
Irrevocable accepted labels through an arbitrary number of arrivals.
Also declared: ComparatorChallenges/MatroidSecretary.lean:173 (same declaration text).
```
noncomputable def secretaryAcceptedThrough {n : ℕ} {Q : Type*} [MeasurableSpace Q]
    (A : SecretaryRule n Q) (q : Q) (w : Weights n) (π : ArrivalOrder n)
    (t : ℕ) : Finset (Fin n) := by
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder
def OAI.MatroidProphet.secretaryReward line 186
Also declared: ComparatorChallenges/MatroidSecretary.lean:180 (same declaration text).
def OAI.MatroidProphet.SecretaryFeasible line 191
Source documentation
Feasibility is pointwise for every seed, vector, order, and arrival prefix.
Also declared: ComparatorChallenges/MatroidSecretary.lean:184 (same declaration text).
```
def SecretaryFeasible {n : ℕ} {Q : Type*} [MeasurableSpace Q]
    (M : Matroid (Fin n)) (A : SecretaryRule n Q) : Prop :=
…
```
Mentions: OAI.MatroidProphet.SecretaryRule
def OAI.MatroidProphet.Secretary.uniformArrivalLaw line 208
Source documentation
Uniform random arrival order, including the unique order on the empty ground set.
Also declared: ComparatorChallenges/MatroidSecretary.lean:200 (same declaration text).
```
noncomputable def uniformArrivalLaw (n : ℕ) : Measure (ArrivalOrder n) :=
…
```
Mentions: OAI.MatroidProphet.ArrivalOrder
def OAI.MatroidProphet.SecretaryChallenge line 224
Source documentation
The full order-oblivious conclusion of cor:secretary, including a measurable history-only rule, every-prefix feasibility, prefix rejection, arbitrary full-seed suffix adversaries, and the unchanged 2⁻²⁹³ ratio.
Also declared: ComparatorChallenges/MatroidSecretary.lean:213 (same declaration text).
```
def SecretaryChallenge.{u} : Prop :=
…
```