OAI/AlgebraicGeometry/Seshadri/Analytic/ConvergentSeries.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MaximalSeshadri.Exponent line 14
  2. def OAI.MaximalSeshadri.monomialDeriv line 16
  3. lemma OAI.MaximalSeshadri.monomialDeriv_eq line 19
  4. lemma OAI.MaximalSeshadri.deriv_monomialDeriv line 24
  5. lemma OAI.MaximalSeshadri.differentiable_monomialDeriv line 28
  6. def OAI.MaximalSeshadri.seriesPartial line 33
  7. def OAI.MaximalSeshadri.seriesEval line 36
  8. lemma OAI.MaximalSeshadri.seriesPartial_zero line 39
  9. def OAI.MaximalSeshadri.derivativeMajorant line 43
  10. def OAI.MaximalSeshadri.DerivativeSummable line 48
  11. lemma OAI.MaximalSeshadri.norm_monomialDeriv_le line 51
  12. lemma OAI.MaximalSeshadri.norm_seriesTerm_le line 56
  13. lemma OAI.MaximalSeshadri.summable_seriesPartial line 66
  14. lemma OAI.MaximalSeshadri.deriv_seriesPartial_left line 71
  15. lemma OAI.MaximalSeshadri.deriv_seriesPartial_right line 91
  16. lemma OAI.MaximalSeshadri.iteratedDeriv_series_left line 111
  17. lemma OAI.MaximalSeshadri.iteratedDeriv_series_right line 126
  18. theorem OAI.MaximalSeshadri.mixedDeriv_seriesEval line 141
  19. def OAI.MaximalSeshadri.AbsolutelyConvergentAt line 153
  20. def OAI.MaximalSeshadri.ConvergentSeries line 156
  21. lemma OAI.MaximalSeshadri.descFactorial_radius_le line 159
  22. theorem OAI.MaximalSeshadri.derivativeSummable_of_absolute line 172