OAI/Geometry/IsometricImmersion/Darboux/QPositiveFloor.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.pointHessianBound line 14
  2. theorem OAI.SmoothLocal.Geometry.pointHessianBound_nonneg line 16
  3. theorem OAI.SmoothLocal.Geometry.inverseMetric_value_bound line 21
  4. theorem OAI.SmoothLocal.Geometry.christoffel_value_bound line 35
  5. theorem OAI.SmoothLocal.Geometry.covHessian_value_bound line 65
  6. def OAI.SmoothLocal.Pulse.shearedHessianUpper line 96
  7. def OAI.SmoothLocal.Pulse.shearedQPositiveFloor line 99
  8. theorem OAI.SmoothLocal.Pulse.shearedHessianUpper_pos line 102
  9. theorem OAI.SmoothLocal.Pulse.shearedQPositiveFloor_pos line 108
  10. theorem OAI.SmoothLocal.Pulse.sheared_Hxx_value_bound line 113
  11. theorem OAI.SmoothLocal.Pulse.positive_negative_ratio_floor line 148
  12. theorem OAI.SmoothLocal.Pulse.actual_sheared_Q5_floor line 161