Dieudonné's proof of Taylor's formula I'm having trouble understanding a lemma which Dieudonné in "Foundations of Modern Analysis", chapter 8.14, pp. 185-186, uses to proof Taylor's formula, and then the proof of the formula itself with this lemma. First, for proving the lemma, Dieudonné uses the following theorem for the derivative of a continuous bilinear map:
Theorem 8.1.4: Let E, F, G be Banach spaces, and $ E \times F \rightarrow G: (x,y) \mapsto [x \cdot y] $ a continuous bilinear map. Then this mapping is differentiable at every point (x, y), and for $ (s, t) \in E \times F $ the derivative is the linear mapping
$ D[x \cdot y](s,t) = [x \cdot t] + [s \cdot y]. \qquad \qquad $(1)
The lemma is then:
Lemma 8.14.1: Let $ I \subset \mathbb{R} $ be an open interval, with two functions $ f \in C_E^p(I) $ and $ g \in C_F^p(I) $, and the continuous bilinear map $ E \times F \rightarrow G: (x,y) \mapsto [x \cdot y] $. Then $ [f \cdot g] $ belongs to $ C_G^p(I) $, and
$ [f \cdot D^pg] - (-1)^p [D^pf \cdot g] = D \big( [f \cdot D^{p-1}g] +(-1)^1 [Df \cdot D^{p-2}g] + \cdots + (-1)^{p-1} [D^{p-1}f \cdot g] \big) $.
And finally Taylor's formula:
Theorem 8.14.2: Let $ I \subset \mathbb{R} $ be an open interval, and a function $ f \in C_E^p(I) $. Then for any pair of points $ \alpha, \xi \in I $
$ f(\xi) = f(\alpha) + \frac{\xi - \alpha}{1!} f'(\alpha) + \frac{(\xi - \alpha)^2}{2!} f''(\alpha) + \cdots + \frac{(\xi - \alpha)^{p-1}}{(p-1)!} f^{(p-1)}(\alpha) + \int_{\alpha}^{\xi} \frac{(\xi - \zeta)^{p-1}}{(p-1)!} f^{(p)}(\zeta) \, d\zeta $.
Dieudonné says, tersely, that the lemma is immediately verified by applying theorem 8.1.4. And that the formula itself is proved by applying 8.14.1 to the bilinear mapping $ (\lambda,x) \mapsto \lambda x $ and to the function $ g(\zeta) = \frac{(\xi - \zeta)^{p-1}}{(p-1)!} $, and then by integrating both sides between $ \alpha $ and $ \xi $.
Thinking about this for quite some time and trying around didn't bring me any closer to understanding these proofs. I have no idea how to apply 8.1.4 to prove 8.14.1. If the arguments of the bilinear map are functions, then what are the arguments s and t? What would be the meaning of the terms on the rhs of an equality like
$ D[f \cdot D^{p-1}g](s,t)= [f \cdot t]+[s \cdot D^{p-1}g] $?
The only idea I have here is that (1) can turn into something like a product rule if the derivatives of the arguments x, y of the bilinear map are applied as (s, t):
$ D[f \cdot g](Df,Dg) = [f \cdot Dg] + [Df \cdot g]. \qquad \qquad $(2)
And I don't understand how to apply 8.14.1 to Taylor's formula, either.
Can anyone help me with this? Thanks a lot in advance.
 A: Well, the original idea has turned out to be valid, at least for proving the lemma. The decisive point is that $ D[f \cdot g] $ always has to be understood as $ D[f \cdot g](Df,Dg) $; it is a shortcut which Dieudonné uses. This is because we have to apply the chain rule. This becomes clearer if we use the notation $ \lambda(x,y) $ for the continuous bilinear map as Serge Lang does. Then we see immediately that
$ D \big( \lambda(f,g) \big) = \lambda'(f,g) \circ (Df,Dg) $.
With this we can write lemma 8.14.1 as
$
 \begin{align*}
  &[f \cdot D^pg] - (-1)^p [D^pf \cdot g] = D \big( [f \cdot D^{p-1}g] +(-1)^1 [Df \cdot D^{p-2}g] + \cdots + (-1)^{p-1} [D^{p-1}f \cdot g] \big) \\
  &= \sum_{i=0}^{p-1} (-1)^i D[D^if \cdot D^{p-1-i}g] = \sum_{i=0}^{p-1} (-1)^i D[D^if \cdot D^{p-1-i}g] (D^{i+1}f, D^{p-i}g) \\
&= \sum_{i=0}^{p-1} (-1)^i [D^if \cdot D^{p-i}g] + [D^{i+1}f \cdot D^{p-1-i}g].
 \end{align*} (3)
$
The proof of the lemma can then be done by induction over p. The beginning is done by (2). The induction step is achieved by differentiating the induction premise. Later in the process, a substitution $ Df \rightarrow f $ has to be made, i.e., the induction premise is applied again (here in the original, non-differentiated shape), this time to the bilinear map $ [Df \cdot g] $.
For anyone interested, here are the details:
The induction claim, under the assumption that $ f, g \in C^{p+1} $, is
$
 \begin{align*}
  &[f \cdot D^{p+1}g] - (-1)^{p+1} [D^{p+1}f \cdot g] = \sum_{i=0}^p (-1)^i D[D^if \cdot D^{p-i}g] (D^{i+1}f, D^{p+1-i}g) \\
  &= \sum_{i=0}^p (-1)^i [D^if \cdot D^{p+1-i}g] + [D^{i+1}f \cdot D^{p-i}g].
 \end{align*} (4)
$
We differentiate (3)
$
 \begin{align*}
  &[f \cdot D^{p+1}g] + [Df \cdot D^pg] - (-1)^p \big( [D^pf \cdot Dg]+[D^{p+1}f \cdot g] \big) \\
  &= \sum_{i=0}^{p-1} (-1)^i \big( [D^if \cdot D^{p+1-i}g] + [D^{i+1}f \cdot
  D^{p-i}g] + [D^{i+1}f \cdot
  D^{p-i}g] + [D^{i+2}f \cdot D^{p-1-i}g] \big).
 \end{align*}
$
Rewriting the result gives
$
 \begin{align*}
  &[f \cdot D^{p+1}g] + (-1)^{p+1} [D^{p+1}f \cdot g] + [Df \cdot D^pg] - (-1)^p [D^pf \cdot Dg] \\
  &= \sum_{i=0}^{p-1} (-1)^i \big( [D^if \cdot D^{p+1-i}g] + [D^{i+1}f \cdot D^{p-i}g]  \big)+ \sum_{i=0}^{p-1} (-1)^i \big( [D^{i+1}f \cdot D^{p-i}g] + [D^{i+2}f \cdot D^{p-1-i}g] \big) \\
  &= \underbrace{\sum_{i=0}^p (-1)^i \big( [D^if \cdot D^{p+1-i}g] + [D^{i+1}f \cdot D^{p-i}g]  \big)}_{(*)} -(-1)^p [D^pf \cdot Dg] + (-1)^{p+1} [D^{p+1}f \cdot g] \\
  &+ \sum_{i=0}^{p-1} (-1)^i \big( [D^{i+1}f \cdot D^{p-i}g] + [D^{i+2}f \cdot D^{p-1-i}g] \big).
 \end{align*}
$
In addition to some further clean-up we substitute (*) by the lhs of (4) in order to see, whether we get a valid equation
$
 \begin{align*}
  &[f \cdot D^{p+1}g] + [Df \cdot D^pg] \\
  &=! \quad [f \cdot D^{p+1}g] - (-1)^{p+1} [D^{p+1}f \cdot g] + \sum_{i=0}^{p-1} (-1)^i \big( [D^{i+1}f \cdot D^{p-i}g] + [D^{i+2}f \cdot D^{p-1-i}g] \big).
 \end{align*}
$
Further rearrangements deliver
$
 \begin{align*}
  [Df \cdot D^pg] - (-1)^p [D^{p+1}f \cdot g] \quad =! \quad \sum_{i=0}^{p-1} (-1)^i D[D^{i+1}f \cdot D^{p-1-i}g].
 \end{align*}
$
Now we substitute $ Df \rightarrow f $ and get again (3)
$
 \begin{align*}
  [(Df) \cdot D^pg] - (-1)^p [D^p(Df) \cdot g] = \sum_{i=0}^{p-1} (-1)^i D[D^i(Df) \cdot D^{p-1-i}g].
 \end{align*}
$
The only thing I cannot confirm ist that one verifies all this immediately.
Concerning the proof of Taylor's formula itself, this is explained in @blargoner's excellent notes. Thanks a lot!
