OAI/Analysis/FreeEntropy/GaussianFlow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.classicalEntropy_continuousOn line 12
2. theorem OAI.FiniteEntropySeparation.classicalFisher_intervalIntegrable line 17
3. theorem OAI.FiniteEntropySeparation.classicalEntropy_flow line 27
4. theorem OAI.FiniteEntropySeparation.smoothedDensity_cond_le line 35
5. theorem OAI.FiniteEntropySeparation.classicalEntropy_cond_lower line 43
6. theorem OAI.FiniteEntropySeparation.classicalEntropy_cond_flow_lower line 60