OAI/Analysis/FreeEntropy/NormalLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.map_withDensity_of_measurePreserving line 12
2. theorem OAI.FiniteEntropySeparation.productNormal_withDensity line 22
3. def OAI.FiniteEntropySeparation.normalLaw line 44
4. theorem OAI.FiniteEntropySeparation.normalLaw_eq_map line 46
5. theorem OAI.FiniteEntropySeparation.normalLaw_eq_scaled line 56
6. theorem OAI.FiniteEntropySeparation.normalLaw_probability line 72
7. theorem OAI.FiniteEntropySeparation.smoothedLaw_eq line 75