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.

A semigroup with continuity at zero is uniformly bounded on every compact time interval

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 let $(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$ (in particular every strongly continuous semigroup satisfies these hypotheses, Strongly continuous semigroup). Then for every $t_{0} \geq 0$ , $\sup_{0 \leq t \leq t_{0}} ∥ T (t) ∥ < \infty$ .

Facts & Assumptions

Given: 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 all $s, t \geq 0$ , and $\lim_{t ↓ 0} T (t) x = x$ for every $x \in X$ . These are the hypotheses of Strongly continuous semigroup with continuity at every time weakened to continuity at $0$ ; the item assumes Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain), carried by the cited uniform boundedness principle, and step 1.1 selects a sequence, which uses Countable Choice, a consequence of DC.

[F1]

The operator norm satisfies $∥ S T ∥ \leq ∥ S ∥ ∥ T ∥$ for all $S, T \in B (X)$ (Composition satisfies |ST|\le|S|,|T|), and $∥ \cdot ∥$ is the operator norm on $B (X)$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, A bounded linear operator between normed spaces).

[F2]

Under DC, a pointwise bounded family of bounded linear operators between a Banach space and a normed space is norm bounded (Uniform boundedness principle).

[F3]

For every $x \in X$ one has $T (t) x \to x$ as $t ↓ 0$ ; this is hypothesis (iii) of Strongly continuous semigroup at the point $0$ , where $T (0) x = x$ .

Proof

technique · direct, combining the uniform boundedness principle with the semigroup law: first a finite bound on a small interval $[0,\delta]$, then iteration over $\lfloor t_0/\delta\rfloor$ steps

1.1F2F3given

There are $δ > 0$ and $M_{0} < \infty$ with $\sup_{0 \leq t \leq δ} ∥ T (t) ∥ \leq M_{0}$ . Otherwise $\sup_{0 < t \leq 1 / n} ∥ T (t) ∥ = \infty$ for every $n$ , so for each $n$ one may select $t_{n} \in (0, 1 / n]$ with $∥ T (t_{n}) ∥ \geq n$ ; this selection is the only use of Countable Choice, available because DC implies ${A C}_{ω}$ .

2.1F3step 1.1

For every $x \in X$ the sequence $T (t_{n}) x$ converges to $x$ , because $t_{n} \leq 1 / n \to 0$ and $\lim_{t ↓ 0} T (t) x = x$ ; hence the family ${T (t_{n}) : n \geq 1}$ is pointwise bounded on the Banach space $X$ .

3.1F2step 1.1step 2.1

By the uniform boundedness principle [F2] the family ${T (t_{n})}$ is norm bounded, that is $\sup_{n} ∥ T (t_{n}) ∥ < \infty$ , contradicting $∥ T (t_{n}) ∥ \geq n \to \infty$ ; hence the assumed unboundedness of every right neighbourhood of $0$ is impossible, proving [step 1.1].

4.1F1step 3.1algebra

Put $M : = \max {1, M_{0}} \geq 1$ . For $t_{0} \geq 0$ and $t \in [0, t_{0}]$ write $t = n δ + s$ with $n : = ⌊ t / δ ⌋ \in N_{0}$ and $s \in [0, δ)$ . The functional equation gives $T (t) = T (δ)^{n} T (s)$ , by induction on $n$ from $T (u + δ) = T (u) T (δ)$ .

5.1F1step 3.1step 4.1algebra

Therefore $∥ T (t) ∥ \leq ∥ T (δ) ∥^{n} ∥ T (s) ∥ \leq M^{n + 1}$ by [F1] and [step 1.1], where $n = ⌊ t / δ ⌋ \leq ⌊ t_{0} / δ ⌋$ ; hence $\sup_{0 \leq t \leq t_{0}} ∥ T (t) ∥ \leq M^{⌊ t_{0} / δ ⌋ + 1} < \infty$ .

6.1step 5.1∎

Since $t_{0} \geq 0$ was arbitrary, $\sup_{0 \leq t \leq t_{0}} ∥ T (t) ∥ < \infty$ for every $t_{0}$ , as required.

Depends on

Used by

Dependency tree · two levels

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