OAI/Geometry/SurfaceImmersion/Correction/PolynomialMeanError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for the actual normalized mean error and its amplitude difference, with explicit finite derivative loss.

  1. theorem OAI.ClosedSurfaceR4.RealModes.polynomial_normalizedMeanError line 15
  2. theorem OAI.ClosedSurfaceR4.RealModes.polynomial_normalizedMeanError_difference line 45