OAI/Probability/MatroidSecretary/Accounting/Observation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The source writes the accounting sacrifice set as D ∪ C, whereas the implementation retains H ∪ D ∪ C. Every candidate is outside H, so these expressions agree on every actual nominal layer, before taking any rank.

  1. lemma OAI.MatroidProphet.MainAlgorithm.groupMask_not_mem_filter line 13
  2. lemma OAI.MatroidProphet.MainAlgorithm.nominalLayer_sacrifice_eq_source line 17