Probability

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

Spare-parts provisioning for repairable ("recoverable") items is a classical inventory problem: aircraft components fail, are sent to repair, and a stock of spares covers the units in the repair pipeline. Sherbrooke's METRIC model (Sherbrooke 1968), developed at RAND for the U.S. Air Force, measures the performance of a stock level by the expected number of backorders, the average number of unfilled demands outstanding at a random time. Every allocation computed by METRIC is driven by this quantity, and in particular by how it depends on the mean demand of each item.

For a new item that mean is not known. Air Force practice at the time produced a single engineering estimate of mean demand and computed backorders from it as if it were exact. In the section Demand Prediction (pp. 138–139) Sherbrooke argues that this practice is biased in one direction: under Poisson demand and any positive spare stock, the point estimate always understates expected backorders whenever the true mean is genuinely uncertain. This is his reason why a Bayesian treatment of demand is "of fundamental importance for all items, not merely low-demand items". The mission formalizes that claim and the computation behind it.

Setting

Fix one item. Its spare stock $s \in \{0, 1, 2, \dots\}$ is stock on hand plus on order plus in repair, minus backorders; under one-for-one replenishment it is constant. Let the number of units in resupply at a random time be Poisson distributed with mean $\lambda > 0$:

$$p(x \mid \lambda) = e^{-\lambda}\frac{\lambda^x}{x!}, \qquad x = 0, 1, 2, \dots$$

The expected backorders at spare stock $s$ are, by the paper's eq. (2),

$$B(s \mid \lambda) = \sum_{x=s+1}^{\infty} (x - s)\, p(x \mid \lambda).$$

In eq. (2) the mean is $\lambda T$ (customer rate times mean resupply time); on p. 138 it is the mean demand over a unit time interval. Only the mean enters, so it is written as one parameter $\lambda$. In Lean this is SherbrookeMetric.PointEstimate.backorders s lam, built on the published Poisson probabilities ServiceParts.StockLevels.poissonPmf.

Uncertain mean demand. The true mean takes the values $\lambda_k > 0$, $k \in K$ ($K$ finite), with probabilities $w_k \ge 0$, $\sum_k w_k = 1$. The point estimate is the mean of this distribution, $\bar\lambda = \sum_k w_k \lambda_k$, and the expected backorders accounting for the uncertainty are $\sum_k w_k B(s \mid \lambda_k)$. The paper's example (p. 138) takes $\lambda \in \{0.5, 1.5\}$ with probability $0.5$ each, so $\bar\lambda = 1$; its procedure (p. 139) discretizes a gamma prior to five to ten values.

Formalization targets

Goal: the point estimate understates backorders (pp. 138–139)

If two distinct values $\lambda_k \ne \lambda_{k'}$ both carry positive probability, then for every spare stock $s \ge 1$

$$B(s \mid \bar\lambda) < \sum_k w_k\, B(s \mid \lambda_k),$$

and for $s = 0$ the two sides are equal for every prior. The goal fixes no constants and no particular prior.

Milestones

1. Eq. (10), p. 139: for $\lambda > 0$, $B(s \mid \cdot)$ is twice differentiable at $\lambda$ with

$$\frac{\partial^2 B(s \mid \lambda)}{\partial\lambda^2} = \frac{e^{-\lambda}\lambda^{s-1}}{(s-1)!} > 0 \quad (s \ge 1),$$

and second derivative $0$ for $s = 0$. 2. Strict convexity, p. 139: for $s \ge 1$, $\lambda \mapsto B(s \mid \lambda)$ is strictly convex on $(0, \infty)$. 3. The worked example, p. 138 (off the goal's path): $B(2 \mid 1) = 3e^{-1} - 1 \approx 0.1036$ and $0.5\,B(2 \mid 0.5) + 0.5\,B(2 \mid 1.5) \approx 0.1486$.

Significance

The result. Expected backorders are the objective METRIC minimizes, item by item, subject to a budget. If the objective is evaluated at a point estimate, every item with uncertain demand looks better stocked than it is, and since the size of the error varies by item, the marginal comparisons that drive the allocation are distorted. The inequality is the quantitative statement behind the paper's recommendation to compute backorders as a posterior mixture over possible mean demands. It also says that an underestimate of demand costs more than an overestimate of the same size when backorders are the objective. For $s = 0$ the bias vanishes because $B(0 \mid \lambda) = \lambda$ is linear.

Formalizing it. The paper proves the statement in one line ("it is easy to show") by differentiating twice. No machine-checked version exists. A formal proof needs termwise differentiation of the Poisson backorder series, a closed form for its second derivative, and the passage from a positive second derivative to strict convexity and then to a strict finite Jensen inequality under a nondegenerate prior. The resulting facts about $\lambda \mapsto B(s \mid \lambda)$ are reusable in any Poisson inventory model (base-stock, $(s-1, s)$ policies, METRIC and VARI-METRIC). Convexity of $B$ in the stock level $s$, the paper's eq. (3), is a different statement; it is already posed on the platform as ServiceParts.StockLevels.backorder_differences (compound Poisson demand) and is not repeated here. The definition of the Poisson probabilities is the published ServiceParts.StockLevels.Basic (Muckstadt 2005).

Difficulty

Each step is classical, but none is a one-liner in Lean. The series $B(s \mid \lambda)$ is an infinite sum whose terms depend on $\lambda$ both through $e^{-\lambda}$ and through $\lambda^x$, so differentiating it twice under the summation sign requires a uniform summability bound for the derivative series on a neighbourhood of $\lambda$. The tempting shortcut of reasoning with deriv alone fails: deriv returns $0$ at points of non-differentiability, so a formula for deriv (deriv B) says nothing about smoothness, and the milestone is stated with HasDerivAt for this reason. The strict inequality further needs strict convexity, not just convexity, and a hypothesis that the prior is not concentrated on one value: with a one-point prior both sides coincide.

Formalization scope

• $B(s \mid \lambda)$ is a real-valued tsum over $x \in \mathbb N$ of $(x - s)\,p(x \mid \lambda)$ for $x > s$ and $0$ otherwise. The family is summable for every real $\lambda$; no statement relies on the tsum junk value.
• Spare stock is a natural number; mean demand is real. Convexity and the second-derivative formula are stated for $\lambda > 0$, the paper's "for any positive $\lambda$".
• Explicit readings of the paper's phrases: "backorders computed from a point estimate" is $B(s \mid \bar\lambda)$ with $\bar\lambda$ the prior mean (the paper assumes "the initial estimate is the mean of the true mean demand distribution"); "the correct value" is the prior expectation $\sum_k w_k B(s \mid \lambda_k)$; "mean demand can assume more than one value" means two distinct values each of positive probability; "positive spare stock" means $s \ge 1$; "understate" is strict.
• The prior is a finite distribution with positive support points. This covers the paper's two-point example and its five-to-ten-point discretization of a gamma prior; a general prior on $(0, \infty)$ would need integrability hypotheses and is not part of the mission.
• The printed value $B^*(2) = 0.1485$ is a rounding slip; the exact value is $0.14864\ldots$, and the worked example states $0.1486$.
• A formalization that fixes $s$, uses $\le$ in place of $<$, drops the nondegeneracy hypothesis (making the strict statement false), or states the second derivative with deriv alone (vacuous at non-differentiable points) does not meet the target.
• Not formalized: the remark that the understatement "is also true for probability distributions like the negative binomial, though difficult to prove analytically" (unproved on the page), the gamma prior and Bayes updating (a procedure), and the comment that the resulting allocation "will produce inferior results" (not a mathematical statement).
• Contributions welcome: termwise differentiation lemmas for Poisson-weighted series, the closed form $B(s \mid \lambda) = \lambda - s + \sum_{x<s}(s - x)p(x \mid \lambda)$, and a strict finite Jensen inequality in the form used here.

Selected references

• C. C. Sherbrooke, METRIC: A Multi-Echelon Technique for Recoverable Item Control, Operations Research 16(1) (1968), 122–141. https://doi.org/10.1287/opre.16.1.122
• G. J. Feeney and C. C. Sherbrooke, The (s−1, s) Inventory Policy under Compound Poisson Demand, Management Science 12(5) (1966), 391–411. https://doi.org/10.1287/mnsc.12.5.391
• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005. https://doi.org/10.1007/0-387-27288-8

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

Volatility estimates from daily high, low and closing prices have been used since Parkinson (1980) and Garman and Klass (1980): the range of a day's log-price carries much more information about the volatility $\sigma$ than the close alone. Rogers and Satchell (1991) propose an estimator, $S_1(S_1-X_1)+I_1(I_1-X_1)$, that is unbiased for $\sigma^2$ whatever the drift of the log-price. The companion mission (Part I) formalizes that unbiasedness.

Every such estimator meets the same practical problem. The true high and low of the continuous path are never observed; one sees the maximum and minimum of the path sampled at $N$ times. The sampled maximum $S$ falls short of the true maximum $S_1$ by an amount $\Delta = S_1 - S \ge 0$, and the resulting downward bias is large in practice (Garman and Klass, and Beckers (1983), identified it). Section 3 of Rogers and Satchell proposes a correction: model $\Delta$ by a random variable with an explicit law, compute its first two moments exactly, and subtract their effect. The constants that appear,

$$a=\sqrt{2\pi}\Big[\tfrac14-\tfrac{\sqrt2-1}{6}\Big],\qquad b=\frac{1+3\pi/4}{12},$$

enter the corrected estimator directly. Their simulations (Tables 1–3 of the paper) show that the correction removes most of the bias.

Setting

Fix a volatility $\sigma>0$ and a sampling mesh $h>0$ (in the paper $h=1/N$). For a level $\alpha\ge0$ define

$$G_{\sigma,h}(\alpha)=\int_0^h e^{-2\alpha^2/(u\sigma^2)}\,\frac{du}{(4uh)^{1/2}} .$$

The factor $e^{-2\alpha^2/(u\sigma^2)}$ is the probability that a Brownian bridge of duration $u$ and volatility $\sigma$ climbs above level $\alpha$. The factor $(4uh)^{-1/2}$ is a probability density on $(0,h]$. Since $G_{\sigma,h}(0)=1$ and $G_{\sigma,h}$ decreases continuously to $0$, it is the survival function of a law on $(0,\infty)$. This law is the paper's display (9).

A real random variable $Z$ has distribution (9) if it is measurable and $P(Z>\alpha)=G_{\sigma,h}(\alpha)$ for every $\alpha\ge0$. In the paper, $Z$ is the overshoot of the continuous maximum over the sampled maximum $x$ in the sampling interval to the left of the time $t$ at which $x$ is attained, and $Z'$ is the overshoot in the interval to the right. The paper then assumes (p. 508) that $Z$ and $Z'$ are independent, each with distribution (9), and approximates $\Delta$ by $Z\vee Z'=\max(Z,Z')$. Write $Z\wedge Z'=\min(Z,Z')$.

In Lean, overshootSurvival σ h α is $G_{\sigma,h}(\alpha)$, HasOvershootLaw P σ h Z is "$Z$ has distribution (9) under $P$", and constA, constB are $a$ and $b$.

Formalization targets

Goal: the two moments of $Z\vee Z'$ (Eq. (11), p. 508, and the display on p. 509)

For $\sigma,h>0$ and $Z,Z'$ independent with distribution (9), the variables $Z\vee Z'$ and $(Z\vee Z')^2$ are integrable, and

$$E(Z\vee Z')=a\,\sigma\sqrt h,\qquad E\big[(Z\vee Z')^2\big]=b\,\sigma^2h .$$

Milestones, in the order the paper uses them

1. (9), p. 507. The two integral forms of the survival function agree:

$$\int_0^h e^{-2\alpha^2/(u\sigma^2)}\frac{du}{(4uh)^{1/2}}=\int_{h^{-1}}^\infty e^{-2\alpha^2s/\sigma^2}\frac{ds}{(4hs^3)^{1/2}} .$$

2. (10), p. 508. $EZ=\sigma(2\pi h)^{1/2}/8$.
3. Display before (11), p. 508. $E(Z\wedge Z')=\sqrt{2\pi h}\,(\sqrt2-1)\,\sigma/6$.
4. (12), p. 508. $EZ^2=\sigma^2h/6$.
5. (13), p. 509. $E[(Z\wedge Z')^2]=\frac{\sigma^2h}{4}\big(1-\frac\pi4\big)$.

The goal combines milestones 2–5 through $Z\vee Z'=Z+Z'-Z\wedge Z'$, which the paper uses in (11).

Significance

The result. The two identities are the coefficients of the corrected estimator (5): replacing $\Delta$ and $\Delta^2$ by $a\sigma\sqrt h$ and $b\sigma^2h$ turns the high–low estimator into an equation whose positive root $\hat\sigma_h$ largely removes the discretization bias. The same constants correct the Garman–Klass estimator (p. 509). Without exact values for $a$ and $b$ the correction has no concrete form.

Formalizing it. The paper does each of the four double integrals in a line and says "after some calculation" twice. A machine-checked derivation confirms the printed constants, which are reused in the high–low volatility literature. It also states precisely what is exact (moments of the model law (9) under independence) and what is approximation (that the model describes $\Delta$). To our knowledge none of these identities has been formalized before.

Difficulty

The statements are elementary but none of them is a one-line identity. Each moment is a double or triple improper integral with singular weights $(4hs^3)^{-1/2}$ on an unbounded domain. The minimum of $Z$ and $Z'$ couples two such integrals, and the resulting kernels $(s+u)^{-1/2}$ and $\sqrt{st}/(s+t)$ have to be integrated in closed form over the unit square. Matching $\sqrt2-1$ and $1-\pi/4$ exactly leaves no room for slack. In Lean, every exchange of integration order, change of variables and passage from survival functions to moments has to be justified for non-negative but unbounded functions, and the expectations must be shown finite: the Bochner integral of a non-integrable function is $0$.

Formalization scope

• Model. Random variables live on an arbitrary probability space (Ω, P) with [IsProbabilityMeasure P]. "Distribution (9)" is Measurable Z ∧ ∀ α ≥ 0, P.real {α < Z} = G σ h α, imposed only at levels $\alpha\ge0$: the formula is even in $\alpha$, and imposing it at negative levels would make the hypothesis unsatisfiable. Independence is IndepFun Z Z' P. $Z\vee Z'$ and $Z\wedge Z'$ are max and min.
• Parameters. $\sigma>0$ and $h>0$ only. The paper's $h=1/N\le1$ is not needed and not imposed.
• Explicit readings. "E" is the Bochner integral, and every expectation identity carries its integrability (Integrable, or MemLp … 2 for second moments). The conditioning "$\mid t-h<H_x<t,\ X_t=x$" in (9) and (10) is the modelling context in which the paper derives the law, not a hypothesis. The paper's "$E(Z\wedge Z')^2$" in (13) is read as $E[(Z\wedge Z')^2]$, as its first line shows. The integrals in (9) run over $(0,h]$ and $[h^{-1},\infty)$.
• Not formalized. The approximate statements $E\Delta\doteq a\sigma\sqrt h$ and $E\Delta^2\doteq b\sigma^2h$, the densities (6) and (7), and the independence remark of p. 508 are modelling approximations about the random walk, not theorems. The estimators (5) and $\hat\sigma^2_{GK,h}$ are definitions with no claim attached. The Brownian-bridge maximum (8) is not stated (its print also has a slip: $1-2/u$ for $1-s/u$). Section 4 (simulations) is out of scope.
• Non-triviality. The hypotheses are satisfiable for every $\sigma,h>0$: a probability measure on $\mathbb R$ with survival function $G_{\sigma,h}$ exists, and the two coordinates under its product measure are independent copies. A formalization that stated the survival condition for all $\alpha\in\mathbb R$ would be vacuous and is ruled out. So is one without the integrability conjuncts, which could hold with both sides $0$.
• Related items. The platform's generic identity survival_mean_ibp (mean as an integral of the survival function, under derivative hypotheses) is related but does not fit this setting. Mathlib's layer-cake formula is the general tool for passing between survival functions and moments.
• Welcome contributions. Closed forms for $\int_0^1\!\int_0^1(s+t)^{-1/2}\,ds\,dt$ and $\int_0^1\!\int_0^1\sqrt{st}/(s+t)\,ds\,dt$, which are reusable lemmas, and a general "moments of $\max$ and $\min$ of independent variables from their survival functions" lemma.

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
• S. Beckers, Variances of security price returns based on high, low and closing prices, Journal of Business 56(1) (1983), 97–112.

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

Optional stopping and the size of a test

Section 4 of Herbert Robbins's 1952 address Some aspects of the sequential design of experiments (Bull. Amer. Math. Soc. 58, 527–535, doi:10.1090/S0002-9904-1952-09620-8) isolates a problem that every user of significance tests meets: if the sample size is not fixed in advance, an experimenter can keep sampling until the test rejects. Robbins shows that a fixed-sample test then loses all control of its error probability, and he proposes the compromise of allowing the sample size to range over a window $n_1\le n\le n_2$, with an explicit bound on the resulting error.

The question is still current. "Optional stopping" and "peeking" at accumulating data are a standard concern in clinical trials and online A/B testing, and the modern theory of always-valid inference and confidence sequences (for example Howard, Ramdas, McAuliffe and Sekhon, Time-uniform, nonparametric, nonasymptotic confidence sequences, Ann. Statist. 49 (2021), arXiv:1810.08240) answers exactly the question Robbins raises: how large is the probability that a running statistic crosses a boundary at some time in a range. The earlier treatment Robbins cites is Feller's 1940 discussion of the statistics of ESP experiments.

Setting

Let $x_1,x_2,\dots$ be independent real random variables on a probability space $(\Omega,\mathcal F,P)$, each normal with mean $0$ and variance $1$. This is the null hypothesis $H_0:\theta=0$ for observations that are normal with unknown mean $\theta$ and unit variance; the alternative is $H_1:\theta>0$. Write

$$S_n=x_1+\cdots+x_n,\qquad S_0=0 .$$

The fixed-sample test of size $n$ rejects $H_0$ if and only if

$$S_n>\alpha n^{1/2}\qquad(21)$$

for a real constant $\alpha$. (In this mission $\alpha$ always denotes this test constant; in Section 2 of the paper the same letter is the mean of a coin.) The standard normal distribution function is

$$\Phi(x)=\frac{1}{(2\pi)^{1/2}}\int_{-\infty}^{x}e^{-t^2/2}\,dt .\qquad(23)$$

For integers $n_1\le n_2$ the window probability is

$$g(n_1,n_2,\alpha)=P\bigl[S_n>\alpha n^{1/2}\ \text{for some}\ n_1\le n\le n_2\bigr],\qquad(24)$$

and $\lambda=n_2/n_1$. In Lean these are Phi, S X n ω = ∑ i ∈ Finset.range n, X i ω and g P X n₁ n₂ α, in the namespace RobbinsSeqDesign.OptionalStopping.

Formalization targets

Goal: the window bound (25)

For integers $1\le n_1<n_2$ and every real $\alpha$, with $\lambda=n_2/n_1$,

$$g(n_1,n_2,\alpha)<\frac{1-\Phi(\alpha)}{1-\Phi\!\Bigl(\alpha\cdot\dfrac{\lambda^{1/2}-1}{(\lambda-1)^{1/2}}\Bigr)} .$$

The inequality is strict, as printed, and holds for every real $\alpha$, not only the large values of practical interest.

Milestone: the fixed-sample error (22)

For every $n\ge1$ and real $\alpha$,

$$\varepsilon(\alpha)=P\bigl[S_n>\alpha n^{1/2}\bigr]=1-\Phi(\alpha).$$

Milestone: rejection infinitely often

For every real $\alpha$, with probability $1$ the inequality $S_n>\alpha n^{1/2}$ holds for infinitely many $n$.

Significance

The results. (22) says that the fixed-sample test has error probability $1-\Phi(\alpha)$ whatever $n$ is. The infinitely-often statement says that this guarantee is void under unrestricted optional stopping: sampling until (21) holds rejects a true $H_0$ with probability one, however large $\alpha$ is. The goal (25) quantifies the compromise: if the stopping time is confined to $[n_1,n_2]$, the error probability is at most the fixed-sample error divided by $1-\Phi(\alpha c_\lambda)$, where $c_\lambda=(\lambda^{1/2}-1)/(\lambda-1)^{1/2}<1$ depends only on the window's ratio. For large $\alpha$ and moderate $\lambda$ this keeps the error of the same order as the fixed-sample error; Robbins notes that it is useful when $\lambda$ is not too large and that sharper inequalities can be devised.

Formalizing it. The three statements are classical and their proofs are short on paper, but none is machine-checked for Gaussian partial sums. The goal needs stopping-time machinery for discrete-time Gaussian random walks; the infinitely-often statement is a consequence of the lower half of the law of the iterated logarithm, which Mathlib does not contain. On the platform, DurrettProbability.brownian_limsup_sqrt (proved) gives $\limsup_t B_t/\sqrt t=\infty$ for Brownian motion, a different process, and AzumaWeightedSums.IteratedLog.theorem2_limsup_le_one gives an upper iterated-logarithm bound for weighted sums, the opposite direction; neither states any of the targets here, but both are related infrastructure.

Difficulty

The goal is a maximal inequality over a window of times. The obvious argument, a union bound over $n_1\le n\le n_2$, gives $(n_2-n_1+1)(1-\Phi(\alpha))$, which grows with the window length instead of depending on $\lambda$ alone, and exceeds $1$ for long windows. The events $\{S_n>\alpha n^{1/2}\}$ for different $n$ are strongly dependent, and the boundary $\alpha n^{1/2}$ is curved, so the bound has to account for when, inside the window, the boundary is first crossed; this requires stopping-time arguments for a discrete-time walk that are not yet available for Gaussian random walks in Mathlib. The strictness of the inequality also has to be tracked through the argument. The infinitely-often statement cannot be obtained from the central limit theorem alone, which gives only $P(S_n>\alpha n^{1/2}\ \text{i.o.})\ge 1-\Phi(\alpha)>0$; upgrading this to probability one needs a zero–one law or the law of the iterated logarithm.

Formalization scope

The observations are X : ℕ → Ω → ℝ on a probability space (Ω, P) with [IsProbabilityMeasure P], iIndepFun X P and ∀ i, HasLaw (X i) (gaussianReal 0 1) P; the paper's $x_i$ is X (i - 1). The explicit readings committed to are:

• $\Phi$ is the integral printed in (23) (a local check shows it equals Mathlib's cdf (gaussianReal 0 1)).
• "The probability of rejecting $H_0$" is P.real of the event; (22) is stated for $n\ge1$.
• "With probability 1 … for infinitely many values of $n$" is ∀ᵐ ω ∂P, ∃ᶠ n in atTop, α * √n < S X n ω, for every real $\alpha$.
• The window of (24) is $n_1\le n\le n_2$ with both endpoints; the stray comma printed in "$n_1, \le n$" is a typesetting slip.
• In (25), $\lambda$ is the real quotient $n_2/n_1$, and the hypotheses $1\le n_1<n_2$ make $\lambda>1$ well defined; the inequality is strict and there is no sign restriction on $\alpha$.
• The numeric example "$\alpha=3.09$ then $\varepsilon(\alpha)\cong .001$" and the phrase "useful when $\lambda$ is not too large" are not formalized.

A trivializing formalization is ruled out: $g$ is the probability of the union over the whole window (not the event at $n=n_2$ alone), $\Phi$ is the fixed standard normal distribution function (not an arbitrary monotone function), and the parameter range excludes $\lambda=1$, where Lean's convention $x/0=0$ would replace the right side by $2(1-\Phi(\alpha))$.

A complete development needs the law of a sum of independent Gaussians, the strong Markov property of a Gaussian random walk at a stopping time (or an equivalent first-passage decomposition), and, for the infinitely-often milestone, either the lower law of the iterated logarithm for Gaussian walks or the Hewitt–Savage/Kolmogorov zero–one law combined with the central limit theorem. These pieces are reusable well beyond this mission; contributions of any of them, as separate lemmas, are welcome.

Selected references

• H. Robbins, Some aspects of the sequential design of experiments, Bull. Amer. Math. Soc. 58 (1952), 527–535. https://doi.org/10.1090/S0002-9904-1952-09620-8
• W. Feller, Statistical aspects of ESP, J. Parapsychology 4 (1940), 271–298 (reference [11] of the paper).
• S. R. Howard, A. Ramdas, J. McAuliffe, J. Sekhon, Time-uniform, nonparametric, nonasymptotic confidence sequences, Ann. Statist. 49 (2021), 1055–1080. https://arxiv.org/abs/1810.08240

Why return terms matter

Manufacturers of perishable goods must decide how much inventory risk to leave with retailers. A retailer who pays for every ordered unit may order less than is best for the manufacturer and retailer together; a generous return policy changes that incentive. Pasternack studies this question in a single-period setting, with a fixed selling price, uncertain demand and goodwill costs when customers cannot be served. The article identifies two familiar endpoint policies that fail: no returns, and unlimited returns reimbursed at the full wholesale price. It then investigates partial credit as a way to align the order decisions. Pasternack (1985)

The target here is the article's paired Theorems 1 and 2. They concern one retailer and one manufacturer, and their conclusion is about the order quantity the retailer chooses. The model does not ask the retailer to choose the selling price, nor does it compare realized profits for one particular demand outcome. The value of the result lies in ruling out two whole classes of pricing and return terms before considering how to divide the gains from a coordinated channel. Pasternack (1985), pp. 169–171

The single-period setting

A manufacturer produces at unit cost $c$ and charges the retailer a wholesale price $c_1$. The retailer orders $Q\ge0$ units before observing demand $X$, then sells at a fixed retail price $p$. Unsold units have salvage value $c_3$. A return policy gives the retailer a credit $c_2$ for a fraction $R\in[0,1]$ of the order: $R=0$ permits no returns and $R=1$ permits returns of every leftover unit. The retailer incurs goodwill cost $g$ for each unmet unit of demand; the manufacturer bears the additional cost $g_1$, and $g_2=g+g_1$ is the total goodwill cost. The paper assumes $c_3<c<c_1<p$ and $c_3<c_2\le c_1<p$. Pasternack (1985), pp. 169–170, (1)–(2)

Demand is described by a density $f$ on the nonnegative reals and distribution function $F(Q)=\int_0^Q f(x)\,dx$. From the same order and demand outcome, the paper computes three expected profits: $EP_T(Q)$ for an integrated company store, $EP_R(Q)$ for the independent retailer, and $EP_M(Q)$ for the manufacturer. Their definitions are equations (3), (6) and (8). An optimal order maximizes the relevant expected profit over nonnegative $Q$. The paper calls the channel coordinated when the retailer chooses a system-optimal order, as if the manufacturer operated the store directly. The formal model compares the sets of all such optimal orders, so it also handles a distribution whose CDF is flat over an interval. Pasternack (1985), pp. 170–171, (3), (6), (8)–(10)

Formalization targets

The integrated company's optimal-order equation (5) supplies the benchmark:

$$F(Q_T^*)=\frac{p+g_2-c}{p+g_2-c_3}.$$

The retailer's optimal-order equation (7) includes both $F(Q)$ and $F((1-R)Q)$. Substituting the integrated benchmark gives equation (10), the common comparison used for the two endpoint policies. The first three milestones formalize these conditions, including existence of an integrated optimum. The last two milestones record the separate calculations in the appendix for full-credit returns and no returns. Pasternack (1985), pp. 170–171, 175

The mission goal combines Theorems 1 and 2 as the article does immediately after stating them. With $R=1,c_2=c_1$ or with $R=0$, every system-optimal order fails to be retailer-optimal:

$$\operatorname*{arg\,max}_{Q\ge0}EP_T(Q)\ne\varnothing,\qquad \operatorname*{arg\,max}_{Q\ge0}EP_T(Q)\cap \operatorname*{arg\,max}_{Q\ge0}EP_R(Q)=\varnothing.$$

The disjointness claim is read separately for each endpoint policy. It says more than merely finding one order on which the firms disagree: neither endpoint policy can induce the retailer to choose a system optimum. Pasternack (1985), Theorems 1–2 and following paragraph, p. 171

What the result establishes

The result separates a policy that reimburses all unsold stock at full wholesale price from one that offers no return option. Both may be simple to administer, but neither aligns the retailer's stocking choice with the integrated company's choice under the article's cost ordering. The result makes the paper's subsequent search for partial-credit terms substantive: the coordinating policy lies away from these two endpoints. It does not say that either endpoint always gives a loss, or that a retailer cannot make a profit. The claim concerns the order that maximizes expected channel profit. Pasternack (1985), pp. 171–172

The known result is proved in the article, but its definitions and theorem statements have not been machine-checked as part of this mission. Formalization gives a reusable account of the paper's piecewise expected profits, feasible order quantities and return fraction, and makes explicit the conditions under which the endpoint conclusions hold. Related proved platform statements include Snyder and Shen's wholesale coordination and wholesale under-ordering. They are not imported: their contract data require $0\le v<c_r$, while Pasternack's retailer has no separate own unit cost and the article does not require nonnegative salvage value.

The difficult boundary cases

The claim is sensitive to the demand model. If demand is deterministic, its CDF has a jump, and an order exactly equal to demand can be optimal under both the integrated profit and unlimited full-credit returns. The paper assumes a demand density; continuity of the CDF is therefore material to Theorem 1. Flat parts of a continuous CDF pose a different issue: a theorem identifying just one optimum would lose some orders, so the milestone conditions identify whole sets of maximizers. Pasternack (1985), p. 170, definition of $f$ and (4)–(7)

The no-return case also depends on the meaning of the manufacturer's additional goodwill cost. The paper names $g_1$ as a cost but does not print a separate nonnegativity inequality. If it were allowed to be negative, the appendix's contradiction with $c_1>c$ could disappear. The formalization states $g_1\ge0$, along with $g\ge0$, and identifies this convention openly. Pasternack (1985), pp. 170, 175

Formalization scope

Lean uses a probability measure $D$ supported on $[0,\infty)$ with finite first moment in place of a named density $f$. The theorems assume that $D$ has no atoms, giving the continuous CDF needed by the paper's first order conditions. The profit definitions retain the piecewise formulas of (3), (6) and (8), including the thresholds $(1-R)Q$ and $Q$. Adjacent pieces agree at their boundaries. The fixed retail price and the fraction $R\in[0,1]$ match the paper's setting. The cost ordering is split between fixed costs and an admissible policy, because the theorem compares particular policy choices.

Only $Q\ge0$ is feasible. An optimal-order predicate includes this membership as well as maximality, and coordination compares complete argmax sets. The goal explicitly asserts that a system optimum exists, preventing a vacuous conclusion about orders when there are none. At $R=0$ the retailer profit is independent of $c_2$, so the goal quantifies over every credit without imposing an unused bound on it. The denominator $p+g_2-c_3$ is positive under $c_3<c<p$ and $g,g_1\ge0$. Contributions that develop the optimal-order characterizations, the substitution identity, or the endpoint contradictions within these conventions directly support the goal.

Selected references

• Barry Alan Pasternack, Optimal Pricing and Return Policies for Perishable Commodities, Marketing Science 4(2):166–176, 1985. DOI: 10.1287/mksc.4.2.166.

Motivation

A manufacturer of a perishable good (newspapers, magazines, bread, seasonal fashion, printed books) sells through a retailer who must commit to an order before demand is known. Unsold units lose most of their value; unmet demand costs goodwill. When the retailer alone bears the risk of leftovers, it orders less than an integrated firm would, and the channel as a whole earns less. This inefficiency is the double marginalization of the newsvendor problem, and return policies, under which the manufacturer buys back unsold units, are the instrument publishers and other suppliers of perishable goods actually use against it.

Barry Alan Pasternack's paper Optimal Pricing and Return Policies for Perishable Commodities (Marketing Science, 1985) was the first to show, in a single-period newsvendor model, which return policies restore the integrated firm's order quantity. It became the starting point of the literature on supply-chain contracts: buy-back contracts are now a textbook chapter (Cachon 2003; Snyder and Shen, Fundamentals of Supply Chain Theory), and the paper's result is the standard example of a contract that coordinates a channel while letting the two firms split the profit.

Setting

A manufacturer produces at unit cost $c$. A retailer sells at the fixed retail price $p$. Leftover units are salvaged at $c_3$ per unit. Each unit of unmet demand costs the retailer a goodwill penalty $g \ge 0$ and the manufacturer an additional penalty $g_1 \ge 0$; write $g_2 = g + g_1$. The data satisfy $c_3 < c < p$.

The manufacturer chooses a policy $(c_1, c_2, R)$: the retailer pays $c_1$ per unit ordered and may return up to the fraction $R \in [0,1]$ of its order $Q$ for a credit $c_2$ per unit. The paper assumes

$$c_3 < c < c_1 < p, \qquad c_3 < c_2 \le c_1 < p. \qquad (1),\ (2)$$

Demand $X \ge 0$ is random with distribution function $F$. Three expected profits are defined as functions of the order $Q$: $EP_T(Q)$, equation (3), the profit of a company store in which the manufacturer sells directly; $EP_R(Q)$, equation (6), the independent retailer's profit under the policy; and $EP_M(Q)$, equation (8), the manufacturer's profit when the retailer orders $Q$. An optimal order for a profit function is a $Q \ge 0$ maximizing it over $[0,\infty)$. The policy coordinates the channel when the retailer's optimal orders are exactly the company store's optimal orders: the decentralized channel then produces the integrated firm's quantity.

The Lean development uses the same letters: Costs carries $c, c_3, p, g, g_1$; Costs.Admissible K c1 c2 R is (1)–(2) with $0 \le R \le 1$; EPT, EPR, EPM are (3), (6), (8); IsOptimalOrder and Coordinates are the two notions just defined; $F$ is cdf D for a demand law D.

Formalization targets

Goal: Theorem 3

A policy which allows for unlimited returns at partial credit will be system optimal for appropriately chosen values of $c_1$ and $c_2$. Precisely, for every price $c_1$ with $c < c_1 < p$ there is a credit $c_2$ with

$$c_3 < c_2 < c_1, \qquad c_1 = (p+g) - \frac{(p+g_2-c)(p+g-c_2)}{p+g_2-c_3} \quad (11),$$

such that the policy $(c_1, c_2, R = 1)$ coordinates the channel for every continuous demand distribution on $[0,\infty)$ with finite mean. The credit is chosen before, and independently of, the demand law.

Milestones

1. (4)–(5): the company store has an optimal order, and $Q$ is optimal iff $F(Q) = (p+g_2-c)/(p+g_2-c_3)$.
2. (7): under an admissible policy, $Q$ is optimal for the retailer iff $0 = -c_1 + p + g - F(Q)[p+g-c_2] - F((1-R)Q)[(1-R)(c_2-c_3)]$.
3. (9)–(10): an admissible policy coordinates the channel iff (10) holds at every system-optimal order.
4. (11): with $R = 1$ and $c_2 < c_1$, coordination holds iff (11) holds, whatever the demand law.
5. Appendix, proof of Theorem 3: for $c < c_1 < p$, (11) has a solution $c_2$ with $c_3 < c_2 < c_1$.

Significance

The result. Theorem 3 says that a buy-back contract with full returns at a partial credit aligns the retailer's incentives with the channel's, and that the coordinating credit depends only on costs. The second point carries the paper's practical conclusion: a manufacturer selling one product to many retailers with different demand distributions can post one price and one return credit and still have every retailer order its system-optimal quantity. The one-parameter family of coordinating pairs $(c_1, c_2)$ then splits the channel profit between the firms. The companion mission (Optimal Pricing and Return Policies for Perishable Commodities II) formalizes the negative results, Theorems 1 and 2: neither full credit with unlimited returns nor a no-returns policy coordinates.

Formalizing it. The paper's proofs are first-order conditions and a short algebraic argument. A machine-checked version adds three things. It makes the analytic content explicit: existence of the system optimum, global optimality of the first-order conditions for an arbitrary atomless demand law, and the quantifier structure "one credit for all demand laws". It repairs a gap: the printed argument for $c_3 < c_2$ establishes only $c_2 > c_3 - g_1$, which suffices only when $g_1 = 0$, although the claim holds for all $g_1 \ge 0$. And it gives a reusable newsvendor layer with returns. Related results are proved on Prove2Me in a different model: Snyder–Shen's SupplyChainTheory.buyback_coordinates (Theorem 14.4) and SupplyChainTheory.buyback_profit_identities. They are not referenced here, because their contract data require a retailer cost $c_r > v \ge 0$, which excludes Pasternack's retailer (no own cost), and because they fix the buy-back price and derive the wholesale price, with no range claim.

Difficulty

The algebraic core, milestone 5, is short. The work sits in the analytic milestones. Differentiating under the integral sign in (3) and (6) needs the integrands' piecewise structure and the absence of atoms; the global-maximum claim needs concavity of the expected profits on $[0,\infty)$, including the boundary $Q = 0$. Coordination is a statement about sets of maximizers, not about one first-order condition: when $F$ is flat at the critical fractile, the optimal orders form an interval, and showing that the retailer's maximizers coincide with the system's requires the monotonicity of the retailer's marginal profit, strict where $F$ increases. The naive reading "both first-order conditions hold at $Q^*_T$" proves one inclusion only.

Formalization scope

Demand is a probability measure D on $\mathbb R$ with D (Iio 0) = 0 and finite mean (IsDemand), and $F$ is cdf D. The paper's density is the hypothesis NullSingletonClass D (no atoms), imposed on each theorem that uses it. The expected profits are Lean integrals of the paper's piecewise integrands, written with if. The goodwill costs satisfy $g, g_1 \ge 0$, implicit in the paper. $R$ is a fraction in $[0,1]$. Optimal orders are maximizers over $Q \ge 0$ that are themselves $\ge 0$. Coordination is equality of the retailer's and the company store's sets of optimal orders. The denominator $p + g_2 - c_3$ is positive under these assumptions, so no division is degenerate.

The goal is not the algebraic statement "there is $c_2 \in (c_3, c_1)$ solving (11)": that is milestone 5. A formalization of Theorem 3 must conclude Coordinates, a statement about the maximizers of the actual profit functions (3) and (6), and must place the quantifier over demand laws inside the existence of $c_2$.

A complete development needs: differentiation of parametric integrals with piecewise-linear integrands, concavity of the newsvendor profit, the intermediate value theorem for continuous distribution functions, and the critical-fractile characterization. The newsvendor layer (milestones 1 and 2) is reusable for any single-period contract model. Proofs of the milestones, alternative proofs (for example via the identity $EP_R = k \cdot EP_T + \text{const}$ under (11), which also removes the no-atoms hypothesis), and the profit formulas (12)–(14) at the coordinated optimum are all welcome.

Selected references

• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science 11, 2003, 227–339. https://doi.org/10.1016/S0927-0507(03)11006-7
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019. https://doi.org/10.1002/9781119584445