OAI/Analysis/FreeEntropy/MatrixHilbertSchmidt.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.hsVector line 10
  2. def OAI.FiniteEntropySeparation.hsNorm line 12
  3. theorem OAI.FiniteEntropySeparation.hsNorm_sq line 13
  4. theorem OAI.FiniteEntropySeparation.hsNorm_nonneg line 17
  5. theorem OAI.FiniteEntropySeparation.hsNorm_add line 18
  6. theorem OAI.FiniteEntropySeparation.hsNorm_sub line 21
  7. theorem OAI.FiniteEntropySeparation.hsNorm_star line 24
  8. theorem OAI.FiniteEntropySeparation.hsNorm_mul_left line 28
  9. theorem OAI.FiniteEntropySeparation.hsNorm_mul_right line 46
  10. theorem OAI.FiniteEntropySeparation.hsNorm_unitary_conjugate line 54
  11. theorem OAI.FiniteEntropySeparation.hermitianChart_injective line 69
  12. theorem OAI.FiniteEntropySeparation.matrixCoordinates_hermitianMatrix line 76
  13. def OAI.FiniteEntropySeparation.rotateCoordinates line 81
  14. theorem OAI.FiniteEntropySeparation.conjugate_hermitian line 83
  15. theorem OAI.FiniteEntropySeparation.hermitianMatrix_rotate line 89
  16. theorem OAI.FiniteEntropySeparation.rotateCoordinates_norm line 92
  17. def OAI.FiniteEntropySeparation.rotateLinearIsometryEquiv line 100