OAI/Geometry/SurfaceImmersion/Correction/JetPolynomialVector.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Four coordinate polynomials represent the actual vector families used by the metric recursion. Dot products and both derivatives preserve representation.

  1. abbrev OAI.ClosedSurfaceR4.JetPolynomial.R4 line 14
  2. abbrev OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression line 15
  3. def OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.SmoothCoeffs line 19
  4. def OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.Represents line 22
  5. def OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.add line 26
  6. def OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.slow line 27
  7. def OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.angle line 28
  8. def OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.mean line 29
  9. def OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.primitive line 30
  10. def OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.dot line 32
  11. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.smoothCoeffs_dot line 35
  12. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.order_dot_le line 41
  13. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.loss_dot_le line 47
  14. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.order_slow_le line 53
  15. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.loss_slow_le line 59
  16. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.represents_add line 64
  17. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.eval_dot line 71
  18. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.represents_slow line 85
  19. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.represents_angle line 107
  20. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.represents_mean line 119
  21. lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.represents_primitive line 135