OAI/Geometry/SurfaceImmersion/Correction/PrimitiveInitialMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual scalar contraction starts the primitive mean iteration. Its normalized defect is only the polynomial perturbation divided by δ².

  1. def OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveSeed line 14
  2. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveSeed_smooth line 17
  3. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.realMetricTensor_const_smul line 20
  4. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveSeed_metric line 33
  5. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveSeed_defect line 42
  6. theorem OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveSeed_defect_bound line 54