MarkedPivotSpecification.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.MatroidProphet.MarkedPivots.Occurrences line 12
def OAI.MatroidProphet.MarkedPivots.label line 14
def OAI.MatroidProphet.MarkedPivots.mark line 17
def OAI.MatroidProphet.MarkedPivots.OldOrdered line 20
def OAI.MatroidProphet.MarkedPivots.FirstSpans line 24
Source documentation
The label is first spanned at this occurrence, and not before it.
```
def FirstSpans {α : Type*} {r q : ℕ} (M : Matroid α)
    (labels : Occurrences r q → α) (time : Occurrences r q → ℕ)
    (e : α) (o : Occurrences r q) : Prop :=
…
```
Mentions: OAI.MatroidProphet.MarkedPivots.Occurrences

def OAI.MatroidProphet.MarkedPivots.Records line 31

Source documentation

The finite set encodes precisely those test coordinates whose pivot has mark one.

def Records {α : Type*} {r q n : ℕ} (M : Matroid α)
    (old : Fin r → α) (movable : Fin q → α) (test : Fin n → α)
    (time : Occurrences r q → ℕ) (oldMark : Fin r → Bool)
    (movableMark : Fin q → Bool) (pattern : Finset (Fin n)) : Prop :=
…

Mentions: OAI.MatroidProphet.MarkedPivots.Occurrences

def OAI.MatroidProphet.MarkedPivots.patterns line 39

Source documentation

All actual pivot-mark vectors over all interleavings and all movable marks.

noncomputable def patterns {α : Type*} {r q n : ℕ} (M : Matroid α)
    (old : Fin r → α) (movable : Fin q → α) (test : Fin n → α)
    (oldMark : Fin r → Bool) : Finset (Finset (Fin n)) := by
…

def OAI.MatroidProphet.MarkedPivots.SourceContract line 50
Source documentation
Full named source obligation, including well-definedness for every interleaving. The test function is injective because the manuscript tests a set of n nonloops. The conclusion actually remains true without that injectivity assumption.
```
def SourceContract.{u} : Prop :=
…
```