Bochner Integral: Derivative

Question

Given a Banach space $E$.

Consider a continuous derivative: $$F'\in\mathcal{C}(\mathbb{R},E):\quad\int_\mathbb{R}\|F'(s)\|\mathrm{d}s<\infty$$

Then its integral computes as: $$\int_a^bF'(s)\mathrm{d}s=F(b)-F(a)$$ How to prove this by modern tools?

Answer 1

The usual proof works, i.e. define

$$ G : [a,\infty) \to E, x\mapsto \int_a^x F'(s) \, ds. $$

Using (only) the definition of the derivative and the continuity of $F'$, it is easy to see that $G$ is differentiable with $G' = F' = H'$ for $H(x) := F(x) - F(a)$.

Since also $H(0) = G(0) = 0$, we conclude $H = G$ on $[a,\infty)$ (see below). But this implies your claim.

To see $H = G$, one possibility is to assume $H(x) \neq G(x)$ for some $x$. Since $E$ is a Banach space (hence locally convex), the bounded (real valued) linear functionals seperate poins, i.e. there is some $\varphi \in E'$ with $\varphi(H(x)) \neq \varphi(G(x))$.

But the chain rule yields $(\varphi \circ H) ' = (\varphi \circ G)'$, which contradicts the classical mean value theorem (for differentiable functions $f : I \to \Bbb{R}$).