OAI/Geometry/IsometricImmersion/Pulses/PulseCurvaturePrincipal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Pulse.thetaPulseMetric line 14
  2. def OAI.SmoothLocal.Pulse.thetaPulseFirstJet line 17
  3. def OAI.SmoothLocal.Pulse.thetaPulseLowerDifference line 20
  4. theorem OAI.SmoothLocal.Pulse.thetaPulseMetric_entry line 25
  5. theorem OAI.SmoothLocal.Pulse.metricFirstJet_thetaPulseMetric line 29
  6. theorem OAI.SmoothLocal.Pulse.secondCoordPartial_add line 52
  7. theorem OAI.SmoothLocal.Pulse.thetaPulseLowerDifference_eq line 68
  8. theorem OAI.SmoothLocal.Pulse.thetaPulse_curvature_density line 76
  9. theorem OAI.SmoothLocal.Pulse.thetaPulseLowerDifference_contDiffOn line 97
  10. theorem OAI.SmoothLocal.Pulse.inverseShearMatrix_det line 107
  11. theorem OAI.SmoothLocal.Pulse.inverseShearMatrix_isUnit line 110
  12. def OAI.SmoothLocal.Pulse.metricInShearCoordinates line 114
  13. theorem OAI.SmoothLocal.Pulse.metricInShearCoordinates_test line 117
  14. theorem OAI.SmoothLocal.Pulse.actual_pulse_curvature_density line 124