OAI/Geometry/SurfaceImmersion/Correction/PolynomialModeBudgets.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The finite free and forced parametrices have polynomial budgets. These are the actual constants used by the existing mode estimates.

  1. theorem OAI.ClosedSurfaceR4.SmallModes.errorConstant_polynomial line 13
  2. theorem OAI.ClosedSurfaceR4.SmallModes.fullErrorConstant_polynomial line 23
  3. theorem OAI.ClosedSurfaceR4.SmallModes.amplitudeConstant_polynomial line 33
  4. theorem OAI.ClosedSurfaceR4.SmallModes.initialConstant_polynomial line 43
  5. theorem OAI.ClosedSurfaceR4.SmallModes.freeModeConstant_polynomial line 50
  6. theorem OAI.ClosedSurfaceR4.SmallModes.gradientErrorConstant_polynomial line 58
  7. theorem OAI.ClosedSurfaceR4.SmallModes.meanErrorConstant_polynomial line 63
  8. theorem OAI.ClosedSurfaceR4.FiniteParametrix.boundProfile_polynomial line 76
  9. theorem OAI.ClosedSurfaceR4.SmallModes.forcedModeBudget_polynomial line 88