OAI/AlgebraicGeometry/Seshadri/Interpolation/Moments.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.Interpolation.zero_of_moments line 12
2. def OAI.MaximalSeshadri.Interpolation.rows line 37
3. def OAI.MaximalSeshadri.Interpolation.row line 39
4. theorem OAI.MaximalSeshadri.Interpolation.mem_row line 42
5. theorem OAI.MaximalSeshadri.Interpolation.row_nonempty line 51
6. def OAI.MaximalSeshadri.Interpolation.rowMoment line 56
7. def OAI.MaximalSeshadri.Interpolation.EulerJetZero line 59
8. theorem OAI.MaximalSeshadri.Interpolation.row_zero_of_euler_jet line 63
9. theorem OAI.MaximalSeshadri.Interpolation.card_sub_one_le_span line 75
10. def OAI.MaximalSeshadri.Interpolation.planeForm line 89
11. theorem OAI.MaximalSeshadri.Interpolation.planeForm_nonneg_on_hull line 91
12. def OAI.MaximalSeshadri.Interpolation.transverse line 105
13. def OAI.MaximalSeshadri.Interpolation.balancedStrip line 108
14. theorem OAI.MaximalSeshadri.Interpolation.balanced_row_constraints line 113
15. theorem OAI.MaximalSeshadri.Interpolation.balanced_diagram_card line 143
16. theorem OAI.MaximalSeshadri.Interpolation.balanced_triangle_euler_test line 170
17. theorem OAI.MaximalSeshadri.Interpolation.transverse_affine line 187
18. theorem OAI.MaximalSeshadri.Interpolation.convex_balancedStrip line 194