OAI/Probability/SKValue/Equations/PolynomialMoment.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValue.jetMoment line 11
  2. lemma OAI.SKValue.IsDiffusion.jetMoment_continuous line 13
  3. lemma OAI.SKValue.IsDiffusion.jetMoment_hasDerivAt line 22
  4. def OAI.SKValue.JetExpr.square line 58
  5. def OAI.SKValue.JetExpr.cube line 59
  6. def OAI.SKValue.JetExpr.momentExpr line 60
  7. def OAI.SKValue.JetExpr.curvatureExpr line 61
  8. def OAI.SKValue.JetExpr.curvatureSlope line 62
  9. lemma OAI.SKValue.JetExpr.momentExpr_eval line 63
  10. lemma OAI.SKValue.JetExpr.curvatureExpr_eval line 64
  11. lemma OAI.SKValue.JetExpr.curvatureSlope_eval line 65
  12. lemma OAI.SKValue.JetExpr.momentExpr_sourceA line 67
  13. lemma OAI.SKValue.JetExpr.momentExpr_sourceP line 69
  14. lemma OAI.SKValue.JetExpr.curvatureExpr_sourceA line 71
  15. lemma OAI.SKValue.JetExpr.curvatureExpr_sourceP line 73
  16. lemma OAI.SKValue.JetExpr.curvatureSlope_sourceA line 75
  17. lemma OAI.SKValue.JetExpr.curvatureSlope_sourceP line 77