OAI/Probability/SKValue/Coercivity/CurvatureMoment.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.IsDiffusion.polyJet_integrable line 12
2. lemma OAI.SKValue.IsDiffusion.jetMoment_hasDerivAt_integral line 20
3. lemma OAI.SKValue.IsDiffusion.momentExpr_hasDerivAt line 26
4. lemma OAI.SKValue.IsDiffusion.curvatureExpr_hasDerivAt line 31
5. lemma OAI.SKValue.IsDiffusion.curvatureSlope_hasDerivAt line 41
6. lemma OAI.SKValue.continuousAt_of_constant_interval line 61
7. lemma OAI.SKValue.IsDiffusion.jetMoment_continuousAt line 66
8. lemma OAI.SKValue.momentExpr_eq_gradientMoment line 71
9. lemma OAI.SKValue.IsDiffusion.curvature_convexOn line 75
10. lemma OAI.SKValue.IsDiffusion.moment_convexOn_zero line 93
11. lemma OAI.SKValue.IsDiffusion.moment_convexOn_zero_closed line 111