OAI/Geometry/SurfaceImmersion/Correction/PolynomialMetricRemainder.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual jet-polynomial representations of every coefficient of the finite pullback-metric remainder.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.finiteMetric line 14
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_finiteMetric line 19
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.order_finiteMetric line 30
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_finiteMetric line 44
  5. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.xTangent line 58
  6. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.yTangent line 62
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_xTangent line 65
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_yTangent line 75
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_xTangent line 83
  10. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_yTangent line 97
  11. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.order_xTangent line 109
  12. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.order_yTangent line 122