TransferContracts.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.MatroidProphet.TransferContracts.recordsPivots_unique line 15

Source documentation

An injectively timed sequence determines one recorded pivot-mark vector.

lemma recordsPivots_unique (M : Matroid α) (label : Occurrence r q → α)
    (test : Fin n → α) (time : Occurrence r q → ℕ)
    (htime : Function.Injective time) (oldMark : Fin r → Bool)
    (movableMark : Fin q → Bool) {t u : Finset (Fin n)}
    (ht : RecordsPivots M label test time oldMark movableMark t)
    (hu : RecordsPivots M label test time oldMark movableMark u) : t = u := by
…

theorem OAI.MatroidProphet.TransferContracts.marked_pivot_contract line 35

Source documentation

Complete marked-pivot contract: arbitrary repeated/redundant old labels, all placements/orders/marks of at most s movable occurrences, and the exact binomial bound. Source old-spanning/nonloop assumptions ensure every permitted interleaving actually contributes exactly one vector. No positivity assumption on s, q, r, or n is imposed.

theorem marked_pivot_contract (M : Matroid α) (b : ℕ → α) (a : Fin q → α)
    (test : Fin n → α) (oldMark : Fin r → Bool) (s : ℕ) (hqs : q ≤ s)
    (hground : ∀ o : Occurrence r q, occurrenceLabel b a o ∈ M.E)
    (holdspan : M.closure (oldPrefix b r) = M.E)
    (htest : ∀ f, test f ∈ M.E ∧ test f ∉ M.closure ∅) :
    (markedPivotPatterns M b a test oldMark).card ≤
        4 ^ s * ∑ k ∈ Finset.Iic s, n.choose k ∧
      ∀ (time : Occurrence r q → ℕ), OldOrdered time → Function.Injective time →
        ∀ movableMark : Fin q → Bool,
          ∃! t, t ∈ markedPivotPatterns M b a test oldMark ∧
            RecordsPivots M (occurrenceLabel b a) test time oldMark movableMark t := by
…

lemma OAI.MatroidProphet.TransferContracts.comparison_group_indep_subset line 62
Source documentation
The independent comparison group is constructed by priority greedy and fair-mask deletion, exactly as in the manuscript (Y_i = (I* \ H) ∩ U_i).
```
lemma comparison_group_indep_subset (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (d : MainMasks n) (a : Fin n → Option ℤ) (i : ℤ) :
    let Y := (positiveGreedy M a \ d.H).filter (fun e => a e = some i)
…
```
Mentions: OAI.MatroidProphet.MainMasks
theorem OAI.MatroidProphet.TransferContracts.sample_to_rank_contract line 81
Source documentation
Full sample-to-rank inequality for the actual rounded weight vector. withMasks averages all density, guard and test bits while fixing H; fairParityExpectation averages parity. listedRankStatistic is explicitly zero on the unlisted branch. Thus there is no conditioning on listing and no independence assumption about the selected residual.
```
theorem sample_to_rank_contract (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (w : Weights n) (d : MainMasks n) (i : ℤ)
    (hn : densityThreshold ≤
      ((trueGroup M d (fun e => roundedLevel weightBase (w e)) i).card : ℝ)) :
    let a := fun e => roundedLevel weightBase (w e)
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.densityThreshold, OAI.MatroidProphet.roundedLevel, OAI.MatroidProphet.weightBase