OAI/Geometry/IsometricImmersion/Taylor/UniformTaylorDenominator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Taylor.stateBaseCompact_mem_of_norm line 14
2. theorem OAI.SmoothLocal.Taylor.stateQDenominator_uniform_fderiv_bound line 21
3. theorem OAI.SmoothLocal.Taylor.qHessian_time_hasDerivAt line 31
4. theorem OAI.SmoothLocal.Taylor.exists_uniform_Hxx_time_variation line 55
5. theorem OAI.SmoothLocal.Taylor.exists_uniform_Hxx_strip_width line 95