OAI/AlgebraicGeometry/Seshadri/Interpolation/ConvergentSeries.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaximalSeshadri.Interpolation.Exponent line 13
2. def OAI.MaximalSeshadri.Interpolation.monomialDeriv line 15
3. lemma OAI.MaximalSeshadri.Interpolation.monomialDeriv_eq line 18
4. lemma OAI.MaximalSeshadri.Interpolation.deriv_monomialDeriv line 23
5. lemma OAI.MaximalSeshadri.Interpolation.differentiable_monomialDeriv line 27
6. def OAI.MaximalSeshadri.Interpolation.seriesPartial line 32
7. def OAI.MaximalSeshadri.Interpolation.seriesEval line 35
8. lemma OAI.MaximalSeshadri.Interpolation.seriesPartial_zero line 38
9. def OAI.MaximalSeshadri.Interpolation.derivativeMajorant line 42
10. def OAI.MaximalSeshadri.Interpolation.DerivativeSummable line 47
11. lemma OAI.MaximalSeshadri.Interpolation.norm_monomialDeriv_le line 50
12. lemma OAI.MaximalSeshadri.Interpolation.norm_seriesTerm_le line 55
13. lemma OAI.MaximalSeshadri.Interpolation.summable_seriesPartial line 65
14. lemma OAI.MaximalSeshadri.Interpolation.deriv_seriesPartial_left line 70
15. lemma OAI.MaximalSeshadri.Interpolation.deriv_seriesPartial_right line 90
16. lemma OAI.MaximalSeshadri.Interpolation.iteratedDeriv_series_left line 110
17. lemma OAI.MaximalSeshadri.Interpolation.iteratedDeriv_series_right line 125
18. theorem OAI.MaximalSeshadri.Interpolation.mixedDeriv_seriesEval line 140
19. def OAI.MaximalSeshadri.Interpolation.AbsolutelyConvergentAt line 152
20. def OAI.MaximalSeshadri.Interpolation.ConvergentSeries line 155
21. lemma OAI.MaximalSeshadri.Interpolation.descFactorial_radius_le line 158
22. theorem OAI.MaximalSeshadri.Interpolation.derivativeSummable_of_absolute line 171
23. lemma OAI.MaximalSeshadri.Interpolation.derivativeSummable_of_norm_le line 202
24. theorem OAI.MaximalSeshadri.Interpolation.mixedDeriv_limit_of_coefficients line 211