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.

Compatibility at time zero for a classical parabolic solution

Statement

Assume Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain) for the cited integral and semigroup suppliers.

Let $A$ be the generator of a strongly continuous semigroup on a Banach space $X$ (Infinitesimal generator of a C0-semigroup, Banach space), let $b > 0$ , $x \in X$ , and let $f : [0, b] \to X$ be continuous with $f (0)$ defined. Suppose $u \in C ([0, b], X) \cap C^{1} ((0, b], X)$ satisfies $u (0) = x$ , $u (t) \in D (A)$ and $u^{'} (t) = A u (t) + f (t)$ for every $t \in (0, b]$ , and suppose $\lim_{t ↓ 0} u^{'} (t)$ exists in $X$ (in particular if $u \in C^{1} ([0, b], X)$ ). Then $x \in D (A)$ and $\lim_{t ↓ 0} u^{'} (t) = A x + f (0);$ consequently $u$ extends to a classical solution on $[0, b]$ in the sense of Classical, strong and mild abstract Cauchy solutions exactly when this limit exists, and in the PDE realisation $x \in D (A)$ is precisely the boundary-and-domain compatibility of the initial datum. One-order propagation under stronger regularity. If, in addition, $f \in C^{1} ([0, b], X)$ , $u \in C^{1} ((0, b], D (A))$ in the graph norm (Unbounded linear operators: domain, graph and extension), and $A x + f (0) \in D (A)$ with $u^{'} (t) \to A x + f (0)$ in the graph norm as $t ↓ 0$ , then $u^{'}$ is right-differentiable at $0$ with $(u^{'})^{'} (0) = A (A x + f (0)) + f^{'} (0)$ . No choice principle beyond Dependent Choice is used.

Facts & Assumptions

Given: A strongly continuous semigroup with generator $A$ on the Banach space $X$ , the closed operator $A$ with domain $D (A)$ , a continuous $f : [0, b] \to X$ with $f (0)$ defined, and $u \in C ([0, b], X) \cap C^{1} ((0, b], X)$ with $u (0) = x$ , $u (t) \in D (A)$ , $u^{'} (t) = A u (t) + f (t)$ on $(0, b]$ and $y : = \lim_{t ↓ 0} u^{'} (t)$ existing in $X$ . For the one-order propagation clause, also assume $f \in C^{1} ([0, b], X)$ , $u \in C^{1} ((0, b], D (A))$ in graph norm, $A x + f (0) \in D (A)$ , and $u^{'} (t) \to A x + f (0)$ in graph norm.

[L1]

$A$ is closed and densely defined: its graph ${(v, A v) : v \in D (A)}$ is closed in $X \times X$ (The generator is closed and densely defined).

[L2]

A classical solution on $[0, b]$ is a function in $C^{1} ([0, b], X)$ with values in $D (A)$ , $A u \in C ([0, b], X)$ , satisfying the equation on $(0, b)$ and the initial condition; continuous forcing on $[0, b]$ extends the equation to the endpoints (Classical, strong and mild abstract Cauchy solutions).

[L3]

Unbounded linear operators: domain, graph and extension: the graph norm on $D (A)$ is $∥ v ∥_{A} = (∥ v ∥^{2} + ∥ A v ∥^{2})^{1 / 2}$ , so $A : D (A)_{g r a p h} \to X$ is bounded.

[L4]

Fundamental theorem of calculus for Banach-valued continuous curves: if a continuous Banach-valued curve is differentiable on $(0, b)$ and its derivative extends continuously to $[0, b]$ , then its increment equals the integral of that derivative.

Proof

technique · direct

1.1givenalgebra

Limit of $A u (t)$ . For $t \in (0, b]$ the equation gives $A u (t) = u^{'} (t) - f (t)$ , and $u^{'} (t) \to y$ by the hypothesis while $f (t) \to f (0)$ by continuity; hence $A u (t) \to y - f (0)$ in $X$ .

1.2given

Limit of $u (t)$ . By continuity of $u$ at $0$ and $u (0) = x$ one has $u (t) \to x$ as $t ↓ 0$ (Fréchet derivative between Banach spaces), and $u (t) \in D (A)$ for every $t \in (0, b]$ .

2.1step 1.1step 1.2L1given

Closedness forces the endpoint compatibility. The pairs $(u (t), A u (t))$ lie in the graph of $A$ for $t \in (0, b]$ and converge to $(x, y - f (0))$ by [step 1.1] and [step 1.2]; since the graph is closed by [L1], the limit lies in the graph: $x \in D (A)$ and $A x = y - f (0)$ , that is $\lim_{t ↓ 0} u^{'} (t) = A x + f (0)$ .

3.1step 2.1L2L4given

Equivalence with the classical solution. If the limit exists, [step 2.1] shows $x \in D (A)$ and, using $A u (t) = u^{'} (t) - f (t) \to A x$ , the derivative $u^{'}$ extends continuously to $[0, b]$ with value $A x + f (0) = A u (0) + f (0)$ . By [L4] applied to $u$ on $[0, t]$ , $u (t) - u (0) = \int_{0}^{t} u^{'} (s) d s$ , so the right derivative at $0$ is this limiting value. Hence $u \in C^{1} ([0, b], X)$ solves the equation at every point of $[0, b]$ and is a classical solution by [L2]; conversely a classical solution has $u \in C^{1} ([0, b], X)$ , so its one-sided derivative at $0$ exists and the limit does.

3.2step 2.1L3L4givenalgebra

(One-order propagation under stronger regularity) Assume the additional hypotheses in the final Statement clause and put $w (0) : = A x + f (0)$ , $w (t) : = u^{'} (t)$ for $t > 0$ . By [L3], $A$ is bounded from the graph-norm domain into $X$ ; since $u$ is $C^{1}$ there in graph norm and $f \in C^{1}$ , differentiating $u^{'} = A u + f$ on $(0, b]$ gives $w^{'} (t) = A w (t) + f^{'} (t)$ . The graph-norm convergence of $w$ and continuity of $f^{'}$ imply $w^{'} (t) \to A (A x + f (0)) + f^{'} (0)$ . By [L4] on $[0, t]$ , $w (t) - w (0) = \int_{0}^{t} w^{'} (s) d s$ ; dividing by $t$ and using continuity of the integrand at $0$ gives the stated right derivative of $u^{'}$ at $0$ .

4.1step 2.1step 3.1step 3.2given∎

Assembly. [step 2.1] proves $x \in D (A)$ and the value of the limit; [step 3.1] gives the stated equivalence with the classical solution; [step 3.2] proves the one-order propagation. The argument used only continuity, closedness of the graph and the equation, so no choice principle beyond Dependent Choice was used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 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)