OAI/Probability/BinarySweep/YoungTheory/KoszulBlocks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Signed.orderedBlocks line 12
2. def OAI.BinaryCoordinateSweeps.Signed.blockPerm line 15
3. lemma OAI.BinaryCoordinateSweeps.Signed.blockPerm_apply line 19
4. lemma OAI.BinaryCoordinateSweeps.Signed.block_lt_iff line 25
5. lemma OAI.BinaryCoordinateSweeps.Signed.block_le_iff line 31
6. lemma OAI.BinaryCoordinateSweeps.Signed.pairWeight_sameBlock line 37
7. lemma OAI.BinaryCoordinateSweeps.Signed.pairWeight_differentBlock line 45
8. theorem OAI.BinaryCoordinateSweeps.Signed.koszulSign_blocks line 54