OAI/Probability/BinarySweep/MatrixBounds/MatrixProjection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Density.projectionMatrix line 12
2. lemma OAI.BinaryCoordinateSweeps.Density.projectionMatrix_linear line 15
3. lemma OAI.BinaryCoordinateSweeps.Density.projectionMatrix_psd line 20
4. lemma OAI.BinaryCoordinateSweeps.Density.projectionMatrix_idempotent line 25
5. lemma OAI.BinaryCoordinateSweeps.Density.trace_toEuclideanLinear line 34
6. lemma OAI.BinaryCoordinateSweeps.Density.projectionMatrix_trace line 43
7. lemma OAI.BinaryCoordinateSweeps.Density.projectionMatrix_coeff line 50
8. lemma OAI.BinaryCoordinateSweeps.Density.projectionMatrix_commutes line 60