OAI/AlgebraicGeometry/Seshadri/Interpolation/TriangleJets.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Interpolation.triangleDoubleArea line 9
2. theorem OAI.MaximalSeshadri.Interpolation.triangle_subset_balanced line 12
3. theorem OAI.MaximalSeshadri.Interpolation.triangle_euler_test line 69
4. def OAI.MaximalSeshadri.Interpolation.fallingSequence line 83
5. theorem OAI.MaximalSeshadri.Interpolation.linearMap_zero_power_of_falling line 89
6. def OAI.MaximalSeshadri.Interpolation.polynomialMoment line 103
7. theorem OAI.MaximalSeshadri.Interpolation.polynomialMoment_apply line 107
8. def OAI.MaximalSeshadri.Interpolation.FallingJetZero line 111
9. theorem OAI.MaximalSeshadri.Interpolation.fallingJetZero_eulerJetZero line 117
10. theorem OAI.MaximalSeshadri.Interpolation.triangle_falling_test line 133
11. def OAI.MaximalSeshadri.Interpolation.laurentEval line 145
12. theorem OAI.MaximalSeshadri.Interpolation.contDiffAt_zpow_one line 148
13. theorem OAI.MaximalSeshadri.Interpolation.laurentRow_deriv_one line 152
14. theorem OAI.MaximalSeshadri.Interpolation.laurentEval_mixed_deriv_one line 162
15. def OAI.MaximalSeshadri.Interpolation.MixedJetZero line 183
16. theorem OAI.MaximalSeshadri.Interpolation.mixedJetZero_iff_fallingJetZero line 187
17. theorem OAI.MaximalSeshadri.Interpolation.triangle_mixed_jet_test line 191