OAI/Geometry/SurfaceImmersion/Correction/PolynomialLocalMeanProfile.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The local mean operator has explicit polynomial majorants in the geometric profile and the current tensor norm.

  1. def OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanProfile line 13
  2. theorem OAI.ClosedSurfaceR4.PhaseMean.polynomial_local_mean_majorants line 16