OAI/Algebra/AlgebraicObstruction/TaylorCoefficients.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.mk_surjective line 13
2. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.representative line 16
3. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.mk_representative line 19
4. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.lower line 23
5. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.lower_mk line 26
6. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv line 29
7. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_mk line 32
8. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_add line 41
9. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_one line 49
10. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_zero line 54
11. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_mul line 58
12. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_C_mul line 66
13. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.coefficient line 71
14. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.coefficient_mk line 74
15. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.coefficient_shiftDeriv line 85
16. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.coefficient_ext line 94
17. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.coefficient_map line 113
18. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.coefficient_add line 118
19. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.coefficient_sub line 125
20. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.coefficient_mem_map line 132
21. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.coefficient_mem_pow line 151
22. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.lower_shift line 166
23. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.reduction_lower line 176
24. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.lower_taylor line 183
25. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.taylor_scalar line 193
26. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.taylorAlgHom line 205
27. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDerivLinear line 213
28. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.completion_approximate line 231
29. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_mem_map line 245
30. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_mem_pow line 257
31. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_sub line 263
32. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_mem_coeff_pow line 270