OAI/Geometry/SurfaceImmersion/Correction/PolynomialMetricForcing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The right-hand sides of the finite triangular correction step are actual higher-jet polynomials. Their maximal jet order is the preceding order plus one.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.mixedForcing line 12
  2. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.longitudinalForcing line 17
  3. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.transverseForcing line 21
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_xCoefficient line 24
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_yCoefficient line 31
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_xxQuadratic line 37
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_xyQuadratic line 45
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_yyQuadratic line 53
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_mixedForcing line 61
  10. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_longitudinalForcing line 69
  11. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.forcing_orders line 76