OAI/Geometry/SurfaceImmersion/Correction/PolynomialFixedOrderThreshold.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

At each fixed order, the reciprocal of the scale threshold is polynomial in the numerical data and reciprocal geometric margins.

  1. theorem OAI.ClosedSurfaceR4.ExactCorrection.fixedOrderNumericalBudget_polynomial line 13
  2. lemma OAI.ClosedSurfaceR4.ExactCorrection.min_inverse_le_add line 31
  3. theorem OAI.ClosedSurfaceR4.ExactCorrection.fixedOrderThreshold_inverse_polynomial line 39