Operations Research

Motivation

Sequential decisions often have costs whose timing matters. A controller may choose an action now, observe a random next state, and choose again. Ordinary expected-cost minimization averages the sum of the costs. A risk-sensitive criterion first applies an increasing function $U$ to the total cost and then takes its expectation. The curvature of $U$ changes how uncertain costs affect the ranking of policies: convex utility penalizes variability in a cost-minimization problem, while concave utility has the opposite tendency. Bäuerle and Rieder study this criterion for controlled Markov processes with general continuous increasing utility, rather than fixing an exponential function. Their finite-horizon discounted result is Theorem 3.6, pp. 10–12 of the authors' manuscript.

Discounting gives early and late costs different weights. For linear $U$, the remaining expected cost can be described using only the current physical state. For general $U$, the effect of a future cost also depends on what has already been paid and on the discount weight currently attached to the next cost. The mission targets the paper's finite-horizon treatment of these two additional quantities. The infinite-horizon problem is a separate part of the paper.

Setting

The state space $E$ and action space $A$ are Borel spaces. At state $x$, the nonempty set $D(x)$ contains the actions that may be chosen. If action $a\in D(x)$ is selected, the next state has distribution $Q(\cdot\mid x,a)$ and the stage cost is $c(x,a)$. The cost is measurable and bounded between positive constants $\underline c$ and $\overline c$. The discount factor satisfies $0<\beta<1$, and $U:[0,\infty)\to\mathbb R$ is continuous and strictly increasing. The paper imposes its compactness and continuity conditions (CC) on $U$, $D$, $c$, and $Q$; these are stated in the model item and correspond to §2, pp. 3–4.

A history policy $\sigma=(g_0,g_1,\ldots)$ chooses $A_n$ measurably from the states and actions observed through time $n$. Starting from $x$, it induces a law for the state-action trajectory. The first $n$ stages incur the discounted cost $C^n_\beta=\sum_{k=0}^{n-1}\beta^k c(X_k,A_k)$, with $C^0_\beta=0$. The paper minimizes $E_x^\sigma[U(C^N_\beta)]$ over every admissible history policy. The inverse utility appearing in the paper's original certainty-equivalent criterion can be omitted when selecting a minimizer because $U$ is strictly increasing §2, p. 3; §3.3, p. 10.

The extended state is $\hat E=E\times[0,\infty)\times(0,1]$. Its coordinates $(x,y,z)$ record the current physical state, accumulated cost, and current discount weight. Define $V_{n\sigma}(x,y,z)=E_x^\sigma[U(y+zC^n_\beta)]$ and $V_n=\inf_{\sigma\in\Pi}V_{n\sigma}$. A measurable extended-state decision rule $f$ chooses an action in $D(x)$. The paper's operator $T_f$ integrates a continuation value at $(x',y+zc(x,f(x,y,z)),z\beta)$; $T$ takes the infimum of the same integral over $D(x)$ equations (3.8)–(3.9), pp. 10–11.

Formalization targets

The first target identifies the cost iteration of any sequence of extended-state rules $\pi=(f_0,f_1,\ldots)$:

The second target is the paper's value iteration for the infimum over all history policies, together with membership of every $V_n$ in its regularity class $C(\hat E)$:

The goal is Theorem 3.6(c): minimizers $f_k^*$ of $V_{k-1}$ exist, and their stage-dependent history rules attain the original objective $J_N(x)=V_N(x,0,1)$ for every $x$. At stage $n<N$, the rule uses $f_{N-n}^*$ at the current state, the observed sum $\sum_{j<n}\beta^jc(X_j,A_j)$, and $\beta^n$. “Optimal” compares against all admissible history policies, including those that use more of the history than these three quantities.

Significance

Theorem 3.6 gives a finite sequence of minimum-operator evaluations for a problem whose utility of total cost is not additively separable in the physical state alone. Its policy statement also identifies which observable quantities an optimal controller needs to retain. Together, these results relate the original history-dependent problem to an extended-state Markov decision problem §3.3, pp. 10–12.

The paper proves these statements. This mission asks for machine-checked definitions and proofs of the finite-horizon discounted theorem, including the comparison with all admissible history policies. The model layer and the finite-dimensional expectation construction can support later formalizations of other risk-sensitive objectives. The mission itself has no completed proof at the drafting stage.

Difficulty

The extra discount coordinate is essential: after one action, the next cost enters utility with weight $z\beta$, not $z$. Keeping only accumulated cost would describe a different process. The other demanding point is the policy comparison. An iteration over extended-state decision rules has to establish the value of an infimum over arbitrary measurable history policies. Regularity and measurable selection must also be maintained at each step under (CC). The proof of Theorem 3.6 invokes the corresponding total-cost argument from Theorem 3.1, pp. 5–6; the formal development must supply the precise discounted version.

Formalization scope

Lean represents $E$ and $A$ as Borel subsets of Polish spaces, with standard Borel measurable structures. The controlled process is a separate reusable definition containing $D$, $Q$, and history policies; the risk-sensitive model adds $c$, $\beta$, and $U$. The admissible graph is Borel and every section $D(x)$ is nonempty. A history is a chronological finite list of earlier state-action pairs and a current state. Each rule is defined on all lists, but only admissible lists of the matching length are visited. The transition kernel is total as a Lean object, and its values outside $D$ are irrelevant.

Policy values use nested kernel integrals representing the finite-dimensional marginals of the path law. They are defined from the cost and utility, so the Bellman recursion remains a theorem. The optimized value is an infimum over the subtype of measurable, admissible infinite history policies. The real infimum is meaningful here because this policy class is nonempty under (CC) and finite-horizon costs keep utility bounded on the relevant interval. The extended state uses real coordinates restricted to $y\ge0$ and $0<z\le1$; its transition stays in that domain. “Increasing” in $C(\hat E)$ means componentwise nondecreasing in $(y,z)$. A minimizer is an admissible measurable rule satisfying $T_fv=Tv$ on the entire extended domain.

The source's proof sentence that $T$ preserves $C(\hat E)$ is recorded with explicit integrability of each one-step continuation. For an arbitrary real-valued member of $C(\hat E)$ on an unbounded state space, the source's conditions alone do not ensure a finite real expectation. This domain condition prevents Lean's zero value for a nonintegrable real integral from turning the assertion into a different one. It does not narrow the finite-horizon values appearing in the goal. Contributions toward finite-dimensional expectation identities, kernel integrability, the regularity of $V_n$, and measurable minimizer selection are within scope.

Selected references

• N. Bäuerle and U. Rieder, More Risk-Sensitive Markov Decision Processes, authors' manuscript, KIT repository 1000039663; published in Mathematics of Operations Research 39(1):105–120, 2014. Manuscript; DOI.

Why observations matter in finite-horizon control

When a controller acts on a system whose state is hidden, measurements may help it choose later actions, but the value of those measurements depends on the transition law, the observation mechanism, and the available controls. Åström's 1965 paper gave a finite-state formulation of this problem and compared the best expected loss under incomplete measurements with two limiting cases: exact state observations and no useful observations. The comparison, stated in (5.12), quantifies the value of the information available to the controller without requiring a particular numerical example. Åström, 1965.

The bounds are useful when an exact partially observed policy is difficult to calculate. The complete-information problem provides an optimistic benchmark, because a controller that sees the hidden state can condition its decision on more information. The open-loop problem provides a conservative benchmark, because it commits to a control schedule without responding to later measurements. Both auxiliary problems have simpler backward equations than the partially observed problem, as Åström notes in §V of the paper. Åström, 1965, pp. 190–193.

Model and notation

The hidden state $x_t$ belongs to a finite nonempty set $S$, and the measured output $y_t$ belongs to a finite nonempty set $Y$. There are $N\ge1$ decision stages. At stage $t$, a control $u(t)$ is chosen from a nonempty compact set $U\subseteq\mathbb R^d$. Given state $i$ and control $u(t)$, the next state is $j$ with probability $p_{ij}(u(t),t+1)$. At state $i$, the observed output is $j$ with probability $q_{ij}$; observations are conditionally independent given the state path. The stage loss is $g(u,i,t)$, with no fixed sign, terminal loss, or discount. The transition probabilities and loss are continuous in the control. Åström, 1965, §II.

An admissible control law may use the whole output history $y_1,\ldots,y_t$ when choosing $u(t)$. Write $J(c)$ for its expected total loss, computed from the joint law of the state and output paths, and write $\mathrm{OPT}$ for the infimum of $J(c)$ over every such admissible law. The distribution of $x_1$ is $p_1$. After the first output $\eta_1$, the belief $w(1)$ is the conditional distribution of $x_1$. More generally, $w(t)$ is the conditional distribution of $x_t$ given outputs through time $t$, when that history has positive probability.

Three backward values describe the information regimes. The partial-observation value $V_k(w)$ obeys the Bayesian recursion (3.28). The complete-information value $V'_k(w)$ is the linear extension $\sum_i S_k(i)w_i$ of the statewise recursion (5.4). The open-loop value $V''_k(w)$ obeys (5.7), in which the belief moves by prediction through $P(u)$ without using an output. Each recursion has terminal value zero at $N+1$. Åström, 1965, pp. 184, 190–191.

Formalization targets

Theorem 2 identifies the partial-observation value with the original control problem: a selector attaining the minimum in (3.28) exists, and every such selector yields an admissible feedback law attaining $\mathrm{OPT}=\mathbb E_{\eta_1}V_1(w(1))$. Theorem 4 gives the complete-information lower bound $V'_k(w)\le V_k(w)$, and Theorem 5 gives the open-loop upper bound $V_k(w)\le V''_k(w)$ for every probability belief and every stage $1\le k\le N$. Both inequalities apply to a general observation matrix. Åström, 1965, Theorems 2, 4 and 5.

The goal is the paper's expected-cost comparison (5.12), with its middle term explicitly identified as the minimum of the original problem:

Here the expectation is over the first measured output under $p_1$ and $Q$. An output with probability zero contributes zero. The left and right members represent, respectively, the costs with perfect state information and with no useful measurements. Åström, 1965, (5.12), p. 193.

What the result provides

For any model satisfying the stated finite-state assumptions, the two easier dynamic programs bracket the best achievable expected loss with partial information. The differences between these values are the paper's measures of the value of perfect state information and the value of incomplete state information, described immediately after (5.12). Because the loss may have either sign, these are order comparisons of minimal costs rather than bounds that depend on a nonnegativity convention. Åström, 1965, (5.13)–(5.14).

The mathematical result was established in the paper. This mission asks for machine-checked proofs of its finite-path model, the three value recursions, the identification of P.1's minimum, and the information bounds. The value functions are linked by shared definitions, so later finite-state partially observed control developments can reuse the pathwise cost and Bayes update instead of rebuilding them for each theorem.

Where the proof is difficult

The tempting comparison between the three Bellman equations cannot simply replace the posterior belief by its average: the controller may choose different actions after different observations, and the continuation value is generally nonlinear in the belief. The exact-information case must also be read at beliefs concentrated at a single state. Its value formula is linear in an arbitrary input belief by definition, but the partial-observation value need not equal that linear function away from those state vertices. A second issue is connecting a feedback solution of (3.28) to the original expected loss over all output-history laws; using a belief-defined objective at the outset would assume the identification that Theorem 2 establishes.

Formalization scope

The Lean model uses finite state, output, and horizon types, a nonempty compact control set in $\mathbb R^d$, stochastic transition and observation rows, and continuous dependence on controls where the paper requires it. All probabilities and expectations are finite sums and products. A Fin N index of zero represents paper time one. The model starts from the law of $x_1$, since §II introduces the law of $x_0$ but specifies neither a control at time zero nor the transition to $x_1$. The transition controlled at time $t$ is therefore written with the paper's transition index $t+1$. These conventions make the first-output expectation and (3.22) use the same timing.

The norm of $z^j$ is its $\ell^1$ norm, the sum of absolute coordinates. At an impossible output, Lean's totalized posterior is zero; the associated continuation term has weight zero. Conditional-probability claims apply only to positive-probability histories. Each minimum over controls is represented by a real infimum over $U$. The compact control set is nonempty and the continuous costs are bounded on it, so this has the intended finite attained meaning on probability beliefs. The terminal values $V_{N+1}$, $S_{N+1}$ and $V''_{N+1}$ are zero.

The original objective is a separate pathwise expected cost, minimized over all admissible output-history laws. The target includes its equality with $\mathbb E_{\eta_1}V_1(w(1))$; stating only an inequality between three unrelated Bellman solutions would omit the subject of (5.12). Reusable contributions include finite-path probability identities, the Bayes recursion, attainment for continuous control minima, and the three value comparisons. No special observation matrix is assumed in Theorems 4, 5, or the goal.

Selected references

• K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. DOI: 10.1016/0022-247X(65)90154-X.

Motivation

In a congestion game, several users choose facilities and each facility becomes more costly as more users choose it. Such games model settings in which each participant chooses a route or collection of resources for personal use while the resulting load is shared. A pure Nash equilibrium is a stable choice of routes: no single participant can lower their own cost by switching. Stability alone gives no assurance that the resulting allocation serves the group well. The price of anarchy compares the social cost of an equilibrium with the best social cost attainable by coordinated choices.

Christodoulou and Koutsoupias studied finite congestion games with linear latency functions and several notions of social cost. For the maximum cost borne by any player, their STOC 2005 paper gives both an upper bound valid for all such games and a family of instances showing that its square-root dependence on the number of players has the right order. This mission formalizes those two claims together. The maximum criterion matters when a single heavily delayed user is significant even if the total cost of the population is moderate.

Setting

Let $N\ge1$ be the number of players and let $E$ be a finite set of facilities. Player $i$ has a finite collection $\Sigma_i$ of available pure strategies, each a subset of $E$. A profile $A$ chooses one strategy $A_i\in\Sigma_i$ for every player. For a facility $e$, its load $n_e(A)$ is the number of players whose chosen strategy contains $e$. The latency of $e$ at load $n$ is $f_e(n)$. Player $i$ pays the sum of the latencies on the facilities they chose:

A profile is a pure Nash equilibrium if no player can decrease this cost by replacing their own strategy while the others keep theirs. The paper calls latencies linear when $f_e(n)=a_en+b_e$ with $a_e,b_e\ge0$; these are affine functions in standard terminology. The paper displays many calculations for the special case $f_e(n)=n$ and states the general nonnegative affine convention in its model section. The maximum social cost is $\operatorname{MAX}(A)=\max_i c_i(A)$; the total cost is $\operatorname{SUM}(A)=\sum_i c_i(A)$. The paper's average social cost is $\operatorname{SUM}(A)/N$.

For a game with at least one pure Nash equilibrium and a positive optimal maximum cost, the maximum-cost pure price of anarchy is the largest equilibrium value of $\operatorname{MAX}$ divided by the smallest feasible value. The Lean targets use inequalities against every feasible comparison profile $P$ rather than dividing by an optimum. This form continues to say something when an optimum has cost zero, and finite strategy sets ensure an optimum exists whenever the profile space is nonempty.

Formalization targets

Universal upper bound

For every $N\ge1$, every finite game with nonnegative affine latencies, every pure Nash equilibrium $A$, and every feasible profile $P$, Theorem 5's proof yields

This states a numerical version of the paper's $O(\sqrt N)$ theorem without an unspecified constant. Taking $P$ to minimize $\operatorname{MAX}$ gives the corresponding price-of-anarchy bound. The bound is about asymmetric games: players may have different strategy sets, and no symmetry assumption is present.

Lower-bound family

For every integer $k\ge2$, let $N=k(k-1)+1$. Theorem 6 provides an identity-latency congestion game with $N$ players and $kN$ facilities, a pure Nash profile $A$, and an optimal profile $P$ for which

Every feasible profile in the instance has maximum cost at least $k$. Thus the ratio is $k$, and $k\ge\sqrt N$. The proof's explicit instance has positive comparison cost, so the lower bound cannot be satisfied by a zero-cost game. The source also says such behavior occurs in network congestion games and sketches a network realization in Figure 2; this mission's formal lower target is the finite congestion-game construction.

Significance

Together these results identify the order of growth of the worst pure equilibrium maximum cost relative to an optimum: it can grow with the population, yet for linear latencies it grows no faster than a constant times $\sqrt N$. The upper statement applies to any feasible comparison profile, so it can also be used when a convenient benchmark is known without solving the entire optimization problem. The lower family prevents replacing the square-root dependence by a bound independent of $N$ for this class of games.

The results are proved in the 2005 paper; the mission is to give them machine-checked Lean proofs in a common finite-game representation. The development also supplies reusable definitions of congestion games, loads, pure cost equilibria, and maximum social cost, together with the total-cost estimate of Theorem 1 and the intermediate bounds appearing in Theorem 5. The current draft contains statements with sorry placeholders, not completed proofs.

Difficulty

A bound on total player cost does not directly control the cost of the most expensive player sharply enough. An individual player can use several facilities whose loads interact, and bounding each load separately loses the dependence required for the square-root result. Affine coefficients add another issue: the proof printed for identity latencies writes a cardinality where the general statement needs a coefficient-weighted quantity. The lower example has an indexing discrepancy in the printed alternative strategies, so the intended Nash profile must be checked against the costs on every permitted deviation.

Formalization scope

Players are represented by Fin N; facilities by an arbitrary finite type in upper bounds and by a type with $kN$ elements in the lower family. A profile is a function from players to finite facility sets, with feasibility stated separately. Latencies are real-valued on natural-number loads. The IsLinear predicate requires explicit nonnegative affine coefficients. Pure Nash uses a cost inequality; it is the negative-payoff version of a standard finite game's payoff equilibrium. MAX requires at least one player, and all upper-bound targets therefore require $N\ge1$. The lower family begins at $k=2$, where $N=k(k-1)+1$ is positive.

The source's number $k^2-k+1$ is written as $k(k-1)+1$ in Lean to keep natural-number subtraction inside its valid range. The two expressions agree for $k\ge2$. In the source's one-based indexing, the proposed alternative strategy uses a ceiling index. The printed denominator $k$ makes some alternative facilities carry $k+1$ users and breaks the Nash assertion; denominator $k-1$ agrees with Figure 2's $k-1$ short-route users per layer and gives the stated costs. This correction is recorded with the lower theorem. No normalization of coefficients or artificially restricted strategy class is assumed. Contributions to the finite-game definitions, Theorem 1, the player-cost bounds, and the explicit lower instance are all in scope.

Selected references

• G. Christodoulou and E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, Proceedings of the 37th Annual ACM Symposium on Theory of Computing, 2005. DOI: 10.1145/1060590.1060600.

Motivation

Large interacting diffusion systems often have different interaction strengths between different pairs of agents. A graphon gives a continuum description of such weighted networks: each agent carries a label in $[0,1]$, and a kernel assigns the strength of interaction between two labels. The question in this mission is whether the law of the resulting continuum stochastic system changes continuously when its graphon changes. This matters when a large finite network is represented by an approximate graphon, since an approximation of the network should lead to an approximation of the dynamics. Bayraktar, Chakraborty and Wu establish this stability as Theorem 2.1(c) of Graphon mean field systems.

The paper also studies dense and less dense finite-particle systems. Their convergence results use a limiting graphon particle system even when the limiting kernel is only measurable, with no continuity in the labels. Theorem 2.1(c) is the continuity result that makes approximation by simpler graphons useful in those later sections Bayraktar–Chakraborty–Wu, §§3–4.

Setting

Let $I=[0,1]$, fix a time horizon $T>0$, and let $\mathcal C_d=C([0,T];\mathbb R^d)$ be the space of continuous paths with the uniform norm $\|x\|_{*,t}=\sup_{0\le s\le t}|x_s|$. A graphon $G:I^2\to[0,1]$ is measurable and symmetric. Its cut norm is the largest absolute integral of $G$ over a measurable rectangle $S\times U\subseteq I^2$. For two graphons, their cut distance is the cut norm of their difference.

For each label $u\in I$, an initial state $X_u(0)$ and a $d$-dimensional Brownian motion $B_u$ live on one probability space. Initial states are mutually independent, Brownian motions are mutually independent, and the two families are independent of each other. The initial state has law $\mu_u(0)$. The process $X_u$ evolves with a drift obtained by averaging $b(X_u(s),x)G(u,v)$ first against the time-$s$ law of $X_v$ and then over $v\in I$. Its diffusion coefficient averages the matrix-valued $\sigma(X_u(s),x)G(u,v)$ in the same way and drives $B_u$. This is the graphon particle system (2.1) Bayraktar–Chakraborty–Wu, p. 3591.

Condition 2.1 requires measurable initial laws, a uniform $(2+\varepsilon)$ moment for some $\varepsilon>0$, and a common global Lipschitz bound for $b$ and $\sigma$. The path-law family $\mu=(\mathcal L(X_u))_{u\in I}$ belongs to $\mathcal M$ when it is measurable as a family of probability measures on $\mathcal C_d$ and has uniformly bounded second moments. The distance $W_{2,t}$ between path laws uses the supremum norm through time $t$; $W^\mathcal M_{2,t}$ is the supremum of these distances over labels Bayraktar–Chakraborty–Wu, pp. 3591–3592.

Formalization targets

Stability of path laws

For graphons $G_n$ converging to $G$ in cut metric, let $\mu^{G_n}_u$ and $\mu^G_u$ be the laws of the associated solutions, with the same initial laws and coefficients. The target is

The conclusion is an integrated law convergence statement. It does not assert that the laws converge uniformly in $u$ or that paths converge almost surely. This is precisely Theorem 2.1(c) Bayraktar–Chakraborty–Wu, p. 3593.

Supporting results

The mission also states the paper's cut-to-operator convergence (Remark 2.1), existence of frozen-flow solutions (5.2), the squared estimate established in the proof of (5.3), well-posedness and moments for the nonlinear system (Proposition 2.1), and the quantitative stability display on p. 3604. These are the source's claims used to reach the target, with their provenance attached to each milestone Bayraktar–Chakraborty–Wu, §§2 and 5.

Significance

Stability shows that the continuum model is robust to graphon approximation in a metric natural for dense networks. Together with Proposition 2.1, it gives a well-defined solution-law family whose dependence on the network kernel can be controlled. The paper uses this framework in its later laws of large numbers for finite interacting systems Bayraktar–Chakraborty–Wu, §§3–4.

The theorem is proved in the paper; this mission asks for a machine-checked proof of the faithful statements. A complete development would also supply reusable Lean interfaces for graphons, cut and operator norms, measurable families of path laws, and stochastic systems whose coefficients depend on those families. The Itô-process and general Wasserstein definitions already available as published modules are reused. The remaining graphon-specific definitions and the estimates in §5 are open proof targets.

Difficulty

A direct stability argument for stochastic differential equations would compare the two coefficients point by point. Cut convergence does not provide pointwise convergence of $G_n(u,v)$ to $G(u,v)$, nor a uniform bound on their difference that tends to zero. The drift and diffusion also contain laws generated by the processes being compared, so a change in the graphon feeds back into the law family. The central challenge is to control these coupled differences using only a weak kernel metric while retaining the measurable structure needed to integrate over labels Bayraktar–Chakraborty–Wu, §5.2.

The result also depends on a well-posedness theory for a continuum of stochastic equations. The laws need to vary measurably with $u$ even though the paper does not assume the sample paths themselves vary measurably with $u$ Bayraktar–Chakraborty–Wu, Remark 2.3(b).

Formalization scope

Lean uses unitInterval for $I$, nonnegative real time, and continuous maps from $[0,T]$ to Fin d → ℝ for $\mathcal C_d$. The norm on $\mathbb R^d$ is the sup norm; the paper's Euclidean norm is equivalent in finite dimension, so existential Lipschitz and stability constants may change while the qualitative claim remains the same. The diffusion coefficient is a $d\times d$ matrix, measured through its entries. Wasserstein quantities and nonnegative expectations are valued in $[0,\infty]$, avoiding defaults for infinite moments. The path-law family uses the measurable space of measures, with the Borel space on paths. A zero-time or zero-dimensional state space is admitted where the formulas still have their stated meaning; $T>0$ and $\varepsilon>0$ are explicit.

For each graphon, a solution is a continuous-path process driven by the same given initial variables and Brownian motions, adapted to the natural filtration of those variables for each label. Its path map is almost everywhere measurable, its law family belongs to $\mathcal M$, and the nested interaction integrals are required to be integrable. These clauses prevent a zero measure from arising through a nonmeasurable pushforward and prevent a nonintegrable Bochner integral from silently evaluating to zero. The graphons are explicitly measurable, symmetric, and $[0,1]$-valued, so the real cut and operator norms are used only on bounded kernels. The theorem also asserts measurability of each Wasserstein integrand, reflecting the paper's treatment of the displayed integral.

The paper's proofs are in §§5–7; this mission concerns §5. Contributions to any stated milestone and to the reusable measure and Itô lemmas needed for them are welcome. A formalization that assumes the stability limit, that treats arbitrary unbounded kernels as graphons, or that uses an empty solution class would not establish this target.

Selected references

• E. Bayraktar, S. Chakraborty and R. Wu, Graphon mean field systems, Annals of Applied Probability 33(5), 3587–3619, 2023. DOI 10.1214/22-AAP1901.

Motivation

A failed buyer can leave a supplier with goods it can no longer sell through an existing order. A failed supplier can leave a buyer without inputs for future production. In a network, either loss can weaken another firm and start a sequence of defaults. Birge, Capponi and Chen model these effects together with two responses: suppliers reroute unsold goods to other buyers, and buyers seek replacement suppliers. Their accepted manuscript asks whether the resulting market decisions and the default cascade determine a single outcome. The issue matters when a network's resilience or fragility is measured from that outcome: a measure based on an unspecified equilibrium would not be well defined.

Setting

A supply chain order network has finitely many firms $i,j$ and goods $m$. An order $o^m_{ij}$ is the nonnegative quantity of good $m$ that firm $i$ promises to deliver to firm $j$. The network also records each good's original price $p^m$, each firm's initial equity $w_i$, its safety stock $\theta_i^m$ and holding cost $\lambda_i^m$, and a realized net production cost $c_i$. The realization is fixed throughout this mission; the source treats it as random when comparing network performance later in the paper. Rerouting one unit costs firm $i$ an amount $\iota_i^m$; an unfilled unit of demand incurs back-order cost $b_i^m$. These costs and the orders and stocks are nonnegative. The basic model is on pp. 8–17 of the manuscript.

If firm $j$ defaults, a promised delivery to it is not made. Write $\gamma^m_{ij}$ for this undelivered order, and $\bar r_i^m=\sum_j\gamma^m_{ij}$ for firm $i$'s total amount of good $m$ available to reroute. If a supplier $j$ defaults, write $\delta^m_{ji}$ for the buyer $i$'s lost input. After using safety stock, that buyer's unserved demand is $\bar\sigma_i^m=(\sum_j\delta^m_{ji}-\theta_i^m)^+$, where $x^+=\max(0,x)$. These are the quantities in equations (1)–(5).

The rerouted market for good $m$ contains firms with $\bar r_i^m>0$. At price $\pi_i^m$, firm $i$ can sell up to $\bar r_i^m$. Aggregate demand at price $\pi$ is $d_m(\pi)$, with inverse demand $d_m^{-1}$. The sourcing market contains firms with $\bar\sigma_i^m>0$. At switching cost $\kappa_i^m$, firm $i$ can replace up to $\bar\sigma_i^m$ units. Aggregate supply is $s_m(\kappa)$, with inverse supply $s_m^{-1}$. In either market, an efficient allocation maximizes the stated integral objective over the capacity box, and allocates proportionally to capacity among firms quoting the same price or cost. A partial equilibrium additionally makes every active firm's quoted price or cost a best response to all nonnegative unilateral deviations. These are Definitions 2.1–2.2 and 3.1–3.2.

A firm's ex-post net worth $e_i^*$ combines original-order revenue, production and stock costs, rerouting revenue and cost, and back-order and replacement-supplier costs exactly as in equation (10). A firm defaults when its net worth is strictly negative. Starting with no undelivered orders or unserved demand, the update maps $\Phi^*$ and $\Psi^*$ mark all orders affected by firms that default after each market has reached its partial equilibrium. A market stable state is both the limit of that sequence and a fixed point of the update. A general equilibrium combines such a state with a partial equilibrium in every market (Definitions 3.3–3.4 and equation (18)).

Formalization targets

The goal is Proposition 4.3, stated on p. 24:

The quadruple consists of rerouting prices $\Pi$, switching costs $K$, undelivered orders $\Gamma$, and unserved demand $\Delta$. The claim includes existence and uniqueness of the full outcome, not merely of its default set. The milestone list follows the paper's dependency path: Propositions A.3 and A.6 identify the unique efficient allocations in the two markets; Propositions 4.1 and 4.2 identify their partial equilibria; Lemma A.7 states that greater disruption cannot increase any firm's partial-equilibrium net worth; and Lemma A.8 states that the default updates are bounded and increasing. The numbered results and their equations are in the E-Companion, EC pp. 4–12, and the main text, p. 22.

Significance

Proposition 4.3 makes the network's outcome a function of its order commitments, stocks, prices, market functions, and realized production costs. Later comparisons of network structures can therefore refer to the equilibrium without choosing among several price or default profiles. The result also separates local market choice from the way losses spread through the network: a firm can reroute or switch optimally and still fail once the effects of other failures are accounted for.

The paper proves the result in its E-Companion, EC pp. 12–13. This mission concerns a Lean statement of that known result and the reusable definitions needed to check a proof. The draft propositions are open proof obligations; this proposal does not claim machine-checked proofs of them. The two market allocation predicates, the default update, and the cascade limit can also support later formal work on the paper's resilience results.

Difficulty

The market and network conditions interact. An arbitrary fixed point of the default update need not be the state reached from zero; using only the fixed-point equation loses the uniqueness asserted by the paper. Conversely, knowing a cascade limit does not by itself show that the limit is fixed, because the update changes discontinuously when a firm's net worth crosses zero. At the market level, the price and switching-cost equilibria must be established from optimization and best-response conditions. Writing the formulas for the claimed equilibrium prices into those definitions would leave the central market claims unproved.

Formalization scope

Firms are Fin N and goods are Fin M, with $N,M>0$; the source numbers both from one, while Lean numbers them from zero. Orders and all default matrices are real valued and coordinatewise ordered. Active markets may be empty, as at the start of the cascade. Market objectives are ordinary real interval integrals over finite capacity boxes. The standing conditions include the paper's smoothness, concavity, and monotonicity assumptions on demand wherever it is positive and on the supply function, plus inverse identities and continuity on the quantity ranges used by the model. The inverse functions remain general data tied to $d_m$ and $s_m$; no linear demand or supply curve is imposed.

Several domain conventions make the displayed formulas meaningful. Assumption 2.1's minimum order is read over positive-order suppliers of a good; over all firms it would force zero safety stock whenever a nonsupplier exists. The inverse supply is nonnegative on feasible quantities, with $s_m(0)\le0$, so the claimed switching cost belongs to the nonnegative strategy space. Demand inverse at zero is fixed to the reservation price. Assumptions 4.1–4.2 apply at each positive active-market total; for the general-equilibrium goal they are required for every binary $0/o^m_{ij}$ profile the cascade can visit. Differentiability at those totals is explicit. Initial equity and the order, stock, holding, rerouting, and back-order data are nonnegative; the realized net production cost can have either sign. The model uses the p. 23 convention for prices and costs outside active markets.

An efficient allocation remains an optimizer of equations (7) or (9), with proportional tie handling; a partial equilibrium remains a best response to every admissible deviation. The general equilibrium includes both the limit from zero and the fixed-point condition. These clauses exclude an equilibrium that is true by definition or a fixed point unrelated to the default cascade. The source's informal statement that every firm “supplies, consumes, or purchases” a good has no separate activity flag in this model; a firm with no internal order can still have outside production or consumption represented in $c_i$. Milestone statements involving arbitrary disruption profiles restrict them to the feasible order box $[0,O]$, where the market inverses are defined.

Selected references

• John R. Birge, Agostino Capponi, and Peng-Chu Chen, Disruption and Rerouting in Supply Chain Networks, accepted manuscript dated October 31, 2022, SSRN 3669363; published in Operations Research, 2023, DOI 10.1287/opre.2022.2409.

Why order diversification matters

A firm can lose a planned input when one of its suppliers defaults. Safety stock can absorb some of that loss, while the rest becomes demand for replacement supply. A network with more buyer and supplier links spreads orders across more firms, but the resulting benefit depends on which firms default, how much each link carries, and the price of replacement supply. Birge, Capponi, and Chen study this interaction in a supply chain model with firm defaults, switched demand, and market prices. Their Theorem 5.1 asserts that a particular order-preserving form of diversification improves the network's resilience. This mission formalizes that comparison in the notation and conventions of the accepted manuscript, including its E-Companion proof.

The question is relevant to supply chain design because adding a link alone does not specify how much business moves to it. The theorem compares two networks that retain each firm's total incoming and outgoing order quantities. It therefore isolates the effect of redistributing those orders among more partners. The result concerns a precise resilience metric: the fraction of a network's baseline out-of-stock cost reduced by holding safety stock. It does not claim that diversification prevents all defaults or reduces every component of systemic loss.

Networks, defaults, and resilience

There are $N$ firms and $M$ goods. The order quantity $o^m_{ij}$ is the amount of good $m$ that firm $i$ promises to deliver to firm $j$. Good $m$ has price $p^m$. Firm $i$ has initial equity $w_i$ and a unit holding cost $\lambda_i^m$ for safety stock of good $m$. Its realized net production cost is $c_i$. Two networks $A$ and $B$ share prices, equity, holding costs, firms, and goods; their order quantities may differ. The source calls this five-part data a supply chain network, with a stock profile that is specialized here to a common scalar $\theta$ for the resilience comparison (§2, pp. 8–9; §5.1, p. 25).

A tiered network places each firm in a tier $m_i\in\{1,\ldots,M+1\}$. A positive order of good $m$ runs from tier $m$ to tier $m+1$. Tier 1 firms supply good 1, tier $M+1$ firms buy good $M$, and every intermediate firm both buys and supplies its designated goods. The undirected graph underlying positive orders is connected. The model's supplier set $U_i$ contains firms delivering good $m_i-1$ to $i$, and its buyer set $L_i$ contains firms receiving good $m_i$ from $i$ (§5.2–5.3, pp. 26–27).

For a common realization $c$ and safety stock $\theta$, the fundamental-default set $D_0(\theta)$ contains firms whose initial net worth is strictly negative:

The switched demand of firm $i$ for good $m$ is $\sigma_i^m(D_0(\theta),\theta)=\left(\sum_{k\in D_0(\theta)}o^m_{ki}-\theta\right)^+$. The inverse supply function $s_m^{-1}$ prices the aggregate replacement demand for good $m$. Firm $i$'s cost $\zeta_i(\theta)$ sums holding cost and switched-demand cost over every good. The network's resilience ratio $\zeta(\theta)$ is its aggregate reduction in this cost divided by aggregate cost at zero safety stock (§5.1, p. 25).

Formalization targets

For each firm, $B$ is more diversified than $A$ when total incoming and outgoing orders are unchanged, $U_i^A\subseteq U_i^B$ and $L_i^A\subseteq L_i^B$, and an expanded neighbor set divides orders into quantities no larger than the old quantities. Where a neighbor set is unchanged, its individual order quantities are unchanged. This is the complete condition of Definition 5.3, with the supplier good indexed as $m_i-1$ as required by §5.2.

The goal is Theorem 5.1: for two tiered networks sharing their non-order data and tier assignment,

for every admissible common safety stock $\theta$ and common realized production-cost vector $c$. The three milestones are the tier-grouped expression for total cost, its order comparison between $A$ and $B$, and equality of their zero-stock baseline costs. They are the steps of the displayed chain in the E-Companion, EC p. 18, rather than separate numbered lemmas.

What the result establishes

The theorem gives an order-sensitive comparison of the paper's out-of-stock metric. It says that, under the stated redistribution constraints, the same amount of uniform safety stock offsets at least as large a fraction of baseline cost in the more diversified network. It supports comparisons of network designs with equal firm-level order totals. It does not rank networks with different equity, prices, or holding costs, and it does not address the paper's distinct contagion-based fragility metric (§5.1–5.3).

The result is proved in the paper; the open work here is its machine-checked formalization. The definitions of tiered order networks, fundamental defaults, switched demand, and the resilience ratio give reusable interfaces for later results about the same model. The draft Lean theorems state the full result and the three intermediate targets, with proofs left for solvers. The comparison also makes the paper's indexing and cost conventions explicit so those interfaces can be audited independently.

Where the difficulty lies

The default set depends on the order network, even though the two networks use the same realized costs. Thus a cost comparison cannot begin by treating defaulted firms as an unrelated common parameter. Moreover, switched demand takes a positive part after subtracting safety stock, and the inverse supply curve is evaluated at an aggregate across firms. Merely comparing individual orders or counting more links does not determine the resulting total cost. The final resilience ratio has a baseline-cost denominator that can be zero. The formalization has to cover that boundary case as well as positive baseline cost.

Formalization scope

Firms use Fin N; goods and tiers use the paper's one-based natural-number indices. Both $N$ and $M$ are positive. Orders and holding costs are nonnegative, prices are nonnegative, and initial equity is nonnegative (the source assumes every firm is initially solvent, p. 9). A tiered network has only consecutive-tier positive orders, has activity appropriate to every firm's tier, and has a connected underlying undirected graph. The two networks share $p$, $w$, $\lambda$, the inverse supply curves, and the tier map. The source's tier-constant rerouting cost does not occur in the resilience metric and is not represented in these statements.

The paper prints Assumption 2.1 as a minimum over all firms. Since non-suppliers have zero orders, that literal reading would force $\theta=0$ and empty the theorem of its intended positive-stock content. The formalization reads the bound over actual suppliers, with $\theta\ge0$. It uses monotone inverse supply curves, as implied by Assumption 2.3, and explicitly requires their values to be nonnegative for nonnegative demand; the latter is an additional convention corresponding to nonnegative inverse supply prices. These choices appear in the definitions and in the statement audit notes.

The printed supplier-order superscript in Definition 5.3 uses $m_i$, while §5.2 says firm $i$ buys good $m_i-1$; the Lean definition uses the latter. The E-Companion's cost chain drops holding costs for goods a firm does not buy, although §5.1 sums them for all goods. The formalized cost and tier-grouped milestone retain the full sum. The paper states an almost-sure comparison under a random cost vector; its proof is pointwise, and the goal quantifies over every common realization. Each network computes its own default set. Lean sets $0/0=0$, so a zero baseline cost requires no extra positive-denominator assumption. These conventions rule out a vacuous zero-stock reading or a cost formula weakened by omitting terms.

Selected references

• J. R. Birge, A. Capponi, and P.-C. Chen, Disruption and Rerouting in Supply Chain Networks, accepted manuscript dated October 31, 2022, SSRN 3669363; Operations Research, 2023, DOI 10.1287/opre.2022.2409. The mission follows the manuscript's pagination and its E-Companion.

Motivation

Brands that sell consumer goods are held responsible by the public for the labour and safety practices of their suppliers. After the 2013 Rana Plaza collapse in Bangladesh, about 200 clothing brands and retailers signed the Accord on Fire and Building Safety and inspect roughly 1,600 factories jointly; pharmaceutical companies such as Pfizer and GSK audit their suppliers jointly through the Pharmaceutical Supply Chain Initiative (both examples from the paper, pp. 4 and 14). Two features of such supply bases matter for auditing. Competing brands often share a common supplier, so a scandal at that supplier hurts both of them. And brands compete downstream, so a scandal that hurts only a rival can help a brand.

Chen, Qi and Dawande (MSOM 2020; accepted manuscript SSRN 2889889) model two competing buyers with one common and two independent suppliers. Their Proposition 2 shows that, when each buyer audits on his own, competition drives the buyers away from the common supplier: in every equilibrium it is left unaudited. This mission formalizes their Proposition 3. It shows that a coalition that audits jointly, and splits the cost by a Shapley-value rule, does audit the common supplier and is stable. A companion mission (Supplier Centrality … I) covers Proposition 2.

Setting

Two buyers $B_1, B_2$ source from three suppliers: $B_i$ from its independent supplier $S_i$, and both from the common supplier $S_c$. Each supplier is compliant with probability $e\in(0,1)$. A non-compliant supplier that passes an audit of effort $x\in[0,1]$ (probability $1-x$) is exposed in public with probability $r\in(0,1]$. An independent supplier audited with effort $x$ therefore causes damage with probability $\lambda_I(x)=r(1-e)(1-x)$. The three suppliers offend independently.

If buyer $B_i$ has $n_i\in\{0,1,2\}$ exposed suppliers, its demand intercept falls from $\alpha$ to $\alpha-d_M$ (by $d_M>0$ once, however many offend). Each exposed supplier also raises its unit input cost from $w$ to $\hat w\ge w$. The buyers then play a Cournot game with differentiated products (substitution $\beta\in(0,1]$). Buyer $B_1$'s equilibrium profit is $\pi^b_1(n_1,n_2)=(q^*_1)^2$, where

The aggregate ex post profit is $\pi^b(i\,d_M,j\,d_M)=\pi^b_1(i,j)+\pi^b_2(i,j)$. Auditing a supplier with effort $x$ costs $K\mathbf 1\{x>0\}+\tfrac a2x^2$.

Unilateral auditing. Each buyer audits at most one of his two suppliers. $\Pi^b_i$ is buyer $B_i$'s expected profit net of his own audit costs. An equilibrium is a pair of mutual best responses in which, by the paper's tie-breaking rule, a buyer who audits strictly prefers it to not auditing. The effort $\hat e_I$ of eq. (2) is a buyer's optimal effort on his own supplier when the rival does not audit.

Joint auditing. The coalition chooses efforts $x=(e_{c1},e_{cc},e_{c2})\in[0,1]^3$ on $S_1,S_c,S_2$, auditing at most two suppliers, and pays each audited supplier's cost once. The buyers still compete downstream. With $R^b_i(x)$ the buyers' expected profits excluding audit costs, the coalition's profit is

The difference of the buyers' profits is $\Delta\Pi=R^b_1-R^b_2$. The cost shares are $\Gamma_{1,2}=\tfrac12[\text{total cost}\pm\Delta\Pi]$ (eq. (3)). The analysis assumes the scenario

Formalization targets

Goal: Proposition 3

There are thresholds $K^L_c\le K^H_c$ such that, for every $K\ge0$, an optimal joint plan

The coalition is also stable. At an optimal plan its aggregate profit is at least the buyers' aggregate profit in any unilateral equilibrium. After paying $\Gamma_i$, each buyer earns at least his profit in a symmetric unilateral equilibrium.

Milestones

The coalition's profit as a sum of unilateral profits (proof of Lemma OA9). Lemma OA9: $S_c$ beats one independent supplier, and beats no audit for $K<\hat K$. Lemma OA10: $S_c$ with $S_1$ beats $S_1$ with $S_2$. Lemma OA11: $S_1$ with $S_c$ beats $S_c$ alone for $K<\tilde K$. The fair shares (3). The case analysis with $K^L_c=\min\{\frac{\hat K+\tilde K}2,\tilde K\}$ and $K^H_c=\max\{\frac{\hat K+\tilde K}2,\hat K\}$. Stability.

Significance

The result separates two effects of downstream competition on responsible sourcing. Under unilateral auditing, a buyer gains nothing private from auditing the shared supplier: the reduction in risk accrues equally to his rival. The joint coalition removes this free-riding. The common supplier is audited whenever anything is, and the Shapley-type split (3) charges the buyer who also has his own supplier audited for the competitive advantage this gives him ($\Gamma_1>\Gamma_2$ exactly when $\Delta\Pi>0$). The paper's welfare comparison (Proposition 4) builds on this proposition and on Proposition 2.

The proof in the e-companion argues through four comparisons of candidate plans and short cost-sharing algebra. None of it is machine-checked. A formal proof fixes the model (in particular which costs the coalition pays and what "at most two suppliers" excludes) and checks each comparison. In one place it also corrects the printed claim: the per-firm stability argument is given only for the symmetric unilateral equilibrium, and it does not extend to the asymmetric one (see Formalization scope).

Difficulty

All objects are explicit polynomials in the efforts. The difficulty is in the comparisons. Lemmas OA9 and OA10 compare different audit plans through the scenario ordering of aggregate ex post profits, an assumption on the stage-2 closed form that is not implied by the standing conditions. The obvious attempt, comparing first-order conditions, fails because the coalition's profit is discontinuous at zero effort (the fixed cost) and the feasible set is not convex: "at most two of three" is a union of faces of the cube. The thresholds $\hat K$, $\tilde K$ are differences of maxima, so the case analysis has to handle ties and the boundary $K=K^H_c$ with weak inequalities. Stability needs the unilateral equilibria of Proposition 2, so the full goal reaches into the companion mission's game.

Formalization scope

• Model. Params holds $\alpha,\beta,w,\hat w,d_M,e,r,a$ with $\beta\in[0,1]$, $w\le\hat w$, $d_M>0$, $e\in(0,1)$, $r\in(0,1]$, $a>0$ and the three positivity conditions of p. 8. Every statement adds $\beta>0$ (Sec. 4.3 continues the competing case) and the p. 13 scenario as five inequalities between piAgg values. Their arguments count exposed suppliers: $\pi^b(2d_M,d_M)$ is a label, not a damage of $2d_M$.
• Expected profits are 8-outcome expectations of the closed-form stage-2 profit. The coalition's profit charges each audited supplier once, and the common supplier's damage probability under a joint audit is $r(1-e)(1-e_{cc})$.
• Thresholds $\hat K,\tilde K$ are the maxima at $K=0$ written as sSup over $[0,1]$ and $[0,1]^2$. At $K=0$ the profit is a polynomial, so these suprema are attained.
• "Yields the highest aggregate profit" is read as "some maximizer over the feasible plans has this pattern"; uniqueness is not claimed. $\Delta\Pi$ is evaluated at that maximizer (its mirror image, which audits $S_2$, has $\Delta\Pi<0$).
• Cost shares use the total cost of the plan. For plans with $e_{c2}=0$ they are the printed formulas (3).
• Unilateral benchmark. The equilibrium includes the tie-breaking rule of p. 10, and the interior-effort assumption of p. 10 is encoded as $\hat e_I<1$, with $\hat e_I$ given by eq. (2).
• Stability, corrected. Condition (b) of Sec. 4.3 (each firm earns more) is stated against symmetric unilateral equilibria only, the case the paper's proof treats. Against the asymmetric equilibrium, where one buyer audits with $\hat e_I$ and the other audits nothing, it fails. Take $\alpha=10$, $\beta=1$, $w=1$, $\hat w=3$, $d_M=\tfrac12$, $e=\tfrac1{10}$, $r=1$, $a=50$, $K=0.2$: the coalition optimally audits nothing, yet the auditing buyer earns more unilaterally than half of the coalition's profit. Condition (a) is stated against every equilibrium. "Higher" is stated as $\ge$.
• The goal's thresholds are existential and come before $\forall K$. Choosing $K^L_c=K^H_c$ does not trivialize it, because the three cases must cover every $K\ge0$. The milestone on part (2) fixes the thresholds explicitly.
• The source is the authors' SSRN accepted manuscript. Main-text page numbers equal PDF pages, and e-companion page ec$k$ is PDF page $28+k$.

Contributions welcome: proofs of Lemmas OA9–OA11, which are self-contained polynomial inequalities; existence of maximizers on the non-convex feasible set (upper semicontinuity); and the link to the unilateral equilibria needed for stability.

Selected references

• F. Chen, A. Qi, M. Dawande, Supplier Centrality and Auditing Priority in Socially-Responsible Supply Chains, Manufacturing & Service Operations Management, 2020; accepted manuscript, SSRN 2889889. https://ssrn.com/abstract=2889889
• E. L. Plambeck, T. A. Taylor, Supplier evasion of a buyer's audit: Implications for motivating supplier social and environmental responsibility, Manufacturing & Service Operations Management 18(2):184–197, 2016. https://doi.org/10.1287/msom.2015.0550
• N. Singh, X. Vives, Price and quantity competition in a differentiated duopoly, RAND Journal of Economics 15(4):546–554, 1984. https://doi.org/10.2307/2555525

Motivation

In an optimal stopping problem the value function $V$ and the gain function $G$ agree on the stopping set $D=\{V=G\}$, and $V>G$ on the continuation set $C$. The smooth fit principle says that, at the boundary $\partial C$ between them, $V$ meets $G$ with matching first derivatives. Smooth fit is one of the boundary conditions in the free-boundary problems that characterise optimal stopping boundaries. It is behind the integral equations for the early-exercise boundary of the American put and for many problems in sequential analysis and finance (Peskir & Shiryaev, 2006). On a finite horizon the value depends on the remaining time, and continuity of the time derivative $\partial_tV$ across $\partial C$ is the step that justifies the local time-space calculus applied to $V$ (Peskir, 2005).

Before De Angelis & Peskir (2020) such continuity results were proved problem by problem, or under sign conditions that the main examples do not satisfy: $G=0$ on the stopping set and $H<0$ globally, which fails for the American put. Their paper gives two general results. Theorem 8 covers the space derivative, and Theorem 15, the subject of this mission, covers the time derivative on a finite horizon. Both are stated for a strong Markov process realised as a stochastic flow, and both rest on probabilistic regularity of the boundary.

Setting

Fix a horizon $T>0$ and $d=m+1\ge1$. The process is the time-space process $X^{t,x}_s=(t+s,X^x_s)$. Its first coordinate is time, and $(X^x_s)_{s\ge0,\,x\in\mathbb R^{d-1}}$ is a stochastic flow on a probability space $(\Omega,\mathcal F,P)$ with a right-continuous filtration $(\mathcal F_s)$, adapted to it, with $X^x_0=x$. Its paths are right-continuous with left limits, it is left-continuous over stopping times, and it is strong Markov. The flow is continuous in the space variable if, outside one null set, $x\mapsto X^x_s(\omega)$ is continuous for every $s$.

Given continuous functions $\lambda\ge0$, $G$ and $H$ of $(t,x)$, write $\Lambda^{t,x}_s=\int_0^s\lambda(t+u,X^x_u)\,du$. The value function is

over stopping times $\tau$ bounded by the remaining time $T-t$. The sets are $C=\{V>G\}$ and $D=\{V=G\}$ inside $[0,T]\times\mathbb R^{d-1}$, and $\partial C=D\cap\overline C$. The problem is well posed if the expected payoffs are integrable and the first entry time $\tau_D$ into $D$ is optimal.

The first hitting time of a set $A$ is $\sigma^{t,x}_A=\inf\{s\in(0,T-t]:X^{t,x}_s\in A\}$. A point $z$ is probabilistically regular for $A$ if $P(\sigma^z_A=0)=1$. The generator $\mathbb L_X$ (2.14) acts in the space variable, with diffusion matrix $\sigma_{ij}$, drift $\mu_i$, killing rate $\lambda$ and jump measure $\nu$. Its coefficient formula is tied to the flow by the right derivative at zero of the killed spatial semigroup applied to $G(t,\cdot)$. The function $\tilde H=G_t+\mathbb L_XG+H$ appears in the hypotheses.

Formalization targets

Goal: Theorem 15, global form (p. 20)

Assume well-posedness, (5.9) ($V$ continuous on $[0,T]\times\mathbb R^{d-1}$ and $C^1$ on $C$), (5.10) ($G\in C^{1,2}$) and (5.11) (Lipschitz continuity of $\tilde H$ and $\lambda$ in $t$, uniformly in $x$), and a continuous flow. Assume the local conditions (5.12)–(5.13) and probabilistic regularity for $D^\circ$ at every $z\in\partial C$. Then

Milestones

1. (5.17): along every sequence $(t_n,x_n)\in C$ with $(t_n,x_n)\to z$, $\displaystyle\liminf_{n}V_t(t_n,x_n)\ge G_t(z)$.
2. (5.20): along the same sequences, $\displaystyle\limsup_{n}V_t(t_n,x_n)\le G_t(z)$.
3. Theorem 15, (5.14): at a single regular $z\in\partial C$,