OAI/Probability/SKValue/Evolution/ColeHopf.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.heat line 12
2. def OAI.SKValue.coleHopf line 15
3. lemma OAI.SKValue.density_hasDerivAt line 18
4. lemma OAI.SKValue.density_mul_integrable line 31
5. lemma OAI.SKValue.gaussian_exp_abs_integrable line 38
6. lemma OAI.SKValue.lipschitz_exp_bound line 54
7. lemma OAI.SKValue.lipschitz_exp_integrable line 68
8. lemma OAI.SKValue.lipschitz_exp_integral_pos line 79
9. lemma OAI.SKValue.gaussian_stein_of_integrable line 84
10. lemma OAI.SKValue.exponential_heat_hasDerivAt line 113
11. lemma OAI.SKValue.lipschitz_heat_integrable line 150
12. lemma OAI.SKValue.heat_hasDerivAt line 165
13. lemma OAI.SKValue.coleHopf_hasDerivAt_of_pos line 183
14. lemma OAI.SKValue.coleHopf_deriv_bound_of_pos line 202