OAI/Analysis/FreeEntropy/GUEFreeLaw.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.FiniteEntropySeparation.FreeTensor.sumJointMomentline 13 - theorem
OAI.FiniteEntropySeparation.FreeTensor.sumJointMoment_cyclicline 16 - theorem
OAI.FiniteEntropySeparation.FreeTensor.sumJointMoment_leftline 21 - theorem
OAI.FiniteEntropySeparation.FreeTensor.sumJointMoment_noiseline 27 - theorem
OAI.FiniteEntropySeparation.FreeTensor.expectedMatrixWord_free_tendstoline 45