Threshold.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact source interpretation of the cumulative count in lem:all-orders. The implementation orders listed groups increasingly by integer weight level. For an actual listed group, counting accepted labels by group index is exactly counting them by the source's rounded-weight threshold.

lemma OAI.MatroidProphet.MainAlgorithm.selected_level_mem_groups line 14

theorem OAI.MatroidProphet.MainAlgorithm.indexed_selection_eq_threshold line 26

Source documentation

No selected label has an unlisted level, so the indexed and literal weight-threshold cumulative accepted sets agree, not merely their sizes.

theorem indexed_selection_eq_threshold (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (d : MainMasks n) (w : Fin n → Option ℤ) (π : ArrivalOrder n)
    {h : ℕ} {i : ℤ} (hi : (groups M d w)[h]? = some i) :
    (selection M hE d w π).filter
      (fun e => ∃ j, w e = some j ∧ h ≤ (groups M d w).idxOf j) =
    (selection M hE d w π).filter
      (fun e => ∃ j, w e = some j ∧ i ≤ j) := by
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.MainAlgorithm.groups, OAI.MatroidProphet.MainAlgorithm.selection

theorem OAI.MatroidProphet.MainAlgorithm.listedLambda_le_threshold_count line 48
Source documentation
Literal source weight-threshold form of the deterministic clause.
```
theorem listedLambda_le_threshold_count (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (d : MainMasks n) (w : Fin n → Option ℤ) (π : ArrivalOrder n)
    {h : ℕ} {i : ℤ} (hi : (groups M d w)[h]? = some i) :
    listedLambda M hE d w h ≤
      ((selection M hE d w π).filter (fun e => ∃ j, w e = some j ∧ i ≤ j)).card := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.MainAlgorithm.groups, OAI.MatroidProphet.MainAlgorithm.listedLambda, OAI.MatroidProphet.MainAlgorithm.selection