OAI/Probability/SKValue/Evolution/HeatRegularity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.ExpGrowth line 12
2. lemma OAI.SKValue.gaussian_abs_mul_exp_integrable line 15
3. lemma OAI.SKValue.expGrowth_shift_bound line 25
4. lemma OAI.SKValue.ExpGrowth.shift_integrable line 36
5. lemma OAI.SKValue.ExpGrowth.shift_mul_integrable line 43
6. lemma OAI.SKValue.gaussian_shift_hasDerivAt line 53
7. lemma OAI.SKValue.gaussian_scale_hasDerivAt line 84
8. lemma OAI.SKValue.gaussian_scale_deriv_eq line 117
9. lemma OAI.SKValue.heat_time_hasDerivAt line 132
10. lemma OAI.SKValue.heat_spatial_hasDerivAt line 145
11. lemma OAI.SKValue.heat_iteratedDeriv line 151
12. lemma OAI.SKValue.heat_contDiff line 164