OAI/Geometry/Immersion/ClosedSurface/MeanError.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ClosedSurfaceR4.SmallModes.FreeCoefficient line 15
2. lemma OAI.ClosedSurfaceR4.SmallModes.FreeCoefficient.sub line 21
3. def OAI.ClosedSurfaceR4.SmallModes.leadingDerivative line 30
4. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_leadingDerivative line 33
5. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_leadingDerivative line 40
6. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_gradient_free line 53
7. def OAI.ClosedSurfaceR4.SmallModes.modeMeanError line 77
8. def OAI.ClosedSurfaceR4.SmallModes.meanErrorConstant line 83
9. lemma OAI.ClosedSurfaceR4.SmallModes.meanErrorConstant_nonneg line 86
10. theorem OAI.ClosedSurfaceR4.SmallModes.weighted_modeMeanError line 95