OAI/Geometry/SurfaceImmersion/Correction/PolynomialMetricCoefficients.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Actual coordinate polynomial expressions for the metric coefficients in the finite oscillatory recursion. Index zero denotes the first correction.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.xCoefficient line 13
  2. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.yCoefficient line 16
  3. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.xxQuadratic line 19
  4. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.xyQuadratic line 23
  5. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.yyQuadratic line 27
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.order_xCoefficient line 31
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.order_yCoefficient line 42
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.order_xxQuadratic line 50
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.order_xyQuadratic line 62
  10. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.order_yyQuadratic line 74
  11. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_xCoefficient line 86
  12. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_yCoefficient line 97
  13. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_xxQuadratic line 106
  14. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_xyQuadratic line 118
  15. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_yyQuadratic line 130