OAI/Analysis/FreeEntropy/GaussianCrossEntropy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.smoothedSecond_integrable line 11
2. theorem OAI.FiniteEntropySeparation.normalCross_integrable line 19
3. theorem OAI.FiniteEntropySeparation.normalCross_integral line 27
4. theorem OAI.FiniteEntropySeparation.density_event_toReal line 38
5. theorem OAI.FiniteEntropySeparation.classicalEntropy_event_gaussian line 43
6. theorem OAI.FiniteEntropySeparation.integral_heatLaw_totalSecond line 68
7. theorem OAI.FiniteEntropySeparation.normalizedEntropy_event_gaussian line 73