OAI/Geometry/IsometricImmersion/Darboux/ActualDriftCoefficients.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.hessianQuotient line 14
  2. def OAI.SmoothLocal.Geometry.darbouxG line 17
  3. def OAI.SmoothLocal.Geometry.connectionTraceY line 20
  4. def OAI.SmoothLocal.Geometry.driftJ line 23
  5. def OAI.SmoothLocal.Geometry.curvatureDriftError line 27
  6. theorem OAI.SmoothLocal.Geometry.curvatureDriftError_eq line 31
  7. theorem OAI.SmoothLocal.Geometry.hessianQuotient_contDiffOn line 40
  8. theorem OAI.SmoothLocal.Geometry.darbouxG_contDiffOn line 46
  9. theorem OAI.SmoothLocal.Geometry.connectionTraceY_contDiffOn line 53
  10. theorem OAI.SmoothLocal.Geometry.driftJ_contDiffOn line 57
  11. theorem OAI.SmoothLocal.Geometry.curvatureDriftError_contDiffOn line 65
  12. theorem OAI.SmoothLocal.Geometry.curvatureWeightedDriftError_contDiffOn line 73
  13. theorem OAI.SmoothLocal.Geometry.darbouxG_pos line 79
  14. theorem OAI.SmoothLocal.Geometry.curvatureDriftError_bound line 84
  15. theorem OAI.SmoothLocal.Geometry.driftJ_bound line 95
  16. theorem OAI.SmoothLocal.Geometry.curvatureDriftError_bound_from_low_data line 128