OAI/Analysis/FreeEntropy/GaussianDifferential.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.normalTimeDerivative line 12
2. def OAI.FiniteEntropySeparation.normalGradient line 14
3. def OAI.FiniteEntropySeparation.normalSecond line 15
4. theorem OAI.FiniteEntropySeparation.normalKernel_hasDeriv_coordinate_at line 16
5. theorem OAI.FiniteEntropySeparation.normalGradient_hasDeriv_coordinate line 28
6. theorem OAI.FiniteEntropySeparation.normal_heatEquation line 36
7. theorem OAI.FiniteEntropySeparation.normalTimeDerivative_continuousOn line 44
8. theorem OAI.FiniteEntropySeparation.normalGradient_continuous line 52
9. theorem OAI.FiniteEntropySeparation.normalSecond_continuous line 56