OAI/AlgebraicGeometry/Seshadri/Analytic/TaylorCoefficients.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.AnalyticCoordinates.wordExponent line 13
  2. lemma OAI.MaximalSeshadri.AnalyticCoordinates.wordExponent_degree line 17
  3. def OAI.MaximalSeshadri.AnalyticCoordinates.coordinateVector line 22
  4. lemma OAI.MaximalSeshadri.AnalyticCoordinates.norm_coordinateVector line 26
  5. lemma OAI.MaximalSeshadri.AnalyticCoordinates.prod_coordinate_word line 29
  6. theorem OAI.MaximalSeshadri.AnalyticCoordinates.multilinear_coordinate_expansion line 33
  7. def OAI.MaximalSeshadri.AnalyticCoordinates.ordinaryCoefficient line 51
  8. lemma OAI.MaximalSeshadri.AnalyticCoordinates.ordinaryCoefficient_norm_le line 55
  9. lemma OAI.MaximalSeshadri.AnalyticCoordinates.ordinaryCoefficient_eq_degree line 66
  10. theorem OAI.MaximalSeshadri.AnalyticCoordinates.ordinaryCoefficient_homogeneous line 73
  11. theorem OAI.MaximalSeshadri.AnalyticCoordinates.ordinaryCoefficient_geometric_bound line 96
  12. theorem OAI.MaximalSeshadri.AnalyticCoordinates.ordinaryCoefficient_absolutely_convergent line 112
  13. lemma OAI.MaximalSeshadri.AnalyticCoordinates.ordinary_hasSum_by_degree line 126
  14. lemma OAI.MaximalSeshadri.AnalyticCoordinates.ordinary_terms_summable line 136
  15. theorem OAI.MaximalSeshadri.AnalyticCoordinates.hasFPowerSeriesOnBall_ordinary_expansion line 146
  16. theorem OAI.MaximalSeshadri.AnalyticCoordinates.analyticAt_exists_ordinary_expansion line 168
  17. lemma OAI.MaximalSeshadri.AnalyticCoordinates.monomialDeriv_at_zero line 190
  18. lemma OAI.MaximalSeshadri.AnalyticCoordinates.seriesPartial_at_zero line 201
  19. theorem OAI.MaximalSeshadri.AnalyticCoordinates.mixedDeriv_at_zero line 212
  20. lemma OAI.MaximalSeshadri.AnalyticCoordinates.mixedDeriv_congr_germ line 222
  21. theorem OAI.MaximalSeshadri.AnalyticCoordinates.convergent_expansion_unique line 237
  22. def OAI.MaximalSeshadri.AnalyticCoordinates.analyticFunctionAlgebra line 247
  23. def OAI.MaximalSeshadri.AnalyticCoordinates.analyticCoefficients line 253
  24. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticCoefficients_spec line 256
  25. theorem OAI.MaximalSeshadri.AnalyticCoordinates.analyticCoefficients_eq_derivative line 269
  26. def OAI.MaximalSeshadri.AnalyticCoordinates.coeffConvolution line 286
  27. lemma OAI.MaximalSeshadri.AnalyticCoordinates.absolute_mono line 289
  28. lemma OAI.MaximalSeshadri.AnalyticCoordinates.absolute_terms_summable line 295
  29. lemma OAI.MaximalSeshadri.AnalyticCoordinates.absolute_convolution line 300
  30. lemma OAI.MaximalSeshadri.AnalyticCoordinates.seriesEval_convolution line 337