OAI/Probability/SKValue/Evolution/SmoothEvolution.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.coleHopf_gradient_pde line 12
2. lemma OAI.SKValue.integral_from_deriv_on_strip line 37
3. structure OAI.SKValue.SmoothEvolution line 57
4. lemma OAI.SKValue.SmoothTerminal.backward_jet_continuous line 71
5. lemma OAI.SKValue.SmoothTerminal.backward_gradient_continuous line 81
6. lemma OAI.SKValue.SmoothTerminal.backward_curvature_continuous line 86
7. lemma OAI.SKValue.SmoothTerminal.backward_third_continuous line 91
8. lemma OAI.SKValue.SmoothTerminal.backward_value_continuous line 97
9. lemma OAI.SKValue.SmoothTerminal.backward_value_pde line 102
10. lemma OAI.SKValue.SmoothTerminal.backward_gradient_pde line 127
11. lemma OAI.SKValue.SmoothTerminal.constant_evolution line 150