Functional Analysis

Why nonlocal generators matter

Markov processes with jumps model changes that cannot be represented by continuous diffusion paths: arrivals in queueing systems, sudden failures, population events, and discontinuous changes in financial or physical systems. Their infinitesimal descriptions are nonlocal generators, because the value of the operator at a state depends on test-function values at displaced states rather than only on derivatives at the current point. Chapter 8, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), treats three complementary regimes. Theorem 3.1 covers finite-rate jumps on a general locally compact state space. Theorem 3.4 treats homogeneous Lévy operators on Euclidean space, including infinite jump activity and degenerate covariance. Theorem 3.3 gives the main target here: well-posedness for a time- and state-dependent compensated Lévy-type martingale problem.

These results connect concrete jump kernels and integro-differential operators to two standard descriptions of stochastic dynamics. Autonomous operators are realized as generators of conservative Feller semigroups, while time-dependent operators are characterized through martingale identities. Keeping all three source results in one mission records the nonlocal-generator theme without claiming that their distinct hypotheses imply one another.

The setting

For the Euclidean results, the state space is $\mathbb R^d$, represented in Lean as EuclideanSpace ℝ (Fin d), with $d>0$. A covariance field $a(t,x)$ is a continuous linear endomorphism, a drift field $b(t,x)$ is a vector, and $\nu(t,x,dy)$ is a measure of jump displacements. For a smooth compactly supported test function $f$, the compensated Lévy-type operator is

$$L_t f(x)=\frac12\sum_{i,j}a_{ij}(t,x)\,\partial_{ij}f(x) +Df(x)[b(t,x)] +\int\!\left(f(x+y)-f(x)-\frac{Df(x)[y]}{1+\lVert y\rVert^2}\right)\nu(t,x,dy).$$

The denominator in the compensation term is part of the source convention. The covariance factor $1/2$ applies only to the second-order term; the drift is unscaled. The weighted moment $\lVert y\rVert^2/(1+\lVert y\rVert^2)$ permits measures with infinite total mass while controlling the compensated integral.

A solution of the Lévy-type martingale problem is a jointly measurable process with the prescribed initial pushforward law whose integrated-generator increments have zero expectation against every bounded continuous function of any finite history. Smooth compactly supported functions are the spatial tests. This definition imposes no path-continuity requirement.

The finite-rate model uses a locally compact, noncompact, separable metric space $E$, a nonnegative rate $\lambda(x)$, and a weakly continuous probability transition kernel $\mu(x,dy)$. Its operator is $Af(x)=\lambda(x)\int(f(y)-f(x))\mu(x,dy)$. Positive weights $\gamma$ and $\eta$ specify the graph domain and control behavior at infinity.

Formalization targets

Goal: nonautonomous Lévy-type well-posedness

The main target is Chapter 8, Section 3, Theorem 3.3. The covariance is continuous, symmetric, bounded, and strictly positive definite at every nonzero vector, without a uniform ellipticity constant. The drift is measurable and bounded. The weighted jump measure is integrable, and for every measurable set its weighted mass is a bounded continuous function of time and state.

For every initial probability measure, the conclusion asserts existence of a measurable-process solution on some probability space and uniqueness of all finite-dimensional distributions among every solution on every probability space. Setwise continuity is retained exactly; it is not replaced by weak convergence of measures or by finite total jump intensity.

Related target: homogeneous Lévy generation

Theorem 3.4 freezes the coefficients in time and space. The covariance may be degenerate but is symmetric and nonnegative, and the jump measure needs only the finite weighted integral. The full $\widehat C^2$ graph consists of functions, first derivatives, and second derivatives that vanish at infinity. Its closure is the exact generator of a positive conservative strongly continuous contraction semigroup on $C_0(\mathbb R^d)$, and smooth compactly supported functions form a core.

Related target: finite-rate jump generation

Theorem 3.1 retains the general-state-space jump model. The transition kernel is both setwise measurable and weakly continuous; the rate and weights satisfy the source's vanishing and signed integral bounds. The weighted graph closes to a single-valued conservative Feller generator, and compactly supported continuous functions form a core.

Significance

The main theorem says that the displayed nonlocal characteristics determine stochastic dynamics in distribution even when the drift is only measurable and jump activity need not be finite. The two autonomous theorems identify concrete domains whose closures are genuine Feller generators, including positivity, contraction, strong continuity, conservativity, and core statements. Together they distinguish finite-rate kernels, homogeneous compensated Lévy dynamics, and nonautonomous Lévy-type dynamics while sharing the same generator language.

The formal contribution is a machine-checkable statement layer, not a proof claim. It exposes the exact compensation, weighted-integrability, graph-domain, semigroup, and finite-history conventions on which later proofs depend. The common diffusion operator, bounded-pointwise closure, and strongly continuous contraction-semigroup predicate are reused from earlier private missions in the same textbook series rather than duplicated under conflicting identifiers.

Where the difficulty lies

The obvious finite-jump approximation does not by itself preserve the full conclusions. Infinite jump activity requires compensation near zero, and convergence of the associated operators must still identify the intended martingale problem or the exact closed Feller generator. In the nonautonomous theorem, setwise continuity of weighted jump masses must coexist with merely measurable drift, while uniqueness ranges over arbitrary probability-space realizations and all finite-dimensional laws. Strengthening to continuous drift, imposing finite total jump intensity, assuming uniform ellipticity, or comparing only continuous-path solutions would materially weaken or alter the source theorem.

Formalization scope and conventions

Nonnegative real time is represented by ℝ≥0; Euclidean coordinates use Fin d. Fréchet derivatives express both gradient and Hessian terms. The jump measure is a measure of displacements $y$, so the operator evaluates $f(x+y)$. Integrable hypotheses prevent Lean's totalized integral from silently assigning zero to a divergent positive weighted moment. Positive dimension is explicit through [NeZero d].

The martingale predicate includes empty finite histories and repeated observation times. Its bounded continuous history tests determine the same finite-dimensional identities used by the source, and no sample-path regularity is inserted. The autonomous graphs live in $C_0\times C_0$; bounded-pointwise closure means closure under uniformly bounded pointwise sequential limits, not ordinary norm closure. The finite-rate theorem preserves its restriction of the additional integrability clause to states with positive rate. No vacuous solution predicate, unweighted moment assumption, hidden nonzero-rate condition, or proof-only theorem dependency is introduced.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Section 3, Theorems 3.1, 3.3, and 3.4. Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 4, Sections 2–3 for Feller and martingale-problem conventions, and Appendix 3 for bounded-pointwise closure. Wiley DOI

Why simplex diffusions matter

Finite-dimensional simplices are the natural state spaces for proportions: allele frequencies, population shares, and other collections of nonnegative coordinates whose total cannot exceed one. A diffusion on such a space must do more than solve an unconstrained stochastic equation. Its covariance degenerates on the boundary, and its drift must respect every face so that the process remains in the simplex. Chapter 8 of Ethier and Kurtz develops generator results for this setting as part of the analytic foundation for Markov-process models with constrained state spaces Ethier and Kurtz, Chapter 8, §2.

This mission formalizes their Theorem 2.8, a known generation theorem rather than an open conjecture. The theorem treats arbitrary Lipschitz drift satisfying the inward boundary inequalities. It identifies the closed diffusion graph as a Feller generator and also states that polynomial restrictions form a core. The generality of the drift distinguishes this result from later population-model applications with particular mutation or selection coefficients.

The simplex and its boundary

For a positive integer $d$, the simplex state space is

$$K_d=\left\{x\in\mathbb R^d: x_i\ge 0\ \text{for every }i, \quad \sum_{i=1}^d x_i\le 1\right\}.$$

The missing mass $1-\sum_i x_i$ may be viewed as an additional coordinate. In Lean, WFState d is the subtype of functions Fin d → ℝ satisfying precisely nonnegativity and the upper bound on the coordinate sum. These conditions already imply $x_i\le 1$ for every coordinate.

Let $b:K_d\to\mathbb R^d$ be the drift. The boundary conditions say that $b_i(x)\ge 0$ whenever $x_i=0$, while $\sum_i b_i(x)\le 0$ whenever $\sum_i x_i=1$. Thus the drift cannot point outward through a coordinate face or through the top face. No mutation–selection formula or extra smoothness condition is imposed: global Lipschitz continuity and these face inequalities are the complete drift hypotheses retained here.

The operator and target theorem

The covariance matrix is

$$a_{ij}(x)=x_i(\delta_{ij}-x_j),$$

and the associated simplex diffusion operator is

$$Gf(x)=\frac12\sum_{i,j}x_i(\delta_{ij}-x_j) \,\partial_i\partial_j f(x)+\sum_i b_i(x)\,\partial_i f(x).$$

Only the second-order sum is multiplied by $1/2$. The covariance becomes singular on boundary faces, so this is not an immediate instance of a uniformly elliptic whole-space theorem.

The formal target asserts that the uniform graph closure of

$$\{(f,Gf):f\in C^2(K_d)\}$$

is single-valued and is exactly the generator graph of a positive, conservative, strongly continuous contraction semigroup on $C(K_d)$. Conservativity is expressed by preservation of the constant function $1$. The generator is identified by the right derivative at time zero, not merely by containment of a convenient operator restriction.

The final clause says that polynomials restricted to $K_d$ are a core: closing the graph obtained from polynomial first coordinates gives the same full generator graph. This is a graph-closure statement and is stronger than uniform density of polynomials as functions.

What the result provides

Single-valuedness shows that the closed graph behaves as an operator rather than a multivalued relation. Generation supplies a Feller semigroup whose positivity and preservation of constants give the Markov interpretation. The exact generator biconditional fixes the full infinitesimal domain, while the polynomial-core conclusion permits generator questions to be reduced to algebraically structured test functions without changing the closed operator.

The source theorem is already proved in the book. The formalization task is to recover its generator statement and core conclusion in Lean with all boundary, closure, and semigroup conventions explicit. The current mission contributes a source-reviewed statement and its expression-level definitions; it does not claim a completed Lean proof.

Why the formalization is delicate

The obvious route through standard elliptic diffusion generation does not apply because $a(x)$ degenerates as coordinates approach the boundary. It is also insufficient to prove only that the displayed differential operator is contained in some generator: the theorem identifies the closure of the entire $C^2(K_d)$ graph and separately asserts the polynomial core.

Boundary semantics create another source of possible weakening. Dropping either inward condition would permit outward drift at a face. Replacing the arbitrary Lipschitz drift by a special population-genetics formula would narrow the theorem. Replacing graph equality by inclusion, or polynomial graph density by ordinary function density, would lose a stated conclusion. These distinctions are all preserved in the target.

Formalization scope

The Lean development uses the book-wide namespace EthierKurtz. The compact space $C(K_d)$ is represented by real-valued bounded continuous functions on WFState d; compactness makes this the intended continuous-function space with the uniform norm. A $C^2(K_d)$ function is represented through a globally twice continuously differentiable extension on the ambient finite-coordinate space, following the book’s Appendix 6 extension convention for closed convex sets.

The operator uses Fréchet derivatives evaluated on coordinate vectors, which represent the first and second partial derivatives in the finite-dimensional ambient space. The graph is closed in the product uniform norm. IsStronglyContinuousContractionSemigroup records identity at zero, the nonnegative-time semigroup law, contraction, and strong right continuity at zero. The target additionally records positivity, preservation of one, and equality between its derivative graph and the closed diffusion graph.

The scope excludes the zero-dimensional case, as required by 0 < d. It does not introduce a continuous-path hypothesis, a special drift parameterization, or uniform ellipticity. The only packaged declarations beyond the goal are the state space, operator, graph, and the already published semigroup predicate needed to state it. Proof-only lemmas and unrelated Chapter 8 results are outside this mission.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, §2, Theorem 2.8, printed p. 375; equation (1.15), printed p. 368; Appendix 6, printed pp. 499–500. DOI

Why endpoint classification matters

A one-dimensional diffusion is governed in the interior by a second-order differential operator, but the interior coefficients alone do not determine what happens when the process approaches the edge of its state space. An endpoint may be reachable from the interior or inaccessible; after arrival it may absorb, reflect, or retain the process according to a boundary parameter. The same issue persists when an endpoint is infinite. Chapter 8 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), organizes these alternatives through scale and speed integrals and identifies the exact operator domain that generates the corresponding Feller evolution. This mission formalizes Chapter 8, Section 1, Theorem 1.1, printed page 367.

The setting

Let $-\infty\le r_0<r_1\le\infty$. The real state interval is $I=[r_0,r_1]\cap\mathbb R$, its interior is $I^\circ=(r_0,r_1)$, and $\bar I$ is the closed interval in the extended real line. A function in $C(\bar I)$ is represented by a continuous function on that compact extended interval, so finite endpoint limits are part of the object even when an endpoint is infinite.

The interior diffusion operator is

$$Gf(x)=\frac{a(x)}2 f''(x)+b(x)f'(x),$$

where $a$ and $b$ are continuous on $I^\circ$ and $a(x)>0$ there. Choose an interior reference point $r$. Define

$$B(x)=\int_r^x \frac{2b(y)}{a(y)}\,dy, \qquad p(x)=\int_r^x e^{-B(y)}\,dy, \qquad m(x)=\int_r^x \frac{2e^{B(y)}}{a(y)}\,dy.$$

The corresponding endpoint tests $u$ and $v$ are nonnegative extended-real integrals. Their values may be $+\infty$; preserving that possibility is essential because the four boundary classes are distinguished precisely by which of the two tests are finite.

Formalization target

Theorem 1.1 — one-dimensional boundary diffusion generation

At either endpoint, the pair $(u,v)$ gives the Feller boundary class:

$$\begin{array}{c|cc} \text{class} & u & v\\ \hline \text{regular} & <\infty & <\infty\\ \text{exit} & <\infty & =\infty\\ \text{entrance} & =\infty & <\infty\\ \text{natural} & =\infty & =\infty. \end{array}$$

Entrance and natural endpoints are inaccessible, so the generator domain imposes no boundary equation there. At an exit endpoint the limiting generator value must be zero. At a regular endpoint $r_i$, a parameter $q_i\in[0,1]$ determines the boundary condition

$$q_i\lim_{x\to r_i}Gf(x) =(-1)^i(1-q_i)\lim_{x\to r_i}e^{B(x)}f'(x).$$

The target states that the graph consisting of $f\in C(\bar I)$ that are twice continuously differentiable in the interior, whose $Gf$ extends continuously to $\bar I$, and that satisfy the applicable condition at both endpoints is exactly the infinitesimal generator of a Feller semigroup on $C(\bar I)$. The conclusion includes the semigroup law, contraction, strong right continuity at zero, positivity, preservation of the constant function $1$, and a biconditional identifying the complete generator graph rather than merely an included core or its closure.

Significance

The theorem translates local coefficients into a global Markov evolution while retaining every possible finite or infinite endpoint type. The endpoint tests determine which boundary behavior is available, and the regular-boundary parameter records absorbing, reflecting, and intermediate behavior in one equation. Without the classification, writing down the differential expression does not specify a unique Feller generator because distinct domains can encode different stochastic behavior at the same endpoint.

The formal contribution is a machine-checkable statement layer for the source theorem. It makes the compactified state space, improper endpoint integrals, one-sided endpoint filters, and exact generator graph explicit. The theorem itself remains an open proof obligation in this statement-only mission. The definitions can also support later formal work on hitting distributions, killed or reflected diffusions, and comparison of boundary regimes.

Where the difficulty lies

The main difficulty is that the classification cannot be reduced to ordinary finite integrals or to boundary values at finite real points. Infinite endpoints and divergent scale or speed tests carry mathematical information; replacing extended-real integrals by totalized real integrals would collapse boundary classes. A second difficulty is identifying the full closed generator domain. Showing that the differential expression is meaningful on smooth interior functions is insufficient: the proof must connect its endpoint asymptotics to positivity, conservativity, strong continuity, and exact generation on the uniform-norm space.

Formalization scope and conventions

Endpoints use EReal, and the state space is Set.Icc r₀ r₁ in the extended line. Coefficients are constrained only on the open real interior; no boundedness or uniform ellipticity is added. The drift primitive and scale/speed tests use oriented interval integrals internally and ENNReal endpoint integrals externally, retaining $+\infty$. Absolute values correct the orientation on the left of the reference point.

The graph stores continuous endpoint extensions of both $f$ and $Gf$. Interior $C^2$ regularity is expressed by ContDiffOn ℝ 2, and endpoint limits use the one-sided neighborhood filter induced from the extended interval. The regular parameter is required to lie in $[0,1]$ only when both boundary tests are finite. The mission does not replace the four cases by an opaque classifier, assume finite endpoints, add a pathwise stochastic differential equation, or weaken exact generation to graph inclusion. The shared book definition of a strongly continuous contraction semigroup is reused from the earlier semigroup-generation mission rather than redeclared.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Section 1, Theorem 1.1 and equations (1.1)–(1.11), printed pp. 366–367. Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 4, printed p. 166, for the Feller semigroup convention used in the conclusion. Wiley DOI

Why whole-space diffusion generators matter

Diffusion processes connect stochastic differential equations, partial differential equations, and Markov semigroups. On Euclidean space, their local behavior is encoded by a second-order operator built from a covariance field and a drift field. A central question is whether those local coefficients determine an actual Markov evolution, and whether the resulting evolution is unique. Ethier and Kurtz organize these questions through generator graphs and martingale problems, which allow the same language to cover smooth elliptic diffusions, degenerate models, and coefficients that vary measurably with time. This mission formalizes three complementary whole-space regimes from Chapter 8 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), principally Theorems 1.6, 1.7, and 2.5.

The setting

The state space is the finite-dimensional Euclidean space $\mathbb R^d$, represented in Lean as EuclideanSpace ℝ (Fin d), with $d>0$. A covariance operator $a(t,x)$ is a continuous linear endomorphism of this space, while a drift $b(t,x)$ is a vector. For a smooth scalar test function $f$, the diffusion operator is

$$G_t f(x)=\frac12\sum_{i,j} a_{ij}(t,x)\,\partial_{ij}f(x) + Df(x)[b(t,x)].$$

The factor $1/2$ multiplies only the covariance-weighted second-order term. The formalization uses Fréchet derivatives evaluated in the standard coordinate directions. In the time-homogeneous cases, the smooth compactly supported graph consists of pairs $(f,Gf)$ viewed in $C_0(\mathbb R^d)\times C_0(\mathbb R^d)$, and its uniform closure is the candidate generator.

For time-dependent coefficients, a measurable process solves the time-inhomogeneous martingale problem when its initial pushforward law is prescribed and the integrated generator identity holds against every smooth compactly supported spatial test and every bounded continuous finite-history test. This formulation records the natural-past moment identities without imposing continuity of sample paths as an extra hypothesis.

Formalization targets

Goal: measurable-drift nonautonomous well-posedness

The main target is Chapter 8, Section 1, Theorem 1.7. The covariance and drift are jointly Borel measurable and locally bounded. The covariance is symmetric and nonnegative. At each fixed spatial point it is uniformly elliptic over every bounded positive time interval, and its spatial continuity is uniform over that interval. A common quadratic bound controls the covariance norm and the one-sided radial drift quantity $\langle x,b(t,x)\rangle$.

For every initial probability measure, the conclusion asserts existence of a measurable-process solution on some probability space and uniqueness of all finite-dimensional distributions among every such solution on any probability space. The drift is not assumed continuous, and no stronger norm-growth condition on the drift or moment condition on the initial law is inserted.

Related target: uniformly elliptic Feller generation

Chapter 8, Section 1, Theorem 1.6 treats bounded Hölder continuous time-homogeneous coefficients with symmetric, globally uniformly elliptic covariance. It concludes that the closure of the smooth compactly supported graph is single-valued and is exactly the generator of a positive, strongly continuous contraction semigroup on $C_0(\mathbb R^d)$. Conservativity is retained through membership of the constant graph pair $(1,0)$ in the bounded-pointwise closure.

Related target: degenerate smooth-core generation

Chapter 8, Section 2, Theorem 2.5 permits degenerate and unbounded covariance fields. Its assumptions are symmetry, nonnegativity, twice continuous differentiability of the matrix entries, bounded second partial derivatives, and a globally Lipschitz drift. Its conclusion is the same full Feller generation and conservativity statement. This regime is related to, but not implied by, the bounded uniformly elliptic regime.

Significance

Together the three statements separate distinct mechanisms for obtaining Markov dynamics from local diffusion data. The two autonomous theorems identify when a concrete smooth core closes to a Feller generator, including positivity, contraction, strong continuity, and conservativity. The nonautonomous theorem establishes existence and uniqueness in distribution under substantially rougher temporal behavior and merely measurable drift. Keeping the regimes together exposes the common operator while preserving their incompatible regularity hypotheses.

The formal contribution is a machine-checkable statement layer for these source results and their expression-essential definitions. It does not claim proofs of the theorems. The definitions make explicit the coordinate form of the generator, the $C_0$ graph, the bounded-pointwise closure convention, and the complete finite-history martingale identities. These components can support later formal proofs and other diffusion or martingale-problem developments.

Where the difficulty lies

The source conclusions are not consequences of a single elementary continuity argument. In the Feller cases, identifying the closure of a graph with the generator requires simultaneous control of the operator domain, the semigroup properties, positivity, and conservativity. In the time-dependent case, measurability of the drift is deliberately weaker than continuity, while uniqueness must cover all measurable-process realizations and all finite collections of observation times. Replacing that conclusion by uniqueness only among continuous processes, or strengthening the drift hypotheses until a standard smooth theory applies, would change the theorem.

Formalization scope and conventions

The development uses nonnegative real time and finite-dimensional real Euclidean space. Covariance matrices act as continuous linear maps; their entries are recovered in the standard orthonormal basis. Smoothness is expressed with ContDiff, compact support with HasCompactSupport, and autonomous generator graphs in C₀. The bounded-pointwise closure is the smallest set closed under uniformly bounded pointwise sequential limits, not merely the set of one-step limits.

The martingale-problem predicate requires joint measurability of the process, equality of the initial pushforward measure, and all bounded continuous finite-history identities. Empty histories and repeated observation times are included. The goal compares the complete finite-dimensional laws of any two solutions. No vacuous solution predicate, arbitrary extension of the generator, chosen matrix square root, hidden path-continuity assumption, or proof-only theorem dependency is used.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Theorems 1.6, 1.7, and 2.5. Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 4 for martingale-problem well-posedness and Feller conventions, and Appendix 3 for bounded-pointwise closure. Wiley DOI

Motivation

Continuous-time Markov processes are often studied through operators that describe how observables evolve. The generation question asks when an operator specified on a domain actually determines a strongly continuous family of contractions. Ethier and Kurtz place this question at the start of Markov Processes: Characterization and Convergence because the resulting semigroup language supports their later treatment of processes and convergence. This mission records the full generation characterization in Chapter 1, Theorem 2.6, and retains the related perturbation result in Theorem 7.1.

Setting

Let (E) be a real Banach space. A linear operator (A) has a linear domain (D(A)\subseteq E), which need not equal (E). A family (T(t)), for nonnegative real (t), consists of bounded linear maps (E\to E). It is a strongly continuous contraction semigroup when (T(0)) is the identity, (T(s+t)=T(s)T(t)), every (T(t)) has norm at most one, and (T(t)x\to x) as (t\downarrow0) for every (x\in E). Its infinitesimal generator has exactly those (x) for which the right-hand difference quotient (t^{-1}(T(t)x-x)) converges, and sends each such (x) to the limit.

An operator is dissipative here when

$$r\lVert x\rVert\leq\lVert rx-Ax\rVert \quad(x\in D(A),\ r>0).$$

The range condition for a positive (r) says every vector in (E) is (rx-Ax) for some (x\in D(A)). Density means that vectors in (D(A)) approximate every vector in (E). These are independent requirements in the formal statement; neither the domain nor the operator is assumed closed or bounded.

For the related perturbation theorem, (A) and (B) may have different domains. Their sum uses the intersection of those domains. Closure is closure of the graph in (E\times E). A graph closure is required to be the graph of a single-valued operator before it can be called a generator.

Formalization targets

Theorem 2.6: generation characterization

The goal is the equivalence

$$A\text{ generates a strongly continuous contraction semigroup} \quad\Longleftrightarrow\quad \overline{D(A)}=E,\quad A\text{ is dissipative},\quad \operatorname{Ran}(rI-A)=E\text{ for some }r>0.$$

The left side uses the full infinitesimal-generator domain, rather than agreement with a generator only on a smaller subdomain. The right side includes dissipativity for every positive parameter and full surjectivity for at least one positive parameter.

Theorem 7.1: relatively bounded perturbation

The retained related result assumes that the closure of (A) is single-valued and generates a strongly continuous contraction semigroup, (D(A)\subseteq D(B)), and (B) is dissipative. It further assumes

$$\lVert Bx\rVert\leq\alpha\lVert Ax\rVert+\beta\lVert x\rVert \quad(x\in D(A)),\qquad 0\leq\alpha<1,\quad\beta\geq0.$$

It concludes that the closure of (A+B) is single-valued and generates such a semigroup, and that its entire graph equals the sum of the graph closures of (A) and (B). This theorem is a related generation variant within the same mission, not a separate main goal.

Significance

The equivalence turns an existence question about a family of operators into conditions on a single potentially unbounded operator. In particular, it preserves the exact-domain requirement: proving only that a semigroup generator extends (A) would answer a weaker question. The perturbation theorem then identifies circumstances under which an already generating operator remains useful after adding a dissipative term that need not itself be bounded.

The textbook proves both statements. The Lean files supplied here are statements with intentional proof holes; they do not claim machine-checked proofs. A completed formalization would supply proofs of these source results while keeping the domain, range, closure, and relative-bound conditions shown in the statements.

Difficulty

The hypotheses describe a linear map on only part of the Banach space, while the conclusion requires bounded operators on all of (E) at every nonnegative time. Checking a semigroup law on a convenient subspace is insufficient unless the resulting operators and generator have the stated full domains. For perturbations, graph closure can enlarge a domain. An equality of formulas on (D(A)) alone would therefore omit the theorem's graph and domain conclusion.

Formalization scope

Lean uses NormedAddCommGroup E, NormedSpace ℝ E, and CompleteSpace E for the real Banach space; Submodule ℝ E for each domain; D →ₗ[ℝ] E for an operator that need not be bounded; and E →L[ℝ] E for each semigroup operator. Semigroup values at negative real times are unconstrained. The derivative is the right limit through positive times. Graph closure is topological closure in the ambient product, and graph sum requires a common input. The strict relative bound (\alpha<1) and positive resolvent parameter remain explicit.

The reusable definitions are the semigroup predicate, full generator predicate, operator graph, and graph sum. The mission welcomes proofs of the two stated theorems and genuinely source-based supporting lemmas. A model with an empty operator domain, an operator restricted from a larger generator, or a conclusion that drops the graph equality would not satisfy the target.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 1, Sections 2 and 7, Theorems 2.6 and 7.1. Book record.