OAI/Geometry/SurfaceImmersion/Correction/JetPolynomialOperations.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.neg line 10
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.sub line 11
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.fluct line 12
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_neg line 14
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_sub line 21
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_neg line 25
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_neg line 26
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_sub line 27
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_sub line 29
  10. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_fluct line 31
  11. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_fluct line 33
  12. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_neg line 36
  13. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_sub line 39
  14. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_fluct line 43
  15. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_fluct line 47