OAI/AlgebraicGeometry/Seshadri/Interpolation/ActualInterpolation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.ActualInterpolation.absolute_of_derivativeSummable line 16
2. def OAI.MaximalSeshadri.ActualInterpolation.seriesValueMap line 24
3. theorem OAI.MaximalSeshadri.ActualInterpolation.exists_common_representation line 36
4. lemma OAI.MaximalSeshadri.ActualInterpolation.mixedDeriv_congr_on_ball line 60
5. def OAI.MaximalSeshadri.ActualInterpolation.germCoefficients line 78
6. theorem OAI.MaximalSeshadri.ActualInterpolation.idealPower_test_of_series_test line 83