OAI/Geometry/SurfaceImmersion/Correction/ChartedFreeResidual.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual free displacement solves the full metric/polynomial linearization to arbitrary finite order, in the original coordinates.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.freeResidual line 16
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.freeInitialFactor line 21
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.freeChartResidualFactor line 24
  4. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.freeResidualFactor line 28
  5. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.freeResidual_bound line 31
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.freeResidual_identity line 72
  7. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.freeDisplacement_residual_bound line 82