ExampleConstruction: Literature-sourcedVerification: 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.

The exponential of a bounded operator is a uniformly continuous semigroup

Example

Let $X$ be a Banach space and let $A \in B (X)$ . The exponential series of The exponential series of a bounded operator defines $E (t) = e^{t A}$ for all real $t$ , and $T (t) : = E (t) ∣_{t \geq 0}$ is a strongly continuous semigroup on $X$ with: (i) $∥ T (t) ∥ \leq e^{t ∥ A ∥}$ and $T (0) = I$ ; (ii) $t \mapsto T (t)$ is continuous for the operator norm, so $T$ is uniformly continuous; (iii) the generator of $T$ is $A$ , with domain $D (A) = X$ ; (iv) $E (t + s) = E (t) E (s)$ for all $s, t \in R$ , so $E$ is a group; and $t \mapsto T (t) x$ solves $u^{'} = A u$ , $u (0) = x$ for every $x \in X$ , in fact classically with $u \in C^{1} (R; X)$ and $u^{'} = A u$ everywhere.

Verification

Given: A Banach space $X$ , an operator $A \in B (X)$ , the exponential series $E (t) = \sum_{n \geq 0} \frac{t^{n}}{n!} A^{n}$ of The exponential series of a bounded operator, and $T (t) : = E (t)$ for $t \geq 0$ .

[F1] For every real $t$ the series $E (t)$ converges absolutely in operator norm, $∥ E (t) ∥ \leq e^{∣ t ∣ ∥ A ∥}$ , $E (0) = I$ , $E (t + s) = E (t) E (s)$ for all real $s, t$ , $E$ is $C^{\infty}$ with $E^{'} (t) = A E (t) = E (t) A$ , and $∥ \frac{E (t) - I}{t} - A ∥ \leq \frac{∣ t ∣}{2} ∥ A ∥^{2} e^{∣ t ∣ ∥ A ∥} \to 0$ (The exponential series of a bounded operator).

[F2] The generator of a strongly continuous semigroup is defined by $D (A) = {x : \lim_{h ↓ 0} \frac{T (h) x - x}{h} exists}$ and $A x$ equal to that limit (Infinitesimal generator of a C0-semigroup, Strongly continuous semigroup).

Proof technique: direct verification of the semigroup axioms and of the generator difference quotients from the exponential-series lemma.

1.1F1

$T (0) = E (0) = I$ and $T (t + s) = E (t + s) = E (t) E (s) = T (t) T (s)$ for $s, t \geq 0$ ; moreover $∥ T (t) ∥ = ∥ E (t) ∥ \leq e^{t ∥ A ∥}$ since $t \geq 0$ , which is claim (i) and the group law restricted to $[0, \infty)$ .

1.2F1F2

$t \mapsto T (t)$ is norm continuous on $[0, \infty)$ , indeed $C^{\infty}$ there with derivative $A E (t)$ ; since $∥ (T (t) - T (t_{0})) x ∥ \leq ∥ T (t) - T (t_{0}) ∥ ∥ x ∥$ , the family is strongly continuous, so it is a $C_{0}$ -semigroup, and it is uniformly continuous as a norm-continuous family: claims (ii) and (iv) for real times follow from the same identities.

1.3F1F2

Generator: for $x \in X$ and $h > 0$ , $∥ \frac{T (h) x - x}{h} - A x ∥ \leq ∥ \frac{E (h) - I}{h} - A ∥ ∥ x ∥ \leq \frac{h}{2} ∥ A ∥^{2} e^{h ∥ A ∥} ∥ x ∥ \to 0$ , so every $x \in X$ lies in the generator domain $D (A)$ of the semigroup and the generator acts by $x \mapsto A x$ ; hence the generator is the bounded operator $A$ with $D (A) = X$ , which is claim (iii).

2.1F1step 1.2

Classical orbits: for $u (t) : = E (t) x$ one has $u^{'} (t) = E^{'} (t) x = A E (t) x = A u (t)$ for every real $t$ , and $u (0) = x$ , so $u \in C^{1} (R; X)$ solves $u^{'} = A u$ classically; $u$ is unique among such solutions by the same argument applied to the difference of two solutions, alternatively by the group law $E (- t) u (t) = x$ .

3.1step 1.1step 1.2step 1.3step 2.1∎

All of (i)-(iv) and the classical-solution statement are established, with $ω = ∥ A ∥$ and $M = 1$ in the exponential bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)
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)