OAI/Probability/BinarySweep/MatrixBounds/CenteredMatrix.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Young.centeredMatrix line 13
2. lemma OAI.BinaryCoordinateSweeps.Young.centeredMatrix_toLin line 19
3. lemma OAI.BinaryCoordinateSweeps.Young.evenMoment_one_matrix line 23
4. theorem OAI.BinaryCoordinateSweeps.Young.specht_moment_one_le_centered_matrix line 38