All missions

Motivation

A two-machine flow shop is the simplest multi-stage production system: every job visits machine 1 and then machine 2, each machine works on one job at a time, and the goal is to finish all jobs as early as possible. S. M. Johnson's 1954 paper (Naval Research Logistics Quarterly 1(1):61–68, doi:10.1002/nav.3800010110) answered this question, posed by R. Bellman, with an exact rule, now called Johnson's rule. It is one of the first exact results in machine scheduling. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) the problem is written $F2\,\|\,C_{\max}$. The rule is the standard polynomial case against which the NP-hardness of the three-machine flow shop (Garey, Johnson and Sethi 1976) is contrasted, and it is still used inside heuristics for larger shops.

Timeline:

• 1954. Johnson proves the two-machine rule and a three-machine special case (the latter is the second mission of this series).
• 1976. Garey, Johnson and Sethi prove that the three-machine flow shop is NP-hard in the strong sense, so the two-machine case marks the boundary of tractability.

Setting

There are $n$ items $i = 1, \dots, n$. Item $i$ needs $A_i > 0$ units of time on machine 1 and then $B_i > 0$ units on machine 2. Each time is setup time plus work time, and the times are otherwise arbitrary. A schedule assigns start times $s^1_i$ and $s^2_i$. It is feasible when all start times are nonnegative, the intervals $[s^1_i, s^1_i + A_i]$ of distinct items do not overlap on machine 1, the intervals $[s^2_i, s^2_i + B_i]$ do not overlap on machine 2, and $s^1_i + A_i \le s^2_i$ for every item. The total elapsed time $T(s) = \max_i (s^2_i + B_i)$ is the time at which the last item leaves machine 2.

An order is a permutation $\sigma$, where $\sigma(k)$ is the item in position $k$. The as-soon-as-possible schedule $a_\sigma$ of an order processes the items in the order $\sigma$ on both machines, with no delay on machine 1. Each item starts on machine 2 as soon as it has left machine 1 and machine 2 is free.

Relation (II). Item $i$ is definitely preferred to item $j$ when

$$\min(A_i, B_j) < \min(A_j, B_i),$$

and the two items are indifferent when equality holds. An order is consistent with all the definite preferences when no item is definitely preferred to an item placed earlier.

For an order $\sigma$ the paper uses the quantities

$$K_u = \sum_{l \le u} A_{\sigma(l)} - \sum_{l < u} B_{\sigma(l)}, \qquad F(\sigma) = \max_u K_u .$$

Formalization targets

Goal: Theorem 1 (p. 63)

For positive $A, B$:

$$\exists\, \sigma \text{ consistent with (II)}, \qquad\text{and}\qquad \forall\, \sigma \text{ consistent with (II)},\ \forall\, s \text{ feasible}:\quad a_\sigma \text{ is feasible and } T(a_\sigma) \le T(s).$$

The comparison is against every feasible schedule, including those whose two machines follow different orders.

Milestones

1. Lemma 1 (p. 61). Every feasible schedule can be replaced, at no greater total elapsed time, by a feasible schedule that follows one common order on both machines.
2. As soon as possible (p. 62). For a fixed common order, $a_\sigma$ is feasible and minimizes $T$ among the feasible schedules that follow $\sigma$.
3. Closed form (p. 62). $T(a_\sigma) = \sum_i B_i + F(\sigma)$, i.e. the total idle time of machine 2 is $\max_u K_u$.
4. Adjacent interchange (p. 63). Interchanging the items in positions $j, j+1$ leaves every other $K_u$ unchanged. Moreover, $\max(K_j, K_{j+1}) < \max(K'_j, K'_{j+1})$ holds if and only if (II) holds for the pair.
5. Interchanges do not increase $F$ (p. 63). If the pair in positions $j, j+1$ satisfies (II) non-strictly, then $F(\sigma) \le F(\sigma')$.
6. Lemma 2 (p. 64). Relation (II) is transitive, except when the middle item is indifferent to both others.
7. Worked example (p. 65). For $A = (4,4,30,6,2)$ and $B = (5,1,4,30,3)$, the order $(5,1,4,3,2)$ takes 47 units with 4 units of idle time. The reversed order takes 78 units, and every order takes between 47 and 78 units.

Significance

The theorem reduces an optimization over a continuum of start-time vectors, and over $n!$ orders, to sorting with respect to a pairwise relation. The paper's working rule computes an optimal order in $O(n \log n)$ time. The two-machine rule is the building block of Johnson's three-machine result, of the Campbell–Dudek–Smith heuristic for $m$ machines, and of lower bounds in branch-and-bound methods for flow shops. The closed form $T(a_\sigma) = \sum_i B_i + \max_u K_u$ reappears across flow-shop theory as a longest-path formula.

The result is classical and proved. This mission contributes a machine-checked proof in Lean 4 against Mathlib. As far as a search of the platform shows, no formal statement of the flow-shop model or of Johnson's rule exists there. The mission also fixes a reusable Lean model of a two-machine schedule: start times, feasibility, total elapsed time and the as-soon-as-possible schedule of an order.

Difficulty

The paper's argument leaves two steps informal, and a formal proof must supply both. First, Lemma 1 is justified by a picture and the phrase "successive interchanges". The page does not show that each interchange keeps the schedule feasible and does not delay the last completion on machine 2, and this is where most of the modelling work sits. Second, relation (II) is not a strict weak order when there are ties, so the obvious sorting argument fails. Consistency on adjacent pairs does not imply optimality: the items $(A, B) = (5,2), (1,1), (2,5)$, in that order, satisfy (II) non-strictly on both adjacent pairs, yet take 13 units against an optimum of 10. Lemma 2's exception is exactly this case.

Formalization scope

Items are Fin n (0-based) and times are real numbers. Positivity $A_i > 0$, $B_i > 0$ is a hypothesis of the goal and of Lemma 1, the as-soon-as-possible step and the closed form, as on p. 61. Lemma 2 and the interchange statements are pure min/sum algebra and carry no positivity. An order is σ : Equiv.Perm (Fin n) with σ k the item in position k. Interchanging positions $j, j+1$ is σ * Equiv.swap j (j+1). The total elapsed time is Finset.univ.fold max 0 of the machine-2 completion times, so it is $0$ when $n = 0$. $K_u$ is indexed by 0-based positions (Lean's $K_u$ is the paper's $K_{u+1}$), and $F$ requires $n \ge 1$.

Conventions made explicit or corrected:

• "Consistent with all the definite preferences" is imposed on all pairs of positions $k < l$ as the non-strict inequality $\min(A_{\sigma(k)}, B_{\sigma(l)}) \le \min(A_{\sigma(l)}, B_{\sigma(k)})$. The goal also asserts that such an order exists, so its main clause is not vacuous.
• The display of $K'_u$ on p. 63 prints the upper limit $u$ on the $B'$-sum. The definition of $K_u$ on p. 62 and the reduction of (I) to (II) require $u-1$, and the formalization uses $u-1$.
• Lemma 2 keeps the page's exception (item 2 indifferent to both items); without it the statement is false.

Measuring the objective by $F(\sigma)$, or comparing only against schedules that follow one common order, would drop Lemma 1 and change the theorem. The goal compares against every feasible start-time schedule. The working rule of p. 64 (a procedure) is not formalized.

Proofs of any milestone are welcome, as are further lemmas about the as-soon-as-possible schedule and a formalization of the working rule. The schedule definitions are the basis for the three-machine mission of this series.

Selected references

• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. doi:10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. doi:10.1287/moor.1.2.117
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5:287–326, 1979. doi:10.1016/S0167-5060(08)70356-X
• H. G. Campbell, R. A. Dudek, M. L. Smith, A heuristic algorithm for the n job, m machine sequencing problem, Management Science 16(10):B630–B637, 1970. doi:10.1287/mnsc.16.10.B630

Motivation

A Markov-renewal program is a sequential decision model in which a system moves among finitely many states, the time between transitions is random and may depend on both the current and the next state, and a reward accrues during each sojourn. It generalizes the Markov decision process, where every transition takes one time unit, and is the standard model for maintenance, inventory and queueing control problems in which decisions are made at irregular epochs. W. S. Jewell introduced the model in two companion papers in Operations Research in 1963 (Part I, Part II).

Part II studies returns over an unbounded planning horizon. When the horizon is measured in number of transitions and rewards are not discounted, the expected return of a stationary policy grows linearly, and the paper's policy-improvement algorithm for this model rests on the precise form of that growth: a rate, the gain, and a state-dependent offset, the bias. Appendix A of Part II derives this asymptotic form from the Kemeny–Snell theory of finite Markov chains. This mission formalizes that derivation.

The result is the transition-counting counterpart of Howard's gain–bias analysis for Markov decision processes (R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960), and the fundamental matrix it uses is that of J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.

Setting

Fix a stationary policy. Only the embedded chain and the mean one-step rewards matter for the infinite-step undiscounted model (the paper, p. 961: these processes "depend only on the means"). The data are:

• a finite nonempty state set $S$ and a transition matrix $P = (p_{ij})_{i,j\in S}$ with $p_{ij}\ge 0$ and $\sum_j p_{ij} = 1$;
• the one-step expected rewards $\rho \in \mathbb R^S$ (the paper's (I 17));
• the terminal rewards $V(0)\in\mathbb R^S$.

The chain is ergodic (assumption 2, p. 951): $P$ is irreducible, meaning every state can be reached from every other state with positive probability. $P$ may be periodic. A stationary probability vector is $\pi\in\mathbb R^S$ with $\pi_i\ge 0$, $\sum_i\pi_i = 1$ and $\pi P = \pi$; $\Pi$ denotes the matrix every row of which is $\pi$.

The $n$-step return of the policy is the recursion (I 16) without the maximization:

$$V_i(n) = \rho_i + \sum_{j} p_{ij}V_j(n-1),\qquad n = 1,2,\ldots$$

The system gain is $G = \sum_i \pi_i\rho_i$ (A 6), the bias after $n$ steps is $W_i(n) = V_i(n) - Gn$, and the fundamental matrix is $Z = (I - P + \Pi)^{-1}$ (A 7).

Formalization targets

Goal: gain and Cesàro bias of the infinite-step return

For every irreducible row-stochastic $P$, stationary $\pi$, rewards $\rho$ and terminal rewards $V(0)$: the matrix $I - P + \Pi$ is invertible, and

$$\lim_{n\to\infty}\frac1n\sum_{m=1}^{n} W(m) = (Z - \Pi)\rho + \Pi V(0).$$

This is (A 4) with (A 5)–(A 7), in the form that is true for every ergodic chain and every terminal-reward vector.

Milestones

In order: the stationary vector exists, is unique and positive, and $\frac1n\sum_{k<n}P^k\to\Pi$ (Appendix A); the increment identity $V(n)-V(n-1) = P^{n-1}\rho$ (A 1) for constant $V(0)$; the Cesàro limit $\Pi\rho = G\mathbf 1$ of the increments (A 2); invertibility of $I-(P-\Pi)$ and the relations $PZ = ZP$, $\pi Z = \pi$, $I - Z = \Pi - PZ$; the Cesàro summability of $I+\sum_{j=1}^{n-1}(P^j-\Pi)$ to $Z$; the finite-$n$ bias formula (A 3) for constant $V(0)$; the relative-value equations $W_i + G = \rho_i + \sum_j p_{ij}W_j$ (4) for the limiting bias; and the paper's two-state machine example, where the four stationary policies have gains $70, 50, 80, 60$, the policy $(B,A)$ is optimal for every $n$ with $V_1(n) = 80n+170+(-1)^{n+1}170$, the limiting biases are $\pm170$, and the relative values of (5) are $340$ and $0$.

Stronger: aperiodic chains

If $P$ is moreover primitive (aperiodic), $W(n)$ itself converges to $(Z-\Pi)\rho + \Pi V(0)$. This is included as a supporting statement.

Significance

The asymptotic $V(n)\approx Gn + W$ is what makes average-reward policy improvement work: substituting it into the recursion yields the linear equations (4), whose solution (the relative values) is the test quantity of the paper's algorithm. The gain identifies which stationary policy earns most per transition in the long run, and the bias separates policies of equal gain. The same gain–bias decomposition underlies average-cost dynamic programming, the analysis of Markov reward processes, and the deviation matrix used in sensitivity analysis of Markov chains.

The result is classical and proved on paper. Formalizing it adds, first, a machine-checked account of the fundamental matrix of an irreducible, possibly periodic, finite chain: invertibility of $I - P + \Pi$, its algebraic relations and its Cesàro characterization. Mathlib has irreducible and primitive nonnegative matrices and row-stochastic matrices, but no stationary-vector uniqueness for irreducible chains, no Cesàro ergodic theorem for finite chains, and no fundamental matrix. Second, it fixes two slips of the printed appendix (below) with an exact statement. No machine-checked proof of this result is known.

Difficulty

The obvious argument writes $W(n) = \sum_{k<n}(P^k - \Pi)\rho + P^nV(0)$ and passes to the limit term by term. This fails for periodic chains: $P^k$ does not converge, $P^k - \Pi$ does not tend to zero, and the series $\sum_k (P^k - \Pi)$ does not converge. The paper's own example ($P$ swaps two states) is of this kind, and there $W(n)$ oscillates forever. What survives is Cesàro convergence, and establishing it needs control of all eigenvalues of $P$ of modulus one (they are simple roots of unity for an irreducible stochastic matrix) or an equivalent combinatorial argument. Invertibility of $I - P + \Pi$ requires that $1$ be a simple eigenvalue of $P$ with left eigenvector $\pi$, which is the Perron–Frobenius uniqueness statement for irreducible matrices; positivity of all entries of $P$, or a one-step Doeblin condition, is not available.

Formalization scope

States are a finite type with decidable equality and at least one element; vectors are S → ℝ, matrices Matrix S S ℝ, column vectors act by P *ᵥ v, the row vector $\pi$ by π ᵥ* P. Ergodicity is P ∈ Matrix.rowStochastic ℝ S ∧ P.IsIrreducible. The stationary vector is a hypothesis-constrained parameter (nonnegative, summing to one, $\pi P = \pi$), which is unique by the first milestone. $\Pi$, $G$ and $Z$ are definitions computed from $P$, $\pi$ and $\rho$, never free variables. Cesàro means are $\frac1n\sum_{m=1}^{n}$, equal to $0$ at $n = 0$. Mathlib's matrix inverse is $0$ on singular matrices, so the goal asserts invertibility of $I - P + \Pi$ explicitly.

Two printed slips are corrected, and the milestone texts are kept verbatim:

1. The paper's (A 4)–(A 5) have $+V(0)$ where iterating (I 16) gives $P^nV(0)$, whose Cesàro limit is $\Pi V(0)$. The goal uses $\Pi V(0)$; this is also the only form consistent with the paper's equation (4). Accordingly (A 1) and (A 3), which hold exactly when $PV(0) = V(0)$, carry the hypothesis that $V(0)$ is constant. The paper's example has $V(0) = 0$, where both readings agree.
2. The paper writes ordinary limits while noting that $P^{n-1}$ "converges or is Cesàro-summable". The goal and (A 2) are Cesàro limits; an ordinary limit is false for periodic chains.

The printed $\pi = \{\pi_1,\ldots,\pi_n\}$ uses $n$ for the number of states $N$.

A trivializing formalization is ruled out: $Z$ is not a junk inverse (invertibility is part of the goal), $\pi$ is a genuine stationary probability vector of $P$ rather than an arbitrary vector, $G$ is computed from $\pi$ and $\rho$, and the hypotheses are met by the paper's periodic two-state example.

Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, positivity, uniqueness), the Cesàro ergodic theorem $\frac1n\sum_{k<n}P^k\to\Pi$, and the fundamental matrix. These are reusable for any finite-chain average-reward result. Contributions proving any milestone, or the aperiodic variant, are welcome.

Selected references

• W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
• W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6), 938–948, 1963. https://doi.org/10.1287/opre.11.6.938
• J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• E. Seneta, Non-negative Matrices and Markov Chains, 2nd ed., Springer, 2006. https://doi.org/10.1007/0-387-32792-4

Motivation

In quantum mechanics an observable is a self-adjoint operator $A$ on a complex Hilbert space $\mathfrak H$, and the dynamics is the Schrödinger equation $i\,\tfrac{d}{dt}\psi(t) = H\psi(t)$. In finite dimensions the solution is the matrix exponential $e^{-itH}\psi(0)$, computed by diagonalizing $H$. The operators of physics (the Laplacian, Schrödinger operators with Coulomb potentials, position and momentum) are unbounded, defined only on a dense subspace, and have no eigenbasis in general. The spectral theorem is the substitute for diagonalization in this setting: it expresses every self-adjoint operator as an integral of the identity function against a family of orthogonal projections, and so gives meaning to $f(A)$ for every Borel function $f$, in particular to $e^{-itA}$ and to the spectral projections $\chi_\Omega(A)$.

The theorem goes back to Hilbert (bounded symmetric forms, 1906) and was extended to unbounded self-adjoint operators by von Neumann (1929/30), Stone (1932) and Riesz. This mission follows the treatment in G. Teschl, Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), Section 3.1: projection-valued measures, their functional calculus for bounded and unbounded functions, and the spectral theorem obtained from resolvents through the Herglotz representation of Borel transforms.

Setting

Let $\mathfrak H$ be a complex Hilbert space, with inner product $\langle\cdot,\cdot\rangle$ conjugate linear in the first argument, and let $\mathfrak L(\mathfrak H)$ be the bounded operators on it. An (unbounded) operator $A$ is a linear map defined on a subspace $\mathfrak D(A) \subseteq \mathfrak H$; $A \subseteq B$ means $B$ extends $A$. $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A^* = A$, domains included.

The resolvent set of $A$ is the set of $z \in \mathbb{C}$ for which $A - z : \mathfrak D(A) \to \mathfrak H$ is a bijection with bounded inverse, and the spectrum is its complement, $\sigma(A) = \mathbb{C} \setminus \rho(A)$.

A projection-valued measure assigns to every Borel set $\Omega \subseteq \mathbb{R}$ an orthogonal projection $P(\Omega) = P(\Omega)^* = P(\Omega)^2$ such that $P(\mathbb{R}) = \mathbb{I}$ and, for pairwise disjoint Borel sets $\Omega_n$, $\sum_n P(\Omega_n)\psi = P(\bigcup_n \Omega_n)\psi$ for every vector $\psi$ (strong, not norm, $\sigma$-additivity). Each $\psi$ gives the spectral measure $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle = \|P(\Omega)\psi\|^2$, a finite Borel measure of total mass $\|\psi\|^2$, and by polarization the complex measures $\mu_{\varphi,\psi}(\Omega) = \langle\varphi, P(\Omega)\psi\rangle$.

For a bounded Borel function $f$ the operator $P(f) = \int f(\lambda)\,dP(\lambda) \in \mathfrak L(\mathfrak H)$ is the bounded operator with $\langle\psi, P(f)\psi\rangle = \int f\,d\mu_\psi$ for all $\psi$. For an arbitrary Borel function $f$ it is the operator with domain

$$\mathfrak D_f = \Big\{\psi \in \mathfrak H \;\Big|\; \int_{\mathbb{R}} |f(\lambda)|^2\, d\mu_\psi(\lambda) < \infty\Big\}$$

and $\langle\psi, P(f)\psi\rangle = \int f\,d\mu_\psi$ for $\psi \in \mathfrak D_f$. An operator $T$ is normal if it is densely defined, $\mathfrak D(T) = \mathfrak D(T^*)$ and $\|T\psi\| = \|T^*\psi\|$ on $\mathfrak D(T)$.

Formalization targets

Goal: the spectral theorem (Theorem 3.7)

For every self-adjoint operator $A$ in $\mathfrak H$ there is a unique projection-valued measure $P_A$ with

$$A = \int_{\mathbb{R}} \lambda\, dP_A(\lambda),$$

an equality of operators including their domains. Uniqueness is among projection-valued measures, compared on Borel sets.

Milestones

• Theorem 3.1. For a projection-valued measure $P$, the map $f \mapsto P(f)$ from bounded Borel functions (sup norm) to $\mathfrak L(\mathfrak H)$ is a unital $C^*$-algebra homomorphism of norm one, $\langle P(g)\varphi, P(f)\psi\rangle = \int g^* f\, d\mu_{\varphi,\psi}$, and $P(f_n) \to P(f)$ strongly when $f_n \to f$ pointwise with $\sup_\lambda |f_n(\lambda)|$ bounded.
• Theorem 3.2. For every Borel $f$, the operator $P(f)$ with $\mathfrak D(P(f)) = \mathfrak D_f$ exists, is normal, and $P(f)^* = P(f^*)$.
• Lemma 3.5. $\alpha P(f) + \beta P(g) \subseteq P(\alpha f + \beta g)$ with domain $\mathfrak D_{|f|+|g|}$, and $P(f)P(g) \subseteq P(fg)$ with domain $\mathfrak D_g \cap \mathfrak D_{fg}$.
• Theorem 3.8. For self-adjoint $A$, $\sigma(A) = \{\lambda \in \mathbb{R} \mid P_A((\lambda-\varepsilon, \lambda+\varepsilon)) \ne 0 \text{ for all } \varepsilon > 0\}$.
• Corollary 3.9. $P_A(\sigma(A)) = \mathbb{I}$ and $P_A(\mathbb{R} \cap \rho(A)) = 0$.

A further supporting statement (not a milestone) records that $\mu_\psi$ is a finite measure with $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle = \|P(\Omega)\psi\|^2$.

Significance

The result itself. The spectral theorem is the foundation of the rest of the book and of mathematical quantum mechanics generally. Stone's theorem and the time evolution $e^{-itA}$, the min-max principle, the RAGE theorem, the decomposition of the spectrum into absolutely continuous, singular continuous and pure point parts, Weyl's theorem on essential spectra and scattering theory are all statements about $f(A)$ or $P_A(\Omega)$. Theorem 3.8 identifies the spectrum with the support of $P_A$, which is what makes spectral questions accessible to measure theory.

Formalizing it. The result is classical and fully proved in the literature. Mathlib has the continuous functional calculus for bounded normal elements of $C^*$-algebras and the finite-dimensional spectral theorem, but no projection-valued measures, no spectral integral of unbounded functions, and no spectral theorem for unbounded operators (LinearPMap). On Prove2Me the related published material is bounded or finite-dimensional (for example diagonalization of self-adjoint endomorphisms and the Fuglede–Putnam theorem). A formal proof here supplies the object $f(A)$ that every later mission of this series currently has to take as data.

Difficulty

The obvious route through the bounded case fails. For bounded self-adjoint $A$ one can build $f(A)$ from polynomials by the sup norm on $\sigma(A)$ and extend by monotone limits; for unbounded $A$ there are no polynomials in $A$ defined on a common useful domain and no sup-norm estimate. The standard reductions (the Cayley transform $(A-i)(A+i)^{-1}$, or the bounded resolvent $(A-z)^{-1}$) produce bounded normal operators whose spectral measures must then be transported back, and the domain $\mathfrak D(A)$ must be recovered exactly as $\mathfrak D_\lambda$; getting the domains right, not just the formulas on a core, is where unbounded arguments usually break. Beyond the domain issue, the projections $P_A(\Omega)$ are not given by any formula in $A$ that Mathlib can evaluate: they have to be recovered from resolvent data, which in the book's development requires the Herglotz representation of Borel transforms and the Stieltjes inversion formula for finite measures, neither of which is in Mathlib. Uniqueness is also not automatic: it requires that a projection-valued measure is determined by the operator $\int \lambda\, dP(\lambda)$ alone.

Formalization scope

$\mathfrak H$ is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since none of the stated results or their proofs in the book need it. Operators are LinearPMaps H →ₗ.[ℂ] H; self-adjointness is Mathlib's IsSelfAdjoint, which includes density. A projection-valued measure is a function Set ℝ → (H →L[ℂ] H) constrained on Borel sets only (IsProjValuedMeasure); uniqueness in the goal compares values on Borel sets. The spectral measure spectralMeasure P ψ is built with Measure.ofMeasurable from $\Omega \mapsto \|P(\Omega)\psi\|^2$. The spectral integral spectralIntegral P f is the operator with domain $\mathfrak D_f$ and quadratic form $\int f\,d\mu_\psi$ (the predicate IsSpectralIntegral), selected by choice; its existence for Borel $f$ is part of the milestone for Theorem 3.2, not an assumption. The bounded calculus boundedSpectralIntegral is characterized the same way in $\mathfrak L(\mathfrak H)$. The spectrum is the resolvent-based TeschlQM.Spectral.spectrum of Section 2.4, not Mathlib's spectrum ℂ of a Banach algebra element. In Theorems 3.8 and 3.9, $P_A$ enters as a projection-valued measure P with the hypothesis A = spectralIntegral P (fun x => x), which by the goal's uniqueness is exactly $P_A$.

Nothing is taken as data that the book derives. In particular the goal is not stated for "a projection-valued measure with $A = \int\lambda\,dP$" given as a hypothesis, and $P_A$ is not defined by choosing such a measure: the goal quantifies existentially and uniquely over projection-valued measures, with self-adjointness of $A$ as the only hypothesis.

Lemma 3.4 (spectral bases), Lemma 3.6 (the family $P_A(\Omega)$ built from the Herglotz representation) and the results of Sections 3.2–3.3 are not stated. A complete development needs finite Borel measures and $L^2$ spaces (in Mathlib), the Herglotz representation and Stieltjes inversion (the subject of the next mission of this series), and the adjoint theory of LinearPMap. The projection-valued measure and spectral-integral layer is reusable by every later mission of the series. Contributions of any milestone, of general lemmas about IsProjValuedMeasure (finite additivity, $P(\Omega_1)P(\Omega_2) = P(\Omega_1 \cap \Omega_2)$, monotonicity), and of alternative proofs of the goal are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009, Chapter 3. https://doi.org/10.1090/gsm/099
• J. von Neumann, Allgemeine Eigenwerttheorie Hermitescher Funktionaloperatoren, Mathematische Annalen 102 (1930), 49–131. https://doi.org/10.1007/BF01782338
• M. H. Stone, Linear Transformations in Hilbert Space and Their Applications to Analysis, AMS Colloquium Publications 15, 1932. https://doi.org/10.1090/coll/015
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Academic Press, 1980, Chapters VII–VIII. https://doi.org/10.1016/B978-0-12-585050-6.X5001-4

Motivation

Many controlled systems do not move in unit time steps. A machine runs for a random time before it breaks down, a repair takes a random time, a queue sits in a state until the next arrival or departure. A Markov-renewal program (in later terminology a semi-Markov decision process) models such a system: the sequence of visited states is a Markov chain controlled by the decision maker, but each transition takes a random time and earns a reward that may depend on that time. When the horizon is long and rewards are not discounted, the natural criterion is the gain rate, the long-run expected reward per unit of time, not per transition.

Howard's policy-iteration algorithm (Howard 1960) finds a policy of maximal gain per transition for finite Markov decision processes. W. S. Jewell's Markov-Renewal Programming. II (Oper. Res. 11 (1963) 949–971) extends it to the time-average criterion. The paper's Fig. 2 gives the algorithm; pp. 954–955 state its claim: the algorithm "will find an optimal stationary policy for the infinite-time, undiscounted model, in the sense that the policy will have a gain rate, $g$, which is at least as large as that obtained for any other policy". Appendix D compares Jewell's test quantity with an alternative one proposed by P. Schweitzer, and states the identity (D 3) that measures the gain-rate improvement produced by either.

Timeline. Howard (1960) introduced policy iteration for the per-transition gain of finite Markov decision processes, and sketched a semi-Markov version. Jewell (1963, Parts I and II) developed Markov-renewal programming, with the ratio test quantity of Fig. 2 for the undiscounted time-average case. Schweitzer (unpublished MIT report, cited in Appendix D) proposed the test quantity (D 1). The ratio criterion was later treated systematically for semi-Markov decision processes (e.g. Puterman 1994, Ch. 11).

Setting

There are finitely many states $i = 1, \dots, N$ and, in each state, finitely many alternatives $z$. Under alternative $z$ in state $i$ the next state is $j$ with probability $p^z_{ij}$ ($p^z_{ij} \ge 0$, $\sum_j p^z_{ij} = 1$). The transition $i \to j$ takes a random time with finite mean $\nu^z_{ij}$, and the transition out of $i$ earns an expected reward $\rho^z_i$. The mean sojourn time is $\nu^z_i = \sum_j p^z_{ij}\nu^z_{ij}$, and it is positive.

A stationary policy $z$ picks one alternative $z(i)$ in each state. Its chain has transition matrix $P^z_{ij} = p^{z(i)}_{ij}$, and $\rho_i$, $\nu_i$ denote the data of $z(i)$. The paper's standing assumption 2 is that this chain is ergodic (irreducible) for every policy. Let $\pi$ be the stationary probability vector of $P^z$ ($\pi_i \ge 0$, $\sum_i \pi_i = 1$, $\pi P^z = \pi$). The gain rate of $z$ is (B 7):

$$g = \frac{\sum_{i=1}^{N} \pi_i \rho_i}{\sum_{k=1}^{N} \pi_k \nu_k}.$$

The value-determination equations (13) of $z$ are, in the $N+1$ unknowns $g, v_1, \dots, v_N$,

$$v_i + g\,\nu_i = \rho_i + \sum_{j=1}^{N} p_{ij} v_j \quad (i = 1, \dots, N), \qquad v_N = 0.$$

The test quantity of Fig. 2 for alternative $z$ in state $i$ is $\frac{1}{\nu^z_i}\{\rho^z_i + \sum_j p^z_{ij} v_j - v_i\}$. One cycle of the algorithm solves (13) for the current policy and then chooses, in every state, an alternative that maximizes the test quantity, retaining the current alternative when it already attains the maximum. The algorithm stops when the policy does not change.

Formalization targets

Goal: Fig. 2 terminates at a policy of maximal gain rate

For every run $z_0, z_1, \dots$ of the algorithm, from any initial policy and with any choice among tied maximizers, there is $K$ with $z_{K+1} = z_K$; and whenever $z_{K+1} = z_K$, $g_K$ is the gain rate of $z_K$ and, for every stationary policy $z'$,

$$g^{z'} = \frac{\sum_i \pi'_i \rho^{z'(i)}_i}{\sum_k \pi'_k \nu^{z'(k)}_k} \;\le\; g_K .$$

Milestones

1. (12)–(13), p. 955. The equations (13) have exactly one solution, and its $g$ equals (B 7).
2. (D 3), p. 970. For policies $A$, $B$, with $\Gamma_j$ and $\gamma_j$ the changes in the test quantities (D 1) and (D 2) computed with $A$'s $(g, v)$, and $P^B_j = \nu^B_j\pi^B_j / \sum_k \pi^B_k\nu^B_k$ the time-stationary probabilities (C 12),

$$g^B - g^A = \sum_{j} \frac{\Gamma_j}{\nu^B_j} P^B_j = \sum_j \gamma_j P^B_j .$$

3. p. 955. If the test quantity indicates a change from $z_1$ to $z_2$, then $g^{z_2} > g^{z_1}$.
4. (29)–(30), p. 961. For two states with $p_{12}, p_{21} > 0$: $g = (p_{21}\rho_1 + p_{12}\rho_2)/(\nu_1 p_{21} + \nu_2 p_{12})$ and $v_1 = (\nu_2\rho_1 - \nu_1\rho_2)/(\nu_1 p_{21} + \nu_2 p_{12})$, $v_2 = 0$.

Significance

The result makes the time-average criterion computable: a finite sequence of linear solves and pointwise maximizations produces a policy whose reward per unit time is optimal among all stationary policies. The identity (D 3) is the quantitative content: it expresses the gain-rate change as an average of local improvements, weighted by the fraction of time the new policy spends in each state. Both test quantities, Jewell's (D 2) and Schweitzer's (D 1), are covered by it. When every $\nu^z_i = 1$ the model is a Markov decision process and the algorithm is Howard's.

The result is classical and has textbook proofs for semi-Markov decision processes. The paper states the proof as "elementary" and does not write it out. None of it is machine-checked on Prove2Me, and no semi-Markov or ratio-criterion result is on the platform. The mission produces a checked account of value determination for irreducible finite chains, the improvement identity, and termination of policy iteration under ties.

Difficulty

The gain rate is a ratio, so the per-transition argument for Markov decision processes does not transfer by rescaling rewards: the denominator $\sum_k\pi_k\nu_k$ changes with the policy. Comparing two policies requires weighting local improvements by the new policy's time-stationary probabilities, and a strict improvement needs those probabilities to be positive in every state, which uses irreducibility of the new policy, not only of the current one. Termination rests on the retain-on-tie rule: without it the algorithm can cycle among tied maximizers without improving. Finally, (13) has $N+1$ unknowns and $N+1$ equations only because of the normalization $v_N = 0$; its unique solvability is a statement about the kernel and range of $I - P$ for an irreducible stochastic $P$.

Formalization scope

States are Fin N with NeZero N; the paper's state $N$ is index $N-1$ (lastState N). Alternatives form a type α; the goal assumes Fintype α and Nonempty α. The model records only $p^z_{ij}$, $\nu^z_{ij} \ge 0$ and $\rho^z_i$, with $\nu^z_i > 0$ as a field. The transition-time distributions and reward functions of the paper enter the undiscounted infinite-time model only through these means, and every such choice of means is realized by some distributions, so nothing is lost. Ergodicity is Matrix.IsIrreducible of the policy matrix for every policy. Stationary vectors are nonnegative, sum to one and satisfy $\pi P = \pi$; every statement quantifies over all of them.

The gain rate is defined by its closed form (B 7). Its identification with $\lim_{t\to\infty} v_i(t)/t$ ((B 6), argued in Appendix B from renewal theory) is not part of the mission. (13) is stated with the full sum $\sum_{j=1}^N$, equal to the paper's $\sum_{j=1}^{N-1}$ because $v_N = 0$. The paper states (D 3) for a policy $A$ "which led to an improved policy $B$"; the identity holds for any two policies and is stated that way. A run of the algorithm is a relation, not a chosen argmax: the goal quantifies over every run, so the termination claim cannot be met by a particular tie-breaking. A run begins at an arbitrary policy; the "initial set of returns" entry of Fig. 2 is a run started one cycle later.

A formalization in which the improvement step already asserts optimality, or in which termination is assumed, would be trivial; here the step only asks for pointwise maximization of the test quantity, and termination is part of the conclusion.

Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, uniqueness, strict positivity), the kernel of $I - P$, and finite-policy termination arguments. These are reusable for any finite Markov decision or semi-Markov model. Proofs of any milestone, and of the $\nu \equiv 1$ specialization, are welcome.

Selected references

• W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
• W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6), 938–948, 1963. https://doi.org/10.1287/opre.11.6.938
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960. https://mitpress.mit.edu/9780262080095/
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

In network revenue management a firm sells $n$ products that consume $m$ capacitated resources over $T$ periods, and in each period it chooses which offer set of products to make available. When customers choose among the offered products according to a choice model, the standard planning tool is the choice-based linear program, which assigns a frequency $u_S\ge 0$ to every offer set $S\subseteq N$ (Liu and van Ryzin 2008). It has $2^n$ variables. Its optimal solution is what the firm actually implements: a randomization over offer sets.

For the Markov chain choice model of Blanchet, Gallego and Goyal (2016), Feldman and Topaloglu (2017) show that the choice-based program is equivalent to a reduced linear program with only $2n$ variables. The reduced program can be solved directly, but its solution is a pair of vectors $(\hat x,\hat z)$, not a randomization over offer sets. This mission formalizes the paper's Section 7, which converts the reduced solution back into a randomization over offer sets: the Dimension Reduction algorithm, and Theorem 9, which says that the algorithm produces at most $n+1$ offer sets and that these sets are nested.

Setting

Products are indexed by $N=\{1,\dots,n\}$. A customer arrives wanting product $j$ with probability $\lambda_j$. If the product she visits is offered, she buys it. Otherwise she moves to product $i$ with probability $\rho_{j,i}$, and leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$. Throughout, $\lambda_j>0$, $\rho_{j,i}\ge0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j,i$.

For an offer set $S\subseteq N$, the (Balance) equations

$$P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S$$

have a unique solution. $P_{j,S}$ is the probability that product $j$ is purchased, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. Write $P_S=(P_{j,S})_j$ and $R_S=(R_{j,S})_j$.

The set $\mathcal H$ consists of all pairs $(x,z)\in\mathbb R^n\times\mathbb R^n$ with $x,z\ge0$ and $x_j+z_j=\lambda_j+\sum_{i}\rho_{i,j}z_i$ for all $j$. The (Reduced) linear program maximizes $\sum_j T r_j x_j$ over $(x,z)\in\mathcal H$ subject to the capacity rows $\sum_j T a_{q,j}x_j\le c_q$ for each resource $q$.

The Dimension Reduction algorithm starts from the optimal solution $(\hat x,\hat z)$ of (Reduced) and sets $(x^1,z^1)=(\hat x,\hat z)$. At iteration $k$ it forms $S^k=\{j: x^k_j>0\}$. It stops with $\alpha^k=1$ if $S^k=\emptyset$. Otherwise it sets $\alpha^k=\min\{x^k_j/P_{j,S^k}: j\in S^k\}$, stops if $\alpha^k=1$, and if not updates

$$x^{k+1}_j=\frac{x^k_j-\alpha^kP_{j,S^k}}{1-\alpha^k},\qquad z^{k+1}_j=\frac{z^k_j-\alpha^kR_{j,S^k}}{1-\alpha^k}.$$

The weights are $\gamma^k=(1-\alpha^1)\cdots(1-\alpha^{k-1})\alpha^k$.

Formalization targets

Goal: Theorem 9

Let $(\hat x,\hat z)$ be optimal for (Reduced). The algorithm stops at some first iteration $K$ with $1\le K\le n+1$. At that $K$,

$$\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},\qquad \sum_{k=1}^K\gamma^k=1,\qquad S^1\supseteq S^2\supseteq\cdots\supseteq S^K .$$

Milestones

In the order the proof uses them:

1. (Balance) has a unique, nonnegative solution for every $S$ (p. 1325).
2. $P_{j,S}>0$ for $j\in S$ (p. 1325).
3. For $(\hat x,\hat z)\in\mathcal H$: $\hat z_j\ge R_{j,S_{\hat x}}$. This is Lemma 11 of the online appendix, as quoted on p. 1332.
4. For $(\hat x,\hat z)\in\mathcal H$ with nonempty support: $\alpha_{\hat x}\le1$ (p. 1332).
5. The two stopping configurations are (Balance) solutions: $S_{\hat x}=\emptyset$ gives $(P_\emptyset,R_\emptyset)$, and $\alpha_{\hat x}=1$ gives $(P_{S_{\hat x}},R_{S_{\hat x}})$ (p. 1332).
6. Lemma 8: one step of the algorithm maps $\mathcal H$ into $\mathcal H$ and removes a minimizing index from the support (p. 1333).
7. The iterates stay in $\mathcal H$, and $S^{k+1}\subseteq S^k\setminus\{j^k\}$ (pp. 1333–1334).

Significance

Theorem 9 makes the reduced program usable. Together with the equivalence of (Reduced) and the choice-based program, it produces an optimal choice-based solution that offers at most $n+1$ sets. By a basic-solution count the choice-based program has an optimal solution with at most $m+1$ nonzero offer sets. Theorem 9 bounds the number by the number of products instead, and adds a structural property: the offered sets form a chain. Each set is contained in the previous one, so the implemented policy offers a single nested sequence of assortments. The algorithm needs at most $n+1$ solutions of linear systems of size $n$. It never enumerates offer sets.

The result is proved in the paper. As far as a search of the platform and of Mathlib shows, it has not been formalized. Mathlib's Carathéodory theorem (Analysis/Convex/Caratheodory) bounds the number of points in a convex combination. It does not construct this decomposition, and it does not give nestedness. Formalizing Theorem 9 therefore requires the paper's argument: a verified, terminating peeling procedure on the polyhedron $\mathcal H$ whose output is a convex combination of (Balance) solutions indexed by a chain of sets.

Difficulty

The algorithm divides twice. Step 2 divides by $P_{j,S^k}$, which must be positive on $S^k$. Step 3 divides by $1-\alpha^k$, which must be nonzero whenever the algorithm continues. Both rest on nontrivial facts: the positivity of purchase probabilities, and the bound $\alpha\le1$ on $\mathcal H$. That bound in turn requires the comparison $\hat z\ge R_{S_{\hat x}}$. The paper proves this comparison only in its online appendix; it is a monotonicity property of the inverse of $I-\rho^\top$ restricted to the unoffered products. The update of Step 3 can make coordinates of $z$ negative unless this comparison holds, so the naive observation that "$(x^k,z^k)$ is a combination of points of $\mathcal H$" does not by itself keep the iterates in $\mathcal H$.

Termination is not a consequence of $\alpha^k<1$ alone. It needs the strict decrease of the support, which comes from choosing a minimizing index. The weights $\gamma^k$ are defined by products of the $(1-\alpha^l)$. Their sum telescopes to $1$ only because the last step has $\alpha^K=1$.

Formalization scope

Everything lives in the namespace MarkovChainChoice.DimReduction. Products are Fin n and offer sets are Finset (Fin n). The model is a structure carrying $\lambda_j>0$, $\sum_i\rho_{j,i}<1$ and, as a disclosed implicit hypothesis, $\rho_{j,i}\ge0$. The pair $(P_S,R_S)$ is chosen by Classical.epsilon among the solutions of (Balance); milestone 1 is what identifies it with the paper's unique solution. Revenues, capacities and consumptions carry no sign conditions. "Optimal for (Reduced)" means feasible and at least as good as every feasible point.

The iterates are indexed from $k=1$ as in the paper. The value at index $0$ is an unused copy of the input. "The algorithm stops at iteration $K$" is the first $K\ge1$ with $S^K=\emptyset$ or $\alpha^K=1$. Iterates after the first stop involve a division by zero, which Lean evaluates to $0$, and no statement refers to them. The termination bound $K\le n+1$ is a conclusion of the goal, not a hypothesis. The goal is about the algorithm's actual iterates, not about an arbitrary sequence that satisfies the invariants. The paper's $\subset$ and $\supset$ denote non-strict inclusion and are rendered as $\subseteq$ and $\supseteq$.

Two milestones are stated more generally than the page. The paper states the iteration invariants for the (Reduced) optimum; the Lean requires only $(\hat x,\hat z)\in\mathcal H$, which every feasible (Reduced) solution satisfies. Lemma 8's $\arg\min$ may be a set; the statement holds for every minimizer. The page contains printed slips: on p. 1332, $\hat v_j$ has numerator $\hat x_j-\alpha R_{j,S}$, and the paper writes $R_{\hat x}$ for $R_{S_{\hat x}}$. The Lean uses the correct forms, as in Lemma 8 and Step 3. None of these slips appears in a milestone quotation.

A complete development needs a small theory of M-matrices, in the form of nonnegativity of $(I-Q)^{-1}$ for substochastic $Q$, together with finite induction on supports. The comparison lemma (milestone 3) and the (Balance) existence and uniqueness result (milestone 1) are reusable across the other missions on this paper. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
• J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
• Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0169

Motivation

A buyer and a seller negotiate over a single indivisible good. Each knows what the good is worth to them but not what it is worth to the other side, and each shades their offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this as a one-shot game in which both parties submit sealed offers simultaneously and a sale takes place at a weighted average of the two offers whenever the buyer's offer is at least the seller's.

The weight $k$ is a design parameter: $k = 1$ lets the buyer set the price, $k = 0$ the seller, and $k = 1/2$ splits the difference. For values uniform on a common interval the paper computes an explicit equilibrium for every $k$ (its Example 1) and then asks the questions a designer of the rule cares about: how often does trade happen, who gains when $k$ moves, and which $k$ maximises the expected gains of the two parties together. The answers are the subject of this mission.

The example became a benchmark for bilateral trade. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) proved that no mechanism can guarantee efficient trade with two-sided private information, and that for uniform values the split-the-difference equilibrium of this game attains the largest expected gains from trade of any mechanism. The numbers $9/32$ and $\tfrac{9}{64}\bar v$ below are therefore the second-best benchmarks against which later work on the $k$-double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) measures inefficiency.

Setting

A seller with reservation price $v_s$ and a buyer with reservation price $v_b$ each know their own value. The two values are drawn independently and uniformly on $[0, \bar v]$, with $\bar v > 0$; this law, written $\mathrm{unif}(\bar v)$, is also each player's belief about the other's value ($F_s(v) = F_b(v) = v/\bar v$ in the paper).

Under the Bargaining Rule with parameter $k \in [0,1]$, the seller asks $s$ and the buyer offers $b$. If $b \ge s$ the good is sold at price $P = kb + (1-k)s$, the seller earns $P - v_s$ and the buyer earns $v_b - P$; otherwise both earn zero. Ties trade.

An offer strategy maps a value to an offer. The strategies of Example 1(a) are

$$S(v_s) = \frac{v_s}{2-k} + \frac{1-k}{2}\bar v \quad\text{for } 0 \le v_s \le \tfrac{2-k}{2}\bar v, \qquad S(v_s) \ge \text{the same expression for } \tfrac{2-k}{2}\bar v < v_s \le \bar v,$$ $$B(v_b) = \frac{v_b}{1+k} + \frac{k(1-k)}{2(1+k)}\bar v \quad\text{for } \tfrac{1-k}{2}\bar v \le v_b \le \bar v, \qquad B(v_b) \le \text{the same expression for } 0 \le v_b < \tfrac{1-k}{2}\bar v.$$

A pair $(S, B)$ with these four properties is said to have the shape of Example 1(a) (IsExample1Pair k v̄ S B). On the two inequality ranges a seller asks too much, or a buyer bids too little, for any trade to occur, so the strategy there is free apart from the bound.

For such a pair, with $(v_s, v_b) \sim \mathrm{unif}(\bar v) \otimes \mathrm{unif}(\bar v)$, the trade probability is $\Pr[S(v_s) \le B(v_b)]$ (tradeProb), and the ex ante expected profits — taken before either value is drawn, as the paper specifies on p. 843 — are

$$\pi_s = \mathbb E\bigl[\mathbf 1\{S(v_s) \le B(v_b)\}\,(kB(v_b) + (1-k)S(v_s) - v_s)\bigr],\qquad \pi_b = \mathbb E\bigl[\mathbf 1\{S(v_s) \le B(v_b)\}\,(v_b - kB(v_b) - (1-k)S(v_s))\bigr]$$

(sellerExAnte, buyerExAnte).

Formalization targets

Goal: Example 1(c)(iii), total expected profit

For $0 \le k \le 1$, $\bar v > 0$ and every pair of the shape of Example 1(a),

$$\pi_s + \pi_b = \frac{\bar v}{16}(1+k)(2-k),$$

and as a function of $k \in [0,1]$ this total attains its maximum $\tfrac{9}{64}\bar v$ at $k = 1/2$. The goal is the paper's efficiency statement: among these equilibria, splitting the difference maximises expected group profit.

Milestones

1. Example 1(b). $\Pr[S(v_s) \le B(v_b)] = \dfrac{-k^2 + k + 2}{8}$, with maximum $9/32$ at $k = 1/2$.
2. Example 1(c)(i). $\pi_s(k) = \dfrac{\bar v}{48}(2-k)^2(1+k)$, strictly decreasing in $k$ on $[0,1]$.
3. Example 1(c)(ii). $\pi_b(k) = \dfrac{\bar v}{48}(1+k)^2(2-k)$, strictly increasing in $k$ on $[0,1]$.

The goal is the sum of milestones 2 and 3 together with a one-variable maximisation; milestone 1 describes the trade region over which both profits are integrated.

Significance

The formulas answer the design question for the rule. Moving $k$ toward the buyer's offer makes the price rule look more favourable to the seller, yet milestone 2 shows the seller's equilibrium profit falls and milestone 3 shows the buyer's rises: the paper (p. 844) uses this to show that an intuition which ignores the players' strategic response is mistaken. The comparison with truthful offers, which would trade with probability $1/2$ and earn expected group profit $\bar v/6$, quantifies the cost of strategic misrepresentation: at best $9/32$ and $\tfrac{9}{64}\bar v$.

The paper states these results as "straightforward computations" and prints no derivation. As far as is known, none of them has a machine-checked proof. A formalization settles the constants against the exact strategies of Example 1(a), including the non-linear no-trade branches the paper allows, and provides a worked example of computing trade probabilities and expected payoffs under a product of uniform laws, reusable for other double-auction and bilateral-trade examples.

Difficulty

The computation is elementary on paper, but the equilibrium strategies are only partly specified: on the seller's high range and the buyer's low range the offers are arbitrary functions subject to a bound, and need not be measurable. The obvious approach — substitute the linear formulas and integrate — is valid only after showing that these free branches never trade, so that the trade event and both integrands agree almost everywhere with their linear versions. The resulting integrals are over a product of two conditioned Lebesgue measures, not over Lebesgue measure on the plane, and the trade region depends on $k$ through both strategies. The monotonicity claims hold only on $[0,1]$ (the seller's cubic is not monotone on $\mathbb R$), and the derivative of each profit vanishes at an endpoint of the interval.

Formalization scope

Values are real numbers; the uniform law on $[0, \bar v]$ is Lebesgue measure conditioned on the interval (volume[|Icc 0 v̄]), and the joint law of $(v_s, v_b)$ is the product measure, with pairs ordered $(v_s, v_b)$. The trade probability is the real number (P {p | S p.1 ≤ B p.2}).toReal; the profits are Bochner integrals over the product. Ties trade. The results are ex ante, not conditional on a player's own value. Every theorem assumes $0 \le k \le 1$ and $\bar v > 0$. Maxima are stated with IsMaxOn on $[0,1]$ plus the value at $k = 1/2$; monotonicity with StrictAntiOn/StrictMonoOn on $[0,1]$.

The statements do not assume that $(S, B)$ is an equilibrium; they are computations about any pair of the shape of Example 1(a). That this pair is an equilibrium is Example 1(a) itself, the goal of a companion mission. No measurability of $S$ or $B$ is assumed: the free branches never trade, so each integrand agrees almost everywhere with a bounded measurable function and the integrals are the paper's expectations. A formalization that assumes $S$ and $B$ linear everywhere, or that integrates over a single uniform variable, proves a different statement.

A complete development needs: the reduction of the trade event and the integrands to their linear versions on $[0,\bar v]^2$; Fubini for the product of conditioned measures; evaluation of polynomial integrals over a triangle; and elementary calculus on cubics. Lemmas on integrating over products of uniform laws are reusable. Contributions of intermediate lemmas, such as the explicit trade region, are welcome.

Selected references

• K. Chatterjee and W. Samuelson, Bargaining under Incomplete Information, Operations Research 31(5):835–851, 1983. https://doi.org/10.1287/opre.31.5.835
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• M. A. Satterthwaite and S. R. Williams, Bilateral Trade with the Sealed Bid k-Double Auction: Existence and Efficiency, Journal of Economic Theory 48(1):107–133, 1989. https://doi.org/10.1016/0022-0531(89)90120-8
• W. Leininger, P. B. Linhart and R. Radner, Equilibria of the Sealed-Bid Mechanism for Bargaining with Incomplete Information, Journal of Economic Theory 48(1):63–106, 1989. https://doi.org/10.1016/0022-0531(89)90121-X

Motivation

The Russian option of Shepp and Shiryaev pays its holder, at an exercise time of their choosing, the running maximum of the stock price, discounted, with no fixed maturity. It is the standard example of a perpetual lookback option, and its value is a model problem of optimal stopping for a two-dimensional Markov process (the price and its running maximum). Perpetual contracts are simple to analyse but economically unrealistic: every real contract ends. Canadization (Carr, Randomization and the American put, Rev. Financial Stud. 11, 1998, https://doi.org/10.1093/rfs/11.3.597) replaces a fixed maturity by an independent exponential time $\eta(\lambda)$. The holder must exercise before $\eta(\lambda)$; if they have not, they are paid the claim evaluated at $\eta(\lambda)$. Because the exponential law is memoryless, the problem stays time-homogeneous and its value can be computed in closed form, while it approximates a contract of finite expected life $1/\lambda$.

Avram, Kyprianou and Pistorius (AKP04) solved both the perpetual and the Canadized Russian problem when the log-price is a spectrally negative Lévy process: a process with stationary independent increments whose only jumps are downward. This covers Brownian motion with drift, the Black–Scholes model, and jump-diffusions with downward jumps (crashes). Their answer is written with the scale functions $W^{(q)}$, $Z^{(q)}$ of the process. This mission is the third of three drawn from that paper, and formalizes the Canadized problem (§7, Theorem 3).

Timeline. Shepp and Shiryaev (1993) solved the Russian option for geometric Brownian motion. Carr (1998) introduced Canadization for the American put. Kyprianou and Pistorius (Ann. Appl. Probab. 13, 2003) studied perpetual options through fluctuation theory; §7 of [AKP04] builds on their calculations. Avram, Kyprianou and Pistorius (2004) solved the perpetual and Canadized problems for general spectrally negative Lévy processes.

Setting

Let $(\Omega,\mathcal F,\mathbf F=\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a filtered probability space with $\mathbf F$ right-continuous, and let $X=\{X_t\}_{t\ge0}$ be a spectrally negative Lévy process adapted to $\mathbf F$: $X_0=0$, paths càdlàg with no upward jumps and not monotone, increments $X_{s+t}-X_s$ stationary and independent of $\mathcal F_s$. The standing assumption is that $X$ has unbounded variation, or bounded variation and a Lévy measure $\Lambda(dx)\ll dx$.

The Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$. Fix $r\ge0$ with $\psi(1)=r$, and let $\mathbb P^1$ be the Esscher measure, $d\mathbb P^1/d\mathbb P|_{\mathcal F_t}=e^{X_t-rt}$.

For $q\ge0$ the $q$-scale function $W^{(q)}:\mathbb R\to[0,\infty)$ vanishes on $(-\infty,0]$, is continuous on $(0,\infty)$, and satisfies $\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=(\psi(\theta)-q)^{-1}$ for $\theta>\Phi(q)$, where $\Phi(q)$ is the largest root of $\psi(\theta)=q$. Further, $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(y)\,dy$. All scale functions in this mission are those of $(X,\mathbb P)$.

Starting from $Y_0=z\ge0$ (the paper's $\mathbb P^1_{-z}$), the reflected process is $Y_t=\overline X_t-X_t$, where $\overline X_t=\max\{0,\sup_{u\le t}(-z+X_u)\}$ and the position is $-z+X_t$. Its passage time above $k$ is $\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}$.

Let $\alpha>0$, and let $\eta(\lambda)$ be an exponential random variable of rate $\lambda>0$ which under $\mathbb P^1$ is independent of $\mathcal F_\infty$. The Canadized Russian problem (32) is

$$w^{CR}(z)=\sup_\tau\ \mathbb E^1_{-z}\Big[e^{-\alpha(\tau\wedge\eta(\lambda))+Y_{\tau\wedge\eta(\lambda)}}\Big],$$

over all $\mathbb P^1$-a.s. finite $\mathbf F$-stopping times $\tau$. Write $p=\alpha+\lambda+r$.

Formalization targets

Goal: Theorem 3

With

$$\kappa_*=\inf\{x\ge0:\ Z^{(p)}(x)-pW^{(p)}(x)\le-\lambda/(p-\lambda)\},\qquad h(z)=\frac{(p-\lambda)e^zZ^{(p)}(\kappa_*-z)}{p}+\frac{\lambda e^z}{p},$$

for every $z\ge0$:

$$w^{CR}(z)=h(z),$$

and $\tau_{\kappa_*}$ is a $\mathbb P^1$-a.s. finite $\mathbf F$-stopping time attaining the supremum. The statement covers every variation regime at once.

Milestones

In attack order:

1. Lemma 2 (i), which gives the monotonicity behind $\kappa_*$.
2. Corollary 1 (29), the value of stopping at $\tau_k$ at discount rate $\alpha+\lambda$.
3. The elimination of $\eta(\lambda)$ (display after (32)):

$$\mathbb E^1_{-z}\big[e^{-\alpha(\tau\wedge\eta)+Y_{\tau\wedge\eta}}\big]=\mathbb E^1_{-z}\Big[e^{-(\alpha+\lambda)\tau+Y_\tau}+\lambda\int_0^\tau e^{-(\alpha+\lambda)t+Y_t}dt\Big].$$

4. The Itô identity (34).
5. The expected $d\overline X$-integral up to $\tau_k$.
6. Lemma 3 (33), the value of $\tau_k\wedge\eta(\lambda)$.
7. Lemma 4, with two misprints corrected.
8. The supermartingale property of $U_t=e^{-(\alpha+\lambda)t}h(Y_t)+\lambda\int_0^te^{-(\alpha+\lambda)u+Y_u}du$.
9. The identity $h(z)=e^z+(p-\lambda)e^z\int_0^{\kappa_*-z}W^{(p)}\ge e^z$.

Significance

The result. Theorem 3 gives the price and the optimal exercise rule of a Russian option with random (exponential) maturity, for every spectrally negative Lévy model at once. It makes three things explicit. The optimal rule is a threshold rule for the reflected process $Y$. The threshold $\kappa_*$ is the crossing point of one explicit function of the scale functions. Whenever $W^{(p)}(0+)\ge(p-\lambda)^{-1}$ (possible only with bounded variation), immediate exercise is optimal. Because scale functions are known in closed form for many models, including Brownian motion with drift and hyper-exponential jump-diffusions (§8 of the paper), the theorem produces explicit prices.

Formalizing it. The result is proved on paper. It is not formalized in any proof assistant, and none of its infrastructure is available in Lean. This mission produces:

• a path-level definition of spectrally negative Lévy processes;
• scale functions defined as definite descriptions;
• the reflected process and its passage times;
• the Esscher change of measure as data;
• a continuous-time optimal stopping problem with an independent random horizon, valued in $[0,\infty]$.

A machine-checked proof would also check the verification argument, which the paper states in detail only for the unbounded-variation case.

Difficulty

The obvious route is to compute the value of every threshold rule (Lemma 3) and optimize over $k$. That identifies the right candidate, but it does not show that no other stopping time does better. The verification step needs two things for all regimes of $W^{(p)}(0+)$: that $U$ is a supermartingale, and that $U$ stopped at $\tau_{\kappa_*}$ is a martingale. For processes of bounded variation, $h$ is only continuous, not $C^1$, at $\kappa_*$, so a smooth Itô formula does not apply directly. Computing the expected $d\overline X$-integral up to $\tau_k$ uses excursion theory of $Y$ away from $0$, which Mathlib does not have. Eliminating $\eta(\lambda)$ is easy only if $\eta$ is independent of the whole filtration. If it is independent of $X$ alone, a stopping time could depend on $\eta$.

Formalization scope

• Conventions. Time is $[0,\infty)$ (ℝ≥0) and values are real. Random times take values in WithTop ℝ≥0, and the payoff is $0$ on $\{\tau=\infty\}$. Expectations of nonnegative payoffs are lower Lebesgue integrals in $[0,\infty]$, and $w^{CR}$ is an extended-real supremum, so no expectation defaults to $0$. Equalities with a real right-hand side also assert finiteness.
• Readings of informal words.
  • "The usual conditions" means right-continuity of $\mathbf F$, without completeness. Completing $\mathcal F_0$ with $\mathbb P$-null sets would contradict the Esscher relation, since $\mathbb P^1$ and $\mathbb P$ are typically singular on $\mathcal F_\infty$.
  • "Unbounded variation" means "not almost surely of bounded variation on compacts". (AC) is stated through jumps.
  • "ψ(v) < ∞" means integrability of $e^{vX_1}$.
  • "Decreases monotonically" means strictly decreasing, and "the unique root" means unique on $[0,\infty)$.
  • $W^{(p)}(0+)$ is the right limit.
  • "Almost surely finite" and the law and independence of $\eta(\lambda)$ are all under $\mathbb P^1$, where independence is from $\mathcal F_\infty$. "Parameter $\lambda$" is the rate.
  • $\mathbb P^1_{s,x}$ is encoded pathwise through the reflected process with $Y_0=s-x$.
  • The elimination of $\eta$ is stated τ by τ, which implies the page's equality of suprema.
  • The supermartingale claim, derived on the page in the unbounded-variation case, is stated for all cases.
  • Corollary 1's discount rate is renamed $a$.
  • (34) is stated as $pA+B=e^{s-x}+C$ with $A$, $B$, $C$ finite.
• Definition choices. Scale functions are defined by choice from their defining property, never as hypotheses on an arbitrary function. $W^{(q)}$ for $q<0$ is the series (5), not the tilting formula of Remark 4. $\mathbb P^1$ is a measure given with the Esscher relation. $d\overline X_t$ is the Lebesgue–Stieltjes measure of the running-maximum path.
• Corrected misprints. Lemma 4 is printed with $p^{-1}$ and $-\lambda/p$. The definition of $\kappa_*$ (p. 233) and the proof of Theorem 3 (p. 235) require $(p-\lambda)^{-1}$ and $-\lambda/(p-\lambda)$, and the printed version is false when $p^{-1}\le W^{(p)}(0+)<(p-\lambda)^{-1}$. The corrected statement is formalized.
• Ruled out. A supremum over stopping times of a filtration containing $\sigma(\eta)$, or a real-valued supremum or Bochner expectation that could be $0$ by default, would trivialize the goal or change it. The admissible class is every $\mathbb P^1$-a.s. finite stopping time of the given filtration, of which $\eta$ is independent. Replacing the goal by the $\eta$-free rewriting would state milestone 3 as if it were Theorem 3.
• Needed and reusable. A complete development needs Lévy process theory, scale functions, fluctuation identities for the reflected process, optional stopping in continuous time, and Itô or change-of-variable formulas for semimartingales with jumps. The Lévy-process, scale-function and reflected-process definitions are shared with the other two missions of the series and are reusable in ruin theory and queueing. Proofs of any milestone, and sorry-free facts about the definitions, are welcome.

Selected references

• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
• P. Carr, Randomization and the American put, Rev. Financial Stud. 11(3), 597–626, 1998. https://doi.org/10.1093/rfs/11.3.597
• L. A. Shepp, A. N. Shiryaev, The Russian option: reduced regret, Ann. Appl. Probab. 3, 603–631, 1993. https://doi.org/10.1214/aoap/1177005715
• A. E. Kyprianou, M. R. Pistorius, Perpetual options through fluctuation theory, Ann. Appl. Probab. 13, 1077–1098, 2003. https://doi.org/10.1214/aoap/1060202835
• J. Bertoin, Lévy Processes, Cambridge University Press, 1996.