OAI/Geometry/IsometricImmersion/Estimates/ActualHighEquation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.HighEquation.coordinateChainTerm line 12
2. def OAI.SmoothLocal.HighEquation.coordinateChainSum line 16
3. def OAI.SmoothLocal.HighEquation.actualHighRemainder line 19
4. theorem OAI.SmoothLocal.HighEquation.chainTerm_eq_coordinateChainTerm line 23
5. theorem OAI.SmoothLocal.HighEquation.chainSum_eq_coordinateChainSum line 33
6. theorem OAI.SmoothLocal.HighEquation.actualP_single_linearization line 45
7. theorem OAI.SmoothLocal.HighEquation.actual_differentiated_Darboux line 57
8. theorem OAI.SmoothLocal.HighEquation.actual_differentiated_Darboux_at line 85