OAI/Probability/SKGap/Matrix/MatrixSeminorm.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.offDiagonalVector line 14
  2. def OAI.SKGap.diagonalSeminorm line 16
  3. def OAI.SKGap.offDiagonalSeminorm line 17
  4. lemma OAI.SKGap.diagonalSeminorm_sq line 20
  5. lemma OAI.SKGap.offDiagonalSeminorm_fourth line 23
  6. lemma OAI.SKGap.diagonalSeminorm_le line 39
  7. lemma OAI.SKGap.offDiagonalSeminorm_le line 44
  8. lemma OAI.SKGap.diagonalVector_sub line 69
  9. lemma OAI.SKGap.diagonalVector_add line 71
  10. lemma OAI.SKGap.offDiagonalVector_sub line 73
  11. lemma OAI.SKGap.offDiagonalVector_add line 78
  12. lemma OAI.SKGap.diagonalSeminorm_lipschitz line 83
  13. lemma OAI.SKGap.offDiagonalSeminorm_lipschitz line 88
  14. lemma OAI.SKGap.diagonalSeminorm_add line 96
  15. lemma OAI.SKGap.offDiagonalSeminorm_add line 99