OAI/Geometry/WeakMTW/Coordinates/CoordinateGeometry.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WeakMTWGlobalSupport.CoordinateGeometry.MetricTensor line 18
  2. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.metric_invertible line 21
  3. def OAI.WeakMTWGlobalSupport.CoordinateGeometry.lowerChristoffel line 38
  4. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.lowerChristoffel_apply line 42
  5. def OAI.WeakMTWGlobalSupport.CoordinateGeometry.christoffel line 46
  6. def OAI.WeakMTWGlobalSupport.CoordinateGeometry.geodesicSpray line 49
  7. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.metric_christoffel line 54
  8. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.derivative_metric_symmetric line 62
  9. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.christoffel_symmetric line 75
  10. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.metric_compatible line 84
  11. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.contDiffOn_metric_inverse line 95
  12. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.contDiffOn_geodesicSpray line 105
  13. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.hasDerivAt_metric_pairing line 130
  14. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.geodesic_energy_hasDerivAt_zero line 146
  15. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.geodesic_energy_constant line 159
  16. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.christoffel_zero_left line 172
  17. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.christoffel_zero_right line 177
  18. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.geodesicSpray_zero line 182
  19. theorem OAI.WeakMTWGlobalSupport.CoordinateGeometry.hasFDerivAt_geodesicSpray_zero line 186