OAI/Geometry/IsometricImmersion/Comparison/ShearFirstJetComparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Pulse.affineFirstJetMap line 12
2. theorem OAI.SmoothLocal.Pulse.affineFirstJetMap_sub line 16
3. theorem OAI.SmoothLocal.Pulse.actualCurvatureFirstInput_affinePullback line 26
4. theorem OAI.SmoothLocal.Pulse.abs_sum_fin_two_le line 39
5. theorem OAI.SmoothLocal.Pulse.affineFirstJetMap_norm_le_eight line 44
6. theorem OAI.SmoothLocal.Pulse.inverseShearMatrix_entry_le_one line 94
7. theorem OAI.SmoothLocal.Pulse.actual_shear_first_jet_distance_le line 98
8. theorem OAI.SmoothLocal.Pulse.actualCurvatureFirstInput_thetaPulseMetric line 115
9. theorem OAI.SmoothLocal.Pulse.actual_sheared_solution_first_jet_error line 124