OAI/Geometry/Immersion/ClosedSurface/OscillationBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.SmallModes.norm_iteratedFDeriv_exp_real line 12
2. lemma OAI.ClosedSurfaceR4.SmallModes.norm_unitMode line 19
3. lemma OAI.ClosedSurfaceR4.SmallModes.contDiff_unitMode line 27
4. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_unitMode line 34
5. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_oscillate line 62
6. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_oscillate line 68
7. def OAI.ClosedSurfaceR4.SmallModes.forcedModeConstant line 88
8. lemma OAI.ClosedSurfaceR4.SmallModes.forcedModeConstant_nonneg line 93
9. theorem OAI.ClosedSurfaceR4.SmallModes.weighted_modeApprox line 103