OAI/Geometry/SurfaceImmersion/Correction/PolynomialMetricForcedBudgets.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial constants for the actual supported forced metric solver. The scale factor in its residual is separated from its geometric budget.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.metricForcedSizeBudget line 14
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.metricForcedResidualBudget line 17
  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.metricForcedSizeBudget_polynomial line 22
  4. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.metricForcedResidualBudget_polynomial line 35
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.metric_size_eq line 59
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.metric_residual_eq line 68