OAI/Geometry/SurfaceImmersion/Correction/PolynomialPerpBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial derivative bounds for the perpendicular product and its unit normalization used by the free mode.

  1. def OAI.ClosedSurfaceR4.RealModes.crossBudget line 15
  2. def OAI.ClosedSurfaceR4.RealModes.minorTermBudget line 16
  3. def OAI.ClosedSurfaceR4.RealModes.perpBudget line 17
  4. lemma OAI.ClosedSurfaceR4.RealModes.perpBudget_nonneg line 19
  5. lemma OAI.ClosedSurfaceR4.RealModes.weighted_minor3 line 23
  6. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_perpProduct line 52
  7. lemma OAI.ClosedSurfaceR4.RealModes.weighted_perpProduct line 67