OAI/Probability/SKValue/Equations/GradientStrip.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SKValue.GradientStrip line 18
2. lemma OAI.SKValue.mesh_mem_strip_ito line 38
3. lemma OAI.SKValue.GradientStrip.measurable_second line 45
4. def OAI.SKValue.gradientMeshError line 51
5. lemma OAI.SKValue.gradientMeshError_nonneg line 56
6. lemma OAI.SKValue.gradientMeshError_bound line 59