Operations Research

Motivation

The prophet inequality of optimal stopping compares a gambler, who sees independent non-negative random values $X_1, \dots, X_n$ one at a time and must accept or reject each on arrival, with a prophet who sees them all in advance. Krengel, Sucheston and Garling showed that the gambler can secure $\mathbb E[X_\tau] \ge \tfrac12\,\mathbb E[\max_i X_i]$, and Samuel-Cahn showed that a single threshold suffices. Since Hajiaghayi, Kleinberg and Sandholm (2007) and Chawla, Hartline, Malec and Sivan (2010), prophet inequalities have served as the approximation guarantees of sequential posted-price mechanisms: an online selection rule with a prophet guarantee turns into a truthful mechanism with a revenue guarantee.

The natural multi-choice generalization lets the gambler accept a set of elements, subject to a feasibility constraint. Kleinberg and Weinberg, Matroid Prophet Inequalities (STOC 2012, arXiv:1201.4764), proved that when the feasible sets are the independent sets of a matroid, the factor $\tfrac12$ is still achievable, by an explicit threshold rule, and even when the order of arrival is chosen adaptively by an adversary.

Timeline:

• 1977–78: Krengel and Sucheston, with Garling: the single-choice prophet inequality with factor $\tfrac12$, which is tight.
• 1984: Samuel-Cahn: a single fixed threshold attains $\tfrac12$.
• 2007: Hajiaghayi, Kleinberg, Sandholm: prophet inequalities read as truthful online auctions, with multi-choice prophet inequalities.
• 2010: Chawla, Hartline, Malec, Sivan: posted-price mechanisms via prophet inequalities, and factor $\tfrac12$ for matroids when the algorithm may choose the order of arrival.
• 2012: Kleinberg–Weinberg: factor $\tfrac12$ for every matroid against an online weight-adaptive adversary, and $\tfrac1{4p-2}$ for intersections of $p$ matroids.

Setting

Let $\mathcal U$ be a finite ground set and $\mathcal M = (\mathcal U, \mathcal I)$ a matroid; $\mathcal I$ is its family of independent sets. For each $x \in \mathcal U$ a distribution $F_x$ on $[0,\infty)$ is given; the weights $w(x)$ are independent with $w(x) \sim F_x$, and $w(A) = \sum_{x \in A} w(x)$. Let $\mathrm{OPT}(w) = \max\{w(S) : S \in \mathcal I\}$ and $\mathrm{OPT} = \mathbb E[\mathrm{OPT}(w)]$.

An online weight-adaptive adversary reveals the elements one at a time: it picks $x_i$ knowing $w(x_1), \dots, w(x_{i-1})$ but not $w(x_i)$. An online algorithm maintains a selected set $A_{i-1} \in \mathcal I$ and, when $x_i$ arrives with its weight, irrevocably accepts or rejects it, keeping $A_i$ independent. A threshold rule offers $x_i$ a threshold $T_i$ computed from the revealed prefix (and $T_i = \infty$ when $A_{i-1} \cup \{x_i\} \notin \mathcal I$) and accepts iff $w(x_i) \ge T_i$.

The algorithm of the paper uses a ghost sample: an independent copy $w'$ of the weights. Let $B$ be a $w'$-maximum-weight basis. For an independent set $A$, among the partitions $B = C \sqcup R$ with $R \cap A = \emptyset$ and $A \cup R$ a basis, $R(A)$, $C(A)$ denote one maximizing $w'(R)$. The algorithm (9) sets

$$T_i = \tfrac12\,\mathbb E_{w'}\big[w'(R(A_{i-1})) - w'(R(A_{i-1}\cup\{x_i\}))\big].$$

Formalization targets

Goal: the matroid prophet inequality

For every matroid on a finite ground set, every family of distributions $F_x$ on $[0,\infty)$ with finite means, and every online weight-adaptive adversary, the set $A$ selected by the algorithm (9) satisfies

$$\mathbb E[w(A)] \;\ge\; \tfrac12\,\mathrm{OPT}.$$

The goal is stated for the paper's own algorithm, which is stronger than the existence statement of §3.

Milestones

1. Proposition 1 (with Definition 1): any threshold rule with $\alpha$-balanced thresholds,

$$\sum_{x_i\in A} T_i \ge \tfrac1\alpha\,\mathbb E[w'(C(A))], \qquad \sum_{x_i\in V} T_i \le \big(1-\tfrac1\alpha\big)\,\mathbb E[w'(R(A))],$$

earns $\mathbb E[w(A)] \ge \tfrac1\alpha\,\mathrm{OPT}$. 2. The identity behind (9) = (10), and the telescoping identity $\sum_{x_i \in A} T_i = \tfrac12\,\mathbb E[w'(C(A))]$ (Property (2) for $\alpha = 2$). 3. Lemma 1 (bijective basis exchange, and its weighted form), Lemma 2 ($R(A)$ is a maximum-weight basis of the contraction $\mathcal M/A$), Lemma 3 ($S \mapsto w'(R(S))$ is submodular on subsets of an independent set). 4. Inequalities (11) and (12), and Proposition 2:

$$\sum_{x_i \in V}\big[w'(R(A_{i-1})) - w'(R(A_{i-1}\cup\{x_i\}))\big] \le w'(R(A)),$$

pointwise in $w' \ge 0$; then Property (3) with $\alpha = 2$ for the thresholds (9).

Significance

The theorem gives the optimal constant: already for a rank-one matroid (choose one element) no online algorithm beats $\tfrac12$. It covers every matroid with one algorithm, including uniform, partition, graphic and transversal matroids, which model capacity, unit-demand and spanning-tree constraints. Through the reduction of Chawla et al., the paper derives from it order-oblivious posted-price mechanisms that are 2-approximations to the optimal revenue in single-parameter settings with matroid feasibility and, through the adaptive adversary, in multi-dimensional unit-demand settings (§6 of the paper). The decomposition through $\alpha$-balanced thresholds is reused in the paper for intersections of $p$ matroids, with factor $\tfrac1{4p-2}$.

The result has been proved since 2012; it has not been formalized. The mission produces a machine-checked development of the model (online adaptive adversaries, threshold rules, the ghost-sample expectations), of the general reduction (Proposition 1), and of the matroid facts the algorithm relies on, notably the bijective exchange lemma (Schrijver, Corollary 39.12a), which is not in Mathlib.

Difficulty

The obvious argument fixes the order of arrival and compares the algorithm with the prophet item by item. It fails here because the order is chosen adaptively from the revealed weights, so the set of elements still to come is random and correlated with the past. The proof must instead compare the algorithm's realized selection with a ghost optimum $B$ built from an independent sample, and bound the value the algorithm forgoes by the value the ghost optimum could still add, $\mathbb E[w'(R(A))]$. The step that needs matroid structure is Property (3): the total threshold offered to any set $V$ that could still be added must be at most half of $\mathbb E[w'(R(A))]$. The thresholds were computed along the history $A_0 \subseteq A_1 \subseteq \dots$, not at the final $A$, so the bound requires the submodularity of $S \mapsto w'(R(S))$ (Lemma 3) and a weight-dominating exchange between $V$ and $R(A)$ in the contraction $\mathcal M/A$. Neither holds for general downward-closed families.

Formalization scope

• The ground set is a Fintype α; the matroid is Mathlib's Matroid α with ground set Set.univ; sets are Finset α; contraction is Matroid.contract.
• The distributions are F : α → Measure ℝ, probability measures with F x (Set.Iio 0) = 0 (support in $[0,\infty)$) and Integrable id (F x) (finite means). The weight law is Measure.pi F, and every expectation is a Bochner integral over it. Finite means make $\mathrm{OPT}(w)$, $w(A)$ and the integrands of the thresholds integrable, so no expectation is a junk value.
• $\mathrm{OPT}(w)$ is a maximum over the nonempty finset of independent sets. The maximum-weight basis $B(w')$ and the maximizer $R(A)$ are fixed by choice when weights tie; Lemma 2 shows $w'(R(A))$ does not depend on the choice. $R(A)$ is required to be disjoint from $A$, as Lemma 2's placement of $R(A)$ in $\mathcal M/A$ needs.
• A threshold rule is a real-valued function of the current selection, the revealed list, the weights and the arriving element, non-negative, depending on the weights only through revealed ones, measurably; the value $\infty$ on infeasible steps is an independence guard in the acceptance test. "Monotone algorithm" in Proposition 1 means such a rule.
• An adversary is a deterministic map from the revealed list and the weights to the next unrevealed element, depending only on revealed weights and measurable. Randomized adversaries are mixtures of these.
• Lemma 1, part 2 is stated for disjoint $V$ and $R$: as printed it fails when they overlap, and the paper uses it only for disjoint sets.

The goal fixes the thresholds by (9) through $B$, $R(\cdot)$ and the ghost expectation; a statement in which the thresholds are free parameters assumed to satisfy (2)–(3) would be Proposition 1 and is not the goal.

Contributions are welcome at every level: the measurability of the online run, the exchange lemma for Mathlib matroids, the greedy characterization of maximum-weight bases of a contraction, and the probabilistic core (7) of Proposition 1. The matroid lemmas are reusable beyond this mission, in particular by the matroid-intersection mission of the same paper.

Selected references

• R. Kleinberg, S. M. Weinberg, Matroid Prophet Inequalities, STOC 2012; arXiv:1201.4764v1. https://arxiv.org/abs/1201.4764 , https://doi.org/10.1145/2213977.2213991
• U. Krengel, L. Sucheston, Semiamarts and finite values, Bull. Amer. Math. Soc. 83, 745–747, 1977.
• U. Krengel, L. Sucheston, On semiamarts, amarts, and processes with finite value, Advances in Probability and Related Topics 4, 197–266, 1978.
• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Annals of Probability 12(4), 1213–1216, 1984.
• M. T. Hajiaghayi, R. Kleinberg, T. Sandholm, Automated mechanism design and prophet inequalities, AAAI 2007, pp. 58–65.
• S. Chawla, J. Hartline, D. Malec, B. Sivan, Multi-parameter mechanism design and sequential posted pricing, STOC 2010, pp. 311–320.
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003 (Corollary 39.12a).

Motivation

Random time changes occur when a process is observed on an operational clock rather than calendar time. In queueing models, for example, an arrival-count path may be evaluated at an evolving service clock. A functional limit theorem for the outer path and another for the clock are useful together only when evaluating one path at the times supplied by the other preserves convergence. Ward Whitt's 1980 paper studies several path operations with this question in mind; composition is its first main operation. The issue is specific to paths with jumps, because a small shift of the clock can move an evaluation across a jump.

Setting

Let $T_1,T_2,T_3$ be nonempty intervals of real time, with $T_2\subseteq T_3$, and let $(S,m)$ be a complete separable metric space. The càdlàg path space $D(T,S)$ consists of paths that are right continuous and have left limits on $T$. Its subspace $C(T,S)$ contains the continuous paths. The nondecreasing clock space $D_0(T_1,T_2)$ consists of càdlàg real-valued paths on $T_1$ that are nondecreasing and take their values in $T_2$. Its subspace $C_0(T_1,T_2)$ contains the continuous, strictly increasing clocks. For $x\in D(T_3,S)$ and $y\in D_0(T_1,T_2)$, composition is the path $(x\circ y)(t)=x(y(t))$ on $T_1$.

Convergence uses the Skorohod $J_1$ topology. On a compact interval $[a,b]$, let $\Lambda_{[a,b]}$ be the increasing homeomorphisms of $[a,b]$ and let $e(t)=t$. With $\rho_{[a,b]}$ denoting uniform distance, Whitt's metric is

$$d_{[a,b]}(u,v)=\inf_{\lambda\in\Lambda_{[a,b]}} \max\{\rho_{[a,b]}(\lambda,e),\rho_{[a,b]}(u,v\circ\lambda)\}.$$

Thus close paths may have nearby jumps at different times, provided an increasing time change aligns them. On a general interval, convergence is checked on compact subintervals whose endpoints are continuity points of the limit or endpoints of the full interval. Whitt gives this definition in §2, then gives $C$, $C_0$, and $D_0$ in §3. All subsets carry relative topologies and products carry product topologies.

Formalization targets

Composition at a continuous outer path

For $x_n\to x$ in $D(T_3,S)$ and $y_n\to y$ in $D_0(T_1,T_2)$, the first milestone states

$$x\in C(T_3,S)\quad\Longrightarrow\quad x_n\circ y_n\to x\circ y\text{ in }D(T_1,S).$$

The path-space definition and the two preparatory milestones are a small-oscillation partition for a càdlàg path, cited by Whitt from Billingsley, and Whitt's Lemma 2.2, which relates convergence on a compact interval to convergence on the two pieces made by splitting it at a continuity point.

Composition at a strictly increasing clock

The second case, and the combined goal, also allow the outer limit path to jump. Let $\partial_T T_1$ mean the endpoints of $T_1$ that belong to $T_1$. The corrected target is

$$\left[x\in C(T_3,S)\quad\text{or}\quad \bigl(y\in C_0(T_1,T_2)\ \text{and} x\text{ is continuous at }y(t)\text{ for every }t\in\partial_T T_1\bigr)\right] \Longrightarrow x_n\circ y_n\to x\circ y\text{ in }D(T_1,S).$$

The goal includes both cases for simultaneously varying $x_n$ and $y_n$. The endpoint condition is vacuous for an endpoint excluded from $T_1$. It is part of the strictly increasing clock case only; it imposes no extra restriction when the outer limit path is continuous.

Significance

This theorem supplies a precise condition for carrying two path limits through a random time transformation. In particular, the assertion includes convergence of the composed paths as elements of a càdlàg space, not merely convergence of their values at individual times. The distinction matters at jumps: pointwise convergence does not control the placement or ordering of nearby jumps. The result is a deterministic continuity statement that can be paired with probabilistic mapping theorems when the corresponding random paths are available.

Whitt proved the composition theorem in 1980, subject to the endpoint issue described below. The formalization work here is to construct its path-space interface in Lean, state the corrected continuity theorem with every domain condition visible, and eventually replace the open sorry proofs with checked proofs. The interface can also support the paper's later results on reflection, first passage, and time reversal; those results are separate missions. No proof of this mission's goal is claimed yet.

Difficulty

The tempting argument is to use separate continuity of $x_n\to x$ and $y_n\to y$ and then substitute $y_n(t)$ into the first convergence. That argument loses control of evaluations near a jump of $x$. A $J_1$ time change may align a jump of $x_n$ with the corresponding jump of $x$, while the clock $y_n$ may cross those times differently. Continuity of the outer limit path removes that difficulty in one case; in the other, the clock must be continuous and strictly increasing. The source explicitly shows that composition is not continuous on all of $D\times D_0$ (§3, p. 75).

The endpoints impose a further obstruction because increasing homeomorphisms of a closed time interval fix its endpoints. Bauer's Remark on p. 75 observes a failure at the right endpoint. There is a symmetric failure at the left endpoint, so the statement here includes both. This is a correction to the printed theorem, not a new claim that the uncorrected theorem is true.

Formalization scope

Paths are represented as total functions $\mathbb R\to S$, with only values on the named interval used. The domain assumptions OrdConnected and Nonempty express nonempty real intervals. The outer interval $T_3$ is also required to have nonempty interior: the formal convergence predicate checks only compact intervals $[a,b]$ with $a<b$, so on a one-point $T_3$ it imposes nothing, and the $C\times D_0$ case would fail for constant outer paths with different values. A clock's range condition is explicit, as is nondecreasingness for every prelimit clock. Membership of all paths in the relevant càdlàg spaces is part of the convergence predicates. The output predicate likewise requires every composition and its limit to be càdlàg. This rules out the trivialization in which one merely proves convergence of selected point evaluations or assumes the compositions already have the conclusion's path-space properties.

The compact uniform distance and the infimum over time changes take values in $[0,\infty]$. They use the actual metric on $S$, not a real supremum with a default value on an unbounded set. A time change is a total function whose restriction to the compact interval is continuous, strictly increasing, and onto. Continuity at a time means continuity relative to the path's interval. The general-interval convergence predicate checks the compact intervals specified by Whitt and requires each sequence member to belong to $D$. The theorem is written as sequential continuity; Whitt's $J_1$ spaces are metrizable, making that equivalent to topological continuity. The real-valued clock space uses the relative topology inherited from real-valued càdlàg paths.

The endpoint correction is exact in the Lean statement. At the right endpoint, take $T_1=T_2=T_3=[0,1]$, $y(t)=t$, $y_n(t)=(1-1/n)t$ for $n\ge2$, and $x=1_{\{1\}}$. Then $x\circ y_n$ is zero while $(x\circ y)(1)=1$. At the left endpoint, take $T_1=T_2=[0,1]$, $T_3=[-1,2]$, $y_n=y=e$, $x=1_{[0,2]}$, and $x_n=1_{[1/n,2]}$. The outer paths converge in $J_1$ on $T_3$, but the compositions disagree at $0$. Both examples show why continuity of $x$ at the image of every included endpoint is required in the $D\times C_0$ case.

The development needs the càdlàg definition, $J_1$ metric and convergence predicates, compact restriction lemma, and the finite oscillation partition. Their definitions and lemmas are reusable for other functionals on path spaces. Contributions that prove the milestones and goal under the stated hypotheses are welcome. This mission does not formalize the Borel measurability or probability-measure machinery discussed elsewhere in Whitt's paper; Theorem 3.1 itself is a deterministic continuity claim.

Selected references

• Ward Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 67–85, 1980. DOI: 10.1287/moor.5.1.67.

Motivation

Random coordinate descent minimizes a smooth convex function $f:\mathbb R^n\to\mathbb R$ by updating one coordinate at a time, chosen at random. Each iteration needs a single partial derivative instead of the full gradient, which is what makes the method usable on problems whose dimension is in the millions or billions ("huge-scale" problems). Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global efficiency estimates for such methods and started a large literature on randomized block and coordinate methods.

The basic method RCDM of the paper takes, along coordinate $i$, a step of length $1/L_i$, where $L_i$ is a Lipschitz constant of the $i$-th partial derivative along the $i$-th coordinate. For simple functions these constants are known; for more complicated ones they are not, and a practical method has to estimate them on the fly. Section 6.1 of the paper analyses a backtracking strategy with restore for this purpose and proves that it keeps the efficiency of RCDM up to a constant factor. This mission formalizes that analysis, Theorem 7 of the paper.

Setting

Write $\nabla_i f(x)=\partial f/\partial x_i(x)$ and $e_i$ for the $i$-th standard basis vector of $\mathbb R^n$, $n\ge1$. The function $f$ is convex and differentiable, attains its minimum $f^*=f(x^*)$, and its partial derivatives are coordinate-wise Lipschitz with constants $L_i>0$ ((2.2) with one-dimensional blocks):

$$|\nabla_i f(x+ue_i)-\nabla_i f(x)|\le L_i|u|\qquad(x\in\mathbb R^n,\ u\in\mathbb R,\ i=1,\dots,n).$$

The weighted norm and its dual are $\|x\|_1=(\sum_iL_ix_i^2)^{1/2}$ and $\|g\|_1^*=(\sum_ig_i^2/L_i)^{1/2}$ ((2.7) with $\alpha=1$), and

$$R_1(x_0)=\max_x\Big\{\max_{x^*\in X^*}\|x-x^*\|_1:\ f(x)\le f(x_0)\Big\}$$

measures the size of the initial level set, $X^*$ being the set of minimizers.

The random adaptive coordinate descent method RACDM$(x_0)$ (6.1) keeps estimates $\hat L_1,\dots,\hat L_n$, initialised with given lower bounds $L_i^0\in(0,L_i]$. At iteration $k$ it

1. draws $i=i_k$ uniformly from $\{1,\dots,n\}$;
2. sets $x_{k+1}=x_k-\hat L_i^{-1}\nabla_if(x_k)e_i$ and, as long as $\nabla_if(x_k)\cdot\nabla_if(x_{k+1})<0$, doubles $\hat L_i$ and recomputes $x_{k+1}$;
3. halves $\hat L_i$.

The loop test uses only the sign of one partial derivative and never a function value. With $\varphi_k=\mathbb E f(x_k)$ (the expectation over $i_0,\dots,i_{k-1}$) and $N_k$ the number of partial derivatives computed in iterations $0,\dots,k$, Theorem 7 states three facts about this method.

Formalization targets

Goal: Theorem 7, item 2, (6.2)

$$\varphi_k-f^*\ \le\ \frac{8nR_1^2(x_0)}{16+3k},\qquad k\ge0.$$

This is the rate of RCDM$(0,x_0)$, $\varphi_k-f^*\le 2nR_1^2(x_0)/(k+4)$ ((2.14)), with a larger constant.

Milestones

1. (6.4) — started from an estimate $0<\hat L_i\le L_i$, the doubling loop terminates and the accepted estimate satisfies $\hat L_i\le2L_i$.
2. Theorem 7, item 1 — at the beginning of each iteration $\hat L_i\le L_i$ for every $i$.
3. One-step decrease (proof of Theorem 7, p. 19) — $f(x_k)-f(x_{k+1})\ge\frac{3}{8L_{i_k}}(\nabla_{i_k}f(x_k))^2$.
4. Expected decrease (proof of Theorem 7, p. 19) — $f(x_k)-\mathbb E_{i_k}f(x_{k+1})\ge\frac3{8n}(\|\nabla f(x_k)\|_1^*)^2$.
5. Theorem 7, item 3, (6.3) — $N_k\le 2(k+1)+\sum_{i=1}^n\log_2(L_i/L_i^0)$.

Significance

The result shows that the constants $L_i$ in RCDM need not be known: a method that starts from any lower bounds and adjusts them by doubling and halving converges at the same $O(nR_1^2(x_0)/k)$ rate, and pays on average about two partial derivatives per iteration plus a logarithmic one-time overhead. This is what makes random coordinate descent applicable to functions whose coordinate smoothness is not available in closed form, and the doubling-with-restore pattern recurs in later adaptive and accelerated coordinate methods (the paper itself indicates the same technique for its accelerated method, (6.5)).

The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The known-constant analogues for scalar coordinates are on Prove2Me in Bubeck's §6.4 development (the one-step and expected decreases are proved there; the rate is open). This mission adds a formal model of the adaptive method itself, including its doubling loop as a first-failure search, and the three statements of Theorem 7 on top of the published coordinate-descent definitions.

Difficulty

The analysis of RCDM rests on the one-step bound $f(x)-f(x-L_i^{-1}\nabla_if(x)e_i)\ge(\nabla_if(x))^2/(2L_i)$, which follows from the smoothness of $f$ along the coordinate line. For RACDM the step uses an estimate $\hat L_i$ that may be smaller than $L_i$, and then the same argument gives no decrease at all: a step that is too long can increase $f$. The method never checks function values, so the decrease has to be extracted from the sign test alone, and it holds only because $f$ is convex along the line, not merely smooth. A second point is that the estimates are random and depend on the whole history, so the expected decrease must hold for every state the method can reach; this is what item 1 secures. The counting statement needs the exact number of loop iterations, so the loop has to be modelled as the least number of doublings after which the test fails, not as some number of doublings.

Formalization scope

The formalization works with scalar coordinates ($N=n$, as the paper does in §6.1) on EuclideanSpace ℝ (Fin n), coordinates indexed $0,\dots,n-1$. It reuses the published definition ConvexOptAlg_CoordDescent_Defs: IsCoordSmooth f g L is (2.2) with an explicit gradient map $g=\nabla f$, wnorm L 1 and wnormDual L 1 are $\|\cdot\|_1$ and $\|\cdot\|_1^*$, and rcdExpect L 0 k is the expectation over $k$ uniform draws as a finite weighted sum. The mission's own definition NesterovRCD.Adaptive.RACDM encodes the trial point, the number of doublings (a minimum over $\mathbb N$), one iteration, the run along an explicit sequence of draws, and the count $N_k$.

The following choices are made explicitly.

• Step 3 of (6.1) is printed "Set $L_{i_k}:=\frac12L_{i_k}$"; it is read as $\hat L_{i_k}:=\frac12\hat L_{i_k}$, as the paper's proof requires. The true constants $L_i$ never change and enter only hypotheses and bounds.
• $R_1(x_0)$ is not computed: the goal takes any $R$ with $\|x-y^*\|_1\le R$ for all $x$ in the level set and all minimizers $y^*$. "$X^*$ nonempty" is a hypothesis; "$X^*$ bounded" follows from the existence of $R$.
• Implicit hypotheses made explicit: $n\ge1$; $L_i^0>0$ and $L_i^0\le L_i$; in the milestones, $0<\hat L_i\le L_i$ on the entry state.
• Convexity is assumed in the statements that need it (the decreases and the rate); (6.4) and items 1 and 3 hold without it and are stated without it.
• $N_k$ counts $d_j+1$ evaluations of $\nabla_{i_j}f$ at iteration $j$ with $d_j$ doublings, the count the paper's proof uses; counting $\nabla_{i_j}f(x_j)$ as well would give $3(k+1)+\sum_i\log_2(L_i/L_i^0)$.

A trivializing encoding is ruled out: the loop count is the least $d$ at which the sign test fails (an arbitrary admissible $d$ would change the method and make the count meaningless), the draws are uniform, and the rate is stated in the norm of the true constants $L_i$, not of the estimates. Contributions welcome: proofs of the milestones, a one-dimensional co-coercivity lemma for convex smooth functions of one variable (reusable well beyond this mission), and the recursion argument from the expected decrease to the rate.

Selected references

• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, CORE Discussion Paper 2010/2, Université catholique de Louvain, 2010. Journal version: SIAM J. Optim. 22(2) (2012) 341–362. doi:10.1137/100802001
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (reference [6] of the paper; inequality (2.1.17)). doi:10.1007/978-1-4419-8853-9
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4) (2015) 231–357, §6.4. arXiv:1405.4980

Motivation

Dynamic programming rests on time consistency: a control that is optimal when viewed from time $0$ stays optimal when viewed from any later time. Many problems of mathematical finance lack this property. The continuous-time mean–variance portfolio problem (Zhou–Li 2000) contains a variance, that is, a nonlinear function of an expectation, and state-dependent risk aversion (Björk–Murgoci–Zhou) lets the criterion itself depend on the current state. For such problems an optimal control computed today is abandoned tomorrow, and the HJB equation is not available.

One response, going back to the game-theoretic view of non-commitment (Ekeland–Lazrak, arXiv:math/0604264; Björk–Murgoci, SSRN 1694759), is to replace optimality by equilibrium: a control that no "future self" can improve by deviating on an infinitesimally short interval. Those works consider feedback (Markov) controls. Hu, Jin and Zhou (arXiv:1111.0818v1) define equilibrium within open-loop controls for a general stochastic linear–quadratic (LQ) problem with random coefficients, and characterize it by a flow of forward–backward SDEs, in the spirit of the stochastic maximum principle (Peng 1990). This mission formalizes that characterization: §2 and §3 of the paper, up to Theorem 3.2. The other two missions of the series build on it. Mission II treats a scalar state with deterministic coefficients (Theorem 4.4), and Mission III treats mean–variance portfolio selection (Theorem 5.4).

Setting

Let $W=(W^1,\dots,W^d)$ be a standard $d$-dimensional Brownian motion on $(\Omega,\mathcal F,\mathbb P)$ with its filtration $(\mathcal F_t)$, and let $T>0$. A control is a process $u\in L^2_{\mathcal F}(0,T;\mathbb R^l)$, that is, progressively measurable with $\mathbb E\int_0^T|u_s|^2ds<\infty$. Its state $X$ solves the linear SDE

$$dX_s=[A_sX_s+B_s'u_s+b_s]\,ds+\sum_{j=1}^d[C^j_sX_s+D^j_su_s+\sigma^j_s]\,dW^j_s,\qquad X_0=x_0.$$

Here $A$ is a bounded deterministic $n\times n$ matrix function. $B$ ($l\times n$), $C^j$ ($n\times n$) and $D^j$ ($n\times l$) are essentially bounded progressive processes, and $b,\sigma^j\in L^2_{\mathcal F}(0,T;\mathbb R^n)$. At time $t$, with state $x_t$ and $\mathbb E_t=\mathbb E[\cdot\mid\mathcal F_t]$, the cost is

$$J(t,x_t;u)=\tfrac12\mathbb E_t\!\int_t^T\!\big[\langle Q_sX_s,X_s\rangle+\langle R_su_s,u_s\rangle\big]ds+\tfrac12\mathbb E_t\langle GX_T,X_T\rangle-\tfrac12\langle h\,\mathbb E_tX_T,\mathbb E_tX_T\rangle-\langle\mu_1x_t+\mu_2,\mathbb E_tX_T\rangle.$$

$Q,R$ are bounded symmetric processes with $Q,R\succeq0$, and $G,h$ are symmetric with $G\succeq0$. The last two terms make the problem time-inconsistent. Given $u^*$ with state $X^*$, the spike variation at $t$ is $u^{t,\varepsilon,v}_s=u^*_s+v\mathbf 1_{[t,t+\varepsilon)}(s)$ for $v\in L^2_{\mathcal F_t}(\Omega;\mathbb R^l)$. The control $u^*$ is an equilibrium (Definition 2.1) if for every $t\in[0,T)$ and every such $v$, almost surely

$$\liminf_{\varepsilon\downarrow0}\frac{J(t,X^*_t;u^{t,\varepsilon,v})-J(t,X^*_t;u^*)}{\varepsilon}\ge0.$$

For each $t$, the first adjoint process $(p(\cdot;t),k(\cdot;t))$ solves on $[t,T]$ the BSDE (3.1) with driver $A'p+\sum_j(C^j)'k^j+QX^*$ and terminal value $GX^*_T-h\,\mathbb E_tX^*_T-\mu_1X^*_t-\mu_2$. The second adjoint process $(P(\cdot;t),K(\cdot;t))$ solves the matrix BSDE (3.2) with terminal value $G$. With these, define

$$\Lambda(s;t)=B_sp(s;t)+\sum_j(D^j_s)'k^j(s;t)+R_su^*_s,\qquad H(s;t)=R_s+\sum_j(D^j_s)'P(s;t)D^j_s.$$

Formalization targets

Goal: Theorem 3.2 (p. 7)

Suppose $u^*\in L^2_{\mathcal F}$, its state $X^*$, and for every $t\in[0,T)$ a solution $(p(\cdot;t),k(\cdot;t))$ of (3.1) are given, and suppose $\Lambda$ satisfies condition (3.4):

$$\mathbb E_t\!\int_t^T|\Lambda(s;t)|\,ds<+\infty,\qquad\lim_{s\downarrow t}\mathbb E_t[\Lambda(s;t)]=0\quad\text{a.s., for all }t\in[0,T).$$

Then $u^*$ is an equilibrium control.

Milestones

1. $P(s;t)\succeq0$ (§3, p. 5).
2. The perturbation decomposition $X^{t,\varepsilon,v}=X^*+Y+Z$, with $\mathbb E_t[Y_s]=0$, $\mathbb E_t\sup|Y|^2=O(\varepsilon)$ and $\mathbb E_t\sup|Z|^2=O(\varepsilon^2)$ (proof of Proposition 3.1, p. 5).
3. Proposition 3.1, the expansion

$$J(t,X^*_t;u^{t,\varepsilon,v})-J(t,X^*_t;u^*)=\mathbb E_t\!\int_t^{t+\varepsilon}\!\Big\{\langle\Lambda(s;t),v\rangle+\tfrac12\langle H(s;t)v,v\rangle\Big\}ds+o(\varepsilon).$$

Significance

Theorem 3.2 is the paper's general tool. Its two explicit results are applications of it. With a scalar state and deterministic coefficients, a pair of coupled Riccati-type equations gives a linear feedback equilibrium (Theorem 4.4). In mean–variance portfolio selection with state-dependent risk aversion and a possibly random risk premium, the equilibrium strategy is found through a quadratic BSDE (Theorem 5.4). Each is proved by exhibiting a solution of the flow (3.6) and checking (3.4). The theorem therefore separates the existence question (solving a flow of FBSDEs) from the equilibrium question. The paper notes that the general existence question remains open.

The results are proved in the paper and have no machine-checked proof. The mission produces a precise statement of open-loop equilibrium for a stochastic LQ problem with random coefficients, together with Lean statements of the spike expansion and of the adjoint flows. Mission II and Mission III restate the same model, and their final steps apply this theorem. Formal proofs of the milestones exercise Itô calculus for linear SDEs and BSDEs with bounded coefficients: product rules, conditional $L^2$ estimates, and uniqueness and sign properties of linear BSDEs. This is infrastructure that Mathlib does not yet have.

Difficulty

The obvious argument is a first-order expansion of $J$ in $\varepsilon$. It fails because the spike changes the control by $v$, which is not small, on a set of small measure. The state's deviation is then of order $\sqrt\varepsilon$ in $L^2$, its square contributes at order $\varepsilon$, and a second-order term $H(s;t)$ appears that a first-order adjoint cannot capture. Two features are absent from the classical maximum principle. The adjoint equations form a whole flow indexed by $t$, because the terminal value of (3.1) contains $\mathbb E_t X^*_T$ and $X^*_t$. And every statement is conditional on $\mathcal F_t$, so the expansion has to hold almost surely at the level of conditional expectations. That rules out arguments based on unconditional expectations.

Formalization scope

Brownian motion, $L^2_{\mathcal F}$, Itô integrals and SDE solutions come from the published definition Peng1990_SMP_Stochastic. The formalization commits to the following conventions.

• The filtration is the natural, uncompleted filtration of $W$. This changes no statement.
• The state from time $t$ (2.2) is the full-horizon state of the control that equals $u^*$ before $t$.
• The spike is additive on $[t,t+\varepsilon)$.
• Definition 2.1 uses the lower limit, in $\overline{\mathbb R}$, along every sequence $\varepsilon_k\downarrow0$, almost surely for each sequence, for every state of $u^*$ and of each perturbed control. The page writes "lim". That limit need not exist for merely bounded measurable $R$, and the proof of Theorem 3.2 only bounds the quotient from below.
• Each adjoint BSDE lives on $[t,T]$, not on $[0,T]$. Equation (3.2) is read entrywise, with symmetric values.
• Condition (3.4) is encoded version-robustly. Part (a) is the generalized conditional expectation, via $\mathcal F_t$-sets of full union. Part (b) requires a jointly measurable process that is, for almost every $s$, a version of $\mathbb E_t[\Lambda(s;t)]$ and that tends to $0$ as $s\downarrow t$.
• The $O(\cdot)$ estimates carry an explicit constant times $|v|^2$, and suprema are taken over rational times.
• "Essentially bounded" and "a.s., a.e." mean $ds\otimes d\mathbb P$-almost everywhere.

The conclusion of the goal is Definition 2.1 itself. It mentions neither $\Lambda$ nor the adjoint processes, so the goal cannot be closed by unfolding. A definition of equilibrium in terms of (3.4) or (3.5) would make Theorem 3.2 trivially true and is ruled out. Condition (3.5) of p. 6 is not a hypothesis of any statement. A degenerate, noise-free example checks that the hypotheses of the goal can hold together.

Contributions are welcome as follows. Proofs of the three milestones are reusable for Missions II and III and for any spike-variation argument. So are general lemmas on linear SDEs and BSDEs over Peng's Itô integral: uniqueness, conditional moment bounds, the Itô product rule, and positivity of linear matrix BSDEs.

Selected references

• Y. Hu, H. Jin, X. Y. Zhou, Time-Inconsistent Stochastic Linear–Quadratic Control, arXiv:1111.0818v1, 2011; SIAM J. Control Optim. 50(3), 2012. https://arxiv.org/abs/1111.0818 , https://doi.org/10.1137/110853960
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28 (1990), 966–979. https://doi.org/10.1137/0328054
• J. Yong, X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3
• T. Björk, A. Murgoci, A general theory of Markovian time inconsistent stochastic control problems, SSRN 1694759, 2010. https://ssrn.com/abstract=1694759
• I. Ekeland, A. Lazrak, Being serious about non-commitment: subgame perfect equilibrium in continuous time, arXiv:math/0604264, 2006. https://arxiv.org/abs/math/0604264
• T. Björk, A. Murgoci, X. Y. Zhou, Mean–variance portfolio optimization with state-dependent risk aversion, Math. Finance 24(1) (2014), 1–24. https://doi.org/10.1111/j.1467-9965.2011.00515.x
• X. Y. Zhou, D. Li, Continuous-time mean-variance portfolio selection: a stochastic LQ framework, Appl. Math. Optim. 42 (2000), 19–33. https://doi.org/10.1007/s002450010003
• Companion missions: Time-Inconsistent Stochastic Linear–Quadratic Control II (Theorem 4.4) and III (Theorem 5.4), same source.

Motivation

A manufacturer must commit to production before its retail customer knows what the market will demand, while the customer would rather postpone its purchase until better information arrives. Left uncoordinated, each firm protects itself: the customer inflates forecasts it is not bound by, and the manufacturer, discounting those forecasts, builds less than the supply chain as a whole should. Quantity flexibility (QF) contracts, used in practice in the electronics and computer industries (Sun Microsystems, Solectron, Nippon Otis and others are cited in the paper), address this by tying the customer's forecast to a band: the manufacturer guarantees supply up to a percentage above the forecast, and the customer promises to buy at least a percentage below it.

Tsay (1999) gives a two-stage model of such a contract with a demand signal that arrives between production and purchase, shows that a supply chain without commitment underproduces, and characterizes when a QF contract restores efficiency. This mission formalizes the efficiency result for the case in which the signal predicts demand perfectly (Proposition 6(a)), together with the steps of the equilibrium that it rests on.

Setting

A manufacturer (EM) produces at unit cost $m$ and sells to a retailer at unit transfer price $c$; the retailer sells at price $p$, unsold units are salvaged at $u$ at either site, and each unit of unmet demand costs a goodwill loss $s$. The standing assumptions are $p > m > 0$, $u < m$ and $s \ge 0$.

Before production, the retailer states a forecast $q \ge 0$. A QF contract $\{c,(\alpha,\omega)\}$ with $\omega\in[0,1]$ and $\alpha\ge-\omega$ obliges the EM to make up to $q(1+\alpha)$ available and the retailer to buy at least $q(1-\omega)$. The EM then builds $Q$. A demand signal $\mu$ with distribution function $\Theta$ is observed, the retailer buys $r$, and market demand is filled from the retailer's stock. In this mission the signal is perfect ($\sigma_\varepsilon = 0$): market demand equals $\mu$, so its distribution $F$ equals $\Theta$.

Given $\mu$, the retailer's profit from buying $r$ is

$$G(r\mid\mu) = p\min[\mu,r] - c\,r - s[\mu-r]^+ + u[r-\mu]^+,$$

and it buys $r^*_{QF} = \mu\perp[q(1-\omega),Q]$, the point of the interval closest to $\mu$. The EM's expected profit (2) is $\pi_{EM,QF}(Q;q) = (c-u)E_\mu\{r^*_{QF}\} - (m-u)Q$. The retailer's forecast problem maximizes $\pi_{R,QF}(q) = E_\mu\{G(r^*_{QF}\mid\mu)\}$ with the EM building $q(1+\alpha)$. A central planner earns $\Pi_{CC}(Q) = E_\mu\{p\min[\mu,Q]-s[\mu-Q]^+ + u[Q-\mu]^+\} - mQ$, maximized at

$$Q^*_{CC} = F^{-1}\!\left(\frac{p+s-m}{p+s-u}\right).$$

The total flexibility of the contract is $\psi = (1+\alpha)/(1-\omega)$.

Formalization targets

Goal: Proposition 6(a)

With $\sigma_\varepsilon = 0$, the QF contract with flexibility $\psi$ and transfer price

$$\bar c(\psi) = u + \frac{m-u}{\dfrac1\psi F\!\left(\dfrac1\psi F^{-1}\!\left(\dfrac{p+s-m}{p+s-u}\right)\right) + \dfrac{m-u}{p+s-u}} \tag{4}$$

is system-efficient: the retailer's unique optimal forecast is $\hat q = Q^*_{CC}/(1+\alpha)$, the EM's unique optimal production given $\hat q$ is $\hat q(1+\alpha) = Q^*_{CC}$, and the resulting expected system profit equals $\max_Q \Pi_{CC}(Q)$.

Milestones

1. §4: $Q^*_{CC}$ exists and is the unique maximizer of $\Pi_{CC}$.
2. §6.1: given $\mu$, the retailer's unique optimal purchase in $[a,b]$ is $\mu\perp[a,b]$.
3. Proposition 3(a): for $\omega<1$, the optimal forecast $q^*_{QF}$ is strictly positive, finite, and the unique solution of the first-order condition (3).
4. §7: for any forecast $q\ge0$, expected system profit equals $\Pi_{CC}(q(1+\alpha))$; hence it is maximal when the production level $q(1+\alpha)$ matches $Q^*_{CC}$.

Significance

The result shows that one contract form, by choosing the transfer price as a function of the flexibility, yields a whole menu of contracts each of which coordinates the supply chain, so that the two firms can trade price against flexibility without losing system profit. Its corollaries in the paper, that any split of expected profit is achievable by some efficient contract and that more flexibility shifts profit to the manufacturer, rest on (4).

The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development supplies them, makes explicit the regularity the argument needs (finite variance, a continuous and strictly increasing $\Theta$, a positive efficient quantity), and gives reusable statements about newsvendor objectives with a clipped purchase. To our knowledge none of these results has been formalized before; the platform's quantity-flexibility theorems in other models (no manufacturer production stage, $\alpha = 0$, retailer side only) do not cover them.

Difficulty

Each firm optimizes its own objective, and the efficient price must work for both at once. Making the retailer's first-order condition hold at $\hat q$ pins down $c$, so nothing is left to adjust for the EM, whose incentive to build more than the contracted $q(1+\alpha)$ has to be ruled out separately at that same price. The retailer's objective is an expectation of a non-smooth function of a clipped purchase, so its derivative must be computed through the distribution of $\mu$ on two moving thresholds $q(1+\alpha)$ and $q(1-\omega)$, and strict concavity must come from the strict increase of $\Theta$ rather than from a density.

Formalization scope

All objects live in the namespace TsayQF.EffQF. The law of $\mu$ is a probability measure $\nu$ on $\mathbb R$ with $\mu\in L^2(\nu)$, whose distribution function cdf ν is differentiable and strictly increasing on $\mathbb R$ (the paper's "differentiable and invertible"). Expectations are Bochner integrals; finite variance makes every integrand integrable. Inverse distribution functions are not used: $Q^*_{CC}$ enters as a real number with the hypothesis $F(Q^*_{CC}) = \kappa_S$, which determines it uniquely, and (4) is defined in its printed shape. Optimality is IsMaxOn over the decision's natural set: forecasts in $[0,\infty)$, the EM's production in $[q(1+\alpha),\infty)$, purchases in $[q(1-\omega),Q]$, central production in $\mathbb R$.

Hypotheses made explicit: $Q^*_{CC} > 0$ in the goal and a positive marginal value of the forecast at $q=0$ in Proposition 3(a), both standing for the paper's presumption that demand is almost certainly nonnegative; $\omega<1$ (Proposition 3's case). The transfer price is only required to satisfy $u<c<p+s$ rather than $m<c<p$, because $\bar c(\psi)$ can exceed $p$ when $s>0$. The milestones are the $\sigma_\varepsilon = 0$ instances of the paper's general statements.

Two modelling choices are fixed. The retailer's forecast objective takes the EM's production to be $q(1+\alpha)$, as §6.1 does after Proposition 2; the full game in which the retailer anticipates other EM responses is not modelled, and the goal instead verifies that the EM's unique best response at $\bar c(\psi)$ is exactly $q(1+\alpha)$. The efficient price is the explicit formula (4), not "a price that makes $Q^*_{CC}$ optimal", which would make the goal a tautology; likewise system efficiency is stated as an inequality against $\Pi_{CC}$ at every production level, not by definition.

Needed infrastructure: derivatives of expectations of piecewise-linear functions of a clipped variable, and the newsvendor fractile characterization. Both are reusable for other contract models. Proofs of any milestone, and of the goal from the milestones, are welcome.

Selected references

• A. A. Tsay, The Quantity Flexibility Contract and Supplier-Customer Incentives, Management Science 45(10):1339–1358, 1999. https://doi.org/10.1287/mnsc.45.10.1339
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in OR & MS vol. 11, 2003, §6.2.5. https://doi.org/10.1016/S0927-0507(03)11006-7
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, Wiley, 2nd ed. 2019, Ch. 14. https://doi.org/10.1002/9781119584445

Motivation

A manufacturer must commit to production before a retailer knows how much it will buy. In practice the retailer sends a forecast first, and the manufacturer plans against it. When the forecast binds neither party, the retailer has no reason to report it honestly, and the manufacturer has no reason to plan for the market rather than for its own margin. Purchasing managers have described this to Tsay directly, and Lee, Padmanabhan and Whang (1997) document such "phantom ordering" in several case studies.

A. A. Tsay, The Quantity Flexibility Contract and Supplier-Customer Incentives (Management Science, 1999), models the situation as a two-stage newsvendor game with a demand-information update between production and purchase. Its first result, Proposition 1, is the benchmark the rest of the paper builds on. Even when both parties share the same beliefs about demand, a linear transfer price alone leaves the manufacturer underproducing relative to a central planner, and the supply chain loses expected profit, for every transfer price. That inefficiency motivates the quantity flexibility (QF) contract studied in the remainder of the paper and in the companion mission of this series.

Setting

Costs. The retail price is $p$ and the unit transfer price paid by the retailer to the manufacturer (the EM) is $c$. The unit production cost is $m$, the unit salvage value is $u$ (the same for either party), and the unit goodwill loss on unmet demand is $s$. The paper's standing assumptions (§3.1, p. 1344) are

$$p > c > m > 0,\qquad u < m,\qquad s \ge 0 .$$

Three critical fractiles recur:

$$\kappa_R = \frac{p+s-c}{p+s-u},\qquad \kappa_{EM} = \frac{c-m}{c-u},\qquad \kappa_S = \frac{p+s-m}{p+s-u}.$$

Demand (§3.3). Market demand is $X = \mu + \varepsilon$. The signal $\mu$ has distribution function $\Theta$, which is differentiable and strictly increasing, and finite variance. The error $\varepsilon \sim N(0,\sigma_\varepsilon^2)$ is independent of $\mu$. $F$ is the distribution function of $X$, $\Phi$ is the standard normal distribution function, and $z_\varepsilon = \Phi^{-1}(\kappa_R)$.

Timing (§3.2). The EM produces $Q$ knowing only the prior. Then $\mu$ is observed and the retailer buys $r \le Q$. Then $X$ is realized, and both parties salvage their surplus. Given $\mu$, the retailer's expected profit from purchase $r$ is

$$G(r\mid\mu) = E_{X\mid\mu}\{p\min[X,r] - c\,r - s[X-r]^+ + u[r-X]^+\}. \tag{1}$$

Without commitment the retailer buys $r^*_{NC}(Q,\mu) = \min[\mu + z_\varepsilon\sigma_\varepsilon, Q]$. The EM's expected profit is

$$\pi_{EM,NC}(Q) = (c-u)\,E_\mu\, r^*_{NC}(Q,\mu) - (m-u)\,Q,$$

and the retailer's is $\pi_{R,NC}(Q) = E_\mu\, G(r^*_{NC}(Q,\mu)\mid\mu)$. A central planner producing $Q$ before the signal earns

$$\Pi_{CC}(Q) = E_X\{p\min[X,Q] - s[X-Q]^+ + u[Q-X]^+\} - mQ .$$

Formalization targets

Goal: Proposition 1 (p. 1347)

Let $Q^*_{NC}$ maximize $\pi_{EM,NC}$ and $Q^*_{CC}$ maximize $\Pi_{CC}$. Then, for every transfer price $c$ admitted by the standing assumptions,

$$Q^*_{NC} < Q^*_{CC}\qquad\text{and}\qquad \pi_{R,NC}(Q^*_{NC}) + \pi_{EM,NC}(Q^*_{NC}) < \Pi_{CC}(Q^*_{CC}).$$

Milestones

1. §4, p. 1345. The centralized optimum exists and is unique:

$$Q^*_{CC} = F^{-1}\!\left(\frac{p+s-m}{p+s-u}\right).$$

2. §5.1, (1), p. 1346. The closed form

$$G(r\mid\mu) = (p+s-c)r - s\mu - (p+s-u)E_{X\mid\mu}[r-X]^+ ,$$

and the retailer's optimal purchase under $r \le Q$ is $\min[\mu + z_\varepsilon\sigma_\varepsilon, Q]$. 3. §5.2, p. 1347. The EM's optimal production exists and is unique:

$$Q^*_{NC} = \Theta^{-1}\!\left(\frac{c-m}{c-u}\right) + z_\varepsilon\sigma_\varepsilon .$$

Significance

Proposition 1 shows that sharing demand information does not remove inefficiency. Under common beliefs and with no commitment, no linear transfer price makes the decentralized chain efficient. Adjusting $c$ moves profit between the parties but cannot recover the planner's expected profit. This is the reason the paper studies richer contracts, and the efficiency result for the QF contract (the paper's Proposition 6) is measured against the benchmark $Q^*_{CC}$ defined here.

The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development therefore supplies arguments the published record does not contain. It also exhibits the exact hypotheses the result needs. In particular it covers the degenerate case $\sigma_\varepsilon = 0$, where the signal is perfect. No part of this mission has a prior formal proof. Newsvendor critical-fractile results exist on Prove2Me for single-decision models, but without the production stage and information update used here.

Difficulty

The EM and the planner solve newsvendor problems against different demand laws. The EM faces the retailer's purchase $\mu + z_\varepsilon\sigma_\varepsilon$, while the planner faces $X = \mu + \varepsilon$. Their fractiles are $\kappa_{EM}$ and $\kappa_S$. The obvious comparison, $\kappa_{EM} < \kappa_S$, settles the case $\sigma_\varepsilon = 0$ only. For $\sigma_\varepsilon > 0$ the two quantities are inverse distribution functions of different random variables. $z_\varepsilon$ may be negative, and the planner's distribution is a convolution. A comparison of fractiles alone therefore does not order $Q^*_{NC}$ and $Q^*_{CC}$. The strict profit gap also needs more than optimality of $Q^*_{CC}$: it requires comparing the decentralized system profit at $Q^*_{NC}$ with the planner's profit at the same production, and then using uniqueness of the planner's optimum.

The analytic infrastructure is also substantial. It includes differentiating expectations of piecewise-linear functions under a Gaussian law and under a general prior, continuity and strict monotonicity of a convolution's distribution function, and existence of a root of $F(Q) = \kappa_S$.

Formalization scope

All objects live in the namespace TsayQF.NoCommit, in one definitions file Model.

• Costs are a structure Data with fields $p, c, m, u, s \in \mathbb R$ and the standing assumptions (i)–(iii) as fields. "For any $c$" is quantification over all Data. No sign is imposed on $u$.
• The prior is a probability measure ν on ℝ; $\Theta$ is cdf ν. "Differentiable and invertible" is Differentiable ℝ (cdf ν) together with StrictMono (cdf ν), and "mean and variance" is MemLp id 2 ν.
• The error variance is v : ℝ≥0, so $\sigma_\varepsilon = \sqrt v$ and v = 0 is allowed. The law of $X$ is the pushforward of ν.prod (gaussianReal 0 v) under addition, and given $\mu$ demand has law gaussianReal μ v.
• Inverse distribution functions are not Lean functions here. $z_\varepsilon$ is a real z with hypothesis cdf (gaussianReal 0 1) z = kR D. The milestones state existence of a solution of each fractile equation and characterize the maximizers by it.
• Expectations are Bochner integrals. Finite variance of $\mu$ makes every integrand integrable, so no expectation silently defaults to zero.
• Optimality is IsMaxOn over Set.univ for productions and over Set.Iic Q for the purchase. Productions range over $\mathbb R$; the paper's presumption that $\mu$ and $X$ are almost certainly nonnegative is not imposed, because no result here needs it.
• The goal quantifies over arbitrary maximizers. Milestones 1 and 3 show that maximizers exist, so the goal is not vacuous. A sorry-free sanity file checks the paper's §8 data $(p,c,m,u,s) = (15,10,6,3,0)$ and shows that a normal prior satisfies the hypotheses on $\Theta$.

The goal must not be weakened to non-strict inequalities, and the EM's demand must remain the retailer's purchase $\min[\mu + z_\varepsilon\sigma_\varepsilon, Q]$, not market demand. Either change trivializes the result or changes it. Reusable pieces are the newsvendor critical-fractile characterization for a general continuous strictly increasing distribution, and monotonicity and continuity of the distribution function of a sum of independent variables with one Gaussian summand. Proofs of the milestones as standalone lemmas are welcome.

Selected references

• A. A. Tsay, The Quantity Flexibility Contract and Supplier-Customer Incentives, Management Science 45(10):1339–1358, 1999. https://doi.org/10.1287/mnsc.45.10.1339
• H. L. Lee, V. Padmanabhan, S. Whang, The Bullwhip Effect in Supply Chains, Sloan Management Review 38(3):93–102, 1997. https://sloanreview.mit.edu/article/the-bullwhip-effect-in-supply-chains/
• A. V. Iyer, M. E. Bergen, Quick Response in Manufacturer-Retailer Channels, Management Science 43(4):559–570, 1997. https://doi.org/10.1287/mnsc.43.4.559
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science 11, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7

Motivation

Minimizing the sum of the $k$ largest eigenvalues of a symmetric matrix that depends affinely on parameters is a basic problem of eigenvalue optimization (survey: A. S. Lewis and M. L. Overton, Eigenvalue optimization, Acta Numerica 5, 1996, doi:10.1017/S0962492900002646). Its objective is convex, and $f_k$ is differentiable at $B$ exactly when $\lambda_k(B)>\lambda_{k+1}(B)$; at optimal solutions the eigenvalues tend to coalesce, which makes the problem a model problem of nonsmooth optimization. G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues (Math. Oper. Res. 23(2), 1998, doi:10.1287/moor.23.2.339), gives a quantitative explanation in terms of the number of free parameters.

The paper also proves a bound on the rank of extreme points of semidefinite programs, now often called the Pataki bound (also obtained by Barvinok, 1995): an extreme point $X$ of $\{X\succeq0: A_i\bullet X=b_i,\ i\le m\}$ satisfies $\operatorname{rank}X(\operatorname{rank}X+1)/2\le m$. This bound is used throughout low-rank semidefinite optimization, for instance in the Burer–Monteiro approach.

Setting

$\mathcal S^n$ is the space of real symmetric $n\times n$ matrices, $X\succeq0$ means $X$ is symmetric positive semidefinite, and $A\bullet B=\sum_{i,j}a_{ij}b_{ij}$. For $B\in\mathcal S^n$, $\lambda_1(B)\ge\dots\ge\lambda_n(B)$ are its eigenvalues and, for $k\in\{1,\dots,n\}$,

$$f_k(B)=\lambda_1(B)+\dots+\lambda_k(B).$$

The multiplicity $\operatorname{mult}(\lambda_i(B))$ is the largest $p\ge1$ with $\lambda_j(B)=\dots=\lambda_{j+p-1}(B)$ for some $j\le i\le j+p-1$.

A face of a convex set $S$ is a convex $F\subseteq S$ such that $x\in F$, $y,z\in S$, $x=\tfrac12(y+z)$ imply $y,z\in F$; an extreme point is a one-point face; $\dim S$ is the maximal number of affinely independent points of $S$, minus one. Write $t(i)=i(i+1)/2$ and

$$\tau(l,r,s)=\max\{\,i+j:\ t(i)+t(j)\le l,\ i\le r,\ j\le s\,\}.$$

Let $A_0,A_1,\dots,A_m\in\mathcal S^n$ be linearly independent, $A(x)=A_0+\sum_{i=1}^mx_iA_i$, and assume $m\ge1$ and $k<n$ (the standing assumptions of §4). The affine eigenvalue problem is

$$(EV_k)\qquad\min\{f_k(A(x)):\ x\in\mathbb R^m\},$$

and $\Theta$ denotes its set of optimal solutions, a closed convex set. For $B\in\mathcal S^n$ the semidefinite program

$$\min\ kz+I\bullet V\quad\text{s.t.}\quad V,W\succeq0,\quad zI+V-W=B \tag{3.14}$$

has optimal value $f_k(B)$; $\Omega_k(B)$ is its set of optimal solutions $(z,V,W)$.

Formalization targets

Goal: Theorem 4.3

If $x^*$ is an extreme point of $\Theta$ and $m>k(n-k)$, then

$$\lambda_k(A(x^*))=\lambda_{k+1}(A(x^*))\qquad\text{and}\qquad \operatorname{mult}(\lambda_k(A(x^*)))\ \ge\ n-\tau\big(t(n)-m-1,\,k-1,\,n-k-1\big).$$

Milestones

1. Theorem 2.1: on a face $F$ of the primal feasible set, $t(\operatorname{rank}X)\le m+\dim F$; on a face $G$ of the dual feasible set, $t(\operatorname{rank}Z)\le t(n)-m+\dim G$.
2. Theorem 2.2: the multi-block version $\sum_jt(\operatorname{rank}X_j)\le m-q+\dim G$ for programs with $p$ semidefinite blocks and $q$ free variables.
3. Lemmas 3.1, 3.2 and Theorem 3.3: the optimal value of (3.14) and an explicit description of $\Omega_k(B)$ through an eigendecomposition $B=Q\operatorname{Diag}(\lambda)Q^T$.
4. The rank identity of §3: $\operatorname{rank}V+\operatorname{rank}W+\operatorname{mult}(\lambda_k(B))=n$ on $\Omega_k(B)$ when $\lambda_k(B)=\lambda_{k+1}(B)$.
5. Lemma 4.2 and (4.31): $\{x^*\}\times\Omega_k(A(x^*))$ is a face of the feasible set of the lifted SDP (4.26), of dimension $1$ or $0$ according as $\lambda_k>\lambda_{k+1}$ or $\lambda_k=\lambda_{k+1}$.
6. Lemma 4.1: $\Theta$ contains no line, so it has extreme points whenever it is nonempty.

Significance

The theorem says that once the number of free parameters $m$ exceeds $k(n-k)$, the $k$-th and $(k+1)$-st eigenvalues necessarily coincide at extreme optimal solutions, so $f_k\circ A$ is typically nonsmooth at its minimizers, and it bounds from below the dimension of the subdifferential $\partial f_k(A(x^*))$, which is $t(\operatorname{mult}(\lambda_k))$. The intermediate rank bounds of §2 are reusable on their own for any semidefinite program.

The results are proved in the paper. As far as is known, none of them (neither the Pataki rank bound, nor the semidefinite characterization of $f_k$, nor Theorem 4.3) has a machine-checked proof. Formalizing them produces a library of faces and dimensions of spectrahedra, the SDP representation of the Ky Fan sum $f_k$, and the multiplicity bound itself.

Difficulty

Extremality of $x^*$ in $\Theta$ is a statement in the parameter space $\mathbb R^m$ and gives no direct information on the spectrum of $A(x^*)$: perturbation arguments on the eigenvalues alone break down precisely at the coalesced eigenvalues the theorem is about, where $f_k$ is not differentiable. The quantitative bound (4.30) also needs more than the optimal value $f_k(A(x^*))$: it depends on the whole optimal set $\Omega_k(A(x^*))$, on the dimension of faces of spectrahedra, and on an exact count relating the ranks of the optimal $V,W$ to the multiplicity of $\lambda_k$. None of these (faces and dimension of spectrahedra, the semidefinite representation of $f_k$, eigenvalue run lengths) is in Mathlib.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; $A\bullet B$ is the published BurerMonteiro.RankIncrease.frob, the primal and dual feasible sets are the published IsPrimalFeasible/IsDualFeasible, and $\lambda_i(B)$ is the published ProjLikeRetr.Spectral.eig B ⟨i-1,_⟩ (Mathlib's nonincreasing eigenvalues, 0-based). Every matrix whose eigenvalues are taken is assumed symmetric. Faces, extreme points and dimension are defined as on p. 341; dimension is integer valued with $\dim\emptyset=-1$. All rank bounds are compared in $\mathbb Z$. $\Theta$ is the argmin set $\{x: f_k(A(x))\le f_k(A(y))\ \forall y\}$ and $\Omega_k(B)$ is the set of feasible points no worse than every feasible point; no infimum is used. Optimal values are stated as least elements of the set of feasible objective values.

Hypotheses added relative to the page, each disclosed in its item: $1\le k<n$ in the statements of §3, which mention $\lambda_{k+1}$; $k\ge1$ (p. 340) in every §4 statement; one common matrix order in Theorem 2.2; and $\lambda_k(B)=\lambda_{k+1}(B)$ in the rank identity of p. 348, which is false as printed when $\lambda_k(B)>\lambda_{k+1}(B)$ ($n=2$, $k=1$, $B=\operatorname{diag}(2,0)$ gives $3\ne2$) and is used in the paper only in the equal case. The linear independence of $A_0,\dots,A_m$ is kept with $A_0$ included, as on p. 348.

Trivializing formalizations are ruled out: $\Theta$ is not defined through a possibly junk infimum, a face must be convex and contained in the set, the dimension is not a junk $0$, $\operatorname{mult}$ is the run length of equal eigenvalues and not a constant or an index, and the eigenvalues are only ever taken of symmetric matrices.

A complete development needs: the rank–dimension bound for faces of spectrahedra (reusable for any SDP), the semidefinite characterization of $f_k$ with its optimal set, and convexity facts on $\Theta$. Proofs of any milestone, alternative proofs of the rank bounds, and the general smooth case of §5 are welcome.

Selected references

• G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23(2), 339–358, 1998. https://doi.org/10.1287/moor.23.2.339
• A. I. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13, 189–202, 1995. https://doi.org/10.1007/BF02574037
• M. L. Overton and R. S. Womersley, Optimality conditions and duality theory for minimizing sums of the largest eigenvalues of symmetric matrices, Mathematical Programming 62, 321–357, 1993. https://doi.org/10.1007/BF01585173
• F. Alizadeh, Interior point methods in semidefinite programming with applications to combinatorial optimization, SIAM Journal on Optimization 5(1), 13–51, 1995. https://doi.org/10.1137/0805002
• A. S. Lewis and M. L. Overton, Eigenvalue optimization, Acta Numerica 5, 149–190, 1996. https://doi.org/10.1017/S0962492900002646
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.