LayerImplementation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The layer rule is the source's accepted-prefix greedy rule

The implementation tests the span of all previous eligible labels. The source algorithm tests the span of the previous accepted labels. Prefix span preservation makes these tests exactly equal, not merely comparable in final reward.

lemma OAI.MatroidProphet.layerGreedy_closure_prefix line 16

theorem OAI.MatroidProphet.layerGreedy_mem_iff_accepted_prefix line 37

Source documentation

The actual layer acceptance test may use only its earlier accepted labels.

theorem layerGreedy_mem_iff_accepted_prefix {α : Type*} [DecidableEq α]
    (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) ∪
        {f | f ∈ layerGreedy M E base layer time ∧
          layer f = layer e ∧ time f < time e}) := by
…

Mentions: OAI.MatroidProphet.layerGreedy

theorem OAI.MatroidProphet.layerGreedy_mem_iff_rank_one line 51

Source documentation

Exact conditional-rank form of the source test at an arrival.

theorem layerGreedy_mem_iff_rank_one {α : Type*} [Fintype α] [DecidableEq α]
    (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) ∪
        {f | f ∈ layerGreedy M E base layer time ∧
          layer f = layer e ∧ time f < time e}) = 1 := by
…

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