OAI/Probability/MatroidSecretary/Pivots/MarkedPivotContract.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Complete finite occurrence version of the marked-pivot lemma

The counting proof is inherited from the actual greedy-support/affine-sign argument. We bridge finite old lists to it only in the nonempty ambient case; the empty ambient case is proved directly, not excluded by an inhabitedness premise. Existence and uniqueness ensure the counted family does not omit an interleaving merely because its record predicate has no witness.

  1. lemma OAI.MatroidProphet.MarkedPivots.records_unique line 23
  2. lemma OAI.MatroidProphet.MarkedPivots.records_existsUnique line 37
  3. lemma OAI.MatroidProphet.MarkedPivots.card_patterns_le line 54
  4. theorem OAI.MatroidProphet.MarkedPivots.sourceContract line 97

    Source documentation

    The complete source-level marked-pivot contract.

    theorem sourceContract : SourceContract := by
…

    Mentions: OAI.MatroidProphet.MarkedPivots.SourceContract