OAI/Probability/MatroidSecretary/Pivots/MarkedPivotEdgeCases.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.MarkedPivots.oldThenMovable line 12

   Source documentation

   One legal interleaving: all old occurrences, followed by all movable occurrences.

   def oldThenMovable (r q : ℕ) : Occurrences r q → ℕ :=
   …

   Mentions: OAI.MatroidProphet.MarkedPivots.Occurrences

2. lemma OAI.MatroidProphet.MarkedPivots.oldThenMovable_ordered line 15
3. lemma OAI.MatroidProphet.MarkedPivots.oldThenMovable_injective line 19
4. lemma OAI.MatroidProphet.MarkedPivots.records_mem_patterns line 35
5. lemma OAI.MatroidProphet.MarkedPivots.patterns_nonempty line 44
6. lemma OAI.MatroidProphet.MarkedPivots.card_patterns_zero_tests line 56

   Source documentation

   With no tested labels there is exactly one (empty) mark vector, even on an empty type.

   lemma card_patterns_zero_tests (M : Matroid α) (old : Fin r → α) (movable : Fin q → α)
       (test : Fin 0 → α) (oldMark : Fin r → Bool) :
       (patterns M old movable test oldMark).card = 1 := by
   …

   Mentions: OAI.MatroidProphet.MarkedPivots.patterns

7. lemma OAI.MatroidProphet.MarkedPivots.card_patterns_zero_movable line 70

   Source documentation

   The source's s=0 endpoint has one actual pattern, not merely at most one.

   lemma card_patterns_zero_movable (M : Matroid α) (old : Fin r → α)
       (movable : Fin 0 → α) (test : Fin n → α) (oldMark : Fin r → Bool)
       (hold : ∀ i, old i ∈ M.E) (hspan : M.closure (Set.range old) = M.E)
       (htest : ∀ f, test f ∈ M.E ∧ test f ∉ M.closure ∅) :
       (patterns M old movable test oldMark).card = 1 := by
   …

   Mentions: OAI.MatroidProphet.MarkedPivots.patterns