OAI/Probability/SKGap/Matrix/MatrixQuad.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.matrixQuad line 56
  2. def OAI.SKGap.matrixOperator line 59
  3. lemma OAI.SKGap.matrixOperator_apply line 63
  4. lemma OAI.SKGap.matrixQuad_inner line 67
  5. lemma OAI.SKGap.matrixQuad_smul line 78
  6. lemma OAI.SKGap.goeMatrix_symm line 88
  7. lemma OAI.SKGap.goeMatrix_neg line 94
  8. lemma OAI.SKGap.goeMatrix_quad line 101
  9. lemma OAI.SKGap.matrixOperator_norm_le_of_quad line 130
  10. lemma OAI.SKGap.goeMatrix_quad_coeff line 156
  11. lemma OAI.SKGap.diagonal_affine_matrix line 164
  12. lemma OAI.SKGap.diagonalSqrt_one line 176
  13. lemma OAI.SKGap.goe_quad_le_top line 182
  14. lemma OAI.SKGap.matrixQuad_neg line 192
  15. lemma OAI.SKGap.goe_norm_le_of_top line 197
  16. theorem OAI.SKGap.goe_norm_tail line 210