Contents

Definition

A power series in a variable $X$ and with coefficients in a ring $R$ is a series of the form

with coefficients $(a_n\in R{)}_{n=0}^{\mathrm{\infty }}$. If there are no additional convergence conditions on a power series we call it for emphasis also formal power series.

If there is $k\in \mathbb{N}$ such that $a_n=0$ for all $n>k$ then this is a polynomial of degree $k$.

The collection of formal power series in variable $X$ with coefficients in a commutative ring $R$ is denoted $R[[X]]$.

More generally, one considers power series ${\sum }_{n_1=0,n_2=0,\dots ,n_k=0}^{\mathrm{\infty }}{a}_{n_1\dots n_k}{X}_1^{n_1}{X}_2^{n_2}\cdots X_k^{n_k}$ in $k$ variables $X_1,\dots ,X_k$ which are declared commutative with $a_{n_1\dots n_k}\in R$, where $R$ is commutative; they form a formal power series ring $R[[X_1,\dots ,X_k]]$. More generally, we can consider noncommutative (associative unital) ring $R$ and words in noncommutative variables $X_1,\dots ,X_k$ of the form

(where $m$ has nothing to do with $k$) and with coefficient $a_w\in R$ (here $w$ is a word of any length, not a multiindex in the previous sense). Thus the power sum is of the form ${\sum }_w{a}_w{X}_w$ and they form a formal power series ring in variables $X_1,\dots ,X_k$ denoted by $R⟨⟨X_1,\dots ,X_k⟩⟩$. Furthermore, $R$ can be even a noncommutative semiring in which case the words belong to the free monoid on the set $S=\{X_1,\dots ,X_k\}$, the partial sums are then belong to a monoid semiring $R⟨S⟩$. The formal power series then also form a semiring, by the multiplication rule

Of course, this implies that in a specialization, $b$-s commute with variables $X_{i_k}$; what is usually generalized to take some endomorphisms into an account (like at noncommutative polynomial level of partial sums where we get skew-polynomial rings, i.e. iterated Ore extensions).

Examples

Taylor series

• Taylor series

MacLaurin series

For $f\in C^{\mathrm{\infty }}(ℝ)$ a smooth function on the real line, and for $f^{(n)}\in C^{\mathrm{\infty }}(ℝ)$ denoting its $n$th derivative its MacLaurin series (its Taylor series at $0$) is the power series

If this power series converges to $f$, then we say that $f$ is analytic.

Laurent series

• Laurent series

Puiseux series

• Puiseux series

Related concepts

• convergence radius

References

A formalization in homotopy type theory and there in Coq is discussed in section 4 of

• Álvaro Pelayo, Vladimir Voevodsky, Michael Warren, A preliminary univalent formalization of the p-adic numbers (arXiv:1302.1207)