OAI/Probability/MatroidSecretary/Residual/FocalFamilyInvariance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The residual family is invariant under every change of the focal group's three masks, including the unlisted outcome with empty density mask.

  1. lemma OAI.MatroidProphet.FocalInvariance.focalMasks_overwrite line 12
  2. lemma OAI.MatroidProphet.FocalInvariance.focalReference_focalMasks line 44
  3. lemma OAI.MatroidProphet.FocalInvariance.focalIndex_focalMasks line 54
  4. lemma OAI.MatroidProphet.FocalInvariance.focalResidualFamily_focalMasks line 64

    Source documentation

    Equality before conditioning on listing: the fixed family uses only H, parity, weights, and density/guard/test bits outside the true group.

    lemma focalResidualFamily_focalMasks (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (κ : ℕ) (d : MainMasks n) (s : Fin n → Option ℤ) (i : ℤ) (ε : Fin 2)
    (A B C : Finset (Fin n))
    (hA : A ⊆ trueGroup M d s i) (hB : B ⊆ trueGroup M d s i)
    (hC : C ⊆ trueGroup M d s i) :
    focalResidualFamily M hE κ (focalMasks d (trueGroup M d s i) A B C) s i ε =
      focalResidualFamily M hE κ d s i ε := by
…

    Mentions: OAI.MatroidProphet.MainMasks