OAI/Probability/SKValue/Evolution/EvolutionPatch.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.patchTime_apply line 13
2. lemma OAI.SKValue.patchTime_gradient line 17
3. lemma OAI.SKValue.patchTime_jet line 21
4. lemma OAI.SKValue.SmoothEvolution.value_rhs_integrable line 26
5. lemma OAI.SKValue.SmoothEvolution.gradient_rhs_integrable line 40
6. lemma OAI.SKValue.primitive_to_integral line 57
7. lemma OAI.SKValue.SmoothEvolution.patch_value_pde line 70
8. lemma OAI.SKValue.SmoothEvolution.patch_gradient_pde line 96
9. lemma OAI.SKValue.SmoothEvolution.patch line 123