OAI/Geometry/IsometricImmersion/Calculus/MovingFirstJetBase.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Hyperbolic.spatialFirstJet line 14
2. theorem OAI.SmoothLocal.Hyperbolic.spatialJet_firstJet_eq_word line 16
3. theorem OAI.SmoothLocal.Hyperbolic.coordinateBound_spatialFirstJet line 24
4. def OAI.SmoothLocal.Hyperbolic.firstJetSliceBudget line 33
5. theorem OAI.SmoothLocal.Hyperbolic.firstJetSliceBudget_coe line 36
6. theorem OAI.SmoothLocal.Hyperbolic.coordinateBound_to_spatialFirstJet_L2 line 41
7. theorem OAI.SmoothLocal.Hyperbolic.coordinateC8_to_spatialFirstJet_L2_seven line 76
8. theorem OAI.SmoothLocal.Hyperbolic.spatialFirstJet_slice_memLp_two line 85