OAI/Geometry/SurfaceImmersion/Correction/PolynomialMeanTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial majorants survive the read/restore operations in an atlas. All dependence on transport constants stays in the profile.

  1. def OAI.ClosedSurfaceR4.PhaseMean.transportedMeanGeometry line 11
  2. lemma OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanProfile_transport_bound line 14
  3. lemma OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanProfile_value_transport_bound line 49
  4. lemma OAI.ClosedSurfaceR4.PhaseMean.transportedMeanGeometry_growth line 58