OAI/Geometry/IsometricImmersion/Curvature/CurvatureLowerTube.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.Pulse.CurvatureFirstInput line 15
  2. def OAI.SmoothLocal.Pulse.curvatureFirstFunction line 17
  3. def OAI.SmoothLocal.Pulse.curvatureFirstDomain line 18
  4. def OAI.SmoothLocal.Pulse.curvatureFirstTube line 19
  5. def OAI.SmoothLocal.Pulse.actualCurvatureFirstInput line 22
  6. def OAI.SmoothLocal.Pulse.thetaCurvatureFirstIncrement line 25
  7. theorem OAI.SmoothLocal.Pulse.curvatureFirstDet_contDiff line 29
  8. theorem OAI.SmoothLocal.Pulse.curvatureFirstDomain_isOpen line 34
  9. theorem OAI.SmoothLocal.Pulse.curvatureFirstFunction_contDiffOn line 37
  10. theorem OAI.SmoothLocal.Pulse.curvatureFirstTube_isCompact line 42
  11. theorem OAI.SmoothLocal.Pulse.curvatureFirstTube_subset_domain line 46
  12. theorem OAI.SmoothLocal.Pulse.curvatureFirstTube_fderiv_bound line 51
  13. theorem OAI.SmoothLocal.Pulse.theta_first_segment_det line 61
  14. theorem OAI.SmoothLocal.Pulse.theta_first_segment_subset_tube line 70
  15. theorem OAI.SmoothLocal.Pulse.thetaPulseLowerDifference_eq_firstFunction line 89
  16. theorem OAI.SmoothLocal.Pulse.thetaCurvatureFirstIncrement_norm_le line 94
  17. theorem OAI.SmoothLocal.Pulse.exists_uniform_thetaPulseLowerDifference_bound line 119