OAI/AlgebraicGeometry/Seshadri/Interpolation/LaurentMoments.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.Interpolation.sum_rows line 9
2. theorem OAI.MaximalSeshadri.Interpolation.laurentEval_eq_sum line 27
3. def OAI.MaximalSeshadri.Interpolation.MomentJetZero line 33
4. theorem OAI.MaximalSeshadri.Interpolation.eulerJetZero_iff_momentJetZero line 36
5. theorem OAI.MaximalSeshadri.Interpolation.contDiffAt_zpow_ne_zero line 47
6. theorem OAI.MaximalSeshadri.Interpolation.laurentEval_mixed_deriv line 51
7. theorem OAI.MaximalSeshadri.Interpolation.mixedJetZero_moments line 77
8. theorem OAI.MaximalSeshadri.Interpolation.MomentJetZero.polynomial line 102
9. def OAI.MaximalSeshadri.Interpolation.affinePolynomial line 125
10. theorem OAI.MaximalSeshadri.Interpolation.affinePolynomial_degree line 129
11. theorem OAI.MaximalSeshadri.Interpolation.MomentJetZero.affine line 137
12. theorem OAI.MaximalSeshadri.Interpolation.primitiveRoot_fourier_sum line 151
13. theorem OAI.MaximalSeshadri.Interpolation.root_project_moments line 166
14. theorem OAI.MaximalSeshadri.Interpolation.MomentJetZero.image line 208