LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Taylor expansion with integral remainder for Banach-valued curves

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the cited integral and semigroup suppliers.

Let $Y$ be a Banach space over $K \in {R, C}$ , let $I \subseteq R$ be an interval, let $n \geq 0$ be an integer, and let $u : I \to Y$ . For a nondegenerate interval, $u \in C^{n + 1} (I; Y)$ means that $u$ is continuous on $I$ , its restriction to $int I$ has norm-continuous derivatives through order $n + 1$ , and each derivative extends continuously to $I$ . Derivatives on the interior are taken with respect to the real parameter, using the underlying real Banach space when $Y$ is complex (Fréchet derivative between Banach spaces), and $u^{(k)}$ denotes the continuous extension at any included endpoint; set $u^{(0)} = u$ . Assume this regularity. Then for all $t \in I$ and $h \in R$ with $[\min {t, t + h}, \max {t, t + h}] \subseteq I$ , $u (t + h) = \sum_{k = 0}^{n} u^{(k)} (t) \frac{h^{k}}{k!} + \frac{1}{n!} \int_{t}^{t + h} (t + h - s)^{n} u^{(n + 1)} (s) d s,$ the integral being a Bochner integral (Bochner-integrable function); for $h < 0$ the symbol $\int_{t}^{t + h}$ denotes the oriented Bochner interval integral $- \int_{t + h}^{t}$ . For $n = 0$ the formula is the fundamental theorem of calculus. For $h = 0$ the formula is understood as $u (t) = u (t)$ ; this also covers singleton intervals without assigning higher derivatives there. No choice principle beyond Countable Choice is used.

Facts & Assumptions

Given: Countable Choice; a Banach space $Y$ over $K$ , an interval $I \subseteq R$ , an integer $n \geq 0$ , a curve $u : I \to Y$ continuous on $I$ whose real-parameter derivatives through order $n + 1$ on $int I$ extend continuously to $I$ when $I$ is nondegenerate, and points $t \in I$ , $h \in R$ with $[\min {t, t + h}, \max {t, t + h}] \subseteq I$ . Write $u^{(k)}$ for these extensions and $u^{(0)} = u$ ; for $h < 0$ use $\int_{t}^{t + h} f : = - \int_{t + h}^{t} f$ , and for $h = 0$ read the formula as $u (t) = u (t)$ , including singleton $I$ .

[L1]

A continuous $f : [a, b] \to Y$ is Bochner integrable; its primitive $G (t) = \int_{a}^{t} f$ is differentiable with $G^{'} = f$ , and for a continuous curve $φ$ of class $C^{1}$ on $(a, b)$ whose derivative extends continuously to $[a, b]$ one has $\int_{a}^{b} φ^{'} = φ (b) - φ (a)$ (Fundamental theorem of calculus for Banach-valued continuous curves).

[L2]

The Bochner integral is linear in its integrand, so $\int (α f + β g) = α \int f + β \int g$ on a fixed interval, and $∥ \int_{E} f ∥ \leq \int_{E} ∥ f ∥$ (Linearity of the Bochner integral, Bochner integral norm inequality). Scalar and vector operations are continuous: $∥ λ v - λ_{0} v_{0} ∥ \leq ∣ λ - λ_{0} ∣ ∥ v ∥ + ∣ λ_{0} ∣ ∥ v - v_{0} ∥$ .

Proof

technique · direct

1.1L1givenalgebra

If $h = 0$ , the formula is $u (t) = u (t)$ for every $n$ , including singleton $I$ . Henceforth let $h \neq 0$ , so $I$ is nondegenerate; its interior is dense in $I$ , making each continuous derivative extension unique. Base case $n = 0$ : for $h > 0$ , the continuous curve $u$ is differentiable inside $[t, t + h]$ with derivative extending continuously there as $u^{'}$ , so [L1] gives $\int_{t}^{t + h} u^{'} (s) d s = u (t + h) - u (t)$ ; for $h < 0$ , [L1] on $[t + h, t]$ and the oriented convention give $\int_{t}^{t + h} u^{'} = - \int_{t + h}^{t} u^{'} = - (u (t) - u (t + h)) = u (t + h) - u (t)$ .

1.2L1L2givenalgebra

Integration by parts identity. For $1 \leq k \leq n$ put $φ (s) : = \frac{(t + h - s)^{k}}{k!} u^{(k)} (s)$ ; on the interior of the ordered segment the scalar-times-vector product rule gives $φ^{'} (s) = - \frac{(t + h - s)^{k - 1}}{(k - 1)!} u^{(k)} (s) + \frac{(t + h - s)^{k}}{k!} u^{(k + 1)} (s)$ , because $φ (s + Δ) - φ (s) = (α (s + Δ) - α (s)) v (s + Δ) + α (s) (v (s + Δ) - v (s))$ for the scalar $α (s) = (t + h - s)^{k} / k!$ and the vector $v = u^{(k)}$ , and scalar multiplication is continuous by [L2]. For $h > 0$ , $φ$ is continuous on $[t, t + h]$ with $φ^{'}$ extending continuously there (the derivatives of $u$ up to order $k + 1$ have continuous extensions), so [L1] gives $\int_{t}^{t + h} φ^{'} = φ (t + h) - φ (t) = - \frac{h^{k}}{k!} u^{(k)} (t)$ ; rearranging with the linearity [L2] yields $\frac{1}{(k - 1)!} \int_{t}^{t + h} (t + h - s)^{k - 1} u^{(k)} (s) d s = \frac{h^{k}}{k!} u^{(k)} (t) + \frac{1}{k!} \int_{t}^{t + h} (t + h - s)^{k} u^{(k + 1)} (s) d s$ . For $h < 0$ the same computation is applied on the interval $[t + h, t]$ with the oriented sign, and the displayed identity is unchanged because both integrals acquire one sign reversal.

2.1step 1.2L1givenalgebra

Induction step. Assume the formula holds with $n - 1 \geq 0$ in place of $n$ for every curve of class $C^{n}$ ; applying it to the $C^{n + 1}$ curve $u$ gives $u (t + h) = \sum_{k = 0}^{n - 1} u^{(k)} (t) \frac{h^{k}}{k!} + \frac{1}{(n - 1)!} \int_{t}^{t + h} (t + h - s)^{n - 1} u^{(n)} (s) d s$ , and [step 1.2] with $k = n$ rewrites the last term as $\frac{h^{n}}{n!} u^{(n)} (t) + \frac{1}{n!} \int_{t}^{t + h} (t + h - s)^{n} u^{(n + 1)} (s) d s$ ; substituting gives the formula with $n$ , all integrands being continuous hence Bochner integrable on the compact interval by [L1].

3.1step 1.1step 2.1given∎

Conclusion. [step 1.1] is the case $n = 0$ for both signs of $h$ and [step 2.1] carries the induction from $n - 1$ to $n$ for every $n \geq 1$ , so the formula holds for all $n \geq 0$ ; the proof used only the one-dimensional fundamental theorem, the product rule for a scalar and a vector curve, and linearity of the Bochner integral, hence no choice principle beyond Countable Choice was used.

Depends on

Used by

Sectorial resolvent characterisation of bounded analytic semigroups Theorem

Dependency tree · two levels

28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Klaus-Jochen Engel and Rainer Nagel, One-Parameter Semigroups for Linear Evolution Equations, Graduate Texts in Mathematics 194 (complete author-hosted monograph) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)