SourceRankMask.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The manuscript writes the observed rank mask as D ∪ C, whereas the algorithm also removes H. The two definitions coincide on every candidate group, including empty and unlisted groups. These lemmas discharge that semantic identification without adding a premise to a source theorem.

lemma OAI.MatroidProphet.SourceRankMask.sdiff_union_of_subset_disjoint line 15
lemma OAI.MatroidProphet.SourceRankMask.nominalLayerSet_sdiff_union line 27
lemma OAI.MatroidProphet.SourceRankMask.nominalRankStatistic_mask_union line 35
lemma OAI.MatroidProphet.SourceRankMask.testRankStatistic_mask_union line 45
lemma OAI.MatroidProphet.SourceRankMask.finalRankStatistic_mask_union line 55
lemma OAI.MatroidProphet.SourceRankMask.groupMask_disjoint_H line 67

lemma OAI.MatroidProphet.SourceRankMask.listedZ_sourceMask line 75

Source documentation

Exact source mask for the nominal statistic; no listing hypothesis.

lemma listedZ_sourceMask (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (d : MainMasks n) (w : Fin n → Option ℤ) (h : ℕ) :
    listedZ M hE d w h =
      nominalRankStatistic M hE (2^100) (groupMask M d w d.D) (groupMask M d w d.C)
        (groupMask M d w d.T) h (groupMask M d w univ h)
        ((d.D ∪ d.C : Finset (Fin n)) : Set (Fin n)) (boolParity d.odd) := by
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.nominalRankStatistic, OAI.MatroidProphet.boolParity

lemma OAI.MatroidProphet.SourceRankMask.listedLambda_sourceMask line 89

Source documentation

Exact source mask for the final statistic used in the all-orders bound.

lemma listedLambda_sourceMask (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (d : MainMasks n) (w : Fin n → Option ℤ) (h : ℕ) :
    listedLambda M hE d w h =
      finalRankStatistic M hE (2^100) (groupMask M d w d.D) (groupMask M d w d.C)
        (groupMask M d w d.T) h (groups M d w).length (groupMask M d w univ h)
        ((d.D ∪ d.C : Finset (Fin n)) : Set (Fin n)) (d.T : Set (Fin n))
        (boolParity d.odd) := by
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.finalRankStatistic, OAI.MatroidProphet.boolParity

lemma OAI.MatroidProphet.SourceRankMask.listedRankStatistic_sourceMask line 105

Source documentation

Exact nominal statistic in the transfer section, including its zero branch.

lemma listedRankStatistic_sourceMask (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (κ : ℕ) (d : MainMasks n) (w : Fin n → Option ℤ) (i : ℤ) (ε : Fin 2) :
    listedRankStatistic M hE κ d w i ε =
      if i ∈ groups M d w then
        nominalRankStatistic M hE κ (groupMask M d w d.D) (groupMask M d w d.C)
          (groupMask M d w d.T) ((groups M d w).idxOf i)
          (trueGroup M d w i : Set (Fin n))
          ((d.D ∪ d.C : Finset (Fin n)) : Set (Fin n)) ε
      else 0 := by
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.nominalRankStatistic