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

Bounded Yosida semigroups converge to the generated 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 $A : D (A) \subseteq X \to X$ be closed and densely defined on a Banach space $X$ and let $M \geq 1$ , $ω \in R$ satisfy $(ω, \infty) \subseteq ρ (A)$ and $∥ R (λ, A)^{n} ∥ \leq M (λ - ω)^{- n}$ for all real $λ > ω$ , $n \geq 1$ . Let $A_{λ} = λ A R (λ, A)$ be the Yosida approximants (Yosida approximants) and let $E_{λ} (t) : = e^{t A_{λ}}$ be the bounded-operator exponentials of The exponential series of a bounded operator. Then for every $x \in X$ the limit $T (t) x : = \lim_{λ \to \infty} E_{λ} (t) x$ exists, uniformly for $t$ in compact subsets of $[0, \infty)$ , and $T$ is a strongly continuous semigroup on $X$ with $∥ T (t) ∥ \leq M e^{ω t}$ and generator $A$ .

Facts & Assumptions

Given: Dependent Choice; A closed densely defined operator $A$ on a Banach space $X$ with $(ω, \infty) \subseteq ρ (A)$ and $∥ R (λ, A)^{n} ∥ \leq M (λ - ω)^{- n}$ for all real $λ > ω$ and $n \geq 1$ ; the Yosida approximants $A_{λ} = λ A R (λ, A)$ and the exponentials $E_{λ} (t) = e^{t A_{λ}}$ of The exponential series of a bounded operator (Yosida approximants, Resolvent and spectrum of a closed operator on a Banach space).

[F1]

Exponential series: $E_{λ} (t) = \sum_{j \geq 0} \frac{t^{j}}{j!} A_{λ}^{j}$ converges in operator norm, $∥ E_{λ} (t) ∥ \leq e^{∣ t ∣ ∥ A_{λ} ∥}$ , $E_{λ} (0) = I$ , $E_{λ} (t + s) = E_{λ} (t) E_{λ} (s)$ , $E_{λ}$ is $C^{1}$ with $E_{λ}^{'} (t) = A_{λ} E_{λ} (t)$ , so $E_{λ} (t) x - x = \int_{0}^{t} E_{λ} (s) A_{λ} x d s$ for every $x$ by the fundamental theorem of calculus (The exponential series of a bounded operator, Fundamental theorem of calculus for Banach-valued continuous curves).

[F2]

The approximants satisfy the norm bound of Yosida approximants are bounded and converge on the domain and $A_{λ} x \to A x$ for every $x \in D (A)$ ; distinct approximants commute and so do the exponentials (Yosida approximants, Composition satisfies |ST|\le|S|,|T|).

[F3]

$A$ is closed and $D (A)$ is dense by hypothesis; since $A_{λ} = λ^{2} R (λ, A) - λ I$ and $R (λ, A)$ commutes with $I$ , the binomial Cauchy-product argument in the exponential-series proof, applied to the commuting bounded operators $- λ I$ and $λ^{2} R (λ, A)$ , gives $E_{λ} (t) = e^{- λ t} e^{t λ^{2} R (λ, A)}$ , so the resolvent power estimates yield $∥ E_{λ} (t) ∥ \leq e^{- λ t} \sum_{j \geq 0} \frac{(t λ^{2})^{j}}{j!} \frac{M}{(λ - ω)^{j}} = M e^{ω t λ / (λ - ω)}$ for $t \geq 0$ . [F1, F2]

[F4]

Average convergence and strong continuity: a continuous curve is Bochner integrable and its forward averages converge to its value (Average convergence for a continuous Banach-valued function); continuity at $0$ plus the semigroup law gives continuity of every orbit (Continuity at time zero implies continuity of every orbit, Strongly continuous semigroup).

[F5]

Laplace formula: a strongly continuous semigroup with $∥ T (t) ∥ \leq M e^{ω t}$ has $(ω, \infty) \subseteq ρ (its generator)$ (Laplace transform formula for the resolvent).

Proof

technique · direct: uniform bounds and a Cauchy estimate on the dense domain, then passage to the limit, and identification of the generator by uniqueness of the resolvent

1.1F3

Uniform bound. For $λ > \max {ω, 0}$ and $t \geq 0$ , [F3] gives $∥ E_{λ} (t) ∥ \leq M e^{ω t λ / (λ - ω)}$ . For every $T_{0} < \infty$ , $ω t λ / (λ - ω) \to ω t$ uniformly on $0 \leq t \leq T_{0}$ . Thus the displayed majorants converge uniformly to $M e^{ω t}$ there; they are uniformly bounded for large $λ$ , and ${lim sup}_{λ \to \infty} ∥ E_{λ} (t) ∥ \leq M e^{ω t}$ for each fixed $t$ , regardless of the sign of $ω$ .

2.1F1F2step 1.1

Cauchy estimate on $D (A)$ . For $x \in D (A)$ and $λ, μ > ω$ , the exponentials commute and the FTC gives $E_{λ} (t) x - E_{μ} (t) x = - \int_{0}^{t} \frac{d}{d s} [E_{λ} (t - s) E_{μ} (s) x] d s = \int_{0}^{t} E_{λ} (t - s) E_{μ} (s) (A_{λ} x - A_{μ} x) d s$ ; hence $∥ E_{λ} (t) x - E_{μ} (t) x ∥ \leq t C (t)^{2} ∥ A_{λ} x - A_{μ} x ∥$ with $C (t) : = \sup_{λ large, 0 \leq s \leq t} ∥ E_{λ} (s) ∥$ finite by [step 1.1]. Since $A_{λ} x \to A x$ by [F2], the family $(E_{λ} (t) x)_{λ}$ is Cauchy, uniformly for $t$ in compact intervals.

3.1F2F3step 1.1step 2.1

The limit and its bound. For $x \in X$ and $y \in D (A)$ close to $x$ , $∥ E_{λ} (t) x - E_{μ} (t) x ∥ \leq ∥ E_{λ} (t) (x - y) ∥ + ∥ E_{μ} (t) (x - y) ∥ + ∥ E_{λ} (t) y - E_{μ} (t) y ∥$ , and the first two terms are small uniformly in $λ, μ$ and $t$ in compacts by [step 1.1] while the last is small by [step 2.1]; density [F3] gives convergence uniformly on compact $t$ -intervals for every $x$ . The limit orbit is continuous on each compact interval: for any point, bound its increment by the two uniform approximation errors and the increment of one continuous approximating orbit. Define $T (t) x : = \lim_{λ} E_{λ} (t) x$ ; then $T (t)$ is linear and bounded with $∥ T (t) x ∥ = \lim_{λ} ∥ E_{λ} (t) x ∥ \leq M e^{ω t} ∥ x ∥$ by [step 1.1].

4.1F1step 3.1

Semigroup law. For $t, s \geq 0$ and $x \in X$ , $E_{λ} (t + s) x = E_{λ} (t) E_{λ} (s) x \to T (t) T (s) x$ by [step 3.1] and the uniform bound on compacts, while $E_{λ} (t + s) x \to T (t + s) x$ ; hence $T (t + s) = T (t) T (s)$ , and $T (0) = I$ .

4.2F1F4step 3.1

Strong continuity. For $x \in D (A)$ and $t$ in a compact interval, $E_{λ} (t) x - x = \int_{0}^{t} E_{λ} (s) A_{λ} x d s = \int_{0}^{t} E_{λ} (s) A x d s + \int_{0}^{t} E_{λ} (s) (A_{λ} x - A x) d s$ , and the two integrals tend to $\int_{0}^{t} T (s) A x d s$ and $0$ uniformly, because $E_{λ} (s) \to T (s)$ strongly uniformly on the interval by [step 3.1] and $A_{λ} x \to A x$ ; hence $T (t) x - x = \int_{0}^{t} T (s) A x d s \to 0$ as $t ↓ 0$ by average convergence [F4]. With the local bound of [step 3.1] this extends from the dense domain to all $x$ , so $T (t) x \to x$ as $t ↓ 0$ ; by the semigroup law and [F4] every orbit is continuous, so $T$ is a strongly continuous semigroup with bound $∥ T (t) ∥ \leq M e^{ω t}$ .

5.1F4step 4.2

The generator contains $A$ . The identity of [step 4.2] shows $T (t) x - x = \int_{0}^{t} T (s) A x d s$ for $x \in D (A)$ ; dividing by $t$ and using average convergence for the continuous curve $s \mapsto T (s) A x$ gives $\frac{T (t) x - x}{t} \to A x$ . Hence $D (A) \subseteq D (B)$ and $B x = A x$ for $x \in D (A)$ , where $B$ is the generator of $T$ .

6.1F2F5step 5.1∎

$A = B$ . By [F5] applied to $T$ and its bound, every real $λ > ω$ lies in $ρ (B)$ ; it also lies in $ρ (A)$ by hypothesis, and $λ I - A = λ I - B$ on $D (A)$ . Thus $λ I - A : D (A) \to X$ and $λ I - B : D (B) \to X$ are both bijections agreeing on $D (A)$ : given $x \in D (B)$ , $(λ I - B) x = (λ I - A) y$ for some $y \in D (A)$ , and since $(λ I - B) y = (λ I - A) y = (λ I - B) x$ while $λ I - B$ is injective, $x = y \in D (A)$ ; hence $D (A) = D (B)$ and $A = B$ .

Depends on

Used by

Hille-Yosida generation theorem Theorem

Dependency tree · two levels

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