OAI/Analysis/FreeEntropy/FisherDeficit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.FreeTensor.fisher_cumulant_deficit line 12
2. def OAI.FiniteEntropySeparation.Model.cumulantConstant line 64
3. def OAI.FiniteEntropySeparation.Model.covarianceFisher line 65
4. def OAI.FiniteEntropySeparation.Model.fisherDeficit line 66
5. theorem OAI.FiniteEntropySeparation.Model.X_variance line 67
6. theorem OAI.FiniteEntropySeparation.Model.fisherDeficit_bounds line 70