OAI/Geometry/SurfaceImmersion/Correction/SupportedMeanError.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual zero-phase metric error is bilinear in the free seeds.

  1. def OAI.ClosedSurfaceR4.SmallModes.seedMeanError line 15
  2. lemma OAI.ClosedSurfaceR4.SmallModes.seedMeanError_sub_left line 21
  3. lemma OAI.ClosedSurfaceR4.SmallModes.seedMeanError_sub_right line 38
  4. lemma OAI.ClosedSurfaceR4.SmallModes.seedMeanError_difference line 55
  5. lemma OAI.ClosedSurfaceR4.SmallModes.seedMeanError_smooth line 63