All missions

Why expected interval length matters

A simulation run often estimates a steady-state mean without producing independent observations. A confidence interval must account for dependence in the output, and the relevant variance constant may be unknown. Standardized time series (STS) methods use the shape of an integrated output path to cancel that constant rather than estimating it separately. The resulting interval can be computed from one run, but its length can vary substantially with the chosen standardizing functional. Glynn and Iglehart introduced a common functional framework for these methods and asked how short their expected intervals can be as the run grows. Their 1990 paper identifies a universal lower bound.

The comparison is operational. A shorter confidence interval conveys a more precise estimate at the same nominal coverage. The authors also compare STS with procedures that consistently estimate the variance constant. They state that the lower bound is attained by the latter procedures and approached, but not attained, by STS intervals. The present mission isolates the bound for STS itself, Corollary 4.16. It does not make the claim that a particular STS rule attains it. This distinction follows the paper's introduction and §4.

The stochastic setting

Let $Y(t)$ be a real simulation output process for $t\ge0$. Its integrated average path at run length $n$ is $\overline Y_n(t)=n^{-1}\int_0^{nt}Y(s)\,ds$ for $0\le t\le1$. The unknown steady-state mean is $\mu$. The paper assumes a functional central limit theorem in the space $C[0,1]$ of continuous real paths:

$$X_n(t):=\sqrt n\bigl(\overline Y_n(t)-\mu t\bigr) \ \Rightarrow\ \sigma B(t),\qquad \sigma>0,$$

where $B$ is standard Brownian motion. Convergence is weak convergence of random continuous paths in the uniform topology. This is Assumption (2.1), rather than a claim that every output process satisfies it. The paper lists several classes of processes for which such a theorem is available under further conditions (§2, pp. 2–3).

An STS scale functional $g:C[0,1]\to\mathbb R$ belongs to $\mathcal M$ when it is measurable, positively homogeneous, unchanged by subtracting any multiple of the identity path $k(t)=t$, positive at $B$ almost surely, and continuous at $B$ almost surely. The last two conditions ensure that the Brownian ratio is a meaningful distributional limit. The paper also describes these functionals through the bridge map $(\Gamma x)(t)=x(t)-t x(1)$: a member of $\mathcal M$ can be written as $b\circ\Gamma$ for a suitable $b$. Thus the scale is determined by a Brownian bridge while the endpoint $B(1)$ is independent of it (Propositions 2.7–2.8).

Define $H(x)=P\{B(1)/g(B)\le x\}$. For a confidence level $1-\delta$, choose endpoints $\alpha,\beta$ with $H(\beta)-H(\alpha)=1-\delta$. The STS confidence interval from equation (2.10) has endpoints $\overline Y_n(1)-g(\overline Y_n)\beta$ and $\overline Y_n(1)-g(\overline Y_n)\alpha$. Its length is $L_n=g(\overline Y_n)(\beta-\alpha)$. Here $\delta$ lies strictly between zero and one; the endpoint equation is part of the construction, not an arbitrary choice.

Formalization target

The goal is Corollary 4.16 for every nonnegative $g\in\mathcal M$ under Assumption (2.1). Write $\Phi$ for the standard normal distribution function and $p=\Phi^{-1}(1-\delta/2)$. Then

$$\liminf_{n\to\infty}\sqrt n\,E[L_n] \ \ge\ 2\sigma p =2\sigma\Phi^{-1}(1-\delta/2).$$

The expectation and liminf admit $+\infty$. The statement does not impose an integrability assumption that would remove that case. It quantifies over every admissible STS functional and every interval whose endpoints have the specified Brownian confidence mass (Corollary 4.16, p. 12).

Three substantial targets precede the corollary. Proposition 4.1(a) relates scaled expected length to $\sigma E[g(B)](\beta-\alpha)$. Proposition 4.3 says a symmetric choice of $\alpha,\beta$ minimizes $\beta-\alpha$. Theorem 4.8 gives $E[g(B)]\Phi^{-1}_g(1-\delta/2)\ge\Phi^{-1}(1-\delta/2)$, where $\Phi^{-1}_g$ denotes the quantile of $H$. The milestone list also includes the cited Brownian independence, mixture distribution, scale invariance, and continuous mapping statements that put these targets in context.

What the bound establishes

The corollary supplies a benchmark for the asymptotic expected length of any interval in this STS class. A proposed standardizing functional cannot beat the normal-quantile constant while retaining the stated functional limit and confidence construction. It also identifies the quantity against which the paper's other interval procedures can be compared. The bound applies uniformly to the class $\mathcal M$, not to a chosen batch size or a particular form of $g$ (Glynn–Iglehart 1990, §4).

The mathematical result has been proved in the source paper. This mission supplies formal statements and their shared definitions as proof targets; it does not claim that their Lean proofs already exist. A complete development would formalize the known arguments for the milestones and corollary, including the Brownian path representation, weak convergence, quantile properties, and expectation inequalities. Those components could be reused in other work on simulation output analysis and ratios of weakly convergent processes.

Where the formal proof is demanding

Weak convergence alone does not imply convergence of expectations. In particular, a continuous mapping limit for $g(X_n)$ cannot simply be integrated as an ordinary finite real expectation when the family is not uniformly integrable. Proposition 4.1(a) asks only for a lower bound, and its statement must still account for $E[g(B)]=+\infty$. This is why the goal is expressed with a liminf and extended nonnegative expectations rather than a real-valued limit. A separate difficulty is that the interval width depends jointly on a distributional scale and a choice of two quantiles. Bounding either one in isolation does not state the corollary.

Formalization scope and conventions

Paths are Mathlib's $C([0,1],\mathbb R)$ with its uniform metric and Borel sigma algebra. A standard Brownian motion is a measurable random continuous path agreeing with an $\mathbb R_{\ge0}$-indexed real Brownian motion on $[0,1]$. The paper's discontinuity set $D(g)$ is the set where $g$ is not continuous. Assumption (2.1) includes joint measurability of $Y$ and finite-interval pathwise integrability so that each integrated average is defined. The path $\overline Y_n$ is supplied together with its defining integral equation, which determines it pointwise. Its values are not free parameters.

Indices $n$ are natural numbers. At $n=0$, the average uses Lean's total division and is zero; this initial value does not affect an asymptotic statement. The positive Brownian scale $\sigma$ is finite. The parameters satisfy $0<\delta<1$, and $H(\beta)-H(\alpha)=1-\delta$. The normal and STS quantiles appear as real parameters pinned by their distribution-function equations, avoiding an unbounded or empty real infimum. Expected nonnegative lengths and scales are integrals valued in $\mathbb R_{\ge0}\cup\{+\infty\}$. The class $\mathcal N$ explicitly requires measurability of $b$, the standing convention needed for its equality with $\mathcal M$.

The corollary retains the entire class $\mathcal M$ and Assumption (2.1), with $g\ge0$ on all continuous paths. It cannot be replaced by a statement about a single easy functional or by assuming the bound on an auxiliary criterion. Useful contributions include the Brownian bridge independence theorem, the normal scale-mixture identity, distribution-function regularity, and the asymptotic expectation result.

Selected references

• P. W. Glynn and D. L. Iglehart, Simulation output analysis using standardized time series, Mathematics of Operations Research 15(1):1–16, 1990. DOI: 10.1287/moor.15.1.1.

Why arrival averages and time averages agree

Queueing analysis constantly moves between two kinds of long-run averages: the fraction of time a system spends in some set of states, and the fraction of arriving customers who find it there. Waiting-time formulas for the M/G/1 queue, blocking probabilities in loss systems and many decomposition arguments rest on the claim that, when arrivals form a Poisson process, the two coincide. This property is known as PASTA, Poisson Arrivals See Time Averages. It is used throughout queueing theory, inventory theory and the analysis of communication networks, usually without proof.

Before 1982 the property had been proved under strong extra structure:

• Strauch (1970) proved an instantaneous version, at a fixed time point, which does not by itself give limit theorems.
• Wolff (1970) proved a limit theorem for a stationary observed process, using particular properties of its interaction with the Poisson stream.
• Stidham (1972) proved a limit theorem for regenerative processes, under restrictions on how regeneration points relate to the arrivals.
• Wolff (1982), the source of this mission, proved the limit theorem with no stationarity, regeneration or ergodicity at all. The only link assumed between system and arrivals is that the system does not anticipate future arrivals. The proof uses Watanabe's (1964) martingale characterization of the Poisson process.
• Melamed and Whitt (1990) recast the result as one instance of a general "arrivals see time averages" (ASTA) principle for arbitrary point processes.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. On it live a process $N=\{N(t),t\ge0\}$, the state of a system, with values in an arbitrary measurable space, and a Poisson process $A=\{A(t),t\ge0\}$ at rate $\lambda>0$, counting customer arrivals in $(0,t]$. The interaction between $A$ and $N$ is unspecified: arrivals may change the state.

Fix a set $B$ of states with $\{N(t)\in B\}\in\mathcal F$ for every $t\ge0$, and define

$$U(t)=\mathbf 1\{N(t)\in B\},\qquad V(t)=t^{-1}\int_0^tU(s)\,ds,\qquad Y(t)=\int_0^tU(s)\,dA(s),\qquad Z(t)=\frac{Y(t)}{A(t)}.$$

$V(t)$ is the fraction of time in $[0,t]$ that $N$ is in $B$. $Y(t)$ is the number of arrivals up to $t$ who find $N$ in $B$, and $Z(t)$ is the fraction of arrivals who do.

The paths of $U$ are assumed left continuous with right-hand limits w.p. 1, so that an arrival is not counted as already present at its own arrival epoch. $U$ is assumed jointly measurable in $(\omega,t)\in\Omega\times[0,\infty)$. The single structural assumption is the Lack of Anticipation Assumption (LAA):

for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ and $\{U(s),0\le s\le t\}$ are independent.

The paper's proof of (6) uses this independence for every event of $\mathcal F_t$, the σ-field generated by $\{A(s),U(s);0\le s\le t\}$. The mission therefore states Theorems 1–2, (6), Lemma 1, (10) and Lemma 2 under lack of anticipation with respect to $\mathcal F_t$: for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ is independent of $\mathcal F_t$. This implies the printed LAA. The printed LAA together with independent increments does not give (6) or Lemma 1, because pairwise independence of the future from the past of $A$ and from the past of $U$ is not independence from their joint past.

Formalization targets

Goal: Theorem 1 (p. 225)

Under lack of anticipation (with respect to $\mathcal F_t$, see above), for every random variable $V(\infty)$,

$$V(t)\to V(\infty)\ \text{w.p. 1}\quad\Longleftrightarrow\quad Z(t)\to V(\infty)\ \text{w.p. 1},\qquad t\to\infty.$$

The limit may be random, and the theorem asserts nothing about whether either average converges. It asserts only that the two converge together, to the same limit.

Milestones

The proof in §2 passes through the following statements, which form the milestone list:

1. (2), (3): $E\{Y(t)\}=\lambda tE\{V(t)\}=\lambda E\{\int_0^tU(s)\,ds\}$.
2. (6): $E\{Y(t+h)-Y(t)\mid\mathcal F_t\}=\lambda E\{\int_t^{t+h}U(s)\,ds\mid\mathcal F_t\}$.
3. Lemma 1: $R(t)=Y(t)-\lambda tV(t)$ is a martingale.
4. (7): the second-moment bound $E\{R^2(t)\}\le\lambda t+2\lambda^2t^2$.
5. (10): the grid strong law $R(nh)/n\to0$ w.p. 1.
6. (11): the pathwise interpolation bound between grid points.
7. Lemma 2: $R(t)/t\to0$ w.p. 1.
8. The strong law $A(t)/t\to\lambda$ for the Poisson process.

Companion: Theorem 2 (p. 228)

For a Poisson process with bounded, integrable rate $\lambda(t)$ and $\Lambda(t)/t\to\bar\lambda\in(0,\infty)$, where $\Lambda(t)=\int_0^t\lambda(s)\,ds$, the same equivalence holds with $V(t)$ replaced by the rate-weighted average $\bar V(t)=\Lambda(t)^{-1}\int_0^tU(s)\lambda(s)\,ds$. Display (12), $E\{Y(t)\}=\int_0^tE\{U(s)\}\lambda(s)\,ds$, is its analogue of (3).

Significance

Theorem 1 justifies replacing customer averages by time averages, and conversely, in any model where arrivals are Poisson and the system does not anticipate them. Examples are queue-length distributions seen by arrivals in M/G/c systems, blocking probabilities in Erlang loss models, and state probabilities at arrival epochs in networks with Poisson external input. It needs no ergodic theory of the observed process: convergence of one average has to be established separately, by whatever means suit the model, and the theorem transfers it to the other. Lemma 2 also implies versions of PASTA under weaker modes of convergence (Remark 6).

The result has been proved for four decades and is textbook material. What this mission adds is a machine-checked proof. No formalization of Theorem 1 in a proof assistant is known. A complete development would also contain machine-checked versions of several standard facts not yet available in Mathlib:

• the strong law for the Poisson process;
• a strong law for square-integrable martingale differences;
• Stieltjes integration against a counting path.

Difficulty

The naive argument conditions on the arrival epochs and claims that each arrival "samples" the state at a uniformly random time. This fails because arrivals influence the state: after an arrival, a queue-length process is no longer independent of the arrival stream. LAA only says that the future increments of $A$ are independent of the past of $U$. The difficulty is to turn this one-sided independence into an almost-sure statement about long-run averages, along every path and at all times rather than only at fixed ones.

On the technical side, the expected-value identity (3) needs a limit of grid sums. That limit relies on left continuity: without it, $U(t)=\mathbf 1\{A \text{ jumps at } t\}$ satisfies LAA with $V\equiv0$ but $Z\equiv1$. The passage from expectations to a strong law needs a martingale structure and a second-moment bound, and the interpolation between grid times needs a pathwise argument.

Formalization scope

• Time and paths. Time is $\mathbb R$, and every hypothesis concerns $t\ge0$ only. Processes are maps $\mathbb R\to\Omega\to(\cdot)$. A Poisson process with intensity function $\lambda(\cdot)$ is a counting process $A:\mathbb R\to\Omega\to\mathbb N$ with $A(0)=0$, every path non-decreasing and right-continuous, Poisson-distributed increments with mean $\int_s^t\lambda$, and independent increments over any finite increasing sequence of times. The constant-rate case is Theorem 1's setting.
• The averages. $Y(t)$ is encoded as $\sum_{k=1}^{A(t)}U(T_k)$ over the arrival epochs $T_k=\inf\{s\ge0:A(s)\ge k\}$, which is the Lebesgue–Stieltjes integral $\int_{(0,t]}U\,dA$ with multiplicities. $Z(t)=0$ when $A(t)=0$, and $V(0)=0$; limits do not see these values.
• The standing hypotheses. These are carried as binders of the goal: measurability of $\{N(t)\in B\}$ for $t\ge0$, path regularity w.p. 1 (left continuity at $t>0$, right limits at $t\ge0$), joint measurability on $\Omega\times[0,\infty)$, and lack of anticipation as independence of the σ-field of future increments of $A$ from $\mathcal F_t$. The milestones (2), (3), (7) and (11) need less: (2) and (3) are stated under the printed LAA, and (7) and (11) under no independence assumption at all.
• The limit and the expectations. $V(\infty)$ is an arbitrary function $\Omega\to\mathbb R$, shared by both sides of the equivalence. Expectations in the milestones come with integrability conclusions, or are lower integrals in $[0,\infty]$, so that no identity holds through Lean's junk value $0$ for non-integrable functions.
• Ruled out. A formalization in which $V(\infty)$ is quantified separately on each side, which loses "to the same limit". A goal that assumes Lemma 2, (3) or the strong law $A(t)/t\to\lambda$ as a hypothesis. A definition of $Y$ that counts distinct jump times and not arrivals.

Welcome contributions:

• a reusable Poisson-process library: the strong law, square moments, independence of increments from a past σ-field;
• a martingale strong law of Feller's type;
• Stieltjes sums against counting paths.

All of these are useful well beyond this mission.

Selected references

• R. W. Wolff, Poisson Arrivals See Time Averages, Operations Research 30(2):223–231, 1982. https://doi.org/10.1287/opre.30.2.223
• S. Watanabe, On discontinuous additive functionals and Lévy measures of a Markov process, Japanese Journal of Mathematics 34:53–70, 1964. https://doi.org/10.4099/jjm1924.34.0_53
• B. Melamed and W. Whitt, On arrivals that see time averages, Operations Research 38(1):156–172, 1990. https://doi.org/10.1287/opre.38.1.156
• P. Brémaud and J. Jacod, Processus ponctuels et martingales: résultats récents sur la modélisation et le filtrage, Advances in Applied Probability 9(2):362–416, 1977. https://doi.org/10.2307/1426091
• S. Stidham, Regenerative processes in the theory of queues, with applications to the alternating-priority queue, Advances in Applied Probability 4(3):542–577, 1972.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.

Motivation

An assembly system must coordinate the production of components that meet at a common downstream item. A shortage of any required component can delay the finished product, while producing a component too early incurs holding cost. In Rosling's 1989 study, the central question is whether optimal decisions for such a tree can be understood using the simpler theory of a pure series inventory system. The paper proves an equivalence when the initial inventory positions are in a condition it calls long-run balance. That equivalence gives a precise route from an assembly network to serial inventory control without discarding its lead times or its discounted costs.

Setting

There are items $1,\ldots,N$ in a tree rooted at end item $1$. Every item $i>1$ has one immediate successor $s(i)<i$; one unit of each component is needed for an end unit. Let $l_i$ be the production or delivery lead time of item $i$. The total lead time $M_i$ is the sum of lead times on the path from $i$ to the end item, with $M_0=0$, and the equivalent lead time is $L_i=M_i-M_{i-1}$. Items are indexed so that $M_i$ is nondecreasing. These definitions and indexing conditions are in §§1–2 of the paper.

At the beginning of each period $t$, outstanding orders arrive, the controller chooses the post-order echelon position $Y_{it}$, and then demand $\xi_t$ for the end item occurs. The pre-order position is $X_{it}$, while $X^l_{kt}$ is the position of predecessor $k$ from orders old enough to arrive after its lead time. A decision is feasible when $X_{it}\le Y_{it}\le X^l_{kt}$ for every immediate predecessor $k$ of $i$. Decisions depend only on demands already observed. The demands are independent and identically distributed, nonnegative, and have a density and a finite positive mean.

The discounted Problem P charges echelon holding cost $h_i$ for item $i$ and a shortage coefficient $p+H_1$ for the end item. Its discount factor is $\alpha$. The objective is the expectation of the sum over periods of the holding charges and the expected end-item shortfall over $l_1+1$ demands, with a constant independent of the policy. The paper's Assumption requires every $h_i>0$ and $\sum_i h_i\alpha^{-M_{s(i)}}<p+H_1$. The system is in long-run balance in period $t$ when positions of adjacent items, compared at the same age relative to total lead time, satisfy equation (5):

$$X^{M_i-\mu}_{it}\le X^{M_{i+1}-\mu}_{i+1,t} \quad(1\le i<N,\ 0\le\mu<M_i).$$

Formalization targets

Equivalent series optimal policies

The equivalent series system has successor $i-1$, lead time $L_i$, the same demand law and shortage coefficient, and holding coefficient $h_i\alpha^{l_i-L_i}$. Theorem 2 states that its optimal policies and those of the assembly system agree when the assembly system is initially in long-run balance. In the formal statement, the first inclusion is unconditional; the reverse inclusion is conditional on Problem P attaining an optimum:

$$\operatorname{Opt}(P)\subseteq\operatorname{Opt}(P_{\mathrm{series}}), \qquad \operatorname{Opt}(P)\ne\varnothing \Longrightarrow \operatorname{Opt}(P_{\mathrm{series}})\subseteq\operatorname{Opt}(P).$$

The target includes Lemmas 1 and 2, Theorem 1, Corollary 1, and the cost identity displayed in the proof of Theorem 2. Lemma 1 limits excess production, Lemma 2 gives a production lower bound, Theorem 1 describes when long-run balance is reached and preserved, and Corollary 1 uses the adjacent series position in that result. Each is stated at the strength given on pp. 568–569 of the paper.

Significance

Theorem 2 identifies the same policy choices in a tree assembly problem and a series problem whose stages have modified lead times and holding coefficients. It makes the serial interpretation exact for initially balanced systems and supports the paper's later discussion of series-system calculations. The statement is an equivalence of optimal policies, rather than just an equality of numerical values, so both the feasible-policy comparison and the cost comparison matter.

The theorem and its supporting results are proved in the 1989 paper; they have not been machine-checked in this development. A complete formalization would supply a reusable account of finite-history inventory policies, random demand histories, echelon positions, and extended-real discounted objectives. The published serial model SupplyChainTheory_multiechelon represents a different stage-indexed system; the assembly tree, its initial pipeline, and Problem P still need their own definitions. The paper's order-up-to Corollary 2 relies on an extension of earlier serial results and is outside this target.

Difficulty

The first natural comparison is to replace the tree's predecessor constraints with adjacent-item constraints. Those feasible sets are not equal for arbitrary states: positions at different total lead times can cross, and initial orders placed before period 1 affect the earliest periods. Long-run balance controls the necessary position comparisons, but equation (5) is empty for an item with $M_i=0$. The printed proof also uses a middle inequality outside the range covered by equation (5) when an equivalent lead time vanishes. A faithful statement must account for these boundary cases without defining the series problem through the assembly problem's optimal policies.

Formalization scope

Items use the paper's indices $1,\ldots,N$, with $N\ge1$ and $s(1)=0$. Lean period $k$ is paper period $t=k+1$; the policy sees exactly $k$ earlier demands. The common demand law $\nu$ is a probability measure on the reals, concentrated on nonnegative values, absolutely continuous with respect to Lebesgue measure, integrable, and of positive mean. The law of demand over $l_1+1$ periods is the pushforward of a finite product law under summation. Feasibility and the optimal-policy bounds are almost-sure statements, so changes on null histories do not alter them. Pathwise balance results quantify over one nonnegative demand path.

Initial positions include the orders placed before period 1. Their ages are monotone and obey the predecessor constraints inherited from that past. In addition to the paper's initial long-run balance, a separate boundary condition carries the missing comparison when $M_i=0$. Discounting is restricted to $0<\alpha<1$: at $\alpha=1$ the paper specifies average cost through a separate limiting prescription. The formal cost lies in the extended reals and is computed from its positive and negative parts; under the Assumption, feasible policies have a finite negative part. The policy-independent constant of equation (2) is omitted from both systems. “Optimal” means feasible and no more costly than every feasible policy, never a default value of an empty infimum.

The series system is built as a second instance of the same model, using the paper's successor, lead-time, and holding-coefficient transformations. Its cost and constraint (3) are then computed by the shared definitions. Contributions toward the lead-time identities, almost-sure policy comparisons, finite-time balance theorem, and extended-real cost identity are all part of the scope.

Selected references

• Kaj Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. DOI: 10.1287/opre.37.4.565.

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

Motivation

A convex minimization problem comes with a dual maximization problem, and the dual value never exceeds the primal value. When the two values differ, a duality gap occurs. Dual bounds, Lagrangian relaxations and optimality certificates are then weaker than hoped. Conditions that rule the gap out are constraint qualifications such as Slater's condition and Rockafellar's notion of a stably set problem. Such conditions say when the gap vanishes, but not what the dual value is when it does not.

R. T. Rockafellar's 1967 paper answers that question for the Fenchel-type pair of problems built from a convex function, a concave function and a continuous linear map between infinite-dimensional spaces. Its Theorem 6 (§6, "Weak duality theorems", pp. 179–180) "explains the exact way in which inf (P) and sup (P*) can fail to be equal", by expressing the dual value through the primal problem alone: the dual supremum is the lower limit of the optimal values of slightly perturbed primal problems. This perturbational view of duality was later developed in Rockafellar's Conjugate Duality and Optimization (1974). It underlies the modern treatment of value functions in convex optimization.

Setting

Two real vector spaces $E$ and $E^*$ are topologically paired when each carries a locally convex Hausdorff topology, they are in duality under a bilinear form $\langle x,x^*\rangle$ that is continuous in each variable, and every continuous linear functional on either space is the pairing with exactly one element of the other. Let $(E,E^*)$ and $(F,F^*)$ be two such pairs. Let $A:E\to F$ be continuous linear and $A^*:F^*\to E^*$ its adjoint, the continuous linear map with $\langle Ax,y^*\rangle=\langle x,A^*y^*\rangle$.

A function $f:E\to[-\infty,+\infty]$ is convex when its epigraph $\{(x,\mu)\mid\mu\in\mathbb R,\ \mu\ge f(x)\}$ is convex in $E\times\mathbb R$. It is proper when it never takes $-\infty$ and is finite somewhere. A function $g$ is proper concave when $-g$ is convex, $g$ never takes $+\infty$, and $g$ is finite somewhere. The standing hypotheses are that $f$ is lower semicontinuous proper convex on $E$ and $g$ is upper semicontinuous proper concave on $F$. Their conjugates are

$$f^*(x^*)=\sup_{x}\{\langle x,x^*\rangle-f(x)\},\qquad g^*(y^*)=\inf_{y}\{\langle y,y^*\rangle-g(y)\}.$$

The primal problem (P) is to minimize $f(x)-g(Ax)$ over $x\in E$. The dual problem (P*) is to maximize $g^*(y^*)-f^*(A^*y^*)$ over $y^*\in F^*$. For $z\in F$ the perturbed problem (P($z$)) is to minimize $f(x)-g(Ax-z)$. Its value defines the perturbation function

$$h(z)=\inf(\mathrm P(z))=\inf_{x\in E}\{f(x)-g(Ax-z)\},\qquad h(0)=\inf(\mathrm P).$$

The lower semicontinuous hull of $h$ is $\bar h(y)=\liminf_{z\to y}h(z)$, where $z=y$ is allowed, so that $\bar h\le h$. All infima and suprema are taken in $[-\infty,+\infty]$.

Formalization targets

Goal: Theorem 6

$$\sup(\mathrm P^*)=\liminf_{z\to 0}\,[\inf(\mathrm P(z))],$$

valid except in the trivial case where the left side is $-\infty$ and the right side is $+\infty$. No consistency, constraint qualification or attainment is assumed, and neither side need be finite. The exception is exactly the stated conjunction. A version assuming (P) consistent would be weaker, since an inconsistent (P), with $h(0)=+\infty$, may still have a finite lower limit.

Milestones: the four claims of the proof (p. 180)

1. $\bar h$ is a lower semicontinuous convex function on $F$.
2. For every $y^*\in F^*$, with $\bar h^*(y^*)=\sup_y\{\langle y,y^*\rangle-\bar h(y)\}$,

$$-\bar h^*(y^*)=\inf_y\{\bar h(y)-\langle y,y^*\rangle\}=\inf_z\{h(z)-\langle z,y^*\rangle\}=g^*(y^*)-f^*(A^*y^*).$$

3. (6.2): if $\bar h$ is proper, then $\bar h(0)=\sup_{y^*}\{\langle 0,y^*\rangle-\bar h^*(y^*)\}$.
4. If $\bar h$ is not proper, the maximand $g^*(y^*)-f^*(A^*y^*)$ of (P*) is identically $-\infty$.

The paper's Lemma 2 (convexity of $h$) is used by the first claim. It is a milestone of the companion mission on Theorem 3 of the same paper and is not restated here.

Significance

Theorem 6 reduces every question about the dual value to a question about the primal value function near the origin. Strong duality $\inf(\mathrm P)=\sup(\mathrm P^*)$ holds exactly when $h$ is lower semicontinuous at $0$ (outside the trivial case). A duality gap is exactly a downward jump of $h$ at $0$. The dual of (P*) obeys the same formula, which the paper uses to derive Theorem 7 on normal problems. An integer-lattice analogue appears in discrete convex analysis (Murota, Theorem 8.53, whose duality relation is already stated on Prove2Me as DiscreteConvex.ConjugacyDualityD.general_duality_relations). That statement has no topology and is not the same theorem.

The result is classical and its proof is published. As far as the platform's index shows, no machine-checked statement of it exists in the paper's generality, nor a statement of extended-real biconjugation on general paired locally convex spaces. The value of the mission is a formal proof in the paper's setting: arbitrary topologically paired spaces, extended-real-valued functions, and both the proper and the improper case of the hull. The biconjugation milestone (6.2) and the hull lemma are reusable for other perturbational duality results.

Difficulty

The obvious argument compares $h(0)$ with the dual objective directly. It cannot give the theorem, because $h$ may jump at $0$, and the dual objective does not detect the value of $h$ at a single point: the target is a lower limit, not a value. In infinite dimensions, conjugacy recovers a function only when it is lower semicontinuous and convex for a topology compatible with the pairing, so the statement depends on the full compatibility of the pairing on $F$, not on a norm. The usual statements of biconjugation cover proper functions only, whereas here the lower limit may take both values $\pm\infty$, and both cases of the theorem must be covered. Finally, extended-real arithmetic must be tracked so that the dual objective, defined from $f^*$, $g^*$ and $A^*$, is matched in every infinite case.

Formalization scope

Values lie in EReal. Infima and suprema are complete-lattice ⨅ and ⨆, so an empty or unbounded family gives $\pm\infty$ as in the paper. The lower limit is Filter.liminf h (nhds y) over the full neighbourhood filter: a punctured limit would change the theorem. Convexity is epigraph convexity in $E\times\mathbb R$, and properness is the paper's two-sided condition. A topological pairing is a structure holding a bilinear map, separate continuity, and existence and uniqueness of representing elements in both directions. No norm, inner product or finite dimension is assumed. The adjoint $A^*$ is continuous linear data satisfying the adjoint identity. The conjugates $f^*$, $g^*$ are defined by the paper's formulas from $f$, $g$, so their regularity is a consequence, not a hypothesis. Properness of $f$ and $g$ excludes the form $(+\infty)-(+\infty)$ from $f(x)-g(Ax-z)$ and from $g^*(y^*)-f^*(A^*y^*)$. No statement is repaired relative to the page.

The dual value is the supremum of the maximand built from $f^*$, $g^*$ and $A^*$ as on p. 172. Defining $\sup(\mathrm P^*)$ through $\bar h$ (for instance as the biconjugate of $\bar h$ at $0$) would make Theorem 6 true by definition and is ruled out.

A complete development needs extended-real conjugates on paired spaces, the lower semicontinuous hull and the closure of a convex epigraph, and Fenchel–Moreau for proper lower semicontinuous convex functions on a locally convex space. All of these are reusable beyond this mission. Proofs of the milestones, and lemmas toward Fenchel–Moreau in this generality, are welcome contributions.

Selected references

• R. T. Rockafellar, Duality and Stability in Extremum Problems Involving Convex Functions, Pacific J. Math. 21 (1967), 167–187. https://doi.org/10.2140/pjm.1967.21.167
• W. Fenchel, On conjugate convex functions, Canad. J. Math. 1 (1949), 73–77. https://doi.org/10.4153/CJM-1949-007-x
• A. Brøndsted, Conjugate convex functions in topological vector spaces, Mat.-Fys. Medd. Dansk. Vid. Selsk. 34 (1964) (reference [2] of the paper; no DOI).
• J.-J. Moreau, Fonctions convexes en dualité, multigraph, Séminaires de Mathématique, Faculté des Sciences, Université de Montpellier, 1962 (reference [12] of the paper; no DOI).
• R. T. Rockafellar, Conjugate Duality and Optimization, CBMS-NSF Regional Conference Series in Applied Mathematics 16, SIAM, 1974. https://doi.org/10.1137/1.9781611970524
• K. Murota, Discrete Convex Analysis, SIAM, 2003, Theorem 8.53. https://doi.org/10.1137/1.9780898718508

Motivation

Demand for many products does not arrive at a constant rate. It moves with an underlying environment: the economy, the season, a product's life-cycle stage, the state of a customer's own operations. Song and Zipkin (Oper. Res. 41(2):351–370, 1993) modelled this environment as a continuous-time Markov chain, the world, whose current state sets the Poisson demand rate, and showed that a basestock policy whose level depends on the current world state is optimal under linear order costs. Missions I and II of this series formalize those optimality results.

A practitioner who uses such a policy wants to know how the levels depend on the world. If a higher world state means more demand now and more demand later, a higher level should be kept. That is what intuition says, but the optimal level depends on the whole future of the world chain, not only on the current demand rate. §4 of the paper answers it for a world with an arbitrary partial order, which covers several independent demand drivers at once.

Setting

The world $A$ is a continuous-time Markov chain on a countable set $\mathbf I$ with generator $Q = (q_{ij})$, $q_i = -q_{ii}$, and bounded rates $q^* = \sup_i q_i$, $\lambda^* = \sup_i \lambda_i$. While $A = i$, unit demands arrive at rate $\lambda_i$, all demand is backlogged, and orders arrive after a random lead time $L$ that is independent of the world and the demand. Costs are discounted at rate $\alpha > 0$. With the unit order cost $\bar c$, holding rate $h$ and penalty rate $p$, set $c = \bar c\,E[e^{-\alpha L}]$ and

$$\hat C(x) = \max\{-px,\ hx\}, \qquad C(i,y) = E\big[e^{-\alpha L}\hat C(y - D^i_L)\big],$$

where $D^i_L$ is the demand during a lead time when the world starts in $i$. Uniformizing at a rate $\mu \ge q^* + \lambda^*$ with $\beta = 1/(\mu+\alpha)$ and $\gamma = \beta\mu$, the myopic cost is $G^+(i,y) = (1-\gamma)cy + \beta C(i,y)$. The linear-cost model ($K = 0$) is solved by value iteration from $W_0 \equiv 0$:

$$G_n(i,y) = G^+(i,y) + \beta\lambda_i c + \beta\Big\{\lambda_i W_{n-1}(i,y-1) + \sum_{j\ne i} q_{ij}W_{n-1}(j,y) + (\mu-\lambda_i-q_i)W_{n-1}(i,y)\Big\},$$

$W_n(i,x) = \min_{y\ge x} G_n(i,y)$, with limits $G_\infty$ and $W_\infty$. The myopic level $y^+(i)$, the finite-horizon levels $y^*_n(i)$ and the optimal level $y^*(i)$ are the smallest minimizers of $G^+(i,\cdot)$, $G_n(i,\cdot)$ and $G_\infty(i,\cdot)$, and $y^*_\infty(i) = \lim_n y^*_n(i)$. Throughout, $\alpha\bar c < p$ (Assumption 1).

The world states carry a partial order $\preceq$. The chain is stochastically partial-monotone (display (14)) if for every $i \preceq j$ there is a probability space carrying copies of $A$ started at $i$ and at $j$ whose paths satisfy $A(t) \preceq A'(t)$ for all $t \ge 0$ almost surely. Condition 1 requires this together with $\lambda_i$ nondecreasing in $i$.

Formalization targets

Goal: Theorem 8

Under Condition 1, the three families of levels exist and are nondecreasing along $\preceq$:

$$i \preceq j \ \Longrightarrow\ y^+(i) \le y^+(j),\qquad y^*(i) \le y^*(j),\qquad y^*_\infty(i) \le y^*_\infty(j).$$

Milestones

• Lemma 8, with its fixed-lead-time form from the proof: $D(l)$ given $A(0)=i$ is stochastically smaller than given $A(0)=j$ for each $l \ge 0$, and $D^i_L \le_{st} D^j_L$.
• Lemma 9: $\Delta C(i,y) \ge \Delta C(j,y)$ for $i \preceq j$.
• Theorem 7: for all $n \ge 1$ and fixed $x$, $\Delta W_{n-1}(i,x)$ and $\Delta G_n(i,x)$ are nonincreasing in $i$, and $y^*_n(i)$ is nondecreasing in $i$.
• Theorem 9 (companion): if $q_{ij} \ne 0$ only for $j \succeq i$, then $y^*(i) = y^+(i)$, so the myopic policy is optimal.
• Theorem 10 (companion): with a fixed order cost $K > 0$, the bounds $S^+(i)$, $r^+(i)$, $r^-(i)$, $r^{--}(i)$ on the optimal $(r,S)$ parameters are nondecreasing in $i$.

Significance

Theorem 8 turns an optimal policy into a structured one. A world-dependent basestock policy has one level per world state; monotonicity says the levels follow the order of the states, which reduces search, makes the levels interpretable, and gives sanity checks for computed solutions. Theorem 9 identifies when nothing beyond the one-step cost needs to be computed at all. Theorem 10 is the paper's substitute for an open question: the authors could not show that the optimal $(r,S)$ parameters are monotone, and instead bound them between monotone functions.

All of these results are proved in the paper. None of them has been machine-checked. The formalization requires a value-iteration argument for a model with unbounded one-period costs, a coupling argument for Markov-modulated Poisson demand, and the passage to the limit in the levels. These are the ingredients of most monotone-policy results in inventory theory with Markov-modulated demand.

Difficulty

The obvious argument fails at the generator. For a single scalar world, stochastic monotonicity is equivalent to the expectation inequality (15) for nondecreasing functions, and the inductive step of Theorem 7 only needs that. For a partial order, the expectation inequality is strictly weaker than the coupling (14) (Massey 1987). The induction must also handle the cross term $\sum_j q_{ij}\Delta W_{n-1}(j,x)$, which requires an embedded discrete-time chain whose one-step kernel preserves the order. The paper's Lemma 7 asserts that the embedded chain $P = I + Q/\nu$ is monotone for every $\nu \ge q^*$. As printed, this is false at $\nu = q^*$: for two states with $q_{01} = q_{10} = 1$, $P$ swaps the states. A complete proof cannot rely on that lemma as printed.

A second difficulty is that the one-period cost is unbounded. The classical theorems that ordered differences survive value iteration (Denardo, Lovejoy) assume bounded costs, so the induction has to be carried out by hand, and the limits $G_\infty$, $y^*_\infty$ must be justified by Lemma 4's uniform bounds.

Formalization scope

The Lean development lives in the namespace SongZipkinFluct.Monotone. World states form a countable nonempty type with a PartialOrder instance; no linear order is assumed. Inventory positions are integers. The demand-count law $f_i(d\mid l)$ and the world transition function $P(t)$ are defined by uniformization at the model's rate $\mu$, the paper's own device. The lead-time law is a probability measure on $[0,\infty)$, and $C(i,y)$ is the series $\sum_d g_i(d\mid\alpha)\hat C(y-d)$ of display (16). $W_n$ uses an infimum over integers $y \ge x$, and $W_\infty$, $G_\infty$ are suprema over $n$, which equal the limits because the sequences are nondecreasing and bounded. Monotonicity in $i$ is Monotone/Antitone with respect to $\preceq$. Smallest minimizers, maxima and minima are IsLeast/IsGreatest characterizations, never sInf on $\mathbb Z$.

Condition 1(a) is encoded as the coupling (14) itself, with one probability space per pair $i \preceq j$ and copies identified by their finite-dimensional distributions. Replacing it by the expectation inequality (15), or the partial order by a total order, would change the theorem and is ruled out. Every goal statement asserts the existence of the levels it constrains before constraining them, so no conclusion holds vacuously. The standing hypotheses together with Condition 1 are satisfiable: a one-state instance is checked in Lean.

Lemma 7 is not included because it is false as printed. A guarded version (for instance with $\nu \ge 2q^*$) would be a welcome contribution. Reusable parts include the uniformized Markov-modulated Poisson process, the coupling definition of stochastic monotonicity for a countable partially ordered state space, and the usual stochastic order on $\mathbb N$. Proofs of Lemma 9 and Theorem 7 that avoid Lemma 7 are particularly welcome.

Selected references

• J.-S. Song and P. Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. https://doi.org/10.1287/opre.41.2.351
• W. A. Massey, Stochastic orderings for Markov processes on partially ordered spaces, Mathematics of Operations Research 12(2):350–367, 1987. https://doi.org/10.1287/moor.12.2.350
• J. Keilson and A. Kester, Monotone matrices and monotone Markov processes, Stochastic Processes and their Applications 5(3):231–241, 1977. https://doi.org/10.1016/0304-4149(77)90033-3
• A. F. Veinott Jr., Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• W. S. Lovejoy, Ordered solutions for dynamic programs, Mathematics of Operations Research 12(2):269–276, 1987. https://doi.org/10.1287/moor.12.2.269