Operations Research

Why this question matters

In a strategic game, each player evaluates a change in their own strategy using that player's own payoff. These incentives need not point in a common direction. A potential game is a case in which one real-valued function records every player's payoff change under a unilateral deviation. This common function lets questions about incentives be expressed as questions about one object on the space of strategy profiles. Monderer and Shapley's 1996 paper introduced several kinds of potential and gave a local characterization of the exact kind. The characterization is the subject of this mission.

The local test matters because the defining condition appears to require finding an unknown potential on the entire profile space. Theorem 2.8 says that a condition on four-step cycles already determines whether such a function exists, even when individual strategy sets are infinite. The paper compares this characterization with the familiar idea that a conservative field has zero integral around closed curves; here the “integral” is a finite sum of payoff changes along unilateral deviations (Monderer and Shapley, pp. 130–131).

Games, deviations, and path sums

Let $N$ be a finite set of players. For each player $i\in N$, let $Y^i$ be a strategy set, and let $Y=\prod_{i\in N}Y^i$ be the set of pure strategy profiles. The payoff of player $i$ is a function $u^i:Y\to\mathbb R$. If $y\in Y$, the notation $(y^{-i},x)$ means the profile obtained by replacing only player $i$'s strategy with $x\in Y^i$. The strategy sets themselves are not required to be finite in this section of the paper (p. 127).

An exact potential is a function $P:Y\to\mathbb R$ such that, for every $i$, every opponents' profile $y^{-i}$, and every $x,z\in Y^i$,

$$u^i(y^{-i},x)-u^i(y^{-i},z) =P(y^{-i},x)-P(y^{-i},z).$$

A game admitting such a function is an exact potential game. The paper uses the shorter term “potential game” for this class when the adjective is clear (pp. 127–128, equation (2.2)).

A path $\gamma=(y_0,\ldots,y_L)$ is a sequence in which each step changes exactly one player's strategy to a different value. Write $i_k$ for the unique player who moves from $y_{k-1}$ to $y_k$. The path sum of the payoff vector $u$ is

$$I(\gamma,u)=\sum_{k=1}^{L} \bigl(u^{i_k}(y_k)-u^{i_k}(y_{k-1})\bigr).$$

The path is closed when $y_0=y_L$. It is simple closed when, in addition, the vertices $y_0,\ldots,y_{L-1}$ are pairwise distinct. Its length is $L$, the number of steps and the number of vertices before the final return. These definitions follow pp. 128, 130–131.

Formalization targets

Theorem 2.8: four equivalent conditions

For a game with finitely many players, Theorem 2.8 asserts the equivalence of all four claims:

$$\begin{aligned} &\Gamma\text{ has an exact potential};\\ &I(\gamma,u)=0\quad\text{for every finite closed path }\gamma;\\ &I(\gamma,u)=0\quad\text{for every finite simple closed path }\gamma;\\ &I(\gamma,u)=0\quad\text{for every simple closed path }\gamma\text{ of length }4. \end{aligned}$$

The last condition is a local criterion, but the goal keeps the full four-way equivalence of the published theorem, p. 131. The milestone list follows five claims in its Appendix A proof: vanishing path sums from a potential, path independence, construction of a potential from vanishing closed-path sums, the local exchange of two different players' moves, and the reduction from all closed paths to length-four simple cycles (pp. 138–139).

Related results in the same development

Corollary 2.9 expresses the length-four test directly as a zero sum of payoff changes around four corners obtained by varying two players' strategies. Lemma 2.7 says that two exact potentials for the same game differ by one additive constant. Both are included as supporting statements from the same definition layer, although they are not milestones in the attack path for Theorem 2.8 (pp. 130–131).

What the result provides

Theorem 2.8 turns existence of a global function into a test on local cycles. Corollary 2.9 makes those cycles visible in payoff tables: fixing all but two players, the alternating sum around each two-player rectangle must vanish. For finite strategy sets this gives a direct finite collection of conditions; for infinite strategy sets the theorem remains a mathematical characterization without claiming a finite algorithm (Monderer and Shapley, p. 131).

The original paper proves these statements. The formalization work is to represent games, paths, path sums, and the four-way equivalence in Lean, then supply machine-checked proofs. The present mission contains compiled statements with open proofs. Its definition modules are also reusable for the paper's other results about potentials, improvement paths, and congestion games.

Where the proof is difficult

The challenging direction is that zero sums on simple length-four cycles force zero sums on every closed path. A closed path may repeat vertices and may involve more than two players. A direct appeal to the local condition does not cover such a path. The Appendix A argument uses changes to a path's sequence of deviators, and its informal treatment of adjacent moves by the same player leaves a boundary case: the two moves can cancel, so replacing them by one move would create a null step, which the definition of a path excludes. A formal proof must account for this case while preserving the paper's exact statement (pp. 138–139).

Formalization scope

Lean represents the finite player set by a finite type $\iota$ and a profile by a dependent function $y:\prod_{i:\iota}Y^i$. Strategy sets $Y^i$ remain arbitrary types. The operation $(y^{-i},x)$ is a one-coordinate update. A finite path stores $L+1$ vertices and its deviator at each of the $L$ steps; the step condition determines that deviator uniquely. Closed paths of length zero are allowed and have sum zero. The paper prints $n$, the number of players, as the upper limit of the path sum on p. 130, although its summands are indexed by path steps. The Lean definition sums over all $L$ steps, as the surrounding definition and later equations require.

The four-cycle hypothesis quantifies only over simple closed paths of exactly four genuine steps. It is not replaced by all four-step walks or by cycles with null or simultaneous deviations. The goal retains all four clauses rather than only its shortest equivalence. Corollary 2.9 explicitly requires the two varying players to be distinct; this is implicit in the paper's four-corner construction. No finite-strategy assumption is imposed on Theorem 2.8, Corollary 2.9, or Lemma 2.7.

The development needs ordinary finite sums, dependent functions, coordinate updates, and finite-indexed paths. Its path and potential definitions are intended as an interface for later work. Contributions proving any of the five source-backed milestones, the goal, or the two related statements are within scope.

Selected references

• Dov Monderer and Lloyd S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. DOI: 10.1006/game.1996.0044.

Motivation

A job shop is the basic model of a factory floor in which every job follows its own route through the machines. Minimizing the time at which the last job is finished (the finish time, or makespan) is one of the central problems of deterministic scheduling theory, and the question of which special cases admit efficient algorithms has organized much of the field since the 1950s.

For two machines the picture is sharp. Jackson (1956) showed that a two-machine job shop in which every job has at most two operations is solved by a simple rule extending Johnson's flow-shop algorithm (Jackson, Naval Research Logistics Quarterly 3, 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 105). Once a single job may have three operations, the non-preemptive problem becomes NP-complete: Lenstra, Rinnooy Kan and Brucker showed this for $n-1$ jobs with one nonzero task each and one job with three (Annals of Discrete Mathematics 1, 1977; a 1975 Mathematisch Centrum report is the paper's reference [1]). Gonzalez and Sahni (Operations Research 26(1), 1978) extended this boundary to preemptive schedules, in which a task may be interrupted and resumed later: even then the two-machine problem is NP-complete, already when only two jobs have three nonzero tasks. This mission formalizes that reduction, Lemma 5 together with Corollary 2 of their paper.

Timeline:

• 1956: Jackson, two-machine job shop with at most two operations per job, solved in $O(n\log n)$.
• 1975/1977: Lenstra, Rinnooy Kan and Brucker, the non-preemptive two-machine job shop NP-complete with $n-1$ one-task jobs and one three-task job.
• 1976: Garey, Johnson and Sethi, the non-preemptive two-machine job shop NP-complete even when problem size is measured by the sum of the task lengths (Mathematics of Operations Research 1, 1976).
• 1978: Gonzalez and Sahni, the preemptive two-machine job shop NP-complete (Lemmas 5 and 6), and the non-preemptive case again by the same reduction (Corollary 2).

Setting

A job shop has processors $P_1, \dots, P_m$ and jobs $1, \dots, n$. Job $i$ is a finite sequence of tasks; task $j$ of job $i$ must be processed on a given processor $k$ for $t_{k,i,j} \ge 0$ time units, and for every job, task $j \ge 2$ can begin only after task $j-1$ has been completed. Schedules start at time $0$. A preemptive schedule assigns to every task a finite set of time intervals $[s, f)$ on its processor, of total length $t_{k,i,j}$, such that intervals on the same processor do not overlap and every interval of task $j$ begins after task $j-1$ of the same job is completed. A non-preemptive schedule processes each task in a single interval. If $f_i(S)$ is the time at which job $i$ is completed, the finish time is $\mathrm{FT}(S) = \max_i f_i(S)$.

PARTITION: a multiset $\{a_1, \dots, a_n\}$ of nonnegative integers has a partition if some index set $u$ satisfies $\sum_{i \in u} a_i = \tfrac12 \sum_{i=1}^n a_i$.

From $a_1, \dots, a_n$, with $T = \sum_i a_i$, the paper builds the two-processor job shop $\mathrm{JS}$ with $n+2$ jobs:

• job $i \le n$: tasks $(P_2, a_i)$, $(P_1, a_i)$;
• job $n+1$: tasks $(P_1, T/2)$, $(P_2, T/2)$, $(P_1, 3T)$;
• job $n+2$: tasks $(P_2, 3T)$, $(P_1, T/2)$, $(P_2, T/2)$.

Each processor carries load exactly $5T$. In Lean, the instance is JS a : JobShopLTAS.Core.Instance 2 (n + 2), a schedule is S : Schedule (JS a) (a finite set of pieces), and the predicates are S.IsPreemptive, S.IsNonPreemptive and S.FinishedBy (5 * T a).

Formalization targets

Goal: Lemma 5 and Corollary 2

For every $n$ and every $a : \mathrm{Fin}\,n \to \mathbb N$,

$$\bigl(\exists\, S \text{ preemptive},\ \mathrm{FT}(S) \le 5T\bigr) \iff \mathrm{Partition}(a) \quad\text{and}\quad \bigl(\exists\, S \text{ non-preemptive},\ \mathrm{FT}(S) \le 5T\bigr) \iff \mathrm{Partition}(a).$$

Milestones

1. Lemma 5(a): a partition yields a non-preemptive schedule of finish time exactly $5T$ (the paper's Figure 3).
2. Observations (i)–(ii) in the proof of Lemma 5(b): in any preemptive schedule with $\mathrm{FT} \le 5T$, task $t_{2,n+1,2}$ is completed by $2T$ and $t_{2,n+2,1}$ by $4T$; no part of $t_{1,n+1,3}$ runs before $T$ and no part of $t_{1,n+2,2}$ before $3T$.
3. Lemma 5(b): without a partition, every preemptive schedule has $\mathrm{FT} > 5T$.
4. Lemma 5: the preemptive equivalence.
5. Corollary 2: the non-preemptive equivalence.

Significance

The result places the boundary of tractability for two-machine job shops exactly: at most two operations per job is solvable in $O(n\log n)$, while two jobs with three operations make the problem NP-complete, and allowing preemption does not help. The same instance serves both schedule types, because its optimum is $5T$ in either model exactly when a partition exists.

The theorem is classical and fully proved on paper; no machine-checked proof is known to exist. Formalizing it requires a precise model of preemptive schedules, which the paper treats informally, and makes explicit an argument (the "no idle time" step of Lemma 5(b)) that the paper compresses into a few sentences. The schedule model built here is shared with the other job-shop missions of this series.

Difficulty

Direction (a) is a concrete schedule and is bookkeeping. Direction (b) is the substance. The tempting argument "each processor has load $5T$, so a schedule of finish time $5T$ has no idle time, hence some set of short jobs fills exactly $[0, T/2]$ on $P_2$" is incomplete for preemptive schedules: the short jobs may be split into many pieces spread over the whole horizon, and $U$, the set of short jobs that touch $P_1$ during $[0, T]$, is defined by pieces rather than by whole tasks. Making the counting argument rigorous requires measuring idle time on each processor across arbitrary finite unions of intervals and tying the amount of processing done on $P_1$ before $T$ to the completed first tasks on $P_2$.

Formalization scope

• Processing times are real numbers; the PARTITION data are natural numbers cast to $\mathbb R$; $T$ is the real sum. Processors are Fin 2 with $P_1 = 0$, $P_2 = 1$; jobs and tasks are 0-based, so the paper's job $n+1$ is job n and job $n+2$ is job n + 1.
• Job-shop data reuse the published JobShopLTAS.Core.Instance. Schedules are finite sets of pieces (task, start, end) with positive length, following the paper's footnote 1 (p. 40). A task of length zero has no pieces and is completed when its predecessor is; it never blocks a processor.
• A non-preemptive schedule is a preemptive one with at most one piece per task. "Finish time $\le \tau$" is ∀ j, S.jobFinish j ≤ τ; "finish time $> 5T$" is the existence of a job finishing after $5T$; "finish time $5T$" in Lemma 5(a) is $\le 5T$ together with a job finishing at exactly $5T$.
• Complexity wording not formalized. "Partition $\alpha$ preemptive JOFT" and "Partition $\alpha$ nonpreemptive JOFT" (polynomial reducibility), "NP-complete", and Lemma 6 ("JOFT is in NP") are not stated. What is stated is the equivalence that the paper's proofs establish for the instance they construct, with the explicit constant $\tau = 5T$.
• The PARTITION condition is written $2\sum_{i\in u} a_i = \sum_i a_i$ in $\mathbb N$, avoiding truncated division.
• A trivializing formalization is ruled out: the schedule notion requires every task to receive its full processing time, so the empty schedule is feasible only when $T = 0$ (and then the empty index set is a partition), and the finish-time bound is over every job, so no statement holds by an unattained supremum or a default value.
• Welcome contributions: a proof of Lemma 5(a) by an explicit piece schedule; infrastructure for measuring busy and idle time of a processor in a finite piece schedule, reusable for Lemma 7 (mission 4) and the preemptive flow-shop missions; the proof of Lemma 5(b).

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• M. R. Garey, D. S. Johnson, R. Sethi, Complexity of Flow Shop and Job Shop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• J. R. Jackson, An Extension of Johnson's Results on Job Lot Scheduling, Naval Research Logistics Quarterly 3(3), 201–203, 1956. https://doi.org/10.1002/nav.3800030307
• R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.

Motivation

Convex programs with inequality constraints arise when a decision must meet capacity, resource, or performance limits. Their Lagrange multipliers assign a price to each constraint. Finding an optimal multiplier gives a dual certificate and can guide a primal optimization method. Classical quadratic multiplier methods update these prices through a particular penalty. Eckstein's 1993 paper places a broader family of multiplier updates inside the theory of Bregman proximal point algorithms, allowing a nonquadratic function to shape each step (Eckstein 1993, §4.2).

The result here concerns the inequality constrained case, where multiplier vectors must be componentwise nonnegative. Eckstein identifies a monotone conjugate that incorporates this restriction into the primal penalty and proves that the resulting multiplier sequence converges to an optimal multiplier when one exists. The paper also studies primal limit points and the behavior when no optimal multiplier exists (Eckstein 1993, Theorem 7 and proof, pp. 216–219).

Setting

Let $C\subseteq\mathbb R^n$ be closed, nonempty, and convex. Let $f,g_1,\ldots,g_m$ be proper lower semicontinuous convex functions, finite on $C$. The primal problem is to minimize $f(x)$ over $x\in C$ subject to $g_i(x)\le 0$ for every $i$. Write $g(x)=(g_1(x),\ldots,g_m(x))$. A point solves the problem only when it lies in $C$, satisfies every inequality, and has no larger objective value than any other feasible point.

For a nonnegative multiplier $p$, the dual functional is $d(p)=\inf_{x\in C}\{f(x)+\langle p,g(x)\rangle\}$; it equals $-\infty$ outside the nonnegative orthant. A multiplier $p^*$ is optimal when it maximizes $d$. The standing assumption that $d$ is not identically $-\infty$ makes this dual functional a meaningful proper concave object (Eckstein 1993, p. 215).

A Bregman function $h$ has an open zone $S$. It is continuously differentiable there, strictly convex and continuous on $\overline S$, and satisfies the boundedness and sequential conditions of Definition 1. Its Bregman distance is $D_h(u,v)=h(u)-h(v)-\langle\nabla h(v),u-v\rangle$, with $u\in\overline S$ and $v\in S$. The zone contains the strict positive orthant, and the image of its gradient contains that orthant. Its monotone conjugate is $h^{*+}(z)=\sup_{p\ge0}\{\langle p,z\rangle-h(p)\}$. Lemma 3 establishes that this function is finite and differentiable everywhere under these assumptions (Eckstein 1993, pp. 205, 215–216).

Given positive step sizes $c_k$ bounded away from zero, recursion (11) chooses $x^{k+1}$ as a minimizer over $C$ of $f(x)+c_k^{-1}h^{*+}(\nabla h(p^k)+c_kg(x))$, then sets $p^{k+1}=\nabla h^{*+}(\nabla h(p^k)+c_kg(x^{k+1}))$. The theorem assumes an infinite sequence conforming to these recursions; it does not assert that each minimizer exists for arbitrary data.

Formalization targets

Multiplier convergence

The goal is Eckstein's Theorem 7. If the dual problem has an optimal multiplier, then the multiplier sequence converges to one:

$$\exists p^*\in\operatorname*{argmax}d\quad\text{such that}\quad p^k\longrightarrow p^*.$$

When every $g_i$ is continuous on $C$ and $S$ contains the closed nonnegative orthant, each subsequential limit of the primal iterates solves the constrained problem. Under the same zone condition, the multiplier sequence is unbounded if the dual has no optimal multiplier. The printed theorem says “if (10) has no solution” in this last clause; its proof on p. 218 establishes the no-optimal-multiplier condition, which is the version formalized here.

Supporting targets

The milestones include the representations of $h^{*+}$ in Lemma 2, the appendix results governing recession directions and the monotone conjugate, Lemma 3's global finiteness and differentiability, the subdifferential chain rule, and the Bregman proximal point result of Theorem 1. They also capture the paper's claims that recursion (11) is a Bregman proximal point run for $\partial(-d)$ and that primal limit points meet the feasibility, complementarity, and Lagrangian conditions.

Significance

The theorem supplies a convergence guarantee for nonquadratic methods of multipliers with inequality constraints. It separates the dual conclusion, which uses the strict positive orthant condition, from the primal limit and unboundedness conclusions, which additionally require the closed orthant to lie in the zone. This distinction lets a Bregman function whose zone excludes boundary points still yield dual convergence when optimal multipliers exist (Eckstein 1993, Theorem 7, pp. 216–218).

Eckstein proved this theorem on paper. The mission asks for machine checked proofs of its precise statements and the supporting results; the draft statements compile but their proofs remain open. A completed development would also provide reusable finite dimensional infrastructure for extended-real convex functions, monotone conjugates, Bregman distances, and convex-analytic multiplier conditions.

Difficulty

A direct appeal to ordinary proximal point convergence does not identify the update in (11) as a proximal step: the primal minimization uses $h^{*+}$, whereas the operator of interest is the subdifferential of the negative dual functional. The nonnegative orthant also introduces boundary behavior absent from the equality constrained case. The link requires precise conjugacy and subdifferential statements, including a globally finite monotone conjugate, before Theorem 1 can apply (Eckstein 1993, pp. 215–218). For primal limit points, the issue is to pass from optimality of each primal subproblem to feasibility, complementarity, and minimization of the limiting Lagrangian.

Formalization scope

Lean uses finite dimensional real inner product spaces for the general proximal point theorem and EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m) for the primal and multiplier spaces. Functions that the paper regards as extended-valued are represented by EReal; their properness excludes $-\infty$. The infimum defining $d$ and the supremum defining $h^{*+}$ remain extended-real operations, so an infinite value cannot silently become zero. Real values are extracted from $h^{*+}$ in recursion (11) only because Lemma 3 asserts finiteness everywhere.

The real function $h$ is total in Lean but constrained only on $\overline S$; its gradient is evaluated only at points in $S$. Every multiplier iterate is explicitly in $S$. The initial primal value $x^0$ is unused by recursion (11). The Bregman proximal point recursion is represented by its equivalent inclusion (4), and a “limit point” is a subsequential limit. The sequential condition (vi) of Definition 1 is stated for $x^k\in\overline S$, the natural first-argument domain of $D_h$. The Appendix's essential strict convexity means strict convexity on convex subsets of the subdifferential domain. Its recession direction uses the stated limit inferior condition.

Lemma A4's printed unconditional claim that its composite $G$ is proper lacks a finite-value witness. The formal statement keeps convexity of $G$ unconditional and states properness at a point $x_0$ where all inner functions and the outer function are finite; differentiability of the outer function there is expressed with local finiteness of its extended-real value. At a zero coefficient, its corresponding subgradient term contributes zero without requiring a subgradient to exist. These conditions expose rather than hide the domain issue. The formulation rules out an arbitrary multiplier sequence, an all-space supremum, or a minimization over infeasible points. Contributions proving the milestones, improving shared convex analysis libraries, and checking the boundary conventions are welcome.

Selected references

• Jonathan Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 202–226, 1993. DOI:10.1287/moor.18.1.202.

Motivation

A backward stochastic differential equation (BSDE) prescribes the value $\xi$ of a process at a terminal time $T$ and asks for an adapted process $Y$ that reaches it while following a given drift $f$. Adaptedness forces a second unknown $Z$, the integrand of a martingale term. Pardoux and Peng (1990) proved that Lipschitz BSDEs are well posed. BSDEs then became a standard language for stochastic control, for pricing and hedging in mathematical finance, and for probabilistic representations of semilinear parabolic PDEs.

Many such problems carry a constraint. The value of an American option must stay above its exercise payoff, and the value of an optimal stopping problem must stay above the reward for stopping now. El Karoui, Kapoudjian, Pardoux, Peng and Quenez (1997) introduced the reflected BSDE: the solution is kept above a given obstacle $S$ by an increasing process $K$ that acts only when the constraint binds. This mission formalizes the paper's first main result, existence and uniqueness of the reflected BSDE, together with the estimates its proof rests on.

Setting

Let $B=(B^1,\dots,B^d)$ be a $d$-dimensional standard Brownian motion on a probability space $(\Omega,\mathcal F,P)$. Let $(\mathcal F_t)$ be its natural filtration, augmented by the $P$-null sets. Fix a horizon $T$. The data are:

• a terminal value $\xi$, $\mathcal F_T$-measurable with $E\xi^2<\infty$ (condition (i));
• a coefficient $f(t,\omega,y,z)$ such that $f(\cdot,y,z)$ is progressively measurable with $E\int_0^Tf(t,y,z)^2dt<\infty$ (ii), and $|f(t,y,z)-f(t,y',z')|\le K(|y-y'|+|z-z'|)$ almost surely for some $K>0$ (iii);
• an obstacle $S$, continuous and progressively measurable, with $E\sup_{t\le T}(S_t^+)^2<\infty$ (iv),

with the standing assumption $S_T\le\xi$ a.s.

A solution is a triple $(Y,Z,K)$ of progressively measurable processes, valued in $\mathbb R$, $\mathbb R^d$ and $\mathbb R_+$, such that

$$Y_t=\xi+\int_t^Tf(s,Y_s,Z_s)\,ds+K_T-K_t-\int_t^T(Z_s,dB_s),\qquad 0\le t\le T\quad\text{(vi)},$$

$Y_t\ge S_t$ (vii), and $K$ is continuous and nondecreasing with $K_0=0$ and $\int_0^T(Y_t-S_t)\,dK_t=0$ (viii). Condition (viii) says that $K$ increases only when $Y$ touches $S$. The integrability conditions are (v), $E\int_0^T|Z_t|^2dt<\infty$, and (v′), $E\sup_{t\le T}Y_t^2<\infty$ and $EK_T^2<\infty$.

Formalization targets

Goal: Theorem 5.2

Under (i)–(iv) and $S_T\le\xi$, the reflected BSDE with (v)–(viii) has a solution, and any two solutions satisfying (v)–(viii) coincide:

$$\exists\,(Y,Z,K)\ \text{solving (v)–(viii)},\qquad (Y,Z,K),(Y',Z',K')\ \text{solving (v)–(viii)}\ \Rightarrow\ Y\equiv Y',\ K\equiv K',\ Z=Z'\ dP\otimes dt\text{-a.e.}$$

Milestones, in the order the proof uses them

1. Lemma 2.1: the deterministic Skorohod problem $y=x+k\ge0$ has a unique solution, with $k_t=\sup_{s\le t}x_s^-$.
2. Proposition 2.2: $K_T-K_t=\sup_{t\le u\le T}\big(\xi+\int_u^Tf\,ds-\int_u^T(Z_s,dB_s)-S_u\big)^-$.
3. Corollary 3.3 (α): (v) implies (v′).
4. Proposition 2.3: $Y_t=\operatorname{ess\,sup}_{v\in\mathcal T_t}E\big[\int_t^vf\,ds+S_v1_{\{v<T\}}+\xi1_{\{v=T\}}\mid\mathcal F_t\big]$.
5. Proposition 3.5: the a priori estimate $E(\sup Y^2+\int|Z|^2+K_T^2)\le C\,E(\xi^2+\int f(t,0,0)^2+\sup(S^+)^2)$.
6. Proposition 3.6: the stability estimate in $(\xi,f,S)$.
7. Corollary 3.7: uniqueness under (v).
8. Proposition 5.1: well-posedness of the backward reflection problem, the case where $f=f(t)$ does not depend on $(y,z)$.

Significance

Theorem 5.2 is the foundation of the theory of reflected BSDEs. With it, the solution gives the value of a mixed optimal stopping problem (Proposition 2.3). For concave $f$ it gives the value of a combined stopping and control problem, and in a Markovian setting it gives the unique viscosity solution of the obstacle problem for a semilinear parabolic PDE. The other two missions of this series formalize those consequences, and both use the existence and uniqueness proved here. The model has many later extensions (two obstacles and Dynkin games, jumps, quadratic growth), and the pricing of American options under constrained or nonlinear dynamics is formulated through it.

The result is classical and fully proved in the paper. As far as is known, no machine-checked proof of existence for a (reflected or plain) BSDE exists. The remaining work is the formalization of the known proof: the Skorohod lemma, the optimal-stopping representation, the a priori and stability estimates, and the Picard contraction. The milestones are reusable well beyond this paper, in particular the Skorohod lemma, the estimates, and the identification of the reflected solution with a Snell envelope.

Difficulty

The natural first idea is to treat (vi) as a forward equation and reflect it pathwise with the Skorohod map, as in forward reflected SDEs. This fails: the pathwise reflection of a backward equation produces a process $K$ that is not adapted (Proposition 2.2 gives $K$ as a supremum over the future). The adaptedness of $(Y,K)$ comes only from the choice of $Z$, i.e. from a martingale representation. Any construction must produce $Z$ and $K$ together, and the estimates must control the contribution of $K$ using only the minimality condition (viii). In the formal setting, Mathlib has Brownian motion, filtrations, stopping times and conditional expectations, but no stochastic integral (the platform definition Peng1990.SMP.IsItoIntegral supplies one, without any calculus), no Itô formula, no martingale representation, no Burkholder–Davis–Gundy inequality and no Snell envelope theory in continuous time.

Formalization scope

The Lean development builds on the published definitions Peng1990.SMP.Stochastic: standard $d$-dimensional Brownian motion, $\mathbb H^2$ as L2F, and the $L^2$ Itô integral IsItoIntegral. It commits to the following conventions:

• time is ℝ≥0, with $T:\mathbb R_{\ge0}$, and only $t\le T$ matters;
• the filtration is the natural Brownian filtration joined with the $\sigma$-algebra of $P$-null sets;
• $\mathbb H^2$ uses progressive rather than predictable measurability;
• $|z|$ is the Euclidean norm on $\mathbb R^d$;
• the stochastic integral is the $L^2$ Itô integral with a version continuous on $[0,T]$. Since that integral is only defined for $Z\in\mathbb H^2$, the predicate for (vi)–(viii) contains (v), which is a recorded deviation for Proposition 2.2;
• (vi)–(viii) hold almost surely, simultaneously for all $t\in[0,T]$;
• the integral $\int(Y-S)\,dK$ is taken against the Stieltjes measure of the path of $K$;
• moments are lower Lebesgue integrals in $[0,\infty]$;
• the essential supremum is a predicate on the candidate;
• uniqueness of $Z$ is $dP\otimes dt$-almost everywhere.

Proposition 2.3 additionally assumes $S\in\mathcal S^2$, which the paper's Remark 3.2 allows without loss of generality, so that every conditional expectation in it is of an integrable variable. The constants of Propositions 3.5 and 3.6 are quantified before the Brownian dimension, probability space, data and solution, and depend only on $(T,K)$; a per-solution constant would make both statements trivial. The condition $S_T\le\xi$ is part of every statement, since without it no solution exists. Proposition 3.1 and Corollary 3.3 (β) are not posed.

A complete proof needs Itô's formula for $Y^2$, the Burkholder–Davis–Gundy inequality, Gronwall's lemma, martingale representation for the Brownian filtration, and the Snell envelope with its Doob–Meyer decomposition. Each of these is reusable on its own, and contributions of any of them are welcome, as are proofs of individual milestones.

Selected references

• N. El Karoui, C. Kapoudjian, É. Pardoux, S. Peng, M. C. Quenez, Reflected solutions of backward SDE's, and related obstacle problems for PDE's, Ann. Probab. 25(2), 1997, 702–737. https://doi.org/10.1214/aop/1024404416
• É. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems & Control Letters 14, 1990, 55–61. https://doi.org/10.1016/0167-6911(90)90082-6
• N. El Karoui, S. Peng, M. C. Quenez, Backward stochastic differential equations in finance, Math. Finance 7(1), 1997, 1–71. https://doi.org/10.1111/1467-9965.00022

Motivation

Actuaries, reliability engineers and demographers ask how much longer an item or a person will live given that it has already survived to a great age $t$. For a lifetime $X$ with distribution function $F$, this is the law of the residual life time $X - t$ given $X > t$, and the question is what this law looks like as $t \to \infty$. Balkema and de Haan (Ann. Probab. 2 (1974) 792–804) determined all possible limit laws of the suitably normed residual life time and the distribution functions attracted to each. When only a scale normalization is allowed, the possible continuous limits are the exponential law and the Pareto-type laws $\Gamma_\alpha$, the counterparts in residual-life theory of the Gumbel and Fréchet laws of extreme value theory. Both theories rest on Karamata's theory of regular variation (de Haan 1970).

Section 5 of the paper restates the domain of attraction of $\Gamma_\alpha$ in terms of moments: weak convergence of the scaled residual life times is equivalent to convergence of a single conditional moment of the scaled residual life. For an exponential limit the analogous link between weak convergence and first moments had been studied by Meilijson (1972). Moment conditions of this form underlie the mean-excess and Hill-type diagnostics used in heavy-tail statistics and in the peaks-over-threshold method (Pickands 1975).

Setting

Let $X$ be a real random variable with law $\mu$ and distribution function $F$, and write $R(x) = 1 - F(x) = P\{X > x\}$ for its tail. The standing assumption is $F(x) < 1$ for every real $x$, i.e. $R(x) > 0$: $X$ has no finite upper endpoint, and conditioning on $\{X > t\}$ makes sense for every $t$.

For $t > 0$, the conditional distribution function of $X/t$ given $X > t$ is

$$P\Big\{\frac{X}{t} \le x \,\Big|\, X > t\Big\} = \frac{P\{t < X \le xt\}}{P\{X > t\}},$$

which vanishes for $x \le 1$. For a real exponent $\xi$, the conditional $\xi$-th moment is

$$E\Big(\Big(\frac{X}{t}\Big)^{\xi}\,\Big|\,X > t\Big) = \frac{1}{P\{X>t\}}\int_{(t,\infty)} \Big(\frac{y}{t}\Big)^{\xi} dF(y).$$

For $\alpha > 0$ the limit law $\Gamma_\alpha$ is $\Gamma_\alpha(x) = 1 - (1+x)^{-\alpha}$ for $x \ge 0$ and $\Gamma_\alpha(x) = 0$ for $x < 0$. The shifted function $\Gamma_\alpha(x-1)$ equals $1 - x^{-\alpha}$ for $x \ge 1$: the Pareto law of index $\alpha$ on $[1,\infty)$. The distribution function $F$ is in the domain of residual life time attraction $D_r(\Gamma_\alpha)$ when

$$\lim_{t\to\infty} P\Big\{\frac{X}{t} \le x \,\Big|\, X > t\Big\} = \Gamma_\alpha(x-1) \qquad \text{for all } x > 0 .$$

In Lean the tail is BalkemaDeHaan.LimitTypes.tail; the scaled conditional distribution and moment are BalkemaDeHaan.Moments.scaledResidualCDF and BalkemaDeHaan.Moments.condMoment. The limit law is BalkemaDeHaan.ParetoBounds.GammaLaw.

Formalization targets

Goal: Theorem 8(a), corrected

For $F(x) < 1$ for all $x$ and $0 < \xi < \alpha$:

$$F \in D_r(\Gamma_\alpha) \iff \int_0^\infty y^\xi\, dF(y) < \infty \ \text{ and } \ \lim_{t\to\infty} E\Big(\Big(\frac{X}{t}\Big)^{\xi}\,\Big|\,X > t\Big) = \Big(1 - \frac{\xi}{\alpha}\Big)^{-1}.$$

Milestones

1. The identity in the proof of Theorem 8(a): for $x > 0$, with a finite $\xi$-th moment,

$$\frac{\int_x^\infty y^\xi dF(y)}{x^\xi(1-F(x))} = \xi\,\frac{\int_x^\infty y^{\xi-1}(1-F(y))\,dy}{x^\xi(1-F(x))} + 1,$$

the left side being $E((X/x)^\xi \mid X > x)$. 2. The value of the limit: $\int_0^\infty x^\xi\, d\Gamma_\alpha(x-1) = (1-\xi/\alpha)^{-1}$ for $0 < \xi < \alpha$. 3. The "only if" half: $F \in D_r(\Gamma_\alpha)$ implies a finite $\xi$-th moment and convergence of the conditional moment to $(1-\xi/\alpha)^{-1}$. 4. The "if" half, corrected: the converse.

Significance

The theorem replaces a distributional limit, required at every $x > 0$, by one numerical limit, for any order $\xi \in (0,\alpha)$. In statistics this justifies testing or estimating heavy-tail behaviour through empirical conditional moments above a high threshold, and it identifies the limit value $(1-\xi/\alpha)^{-1}$, from which $\alpha$ can be read off. Combined with Theorem 4 of the same paper ($D_r(\Gamma_\alpha) = D(\Phi_\alpha)$), it gives a moment criterion for the Fréchet domain of attraction of extreme value theory.

The result is classical and proved, by reduction to Karamata's theorem on integrals of regularly varying functions. No machine-checked proof is known. Mathlib has no theory of regular variation, no Karamata theorem and no domains of attraction, so a formal proof also produces a reusable piece of the theory of regularly varying tails: the direct and converse halves of Karamata's integral theorem for tails of probability laws.

Difficulty

Both directions pass through the asymptotics of $\int_x^\infty y^{\xi-1}R(y)\,dy$ against $x^\xi R(x)$. The direct half requires uniform control of $R(tx)/R(t)$ over $x \in (1,\infty)$ to exchange the limit $t\to\infty$ with an integral over an unbounded range; pointwise convergence of the tail ratio alone does not dominate the integrand. The converse half must recover regular variation of $R$ from the behaviour of a single integral functional, and here the limit value matters: the page's hypothesis that the limit merely exists does not identify $\alpha$ (see below), so an argument that never uses the value $(1-\xi/\alpha)^{-1}$ cannot succeed.

Formalization scope

• The law of $X$ is μ : Measure ℝ with IsProbabilityMeasure μ; $F(x) < 1$ for all $x$ is ∀ x, 0 < μ (Set.Ioi x). All conditional quantities divide by μ (Set.Ioi t), which this hypothesis keeps nonzero.
• "$\int_0^\infty y^\xi dF(y)$ is finite" is IntegrableOn (fun y => y ^ ξ) (Set.Ioi 0) μ (real power on positive bases). In the "only if" half it is part of the conclusion, never an assumption; Lean's value $0$ for a non-integrable Bochner integral therefore cannot make the statements hold trivially. Milestone 1 asserts integrability of $y^{\xi-1}R(y)$ on $(x,\infty)$ as well.
• "$\lim_{t\to\infty}$" is Tendsto … atTop along real $t$; the limit form of $D_r(\Gamma_\alpha)$ is required for every $x > 0$, as printed (the limit $\Gamma_\alpha(x-1)$ is continuous, so this is weak convergence). The goal uses this explicit form, the one given after "i.e." on the page, not a separate definition of $D_r$.
• $\int_0^\infty x^\xi d\Gamma_\alpha(x-1)$ is the integral against a probability measure whose distribution function (ProbabilityTheory.cdf) is $x \mapsto \Gamma_\alpha(x-1)$; milestone 2 asserts such a measure exists and computes the moment for every such measure.
• Corrected statement. The source is the published article (Annals of Probability, DOI 10.1214/aop/1176996548). As printed, the "if" direction asks only that $c = \lim E((X/t)^\xi \mid X>t)$ exist and be finite. That is false: the tail $R(x) = x^{-\beta}$ for $x \ge 1$, with $\beta > \xi$ and $\beta \ne \alpha$, has a finite $\xi$-th moment and $E((X/t)^\xi\mid X > t) = (1-\xi/\beta)^{-1}$ for all $t \ge 1$, but its limit law is $\Gamma_\beta(x-1)$. The goal and milestone 4 require $c = (1-\xi/\alpha)^{-1}$, the value the page itself states in "Then $c = (1-\xi/\alpha)^{-1}$". The "only if" direction is exactly the page's.
• No hypothesis beyond the page is added; $\alpha > 0$ follows from $0 < \xi < \alpha$.

A complete development needs regularly varying functions, uniform convergence (or Potter bounds) for regularly varying tails, and Karamata's integral theorem with its converse; all are reusable beyond this mission. Proofs of the milestones, of these general tools, and of the Pareto moment computation are welcome.

Selected references

• A. A. Balkema and L. de Haan, Residual life time at great age, Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
• L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970 (Theorem 1.2.1 and Remark 1.2.1).
• N. H. Bingham, C. M. Goldie and J. L. Teugels, Regular Variation, Cambridge University Press, 1987. https://doi.org/10.1017/CBO9780511721434
• I. Meilijson, Limiting properties of the mean residual lifetime function, Annals of Mathematical Statistics 43 (1972), 354–357. https://doi.org/10.1214/aoms/1177692729
• J. Pickands III, Statistical inference using extreme order statistics, Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003

Motivation

A lifetime observed only after it has survived to a high age is described by its residual life: the additional time until failure, conditional on survival so far. Reliability analysis asks whether these conditional distributions settle into a stable shape after scaling and shifting. Extreme-value theory asks a related question about the largest observation in a large independent sample. Balkema and de Haan identify an exact connection between these questions for the exponential residual-life limit and the Gumbel maxima limit in Theorem 3 of their 1974 article. The connection lets one recognize the asymptotic form of old-age lifetimes from the domain of attraction of sample maxima, provided the lifetime distribution has no finite upper endpoint.

The article studies several residual-life limits. This mission isolates its exponential case, where the limiting conditional excess has distribution function $\Pi(x)=1-e^{-x}$ for $x\ge0$. The other continuous family $\Gamma_\alpha$ and the paper's discrete limits have separate hypotheses and attraction domains; they are outside this theorem.

Setting

Let $X$ have a probability distribution function $F$ on $\mathbb R$, and let its survival function be $R(x)=\Pr(X>x)=1-F(x)$. For a threshold $t$ with $R(t)>0$, the residual-life distribution function is

$$F_t(x)=\Pr(X-t\le x\mid X>t)=\frac{\Pr(t<X\le t+x)}{R(t)}.$$

It is zero for $x<0$. The class $D_0$ consists of the distributions with $R(x)>0$ for every real $x$. This says that the upper endpoint is infinite and makes $F_t$ meaningful at every threshold.

A law $F$ belongs to the domain of residual-life attraction $D_r(G)$ when $F\in D_0$ and there are a positive scale $a(t)$ and a shift $b(t)$ such that $F_t(b(t)+xa(t))$ converges weakly to $G(x)$ as $t\to\infty$. The shift here acts on $X-t$, the residual lifetime. Weak convergence means convergence at every continuity point of the limiting distribution function; it does not require convergence at a jump.

For maxima, $F$ belongs to the domain of attraction $D(G)$ if there are sequences $a_n>0$ and $b_n$ for which $F(a_nx+b_n)^n$ converges weakly to $G(x)$ as $n\to\infty$. The power is the distribution function of the maximum of $n$ independent observations after the indicated normalization. The relevant limit laws are the exponential residual-life law and the Gumbel law:

$$\Pi(x)=\begin{cases}0,&x<0,\\1-e^{-x},&x\ge0,\end{cases}\qquad \Lambda(x)=e^{-e^{-x}}\quad(x\in\mathbb R).$$

These definitions and formulas come from the introduction and §2 of the published article, printed pages 792–793 and 798.

Formalization targets

Theorem 3: the exact domain identity

The goal is the identity stated on printed page 798:

$$D_r(\Pi)=D(\Lambda)\cap D_0.$$

Both inclusions are required. In particular, membership in the maxima domain alone is insufficient: the maximum of a sample can have a Gumbel limit even when the underlying distribution has a finite upper endpoint, while residual life cannot be conditioned on survival beyond that endpoint. The $D_0$ condition is therefore part of the mathematical claim.

Supporting targets

The milestone list follows the statements used in the article's treatment of Theorem 3: the convergence-of-types remark on page 795; Lemma 3's asymptotic ratio $R(x-0)/R(x+0)\to1$; the tail criterion $nR(b_n+xa_n)\to e^{-x}$ associated with Gumbel attraction; the inclusion $D(\Lambda)\cap D_0\subseteq D_r(\Pi)$; and the passage from this tail limit on $x>0$ to all $x\in\mathbb R$. The last step retains the same normalization sequences. The article presents the criterion in one direction and relies on its converse at the end; the formal milestone records both directions with the same sequences.

Significance

The identity translates a conditional limit at a moving high threshold into a classical maxima-domain statement. A theorem about sample extremes can therefore characterize whether normalized remaining lifetime is asymptotically exponential. Conversely, observing exponential residual-life attraction determines a Gumbel maxima limit once the tail normalization is extended across the real line. The condition $D_0$ marks exactly where the conditional lifetime exists; omitting it would misstate the equivalence.

The article proves the result mathematically. The Lean targets here provide a precise representation of its distributions, normalizations, and limiting claims, with Theorem 3 still posed for formal proof. A complete development would add proofs of the supporting tail and convergence-of-types statements, then establish both inclusions. The definitions of weak convergence at continuity points, survival functions, and attraction domains can also support later formalizations of the paper's Pareto and discrete cases.

Difficulty

The simple comparison $F(a_nx+b_n)^n\approx e^{-nR(a_nx+b_n)}$ only relates the two limits after a suitable normalization is already available. The reverse direction starts with conditional residual-life convergence indexed by real thresholds, whereas maxima attraction needs a sequence indexed by integers. Sampling thresholds must preserve the tail asymptotics despite possible atoms. More seriously, the residual-life statement initially yields the required scaled-tail convergence only for positive arguments. The maxima limit must hold on the whole real line. A proof confined to that half-line cannot establish $D(\Lambda)$; the continuation across its left boundary is the central difficulty highlighted by the article on printed pages 798–799.

Formalization scope

Lean represents $F$ as the cumulative distribution function of a probability measure on $\mathbb R$ and uses real-valued probabilities of intervals for $R$ and $F_t$. The residual-life denominator is positive wherever $D_r$ is asserted. The extrema normalization is indexed by natural numbers, while the residual-life normalization is indexed by real thresholds. The scale is positive at every index; only large indices affect the limit. Weak convergence is encoded at every continuity point of the limit. As $\Pi$ and $\Lambda$ are continuous, their particular domain conditions amount to convergence at every real argument.

The paper uses two shift conventions: $F_t(b(t)+xa(t))$ shifts $X-t$, while the scaled-tail expressions $R(b_n+xa_n)$ shift $X$. Each statement uses the convention of its source passage. The convergence-of-types remark makes explicit the antitonicity and right-continuity of its limiting tails and states its identity where both arguments lie in the half-line on which convergence is known. Gnedenko's criterion is formalized as an equivalence: the printed sentence states the forward implication, and the conclusion of Theorem 3 uses the converse. The page-799 expression $R(b(t)+xa(t))/(t)$ has a missing $R$ in the denominator; the formal statement uses the intended $R(t)$, consistent with conditional probability and with equation (11). These choices prevent a zero-denominator quotient or an out-of-domain limit identity from trivializing a target. In particular, $D_0$ is part of the definition of $D_r(G)$: without it a law with a finite upper endpoint would have $R(t)=0$ for large $t$, the conditional distribution would be the junk quotient $0/0=0$, and the domain would be mis-specified. In Lemma 3 the limit $G$ is the distribution function of a probability measure, assumed continuous on all of $\mathbb R$.

The development needs measure-theoretic cumulative distributions and interval probabilities, filters for limits, and real exponential identities. The domain definitions and scaled-tail predicate are reusable beyond this theorem. Contributions that prove the stated milestones, or supply general lemmas about weak convergence and normalized tails, fit the scope.

Selected references

• A. A. Balkema and L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2(5), 792–804 (1974). DOI: 10.1214/aop/1176996548.
• B. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44(3), 423–453 (1943). DOI: 10.2307/1968974.

Residual life at great age

A component that has survived to age $t$ has a residual life time $X - t$, and in reliability, actuarial work and the analysis of excesses over high thresholds the question is what its conditional law looks like when $t$ is large. Balkema and de Haan (Ann. Probab. 2 (1974), 792–804) answered this in full generality: after an affine normalization, the only possible limit laws are the exponential law $\Pi$, the Pareto-type laws $\Gamma_\alpha$, and a two-parameter family of discrete laws $\Pi_{p,c}$. The continuous half of their classification became the Pickands–Balkema–de Haan theorem behind the peaks-over-threshold method of extreme-value statistics. The discrete half is less known, and this mission treats it: Theorem 5 of the paper (§3, p. 800) describes exactly which lifetimes are attracted to $\Pi_{p,c}$.

Discrete limits appear only when the normalization is allowed both a scale and a shift. They describe lifetimes that live, asymptotically, on a lattice-like set of ages whose spacing grows geometrically, with a fixed fraction of survivors failing at each lattice point.

The source is the published article in The Annals of Probability (DOI 10.1214/aop/1176996548); page numbers below are the journal's.

Setting

Let $X$ be a real random variable with law $\mu$, distribution function $F$ and tail $R(x) = 1 - F(x) = P\{X > x\}$, and assume $F(x) < 1$ for every $x$. The residual life distribution function at age $t$ is (1), p. 792,

$$F_t(x) = P\{X - t \le x \mid X > t\} = \frac{\mu((t, t+x])}{\mu((t,\infty))}.$$

A family of distribution functions $H_t$ converges weakly to $G$ if $H_t(x) \to G(x)$ at every continuity point $x$ of $G$. The domain of residual life time attraction $D_r(G)$ (p. 798) is the set of $F$ with $F(x) < 1$ for all $x$ for which some $a(t) > 0$ and $b(t)$ give

$$F_t(b(t) + x a(t)) \to G(x) \quad \text{weakly as } t \to \infty.$$

For $p > 0$ and $c \ge 0$ the discrete limit law is (p. 793), for $x \ge 0$,

$$\Pi_{p,c}(x) = 1 - \exp\Big(-p\Big[1 + \frac{\log(1+cx)}{cp}\Big]\Big) \ (c > 0), \qquad \Pi_{p,0}(x) = 1 - \exp\Big(-p\Big[1 + \frac{x}{p}\Big]\Big),$$

and $\Pi_{p,c}(x) = 0$ for $x < 0$; $[\,\cdot\,]$ is the integer part. Its tail takes the values $e^{-p}, e^{-2p}, \dots$ and jumps at $(e^{kpc} - 1)/c$, $k = 0, 1, \dots$ (at $kp$ if $c = 0$).

A distribution function $F_0 = 1 - R_0$ is discrete with jump sequence $t_0 < t_1 < \cdots$ if the $t_n$ are unbounded, each carries positive mass and there is no other mass. Two distribution functions with $F_i(x) < 1$ for all $x$ are tail equivalent if $1 - F_1(x) \sim 1 - F_2(x)$ as $x \to \infty$. The conditions of §3 are

$$\text{(12a)}\ \ \frac{t_{n+1} - t_n}{t_n - t_{n-1}} \to e^{pc}, \qquad \text{(12b)}\ \ \frac{R_0(t_{n+1})}{R_0(t_n)} \to e^{-p}.$$

Formalization targets

Goal: Theorem 5 (p. 800)

For $p > 0$ and $c \ge 0$,

$$F \in D_r(\Pi_{p,c}) \iff F \text{ is tail equivalent to a discrete } F_0 \text{ whose jumps satisfy (12a) and whose tail satisfies (12b).}$$

Milestones

1. (§3, pp. 799–800) A discrete $F$ satisfying (12a) and (12b) lies in $D_r(\Pi_{p,c})$.
2. (§3, p. 800) If $F_1$ is tail equivalent to $F_2 \in D_r(\Pi_{p,c})$, then $F_1 \in D_r(\Pi_{p,c})$. Milestones 1 and 2 give the "if" half.
3. (Proof of Theorem 5, p. 800) If $F \in D_r(\Pi_{p,c})$, there are $b_n \uparrow \infty$ with $R(b_{n+1})/R(b_n) \to e^{-p}$ and a discrete $F_0$, tail equivalent to $F$, with $R_0(t_n) = R(b_n)$ at its jumps.
4. (Proof of Theorem 5, pp. 800–801) Such an $F_0$ satisfies (12b) and (12a). Milestones 3 and 4 give the "only if" half.

Significance

Theorem 5, together with Theorems 1, 3 and 4 of the paper, completes the description of residual-life attraction: every nondegenerate limit is of one of the listed types, and each type's domain of attraction is identified. For the discrete types the answer is a statement purely about the geometry of the atoms of an approximating law, which makes membership checkable for concrete lifetimes (geometric-type laws on $\{0, 1, 2, \dots\}$ fall under $c = 0$, laws on a geometric grid $\{\lambda^n\}$ under $c > 0$). It also explains why discrete limits are invisible when only a scale normalization is allowed.

The theorem has been proved since 1974; it has not been formalized. A machine-checked development would supply weak convergence of distribution functions at continuity points, residual-life normalizations and tail equivalence as reusable objects, and would check a proof that the paper compresses into a page, including a convergence-of-types step on a half line that the paper cites from its own §1.

Difficulty

The "if" half is close to a computation, but the computation is about weak convergence to a step function: the normed tails converge only off the jumps, and the normalization must be extended from the jump times $t_n$ to all real ages $t$.

The "only if" half is the core. From $F \in D_r(\Pi_{p,c})$ alone one has to manufacture the atoms $t_n$ of a discrete law that $F$ itself need not have. The obvious attempt, reading the atoms off the jumps of $F$, fails because $F$ may be continuous: membership in $D_r(\Pi_{p,c})$ only says that $F$ drops by a factor close to $e^{-p}$ over short stretches, relative to the normalization, and never by an intermediate factor. Making "never by an intermediate factor" precise uniformly in the age $t$, with normalizations $a(t), b(t)$ about which nothing but their existence is known, is where the work lies; the same lack of control over $a(t)$ is what makes the gap ratio (12a) hard to extract.

Formalization scope

A law is a measure μ : Measure ℝ with IsProbabilityMeasure μ; the tail $R(x)$ is (μ (Set.Ioi x)).toReal, and $F_t(x)$ is μ((t, t+x]) / μ((t,∞)). $D_r(G)$ (InDr) includes $F(x) < 1$ for all $x$, normalizations $a(t) > 0$ for all real $t$, and "weakly" means convergence at every continuity point of $G$ and nowhere else; requiring convergence at the jumps of $\Pi_{p,c}$ would make $D_r(\Pi_{p,c})$ empty. $\Pi_{p,c}$ (piPC) is defined by cases $c = 0$ / $c > 0$ with Int.floor, so that $c = 0$ is not the junk value of a division by zero; it is used only with $p > 0$, $c \ge 0$. A discrete law with jump sequence $t$ (IsDiscreteWithJumps) has $t$ strictly increasing and tending to $\infty$, positive mass at each $t_n$ and no mass elsewhere. (12a) is indexed from $n = 1$. Tail equivalence (TailEquiv) includes $F_i(x) < 1$ for both laws.

Conventions and disclosed readings:

• The page proves the "if" direction by showing convergence to a function of the type of $1 - \Pi_{p,c}$; since $D_r$ lets $a, b$ be chosen freely, milestone 1 is stated with $\Pi_{p,c}$ itself.
• The proof of Theorem 5 uses the normalization (2)–(3) of p. 794, where $b(t)$ shifts $X$ rather than $X - t$; milestone 3 only asserts the existence of the sequence $b_n$ with $R(b_{n+1})/R(b_n) \to e^{-p}$, so no convention enters its statement.
• "$F_0$ only takes the values $F(b_n)$" is formalized as $R_0(t_n) = R(b_n)$ for all $n$, the form the next paragraph of the page uses. This identity is a hypothesis of milestone 4, as on the page, and cannot be dropped: a law tail equivalent to $F$ may carry extra atoms of vanishing relative mass, at which (12a) and (12b) fail.
• The page identifies the limit of the gap ratios as the scale constant $A$ of a functional equation; milestone 4 states it as $e^{pc}$, the gap ratio of the jumps of $\Pi_{p,c}$.
• Theorem 5 prints "distribution fuction"; this typo is kept in the quoted text only.

No statement is trivialized: $D_r(\Pi_{p,c})$ is nonempty (the geometric law on $\{0,1,2,\dots\}$ lies in $D_r(\Pi_{p,0})$), and Theorem 5 is not a definitional unfolding, since $D_r$ is defined by weak convergence and the right-hand side by discrete approximation.

A complete development needs: weak convergence of distribution functions at continuity points, a convergence-of-types lemma on a half line (the Remark after Lemma 1 of the paper, p. 795), and elementary facts on step functions. The first two are reusable across the whole paper and across extreme-value theory. Contributions of either half of the theorem, or of the convergence-of-types lemma, are welcome.

Selected references

• A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
• J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003
• B. V. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44 (1943), 423–453. https://doi.org/10.2307/1968974
• L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970.

Motivation

Economic lot sizing asks when to produce goods across a finite planning horizon when demand in each period is known. Producing in a period incurs a fixed setup charge and a marginal cost per unit, while goods may be produced before the period in which they are needed. Such a decision has to balance paying another setup charge against producing more units earlier. The model is a standard setting for studying how dynamic programming and linear optimization describe the same planning decision. Wagelmans, Van Hoesel and Kolen study faster algorithms for this model and, in Section 4, connect the optimal lot-sizing cost to a greedy solution of a dual program Wagelmans et al. (1992).

The dual connection is useful in its own right. It supplies a certificate for the cost returned by the forward dynamic program: a feasible dual vector attains that cost. The paper allows demand to vanish in some periods, which makes the dual values at those periods free and forces care in defining the dynamic program. The mission targets precisely that case.

Setting

There are periods $1,\ldots,n$. Demand $d_t$ and setup cost $f_i$ are nonnegative for the periods in the horizon. The marginal production cost $c_i$ is any real number. Write $d_{i,j}=\sum_{t=i}^j d_t$ for cumulative demand from $i$ through $j$. Values at period zero and beyond the horizon are bookkeeping only; every optimization constraint concerns periods $1,\ldots,n$.

The forward lot-sizing cost $F(j)$ describes the least cost of serving periods $1,\ldots,j$ under the zero-inventory property cited by the paper. Its recursion starts with $F(0)=0$. If $d_j=0$, no new production is needed and $F(j)=F(j-1)$. If $d_j>0$, the last production setup may occur at some $i\le j$, giving

$$F(j)=\min_{1\le i\le j}\bigl(f_i+c_i d_{i,j}+F(i-1)\bigr).$$

This piecewise definition matters even when only one period has zero demand. Taking the displayed minimum at $d_j=0$ would charge a setup that need not occur.

Program D′ chooses free real values $v_1,\ldots,v_n$ to maximize $\sum_{t=1}^n d_tv_t$, subject to

$$\sum_{t=i}^n d_t\max\{0,v_t-c_i\}\le f_i \qquad(1\le i\le n).$$

“Free” means there is no nonnegativity constraint on $v_t$. The paper obtains D′ from the dual of the linear relaxation of its simple plant location formulation, using the variables of Formulation III Wagelmans et al., pp. S147, S152–S153. The mission takes D′ as the defined optimization problem.

The greedy forward rule visits periods in increasing order. At a period with $d_j>0$, the chosen value is the minimum of the upper bounds left by the constraints indexed $i\le j$:

$$v_j=\min_{1\le i\le j} \left(c_i+\frac{f_i-\sum_{t=i}^{j-1}d_t\max\{0,v_t-c_i\}}{d_j}\right).$$

When $d_j=0$, the rule places no restriction on $v_j$. This matches the paper's statement that it may be assigned an arbitrary value. One concrete recursive vector in the definitions sets each such value to zero, but the goal covers every assignment.

Formalization targets

The goal says that every vector satisfying the greedy rule is feasible for D′, agrees with the dynamic-programming cost at every prefix, and is optimal among all feasible D′ vectors:

$$\sum_{t=1}^j d_tv_t=F(j)\quad(1\le j\le n), \qquad \sum_{t=1}^n d_tu_t\le\sum_{t=1}^n d_tv_t \quad\text{for every feasible }u.$$

The milestone path follows the Section 4 statements: feasibility of the greedy vector; decreasing greedy values across positive-demand periods; the prefix upper bound for any feasible dual vector; and Equation (2), which expresses a greedy prefix value using a minimizing production period. Equation (2) is stated with the induction hypothesis that appears immediately before it in the paper. The goal combines these claims without treating the desired value identity as a hypothesis.

Significance

The result identifies a dual certificate whose value matches the forward lot-sizing cost. It also explains why a greedy forward assignment can solve D′ despite each constraint linking the current value with all later periods. The full-horizon identity recovers the cost $F(n)$, and the comparison with every feasible vector makes the word “optimal” precise. The paper additionally says that this dual computation directly provides an optimal primal solution; this mission does not encode that reconstruction because it would require the primal formulation and its correspondence to $F$ Wagelmans et al., p. S153.

A formal proof would provide a reusable finite-horizon certificate theorem for this dual formulation and a careful treatment of empty and zero-demand prefixes. The paper's result is already proved mathematically. The Lean files in this proposal state the goal and its milestones; their theorem proofs remain to be supplied by solvers. Related platform goals about the convex hull of other lot-sizing formulations and the Federgruen–Tzur forward algorithm concern different objects, so they are credited as neighboring work rather than imported as this theorem.

Difficulty

A current greedy value is limited by every earlier production index, and feasibility must still hold for the entire horizon, not merely for the constraints truncated at the current period. Equality with $F(j)$ also has to survive periods with zero demand, where the dual coordinate is unrestricted but its weighted contribution vanishes. The forward recurrence has a separate branch at exactly those periods. A formulation that assumes every demand is strictly positive would avoid the delicate case and would miss a feature the authors explicitly retain.

Formalization scope

Lean represents the horizon by natural-number indices $1,\ldots,n$ and the demand, setup, marginal-cost and dual sequences by functions $\mathbb N\to\mathbb R$. Finite sums use closed intervals; the sum before period $j$ uses $[i,j)$, so it is empty when $i=j$. Minima are over the nonempty finite set $\{1,\ldots,j\}$, only when $j\ge1$. The horizon $n=0$ has empty sums and no constraints. The cost and dual values are real, with no sign condition on $c_i$ or $v_i$.

Several informal phrases are made explicit. “The solution is feasible” means every D′ constraint through $n$ holds. “Optimal” includes feasibility, every prefix identity, and comparison with every feasible dual vector. “Can be given an arbitrary value” is represented by no greedy-rule condition at zero demand; the theorem quantifies over all vectors that satisfy the positive-demand conditions. The paper states monotonicity for consecutive nonzero-demand periods; the milestone uses any two positive-demand periods, skipping zero-demand positions so it holds for every choice of their dual values. The weak-duality milestone spells out the paper's reference to “duality and the structure of D′” as an inequality for each feasible vector and prefix.

The identification of $F$ with the optimum of the primal lot-sizing model relies on the zero-inventory property cited by the authors and is not separately formalized. Neither the equivalence of Program D and D′ nor the recovery of a primal production plan is an item here. The paper's running-time claims, including $O(n^2)$ for the greedy forward algorithm and $O(n\log n)$ for its backward algorithm, are outside the scope: the paper does not fix a machine model or constants for them. A definition of $F$ as the optimum of D′ would make the value identity circular; the proposal defines it by the paper's forward recursion instead. The backward algorithm of pp. S153–S155 belongs to a separate development.

Selected references

• A. Wagelmans, S. Van Hoesel and A. Kolen, Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40, Supplement 1, 1992, S145–S156. DOI