OAI/Analysis/FreeEntropy/GUEFock.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.FiniteEntropySeparation.matrixTraceWord_gue_mapline 11 - theorem
OAI.FiniteEntropySeparation.gueTraceWord_stein_pureline 15 - theorem
OAI.FiniteEntropySeparation.gueTraceWord_expected_tendstoline 27 - theorem
OAI.FiniteEntropySeparation.gueTraceWord_probability_tendstoline 48