OAI/Probability/SKRatio/Matrices/MatrixQuad.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.matrixQuad line 57
2. def OAI.SKRatioGaussian.matrixOperator line 60
3. lemma OAI.SKRatioGaussian.matrixOperator_apply line 64
4. lemma OAI.SKRatioGaussian.matrixQuad_inner line 68
5. lemma OAI.SKRatioGaussian.matrixQuad_smul line 79
6. lemma OAI.SKRatioGaussian.goeMatrix_symm line 89
7. lemma OAI.SKRatioGaussian.goeMatrix_neg line 95
8. lemma OAI.SKRatioGaussian.goeMatrix_quad line 102
9. lemma OAI.SKRatioGaussian.matrixOperator_norm_le_of_quad line 131