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.

Exponential bound for a C0-semigroup

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$ (Strongly continuous semigroup). Then there exist $M \geq 1$ and $ω \in R$ with $∥ T (t) ∥ \leq M e^{ω t}$ for all $t \geq 0$ . For $X \neq {0}$ one may take $M : = \sup_{0 \leq s \leq 1} ∥ T (s) ∥$ and $ω : = \log M$ ; for $X = {0}$ take $M = 1$ , $ω = 0$ .

Facts & Assumptions

Given: Dependent Choice; A strongly continuous semigroup $(T (t))_{t \geq 0}$ on a Banach space $X$ (Strongly continuous semigroup).

[F1]

Local boundedness: $M_{0} : = \sup_{0 \leq s \leq 1} ∥ T (s) ∥ < \infty$ ; the proof of the lemma uses DC through the uniform boundedness principle (A semigroup with continuity at zero is uniformly bounded on every compact time interval).

[F2]

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

[F3]

The semigroup law $T (r + s) = T (r) T (s)$ for $r, s \geq 0$ and $T (0) = I$ (Strongly continuous semigroup).

[F4]

The real exponential satisfies $e^{u + v} = e^{u} e^{v}$ , $e^{u} > 0$ for all real $u$ , $\exp : R \to (0, \infty)$ is a bijection, and $e^{u} \geq 1$ for $u \geq 0$ (The real exponential function and the number $e$ by a power series, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , The exponential is a continuous bijection from $R$ onto $(0, \infty)$ ).

Proof

technique · direct, bounding the powers of $T(1)$ by the local bound and absorbing them into an exponential

1.1F1F3F4

If $X = {0}$ take $M : = 1$ and $ω : = 0$ : then $∥ T (t) ∥ = 0 \leq M e^{ω t}$ for every $t$ . Otherwise $X \neq {0}$ , so $∥ I ∥ = 1$ and [F1] gives $M : = \sup_{0 \leq s \leq 1} ∥ T (s) ∥ \geq ∥ T (0) ∥ = 1$ with $M < \infty$ ; set $ω : = \log M$ , which exists by [F4] because $M \geq 1$ .

2.1F2F3step 1.1

For $t \geq 0$ write $t = n + s$ with $n : = ⌊ t ⌋ \in N_{0}$ and $s \in [0, 1)$ . By the semigroup law, $T (t) = T (s) T (1)^{n}$ , hence $∥ T (t) ∥ \leq ∥ T (s) ∥ ∥ T (1) ∥^{n} \leq M^{n + 1}$ by [F2] and the choice of $M$ .

3.1F4step 2.1

Since $M \geq 1$ and $n \leq t$ , [F4] gives $M^{n + 1} = M e^{n \log M} \leq M e^{t \log M} = M e^{ω t}$ .

4.1step 1.1step 3.1∎

Combining [step 2.1] and [step 3.1], $∥ T (t) ∥ \leq M e^{ω t}$ for every $t \geq 0$ , with $M \geq 1$ and $ω \in R$ ; in the nonzero case the displayed $M = \sup_{0 \leq s \leq 1} ∥ T (s) ∥$ and $ω = \log M$ are the explicit choices, and in the zero-space case the bound holds trivially for $M = 1$ , $ω = 0$ .

Note. The constant $ω = \log M$ need not be optimal: any larger $ω$ also works, since $e^{ω t}$ is nondecreasing in $ω$ for $t \geq 0$ ; the growth bound $ω_{0} (T) = \inf {ω : \exists M, ∥ T (t) ∥ \leq M e^{ω t}}$ is not needed here.

Depends on

Used by

Dependency tree · two levels

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