OAI/Geometry/Immersion/ClosedSurface/MeanDifferences.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.SmallModes.gradientAmplitude_congr line 13
2. lemma OAI.ClosedSurfaceR4.SmallModes.gradientAmplitude_sub line 17
3. lemma OAI.ClosedSurfaceR4.SmallModes.gradientAmplitude_free_sub line 26
4. lemma OAI.ClosedSurfaceR4.SmallModes.leadingDerivative_sub line 43
5. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_modeMeanError line 48
6. lemma OAI.ClosedSurfaceR4.SmallModes.modeMeanError_sub_left line 59
7. lemma OAI.ClosedSurfaceR4.SmallModes.modeMeanError_sub_right line 71
8. lemma OAI.ClosedSurfaceR4.SmallModes.modeMeanError_difference line 83
9. theorem OAI.ClosedSurfaceR4.SmallModes.weighted_modeMeanError_difference line 98