OAI/Probability/SKGap/Localization/Conjugation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.ComplexMatrix.conjugate_frobenius line 13
  2. def OAI.SKGap.ComplexMatrix.conjugateIsometry line 19
  3. lemma OAI.SKGap.ComplexMatrix.conjugate_opNorm line 24
  4. lemma OAI.SKGap.ComplexMatrix.matrixProject_conjugate line 33
  5. lemma OAI.SKGap.ComplexMatrix.truncatedG_conjugate line 45
  6. lemma OAI.SKGap.ComplexMatrix.truncatedK_conjugate line 57
  7. def OAI.SKGap.signConjugate line 75
  8. def OAI.SKGap.signUnitary line 78
  9. lemma OAI.SKGap.sign_conjugate_entry line 89
  10. lemma OAI.SKGap.sign_conjugate_diagonal line 95
  11. lemma OAI.SKGap.sign_conjugate_lift line 106
  12. lemma OAI.SKGap.realPart_sign_conjugate line 111
  13. lemma OAI.SKGap.realTruncatedK_sign line 116