OAI/Geometry/IsometricImmersion/Flows/FlowCurvature.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Flow.capChartDomain line 14
  2. def OAI.SmoothLocal.Flow.capFlowHeight line 16
  3. def OAI.SmoothLocal.Flow.capChart line 18
  4. def OAI.SmoothLocal.Flow.capChartRho line 21
  5. def OAI.SmoothLocal.Flow.capModelCurvature line 24
  6. theorem OAI.SmoothLocal.Flow.capChartDomain_isOpen line 27
  7. theorem OAI.SmoothLocal.Flow.capChart_zero line 29
  8. theorem OAI.SmoothLocal.Flow.capChart_one line 32
  9. theorem OAI.SmoothLocal.Flow.capChart_eq_vec line 35
  10. theorem OAI.SmoothLocal.Flow.capFlowHeight_contDiffOn line 42
  11. theorem OAI.SmoothLocal.Flow.capChart_contDiffOn line 48
  12. theorem OAI.SmoothLocal.Flow.capModelCurvature_contDiffOn line 54
  13. theorem OAI.SmoothLocal.Flow.boxPoint_coord_eta line 59
  14. theorem OAI.SmoothLocal.Flow.capFlowHeight_hasDerivAt_time line 63
  15. theorem OAI.SmoothLocal.Flow.capFlowHeight_hasDerivAt_initial line 80
  16. theorem OAI.SmoothLocal.Flow.capFlowHeight_partial_time line 99
  17. theorem OAI.SmoothLocal.Flow.capFlowHeight_partial_initial_pos line 111
  18. theorem OAI.SmoothLocal.Flow.capChartRho_pos line 119
  19. theorem OAI.SmoothLocal.Flow.capChartRho_contDiffOn line 126
  20. theorem OAI.SmoothLocal.Flow.capModelCurvature_partial line 134
  21. theorem OAI.SmoothLocal.Flow.capModelCurvature_partial_time line 156
  22. theorem OAI.SmoothLocal.Flow.capModelCurvature_partial_initial line 167
  23. theorem OAI.SmoothLocal.Flow.capChart_mem_modelSquare line 175
  24. theorem OAI.SmoothLocal.Flow.cap_model_full_principal_lower line 183
  25. theorem OAI.SmoothLocal.Flow.exists_cap_curvature_chart line 225