OAI/Probability/SKValue/Evolution/BoundedSmooth.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SKValue.BoundedSmooth line 12
2. lemma OAI.SKValue.BoundedSmooth.bound_zero line 16
3. lemma OAI.SKValue.BoundedSmooth.const line 20
4. lemma OAI.SKValue.BoundedSmooth.deriv line 27
5. lemma OAI.SKValue.BoundedSmooth.add line 33
6. lemma OAI.SKValue.BoundedSmooth.mul line 46
7. lemma OAI.SKValue.BoundedSmooth.const_mul line 66
8. lemma OAI.SKValue.BoundedSmooth.expGrowth line 69
9. def OAI.SKValue.expJet line 74
10. lemma OAI.SKValue.expJet_boundedSmooth line 78
11. lemma OAI.SKValue.exp_iteratedDeriv line 84
12. lemma OAI.SKValue.exp_iteratedDeriv_growth line 101
13. lemma OAI.SKValue.coleHopf_contDiff_of_pos line 108