CandidateSpecification.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MatroidProphet.CandidateSpecification.higher line 11
Source documentation
Strict rounded-weight priority, including the fixed label tie-breaking rule.
```
def higher {n : ℕ} (f : Fin n) (a : Option ℤ) (e : Fin n) (b : Option ℤ) : Prop :=
…
```
def OAI.MatroidProphet.CandidateSpecification.candidates line 19
Source documentation
Source candidate set: positive, unobserved, and not spanned by higher-priority observed labels. The full candidate set is analytical, not given to the algorithm.
```
noncomputable def candidates {n : ℕ} (M : Matroid (Fin n))
    (a : Fin n → Option ℤ) (H : Finset (Fin n)) : Finset (Fin n) := by
…
```
def OAI.MatroidProphet.CandidateSpecification.greedy line 27
Source documentation
Positive priority-greedy on the entire ground set, characterized by failure of the strictly higher-priority labels to span the current label.
```
noncomputable def greedy {n : ℕ} (M : Matroid (Fin n))
    (a : Fin n → Option ℤ) : Finset (Fin n) := by
…
```
def OAI.MatroidProphet.CandidateSpecification.survivors line 34
Source documentation
The source comparison independent set after sacrificing the fair mask.
```
noncomputable def survivors {n : ℕ} (M : Matroid (Fin n))
    (a : Fin n → Option ℤ) (H : Finset (Fin n)) : Finset (Fin n) :=
…
```
def OAI.MatroidProphet.CandidateSpecification.CandidateMass line 40
Source documentation
The complete mathematical assertion of Lemma lem:filter, stated solely using the concrete source definitions and the finite independent fair-mask law.
```
def CandidateMass : Prop :=
…
```