TheoremStatement: 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.

An orbit is right differentiable at zero exactly on the generator domain

Statement

Assume Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). Let $(T (t))_{t \geq 0}$ be a strongly continuous semigroup on a Banach space $X$ with generator $(A, D (A))$ (Infinitesimal generator of a C0-semigroup). For every $t \geq 0$ and $x \in X$ , the right derivative of the orbit exists in $X$ exactly when $T (t) x \in D (A)$ , and then it equals $A T (t) x$ . In particular, at $t = 0$ this derivative exists if and only if $x \in D (A)$ and equals $A x$ . If $x \in D (A)$ , domain invariance gives $T (t) x \in D (A)$ and $A T (t) x = T (t) A x$ for every $t \geq 0$ (The generator commutes with the semigroup on its domain). A vector outside $D (A)$ may still yield a differentiable orbit at a positive time when $T (t)$ maps it into $D (A)$ .

Facts & Assumptions

Given: Dependent Choice; A strongly continuous semigroup $(T (t))_{t \geq 0}$ on a Banach space $X$ with generator $(A, D (A))$ (Strongly continuous semigroup, Infinitesimal generator of a C0-semigroup); times $t \geq 0$ and vectors $x \in X$ .

[F1]

Definition of the generator: $z \in D (A)$ exactly when the right difference quotient $\frac{T (h) z - z}{h}$ has a limit in $X$ as $h ↓ 0$ , and that limit is $A z$ (Infinitesimal generator of a C0-semigroup).

[F2]

For $t \geq 0$ and $h > 0$ the semigroup law gives $T (t + h) x = T (h) T (t) x$ , so the right difference quotient of the orbit at $t$ is exactly the generator quotient of the vector $T (t) x$ . More generally the orbit is defined for all nonnegative times and the family is strongly continuous (Strongly continuous semigroup).

[F3]

Domain invariance and commutation: for $x \in D (A)$ one has $T (t) x \in D (A)$ and $A T (t) x = T (t) A x$ for every $t \geq 0$ (The generator commutes with the semigroup on its domain).

Proof

technique · direct: apply the definition of the generator to the vector $T(t)x$

1.1F1

At $t = 0$ the right derivative of $s \mapsto T (s) x$ at $0$ is by definition the limit of $(T (h) x - x) / h$ , which exists exactly when $x \in D (A)$ by [F1], and then equals $A x$ .

1.2F1F2

For fixed $t \geq 0$ and $h > 0$ , [F2] gives $\frac{T (t + h) x - T (t) x}{h} = \frac{T (h) T (t) x - T (t) x}{h}$ ; this is precisely the generator difference quotient of the vector $z : = T (t) x$ . Hence by [F1] the right derivative of the orbit at $t$ exists exactly when $T (t) x \in D (A)$ , and then equals $A T (t) x$ .

2.1F3step 1.2

When $x \in D (A)$ , [F3] gives $T (t) x \in D (A)$ and $A T (t) x = T (t) A x$ for every $t \geq 0$ , so the criterion of [step 1.2] is automatically satisfied; conversely, for $x \notin D (A)$ the criterion shows that differentiability of the orbit at time $t > 0$ holds or fails according to whether $T (t) x \in D (A)$ , which need not fail for every positive time.

3.1step 1.1step 1.2∎

Combining [step 1.1] and [step 1.2]: for every $t \geq 0$ and $x \in X$ the right derivative exists exactly when $T (t) x \in D (A)$ and equals $A T (t) x$ , with the case $t = 0$ reducing to the criterion $x \in D (A)$ and value $A x$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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