OAI/Geometry/SurfaceImmersion/Correction/ExtendedCombinedMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Extend the actual local combined mean through its fixed compact support.

  1. def OAI.ClosedSurfaceR4.PhaseMean.extendedCombinedMean line 19
  2. lemma OAI.ClosedSurfaceR4.PhaseMean.extendedCombinedMean_smooth line 26
  3. lemma OAI.ClosedSurfaceR4.PhaseMean.extendedCombinedMean_value line 42
  4. lemma OAI.ClosedSurfaceR4.PhaseMean.extendedCombinedMean_difference line 54