OAI/NumberTheory/Jacobsthal/Estimates/BivariateCalculus.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos970.ErdosImplicitCurvature.Bivariate line 11
2. def OAI.Erdos970.ErdosImplicitCurvature.peval line 13
3. def OAI.Erdos970.ErdosImplicitCurvature.partialX line 16
4. def OAI.Erdos970.ErdosImplicitCurvature.partialY line 17
5. theorem OAI.Erdos970.ErdosImplicitCurvature.peval_C line 19
6. theorem OAI.Erdos970.ErdosImplicitCurvature.peval_add line 21
7. theorem OAI.Erdos970.ErdosImplicitCurvature.peval_mul line 23
8. theorem OAI.Erdos970.ErdosImplicitCurvature.peval_X_zero line 25
9. theorem OAI.Erdos970.ErdosImplicitCurvature.peval_X_one line 26
10. theorem OAI.Erdos970.ErdosImplicitCurvature.peval_zero line 27
11. theorem OAI.Erdos970.ErdosImplicitCurvature.peval_one line 28
12. theorem OAI.Erdos970.ErdosImplicitCurvature.mixed_partials line 30
13. theorem OAI.Erdos970.ErdosImplicitCurvature.hasDerivAt_peval line 36
14. theorem OAI.Erdos970.ErdosImplicitCurvature.hasDerivAt_peval_graph line 63