OAI/Geometry/SurfaceImmersion/Correction/PolynomialSplitBudgets.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The explicit finite-chart constants have polynomial dependence on the coordinate and splitting profiles.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.tensorChartBudget_polynomial line 12
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.splitInputBudget_polynomial line 23
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.splitSizeBudget_polynomial line 29
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.splitResidualBudget_polynomial line 40