OAI/Probability/SKRatio/Matrices/GoeMatrixQuadCoeff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatioGaussian.goeMatrix_quad_coeff line 61
2. lemma OAI.SKRatioGaussian.diagonal_affine_matrix line 69
3. lemma OAI.SKRatioGaussian.diagonalSqrt_one line 81
4. lemma OAI.SKRatioGaussian.goe_quad_le_top line 87
5. lemma OAI.SKRatioGaussian.matrixQuad_neg line 97
6. lemma OAI.SKRatioGaussian.goe_norm_le_of_top line 102
7. theorem OAI.SKRatioGaussian.goe_norm_tail line 115