synthetic differential geometry
Introductions
from point-set topology to differentiable manifolds
geometry of physics: coordinate systems, smooth spaces, manifolds, smooth homotopy types, supergeometry
Differentials
Tangency
The magic algebraic facts
Theorems
Axiomatics
(shape modality $\dashv$ flat modality $\dashv$ sharp modality)
$(ʃ \dashv \flat \dashv \sharp )$
dR-shape modality $\dashv$ dR-flat modality
$ʃ_{dR} \dashv \flat_{dR}$
(reduction modality $\dashv$ infinitesimal shape modality $\dashv$ infinitesimal flat modality)
$(\Re \dashv \Im \dashv \&)$
fermionic modality $\dashv$ bosonic modality $\dashv$ rheonomy modality
$(\rightrightarrows \dashv \rightsquigarrow \dashv Rh)$
Models
Models for Smooth Infinitesimal Analysis
smooth algebra ($C^\infty$-ring)
differential equations, variational calculus
Chern-Weil theory, ∞-Chern-Weil theory
Cartan geometry (super, higher)
Borel's Theorem (also called Borel's Lemma) says that every power series is the Taylor series of some smooth function. In other words: for every collection of prescribed partial derivatives at some point, there is a smooth function having these as its actual derivatives.
The canonical map from the ring of germs of $C^\infty$ function at $0 \in \mathbb{R}^n$ to the ring of formal power series obtained by taking the Taylor series at $0$ is surjective.
There are many extensions and variants.
For $\mathbb{R}^{n+m}$ a Cartesian space of dimension $n+m \in \mathbb{N}$, write $C^\infty(\mathbb{R}^{n+m})$ for the $\mathbb{R}$-algebra of smooth functions with values in $\mathbb{R}$.
Write $m^\infty_{\mathbb{R}^n \times \{0\}} \subset C^\infty(\mathbb{R}^{n+m})$ for the ideal of functions all whose partial derivatives along $\mathbb{R}^m$ vanish.
Forming the Taylor series constitutes an isomorphism
between smooth functions modulo those whose derivatives along $\mathbb{R}^m$ vanish and the ring of power series in $m$-variables over $C^\infty(\mathbb{R}^n)$.
This appears for instance as (Moerdijk-Reyes, theorem I.1.3).
There is a full proof in Moerdijk–Reyes, cited above. Here we prove Theorem 1 to indicate the method; the general version is not substantially different. (This is based on the proof in the English Wikipedia article at the time of writing, but with more details.)
A real power series at $0$ is given simply by an infinite sequence $c = (c_n)_{n\geq{0}}$ of real numbers. Given such a sequence, we would ideally use
but this is only correct if the sum converges on at least some neighbourhood of $0$ (in other words if the power series has a positive radius of convergence).
To ensure this, let $\psi$ be a smooth bump function chosen so that $\psi(x) = 1$ for ${|x|} \leq 1$ and $\psi(x) = 0$ for ${|x|} \geq 2$. (For example, $\psi(x) = \frac{\phi(x + 2)} {\phi(x + 2) + \phi(-x - 1)} \frac{\phi(-x + 2)} {\phi(-x + 2) + \phi(x - 1)}$, where $\phi(x)$ is $\exp(-1/x)$ when $x \gt 0$ and otherwise vanishes.) Next, choose an infinite sequence $H = (H_n)_{n\geq{1}}$ of positive finite numbers:
(where $m^{\underline{j}}$ is the falling power $\prod_{0\leq{h}\lt{j}} (m - h)$, including the special case $m! = m^{\underline{m}}$); also, let $H_0 = 0$ (the bottom element of $[0,\infty]$, since $0 \leq k \lt 0$ never occurs). Finally, define
If things go well, the derivatives of $f$ will be
and I claim that this is so. Since $\psi^{(k-i)}(H_n x) = 0$ for ${|x|} \geq 2/H_n$, we have
which is finite. This proves uniform convergence of each claimed derivative (although not equiconvergence of all at once), and so each series not only converges but also may be antidifferentiated term by term, proving that $f^{(k)}$ is as claimed.
Finally (because $\psi^{(m)}(0) = 0$ for $m \gt 0$ but $\psi(0) = 1$, and the same goes for $0^m$),
making $c_k$ the $k$th coefficient of the Taylor series of $f$ at $0$, as desired.
The original reference is
It had been actually proved by Guiseppe Peano before Borel
Textbook discussion includes
A generalization to Banach spaces is in
and is cited (along with extensive discussion and (counter)examples) also as (Ch.III) 15.4 in
Last revised on January 14, 2018 at 10:21:01. See the history of this page for a list of all contributions to it.