OAI/Geometry/SurfaceImmersion/Correction/PerturbationTaylorBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite polynomial perturbation has a cubic nonlinear remainder with one fixed scale loss.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.taylorRemainder line 16
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.taylorRemainder_identity line 19
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.expression_taylorRemainder_smooth line 31
  4. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.compact_taylorRemainder_bound line 37