OAI/Probability/MatroidSecretary/Pivots/RawPatternCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Literal eq:raw-pattern-count (transfer.tex:282--285), before the exponential relaxation. The family is the actual fixed labeled residual family, not a replacement cardinality expression. The empty-group case is included.

  1. theorem OAI.MatroidProphet.integerResidualFamily_card_raw line 15
  2. theorem OAI.MatroidProphet.labeledResidualFamily_card_raw line 25

    Source documentation

    Both subset choices and both marked-sequence counts are retained exactly. No lower bound on the group size or density threshold is needed.

    theorem labeledResidualFamily_card_raw (M : Matroid α) (hE : M.E = Set.univ)
    (U : Finset α) (κ : ℕ) (F : ℤ → Set α) (a : ℤ) (ε : Fin 2)
    (K : ParityWindow a ε → Set α) :
    (labeledResidualFamily M U κ F a ε K).card ≤
      (binomialSum U.card (U.card / κ))^2 *
        (4^(2*(U.card / κ)) * binomialSum U.card (2*(U.card / κ)))^2 := by
…

    Mentions: OAI.MatroidProphet.labeledResidualFamily