OAI/AlgebraicGeometry/Seshadri/Interpolation/SeshadriUpper.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.Geometry.Surface.exists_curve_ratio_lt line 18
2. lemma OAI.MaximalSeshadri.Geometry.Surface.seshadri_ratios_nonempty line 56
3. lemma OAI.MaximalSeshadri.Geometry.Surface.seshadri_ratios_bddBelow line 64
4. theorem OAI.MaximalSeshadri.Geometry.Surface.seshadri_le_sqrt line 72
5. lemma OAI.MaximalSeshadri.Geometry.Surface.seshadri_eq_of_curve_lower line 80
6. theorem OAI.MaximalSeshadri.Geometry.Surface.eventual_seshadri_equality line 91