LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Continuity at time zero implies continuity of every orbit

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 $X$ be a Banach space and $(T (t))_{t \geq 0} \subseteq B (X)$ satisfy $T (0) = I$ , $T (t + s) = T (t) T (s)$ for $s, t \geq 0$ and $\lim_{t ↓ 0} T (t) x = x$ for every $x \in X$ . Then $(T (t))$ is a strongly continuous semigroup (Strongly continuous semigroup): every orbit map $t \mapsto T (t) x$ is continuous on $[0, \infty)$ .

Facts & Assumptions

Given: Dependent Choice; A Banach space $X$ and a family $(T (t))_{t \geq 0} \subseteq B (X)$ with $T (0) = I$ , $T (t + s) = T (t) T (s)$ for $s, t \geq 0$ and $\lim_{t ↓ 0} T (t) x = x$ for every $x \in X$ .

[F1]

Local boundedness: for every $t_{0} \geq 0$ there is $M < \infty$ with $∥ T (t) ∥ \leq M$ for all $t \in [0, t_{0}]$ ; this uses DC through the uniform boundedness principle (A semigroup with continuity at zero is uniformly bounded on every compact time interval).

[F2]

For $S \in B (X)$ the operator norm satisfies $∥ S y ∥ \leq ∥ S ∥ ∥ y ∥$ for all $y$ , and $∥ S T ∥ \leq ∥ S ∥ ∥ T ∥$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Composition satisfies |ST|\le|S|,|T|).

[F3]

The hypotheses are those of a strongly continuous semigroup with continuity required only at $0$ (Strongly continuous semigroup): $T (0) = I$ , the functional equation holds, and $T (h) x \to x$ as $h ↓ 0$ for every $x$ .

Proof

technique · direct, transporting continuity at $0$ to an arbitrary time with the functional equation and the local bound

1.1F1

Fix $t_{0} \geq 0$ and let $M$ be a bound for $∥ T (t) ∥$ on $[0, t_{0}]$ , which exists by [F1]; fix also $x \in X$ .

1.2F2F3

Right continuity at $t_{0}$ : for $h > 0$ , the functional equation gives $T (t_{0} + h) x - T (t_{0}) x = T (t_{0}) (T (h) x - x)$ , whose norm is at most $∥ T (t_{0}) ∥ ∥ T (h) x - x ∥ \to 0$ as $h ↓ 0$ by [F2] and [F3].

1.3F1F2F3

Left continuity at $t_{0}$ : for $0 < h \leq t_{0}$ one has $T (t_{0}) = T (t_{0} - h + h) = T (t_{0} - h) T (h)$ , hence $T (t_{0} - h) x - T (t_{0}) x = T (t_{0} - h) (x - T (h) x)$ and, since $t_{0} - h \in [0, t_{0}]$ , $∥ T (t_{0} - h) x - T (t_{0}) x ∥ \leq M ∥ x - T (h) x ∥ \to 0$ by [F1], [F2] and [F3].

2.1F3step 1.2step 1.3∎

The two one-sided limits at $t_{0}$ both equal $T (t_{0}) x$ , so the orbit $t \mapsto T (t) x$ is continuous at every $t_{0} \geq 0$ ; as $x$ was arbitrary, all orbits are continuous on $[0, \infty)$ , and the family is a strongly continuous semigroup as defined in [F3].

Depends on

Used by

Dependency tree · two levels

16 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)
Roland Schnaubelt, Evolution Equations, Karlsruhe Institute of Technology (2023/24 course, complete lecture notes) (standard reference, not scraped)