OAI/Geometry/IsometricImmersion/Darboux/HeightPrincipalBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.gaussianCurvature_coordinate_bound_one_closed line 13
  2. def OAI.SmoothLocal.Flow.heightAJetBound line 32
  3. theorem OAI.SmoothLocal.Flow.heightG1JetBound_nonneg line 36
  4. theorem OAI.SmoothLocal.Flow.heightAJetBound_nonneg line 44
  5. theorem OAI.SmoothLocal.Flow.heightBJetBound_nonneg line 53
  6. theorem OAI.SmoothLocal.Flow.heightRemainderBound_nonneg line 61
  7. theorem OAI.SmoothLocal.Flow.capFlowHeight_partial_bound_of_rho line 71
  8. theorem OAI.SmoothLocal.Flow.capPullback_bound_one_from_partials line 93
  9. theorem OAI.SmoothLocal.Flow.heightChartA_bound_one line 121
  10. theorem OAI.SmoothLocal.Flow.heightChartB_primitive_bounds line 151