OAI/Probability/ThorpShuffle/ExceptionalShapes.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Current.full_row_iff line 13

   Source documentation

   Verification that the index predicate in exceptionalFirst excludes exactly the row and the column, rather than a merely degree-based surrogate.

   lemma full_row_iff (D : YoungDiagram) :
       D.rowLen 0 = Fintype.card (Cells D) ↔ ∀ x : Cells D, x.val.1 = 0 := by
   …

2. lemma OAI.Thorp.Current.full_column_iff line 28
3. lemma OAI.Thorp.Current.defect_zero_iff_row_or_column line 41
4. lemma OAI.Thorp.Current.exceptionalFirst_exact_nonrow_noncolumn line 52