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

Contraction Hille-Yosida theorem

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$ . Then $A$ generates a strongly continuous semigroup of contractions ( $∥ T (t) ∥ \leq 1$ for all $t \geq 0$ ) if and only if $(0, \infty) \subseteq ρ (A)$ and $∥ λ R (λ, A) ∥ \leq 1$ for all $λ > 0$ , equivalently $∥ R (λ, A) ∥ \leq 1 / λ$ for all $λ > 0$ . In this case the first-power estimate implies all the power estimates $∥ R (λ, A)^{n} ∥ \leq λ^{- n}$ by submultiplicativity, so no separate power condition is needed; when $X$ is complex, every $z$ with $Re z > 0$ belongs to $ρ (A)$ and $∥ R (z, A)^{n} ∥ \leq (Re z)^{- n}$ for every $n \geq 1$ .

Facts & Assumptions

Given: Dependent Choice; A closed densely defined operator $A$ on a Banach space $X$ (Hille-Yosida generation theorem).

[F1]

Hille-Yosida with $M = 1$ , $ω = 0$ : $A$ generates a strongly continuous semigroup with $∥ T (t) ∥ \leq 1$ for all $t \geq 0$ if and only if $(0, \infty) \subseteq ρ (A)$ and $∥ R (λ, A)^{n} ∥ \leq λ^{- n}$ for every real $λ > 0$ and every $n \geq 1$ (Hille-Yosida generation theorem).

[F2]

The operator norm is submultiplicative, $∥ S T ∥ \leq ∥ S ∥ ∥ T ∥$ (Composition satisfies |ST|\le|S|,|T|), and is a norm on $B (X)$ (The operator norm is a norm on the space of bounded linear operators).

[F3]

The complex exponential satisfies $∣ e^{- z t} ∣ = e^{- t Re z}$ and $\frac{d}{d t} e^{- z t} = - z e^{- z t}$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , The complex exponential is entire and its complex derivative is itself). The Laplace inverse argument and resolvent differentiation for real parameters are proved in Laplace transform formula for the resolvent and Resolvent power estimates for semigroup generators; their complex extension is derived in step 2.1.

Proof

technique · direct: specialise the general theorem and observe that the first-power estimate implies all power estimates by submultiplicativity

1.1F1

Suppose $A$ generates a contraction semigroup, $∥ T (t) ∥ \leq 1$ . Then [F1] with $M = 1$ , $ω = 0$ gives $(0, \infty) \subseteq ρ (A)$ and $∥ R (λ, A)^{n} ∥ \leq λ^{- n}$ for all $n \geq 1$ ; in particular the first-power estimate $∥ λ R (λ, A) ∥ \leq 1$ , equivalently $∥ R (λ, A) ∥ \leq 1 / λ$ , holds for all $λ > 0$ .

1.2F1F2

Conversely, suppose $(0, \infty) \subseteq ρ (A)$ and $∥ λ R (λ, A) ∥ \leq 1$ , i.e. $∥ R (λ, A) ∥ \leq 1 / λ$ , for all $λ > 0$ . By submultiplicativity [F2], $∥ R (λ, A)^{n} ∥ \leq ∥ R (λ, A) ∥^{n} \leq λ^{- n}$ for every $n \geq 1$ ; hence the power conditions of [F1] hold with $M = 1$ , $ω = 0$ , and $A$ generates a strongly continuous semigroup of contractions.

2.1F1F3step 1.2

Let $X$ be complex, $a : = Re z > 0$ , and $J_{z} x : = \int_{0}^{\infty} e^{- z s} T (s) x d s$ . By [F3] its tail norm is at most $e^{- a R} ∥ x ∥ / a$ . For $x \in D (A)$ , integration of the derivative of $e^{- z s} T (s) x$ , with the closed-graph integration argument of the Laplace theorem, gives $(z I - A) J_{z} x = x = J_{z} (z I - A) x$ ; density and closedness extend the first identity to every $x \in X$ , exactly as in that theorem, so $z \in ρ (A)$ and $R (z, A) = J_{z}$ . For small real $h$ , the resolvent identity gives $d R (z + h, A) / d h ∣_{h = 0} = - R (z, A)^{2}$ in operator norm. Differentiating the integral along this real increment is justified by splitting off its tail and dominating by $s^{k} e^{- a s / 2} ∥ x ∥$ for each needed order; induction gives $R (z, A)^{n} x = (n - 1)!^{- 1} \int_{0}^{\infty} s^{n - 1} e^{- z s} T (s) x d s$ . The scalar integral of the norm majorant is $(n - 1)! / a^{n}$ , by the integration-by-parts recurrence of the power-estimate proof. Hence $∥ R (z, A)^{n} ∥ \leq a^{- n}$ , the precise complex half-plane estimate.

3.1step 1.1step 1.2step 2.1∎

Therefore contractivity of the generated semigroup is equivalent to $(0, \infty) \subseteq ρ (A)$ and $∥ λ R (λ, A) ∥ \leq 1$ for all $λ > 0$ , and in this case the single estimate forces all the resolvent power bounds.

Depends on

Used by

Lumer-Phillips generation theorem Theorem

Dependency tree · two levels

43 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)
Mathew A. Johnson, Math 951 Lecture Notes, Chapter 6: Introduction to Semigroup Methods, University of Kansas (complete 37-page chapter) (standard reference, not scraped)
Roland Schnaubelt, Evolution Equations, Karlsruhe Institute of Technology (2023/24 course, complete lecture notes) (standard reference, not scraped)