OAI/Geometry/IsometricImmersion/Coordinates/ActualShearHyperbolicity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Pulse.metricInShearCoordinates_smoothPositive line 13
2. theorem OAI.SmoothLocal.Pulse.gaussianCurvature_in_shear_coordinates line 20
3. theorem OAI.SmoothLocal.Pulse.darboux_in_shear_coordinates line 30
4. def OAI.SmoothLocal.Pulse.shearTimeFactor line 44
5. theorem OAI.SmoothLocal.Pulse.sheared_principal_coefficients line 49
6. theorem OAI.SmoothLocal.Pulse.actual_shear_hyperbolicity line 83