OAI/Geometry/SurfaceImmersion/Correction/AssembledCombinedMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Assemble the actual local mean corrections and perform a finite number of substitutions with one common scale threshold and derivative loss.

  1. def OAI.ClosedSurfaceR4.PhaseMean.assembledCombinedMean line 14
  2. theorem OAI.ClosedSurfaceR4.PhaseMean.finite_assembled_combined_mean line 19