OAI/Analysis/FreeEntropy/FreeEntropyFlow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.Model.reciprocal_variance_intervalIntegrable line 9
2. theorem OAI.FiniteEntropySeparation.Model.covarianceFisher_intervalIntegrable line 18
3. theorem OAI.FiniteEntropySeparation.Model.covarianceFisher_integral line 22
4. theorem OAI.FiniteEntropySeparation.Model.gaussianEntropy_flow line 34
5. theorem OAI.FiniteEntropySeparation.Model.fisherDeficit_intervalIntegrable line 40
6. theorem OAI.FiniteEntropySeparation.Model.heatFisherReal_intervalIntegrable line 44
7. theorem OAI.FiniteEntropySeparation.Model.chiStar_flow line 51