Probability

Motivation

Kingman's subadditive ergodic theorem (Theorem 1 of Kingman 1973, first proved in Kingman 1968) says that for a discrete-parameter subadditive process $x=(x_{st})$ the ratio $x_{0t}/t$ converges with probability one and in mean. Applications in first-passage percolation, products of random matrices and longest increasing subsequences often come with a continuous time parameter, so it is natural to ask whether the theorem holds with $t$ ranging over $[0,\infty)$.

Section 1.4 of the 1973 paper answers this question. Under separability alone, a continuous-parameter version would contain, as its additive special case, the claim that every separable process $(y_t;\,t\ge0)$ with stationary increments and finite expectations has a finite limit $\lim_{t\to\infty}y_t/t$ with probability one. Kingman remarks that no such theorem appears in the literature, "for the excellent reason that the conclusion is false, and in a very strong sense" (p. 888). Theorem 3 makes that sentence precise. It is the reason the continuous-parameter theorem of the paper (Theorem 4) carries an extra integrability hypothesis on the oscillation $\Omega_I=\sup_{s<t,\,s,t\in I}|x_{st}|$.

Setting

A real-time process is a family $(y_t;\,t\ge0)$ of real random variables on a probability space $(\Omega,\mathcal F,P)$. Its joint law is the law of the path $t\mapsto y_t$ on $\mathbb R^{[0,\infty)}$ with the product $\sigma$-algebra, that is, the collection of all finite-dimensional distributions.

• $(y_t)$ is stationary if for every $\tau\ge0$ the shifted process $(y_{t+\tau})_{t\ge0}$ has the same joint law as $(y_t)_{t\ge0}$.
• $(y_t)$ has stationary increments if for every $\tau\ge0$ the process $(y_{t+\tau}-y_\tau)_{t\ge0}$ has the same joint law as $(y_t-y_0)_{t\ge0}$.
• $(y_t)$ has finite expectations if $E|y_t|<\infty$ for every $t\ge0$.
• The sample function at $\omega\in\Omega$ is $t\mapsto y_t(\omega)$. It has derivatives of all orders if it is $C^\infty$ on $[0,\infty)$.

A growth bound is a function $\Gamma:(0,\infty)\to(0,\infty)$ that is increasing (non-decreasing). The event "$|y_t|\le\Gamma(t)$ for all sufficiently large $t$" is the set of $\omega$ for which some $T$ exists with $|y_t(\omega)|\le\Gamma(t)$ for every real $t\ge T$.

In the Lean development these notions are IsStationary, HasStationaryIncrements, Integrable (y t) P and ContDiffOn ℝ ∞ (fun t => y t ω) (Set.Ici 0), all in the namespace KingmanSubadditive.StationaryIncrements.

Formalization targets

Goal: Theorem 3 (p. 888)

For every positive non-decreasing $\Gamma$ on $(0,\infty)$ there are a probability space and a process $(y_t;\,t\ge0)$ with stationary increments, finite expectations and $C^\infty$ sample functions such that

$$P\{|y_t|\le\Gamma(t)\ \text{for all sufficiently large }t\}=0. \tag{1.4.4}$$

The quantifiers are "for every $\Gamma$ there exists $y$". Because $\Gamma$ may grow arbitrarily fast, no normalization $y_t/a(t)$ with a deterministic $a$ can converge to a finite limit almost surely.

Milestones

The milestones are the four steps of Kingman's proof, stated for the explicit process $y_t=Y_{t+\eta}$ of (1.4.5) built from a bump function $\psi$, a uniform $\eta$ and independent integer-valued $\nu_0,\nu_1,\dots$ with a law $m_\Gamma$ that depends on $\Gamma$:

1. $(y_t)$ is stationary, hence has stationary increments, and its sample functions are $C^\infty$ (p. 888).
2. $E(|y_t|)=E(y_0)=\int_0^1\psi(u)\,du<\infty$ (p. 888).
3. $\sum_{n\ge1}P\{\nu_n>\Gamma(n+\tfrac12)\}\ge\sum_{n\ge1}\sum_{r\ge n}\frac1{r(r+1)}=\infty$ (p. 889).
4. $P\{|y_t|\le\Gamma(t)\text{ eventually}\}\le P\{|y(n+\tfrac12\nu_n^{-1}-\eta)|\le\Gamma(n+\tfrac12\nu_n^{-1}-\eta)\text{ eventually}\}\le P\{\nu_n\le\Gamma(n+\tfrac12)\text{ eventually}\}=0$ (p. 889).

Significance

The result. Theorem 3 rules out any continuous-parameter subadditive ergodic theorem whose only hypotheses are separability, stationarity of the increments and finite means, and in fact any such theorem whose hypotheses are met by smooth stationary processes with finite means. The obstruction does not come from irregular paths: the counterexample is as regular as a path can be short of analyticity. Any continuous-time ergodic theorem therefore needs a hypothesis that controls the behaviour of the process inside unit intervals, such as $E(\Omega_I)<\infty$ in Theorem 4, or the integrability of $\int_I|y'|$ in the classical continuous-parameter ergodic theorem. The result also separates two kinds of time. Along the integers, a stationary-increment process with finite mean is an additive discrete process, so $y_n/n$ converges almost surely; Theorem 3 shows that the real-time path can still escape any envelope between the integers.

Formalizing it. The theorem is classical and its proof is complete in the paper. To our knowledge it has no machine-checked proof. A formalization requires the existence of a probability space carrying a uniform variable and an independent i.i.d. sequence with a prescribed law on the integers, the joint-law notion of stationarity for real-time processes, a stationarity argument for a randomly shifted process, an expectation computation with a change of variables, and the second Borel–Cantelli lemma. The definitions of stationarity and stationary increments for real-time processes on $[0,\infty)$ are reusable beyond this mission.

Difficulty

The natural first attempt is a process with linear or polynomial growth, such as $y_t=Zt$ with a heavy-tailed integrable $Z$. Every such attempt fails against a $\Gamma$ that grows faster, so the process must depend on $\Gamma$. A process that is large on a whole interval of length one cannot have finite mean when $\Gamma$ grows fast. The difficulty is to have excursions that are taller than any prescribed envelope infinitely often, and still keep finite expectation, stationarity in real time and smoothness. In the formal proof, the stationarity step is where most of the work sits: the shifted path must be identified in law with the original one for every real shift $\tau$, not only for integer shifts.

Formalization scope

• The process is y : ℝ → Ω → ℝ, with values at $t<0$ ignored; $\Omega$ lives in Type. Every $y_t$ with $t\ge0$ is measurable, and both stationarity definitions include almost-everywhere measurability, so Measure.map never takes its junk value.
• Joint laws are push-forwards to Set.Ici (0:ℝ) → ℝ with the product $\sigma$-algebra. Stationary increments compare the laws of $(y_{t+\tau}-y_\tau)_t$ and $(y_t-y_0)_t$ for every real $\tau\ge0$.
• "Increasing" is non-decreasing on $(0,\infty)$ (MonotoneOn Γ (Set.Ioi 0)), which gives the stronger theorem. $\Gamma$ is a total function on $\mathbb R$; its values at $t\le0$ are irrelevant.
• "Derivatives of all orders" is ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) on $[0,\infty)$ for every $\omega$. This is $C^\infty$, not the analytic order.
• In (1.4.4) "sufficiently large $t$" ranges over real $t$. The event need not be measurable a priori; $P$ of a set is its outer measure.
• A statement with a fixed $\Gamma$, with $\exists\Gamma$, with "for some large $t$", or with $t$ restricted to the integers would be trivial or false and is not the theorem. The integer skeleton is precisely what does not fail.
• For the milestones, the random ingredients are hypotheses: any $\eta,\nu_0,\nu_1,\dots$ that are independent, with $\eta$ uniform on $(0,1)$ and each $\nu_r$ of law $m_\Gamma$. The existence of such a family is part of the goal's proof.

Contributions welcome: proofs of the milestones, a general lemma that a uniformly shifted process built from an i.i.d. sequence of unit blocks is stationary in real time, and a proof of the goal.

Selected references

• J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
• J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society, Series B 30(3):499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x

Why semi-Markov control matters

A decision maker may choose an action whenever a system changes state, even though the time until the next change is random. Maintenance and replacement decisions are examples: a repair choice changes both the next operating state and the length of time before another choice is available. A discrete-time Markov decision model gives every decision epoch the same duration. A semi-Markov decision process allows the holding time to depend on the current state, action, and next state. Kallenberg's Chapter 7 develops discounted and average-reward versions of this finite-state model, including a characterization of optimal discounted value through inequalities and a linear program (Kallenberg 1983, Chapter 7).

The mission focuses on the discounted part of that chapter. The result is known: Kallenberg proves it as Theorem 7.2.1. The formalization task is to state and eventually prove the result for the same policy class and the same general holding-time distributions. Those details matter because a stationary-policy-only version would omit the comparison that the theorem makes with all admissible policies.

Model and notation

Let $E$ be a nonempty finite state set. Each $i\in E$ has a finite nonempty set $A(i)$ of available actions. If action $a\in A(i)$ is chosen, the next state is $j$ with probability $p_{iaj}\geq0$, with $\sum_jp_{iaj}=1$. Conditional on $j$, the nonnegative time until that transition has distribution $F_{iaj}$. The action earns a lump reward $r_{ia}$ immediately and a reward rate $s_{ia}$ during the ensuing sojourn. Neither the holding-time laws nor the reward rates are required to be identical across transitions (Kallenberg 1983, pp. 210–212).

Fix a positive continuous discount rate $\lambda$. The factor applied after elapsed time $t$ is $e^{-\lambda t}$. Assumption 7.2.1 requires the Laplace–Stieltjes transform of each conditional holding-time law to satisfy

$$L_{iaj}(\lambda):=\int_0^\infty e^{-\lambda t}\,dF_{iaj}(t)<1 \qquad(i,j\in E,\ a\in A(i)).$$

The assumption is strict for every triple; it does not require a particular parametric family. Define the one-epoch expected discounted reward and discounted transition entry by

$$r^*_{ia}=\sum_jp_{iaj}\int_0^\infty \left(r_{ia}+s_{ia}\int_0^t e^{-\lambda u}\,du\right)dF_{iaj}(t), \qquad p^*_{iaj}=p_{iaj}L_{iaj}(\lambda).$$

A policy $R$ is a sequence of randomized decisions. At each epoch its choice may depend on every previously observed state and chosen action and the current state. It does not observe previous sojourn times when choosing. Let $v_i^\lambda(R)$ be the expected sum of discounted lump and rate rewards from initial state $i$, as in equation (7.2.1). The DRD value vector is $v_i^\lambda=\sup_R v_i^\lambda(R)$, with the supremum over this full policy class. A real vector $w$ is DRD-superharmonic when

$$w_i\geq r^*_{ia}+\sum_jp^*_{iaj}w_j \qquad(i\in E,\ a\in A(i)).$$

These are Kallenberg's Definitions 7.2.1 and 7.2.2 (p. 214).

Formalization targets

Goal: the smallest superharmonic vector

Theorem 7.2.1 states that the value vector itself satisfies the superharmonic inequalities and lies below every other vector satisfying them:

$$v^\lambda\text{ is DRD-superharmonic},\qquad w\text{ is DRD-superharmonic}\Longrightarrow v_i^\lambda\leq w_i\quad(i\in E).$$

This is the mission goal. Its content includes both clauses: merely showing that every superharmonic vector bounds policy rewards would leave out the assertion that the value is superharmonic.

Supporting results

Lemma 7.2.1 expresses $v_i^\lambda(R)$ as a sum of expected discounted state-action occupancies. Theorem 7.2.2 says that a feasible action choice attaining equality in the value equation at every state yields an optimal pure stationary policy. Theorem 7.2.3 says that positive support in an optimal solution of the dual linear program (7.2.11) yields such a policy. Their statements and exact conditions are the mission's milestones (Kallenberg 1983, pp. 212, 216–217).

What the results provide

The goal turns a supremum over possibly history-dependent randomized policies into a finite system of inequalities indexed by available state-action pairs. The next two results explain how equality in those inequalities and an optimal linear-programming solution identify a pure stationary policy with the same value. Thus the finite programs are statements about the original semi-Markov process rather than a separate discounted matrix model (Kallenberg 1983, pp. 214–217).

Kallenberg supplies paper proofs. This mission supplies Lean statements and a shared model interface; the proposed theorem items still require machine-checked proofs. The model's arbitrary conditional holding-time measures, its distinction between the current reward and future discounted value, and its history-dependent policy class are reusable for other finite semi-Markov arguments. The average-reward section of Chapter 7 is outside this mission.

Main difficulty

The straightforward finite-state discounted equation concerns expected one-step rewards. The source value, however, is defined from rewards earned at random physical times, and a policy can react to its entire discrete history. Identifying these two descriptions requires accounting for the joint state, action, and elapsed-time law without giving the policy access to past holding times. Holding times may equal zero with positive probability; the strict transform assumption excludes a degenerate law concentrated entirely at zero, but it does not make each holding time strictly positive. A second issue is real-valuedness: all-policy suprema and integrals must represent the finite quantities in the source rather than Lean's default values on ill-posed inputs.

Formalization scope

Lean uses finite types for states and actions, with a nonempty available-action finset for each state. Conditional sojourn laws are probability measures on $\mathbb R$ with no mass on negative times. This includes arbitrary distributions on $[0,\infty)$ and permits an atom at zero. The model stores stochastic transition rows, lump rewards, and rate rewards. The discounted layer stores $\lambda>0$ and the source's strict per-triple transform inequality. The expected one-epoch reward uses a Lebesgue integral against each sojourn law.

Policy decision rules read a list of past state-action pairs and the current state. Finite-horizon value recursively integrates the original epoch reward and its holding-time discount; policy value is its limit. The coordinatewise supremum ranges over all such policies. The occupation sum of Lemma 7.2.1 is a separate theorem, not the definition of policy value. A proof must establish convergence and boundedness from Assumption 7.2.1 so that Lean's total limit, integral, and real-supremum operations have their intended meanings.

The dual program sums only over actions available in each state and uses strictly positive weights $\beta_j$, equality flow constraints, and nonnegative variables as printed. Its pure stationary selector must choose an available action with positive dual mass in every state. Contributions establishing the occupation identity, value bounds, Bellman inequalities, or dual decoding all fit the mission.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, Chapter 7, pp. 210–227. Publisher repository.

Why deteriorating jobs need a scheduling rule

On one processor, the completion time of a job normally depends on how much work precedes it. In the model of Browne and Yechiali (1990), waiting also changes the job's own processing requirement: a job that starts later takes longer. The sequence therefore changes both when each job starts and how long subsequent jobs must wait. This matters when the goal is a weighted completion cost, because a delay to one job can raise the completion costs of many others.

The paper gives an expected-makespan ordering for this linear deterioration model and, in Proposition 2, a sufficient condition under which the original job order minimizes weighted expected completion cost. The latter is the target of this mission. Related platform work on Delayed SWPT and the AvgCompletionSched family treats weighted completion scheduling without this job-specific linear deterioration. Their additive processing-time models do not supply the completion-time object used here.

Jobs, schedules, and cost

There are $N$ jobs, all available at time zero, processed one at a time on a single machine without idle time or preemption. A schedule $\pi$ is a permutation of the jobs: $\pi(k)$ is the job processed in position $k$. The paper labels positions and jobs from $1$ to $N$; the Lean development labels them from $0$ to $N-1$. The identity schedule $\pi_0$ processes jobs in label order.

For job $i$, $X_i$ is its random initial processing requirement, $\alpha_i$ its deterministic growth rate, and $c_i$ its waiting cost rate. If the job starts at time $t$, its actual processing time is $Y_i(t)=X_i+\alpha_i t$. Deterioration stops once processing starts. Write $S_k(\pi)$ for the time at which the first $k$ scheduled jobs have all finished. The model sets $S_0(\pi)=0$ and

$$S_{k+1}(\pi)=S_k(\pi)+X_{\pi(k+1)}+\alpha_{\pi(k+1)}S_k(\pi)$$

in the paper's one-based position notation. Thus the completion time of the job in position $k$ is $S_k(\pi)$. Its cost is its own rate $c_{\pi(k)}$ times that completion time, giving

$$C(\pi)=\sum_{k=1}^{N}c_{\pi(k)}S_k(\pi).$$

All of these are random quantities until an expectation is taken. Equation (2) of the paper writes $S_k$ as a sum of the initial requirements multiplied by the later growth factors. Equation (8) substitutes that expression into $C(\pi_0)$. Both equations are included as milestones, stated along an arbitrary schedule by relabelling the jobs. The third milestone is the exact change in $C$ from swapping two adjacent jobs. These three statements are pathwise identities, so their mathematical content does not depend on a probability distribution.

Formalization targets

The principal target is Proposition 2: if both sequences of job-indexed ratios are strictly increasing,

$$\frac{E(X_1)}{\alpha_1}<\cdots<\frac{E(X_N)}{\alpha_N}, \qquad \frac{\alpha_1}{c_1(1+\alpha_1)} <\cdots< \frac{\alpha_N}{c_N(1+\alpha_N)},$$

then, for every permutation $\sigma$,

$$E[C(\pi_0)]\le E[C(\sigma)].$$

The first ratio compares an initial expected requirement with its growth rate. The second couples growth and the cost rate. The conclusion is global optimality over the paper's whole class of nonpreemptive, non-idling permutations. It does not assert that the identity order is the unique minimizer; strict input ratios do not by themselves justify a uniqueness claim.

The attack path records exactly the supporting statements printed in the paper: the closed completion-time formula (2), the weighted cost formula (8), and the unnumbered adjacent-interchange identity after (8). The milestone quotations preserve the paper's printed display, while the Lean statements use an arbitrary permutation where relabelling permits it. The interchange display has a multiplication dot before its second bracket; expansion for two jobs shows that the term is added. The formal statement records that correction, and the source quotation retains the printed symbol.

What the result establishes

The proposition identifies a directly checkable pair of ordering conditions under which the natural job-label order solves a weighted stochastic scheduling problem. A condition involving only $E(X_i)/\alpha_i$, enough for the paper's expected-makespan target, does not determine this weighted objective. The cost rates introduce another ordering requirement. The result gives a sufficient rule, not a characterization of every optimal schedule or of every parameter choice.

The mathematical result was published in 1990; this mission asks for its machine-checked formalization. A complete development will connect the processing-time recursion, the pathwise cost identities, and the expected optimality statement in Lean. The recursion and cost definitions can be reused for other finite single-machine problems in which a job's processing time depends on its start time. The milestone identities are also useful independently of the final sufficient condition, including for studying other choices of weights and ordering indices.

Where the argument is difficult

Sorting by expected initial requirement alone cannot settle the problem, because processing a job changes later start times and hence later processing times. Even sorting by the expected-makespan index leaves the cost rates unaccounted for. The value of an adjacent swap depends on the elapsed time before the pair and on the completion costs of jobs after the pair. It is not enough to compare the two jobs' own completion costs in isolation.

The source states the sufficient condition after its interchange display but does not present a full proof of the global claim. Closing the Lean goal requires connecting local comparisons to every schedule and handling the expected value of the recursively defined cost. The identities are finite, but their indices change between zero-based Lean positions and the paper's one-based display, especially at the first position and at an empty suffix.

Formalization scope

Jobs are $\mathrm{Fin}\,N$, and a policy is an equivalence permutation with $\pi(k)$ equal to the job in position $k$. Completion time is defined by the processing rule $Y_i(t)=X_i+\alpha_i t$, not by the closed form (2). At positions beyond the $N$ jobs it stays constant, and theorems about the closed form restrict $k$ to $0\le k\le N$. The total cost is defined from job-weighted completion times, not from equation (8). This keeps both identities substantive.

The proposition uses a probability space and the Bochner integral of the real-valued cost. Every $X_i$ is integrable, so its expectation and the finite linear combinations appearing in the cost are meaningful. Initial requirements are nonnegative at every outcome, reflecting the paper's standing positive-processing convention; strict positivity is unnecessary for the claim. Growth rates and cost rates are strictly positive. Those two assumptions make the printed ratios well-defined and support the ordering rule. The paper's common independence convention is not required for these expectations and is not assumed.

The two strict orderings are over the labels of jobs in $\pi_0$, not positions of an arbitrary schedule. The conclusion compares $\pi_0$ with every permutation, not only with schedules obtained by one adjacent swap. The $N=0$ and $N=1$ cases are allowed: the order conditions have no pair to compare, and there is only one permutation. Solvers may contribute the finite-sum, interchange, and integrability facts needed to link the milestones to Proposition 2. The pathwise identities require no probability assumptions and can support later variants.

Selected references

• Browne, Sid, and Uri Yechiali, Scheduling Deteriorating Jobs on a Single Processor, Operations Research 38(3), 495–498 (1990). DOI: 10.1287/opre.38.3.495.

Motivation

The residual life time of a lifetime $X$ at age $t$ is the remaining life $X - t$ given survival past $t$. Its distribution at great age is a basic object in reliability, insurance and the statistics of extremes: excess-of-loss reinsurance prices the part of a claim above a retention level, and peaks-over-threshold methods fit a model to the observations exceeding a high level. Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974), 792–804, doi:10.1214/aop/1176996548) determined every possible limit law of the suitably normed residual life time as $t \to \infty$ and the domains of attraction of these laws; Pickands (1975) obtained the continuous part of the same picture, which is the probabilistic basis of the generalized Pareto approximation used in practice.

Limit theorems describe the behaviour only as $t \to \infty$. Section 4 of the paper gives approximation results for finite $t$. In extreme-value theory, von Mises (1936) gave a sufficient condition for attraction to the Fréchet law $\Phi_\alpha$: $tF'(t)/(1 - F(t)) \to \alpha$. Theorem 6 of the paper is a non-asymptotic, two-sided counterpart for the residual life time: two-sided bounds on the scaled hazard rate give two-sided bounds on the residual life distribution at every age past a threshold. This mission formalizes Theorem 6 (p. 801).

Setting

Let $X$ be a real random variable with law $\mu$ and distribution function $F(x) = P\{X \le x\}$. For an age $t$ with $P\{X > t\} > 0$, the residual life distribution function is

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

which is $0$ for $x < 0$. For $t > 0$ the residual life scaled by the age has distribution function $P\{(X - t)/t \le x \mid X > t\} = F_t(xt)$.

For $\alpha > 0$ the Pareto-type law $\Gamma_\alpha$ is

$$\Gamma_\alpha(x) = 1 - (1 + x)^{-\alpha} \quad (x \ge 0), \qquad \Gamma_\alpha(x) = 0 \quad (x < 0).$$

It is the law of $Y - 1$ when $P\{Y > y\} = y^{-\alpha}$ for $y \ge 1$. $F$ has a positive density $F'$ for $t \ge t_0$ if $F$ is differentiable at every $t \ge t_0$ with derivative $F'(t) > 0$. The quantity $F'(t)/(1 - F(t))$ is the hazard rate of $X$ at $t$, and $tF'(t)/(1 - F(t))$ is the hazard rate scaled by the age.

Formalization targets

Goal: Theorem 6 (p. 801)

Let $F$ have a positive density $F'$ for $t \ge t_0$, and let $\alpha_1, \alpha_2 > 0$ satisfy $\alpha_1 \le tF'(t)/(1 - F(t)) \le \alpha_2$ for $t \ge t_0$. Then for all $t \ge t_0$ and all real $x$,

$$\Gamma_{\alpha_1}(x) \;\le\; P\Big\{\frac{X - t}{t} \le x \;\Big|\; X > t\Big\} \;\le\; \Gamma_{\alpha_2}(x).$$

The smaller constant gives the lower bound: a smaller scaled hazard rate means a heavier tail and hence a larger chance that the remaining life is long. For a Pareto tail $1 - F(t) = Ct^{-\alpha}$ one may take $\alpha_1 = \alpha_2 = \alpha$, and both inequalities are equalities.

Milestone: the integrated hazard bounds (proof of Theorem 6, p. 801)

For $t \ge t_0$ and $x > 0$,

$$\alpha_1 \int_t^{(1+x)t} \frac{du}{u} \le \int_t^{(1+x)t} \frac{F'(u)}{1 - F(u)}\,du \le \alpha_2 \int_t^{(1+x)t} \frac{du}{u}.$$

Significance

The theorem turns a pointwise condition on the hazard rate, which can be checked on a density, into a bound on the whole conditional distribution of the residual life, valid at every age $t \ge t_0$ rather than only in the limit. If moreover $tF'(t)/(1 - F(t)) \to \alpha$, then $\alpha_1, \alpha_2$ can be taken arbitrarily close to $\alpha$ for large $t_0$, which recovers the convergence $P\{(X - t)/t \le x \mid X > t\} \to \Gamma_\alpha(x)$ with an explicit error at finite ages. Such bounds are what a practitioner fitting a Pareto tail above a threshold needs to quantify the approximation.

The result is classical and its proof is short; it is not open. As far as is known, no machine-checked version exists, and Mathlib has no theory of residual life distributions or of the limit laws of Balkema and de Haan. A formal proof would provide reusable pieces: the identity between the integrated hazard rate and $-\log(1 - F)$ for a distribution function with a density, and the comparison of a residual life distribution with a Pareto law. The other missions of this series formalize the paper's limit theorems, for which this mission's objects (the residual life distribution and $\Gamma_\alpha$) are shared.

Difficulty

The mathematics is elementary; the work lies in the regularity bookkeeping that the printed proof leaves implicit. The density is only assumed to exist pointwise, so the fundamental theorem of calculus must be applied to $-\log(1 - F)$ with a derivative that is not assumed continuous, and its integrability on $[t, (1+x)t]$ has to come from the hazard bounds themselves. That $1 - F$ stays positive, that $t_0 > 0$, and that the case $x \le 0$ is trivial all have to be derived from the hypotheses rather than assumed. Finally, the conditional probability must be identified with $1 - R((1+x)t)/R(t)$, where $R = 1 - F$, through the measure of intervals.

Formalization scope

The law of $X$ is a probability measure $\mu$ on $\mathbb R$, and $F$ is Mathlib's ProbabilityTheory.cdf μ. The probability $P\{(X - t)/t \le x \mid X > t\}$ is residualLife μ t (x * t) $= \mu((t, t + xt])/\mu((t, \infty))$. $\Gamma_\alpha$ is a real function defined by cases, with Real.rpow for the power. The density is an explicit function $f$ with $F$ having derivative $f(t) > 0$ at every $t \ge t_0$, the derivative taken within $[t_0, \infty)$. This is a right derivative at $t_0$ and the ordinary derivative for $t > t_0$. It is the weakest reading of "positive density $F'$ for $t \ge t_0$", and it admits the exact Pareto law with $t_0 = 1$, whose distribution function has no two-sided derivative at $1$. The bounds are stated for $t \cdot f(t)/(1 - F(t))$ with Lean's real division.

No hypothesis is added to the printed theorem, and no printed slip was found. The conditions $t_0 > 0$ and $F(t) < 1$ follow from the hypotheses: for $t \le 0$ the ratio is not $\ge \alpha_1 > 0$, and a positive derivative on $[t_0, \infty)$ makes $F$ strictly increasing there. Lean's convention $a/0 = 0$ therefore never acts at the ages concerned. The conclusion is stated for all real $x$, as printed; for $x \le 0$ all three quantities are $0$. The milestone does not assume the hazard rate integrable: it is bounded and measurable on $[t, (1+x)t]$, and a non-integrable integrand would make the inequality false rather than trivially true. A formalization that dropped the density hypothesis, replaced $F'$ by deriv without differentiability, or let the bounds hold only on a set not containing every $t \ge t_0$ would not be this theorem; all three are excluded by the statement.

A proof needs the fundamental theorem of calculus for derivatives within a half-line (in Mathlib), the identity $\int_t^{(1+x)t} du/u = \log(1+x)$, and the chain rule for $\log(1 - F)$. Proofs of the milestone and the goal are welcome, as are sorry-free lemmas showing that $\Gamma_\alpha$ is a distribution function and that the Pareto law satisfies the hypotheses with $\alpha_1 = \alpha_2$.

Selected references

• A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
• J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), no. 1, 119–131. https://doi.org/10.1214/aos/1176343003
• R. von Mises, La distribution de la plus grande de n valeurs, Revue Mathématique de l'Union Interbalkanique 1 (1936), 141–160.
• L. de Haan, A. Ferreira, Extreme Value Theory: An Introduction, Springer, 2006. https://doi.org/10.1007/0-387-34471-3

Motivation

PERT (Program Evaluation and Review Technique) and the critical path method model a project as a directed acyclic network whose arcs are jobs and whose nodes are events; the duration of the project is the length of a longest path from the origin to the terminal. When job durations are random, the quantity a planner wants is the expected duration. Computing it exactly requires solving one longest-path problem for every joint outcome of the job durations: with $m$ jobs each taking two values, $2^m$ deterministic problems. Classical PERT practice replaced every random duration by its mean and reported the longest path for the mean durations. That figure is known to be optimistically biased.

D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks (RAND Memorandum RM-3075-PR, 1962; Operations Research 10(6):808–817, 1962, doi:10.1287/opre.10.6.808), proposed a second estimate, computed node by node with work exponential only in the size of a single node's bundle of incoming arcs, and proved that it lies between the classical mean-length figure and the true expectation.

Setting

A project network has events $0,1,\dots,n$ with $n\ge1$, origin $0$ and terminal $n$. Its arcs are ordered pairs $(i,j)$ with $i<j$, at most one per pair, and every event lies on a directed path from the origin to the terminal. Fulkerson numbers his nodes $1,\dots,n$; his node $i$ is event $i-1$ here. The bundle $B_j$ of an event $j$ is the set of arcs entering $j$, and $\operatorname{pred}(j)$ the set of their tails; the origin's bundle is empty.

For arc lengths $t$, let $\ell_i(t)$ be the length of a longest (critical) path from the origin to $i$; equivalently $\ell_0=0$ and $\ell_j=\max_{i\in\operatorname{pred}(j)}(\ell_i+t_{ij})$.

The lengths of the arcs of each bundle $B_j$ form a random vector with a finite distribution: a finite set $S_j$ of bundle vectors $v$, where $v_i$ is the length of arc $(i,j)$, with probabilities $p_j(v)\ge 0$ summing to $1$. Arcs within a bundle may be correlated; distinct bundles are independent, so an assignment $\omega=(\omega_j)_j$ of one bundle vector per event has probability $p(\omega)=\prod_j p_j(\omega_j)$. Three numbers are attached to each event $i$:

1. the expected critical path length $e_i=\sum_\omega p(\omega)\,\ell_i(t(\omega))$;
2. the mean-length estimate $g_i=\ell_i(\bar t)$, where $\bar t_{ij}=\sum_{v\in S_j}p_j(v)\,v_i$ is the expected length of arc $(i,j)$;
3. Fulkerson's numbers $f_0=0$ and, for $j\neq0$,

$$f_j=\sum_{v\in S_j}p_j(v)\,\max_{i\in\operatorname{pred}(j)}\bigl(f_i+v_i\bigr).$$

Formalization targets

Goal: (4.4)

$$g_i\;\le\;f_i\;\le\;e_i\qquad\text{for every event } i .$$

Milestones

In the order of Fulkerson's induction (pp. 10–12):

1. the recursion for $\ell$ computes the greatest path length (§3, (3.6), and the display on p. 11);
2. $\ell_i(t)$ depends only on the arcs of the bundles $B_0,\dots,B_i$ (p. 6);
3. (4.8): $\max_{i\in\operatorname{pred}(j)}(f_i+\bar t_{ij})\le f_j$;
4. (4.5)/(4.9): if $g_k\le f_k$ for all $k<j$, then $g_j\le f_j$;
5. (4.13): $\sum_{v\in S_j}p_j(v)\max_{i\in\operatorname{pred}(j)}(e_i+v_i)\le e_j$;
6. (4.10)/(4.14): if $f_k\le e_k$ for all $k<j$, then $f_j\le e_j$.

Companion statements

• $g_i\le e_i$ under an arbitrary joint distribution of all arc lengths (remark, p. 12).
• Fig. 4.2: with correlated bundles, $e_3=g_3=1$ but $f_3=5/4$, so (4.4) fails without bundle independence.
• (4.17): an independent example with $g_3=f_3=1<e_3=5/4$.
• Fig. 4.1: explicit values $g_4=3/2$, $f_2=1/2$, $f_3=9/8$, $f_4=55/32$, and $f_i=e_i$.

Significance

The chain (4.4) says that the classical PERT estimate $g$ never overstates the expected project duration, and that the numbers $f$ are a lower bound at least as tight. The $f$ computation visits each node once and sums over the support of that node's bundle only, so its cost grows exponentially with bundle size rather than with network size, while the exact expectation $e$ requires the whole product space. The Fig. 4.2 example shows that the bundle-independence hypothesis cannot be dropped for the upper inequality, while the lower inequality $g\le e$ survives arbitrary dependence.

The result has a complete published proof. This mission seeks a machine-checked proof of (4.4) for finite distributions, with the longest-path characterisation of the earliest-event-time recursion and the locality of critical path lengths as reusable lemmas, and machine-checkable versions of the paper's numerical examples, including the counterexample showing the role of independence.

Difficulty

The left inequality compares an average of maxima with a maximum of averages. The right inequality requires more: $f_j$ averages over the bundle entering $j$, while $e_j$ averages over assignments to every bundle. Taking expectations in $\ell_j=\max_i(\ell_i+t_{ij})$ yields $e_j\ge\max_i(e_i+\bar t_{ij})$, which gives the weaker bound $g\le e$. Fig. 4.2 shows that $f\le e$ can fail when the bundles are dependent. In Lean, $e$ is a sum over a dependent product of finite supports (Fintype.piFinset); its interaction with the local recurrence for $f$ is the central technical difficulty.

Formalization scope

• Network: the published CriticalPath.Events.ProjectNetwork (Kelley–Walker 1959): events Fin (n + 1), arcs a Finset of ordered pairs with strictly increasing labels, origin preceding and terminal following every event. This requires $n\ge1$. Fulkerson's numbering condition "$i\le j$" on p. 3 is read as the strict $i<j$ (arcs join distinct nodes of an acyclic network). There is one arc per ordered pair, Fulkerson's own convention in (3.13).
• Critical path length: the published CriticalPath.Events.earliest, a recursion with Finset.sup' over the nonempty set of incoming arcs. This is the paper's convention that terms of missing arcs are ignored. Nothing uses a default value of $0$ or $-\infty$.
• Distributions: finite, given as data (a support Finset and a weight function per bundle) plus a predicate IsProb (nonnegative weights on the support, summing to $1$, for every event including the origin). Bundle vectors are functions on all events, and coordinates outside $\operatorname{pred}(j)$ are never read.
• Arc lengths are arbitrary reals. §3 assumes nonnegative lengths, but its footnote on p. 4 states that nonnegativity "is not essential in this or the following section"; the statements are given in this more general form.
• No trivialization: $e_i$ is the sum over every assignment of bundle vectors, weighted by the product probability (3.5). It is not defined by a recursion, and the goal assumes none of the milestones. $f$ at node $j$ uses only the distribution of the bundle of $j$.

Infrastructure that a full development needs, and that is reusable elsewhere, includes the longest-path characterisation of the earliest-event-time recursion, the locality lemma, and the factorisation of sums over Fintype.piFinset along one coordinate. Proofs of any milestone or companion are welcome. Out of scope here: §5 (computational examples) and the general-network analogues of §6.

Selected references

• D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks, RAND Memorandum RM-3075-PR, March 1962; published in Operations Research 10(6):808–817, 1962. doi:10.1287/opre.10.6.808
• J. E. Kelley Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proceedings of the Eastern Joint Computer Conference, 1959, pp. 160–173. doi:10.1145/1460299.1460318
• D. G. Malcolm, J. H. Roseboom, C. E. Clark and W. Fazar, Application of a Technique for Research and Development Program Evaluation, Operations Research 7(5):646–669, 1959. doi:10.1287/opre.7.5.646

Motivation

Many decisions in operations research and machine learning minimize an expected cost $\mathbb E^{P}[h(x,\xi)]$ whose distribution $P$ is unknown and is seen only through $N$ independent samples. The sample-average approximation replaces $P$ by the empirical distribution and is known to produce decisions with poor out-of-sample performance when $N$ is small. Distributionally robust optimization instead minimizes the worst-case expected cost over a set of distributions that are plausible given the data. Mohajerin Esfahani and Kuhn (arXiv:1505.05116v3, published in Mathematical Programming 171, 2018) take this set to be a ball in the Wasserstein metric around the empirical distribution, and show that such balls deliver both finite-sample certificates and asymptotic consistency. This mission formalizes the statistical half of that paper: Section 3 and Appendix A.

A data-driven method should, at a minimum, be consistent: as the sample grows, its optimal value and decisions should approach those of the true problem. For Wasserstein balls this requires a measure concentration inequality for empirical distributions in the Wasserstein metric, which was supplied by Fournier and Guillin (PTRF 2015). The paper combines that inequality with the Kantorovich–Rubinstein duality and the Borel–Cantelli lemma.

Setting

Let $E$ be $\mathbb R^m$ with an arbitrary norm $\|\cdot\|$ and its Borel $\sigma$-algebra. A decision $x$ ranges over a feasible set $X\subseteq\mathbb R^n$; the random vector $\xi$ has distribution $P$, supported on the uncertainty set $\Xi\subseteq E$; the loss is $h:\mathbb R^n\times E\to\mathbb R$. The true problem (1) has optimal value

$$J^\star=\inf_{x\in X}\mathbb E^P[h(x,\xi)].$$

The Wasserstein distance between distributions $Q_1,Q_2$ with finite first moment is

$$d_W(Q_1,Q_2)=\inf\Big\{\int\|\xi_1-\xi_2\|\,\Pi(d\xi_1,d\xi_2):\ \Pi\text{ a coupling of }Q_1\text{ and }Q_2\Big\}.$$

Given samples $\hat\xi_1,\dots,\hat\xi_N$ drawn independently from $P$ (joint law $P^N$, and $P^\infty$ for the infinite sequence), the empirical distribution is $\widehat P_N=\frac1N\sum_{i=1}^N\delta_{\hat\xi_i}$, and the Wasserstein ball $\mathbb B_\varepsilon(\widehat P_N)$ is the set of distributions $Q$ on $\Xi$ with $d_W(\widehat P_N,Q)\le\varepsilon$. The distributionally robust program (5) has optimal value

$$\widehat J_N=\inf_{x\in X}\ \sup_{Q\in\mathbb B_\varepsilon(\widehat P_N)}\mathbb E^Q[h(x,\xi)],$$

and an optimizer of it is written $\widehat x_N$.

The light-tail condition (Assumption 3.3) asks for an exponent $a>1$ with $A=\mathbb E^P[\exp(\|\xi\|^a)]<\infty$. Under it, and for $m\ne2$, Theorem 3.4 (Fournier–Guillin) gives constants $c_1,c_2>0$ with

$$P^N\{d_W(P,\widehat P_N)\ge\varepsilon\}\le\begin{cases}c_1e^{-c_2N\varepsilon^{\max\{m,2\}}},&\varepsilon\le1,\\ c_1e^{-c_2N\varepsilon^{a}},&\varepsilon>1,\end{cases}\tag{7}$$

for all $N\ge1$, $\varepsilon>0$. Solving the right-hand side $=\beta$ for $\varepsilon$ gives the radius

$$\varepsilon_N(\beta)=\Big(\frac{\log(c_1\beta^{-1})}{c_2N}\Big)^{1/\max\{m,2\}}\text{ if }N\ge\frac{\log(c_1\beta^{-1})}{c_2},\qquad\Big(\frac{\log(c_1\beta^{-1})}{c_2N}\Big)^{1/a}\text{ otherwise}.\tag{8}$$

Formalization targets

Goal: Theorem 3.6 (asymptotic consistency)

Let $\beta_N\in(0,1)$ with $\sum_N\beta_N<\infty$ and $\varepsilon_N(\beta_N)\to0$, and use the radius $\varepsilon_N(\beta_N)$ in (5).

(i) If $h(x,\cdot)$ is upper semicontinuous on $\Xi$ and $|h(x,\xi)|\le L(1+\|\xi\|)$ on $X\times\Xi$, then $P^\infty$-almost surely

$$\widehat J_N\ge J^\star\ \text{for all large }N\quad\text{and}\quad\widehat J_N\to J^\star.$$

(ii) If moreover $X$ is closed and $h(\cdot,\xi)$ is lower semicontinuous on $X$, then $P^\infty$-almost surely every accumulation point of $(\widehat x_N)$ is an optimal solution of (1).

Milestones

1. Theorem 3.5 (finite sample guarantee). For fixed $N\ge1$ and $\beta\in(0,1)$, with radius $\varepsilon_N(\beta)$,

$$P^N\big\{\mathbb E^P[h(\widehat x_N,\xi)]>\widehat J_N\big\}\le\beta.$$

2. Lemma A.1. An upper semicontinuous $h$ on $\Xi$ with $h(\xi)\le L(1+\|\xi\|)$ is the pointwise limit on $\Xi$ of a non-increasing sequence of Lipschitz functions.
3. Lemma 3.7 (convergence of distributions). Any data-dependent $\widehat Q_N\in\mathbb B_{\varepsilon_N(\beta_N)}(\widehat P_N)$ satisfies

$$P^\infty\Big\{\lim_{N\to\infty}d_W(P,\widehat Q_N)=0\Big\}=1.$$

Theorem 3.2 (Kantorovich–Rubinstein duality, $d_W(Q_1,Q_2)=\sup\{\int f\,dQ_1-\int f\,dQ_2:\ f\ 1\text{-Lipschitz}\}$), which the proof of (i) uses, enters as a reference item: the open platform theorem WassersteinDRO.Duality.kantorovich_rubinstein, stated on the whole space for all Borel probability measures. It is not a milestone, because that statement is more general than the paper's version on $\mathcal M(\Xi)$ (the two agree for distributions in $\mathcal M(\Xi)$ by extending Lipschitz functions from $\Xi$ to the whole space).

A companion item, Example 1 (1), records that upper semicontinuity cannot be dropped in (i): for $\Xi=[0,1]$, $P=\delta_0$ and $h=\mathbb 1_{(0,1]}(\xi)$ one has $J^\star=0$ but $\widehat J_N\ge1$ for every radius $\varepsilon>0$.

Significance

Theorem 3.5 makes the robust optimal value an upper confidence bound on the out-of-sample cost of the robust decision. Theorem 3.6 shows that this protection does not cost consistency: with radii shrinking at a rate governed by summable confidence levels, such as $\beta_N=e^{-\sqrt N}$, both the certificate and the decisions converge to their true counterparts. Together they are the statistical justification for the Wasserstein ambiguity sets that the rest of the paper reformulates as finite convex programs, and they are cited as the reference consistency results for Wasserstein distributionally robust optimization.

All results here are proved in the paper. None of them, nor the Fournier–Guillin inequality, is formalized on Prove2Me or in Mathlib to our knowledge. The mission adds machine-checked versions of the finite-sample and consistency statements, a monotone Lipschitz approximation lemma for semicontinuous functions with linear growth (useful wherever Lipschitz duality has to be extended to semicontinuous integrands), and a convergence lemma for measures in shrinking Wasserstein balls.

Difficulty

The obvious argument for (i) bounds the worst-case expectation by the true expectation plus a Lipschitz constant times the radius. That fails, because $h$ is only upper semicontinuous in $\xi$, not Lipschitz, and has no Lipschitz constant to multiply. The expectations of a merely semicontinuous loss must be controlled uniformly over every distribution in the ball, including data-dependent worst-case distributions, and the almost-sure convergence of the empirical distribution alone does not give this. Example 1 of the paper shows that each regularity hypothesis is needed. On the formal side, the Wasserstein distance is an infimum over couplings on a Polish space; even its triangle inequality (gluing of couplings) and the Kantorovich–Rubinstein duality are substantial.

Formalization scope

$E$ is a finite-dimensional real normed space with its Borel $\sigma$-algebra (BorelSpace), and $m$ is its dimension; decisions live in EuclideanSpace ℝ (Fin n). The definitions $d_W$ (type $p=1$), $\widehat P_N$, $\mathbb B_\varepsilon(\widehat P_N)$, $\mathbb E^Q$ and the worst-case expectation are the published WassersteinDRO.Duality definitions. The optimal values $J^\star$ and $\widehat J_N$ are extended reals. Standing conventions and pinned hypotheses:

• "Supported on $\Xi$" is $P(\Xi^c)=0$; $\Xi$ is neither closed nor convex in general. The samples lie in $\Xi$ almost surely, and optimizers and ball selections are required only for samples in $\Xi$.
• The constants $c_1,c_2>0$ enter as any constants for which (7) holds, which is how (8) is defined from Theorem 3.4. The theorem of Fournier and Guillin is not part of this mission, and $m\ne2$ is assumed because (7) and (8) are printed only for $m\ne2$.
• The loss is real-valued. In Theorem 3.5 it is assumed $P$-integrable on $X$, because the worst-case expectation counts only distributions under which the loss is integrable. In Theorem 3.6 the linear growth bound makes this automatic.
• Probabilities "at least $1-\beta$" are stated as bounds on the outer measure of the failure event, and "$P^\infty$-almost surely" as an almost-everywhere statement for the product measure on sequences.
• The paper's "$\widehat J_N\downarrow J^\star$" is stated as eventual domination $\widehat J_N\ge J^\star$ plus convergence, which is what its proof establishes; monotonicity in $N$ is not claimed.

A statement in which (7) could not hold for any constants would make the goal vacuous. The concentration inequality is satisfiable (for instance by a Dirac distribution with any constants), and $\varepsilon_N(\beta)$ is defined by the paper's formula, not chosen freely.

Welcome contributions: the triangle inequality and Kantorovich–Rubinstein duality for $d_W$, the Borel–Cantelli step for product measures, Lemma A.1, and the Fatou argument of (ii).

Selected references

• P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018); source version arXiv:1505.05116v3. https://arxiv.org/abs/1505.05116v3
• N. Fournier and A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
• L. V. Kantorovich and G. S. Rubinstein, On a space of totally additive functions, Vestnik Leningrad. Univ. 13 (1958).
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• D. Bertsimas, V. Gupta and N. Kallus, Robust sample average approximation, Mathematical Programming 171 (2018). https://arxiv.org/abs/1408.4445

Motivation

A manufacturer launching a new product often depends on a single supplier for a critical component, and the supplier must build capacity before demand is known. The manufacturer usually knows more about demand than the supplier does: her sales force, market research and order history give her a forecast the supplier cannot verify, and she has a reason to inflate it, since more capacity costs her nothing if the supplier pays for it. Whether contracts can make forecast sharing credible, and at what cost to the supply chain, is the subject of Cachon and Lariviere, "Contracting to assure supply: how to share demand forecasts in a supply chain" (Management Science 47(5), 2001, doi:10.1287/mnsc.47.5.629.10486). Section 6.10 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents a simplified version of that model, and this mission formalizes it from the author's January 2003 draft.

The section separates two regimes. Under forced compliance the supplier must build exactly the capacity the contract specifies; under voluntary compliance he may build less. The section's conclusion is that forced compliance allows both coordination and credible forecast sharing, while voluntary compliance allows forecast sharing only at the price of under-investment in capacity.

Setting

Demand $D_\theta$ has one of two types $\theta \in \{h, l\}$ with distribution function $F_\theta(x) = F(x\mid\theta)$. The page assumes $F_\theta(x) = 0$ for $x < 0$, $F_\theta(x) > 0$ for $x \ge 0$ (so demand has an atom at $0$), $F_\theta$ increasing and differentiable, and stochastic dominance $F_h(x) < F_l(x)$ for all $x \ge 0$. The supplier $S$ builds capacity $k$ at cost $c_k > 0$ per unit; after demand is observed he produces $\min\{D_\theta, k\}$ at cost $c_p > 0$ per unit; the manufacturer $M$ earns $r > c_p + c_k$ per unit of demand satisfied; unused capacity is worth nothing.

Expected sales with $x$ units of capacity are $S_\theta(x) = x - E[(x - D_\theta)^+]$, and the supply chain's expected profit is

$$\Omega_\theta(k) = (r - c_p)S_\theta(k) - c_k k .$$

An optimal capacity $k_\theta^o$ maximizes $\Omega_\theta$ over $k \ge 0$, and $\Omega_\theta^o = \Omega_\theta(k_\theta^o)$.

In an options contract $M$ buys $q_i$ options at $w_o$ each and pays $w_e$ for each option exercised. With $k = q_i$ her profit is $\Pi_\theta(q_i) = (r - w_e)S_\theta(q_i) - w_o q_i$ and the supplier's is $(w_e - c_p)S_\theta(q_i) + w_o q_i - c_k q_i$. The contract with share $\lambda$ sets $r - w_e = \lambda(r - c_p)$ and $w_o = \lambda c_k$. Under a wholesale price contract with price $w$ the supplier earns $\pi_\theta(k) = (w - c_p)S_\theta(k) - c_k k$; the price inducing capacity $k$ is $w_\theta(k) = c_k/\bar F_\theta(k) + c_p$ with $\bar F_\theta = 1 - F_\theta$, and the manufacturer then earns $\Pi_\theta(k) = (r - w_\theta(k))S_\theta(k)$.

With asymmetric information only $M$ observes $\theta$. Let $\hat\pi$ be the supplier's minimum acceptable profit, and define the shares

$$\lambda_l = 1 - \frac{\hat\pi}{\Omega_l^o},\qquad \lambda_h = 1 - \frac{\hat\pi}{\Omega_h^o},\qquad \hat\lambda_h = \frac{\Omega_l^o - \hat\pi}{\Omega_l(k_h^o)},\qquad \lambda_H = \min\{\lambda_h, \hat\lambda_h\}.$$

Formalization targets

Goal: forced-compliance separating contracts (§6.10.3, pp. 103–104)

The low type offers the options contract with share $\lambda_l$ and initial order $k_l^o$, the high type the one with share $\lambda_H$ and initial order $k_h^o$. Assuming $0 < \hat\pi < \Omega_l^o$ and $\Omega_l(k_h^o) > 0$:

$$0 < \lambda_l < \lambda_H < 1,\qquad \lambda_l\,\Omega_h(k_l^o) < \lambda_H\,\Omega_h^o,\qquad \lambda_H\,\Omega_l(k_h^o) \le \Omega_l^o - \hat\pi,$$

the supplier earns $\hat\pi$ from the low type and at least $\hat\pi$ from the high type, and each initial order $k_\theta^o$ maximizes both firms' profits. The profit comparisons are stated between the contract profit functions, not between shares.

Milestones

1. $S_\theta(x) = x - \int_0^x F_\theta$ (p. 98).
2. $\Omega_\theta$ is concave, and $k > 0$ is optimal iff $\bar F_\theta(k) = c_k/(r - c_p)$ (p. 99).
3. $\Omega_l(k) < \Omega_h(k)$ for $k > 0$, hence $\Omega_l^o < \Omega_h^o$ (implicit on p. 104).
4. The options contract with share $\lambda \in [0,1]$ gives $\Pi_\theta = \lambda\Omega_\theta$ and the supplier $(1-\lambda)\Omega_\theta$, so it coordinates (pp. 99–100).
5. Under voluntary compliance, $\partial\pi(k_\theta^o, k_\theta^o, \theta)/\partial k < 0$ (p. 100).
6. A capacity $k > 0$ is optimal for the supplier under a wholesale price $w$ iff $w = w_\theta(k)$ (p. 101).
7. A stationary point $k^*$ of $\Pi_\theta$ satisfies $\bar F_\theta(k^*) = \bar F_\theta(k_\theta^o)\bigl(1 + f_\theta(k^*)S_\theta(k^*)/\bar F_\theta(k^*)^2\bigr)$, so $k^* < k_\theta^o$ (p. 102).

Significance

The goal shows that with forced compliance a high-demand manufacturer can share her forecast credibly through the terms of a coordinating contract rather than its form: both types use the same contract family, the supply chain is coordinated in every state, and the only cost of asymmetric information is that the high type may be unable to push the supplier down to his reservation profit. The voluntary-compliance milestones show the other side: once the supplier may under-build, only the wholesale price affects his capacity, and the resulting capacity is strictly below the integrated optimum. Together they explain why compliance regimes matter in capacity contracting.

The results are established on the page with short arguments; none has a machine-checked proof. Formalizing them requires the derivative of expected sales for a distribution with an atom, the first-order characterization of a concave maximizer on a half-line, and careful bookkeeping of the incentive constraints. The demand and profit definitions are reusable for other capacity-procurement and newsvendor-type models.

Difficulty

The incentive constraints look like arithmetic on shares, but the strict inequality $\lambda_l < \hat\lambda_h$ needs $\Omega_l(k_h^o) < \Omega_l^o$: the low type's chain profit at the high type's capacity must be strictly below its optimum. The obvious argument via uniqueness of the maximizer is not available, because the page does not assume $F_\theta$ strictly increasing, so $\Omega_l$ need not be strictly concave and may have a whole interval of maximizers. Likewise $\Omega_l^o < \Omega_h^o$ needs a strict comparison of integrals of distribution functions. In the voluntary-compliance part, the derivative of $w_\theta(k)$ needs the density at $k^*$, and $k^* < k_\theta^o$ fails when that density is $0$.

Formalization scope

Each demand law is a probability measure on $\mathbb R$ and $F_\theta$ is Mathlib's cdf. $F_\theta$ is required to be differentiable only on $(0,\infty)$, because the page's $F_\theta(0) > 0$ makes it jump at $0$. $S_\theta$ is defined by the expectation $x - E[(x - D_\theta)^+]$, whose integrand is integrable because $D_\theta \ge 0$ almost surely. Optimal capacities are passed as arguments characterized as maximizers over $[0,\infty)$, never chosen; $k_\theta^o > 0$ is footnote 46's assumption. Derivatives are HasDerivAt statements.

Hypotheses added relative to the page, all disclosed in the items: $0 < \hat\pi < \Omega_l^o$ and $\Omega_l(k_h^o) > 0$ in the goal (the page divides by $\Omega_l(k_h^o)$ and needs $\lambda_l \in (0,1)$); $\lambda > 0$ for the voluntary-compliance derivative (at $\lambda = 0$ it vanishes); $\bar F_\theta(k^*) > 0$ and $f_\theta(k^*) > 0$ for the non-coordination result. The page's assumption $w''_\theta > 0$ is not needed and not imposed; its strict-concavity claim on p. 101 is not stated, because it would need $F_\theta$ strictly increasing. The prior $\Pr(\theta = h) = \rho$ does not enter any statement. The page's "separating equilibrium" is formalized by its defining incentive and participation conditions, not by a general signalling-game solution concept; a predicate that holds by construction of $\hat\lambda_h$ (for example $\lambda_H \le \hat\lambda_h$) is not an acceptable substitute for the profit inequalities. The fixed-fee condition of p. 105 is pure algebra on four numbers and is not included.

All definitions are local to the namespace CachonCoord.CapacityForecast. No platform theorem formalizes this model; the Snyder–Shen newsvendor definitions (SupplyChainTheory_contracts) and the revenue-sharing model of Cachon–Lariviere 2005 (RevShareCoord.*) concern different games and are not reused. Proofs of any milestone, and a sanity instance showing the model's hypotheses are satisfiable (for example demand with an atom $p_\theta$ at $0$ and an exponential tail, $p_h < p_l$), are welcome.

Selected references

• G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6. doi:10.1016/S0927-0507(03)11006-7 (formalized from the author's 3rd draft, January 2003).
• G. P. Cachon and M. A. Lariviere, Contracting to assure supply: how to share demand forecasts in a supply chain, Management Science 47(5), 629–646, 2001. doi:10.1287/mnsc.47.5.629.10486
• R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965 (increasing failure rate distributions, cited on p. 102).