OAI/Geometry/IsometricImmersion/Curvature/CurvatureParameter.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.ODE.coordinate_square_isOpen line 17

    Also declared: ComparatorChallenges/IsometricImmersion.lean:31 (same declaration text).

  2. def OAI.SmoothLocal.ODE.coordinatePoint line 25
  3. theorem OAI.SmoothLocal.ODE.coordinatePoint_mem_square line 28
  4. theorem OAI.SmoothLocal.ODE.coordinatePoint_hasDerivAt_y line 36
  5. def OAI.SmoothLocal.ODE.curvatureYDerivative line 44
  6. theorem OAI.SmoothLocal.ODE.curvatureYDerivative_smooth line 48
  7. theorem OAI.SmoothLocal.ODE.compact_x_mem_square_interval line 56
  8. def OAI.SmoothLocal.ODE.coordinateCurvatureFamily line 60
  9. theorem OAI.SmoothLocal.ODE.coordinateCurvatureFamily_apply line 63
  10. theorem OAI.SmoothLocal.ODE.coordinateCurvatureFamily_contDiffOn line 74
  11. theorem OAI.SmoothLocal.ODE.coordinateCurvatureFamily_norm_le line 103
  12. def OAI.SmoothLocal.ODE.prescribedVolterraFamily line 113
  13. theorem OAI.SmoothLocal.ODE.prescribedVolterraFamily_contDiffOn line 117
  14. theorem OAI.SmoothLocal.ODE.prescribedVolterraFamily_equation line 126