GreedyExecution.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact agreement between the source's previous-accepted-label test and the concrete implementation's previous-eligible-label test. No arrival-order assumption beyond the explicit arrival times is used in span preservation.

theorem OAI.MatroidProphet.layerGreedy_closure_prior line 15

Source documentation

Rejected earlier eligible labels do not change the span of a layer prefix.

theorem layerGreedy_closure_prior (M : Matroid α) (E : Finset α)
    (base : ℤ → Set α) (layer : α → ℤ) (time : α → ℕ)
    (hE : M.E = Set.univ) (b : ℤ) (k : ℕ) :
    M.closure (base b ∪ layerPrior E layer time b k) =
      M.closure (base b ∪
        layerPrior (layerGreedy M E base layer time) layer time b k) := by
…

Mentions: OAI.MatroidProphet.layerPrior, OAI.MatroidProphet.layerGreedy

theorem OAI.MatroidProphet.layerGreedy_mem_iff_previous_accepted line 37

Source documentation

The online decision can be implemented using only earlier accepted labels of the same layer, exactly as in step 3 of the manuscript algorithm.

theorem layerGreedy_mem_iff_previous_accepted (M : Matroid α) (E : Finset α)
    (base : ℤ → Set α) (layer : α → ℤ) (time : α → ℕ)
    (hE : M.E = Set.univ) (e : α) :
    e ∈ layerGreedy M E base layer time ↔
      e ∈ E ∧ e ∉ M.closure (base (layer e) ∪
        layerPrior (layerGreedy M E base layer time) layer time (layer e) (time e)) := by
…

Mentions: OAI.MatroidProphet.layerGreedy, OAI.MatroidProphet.layerPrior

theorem OAI.MatroidProphet.conditionalRank_singleton_eq_one_iff line 51
Source documentation
On a finite ground set the source's rank-one test is precisely nonmembership in the closure, including rank-zero and loop cases.
```
theorem conditionalRank_singleton_eq_one_iff [Fintype α] (M : Matroid α)
    (hE : M.E = Set.univ) (P : Set α) (e : α) :
    conditionalRank M {e} P = 1 ↔ e ∉ M.closure P := by
…
```
Mentions: OAI.MatroidProphet.conditionalRank

theorem OAI.MatroidProphet.layerGreedy_mem_iff_rank_previous_accepted line 61

Source documentation

Exact rank form of the source's accept/reject condition.

theorem layerGreedy_mem_iff_rank_previous_accepted [Fintype α]
    (M : Matroid α) (E : Finset α) (base : ℤ → Set α)
    (layer : α → ℤ) (time : α → ℕ) (hE : M.E = Set.univ) (e : α) :
    e ∈ layerGreedy M E base layer time ↔
      e ∈ E ∧ conditionalRank M {e} (base (layer e) ∪
        layerPrior (layerGreedy M E base layer time) layer time (layer e) (time e)) = 1 := by
…

Mentions: OAI.MatroidProphet.layerGreedy, OAI.MatroidProphet.conditionalRank, OAI.MatroidProphet.layerPrior

theorem OAI.MatroidProphet.layerKeyDecision_eq_rank_previous_accepted line 72

Source documentation

The concrete history-based online decision agrees with the rank test on previously accepted labels in the current layer.

theorem layerKeyDecision_eq_rank_previous_accepted {n : ℕ} {K : Type*}
    (M : Matroid (Fin n)) (hE : M.E = Set.univ) (base : ℤ → Set (Fin n))
    (assign : Fin n → K → Option ℤ) (v : Fin n → K)
    (π : ArrivalOrder n) (k : Fin n) :
    layerKeyDecision M base assign k (keyHistory v π k) = true ↔
      π k ∈ assignedEligible assign v ∧
      conditionalRank M {π k} (base (assignedLayer assign v (π k)) ∪
        layerPrior
          (layerGreedy M (assignedEligible assign v) base (assignedLayer assign v)
            (fun e => (π.symm e).val))
          (assignedLayer assign v) (fun e => (π.symm e).val)
          (assignedLayer assign v (π k)) k.val) = 1 := by
…

Mentions: OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.layerKeyDecision, OAI.MatroidProphet.keyHistory, OAI.MatroidProphet.assignedEligible, OAI.MatroidProphet.conditionalRank, OAI.MatroidProphet.assignedLayer, OAI.MatroidProphet.layerPrior, OAI.MatroidProphet.layerGreedy