OAI/Geometry/IsometricImmersion/Taylor/ChainResidual.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.HighEquation.ChainWord.single line 13
2. def OAI.SmoothLocal.HighEquation.ChainWord.pair line 14
3. def OAI.SmoothLocal.HighEquation.ChainWord.triple line 15
4. def OAI.SmoothLocal.HighEquation.ChainWord.children line 17
5. def OAI.SmoothLocal.HighEquation.chainSum line 20
6. theorem OAI.SmoothLocal.HighEquation.chainSum_append line 24
7. theorem OAI.SmoothLocal.HighEquation.chainSum_replicate line 30
8. theorem OAI.SmoothLocal.HighEquation.chainSum_children line 36
9. theorem OAI.SmoothLocal.HighEquation.chainSum_hasDerivAt line 43
10. theorem OAI.SmoothLocal.HighEquation.ChainWord.children_properties line 57
11. def OAI.SmoothLocal.HighEquation.topResidualWords line 67
12. theorem OAI.SmoothLocal.HighEquation.topResidualWords_properties line 74
13. theorem OAI.SmoothLocal.HighEquation.topResidualWords_sum_succ line 121
14. theorem OAI.SmoothLocal.HighEquation.topResidual_high_unique line 131