Operations Research

Why marginal allocation needs a convex hull

Service organizations keep repairable spare parts at a depot and at operating bases. Stock has a purchase or holding cost, while insufficient stock leaves backorders. Craig Sherbrooke's METRIC study describes how to evaluate such a system and distribute additional units among item types. Its fifth computational stage compares the reduction in expected backorders from the next unit with the cost of that unit. The comparison is delicate because the backorder function after optimizing the depot–base split can fail to be convex as a function of total item stock, even though a fixed depot-stock version is convex. Sherbrooke therefore introduces a convex extension before applying marginal analysis (Sherbrooke 1968, pp. 134–135).

This mission isolates the theorem in the paper's Appendix. It concerns abstract item functions with the properties needed for the allocation rule, so the result can be studied independently of the queueing assumptions and the FORTRAN procedure that produced those functions in METRIC. The paper supplies a proof of the Appendix theorem; the mission seeks a machine-checked formalization of its precise mathematical content (Sherbrooke 1968, pp. 140–141).

Setting: stock levels, costs, and the lower boundary

There is a finite collection of items indexed by $i$. A decision assigns each item a stock level $m_i\in\mathbb N$, where $0$ is permitted. Item $i$ has a unit cost $c_i$ and a real-valued function $\Xi_i(m)$ representing the backorder contribution associated with stock level $m$. In the METRIC application, $\Xi_i$ is obtained after choosing the best allocation of $m$ units between depot and bases. The Appendix theorem uses only that $\Xi_i$ is nonincreasing and has a finite lower bound. “Decreasing” is read weakly: the paper's justification says that adding a unit “cannot exceed” the backorders at the previous level (Sherbrooke 1968, p. 136).

For a function $g:\mathbb N\to\mathbb R$, write $\Delta g(m)=g(m+1)-g(m)$. The function is discretely convex when $\Delta g(m+1)\ge\Delta g(m)$ at every level. The lower convex hull $H_i$, written $\Xi_i'$ in the paper, is the greatest discretely convex function at or below $\Xi_i$. It follows the lower boundary of the convex hull of the points $(m,\Xi_i(m))$; a point above that boundary is lowered, while a contact point keeps its original value (Sherbrooke 1968, pp. 135–136, 140). The existing ServiceParts.StockLevels.Basic definition supplies $\Delta$ and $\Delta^2$ for real stock-level functions; this mission reuses it.

The original objective is the separable sum

$$J(m)=\sum_i\bigl(c_i m_i+\Xi_i(m_i)\bigr).$$

For each item, conditions (12) select the first level $\bar m_i$ where adding another unit no longer lowers the convexified cost:

$$c_i+H_i(\bar m_i+1)-H_i(\bar m_i)\ge0,\qquad \bar m_i>0\Longrightarrow c_i+H_i(\bar m_i)-H_i(\bar m_i-1)<0.$$

The second condition is automatic at $\bar m_i=0$, following the paper's convention $H_i(-1)=+\infty$ (Sherbrooke 1968, p. 140, Eqs. (11)–(12)).

Formalization targets

The Appendix goal is that each item's conditions (12) have exactly one solution and that the vector formed from those solutions minimizes the original, possibly nonconvex objective:

$$\forall i\;\exists!\bar m_i\in\mathbb N\text{ satisfying (12)}, \qquad J(\bar m)\le J(m)\quad\text{for every }m\in\mathbb N^I.$$

The milestone list follows the Appendix's claims: the lower boundary is a convex minorant; its marginal changes approach zero; (12) has a solution and that solution is unique; it minimizes the convexified single-item cost; and the selected level is a contact point where $H_i(\bar m_i)=\Xi_i(\bar m_i)$. The final comparison is with $J$, not just with the objective formed from $H_i$ (Sherbrooke 1968, pp. 140–141).

What the result establishes

The theorem licenses the paper's marginal allocation rule even when an item's original backorder function has nonconvex points. The rule can use a convex lower boundary to identify a level, yet the resulting allocation is optimal for the original function. Without the contact-point conclusion, optimality of the modified objective alone would not give that guarantee. The theorem is stated for any finite number of independent items with the listed properties, so it is reusable beyond the specific depot–base model (Sherbrooke 1968, pp. 134–136, 140–141).

The paper proves the result informally. This mission's definitions and theorem statements compile locally as open Lean goals; they do not yet constitute a machine-checked proof. A related published Prove2Me result, ServiceParts.Allocation.allocOpt_correct, proves correctness of an allocation algorithm for piecewise-linear functions assumed convex. It does not address the convexification or contact claim here. The platform's posed ServiceParts.StockLevels.optimal_stock_criterion and greedy_fill_rate_optimal concern other marginal criteria and likewise do not settle this Appendix theorem. A successful development would provide reusable Lean infrastructure for lower convex envelopes of integer sequences, their forward differences, and separable finite allocations.

Difficulty

A one-step marginal comparison on the raw $\Xi_i$ is insufficient when its forward differences can fall and then rise: an apparent local stopping point need not minimize the full sequence. Replacing $\Xi_i$ by a convex minorant restores ordered marginal changes, but a minimizer of a smaller function need not minimize the original function. The central burden is therefore the exact relation between the lower boundary and the original points at a level selected by the strict condition in (12). Ties in the objective add a second precision issue: the selected level is unique under the rule even when the objective has more than one minimizer (Sherbrooke 1968, pp. 135, 140–141).

Formalization scope and conventions

Stock levels are natural numbers, item contributions and costs are real, and the item type is finite; the empty item type is allowed, making both the sum and the coordinatewise statement trivial. The functions $\Xi_i$ are nonincreasing and bounded below, as in the Appendix. The lower hull is a pointwise real supremum over all discretely convex minorants. Its defining family is nonempty and bounded at each point under the lower-bound hypothesis, which every hull theorem carries. The hull is therefore fixed by the input function rather than supplied as an arbitrary minorant. The goal compares every vector in $\mathbb N^I$, without a budget restriction. The formalization does not use a default value for $H_i(-1)$: the predecessor condition applies only to positive stock levels.

The paper prints $c_i\ge0$ with at least one positive cost. Its existence assertion fails when a particular $c_i=0$: for $\Xi_i(m)=1/(m+1)$, a bounded, decreasing, convex sequence, the first inequality of (12) never holds. The goal and existence milestone therefore require $c_i>0$ for every present item. The paper's phrase “unique optimizing” is interpreted as uniqueness of the stock vector determined by (12), together with its optimality. It cannot assert uniqueness among all minimizers: with $c=1$, $\Xi(0)=1$, and $\Xi(m)=0$ for $m\ge1$, levels $0$ and $1$ tie. The proof's own wording identifies (12) as the unique selection rule (Sherbrooke 1968, p. 140).

The formalization contains separate definitions for discrete convexity, the greatest lower hull, conditions (12), and objective (11). It welcomes proofs and general lemmas about convex integer sequences and finite separable sums. The METRIC computation, empirical Air Force data, equations (7)–(9), and the discussion of Lagrangian versus combinatorial solutions are context rather than goals of this mission. A definition that simply sets $H_i=\Xi_i$, or a conclusion that minimizes only the hull objective, would omit the theorem's content.

Selected references

• Craig C. Sherbrooke, METRIC: A Multi-Echelon Technique for Recoverable Item Control, Operations Research 16(1), 122–141, 1968. DOI: 10.1287/opre.16.1.122.

Motivation

A finite dynamic program with total reward is the basic model of sequential decision making without discounting: a system moves among finitely many states, a decision maker picks an action in each state, collects a reward, and the system moves on or stops. The quantity of interest is the expected total reward of a policy, summed over the whole (possibly infinite) horizon, and the question is whether a simple policy — one that uses the same decision rule at every step — is as good as any other.

For discounted or strictly substochastic models the answer has long been known. Shapley (1953) showed by successive approximations that, when every transition matrix has row sums strictly below one, some stationary policy maximizes the total reward among stationary policies; Howard (1960) gave the policy-improvement method for finding one; Blackwell (1962) showed that the maximum over all policies is attained among stationary ones. All of these rest on a contraction hypothesis $\|P(f)\|<1$.

Veinott's 1969 paper (DOI 10.1214/aoms/1177697379), best known for its sensitive discount optimality criteria, opens in §2 by proving these classical results under the much weaker hypothesis that each stationary policy is transient, and without requiring the transition weights to be substochastic at all. Partial results in this direction were due to Eaton and Zadeh, Derman, and Denardo. The total-reward model without a contraction assumption covers stopping problems, shortest-path type problems and models in which "transition weights" are not probabilities (growth factors, populations), which is why the generalized model is of independent interest.

Setting

There are $S\ge 1$ states $1,\dots,S$. In state $s$ a finite nonempty set $A_s$ of actions is available; taking action $a$ earns the real reward $r(s,a)$ and assigns the transition weight $p(t\mid s,a)\ge 0$ to each state $t$. No bound on $\sum_t p(t\mid s,a)$ is assumed. The set of decision rules is $F=\times_{s=1}^S A_s$; for $f\in F$, $r(f)$ is the vector $(r(s,f(s)))_s$ and $P(f)$ the matrix $(p(t\mid s,f(s)))_{s,t}$.

A policy is a sequence $\pi=(f_1,f_2,\dots)$ of decision rules. The policy $f^\infty=(f,f,\dots)$ is stationary; $(g,\pi)=(g,f_1,f_2,\dots)$ uses $g$ first and then follows $\pi$; ${}^N\pi$ repeats the first $N$ rules of $\pi$ forever and is called periodic. Let $P^0(\pi)=I$ and $P^N(\pi)=P(f_1)\cdots P(f_N)$. The policy $\pi$ is transient if $\sum_{N\ge0}P^N(\pi)$ converges, and then its vector of total returns is

$$V(\pi)=\sum_{N=0}^\infty P^N(\pi)\,r(f_{N+1}).$$

The one-step comparison $v(g,\pi^*)=V(g,\pi^*)-V(\pi^*)$ measures the gain from deviating to $g$ for one step. Vectors are compared coordinatewise, and $x>y$ means $x\ge y$, $x\ne y$. For a matrix $B$, $\|B\|=\max_i\sum_j|b_{ij}|$ and $|\sigma(B)|$ is its spectral radius. Finally $V^*=\max_f V(f^\infty)$ and $\Re V=\max_g[r(g)+P(g)V]$, both coordinatewise.

Formalization targets

Goal: Corollary 6

If every stationary policy is transient, there is $f\in F$ with

$$V(\pi)\le V(f^\infty)\qquad\text{for every policy }\pi.$$

The hypothesis concerns only the finitely many stationary policies; the conclusion compares against every policy, stationary or not.

Milestones

1. Lemma 1. For transient $\pi=(g_i)$ and $\pi^*$: $V(\pi)-V(\pi^*)=\sum_N P^N(\pi)\,v(g_{N+1},\pi^*)$, and $V(g^\infty)-V(\pi^*)=[I-P(g)]^{-1}v(g,\pi^*)$.
2. Lemma 2. If every stationary policy is transient and $f\in F$: either $v(g,f^\infty)>0$ for some $g$, and then $V(g^\infty)>V(f^\infty)$, or $v(g,f^\infty)\le0$ for all $g$, which holds iff $f^\infty$ is best among stationary policies.
3. Corollary 1. If every stationary policy is transient, some stationary policy maximizes $V$ over the stationary policies.
4. Corollary 2. Under the same hypothesis, $V^*$ is the unique fixed point of $\Re$.
5. Lemma 3 (Hoffman). For every $\varepsilon>0$ and every program there is a positively similar program with $\max_g\|\tilde P(g)\|<\max_g|\sigma(P(g))|+\varepsilon$.
6. Corollary 4, read with "every" and with "some": stationary, periodic and arbitrary policies are transient together, and this is equivalent to $\|P^N(\pi)\|<1$ for some $N\ge1$; with $\|P(g)\|\le1$ also to $\|P^S(\pi)\|<1$.
7. Theorem 1. If every stationary policy is transient and $\pi^*$ is any policy: $v(g,\pi^*)>0$ implies $V(g^\infty)>V(\pi^*)$, and $v(\cdot,\pi^*)\le0$ iff $V(\pi)\le V(\pi^*)$ for all $\pi$.

Significance

Corollary 6 is the existence half of the theory of total-reward Markov decision processes: it says that the search for an optimal policy can be restricted to the finite set of stationary policies, and, together with Corollary 2 and Theorem 1, that such a policy is characterized by the optimality equation $\Re V=V$ and by the absence of one-step improvements. Corollary 4, which the paper's introduction singles out as the section's main new result, shows that transience of the finitely many stationary policies already forces transience of every policy, uniformly; this is what makes $V(\pi)$ well defined for all policies. Hoffman's Lemma 3 converts transience into a contraction in a rescaled norm, the device behind geometric convergence of value iteration (Corollary 3 of the paper).

On the formal side, Mathlib has matrices, summability and spectral radii but no total-reward decision model. These results are proved in the 1969 paper and are standard in the textbook literature on Markov decision processes; none of them has a machine-checked proof that we know of. Related platform items concern other models: the stochastic shortest path results of Bertsekas and Tsitsiklis (a cost model with a termination state, stochastic rows and an infinite-cost assumption on improper policies) and Blackwell's discounted model; neither covers nonnegative, non-substochastic weights.

Difficulty

Without a contraction, the standard argument — $\Re$ is a contraction, so it has a unique fixed point attained by a stationary policy — has nothing to start from: $\|P(g)\|$ may exceed one for every $g$, and the transition weights need not be probabilities, so no probabilistic coupling or stopping-time argument applies directly. Transience of each stationary policy is a statement about finitely many matrix powers $P(g)^N$, whereas the goal concerns infinite products of different matrices $P(f_1)P(f_2)\cdots$, whose behaviour is not controlled by the spectral radii of the factors in general. Passing from the stationary policies to all policies is the step where the obvious argument fails.

Formalization scope

The Lean development fixes these conventions.

• States are a nonempty finite type St; actions are a family of nonempty finite types A : St → Type, so $F$ is the dependent function type (s : St) → A s, not a common action set.
• A program is a structure Program St A with real rewards and nonnegative weights; no row-sum bound is part of the structure. Only 5° of Corollary 4 assumes $\|P(g)\|\le1$.
• Policies are deterministic Markov sequences ℕ → F, indexed from $0$: π 0 is $f_1$. "All policies" means all such sequences.
• Transience is Summable of $N\mapsto P^N(\pi)$ in the entrywise topology. $V$ is a tsum; it is the genuine series exactly for transient policies.
• $>$ on vectors is written out as $\ge$ and $\ne$; $\|\cdot\|$ is the maximum absolute row sum, defined explicitly; $|\sigma(\cdot)|$ is Mathlib's spectralRadius ℂ of the complexified matrix, valued in $[0,\infty]$.
• $V^*$ and $\Re$ are coordinatewise Finset.sup' over the finite set $F$.

A trivializing formalization is ruled out: the goal and Theorem 1 do not assume the competing policies transient (that would hide Corollary 4 inside the hypothesis), and since a non-summable tsum is $0$, no statement compares $V$ of a policy whose transience is not either assumed or implied by the hypotheses. The hypothesis "every stationary policy is transient" is satisfiable (for instance when all weights are zero) and is not implied by any row-sum bound.

A complete development needs Neumann series for nonnegative matrices, the Perron–Frobenius-type fact that a nonnegative matrix with spectral radius below one has a nonnegative $(I-B)^{-1}=\sum B^N$, and finite-dimensional spectral theory relating $|\sigma(B)|<1$ to $B^N\to0$. These are reusable well beyond this mission; contributions of such lemmas, and of proofs of the milestones in any order, are welcome.

Selected references

• A. F. Veinott, Jr., Discrete dynamic programming with sensitive discount optimality criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• D. Blackwell, Discrete dynamic programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• L. S. Shapley, Stochastic games, Proc. Nat. Acad. Sci. 39(10):1095–1100, 1953. https://doi.org/10.1073/pnas.39.10.1095
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2):165–177, 1967. https://doi.org/10.1137/1009030
• C. Derman, On sequential decisions and Markov chains, Management Sci. 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16

Motivation

A firm that holds a single stock of a product often serves customers of different priority: military and civilian requisitions, contract and spot customers, emergency and routine orders for spare parts. When stock runs short, it must decide not only how much demand to satisfy but whose. Satisfying a low-priority order now may leave the firm unable to serve a high-priority order that arrives later in the same replenishment cycle. Inventory rationing asks for the optimal rule.

Veinott (Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13 (1965)) studied a model with $n$ demand classes, but fixed in advance the rule that a lower class is served only when every higher class has been served in full, and gave conditions on the costs under which that rule is optimal. Topkis (Management Science 15 (1968), 160–176) dropped the fixed rule and characterized the optimal rationing policy within a replenishment period. Theorem 1 of that paper is the target of this mission. It extends the author's earlier two-class analysis; the two-class case was later partly rediscovered by Evans and by Kaplan. Critical-level rationing policies of this kind are a standard object in the later literature on multi-class inventory systems.

Setting

A period between two replenishments is divided into $k$ intervals, indexed backwards: interval $t$ has $t-1$ intervals after it, so the period starts in interval $k$ and ends in interval $1$. Demand comes in classes $1,\dots,n$, with class $n$ the most important. At the start of interval $t$ the firm holds stock $z\ge0$ and faces the outstanding demand vector $B=(B^1,\dots,B^n)\ge0$: the backlog $b$ carried in plus the new demand $d_t$, whose law $\mu_t$ on $[0,\infty)^n$ has finite means. Demands of different intervals are independent.

The firm chooses the vector $u$ of demand left unsatisfied, with $0\le u\le B$, so that $w=z-\mathbf 1\cdot(B-u)\ge0$ units remain in stock, where $\mathbf 1\cdot y=\sum_j y^j$. It pays the penalty $p_t\cdot u$ and the holding cost $h_t(w)$. A fraction $a_t\ge0$ of the unsatisfied demand is carried into the next interval: $b_{t-1}=a_tu$, with $a_t=1$ meaning complete backlogging and $a_t=0$ lost sales. At the end of interval $1$ the salvage cost $v_1(z)+v_2(z-\mathbf 1\cdot b)$ is charged. The standing assumptions are:

• (A) $h_t$ is convex and continuous on $[0,\infty)$;
• (B) $v_1$ is convex and continuous on $[0,\infty)$, $v_2$ is convex and continuous on $\mathbb R$, and $D^+v_2$ is bounded below, where $D^+$ is the right derivative;
• (C) $0\le p_t^1\le\cdots\le p_t^n$.

The minimal expected cost $f_t$ of the last $t$ intervals and its expectation $g_t$ satisfy

$$f_t(z,B)=\inf_{\substack{0\le u\le B\\ w=z-\mathbf 1\cdot(B-u)\ge0}}\big[p_t\cdot u+h_t(w)+g_{t-1}(w,a_tu)\big],\qquad g_t(z,b)=\mathbb E\,f_t(z,b+d_t),$$

with $g_0(z,b)=v_1(z)+v_2(z-\mathbf 1\cdot b)$.

For a class $j$, with $\delta_j$ its unit vector, the critical rationing level $\bar z_t^j\in[0,+\infty]$ is $+\infty$ if $\varphi_t^j(w)=p_t^jw+h_t(w)+g_{t-1}(w,a_tw\delta_j)$ is strictly decreasing on $[0,\infty)$, and is the smallest minimizer of $\varphi_t^j$ on $[0,\infty)$ otherwise. With $B^{(j)}=\sum_{i\ge j}B^i$, the rationing level policy leaves unsatisfied

$$u^j=\big(B^{(j)}-z+\bar z_t^j\big)^+\wedge B^j .$$

In words: going down from class $n$, it serves as much of each class as it can without letting the stock fall below that class's critical level.

Formalization targets

Goal: Theorem 1

Suppose $a_i\in\{0,1\}$ for every $i\le t$. Then

1. the rationing level policy attains $f_t(z,B)$ for every $z\ge0$, $B\ge0$;
2. the critical levels are ordered as

$$\bar z_t^1\ge\bar z_t^2\ge\cdots\ge\bar z_t^n;$$

3. for $\varepsilon>0$, the differences $f_t(z,B)-f_t(z+\varepsilon,B+\varepsilon\delta_j)$ and $g_t(z,b)-g_t(z+\varepsilon,b+\varepsilon\delta_j)$ do not depend on $B^1,\dots,B^j$ and $b^1,\dots,b^j$.

Milestones

In attack order:

1. Lemma 1: the infimum of a convex function over one block of variables is convex.
2. Lemma 2: $g_t$ and $f_t$ are convex and continuous on the orthant, and the infimum in (1) is a minimum.
3. The critical levels exist, so they are well defined.
4. Lemma 3: moving $\varepsilon$ of demand from class $i$ to a less important class $j<i$ does not raise $f_t$ or $g_t$.
5. (6): $f_t(z,B)=\min_wf_t(w;z,B)$, where $f_t(w;z,B)$ is the cost of issuing exactly $z-w$ units.
6. Lemma 4: for each $w$, serving the classes in order of importance is optimal.
7. Corollary 1: some optimal $u$ never serves a class before every more important class has been served in full.

A companion item states the paper's remark that with a linear ordering cost $c(y)=c\cdot y$ the optimal order is $y(z)=(y(0)-z)^+$.

Significance

Theorem 1 reduces the $n$-dimensional rationing decision in each interval to $n$ numbers, which are computed from one-dimensional convex minimizations. Under complete or no backlogging this is the structural result that the rest of the paper builds on: the monotonicity of the levels in time (Theorem 2), the reduction of the backlog case to a single-interval problem (Theorem 3), and the multi-period ordering policy (Theorem 4). The hypothesis on $a_i$ is sharp in the sense the paper shows: for $a_2\in(0,1)$ an example on pp. 165–166 has no optimal policy of this form.

The theorem is proved in the paper, but no part of it is machine-checked. A formal development would contribute a reusable treatment of finite-horizon dynamic programs whose value function is defined by an infimum and an expectation over an orthant, with convexity and continuity propagated through the recursion. It would also contribute the comparative statics of critical-level policies.

Difficulty

The obvious argument proves optimality of the rationing level policy by induction from convexity alone. That is not enough. Convexity gives a one-dimensional problem in $w$ (by (6) and Lemma 4). But identifying its minimizer with the class-wise critical levels requires the marginal value of class-$j$ demand to be independent of the demand of the less important classes, which is part (c). Part (c) is false when $0<a_t<1$, so the induction must carry (a), (b) and (c) together and use $a_t\in\{0,1\}$ at every step. A second difficulty is analytic: $f_t$ is an infimum and $g_t$ an expectation, and before any structural argument starts the value functions must be shown to be finite, attained, continuous and integrable on the closed orthant (Lemma 2).

Formalization scope

• Representation. Classes are Fin n; the paper's class $j$ is index $j-1$, so class $n$ is the largest index and (b) is Antitone. Intervals are natural numbers counted backwards, as in the paper. Vectors are Fin n → ℝ with the pointwise order.
• Value functions. $f_t$ is defined by the recursion (1) itself, with a real infimum (sInf), and $g_t$ by a Bochner integral against $\mu_t$. Every statement about $f_t$, $g_t$ is restricted to $z\ge0$ and $B\ge0$ (or $b\ge0$). Lemma 2's attainment and integrability conjuncts are what identify these values with the paper's.
• Critical levels. The levels live in WithTop ℝ, with $\top=+\infty$. They are specified by the predicate IsCriticalLevel: strictly decreasing for $+\infty$, smallest minimizer otherwise. They are never computed by a real sInf, which would give the junk value $0$ when no minimizer exists.
• Standing assumptions. (A)–(C) are imposed for $1\le t\le k$. (B)'s limit condition is read as "$D^+v_2$ is bounded below". $D^+$ is an extended-real right Dini derivative. Assumption (D) on the ordering cost is not used.
• Added hypothesis. Lemma 1 adds the hypothesis that the function is bounded below on every fibre, because a real infimum cannot be $-\infty$.
• Not stated. The paper's remark that Assumption (D) ensures an optimal order $y(z)$ exists for a general continuous $c$ is not formalized. With $n=k=1$, $h_1(w)=w^2$, $c(w)=w-w^2$, $p_1=1$, $v_1=v_2=0$ and demand $1$ with certainty, (D) holds but $c(y)+g_1(y,0)=1-y$ for $y\ge1$, so no minimizer exists.
• Ruled out. Theorem 1 is not proved by assuming Lemma 2, the shape of the optimal vector, or the paper's derivative formulas (8)–(9). Those appear only as milestones or not at all. Part (a) asserts optimality over all feasible $u$, not among rationing level policies.
• Contributions welcome. Proofs of the milestones, general lemmas on convexity of partial infima and on continuity of parametric minima over polytopes, and integrability of functions of linear growth against laws with finite means.

Selected references

• D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3) (1968), 160–176. https://doi.org/10.1287/mnsc.15.3.160
• A. F. Veinott, Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5) (1965), 761–778. https://doi.org/10.1287/opre.13.5.761
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (convexity of partial minima, Theorem 5.7). https://doi.org/10.1515/9781400873173

Why two traffic speed averages differ

A speed recorded as a vehicle passes a fixed point and a speed recorded among vehicles occupying a road segment answer different questions. Fast vehicles pass a detector more often per unit time; slow vehicles remain visible along the segment for longer. Traffic studies therefore need to identify which distribution a measurement samples before comparing average speeds. J. G. Wardrop made this distinction explicit in his 1952 treatment of road traffic, then quantified it through the variance of the spatial speed distribution (Wardrop 1952, pp. 327–331 and Appendix II).

The result belongs to the paper's mathematical account of traffic flow. It is useful even when the subsidiary streams do not describe a random vehicle process: the identities concern finite positive flows and speeds. The paper also applies the same distributions to speed samples from radar and aerial photographs and to an idealized count of overtaking events (Wardrop 1952, pp. 330, 333–334).

Traffic streams and their two distributions

A road's traffic stream is divided into $C$ subsidiary streams, indexed by $i=1,\ldots,C$. Stream $i$ has flow $q_i$, the number of vehicles passing a point per unit time, and speed $v_i$. Its concentration is $k_i=q_i/v_i$, the number of vehicles occupying a unit road length. Total flow and concentration are $Q=\sum_i q_i$ and $K=\sum_i k_i$. The time frequency $f_i=q_i/Q$ weights each stream by how often its vehicles pass a point. The space frequency $f'_i=k_i/K$ weights it by the fraction of vehicles present along the road.

The time-mean speed is $\bar v_t=\sum_i q_i v_i/Q=\sum_i f_i v_i$. The space-mean speed is $\bar v_s=\sum_i k_i v_i/K=\sum_i f'_i v_i$. Both are averages of the same speeds; the weights differ. Wardrop defines the space-distribution variance independently as $\sigma_s^2=\sum_i k_i(v_i-\bar v_s)^2/K$, and the corresponding coefficient of variation as $c_s=\sigma_s/\bar v_s$ (equations (1)–(3), (7), pp. 328–331).

These are finite sums, not limits of a stochastic process. The model requires at least one subsidiary stream and positive flow and speed for each stream. Positive flows ensure that every speed in the equality criterion belongs to a present stream; positive speeds make concentration meaningful. The count $C$ is allowed to be one. In that case both means coincide and the variance is zero, as the formulas require.

Formalization targets

The main target is Wardrop's equation (6), together with its stated comparison and equality case (p. 330; Appendix II, p. 356):

$$\bar v_t=\bar v_s+\frac{\sigma_s^2}{\bar v_s},\qquad \bar v_s\le\bar v_t,\qquad \bar v_t=\bar v_s\iff v_i=v_j\text{ for every }i,j.$$

The subsidiary targets follow the paper's order. Equation (4) says $k_i v_i=q_i$ for each stream, giving equation (5), $Q=K\bar v_s$. Appendix II then uses the centered identity $\sum_i f'_i(v_i-\bar v_s)=0$ and rewrites the time mean as $\bar v_t=(\sum_i f'_i v_i^2)/\bar v_s$. These three claims are the mission milestones. Equation (8) is included as a companion formulation:

$$\bar v_t=\bar v_s(1+c_s^2).$$

The mission also records the paper's formulas for equally weighted time and space speed samples and the equivalent space- and time-frequency formulas for the idealized overtaking count. These companions use the same definitions without changing the main target (pp. 330–334).

What the result supplies

The identity gives an exact size and direction for the difference between the two averages. Since the variance is nonnegative and $\bar v_s$ is positive, the time mean cannot fall below the space mean. If all constituent speeds are equal, the difference vanishes; if any two present streams have different speeds, the difference is positive. The formula therefore lets a reader decide whether two reported speed averages can be compared directly, and it identifies the spatial variance as the quantity needed to convert between them.

The sample formulas sharpen that interpretation. Equal weights among vehicles passing a point make the time mean the arithmetic mean of the sampled speeds and the space mean their harmonic mean. Equal concentrations reverse which mean is arithmetic; the time mean becomes $\sum_i v_i^2/\sum_i v_i$. The overtaking formulas express a single pairwise count using either frequency system, provided the speeds are ordered and the paper's assumption of no interference with overtaking is used (Wardrop 1952, pp. 330, 333–334).

Wardrop proved these formulas in print. The remaining work in this mission is a machine-checked proof of the finite-sum identities and their strict equality case. The proposal supplies typed statements and definitions, but the theorem proofs are open. The resulting concentration and frequency definitions are reusable in other traffic-flow formalizations; the statements also provide small algebraic interfaces for testing more elaborate traffic models.

Where the formal proof needs care

The relation looks like a routine identity for weighted means, but the two weight systems are coupled through $k_i=q_i/v_i$. One cannot treat the time and space frequencies as independent arbitrary probability vectors and still obtain equation (6). The strict case needs more than nonnegativity of the variance: it needs the fact that every space weight is positive, so zero variance forces every constituent speed to equal the mean. The single-stream case and every denominator need the same attention.

The overtaking statement has a separate modelling boundary. Its algebraic equalities use a rate defined by pairwise speed differences. Wardrop's physical interpretation of that rate assumes that overtaking does not interfere with other overtaking. The mission records the identities for that idealized rate, without claiming that a measured road necessarily meets the physical assumption.

Formalization scope

Lean uses Fin C for the streams and real numbers for $q_i$, $v_i$, $k_i$, both means, the variance, and the overtaking rate. Finite sums are taken over all streams. The theorem hypotheses require $0<C$, $0<q_i$, and $0<v_i$ for every $i$. These requirements make $Q$, $K$, and $\bar v_s$ positive; Lean's total division would otherwise assign a zero value at a zero denominator that has no meaning in the paper's model. For the overtaking identity, StrictMono v retains Wardrop's ordering $v_1<\cdots<v_C$.

The variance is defined from equation (7), $\sum_i k_i(v_i-\bar v_s)^2/K$. Defining it by rearranging equation (6) would make the target true by definition and would erase the mathematical claim. The standard deviation uses the real square root of that variance. An observation in the sample companion is represented as one subsidiary stream of equal time or space weight; this is the formal reading of the paper's sampling paragraphs. No probability-measure library is needed, since $f_i$ and $f'_i$ are explicit finite weights.

A complete proof needs finite-sum rearrangements, elementary real division under positive denominators, nonnegative weighted squares, and the equality case of a positive weighted sum of squares. The definitions and the mean identities are welcome as separate reusable contributions. The mission does not include the paper's normal approximation for overtaking density in equation (11), which Wardrop presents as an approximation rather than an exact finite-sum theorem.

Selected references

• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers, Part II 1 (1952), 325–362. DOI: 10.1680/ipeds.1952.11259.

Motivation

A Markov decision process with the average cost criterion asks for a policy that minimizes the long-run expected cost per unit time. The criterion is the natural one for inventory, queueing and maintenance systems that run indefinitely without a meaningful discount rate, and it is the standard benchmark in the theory of controlled Markov chains (Arapostathis et al. 1993, Hernández-Lerma and Lasserre 1996). Unlike the discounted criterion, it has no contraction to work with, and an average-optimal policy may fail to exist.

The classical route to average optimality is the vanishing discount approach: solve the $\beta$-discounted problem, which is well behaved, and let $\beta \uparrow 1$. Schäl's paper gives conditions on a model with a general (Borel) state space under which this limit produces an average-optimal stationary policy.

Timeline. Taylor (1965) and Ross (1968) used the vanishing discount approach with equicontinuity via Arzelà–Ascoli. Sennott (1989) proved, for countable state spaces, that pointwise bounded relative discounted values yield an average cost optimality inequality and an average-optimal stationary policy. Schäl (1993, this mission) extended this to standard Borel state spaces under two alternative compactness–continuity conditions, (W) and (S). Later work, e.g. Feinberg, Kasyanov and Zadoianchuk (2012) and Feinberg and Liang (2022), weakened the compactness assumptions and studied when the inequality becomes an equation.

Setting

The model $(S, A, A(\cdot), q, c)$ consists of standard Borel spaces $S$ (states) and $A$ (actions); nonempty action sets $A(x) \subseteq A$ whose graph $\{(x, a) : a \in A(x)\}$ is measurable; a transition law $q(\cdot \mid x, a)$; and a measurable one-step cost $c(x, a) \in [0, \infty]$. A policy $\delta \in \Delta$ chooses, at each stage $n$, a randomized action that may depend on the whole history and lies in $A(x_n)$ with probability one. A stationary policy $f \in \mathbb F$ is a measurable $f : S \to A$ with $f(x) \in A(x)$.

For a policy $\delta$ and initial state $x$, $J^n(\delta, x)$ is the expected total cost of the first $n$ stages, and

$$\Phi(\delta, x) = \limsup_{n\to\infty} \tfrac1n J^n(\delta, x), \qquad g = \inf_{x \in S}\inf_{\delta \in \Delta} \Phi(\delta, x).$$

A policy is average optimal if $\Phi(\delta, x) = g$ for every $x$. The General Assumption is $g < \infty$.

For $0 < \beta < 1$, $J_\beta(\delta, x)$ is the expected total $\beta$-discounted cost, $v_\beta(x) = \inf_\delta J_\beta(\delta, x)$, $m_\beta = \inf_x v_\beta(x)$, and $w_\beta = v_\beta - m_\beta \ge 0$ is the relative discounted value function. The quantities $\bar g$ and $\underline g$ are the upper and lower limits of $(1-\beta)m_\beta$ as $\beta \uparrow 1$. Condition (B) requires $\sup_{\beta < 1} w_\beta(x) < \infty$ for each $x$.

Condition (W): $S$ is locally compact with countable base, the $A(x)$ are compact and $x \mapsto A(x)$ is upper semicontinuous, $q$ is weakly continuous on the graph of $A$, and $c$ is lower semicontinuous there. Condition (S): the $A(x)$ are compact, and for each fixed $x$, $a \mapsto q(\cdot \mid x, a)$ is setwise continuous and $a \mapsto c(x, a)$ is lower semicontinuous on $A(x)$.

Formalization targets

Goal: Theorem 3.8

Under the General Assumption, (B), and (W) or (S):

$$\exists f_1 \in \mathbb F:\ \Phi(f_1, x) = g \ \ \forall x \in S, \qquad g = \lim_{\beta\to1}(1-\beta)m_\beta = \lim_{\beta \to 1}(1-\beta)v_\beta(x)\ \ \forall x.$$

Moreover, for every sequence $\beta(k) \uparrow 1$ and every choice of $\beta(k)$-discount-optimal stationary policies $f_{\beta(k)}$, some average-optimal $f_1$ is a limit of them: under (W), $f_1(x) = \lim_m f_{\beta_m}(x_m)$ with $\beta_m$ from $\{\beta(k)\}$, $\beta_m \to 1$ and $x_m \to x$; under (S), $f_1(x) = \lim_m f_{\beta_m}(x)$.

Milestones

1. Lemma 1.2: $\limsup_{\beta\to1}(1-\beta)J_\beta(\delta, x) \le \Phi(\delta, x)$, and $\underline g \le \bar g \le g$.
2. Proposition 1.3: a finite measurable $\underline w \ge 0$ and $f_1 \in \mathbb F$ with $\underline w(x) + \underline g \ge c(x, f_1(x)) + \int \underline w\, dq(x, f_1(x))$ give $\Phi(f_1, \cdot) = g = \underline g = \bar g$.
3. Proposition 2.1 and (2.2): existence of discount-optimal stationary policies, the discounted optimality equation and its relative form.
4. Lemma 2.3: Fatou's lemma for setwise and for weakly converging measures.
5. (3.2), Lemmas 3.3, 3.4: the lower limit $\underline w(x) = \liminf_{k\to\infty, y\to x} w_{\beta(k)}(y)$ is attained along measurable sequences.
6. Proposition 3.5 and its (S) version (3.7): $\underline w$ and some $f_1$ satisfy the optimality inequality with $\underline g$.

Significance

The theorem gives existence of an average-optimal stationary policy on a general state space from checkable model conditions plus pointwise bounds on relative values, without assuming a solution of the average cost optimality equation. It also identifies the optimal average cost as the Abelian limit of discounted values, and says how to compute an optimal policy: as a limit of discount-optimal ones. §4 of the paper verifies (B) through entrance-time bounds and applies the theorem to Assaf's invariant problem and to a finite-capacity inventory model.

The result is a published theorem; none of it is machine-checked. Formalizing it requires the measure-theoretic layer of Borel dynamic programming (canonical path measures of history-dependent policies, discounted optimality equations, measurable selection of minimizers and of accumulation points) and Fatou lemmas for varying measures. These components are reusable for any Borel-space MDP. Related platform work: the Feinberg–Liang average-cost optimality equation under an additional equicontinuity assumption is posed separately (FeinbergLiang.ACOE.acoe_of_assumptionEC); it is a different theorem.

Difficulty

The naive argument takes a pointwise limit of $w_{\beta}$ as $\beta \to 1$ in the relative optimality equation (2.2). Under (B) the family $\{w_\beta(x)\}$ is only bounded pointwise, so no subsequence need converge, and even a pointwise lower limit loses the continuity needed to pass $\int w_\beta\, dq(x, f_\beta(x))$ to the limit when $q$ is only weakly continuous. The generalized lower limit $\underline w(x) = \liminf_{k, y\to x} w(k, y)$ repairs this, but then the limit has to be realized along measurably chosen states and indices, and the limiting actions must be selected measurably as accumulation points. The second obstacle is that only an inequality survives, with the constant $\underline g$; turning it into average optimality needs the Tauberian comparison of Lemma 1.2.

Formalization scope

The model reuses the published FeinbergLiang.ACOE.MDP (history-dependent randomized policies, the Ionescu-Tulcea path measure, $J^n$, $J_\beta$, $\Phi$) with its constant lower = 0, and a local definition file adds action sets, admissibility, $g$, $v_\beta$, $m_\beta$, $\bar g$, $\underline g$, $w_\beta$, $\underline w$ and Conditions (W), (S), (B). Committed conventions:

• All costs and values lie in $[0, \infty]$; $(1-\beta)$ is a nonnegative extended real, and $\beta \to 1$ means $\beta \uparrow 1$.
• Every infimum defining $g$ and $v_\beta$ runs over admissible policies only (actions in $A(x)$ almost surely); $q$ and $c$ are defined on $S \times A$, but only their values on the graph of $A$ enter.
• $w_\beta$ is a truncated difference, which equals $v_\beta - m_\beta$ because the General Assumption gives $m_\beta < \infty$. The General Assumption is an explicit hypothesis of every statement that involves $g$, $\underline g$, $\bar g$, $m_\beta$ or $w_\beta$.
• Upper semicontinuity of $A(\cdot)$ is Berge's. Condition (W)(0) is part of CondW: the topology on $S$ generates its σ-algebra and is locally compact, second countable and Hausdorff, hence metrizable; the metric $\rho$ of §3 is a metric-space instance. Under (S) no topology on $S$ is used, and the lower limit is $\liminf_k w_{\beta(k)}(x)$ (the discrete metric).
• (W)(1) prints "$A(x) \in \mathcal C(x)$", read as $\mathcal C(A)$. (3.2) prints $\inf_{k\ge n}\underline w_k(k, x)$, which is false in general; the subscript-$n$ version used in the proof of Lemma 3.4 is stated. "$\{\beta_m\} \subset \{\beta(k)\}$, $\beta_m \to 1$" is encoded as $\beta_m = \beta(k_m)$ with $k_m \to \infty$.
• Theorem 3.8's "$\{\beta(k)\}$ can be any sequence" is a universal quantifier over sequences and over choices of discount-optimal policies.

A formalization that assumes an average cost optimality inequality or equation, or that assumes the existence of the limit $\lim(1-\beta)m_\beta$, proves Proposition 1.3 rather than the goal; the goal derives the inequality from (W) or (S), (B) and the General Assumption alone. Contributions to the shared infrastructure (Markov property of the canonical process, measurable selection theorems such as Brown–Purves, Fatou lemmas for varying measures) are welcome as separate theorems. §4 of the paper (entrance-time bounds for (B)) is outside this mission.

Selected references

• M. Schäl, Average Optimality in Dynamic Programming with General State Space, Mathematics of Operations Research 18(1), 163–172, 1993. https://doi.org/10.1287/moor.18.1.163
• M. Schäl, Conditions for optimality in dynamic programming and for the limit of n-stage optimal policies to be optimal, Z. Wahrscheinlichkeitstheorie verw. Gebiete 32, 179–196, 1975. https://doi.org/10.1007/BF00532612
• L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Operations Research 37(4), 626–633, 1989. https://doi.org/10.1287/opre.37.4.626
• R. F. Serfozo, Convergence of Lebesgue integrals with varying measures, Sankhyā Ser. A 44, 380–402, 1982.
• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2), 282–344, 1993. https://doi.org/10.1137/0331018
• E. A. Feinberg, P. O. Kasyanov, N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probabilities, Mathematics of Operations Research 37(4), 591–607, 2012. https://doi.org/10.1287/moor.1120.0555

Motivation

Axiomatic bargaining theory asks which rule should divide a set of feasible utility vectors among a group of agents, and answers by listing properties a reasonable rule must have and determining the rules that have them. Nash's solution (Nash 1950) and the Kalai–Smorodinsky solution (Kalai and Smorodinsky 1975) are the two classical answers for a fixed set of two agents. Both characterizations take the number of agents as given.

In many division problems the group is not fixed: a supply of goods that was to be shared among some agents must later be shared among more. Thomson (1983) (Math. Oper. Res. 8:319–326) introduced a framework in which the population varies and a solution is a family of rules, one for each finite group. He proposed an axiom tying the rules for different groups together: when new agents arrive and the resources stay fixed, none of the original agents should gain (population monotonicity). The paper shows that this axiom, combined with four standard ones, singles out the Kalai–Smorodinsky solution.

Timeline.

• 1950: Nash characterizes the Nash solution for two agents.
• 1975: Kalai and Smorodinsky replace Nash's independence axiom by individual monotonicity and characterize their solution for two agents.
• 1980: Roth (Internat. J. Game Theory 8, 129–132, cited as [5] in Thomson 1983) discusses the $n$-agent extension; Thomson notes that without comprehensiveness the $n$-agent solution can fail weak Pareto-optimality once $n \ge 3$.
• 1983: Thomson characterizes the Kalai–Smorodinsky solution for a variable population by WPO, anonymity, scale invariance, continuity and population monotonicity. This is the result of this mission.

Setting

The agents are the natural numbers, and a group $P$ is a nonempty finite set of agents. For a group $P$, $\mathbb R^P$ is the space of real vectors indexed by $P$, and $\mathbb R^P_+$ its nonnegative orthant. For vectors, $x > y$ means $x_i > y_i$ for every $i$, $x \geqq y$ means $x_i \ge y_i$ for every $i$, and $x \geqslant y$ means $x \geqq y$ with $x \ne y$.

A division problem for $P$ is a set $S \subseteq \mathbb R^P_+$ that is compact, convex, contains a strictly positive vector, and is comprehensive: if $x \in S$ and $0 \leqq y \leqq x$, then $y \in S$. The class of these problems is $\Sigma^P$. The subclass $\tilde\Sigma^P$ also requires that whenever $x, y \in S$ and $y \geqslant x$, some $z \in S$ satisfies $z > x$.

A solution $F$ chooses a point $F^P(S) \in S$ for every group $P$ and every $S \in \Sigma^P$. The ideal point of $S$ is $a(S)$, with $a_i(S) = \max_{x \in S} x_i$. The Kalai–Smorodinsky solution $K$ selects the largest point of $S$ on the segment from the origin to $a(S)$:

$$K^P(S) = t^*\,a(S), \qquad t^* = \max\{t \ge 0 : t\,a(S) \in S\}.$$

The axioms on a solution $F$ are:

• WPO: no $y \in S$ has $y > F^P(S)$.
• PO: no $y \in S$ has $y \geqslant F^P(S)$.
• An: relabelling the agents along a bijection $\gamma : P \to P'$ relabels the outcome.
• S. Inv: rescaling each agent's utility by a positive factor rescales the outcome the same way.
• Cont: $F^P(S^k) \to F^P(S)$ whenever $S^k \to S$ in the Hausdorff metric.
• Mon: if $P \subseteq Q$, $S \in \Sigma^P$, $T \in \Sigma^Q$, and $S = T \cap \mathbb R^P$ (the points of $T$ that give zero to everyone outside $P$), then $F^P_i(S) \ge F^Q_i(T)$ for every $i \in P$.

Formalization targets

Goal: the characterization (Theorems 1 and 3)

For every solution $F$,

$$F \text{ satisfies WPO, An, S. Inv, Cont, Mon} \iff F^P(S) = K^P(S)\ \text{ for all finite } P \text{ and all } S \in \Sigma^P.$$

Milestones

1. Theorem 1. $K$ is a solution and satisfies WPO, An, S. Inv, Cont and Mon.
2. Theorem 2, $|P| = 2$. Under WPO, An, S. Inv and Mon, $F^P(S) \geqq K^P(S)$ for every two-agent group.
3. The replica problem (appendix). If $a(S) = e^P$, $a e^P \in S$ and $i_0 \in P$, there are $Q \supseteq P$ with $|Q| = 3|P| - 2$ and $T \in \Sigma^Q$ such that $T \cap \mathbb R^P = S$ and $a e^Q \in T$. In addition, every agent $j \in Q$ faces, in some slice of $T$, a relabelled copy of $S$ in which $j$ holds agent $i_0$'s position.
4. Theorem 2. Under WPO, An, S. Inv and Mon, $F^P(S) \geqq K^P(S)$ for every $P$ and every $S \in \Sigma^P$.
5. Corollary 1. Under the same four axioms, $F = K$ on every $\tilde\Sigma^P$.
6. Density. Every $S \in \Sigma^P$ is a Hausdorff limit of problems in $\tilde\Sigma^P$.
7. Theorem 3. WPO, An, S. Inv, Cont and Mon imply $F = K$ on every $\Sigma^P$.

Two further statements accompany the goal. Corollary 2 says that no solution satisfies PO, An, S. Inv and Mon. Lemma 1 says that some solution other than $K$ satisfies WPO, An, S. Inv and Mon.

Significance

The theorem identifies the Kalai–Smorodinsky solution as the only rule, among those treating agents symmetrically and ignoring utility units, under which an arrival of new claimants never benefits existing ones. Corollary 2 shows that weak Pareto-optimality cannot be strengthened to Pareto-optimality. Lemma 1 shows that continuity cannot be dropped. Together they fix the logical boundary of the result. The replica construction of the appendix is a reusable device: a problem in which every agent of a larger group faces an exact copy of one agent's situation.

The result has been proved since 1983. It has not been machine-checked, and to our knowledge no proof assistant library contains bargaining problems, solutions or the Kalai–Smorodinsky solution. The mission produces these definitions and checks the full argument, including two steps the paper asserts without proof. One is that the replica problem has the required slices. The other is that problems satisfying condition (c) are dense in the Hausdorff metric. Formalizing the paper also exposes a printed slip: Theorem 2 is stated as an equivalence, but only one direction is true and proved, and only that direction is stated here.

Difficulty

Theorem 1 asks for routine but real convex analysis. Continuity of $K$ requires the ideal point and the maximal scalar $t^*$ to move continuously with $S$ in the Hausdorff metric. Comprehensiveness and the strictly positive vector are what make this work.

The substance is in Theorem 2. The first thought is to compare $F^P(S)$ with $K^P(S)$ inside $S$ alone, using only WPO, An and S. Inv. That cannot work: Lemma 1 exhibits a solution satisfying all four axioms that differs from $K$, so the argument must leave the group $P$. The proof builds a larger problem $T$ in which every member of an enlarged group faces a copy of the worst-treated agent's position. Mon then caps each agent's payoff in $T$, and WPO fails at the diagonal point $a e^Q$. Choosing the groups and bijections, and verifying that each slice of the convex comprehensive hull is exactly the intended copy, is the delicate part. The paper dismisses it as "clear".

Theorem 3 needs the density of $\tilde\Sigma^P$ in $\Sigma^P$. An approximating problem must lose every flat face on its weak Pareto boundary while staying compact, convex and comprehensive.

Formalization scope

Agents are ℕ, where the paper uses $\{1, 2, \dots\}$; this relabelling is harmless. Groups are nonempty: for the empty group, $\mathbb R^\emptyset$ is a point and WPO would hold for no solution, so the page's "finite subsets" is read as nonempty finite subsets. A group is a Finset ℕ, and $\mathbb R^P$ is the function type P → ℝ, whose metric is the sup metric. Hausdorff convergence uses Mathlib's extended Hausdorff distance Metric.hausdorffEDist. Convergence in it is equivalent to Euclidean Hausdorff convergence, because the norms are equivalent.

A solution is a total function on all sets, together with the hypothesis IsSolution F that $F^P(S) \in S$ for $S \in \Sigma^P$. Every axiom quantifies over problems in $\Sigma^P$ only, and "$F$ is the Kalai–Smorodinsky solution" means agreement on every $\Sigma^P$. Two formalizations of the goal would be trivial or false, and the statements here rule out both: one that equates $F$ and $K$ as functions, and one that drops IsSolution.

The remaining conventions are these.

• $K$ and the ideal point use sSup. Both suprema are attained on $\Sigma^P$.
• $T \cap \mathbb R^P$ is the set of $x$ whose zero-extension lies in $T$.
• An quantifies over bijections P ≃ P'.
• Scalings have strictly positive factors.

Deviation from the page. Theorem 2's printed "if" direction is false, so only "only if" is stated. For example, choosing $(2,1,1)$ on $\mathrm{cch}\{(2,1,1),(0,2,0),(0,0,2)\}$ and $K$ elsewhere gives a solution with $F \geqq K$ that violates S. Inv. The replica milestone states the appendix construction existentially, for a generic agent $i_0$ instead of agent 1.

Out of scope: Theorem 4 (solutions defined on $\tilde\Sigma^P$ only, whose necessity proof is a sketch), and the remarks of §4.2–§4.4.

A complete development needs Hausdorff-metric continuity of maxima over compact sets and the convex comprehensive hull. It also needs elementary facts about slices and relabellings of comprehensive sets. All of these are reusable for other bargaining and fair-division formalizations. Contributions are welcome on any milestone, and on lemmas about $\Sigma^P$ that several milestones share.

Selected references

• W. Thomson, The fair division of a fixed supply among a growing population, Mathematics of Operations Research 8(3):319–326, 1983. https://doi.org/10.1287/moor.8.3.319
• E. Kalai and M. Smorodinsky, Other solutions to Nash's bargaining problem, Econometrica 43(3):513–518, 1975. https://doi.org/10.2307/1914280
• J. F. Nash, The bargaining problem, Econometrica 18(2):155–162, 1950. https://doi.org/10.2307/1907266
• A. E. Roth, An impossibility result for n-person games, International Journal of Game Theory 8:129–132, 1980 (as cited in Thomson 1983, reference [5]); see the reference list of https://doi.org/10.1287/moor.8.3.319

Motivation

The logarithm of a share price is commonly modelled as a Brownian motion with drift, $X_t=\sigma B_t+ct$. The Black–Scholes option pricing formula needs the volatility $\sigma$ but not the drift $c$, so a practitioner must estimate $\sigma^2$ from data. Observing the whole path would give $\sigma^2$ exactly through its quadratic variation, but a real observer sees far less. The most readily available daily information is the opening and closing prices together with the day's high and low.

Parkinson (1980) proposed an estimator from the high–low range, and Garman and Klass (1980) found the minimum-variance estimator among a class of quadratic functions of high, low and close. Both were derived assuming zero drift, $c=0$, and the Garman–Klass estimator is biased when $c\neq0$. Rogers and Satchell (Ann. Appl. Probab. 1 (1991) 504–512) proposed the estimator

$$\hat\sigma^2\equiv S_1(S_1-X_1)+I_1(I_1-X_1),$$

which is unbiased for every drift. Their estimator is now a standard tool in empirical finance for range-based volatility measurement.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ carrying a standard Brownian motion $B=(B_t)_{t\ge0}$: $B_0=0$, its increments over disjoint intervals are independent and Gaussian with variance equal to the length of the interval, and every sample path $t\mapsto B_t(\omega)$ is continuous. Fix a drift $c\in\mathbb R$ and a volatility $\sigma\ge0$. The log-price is

$$X_t=\sigma B_t+ct,\qquad t\ge0,$$

and, for a trading period $[0,t]$, the running maximum and running minimum are

$$S_t=\sup_{0\le u\le t}X_u,\qquad I_t=\inf_{0\le u\le t}X_u.$$

Thus $S_t$, $I_t$ and $X_t$ are the high, the low and the close of the log-price (with the open normalized to $X_0=0$). In Lean these are logPrice σ c B t ω, runMax σ c B t ω and runMin σ c B t ω in the namespace RogersSatchell.Unbiased.

The proof in the paper passes through an exponential time: a random variable $T$ with $P(T>x)=e^{-\lambda x}$ (rate $\lambda>0$, mean $\lambda^{-1}$), independent of the whole path $B$. For $\sigma>0$ the rates

$$\alpha=\frac{\sqrt{c^2+2\lambda\sigma^2}-c}{\sigma^2},\qquad \beta=\frac{\sqrt{c^2+2\lambda\sigma^2}+c}{\sigma^2}$$

appear, in Lean alpha σ c lam and beta σ c lam.

Formalization targets

Goal: display (3)

For every $c\in\mathbb R$, every $\sigma\ge0$ and every $t\ge0$, $S_t(S_t-X_t)+I_t(I_t-X_t)$ is integrable and

$$E\big[S_t(S_t-X_t)+I_t(I_t-X_t)\big]=\sigma^2t.$$

At $t=1$ this is the unbiasedness of $\hat\sigma^2$ of display (2). The statement quantifies over all drifts; the absence of $c$ on the right-hand side is the content.

Milestones (Section 2, pp. 505–506)

1. At an independent exponential time $T$ of rate $\lambda$: $S_T\sim\operatorname{Exp}(\alpha)$ and $-I_T\sim\operatorname{Exp}(\beta)$.
2. The Wiener–Hopf splitting: $S_T$ and $S_T-X_T$ are independent, and $S_T-X_T$ has the law of $-I_T$.
3. $E[S_T(S_T-X_T)]=1/(\alpha\beta)=\sigma^2/2\lambda$.
4. $E[S_T(S_T-X_T)]=\int_0^\infty\lambda e^{-\lambda t}\,E[S_t(S_t-X_t)]\,dt$.
5. $E[S_t(S_t-X_t)]=\sigma^2t/2$ for every $t\ge0$.
6. $E[I_t(I_t-X_t)]=\sigma^2t/2$ for every $t\ge0$.
7. (off the goal's path) With $Y_1=S_1(S_1-X_1)$, $Y_2=I_1(I_1-X_1)$: $E Y_1^2=EY_2^2=\sigma^4/2$, $E(Y_1+Y_2)^2\le2\sigma^4$ and $\operatorname{var}(\hat\sigma^2)\le\sigma^4$, for every drift $c$.

Significance

The goal certifies a drift-free unbiased volatility estimator built from four numbers per trading day. Because only $\sigma^2$ enters the Black–Scholes formula, an estimator whose mean does not depend on the nuisance parameter $c$ is exactly what is needed. Milestone 7 complements this with a drift-uniform bound on its variance, $\operatorname{var}(\hat\sigma^2)\le\sigma^4$, while the exact value $0.331\sigma^4$ quoted in the paper is only available at $c=0$.

On the formalization side, the results are classical and proved; none is machine-checked as far as the platform's catalog shows. A complete development would give the first formal treatment of the joint law of the running maximum of drifted Brownian motion at an exponential time, of the Wiener–Hopf splitting at the maximum, and of a Laplace-inversion argument for a moment function of the time horizon. All three are reusable well beyond volatility estimation: in ruin theory, queueing (reflected Brownian motion), and the pricing of lookback and barrier options.

Difficulty

The obvious approach, computing $E[S_t(S_t-X_t)]$ directly from the joint density of $(S_t,X_t)$ for drifted Brownian motion, requires the reflection principle combined with a Girsanov change of measure, followed by a double integral involving Gaussian tails, done separately for each sign of $c$. The cancellation that makes the drift disappear is not visible in that computation, and a statement specialized to $c=0$ (where the reflection principle alone suffices) does not carry over. Every step of the milestone list rests on path properties of Brownian motion (the strong Markov property, the law of the running maximum, splitting at the maximum) that Mathlib does not yet provide for IsBrownianReal, and the passage from milestone 4 to milestone 5 needs uniqueness of the Laplace transform.

Formalization scope

• Brownian motion is Mathlib's ProbabilityTheory.IsBrownianReal B P with B : ℝ≥0 → Ω → ℝ, plus the hypothesis that every sample path is continuous (the standard choice of a continuous version). Time is ℝ≥0.
• $S_t$ and $I_t$ are the real sSup/sInf of the path over the interval $[0,t]$; with continuous paths they are attained. The supremum is never taken over all times or in extended reals.
• "$E$" is the Bochner integral, and every expectation identity also asserts integrability, so no identity can hold through Lean's convention that a non-integrable function integrates to $0$.
• "$T$ exponential with mean $\lambda^{-1}$" is HasLaw T (expMeasure λ) P; "parameter $\alpha$" is read as rate $\alpha$. "Independent of $B$" is independence from the path-valued random variable with the product σ-algebra. $S_T$ is evaluated at $T$ truncated to $[0,\infty)$.
• "Has the same law as" is equality of image measures, together with the almost-everywhere measurability of both maps.
• "Inversion of the Laplace transform gives" becomes the fixed-time identity for every $t\ge0$ (milestones 5 and 6), separate from the Laplace identity (milestone 4).
• Milestones 1 and 3 assume $\sigma>0$ because $\alpha,\beta$ divide by $\sigma^2$; the Wiener–Hopf splitting, the goal, and milestones 4–7 allow $\sigma\ge0$.

A formalization that specializes to $c=0$, takes the supremum over all of $[0,\infty)$, or omits the integrability conjuncts is not the statement of this mission.

Infrastructure that a complete development needs: the reflection principle or the strong Markov property for Brownian motion, the exponential-time law of the running maximum of a Lévy process, and uniqueness of Laplace transforms for continuous functions. All of these are reusable; contributions of any of them are welcome. Related platform items cover other objects and are credited here: running maxima and exit problems for spectrally negative Lévy processes (Avram2004.Exit.reflected), a drifted Brownian motion in characteristic-function form in a queueing-network setting (Reiman84.QueueLength.Paths), and a GI/G/1 Wiener–Hopf transform identity (QueueingFundamentals.GG1.wiener_hopf_transform).

Selected references

• L. C. G. Rogers and S. E. Satchell, Estimating variance from high, low and closing prices, The Annals of Applied Probability 1(4), 1991, 504–512. https://doi.org/10.1214/aoap/1177005835
• M. B. Garman and M. J. Klass, On the estimation of security price volatilities from historical data, Journal of Business 53(1), 1980, 67–78. https://doi.org/10.1086/296072
• M. Parkinson, The extreme value method for estimating the variance of the rate of return, Journal of Business 53(1), 1980, 61–65. https://doi.org/10.1086/296071
• P. Greenwood and J. Pitman, Fluctuation identities for Lévy processes and splitting at the maximum, Advances in Applied Probability 12(4), 1980, 893–902. https://doi.org/10.2307/1426747