OAI/Geometry/NilpotentCharts/Polynomials.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RawPolynomial.IsPoly line 14
2. lemma OAI.RawPolynomial.IsPoly.congr line 17
3. lemma OAI.RawPolynomial.isPoly_const line 20
4. lemma OAI.RawPolynomial.isPoly_coordinate line 21
5. lemma OAI.RawPolynomial.IsPoly.add line 22
6. lemma OAI.RawPolynomial.IsPoly.neg line 25
7. lemma OAI.RawPolynomial.IsPoly.sub line 28
8. lemma OAI.RawPolynomial.IsPoly.mul line 30
9. lemma OAI.RawPolynomial.IsPoly.pow line 33
10. lemma OAI.RawPolynomial.isPoly_sum line 36
11. lemma OAI.RawPolynomial.IsPoly.comp line 44
12. def OAI.RawPolynomial.IsPolyVec line 56
13. lemma OAI.RawPolynomial.isPolyVec_const line 58
14. lemma OAI.RawPolynomial.IsPolyVec.congr line 60
15. lemma OAI.RawPolynomial.IsPolyVec.smul line 64
16. lemma OAI.RawPolynomial.isPolyVec_sum line 68
17. lemma OAI.RawPolynomial.IsPolyVec.linear line 74
18. def OAI.RawPolynomial.primitive line 86
19. lemma OAI.RawPolynomial.derivative_primitive line 89
20. lemma OAI.RawPolynomial.primitive_eval_zero line 103
21. lemma OAI.RawPolynomial.primitive_hasDerivAt line 106
22. lemma OAI.RawPolynomial.primitive_eval₂_zero line 116
23. lemma OAI.RawPolynomial.eval₂_hasDerivAt line 120
24. lemma OAI.RawPolynomial.eval₂_substitute line 124
25. lemma OAI.RawPolynomial.eq_of_hasDerivAt_eq line 136
26. lemma OAI.RawPolynomial.triangular_ode_polynomial line 143
27. lemma OAI.RawPolynomial.triangular_ode_prefix line 230
28. lemma OAI.RawPolynomial.triangular_ode_collection line 300
29. lemma OAI.RawPolynomial.rational_projection line 374
30. lemma OAI.RawPolynomial.rational_of_integer_values line 379
31. lemma OAI.RawPolynomial.IsPolyVec.linear_apply line 431
32. lemma OAI.RawPolynomial.IsPolyVec.mem_span_integer_grid line 440
33. lemma OAI.RawPolynomial.IsPoly.comp_differentiable line 467
34. lemma OAI.RawPolynomial.IsPolyVec.comp_differentiable line 484
35. lemma OAI.RawPolynomial.isPolyVec_linear_coordinates line 496