OAI/Geometry/SurfaceImmersion/Correction/PolynomialJetSmoothness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite correction expressions have coefficients smooth throughout the admissible low-jet domain. No higher jets occur in coefficient inverses.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_longitudinal line 13
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_transverse line 22
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_initial line 30
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_step line 39
  5. theorem OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.coefficients_smooth line 56