OAI/Analysis/FreeEntropy/TensorMatrices.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.tensorMatrixTuple line 9
2. theorem OAI.FiniteEntropySeparation.tensorMatrixTuple_some line 11
3. theorem OAI.FiniteEntropySeparation.tensorMatrixTuple_none line 13
4. theorem OAI.FiniteEntropySeparation.tensorMatrixTuple_norm_le line 15
5. theorem OAI.FiniteEntropySeparation.tensorMatrixTuple_isHermitian line 27
6. theorem OAI.FiniteEntropySeparation.tensorMatrixTuple_word line 36
7. theorem OAI.FiniteEntropySeparation.tensorMatrixTuple_moment line 55