OAI/Analysis/FreeEntropy/GUEOperatorTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.gueMatrix line 8
2. theorem OAI.FiniteEntropySeparation.coordinateMatrix_norm_tail line 10
3. theorem OAI.FiniteEntropySeparation.gueMatrix_norm line 39
4. theorem OAI.FiniteEntropySeparation.gueMatrix_norm_tail line 42