OAI/Geometry/SurfaceImmersion/Correction/PolynomialSolveData.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Geometric and quantitative data for the already constructed finite polynomial phase solver. The operator bound here is supplied by phaseChartPolynomialOperator_bounds; it concerns the actual transported polynomial derivative.

  1. structure OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData line 15
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.norm line 57
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.κ line 61
  4. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.size line 64
  5. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.residual line 68
  6. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.exists_solution line 74