OAI/Geometry/IsometricImmersion/Flows/FlowSecondVariation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Flow.initialFlowDerivative line 12
  2. theorem OAI.SmoothLocal.Flow.flowCoordinateMap_mem_modelSquare line 26
  3. theorem OAI.SmoothLocal.Flow.flowPullback_contDiffOn line 38
  4. theorem OAI.SmoothLocal.Flow.initialFlowDerivative_eq_pairPartialY line 46
  5. theorem OAI.SmoothLocal.Flow.initialFlowDerivative_contDiffOn line 54
  6. theorem OAI.SmoothLocal.Flow.flowPullback_partial_y line 63
  7. theorem OAI.SmoothLocal.Flow.cap_flow_initial_second_hasDerivAt line 92
  8. theorem OAI.SmoothLocal.Flow.cap_flow_initial_second_formula line 124
  9. theorem OAI.SmoothLocal.Flow.flow_initial_second_integral_bound line 132
  10. theorem OAI.SmoothLocal.Flow.cap_flow_initial_second_bound line 171