OAI/Analysis/FreeEntropy/MatrixFisherTest.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.FiniteEntropySeparation.matrixPolynomialDerivativeline 9 - def
OAI.FiniteEntropySeparation.matrixFisherTestline 12 - def
OAI.FiniteEntropySeparation.matrixRealScoreline 14 - theorem
OAI.FiniteEntropySeparation.matrixRealScore_polynomialline 16 - theorem
OAI.FiniteEntropySeparation.matrixRealScore_derivativeline 18 - theorem
OAI.FiniteEntropySeparation.matrixRealScore_divergenceline 26 - theorem
OAI.FiniteEntropySeparation.matrixFisherTest_pointwiseline 51