OAI/Probability/BinarySweep/MatrixBounds/MatrixSqrtBlocks.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Density.block_diagonal_commute line 12
2. lemma OAI.BinaryCoordinateSweeps.Density.sqrt_block_diagonal line 21
3. lemma OAI.BinaryCoordinateSweeps.Density.sqrt_submatrix_invariant line 32
4. lemma OAI.BinaryCoordinateSweeps.Density.sqrt_gram line 39