Operations Research

Motivation

Randomized coordinate descent updates one block of variables per iteration, chosen at random. For problems whose dimension makes even one full gradient expensive (the "huge-scale" problems of the title, such as sparse least squares or truss topology design), a coordinate step can cost a tiny fraction of a gradient step. Nesterov's paper (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362) gave the first global complexity bounds for such methods with non-uniform sampling, and it is the reference point for the later literature on randomized block methods (Richtárik and Takáč 2014, Lu and Xiao 2015, Allen-Zhu et al. 2016).

The first results of the paper (Theorem 1, the subject of a companion mission) bound the expected objective value after k iterations. An expected bound does not say what happens in a single run. This mission formalizes the paper's answer to that question in §3: by running the method on a slightly regularized objective, one run returns an ε-solution with any prescribed probability β, after a number of iterations that grows only logarithmically in 1/(1 − β).

Setting

The variable space is a product $\mathbb R^N=\mathbb R^{n_1}\times\cdots\times\mathbb R^{n_n}$ of $n\ge1$ blocks; a point $x$ has blocks $x^{(i)}$, and $U_ih$ is the point whose $i$-th block is $h$ and whose other blocks vanish. In this mission each block carries a Euclidean norm $\|h^{(i)}\|_{(i)}^2=\langle B_ih^{(i)},h^{(i)}\rangle$ with $B_i\succ0$ (3.4), and the whole space carries

$$\|h\|_0^2=\sum_{i=1}^n\|h^{(i)}\|_{(i)}^2,\qquad \|g\|_0^*=\Big[\sum_{i=1}^n\big(\|g^{(i)}\|_{(i)}^*\big)^2\Big]^{1/2}.$$

The objective $f:\mathbb R^N\to\mathbb R$ is convex and differentiable, has a minimizer $x_*$ with value $f^*$, and its partial gradients $f'_i(x)=U_i^T\nabla f(x)$ are Lipschitz along their own block with constants $L_i>0$ (2.2): $\|f'_i(x+U_ih)-f'_i(x)\|^*_{(i)}\le L_i\|h\|_{(i)}$. Write $S_\alpha=\sum_iL_i^\alpha$.

The method RCDM$(\alpha,x_0)$ (2.6) draws, independently at each step, block $i$ with probability $L_i^\alpha/S_\alpha$ and replaces $x$ by $T_i(x)=x-\frac1{L_i}U_if'_i(x)^\#$, where $s^\#$ is a maximizer of $\langle s,x\rangle-\frac12\|x\|^2$ (1.8). The quantity $\phi_k$ is the expectation of $f(x_k)$ over the first $k$ draws.

The level-set radius is $R_0(x_0)=\max_x\{\max_{x_*}\|x-x_*\|_0: f(x)\le f(x_0)\}$, and for $\mu>0$ the regularized objective is

$$f_\mu(x)=f(x)+\frac\mu2\|x-x_0\|_0^2 .$$

It has block constants $L_i+\mu$, so RCDM$(1,x_0)$ applied to $f_\mu$ samples block $i$ with probability $(L_i+\mu)/(S_1+n\mu)$ and steps with $1/(L_i+\mu)$.

Formalization targets

Goal: Theorem 4 (p. 11)

For $\epsilon>0$, $\beta\in(0,1)$, $\mu=\epsilon/(4R_0^2(x_0))$ and

$$k\ \ge\ 2\Big[n+\frac{4S_1R_0^2(x_0)}{\epsilon}\Big]\Big(\ln\frac1{1-\beta}+\ln\Big(\frac12+\frac{2S_1R_0^2(x_0)}{\epsilon}\Big)\Big),$$

the point $x_k$ produced by RCDM$(1,x_0)$ on $f_\mu$ satisfies

$$\mathrm{Prob}\big(f(x_k)-f^*\le\epsilon\big)\ge\beta .$$

Milestones

1. Theorem 2 (p. 9), for arbitrary block norms: if $f$ is $\sigma$-strongly convex in $\|\cdot\|_{1-\alpha}$, then $\phi_k-f^*\le(1-\sigma/S_\alpha)^k(f(x_0)-f^*)$.
2. The constants of $f_\mu$ (p. 11): $f_\mu$ is $\mu$-strongly convex in $\|\cdot\|_0$, has block constants $L_i+\mu$, so that $S_1(f_\mu)=S_1(f)+n\mu$, and its gradient is $(S_1(f)+\mu)$-Lipschitz in $\|\cdot\|_0$.
3. Lemma 4 (p. 11): $\mathbb E\,\|\nabla f_\mu(x_k)\|_0^*\le\big[2(S_1+\mu)(f(x_0)-f^*)(1-\mu/(S_1+n\mu))^k\big]^{1/2}$.

Significance

Theorem 4 turns an in-expectation guarantee into a single-run guarantee with an explicit, non-asymptotic iteration count. Its dependence on the confidence level is logarithmic, so very high confidence costs little; and the count $O\big((n+S_1R_0^2/\epsilon)\log(1/\epsilon)\big)$ replaces the largest eigenvalue of the Hessian, which governs the full gradient method, by the trace-type quantity $S_1$, which for sparse problems makes groups of $n$ coordinate steps competitive with one gradient step. Theorem 2 is the linear-rate result for strongly convex objectives that later analyses of randomized block methods take as their starting point.

The results are proved in the paper. None of them is formalized in the block setting. The scalar Euclidean case $n_i=1$ of Theorem 2 is proved on Prove2Me as ConvexOptAlg.CoordDescent.theorem_6_8 (Bubeck, Theorem 6.8), and the bound (3.2), $f(x)-f^*\le\frac1{2\sigma}(\|\nabla f(x)\|^*)^2$ for a $\sigma$-strongly convex $f$ in any norm, is proved as ConvexOptAlg.CoordDescent.lemma_6_9. This mission adds block variables with general norms (Theorem 2), the regularization constants, the gradient-norm bound, and the high-probability statement itself, which has no formalized counterpart.

Difficulty

The obvious argument fails. Theorem 2 controls the expected suboptimality of $f_\mu$, not of $f$, and Markov's inequality applied to $f_\mu(x_k)-f_\mu^*$ does not reach accuracy ε: $f_\mu^*$ and $f^*$ differ by an amount comparable to ε, and the contraction factor itself depends on μ. Relating the run on $f_\mu$ to the original problem requires the global Lipschitz constant of $\nabla f_\mu$ in $\|\cdot\|_0$, which for $f$ is the weighted co-coercivity statement of Lemma 2 of the paper and is not a consequence of (2.2) alone without convexity. The constants of (3.11) are exact, including the factor 2 and the ½, so no estimate may lose a constant. Finally, the iterates depend on all previous draws, so even the finite-sum expectations need a careful account of linearity and of conditioning on the last draw.

Formalization scope

• $\mathbb R^N$ is the dependent product Blocks E of finite-dimensional real spaces E i indexed by Fin n (0-based for the paper's 1, …, n). Euclidean blocks (3.4) are inner-product spaces, with $B_i$ absorbed into the inner product; Theorem 2 is stated for arbitrary normed blocks. The dual norm of a block is the operator norm of a functional.
• The draws are explicit sequences Fin k → Fin n; expectations and probabilities are finite sums weighted by $\prod_sp(i_s)$. No measure theory is involved.
• The vectors $s^\#$ are an arbitrary selection satisfying (1.8); the theorems hold for every selection.
• $R_0(x_0)$ is replaced by any positive upper bound $R$ (every point of the level set within $R$ of every minimizer), and $\mu=\epsilon/(4R^2)$ is defined from it. The paper's theorem is the case $R=R_0(x_0)$; $R>0$ excludes the case $R_0(x_0)=0$, in which the paper's μ is undefined.
• Explicit hypotheses the paper leaves implicit: $n\ge1$, $L_i>0$, $f$ convex and differentiable, existence of a minimizer, and $\epsilon>0$, $\beta\in(0,1)$ (fixed on p. 10).
• The paper prints Theorem 2's left side as $\phi_k-\phi^*$; the statement uses $\phi_k-f^*$, which is what its proof establishes.
• The run in Theorem 4 and Lemma 4 is on $f_\mu$ with $f_\mu$'s constants $L_i+\mu$ (step and sampling); the event of Theorem 4 is about $f$ and $f^*$ of the original problem. Running RCDM with $f$'s constants $L_i$, or stating the event for $f_\mu$, would be a different theorem.
• Lemma 3 and Theorem 3 (the variant in the norm $\|\cdot\|_1$) are not posed: applied to $f_\mu$ with constants $(1+\mu)L_i$, Theorem 2 gives a contraction factor weaker than the printed $1-\mu/n$, and the paper's argument does not establish them as printed.

Contributions are welcome on the probabilistic bookkeeping for expect (normalization, linearity, conditioning on the last draw, Jensen for a concave function), which is reusable by every mission of this series; on Lemma 2 of the paper in the block setting; and on the milestones in the stated order.

Selected references

• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, CORE Discussion Paper 2010/2, Université catholique de Louvain, 2010. https://core.ac.uk/download/6430808.pdf
• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2), 341–362, 2012. https://doi.org/10.1137/100802001
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 231–357, 2015, §6.4. https://arxiv.org/abs/1405.4980
• P. Richtárik and M. Takáč, Iteration complexity of randomized block-coordinate descent methods for minimizing a composite function, Mathematical Programming 144, 1–38, 2014. https://doi.org/10.1007/s10107-012-0614-z
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

A retailer that orders stock months before the selling season carries inventory risk: its profit depends on a demand it cannot observe when it commits. For many goods that demand moves with a quantity traded on financial markets: sales of housing-related products with an interest-rate or construction index, sales of fashion or luxury goods with a stock index, sales of commodity-intensive products with a commodity price. V. Gaur and S. Seshadri, Hedging Inventory Risk Through Market Instruments (MSOM 7(2), 2005), ask what such a firm gains by trading in that market, and how the trade interacts with the ordering decision.

Their analysis has two halves. When demand is perfectly correlated with the asset price, the newsvendor payoff can be replicated by a portfolio of the asset and call options, and inventory risk can be removed completely (§2). When demand is only partially correlated, the hedge is imperfect, and the question becomes whether a decision maker with a concave utility still benefits from hedging, and whether hedging changes the order quantity (§3.2). This mission formalizes the first of these two questions in the partially correlated model: Proposition 5, which says that a small fair hedge never lowers expected utility at the margin. A companion mission of the same series treats Proposition 7, on the order quantity.

Setting

A firm orders $I$ units now at unit cost $c$, sells at price $p$ at a future time $T$, and salvages leftovers at $s$. The demand is

$$D = a + bS_T + \varepsilon',$$

where $S_T$ is the time-$T$ price of a traded asset and $\varepsilon'$ is a forecast error, independent of $S_T$, with $\mathbb E[\varepsilon'] = 0$ and $\mathbb E[\varepsilon'^2] < \infty$ (§3, p. 107). Write $\varepsilon = \varepsilon'/b$. The paper's standing assumptions (§2, p. 106) are $b > 0$, $I > \max\{a, 0\}$, and $p > ce^{rT} > s$, where $r$ is the risk-free rate.

After scaling all cash flows by $1/((p-s)b)$ (p. 110) the firm's terminal wealth without hedging is

$$W + \Pi_U(I) = W + \min\{S_T + \varepsilon,\ (I-a)/b\} - c_1 I,$$

with $c_1 = (ce^{rT}-s)/((p-s)b)$ and $W$ the scaled initial wealth plus $(p-s)a$. In these units $p > ce^{rT} > s$ reads $0 < c_1$ and $c_1 b < 1$.

A hedge is a portfolio with time-$T$ payoff $X_T$ and time-0 price $X_0$. The paper requires it to be a fair gamble, $\mathbb E[X_T - X_0e^{rT}] = 0$ (12), and $X_T$ to be an increasing function of $S_T$ (p. 111). If the firm shorts $\alpha$ units of the hedge, its wealth is

$$W + \Pi_H(I,\alpha) = W + \min\{S_T + \varepsilon, (I-a)/b\} - c_1 I - \alpha X_T + \alpha X_0 e^{rT}, \tag{14}$$

and a decision maker with utility $u:\mathbb R \to \mathbb R$ evaluates it by $\mathbb E[u(\Pi_H(I,\alpha))]$.

In Lean, the law of $S_T$ is a probability measure ν on ℝ, the law of $\varepsilon$ is a probability measure G on ℝ, the hedge is X_T = φ S_T for a function φ : ℝ → ℝ, the forward price $X_0e^{rT}$ is one real x0r, and every expectation is an integral against the product measure ν.prod G. The definitions file provides unhedgedPayoff, hedgedPayoff and expUtil.

Formalization targets

Goal: Proposition 5 (p. 111)

For any concave and differentiable utility function $u$, and any fixed order quantity $I$,

$$\frac{d}{d\alpha}\,\mathbb E[u(\Pi_H(I,\alpha))]\Big|_{\alpha = 0} \ \ge\ 0. \tag{15}$$

The Lean statement asserts that the two-sided derivative exists at $\alpha = 0$ and is nonnegative.

Milestones (proof of Proposition 5, p. 118)

1. Derivative at $\alpha = 0$. The derivative exists and equals

$$\mathbb E\big[u'(W + \min\{S_T + \varepsilon, (I-a)/b\} - c_1I)\,\{-X_T + X_0e^{rT}\}\big].$$

2. Covariance inequality. Since both factors decrease in $S_T$,

$$\mathbb E\big[u'(W+\Pi_U)\{-X_T + X_0e^{rT}\}\big] \ \ge\ \mathbb E[u'(W+\Pi_U)]\cdot\mathbb E[-X_T + X_0e^{rT}] = 0.$$

Significance

Proposition 5 is the paper's answer to "should a risk-averse newsvendor hedge at all?": with any concave utility and any order quantity, a small short position in a fair hedge that rises with the asset price weakly increases expected utility. It needs no assumption on the shape of the utility beyond concavity, no sign of $u'$, and no assumption on the law of the forecast error beyond independence. It is the starting point for the paper's later results on the optimal hedge (Proposition 4) and on how hedging raises the optimal order (Propositions 6 and 7), and it is a clean instance of a general principle in operations-finance: a fair bet that is negatively correlated with marginal utility is worth taking at the margin.

The result is proved in the paper in a few lines. What this mission adds is a machine-checked version with every regularity condition explicit: the paper differentiates under the expectation and multiplies expectations without stating when this is legitimate, and conditions on $S_T$ informally. To the best of a search of the Prove2Me catalog, neither the result nor the two steps of its proof (an integral version of Chebyshev's covariance inequality for monotone functions, and differentiation of a concave expected utility under the integral sign) is formalized there.

Difficulty

The obvious argument has two analytic gaps. First, exchanging $d/d\alpha$ with the expectation needs a dominating function, and the only integrability available is at finitely many values of $\alpha$, for both signs of $\alpha$. Second, "$u'(\cdot)$ is a decreasing function of $S_T$" is false as a statement about the pair $(S_T, \varepsilon)$: $u'(W + \Pi_U)$ depends on $\varepsilon$ too. The covariance step is Chebyshev's inequality for the function $s \mapsto \mathbb E_\varepsilon[u'(W + \min\{s+\varepsilon, (I-a)/b\} - c_1 I)]$ and the function $s \mapsto X_0e^{rT} - X_T(s)$, which needs independence (Fubini on the product measure) and has to cope with the conditional expectation being finite only almost everywhere. Neither $u'$ nor the hedge payoff is bounded.

Formalization scope

The Lean development commits to the following conventions.

• Random inputs are two probability measures ν (law of $S_T$) and G (law of $\varepsilon$) on ℝ; independence is the product measure ν.prod G. The standing assumptions $\mathbb E[\varepsilon] = 0$ and $\mathbb E[\varepsilon^2] < \infty$ are hypotheses (∫ e, e ∂G = 0, MemLp id 2 G).
• The scaled parameters $W, a, b, c_1, I$ are reals with $b > 0$, $\max\{a,0\} < I$, $0 < c_1$, $c_1 b < 1$.
• The hedge is φ : ℝ → ℝ, monotone (nondecreasing, reading the paper's "increasing" weakly), measurable and ν-integrable; the fair-gamble condition (12) is ∫ s, φ s ∂ν = x0r. The paper's further remark that $X_T$ is piecewise continuous and a.e. differentiable is not needed and not imposed.
• The utility is u : ℝ → ℝ with ConcaveOn ℝ Set.univ u and Differentiable ℝ u, exactly "concave and differentiable"; no monotonicity of $u$ is assumed.
• Regularity hypotheses, disclosed: for some $\delta > 0$ the utility $u(W + \Pi_H(I,\alpha))$ is integrable at $\alpha \in \{-\delta, 0, \delta\}$, and $u'(W + \Pi_U)$ is integrable. The paper uses these silently.

A statement of the form 0 ≤ deriv (fun α => expUtil …) 0 would be trivially true whenever the derivative fails to exist (Lean's deriv returns 0 there); the goal instead asserts HasDerivAt with a value D and 0 ≤ D. The hypotheses are satisfiable with a non-constant hedge: a sorry-free check uses $u(w) = -e^{-w}$, $S_T$ uniform on $\{0,1\}$, $\varepsilon$ uniform on $\{-1,1\}$ and $X_T = S_T$.

Infrastructure that a complete proof needs, reusable beyond this mission: Chebyshev's integral (covariance) inequality for two monotone functions of a real random variable; differentiation under the integral sign for concave integrands with integrability at three points; Fubini-based conditioning on one coordinate of a product measure. Contributions of these general lemmas as separate theorems are welcome. The source PDF is a scan of the published article.

Selected references

• V. Gaur, S. Seshadri, Hedging Inventory Risk Through Market Instruments, Manufacturing & Service Operations Management 7(2):103–120, 2005. https://doi.org/10.1287/msom.1040.0061
• K. J. Arrow, Essays in the Theory of Risk-Bearing, Markham, 1971 (absolute risk aversion, cited on p. 111 of the paper).
• M. S. Kimball, Precautionary Saving in the Small and in the Large, Econometrica 58(1):53–73, 1990. https://doi.org/10.2307/2938334

Motivation

In a time-inconsistent control problem, a control that is optimal when planned at time $t$ stops being optimal when the problem is re-solved at a later time. Two sources of time inconsistency are common in finance and economics. One is a variance term in the objective, as in continuous-time Markowitz mean–variance portfolio selection (Zhou–Li 2000; Basak–Chabakauri 2010). The other is a state-dependent target, as in Björk–Murgoci–Zhou 2014. Dynamic programming does not apply. A standard response is to look for an equilibrium: a control that no planner at any time $t$ can improve by an infinitesimal deviation on $[t,t+\varepsilon)$.

Hu, Jin and Zhou define open-loop equilibria for a general stochastic linear–quadratic (LQ) problem with both sources of time inconsistency. They give a sufficient condition through a flow of forward–backward SDEs, which is the subject of mission I of this series. This mission covers §4 of the paper: the scalar-state case with deterministic coefficients, where the equilibrium is computed explicitly from a system of coupled Riccati equations. Mission III covers §5, the mean–variance application with random coefficients.

Setting

On a probability space carrying a standard $d$-dimensional Brownian motion $W$ with its filtration $(\mathcal F_t)$, the state $X$ is scalar ($n=1$) and the control $u$ takes values in $\mathbb R^l$:

$$dX_s=[A_sX_s+B_s'u_s+b_s]\,ds+[C_sX_s+D_su_s+\sigma_s]'\,dW_s,\qquad X_0=x_0.$$

The coefficients are deterministic functions on $[0,T]$: $A_s,b_s,Q_s\in\mathbb R$, $B_s\in\mathbb R^l$, $C_s,\sigma_s\in\mathbb R^d$, $D_s\in\mathbb R^{d\times l}$ and $R_s\in\mathbb R^{l\times l}$ symmetric. $A,B,C,D,Q,R$ are bounded, $b,\sigma$ are square integrable, $Q\ge0$, $R\succeq0$, and $G\ge0$. At time $t$, in state $x_t$, the planner evaluates

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

where $\mathbb E_t=\mathbb E[\,\cdot\mid\mathcal F_t]$. The third term (the variance-like term) and the fourth term (which depends on $x_t$) make the problem time-inconsistent. A control $u^*$ with state $X^*$ is an equilibrium (Definition 2.1) if, for every $t\in[0,T)$ and every $\mathcal F_t$-measurable square-integrable $v$, the spike $u^{t,\varepsilon,v}=u^*+v\mathbf 1_{[t,t+\varepsilon)}$ satisfies

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

With $\Gamma^{(1)}_s=\mu_1e^{\int_s^TA_r\,dr}$, $|C|^2=C'C$ and $K=(R+MD'D)^{-1}$, the coupled Riccati system (4.9) for deterministic $(M,N)$ is

$$\begin{aligned}\dot M&=-\big[2A+|C|^2+\Gamma^{(1)}B'K(B+D'C)\big]M-Q+(B+D'C)'K(B+D'C)M^2-B'K(B+D'C)MN,& M_T&=G,\\ \dot N&=-\big[2A+\Gamma^{(1)}B'KB\big]N+B'K(B+D'C)MN-B'KBN^2,& N_T&=h.\end{aligned}$$

Given $(M,N)$, a linear ODE (4.8) determines $\Phi$ with $\Phi_T=-\mu_2$. The candidate equilibrium is the linear feedback (4.4)

$$u^*_s=\alpha_sX^*_s+\beta_s,\quad\alpha_s=-K_s\big[(M_s-N_s-\Gamma^{(1)}_s)B_s+M_sD_s'C_s\big],\quad\beta_s=-K_s(\Phi_sB_s+M_sD_s'\sigma_s).$$

Formalization targets

Goal: Theorem 4.4

Suppose $G\ge h>0$ and one of three cases holds:

• (i) $R\succeq\delta I$, $\frac{QD'D+|C|^2R}{l}+\Gamma^{(1)}\mathcal S(D'CB')\succeq0$ and $B=\lambda D'C$ with $\lambda\ge0$;
• (ii) the first two conditions of (i) and $D'D\succeq\delta I$;
• (iii) $R\equiv0$, $D'D\succeq\delta I$, $Q+\Gamma^{(1)}B'(D'D)^{-1}(B+D'C)\ge0$ and $Q+\Gamma^{(1)}B'(D'D)^{-1}D'C\ge0$.

Then

$$\text{(4.9) has a unique positive solution pair }(M,N)\text{ on }[0,T],$$

and, for every solution $\Phi$ of (4.8), the closed-loop equation of (4.4) has a solution, and the feedback control along every closed-loop state is an equilibrium.

Milestones

• Proposition 4.1: a positive solution $(M,J)$ of the transformed system (4.10) gives the positive solution $(M,M/J)$ of (4.9).
• Theorem 4.2: existence and uniqueness of positive solutions of (4.10) and (4.9) in the standard case $R\succeq\delta I$.
• Theorem 4.3: existence for (4.13) and (4.9) in the singular case $R\equiv0$.
• Three steps from the proof of Theorem 4.4:
  • $\alpha$ is bounded, so $u^*$ is admissible and $X^*$ has continuous paths with $\mathbb E\sup_s|X^*_s|^2<\infty$;
  • the ansatz $p(s;t)=M_sX^*_s-N_s\mathbb E_t[X^*_s]-\Gamma^{(1)}_sX^*_t+\Phi_s$, $k(s;t)=M_s[C_sX^*_s+D_su^*_s+\sigma_s]$ solves the adjoint flow (3.10);
  • the identity $\Lambda(s;t)=N_s[X^*_s-\mathbb E_tX^*_s]B_s+\Gamma^{(1)}_s(X^*_s-X^*_t)B_s$ holds, and $\Lambda$ satisfies condition (3.4).

Significance

The theorem gives an equilibrium in closed form, as a linear feedback of the current state with deterministic gains. That makes the equilibrium computable and comparable with the classical, time-consistent LQ regulator. Setting $h=\mu_1=0$ recovers a standard LQ problem, but (4.9) differs from the classical Riccati equation even then: it is a nonsymmetric coupled system (footnote 2, p. 10), and the cases (i)–(iii) are the conditions under which it is solvable. The mean–variance results of §5 (mission III) follow the same pattern.

The result is proved in the paper; to our knowledge it has not been formalized. A formal proof needs global existence for a nonlinear, nonautonomous ODE system with Carathéodory coefficients, obtained by truncation and a priori bounds. It also needs linear SDEs with bounded feedback, Itô calculus for products of deterministic and Itô processes, and the sufficient condition of mission I. Uniqueness in case (iii) is claimed by Theorem 4.4 but not proved in Theorem 4.3; it is part of the goal.

Difficulty

The system (4.9) is quadratic in $(M,N)$. Its solutions can blow up in finite time, and $(R+MD'D)^{-1}$ can degenerate when $M$ changes sign. Picard–Lindelöf therefore gives only local solutions, and a global solution needs a priori bounds $0<\eta\le M\le L$ and $J\ge1$, with $\eta$ and $L$ independent of the truncation level. Those bounds are where the case hypotheses enter. In the stochastic half, the equilibrium property is not proved by computing $J$ directly. It requires checking that the explicit candidate meets the flow-of-FBSDE sufficient condition, and the flow carries a parameter $t$ and the conditional expectations $\mathbb E_t[X^*_s]$ for every $s\ge t$.

Formalization scope

The general model (data, standing assumptions, states, conditional cost, spike, equilibrium) is stated for arbitrary $n$ and instantiated at $n=1$ through toData. It is built on the published substrate Peng1990_SMP_Stochastic (Brownian motion, natural filtration, $L^2_{\mathcal F}$, Itô integrals, SDE solutions). The formalization commits to the following choices.

• Definition 2.1 uses $\liminf$ in $\overline{\mathbb R}$, along every sequence $\varepsilon_k\downarrow0$, almost surely for each sequence, and for every version of the state and of the perturbed states. The page writes $\lim$, which need not exist.
• The filtration is the natural, uncompleted filtration of $W$, not the augmented one.
• The state from time $t$ is encoded through the full horizon. The spike is additive on $[t,t+\varepsilon)$.
• "Essentially bounded" and "a.s., a.e." are read $d\mathbb P\otimes ds$-a.e.
• Every ODE ((4.8), (4.9), (4.10), (4.13)) is stated in integral form on $[0,T]$, because the coefficients are only bounded measurable. A solution includes invertibility of $R+MD'D$ (resp. $D'D$) on $[0,T]$. Uniqueness means agreement on $[0,T]$.
• The constants $\delta,\lambda$ are uniform in $s$, and the case conditions hold for every $s\in[0,T]$. In $\frac{QD'D+|C|^2R}{l}$, $l$ is the control dimension.
• "Let $\Phi$ be a solution of (4.8)" means every solution. "$u^*$ is an equilibrium" means that a closed-loop state exists and that the feedback is an equilibrium along every closed-loop state.
• Conditional-expectation families $\mathbb E_t[X^*_s]$ are handled through arbitrary progressive versions. Condition (3.4) is stated exactly: its first part as a localization on $\mathcal F_t$-sets, its second part with a jointly measurable version and "a.e. $s$".
• The paper's "$\beta$ uniformly bounded" is false when $\sigma$ is only square integrable. The milestone states the true claim: $\alpha$ is essentially bounded on $[0,T]$ (the coefficients are only essentially bounded) and $\beta$ is square integrable.

The goal's conclusion is Definition 2.1 itself; it does not mention $\Lambda$, $p$ or (3.4). Existence of the closed-loop state is asserted, not assumed. A formalization that assumes existence, or that replaces equilibrium by condition (3.4), is a different and weaker theorem.

Theorem 3.3 (the $n=1$ sufficient condition) is not posed here. Under the shared model it is mission I's goal at $n=1$. Contributions are welcome on the ODE layer (truncation, comparison and Gronwall bounds for Carathéodory systems), on linear SDEs with bounded feedback, and on the Itô product rule. These parts are reusable well beyond this paper.

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
• T. Björk, A. Murgoci, X. Y. Zhou, Mean–variance portfolio optimization with state-dependent risk aversion, Mathematical Finance 24(1), 2014. https://doi.org/10.1111/j.1467-9965.2011.00515.x
• S. Basak, G. Chabakauri, Dynamic mean–variance asset allocation, Review of Financial Studies 23(8), 2010. https://doi.org/10.1093/rfs/hhq028
• X. Y. Zhou, D. Li, Continuous-time mean–variance portfolio selection: a stochastic LQ framework, Applied Mathematics and Optimization 42, 2000. https://doi.org/10.1007/s002450010003
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. 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
• Missions I and III of this series: the sufficient condition (Theorem 3.2) and the mean–variance equilibrium (Theorem 5.4).

Motivation

A prophet inequality compares a gambler who sees independent random rewards one at a time, and must accept or reject each on arrival, with a prophet who sees all rewards in advance. The classical inequality of Krengel, Sucheston and Garling (1977–78, as cited in the paper) says that when only one reward may be kept, a single threshold rule earns at least half of $\mathbb E[\max_i X_i]$, and Samuel-Cahn (1984) showed that the threshold can be chosen as a median. Such statements are the analytical core of sequential posted-price mechanisms: Hajiaghayi, Kleinberg and Sandholm (2007) observed that threshold rules are truthful online auctions, and Chawla, Hartline, Malec and Sivan (2010) showed that sequential posted prices approximate the optimal Bayesian revenue in many settings, with prophet inequalities for the feasibility constraint as the key technique.

When several items may be accepted subject to a combinatorial constraint, the natural constraints in this application are matroids (for example, at most $k$ items, or at most one item per group) and intersections of matroids (for example, bipartite matchings, which are intersections of two partition matroids). Kleinberg and Weinberg (STOC 2012) proved that for every matroid there is an online algorithm with expected payoff at least half of the expected maximum-weight basis, and that for the intersection of $p$ matroids the summed version of the same algorithm earns at least $\frac{1}{4p-2}$ of the expected optimum. This mission formalizes the second result.

Timeline:

• 1977–78: Krengel–Sucheston and Garling, single-choice prophet inequality with factor 2.
• 1984: Samuel-Cahn, the median threshold rule attains factor 2.
• 2007: Hajiaghayi–Kleinberg–Sandholm, threshold rules from prophet inequalities read as truthful online auction mechanisms.
• 2010: Chawla–Hartline–Malec–Sivan, sequential posted pricing; factor 2 for matroids when the algorithm may choose the order in which elements are observed.
• 2012: Kleinberg–Weinberg, factor 2 for matroids and $4p-2$ for intersections of $p$ matroids, against online weight-adaptive adversaries.

Setting

A finite ground set $\mathcal U$ carries $p \ge 1$ matroids $\mathcal M_1,\dots,\mathcal M_p$ with independent sets $\mathcal I_1,\dots,\mathcal I_p$ and closure operators $\mathrm{cl}_1,\dots,\mathrm{cl}_p$. A set is feasible if it lies in $\mathcal I = \bigcap_j \mathcal I_j$. Each element $x$ has a random weight $w(x) \ge 0$; the weights are independent and $w(x)$ has law $F_x$. For a set $S$, $w(S) = \sum_{x \in S} w(x)$, $\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 chooses the $i$-th element $x_i$ after learning $w(x_1),\dots,w(x_{i-1})$, but without knowing $w(x_i)$ or any other unrevealed weight. A threshold algorithm offers $x_i$ a threshold $T_i$ computed from what has been revealed and from the set $A_{i-1}$ already selected, and selects $x_i$ exactly when $A_{i-1}\cup\{x_i\}\in\mathcal I$ and $w(x_i) \ge T_i$.

The algorithm of the paper uses a ghost sample $w'$, an independent copy of $w$. Let $B$ be a $w'$-maximum feasible set. For a set $A$ and each $j$, $R_j(A) \subseteq B \setminus A$ is a set of maximum $w'$-weight with $A \cup R_j(A) \in \mathcal I_j$ and $B \subseteq \mathrm{cl}_j(A \cup R_j(A))$, and $C_j(A) = B \setminus R_j(A)$. Put $R(A) = \bigcap_j R_j(A)$ and $C(A) = \bigcup_j C_j(A)$. For a parameter $\alpha$, the summed thresholds are

$$T(A,i) = \sum_{j=1}^p \frac1\alpha\, \mathbb E_{w'}\big[w'(R_j(A)) - w'(R_j(A \cup \{x_i\}))\big],$$

and the algorithm of §4.2 uses $T_i = T(A_{i-1}, i)$. An algorithm has $\alpha$-balanced thresholds (Definition 3) if, for every input sequence with selected set $A$ and every $V$ disjoint from $A$ with $A \cup V \in \mathcal I$,

$$\sum_{x_i\in A} T_i \ge \frac1\alpha \mathbb E\Big[\sum_j w'(C_j(A))\Big], \qquad \sum_{x_i\in V} T_i \le \frac1\alpha \mathbb E\Big[\sum_j w'(R_j(A))\Big].$$

Formalization targets

Goal: the prophet inequality for $p$ matroids

For every $p \ge 1$, all matroids $\mathcal M_1,\dots,\mathcal M_p$ on $\mathcal U$, all laws $F_x$ on $[0,\infty)$ with finite means, and every online weight-adaptive adversary, the algorithm of §4.2 with $\alpha = 2p$ selects a set $A$ with

$$\mathbb E[w(A)] \ge \frac{1}{4p-2}\, \mathbb E[\mathrm{OPT}(w)].$$

For $p = 1$ this is the factor-2 matroid prophet inequality.

Proposition 3

If a threshold algorithm has $\alpha$-balanced thresholds for some $\alpha \ge 2$, then against every online weight-adaptive adversary

$$\mathbb E[w(A)] \ge \frac{\alpha - p}{\alpha(\alpha-1)}\, \mathrm{OPT}.$$

Milestones

Proposition 2 for each matroid $\mathcal M_j$; the identity between the two forms of $T(A,i,j)$; properties (13) and (14) for the summed thresholds; the identities (20)–(21); and the inequalities (23)–(24) of Appendix A. Together with Proposition 3 these give the goal.

Significance

The bound gives a posted-price style selection rule for any feasibility constraint that is an intersection of $p$ matroids, with a guarantee depending only on $p$; the paper's §5 shows that a ratio of order $p$ is necessary. Section 6 of the paper turns the result into sequential posted-price mechanisms for multi-dimensional mechanism design, and that application needs the guarantee against the online weight-adaptive adversary, not only against a fixed order. The reduction "balanced thresholds imply an approximation" (Proposition 3) is reusable for other threshold constructions.

The result is proved in the paper; to our knowledge no machine-checked proof exists. The mission produces a formal proof of the $\frac{1}{4p-2}$ guarantee, with the probabilistic part (the ghost-sample argument against an adaptive adversary) and the combinatorial part (the per-matroid exchange inequality) as separate milestones. The paper justifies the per-matroid use of Proposition 2 in one paragraph; because $B$ maximizes $w'$ over the intersection rather than over $\mathcal I_j$, the description of $R_j(A)$ as a maximum-weight basis of a contraction (Lemma 2 in the single-matroid case) does not apply verbatim, and the formal proof of that milestone is not a copy of the paper's single-matroid argument.

Difficulty

Two steps do not follow from routine bookkeeping. First, the inequality (23) compares the gambler's surplus, collected along an order that the adversary adapts to the realized weights, with the ghost sample's surplus on the random set $R(A)$. The index $x_i$ revealed at step $i$ is itself random, so the step "the weight of the element offered next is distributed as its ghost weight" has to be justified for an adaptively chosen index under a product measure; it fails for an adversary that may look at unrevealed weights. Second, the paper obtains (14) by applying the single-matroid Proposition 2 to each $\mathcal M_j$, but its proof of Proposition 2 describes $R(A)$ as a maximum-weight basis of a contraction, which uses that $B$ is optimal for the matroid in question. Here $B$ is optimal only for the intersection $\mathcal I$, so the obvious transfer of the single-matroid argument does not go through as written and the per-matroid statement needs its own proof.

Formalization scope

The ground set is a Fintype; the matroids are Mathlib's Matroid α, indexed by Fin p, each with ground set Set.univ; sets are Finset α. Weights are functions α → ℝ, the weight law is Measure.pi F, and every theorem assumes each F x is a probability measure with F x (Iio 0) = 0 and a finite mean. Expectations are Bochner integrals; under these assumptions every integrand is integrable. Ties in the maximizers $B$ and $R_j(A)$ are broken by a fixed rule that does not depend on the weights. $R_j(A)$ is taken disjoint from $A$. The threshold $\infty$ on infeasible steps is a feasibility test in the selection rule. Adversaries and generic threshold rules are deterministic, see only revealed weights, and are measurable in them; randomized adversaries are mixtures of deterministic ones. Generic thresholds in Proposition 3, (23) and (24) are non-negative, as in the paper's $T_i \in \mathbb R_+ \cup \{\infty\}$.

The goal fixes the thresholds to the summed thresholds of §4.2 with $\alpha = 2p$, computed from the ghost-sample objects. A version in which the thresholds are free parameters assumed to satisfy (13)–(14) would be Proposition 3 itself and is ruled out; conversely, Proposition 3 does not mention the §4.2 thresholds.

A complete development needs: elementary facts about maximizers over finite families; matroid exchange properties (a bijective exchange between equal-size independent sets, available in Schrijver's book but not in Mathlib); submodularity of weighted-rank-type functions; and the independence argument for adaptively chosen indices under a product measure. The last two are reusable beyond this mission, as is Proposition 3. Proofs of individual milestones and of these auxiliary facts are welcome.

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 (1977), 745–747.
• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Ann. Probab. 12 (1984). https://doi.org/10.1214/aop/1176993150
• M. T. Hajiaghayi, R. Kleinberg, T. Sandholm, Automated online mechanism design and prophet inequalities, Proc. 22nd AAAI Conference on Artificial Intelligence, 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; arXiv:0907.2435. https://arxiv.org/abs/0907.2435
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer 2003 (Corollary 39.12a).

Motivation

Mean–variance portfolio selection (Markowitz, 1952) trades off the expected terminal wealth of an investor against its variance. In a dynamic setting the problem is time-inconsistent: the variance is not a conditional expectation of a function of terminal wealth, so the dynamic-programming principle fails, and a strategy that is optimal when computed at time $0$ is no longer optimal when re-evaluated at a later time. A standard response is to treat the investor at each time $t$ as a separate player and to look for a subgame-perfect equilibrium strategy, which no future self wishes to deviate from locally (Björk–Murgoci, Ekeland–Lazrak, and others).

Hu, Jin and Zhou (arXiv:1111.0818v1; SIAM J. Control Optim. 50(3), 2012) define open-loop equilibria for a general class of time-inconsistent stochastic linear–quadratic (LQ) problems and characterize them through a flow of forward–backward SDEs. Their §5 applies this to mean–variance investment in a complete market with a random risk premium, where the weight on expected wealth depends on current wealth (a state-dependent risk aversion, motivated in Björk–Murgoci–Zhou, 2014). Earlier equilibrium results for mean–variance investment (Basak–Chabakauri, 2010; Björk–Murgoci–Zhou) work with deterministic or Markovian coefficients and within feedback classes.

This mission is the third of a series on the paper. Mission I formalizes the general sufficient condition (Theorem 3.2); Mission II treats deterministic coefficients and coupled Riccati equations (Theorem 4.4). This mission targets the explicit mean–variance equilibrium of Theorem 5.4.

Setting

Fix a horizon $T>0$ and a probability space carrying a standard $d$-dimensional Brownian motion $W$ with its filtration $(\mathcal F_t)$; write $E_t=E[\,\cdot\,|\mathcal F_t]$. The market has a deterministic bounded interest rate $r$ and a progressively measurable, essentially bounded risk premium $\theta$ with values in $\mathbb R^d$. A strategy is a progressively measurable $u$ with $E\int_0^T|u_s|^2ds<\infty$ (the class $L^2_{\mathcal F}(0,T;\mathbb R^d)$); the wealth $X$ under $u$ solves

$$dX_s=r_sX_s\,ds+\theta_s'u_s\,ds+u_s'\,dW_s,\qquad X_0=x_0 .\tag{5.2}$$

At time $t$, with current wealth $x_t$, the investor's cost is

$$J(t,x_t;u)=\tfrac12\mathrm{Var}_t(X_T)-(\mu_1x_t+\mu_2)E_t[X_T],\qquad\mu_1\ge0 .\tag{5.3}$$

This is the case $n=1$ of the paper's general LQ problem, with $A=r$, $B=\theta$, $C=0$, $D=I$, $Q=R=0$, $G=h=1$; the mission states it that way. For $t\in[0,T)$, $\varepsilon>0$ and an $\mathcal F_t$-measurable square-integrable $v$, the spike $u^{t,\varepsilon,v}_s=u_s+v\,\mathbf 1_{[t,t+\varepsilon)}(s)$ perturbs $u$ on a short window. A strategy $u^*$ with wealth $X^*$ is an equilibrium (Definition 2.1) if, for all such $t$ and $v$,

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

The equilibrium is built from $\Gamma^{(1)}_s=\mu_1e^{\int_s^Tr}$, $\Gamma_s=-\mu_2e^{\int_s^Tr}$, and two backward SDEs: an indefinite stochastic Riccati equation for $(M,U)$,

$$dM_s=-\big(2r_sM_s-U_s'\theta_s+\Gamma^{(1)}_s|\theta_s|^2-M_s^{-1}|U_s|^2+\Gamma^{(1)}_sM_s^{-1}U_s'\theta_s\big)ds+U_s'\,dW_s,\quad M_T=1,\tag{5.8}$$

and a linear BSDE (5.13) for $(\Gamma^{(2)},\gamma^{(2)})$ whose coefficients involve $M$ and $U$. A process $Z$ gives a BMO martingale $Z\cdot W$ if $E[\int_\tau^T|Z_s|^2ds\,|\,\mathcal F_\tau]\le C$ for all stopping times $\tau\le T$.

Formalization targets

Goal: Theorem 5.4

If $(M,U)$ solves (5.8) with $M$ bounded and $M\ge c>0$, and $(\Gamma^{(2)},\gamma^{(2)})$ solves (5.13) with $\Gamma^{(2)}$ bounded, then

$$u^*_s=-M_s^{-1}\Big[\big(U_s-\theta_s\mu_1e^{\int_s^Tr_v\,dv}\big)X^*_s+\Gamma_s\theta_s+\gamma^{(2)}_s\Big]$$

is an equilibrium: the closed-loop wealth exists, and for every closed-loop wealth $X^*$ the strategy $u^*$ satisfies Definition 2.1.

Milestones

1. Proposition 5.1: (5.8) has a unique solution in $L^\infty\times L^2$ with $M\ge c>0$, and $U\cdot W$ is BMO.
2. Proposition 5.2: (5.13) has a unique solution in $L^\infty\times L^2$, and $\gamma^{(2)}\cdot W$ is BMO.
3. Proposition 5.3: the closed-loop wealth under the feedback exists with continuous paths, $E\sup_t|X^*_t|^2<\infty$, and $u^*\in L^2$.
4. Proof of Theorem 5.4: the processes $p(s;t)$, $k(s;t)$ of (5.5) and (5.7) solve the adjoint equation (5.4), $\Lambda(s;t)=p(s;t)\theta_s+k(s;t)$ has the closed form displayed on p. 22, and $\Lambda$ meets condition (3.4).

Significance

Theorem 5.4 gives the equilibrium of a time-inconsistent mean–variance investor in closed form, linear in current wealth, for a random risk premium. With a deterministic premium it reduces to explicit formulas (§5.4), and for $\mu_1=0$ it recovers the equilibrium of Basak–Chabakauri and Björk–Murgoci; for $\mu_2=0$ it differs from the feedback equilibrium of Björk–Murgoci–Zhou, which shows that open-loop and feedback equilibria are different notions. The random premium is what makes $U\neq0$ and the feedback gain unbounded.

The result is proved in the paper; nothing here is formalized elsewhere. The mission produces machine-checked statements of the equilibrium, of solvability of the Riccati-type BSDE (5.8), and of the integrability of a linear SDE with BMO-type coefficients, on the platform's published stochastic-calculus substrate. The definition of BMO martingales and the encoding of open-loop equilibria are reusable beyond this paper.

Difficulty

The verification step that most readers try first, plugging $u^*$ into the wealth equation and applying standard SDE estimates, fails: the gain $\alpha=(\Gamma^{(1)}\theta-U)/M$ is unbounded, because $U$ is only BMO, so the closed-loop SDE is linear with non-Lipschitz-bounded random coefficients and neither existence of the wealth nor $u^*\in L^2$ follows from standard theory (Proposition 5.3). The BSDE (5.8) has a driver with quadratic growth in $U$ and a singular factor $M^{-1}$; it is not covered by the standard theory of stochastic Riccati equations and its solution must be bounded away from zero for the feedback to make sense. Uniqueness in (5.8) and solvability of (5.13) rely on BMO-martingale and change-of-measure facts (Kazamaki) that are not in Mathlib. Finally, the equilibrium property is a statement about every $t$ and every perturbation, and the sufficient condition (Theorem 3.3) needs the limit behaviour of conditional expectations $E_t[\Lambda(s;t)]$ as $s\downarrow t$.

Formalization scope

Everything is built on the published definition Peng1990_SMP_Stochastic (Brownian motion, $L^2_{\mathcal F}$, Itô integrals, SDEs and BSDEs as relations). The general LQ model, the spike, the conditional cost and Definition 2.1 are in Model; the adjoint equation on $[t,T]$, $\Lambda$ and condition (3.4) in Adjoint; the market, $\Gamma^{(1)}$, $\Gamma$, BMO, (5.8), (5.13) and (5.14) in Market. Conventions the statements commit to:

• Lower limit. Definition 2.1 is stated with $\liminf$ in $\overline{\mathbb R}$, along every sequence $\varepsilon_k\downarrow0$, almost surely for each sequence. The page writes $\lim$; the limit need not exist, and the paper's own argument bounds the lower limit.
• Filtration. The natural, uncompleted filtration of $W$ instead of the augmented one; conditional expectations and progressive processes agree up to null sets.
• States from time $t$ are solutions on the whole horizon $[0,T]$ for a control equal to $u^*$ before $t$.
• Versions. Conditions involving conditional expectations at uncountably many times are stated through jointly measurable versions; "a.s., a.e." means $ds\otimes dP$-a.e.; uniqueness of BSDE solutions is up to modification and $ds\otimes dP$-null sets; BMO is in integrated form.
• Market primitive. The risk premium $\theta$ is the primitive, as in (5.2); every bounded progressive $\theta$ comes from some bounded $(\mu,\sigma)$ with $\sigma\sigma'\succeq\varepsilon I$.
• Existence statements. Peng's SDE solutions already carry $u^*\in L^2$ and $\sup_tE|X_t|^2<\infty$, so Proposition 5.3 is stated as existence of a closed-loop solution with continuous paths and $E\sup_t|X^*_t|^2<\infty$. Theorem 5.4 asserts existence of the closed-loop wealth instead of assuming it.

The goal does not assume the BMO properties of $U$ and $\gamma^{(2)}$ (they are conclusions of Propositions 5.1–5.2), does not assume $\theta$ deterministic or $U=0$ (that is the special case of §5.4), and keeps $Q=R=0$, $G=h=1$; a formalization that assumes any of these, or that admits the junk value $M^{-1}=0$ on a non-null set, proves a different theorem. Theorem 3.3, the sufficient condition used in the last line of the proof, is the $n=1$ case of Mission I's goal and is not restated here. Welcome contributions: a BMO and Girsanov library on the Peng substrate, existence for quadratic BSDEs, and a proof of the sufficient condition.

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
• S. Basak, G. Chabakauri, Dynamic mean-variance asset allocation, Rev. Financ. Stud. 23(8), 2010. https://doi.org/10.1093/rfs/hhq028
• T. Björk, A. Murgoci, X. Y. Zhou, Mean–variance portfolio optimization with state-dependent risk aversion, Math. Finance 24(1), 2014. https://doi.org/10.1111/j.1467-9965.2011.00515.x
• N. Kazamaki, Continuous Exponential Martingales and BMO, Lecture Notes in Math. 1579, Springer, 1994. https://doi.org/10.1007/BFb0073585
• M. Kobylanski, Backward stochastic differential equations and partial differential equations with quadratic growth, Ann. Probab. 28(2), 2000. https://doi.org/10.1214/aop/1019160253
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054

Rolling schedules and quantity flexibility

Manufacturers routinely share rolling schedules with their suppliers: each period the buyer commits to a purchase for the current period and issues non-binding estimates for future periods, then revises those estimates as the horizon rolls forward. Unconstrained revisions push forecast risk upstream and are a recognized source of the bullwhip effect. A quantity flexibility (QF) contract bounds how far each estimate may move between consecutive issues, giving the supplier a guarantee in exchange for a commitment to cover any order within the bounds. Tsay and Lovejoy (MSOM 1(2), 1999) model a chain of firms linked by QF contracts and ask how a firm in the middle of the chain, the flex node, should translate the schedules it receives into the schedules it issues. Their answer is the Minimum Commitment (MC) policy, justified by Proposition 1: MC solves the node's open-loop planning problem and never breaks either contract.

This mission formalizes Proposition 1. A companion mission (Quantity Flexibility Contracts and Supply Chain Performance 1) formalizes Proposition 2, on when MC keeps zero inventory.

Setting

Periods are $t = 0, 1, 2, \dots$. In period $t$ the node receives from its customer a release schedule $f(t) = [f_0(t), f_1(t), \dots]$: $f_0(t)$ is bought now, $f_j(t)$ estimates the purchase in period $t + j$. The node issues to its supplier a replenishment schedule $r(t) = [r_0(t), r_1(t), \dots]$ of the same form. Its ending stock is $I(t) = I(t-1) + r_0(t) - f_0(t)$.

The contracts carry parameters $\alpha_q \ge 0$ and $0 \le \omega_q \le 1$ ($q \ge 1$): output parameters $(\alpha^{out}, \omega^{out})$ with the customer and input parameters $(\alpha^{in}, \omega^{in})$ with the supplier. The incremental revision (IR) constraints are, for all $t$ and $j \ge 1$,

$$(1-\omega^{out}_j) f_j(t) \le f_{j-1}(t+1) \le (1+\alpha^{out}_j) f_j(t), \qquad (6)$$ $$(1-\omega^{in}_j) r_j(t) \le r_{j-1}(t+1) \le (1+\alpha^{in}_j) r_j(t). \qquad (7)$$

The cumulative parameters are $1 + A_j = \prod_{q=1}^j (1+\alpha_q)$ and $1 - \Omega_j = \prod_{q=1}^j (1-\omega_q)$, so $A_0 = \Omega_0 = 0$. A convex cost $G$, minimized at $0$, is charged on ending stock.

At period $t$, with $I(t-1)$, $r(t-1)$ and $f(t)$ known, the open-loop program (F-OLFC) chooses $r(t)$ and the planned purchases $r_0(t+j)$, $j = 0, \dots, h$, to minimize $\sum_{j=0}^h G(I(t+j))$ subject to the stock balance $I(t+j) = I(t+j-1) + r_0(t+j) - (1+A^{out}_j) f_j(t)$ (17), coverage $I(t+j) \ge 0$ (18), the input IR constraints (19) between $r(t-1)$ and $r(t)$, and the cumulative bounds $(1-\Omega^{in}_j) r_j(t) \le r_0(t+j) \le (1+A^{in}_j) r_j(t)$ (20).

The MC policy computes $r(t)$ and projected inventories $l_j(t)$ by one recursion on $j$: $l_0(t) = I(t-1)$,

$$r_j(t) = \max\Big[\frac{(1+A^{out}_j) f_j(t) - l_j(t)}{1+A^{in}_j},\ (1-\omega^{in}_{j+1}) r_{j+1}(t-1)\Big], \qquad (21)\text{–}(22)$$ $$l_{j+1}(t) = \big[l_j(t) + (1-\Omega^{in}_j) r_j(t) - (1+A^{out}_j) f_j(t)\big]^+. \qquad (23)$$

In Lean: QFParams, Acum, Ωcum, IROut, IRIn, mcStep, run, inv, sched, projInvAt (module Model) and stock, Feasible, RelaxedFeasible, objective, lbar, pStar (module FOLFC).

Formalization targets

Goal: Proposition 1 (p. 96)

For an MC run from $(I(0), r(0))$ with $r(0) \ge 0$, against any customer schedules obeying (6), and any convex $G$ minimized at zero:

$$I(t) \ge 0 \ (t \ge 1), \qquad (1-\omega^{in}_{j+1}) r_{j+1}(t-1) \le r_j(t) \le (1+\alpha^{in}_{j+1}) r_{j+1}(t-1) \ (t \ge 2,\ j \ge 0),$$

and for every $t \ge 2$ the schedule $r(t)$, with suitable planned purchases, is feasible for (F-OLFC) at period $t$ and attains its minimum.

Milestones

1. Lemma 1 (p. 108): under (a) $I(t-1) \ge 0$ and (b) the upside of (6), $l_j(t) \ge l_{j+1}(t-1)$ for all $j \ge 0$.
2. (30)–(31) (pp. 107–108): with the upper bounds of (19) and (20) removed, the lot-for-lot purchases $r_0^*(t+j) = \max\{(1+A^{out}_j) f_j(t) - \bar l_j(t),\ (1-\Omega^{in}_{j+1}) r_{j+1}(t-1)\}$ are optimal.
3. Upper bound of (19) (p. 108): $r_j(t) \le (1+\alpha^{in}_{j+1}) r_{j+1}(t-1)$ along the run.

Significance

Proposition 1 is what makes MC a well-defined operating rule for an intermediate firm: whatever the customer does within its contract, the node can serve it from stock and its own revisions stay within the supplier's contract, so the chain of contracts composes. Proposition 2 and the paper's simulation study of how flexibility propagates along a supply chain (§§5–6) both assume the node uses MC, and rely on Proposition 1 for that choice being both feasible and myopically optimal.

The paper's optimality argument is sketched: the relaxed solution is attributed to "a straightforward application of Kuhn–Tucker conditions" with details in an unpublished thesis, the equivalence of (32) with (21)–(23) is omitted, and Lemma 1's proof is replaced by intuition. A machine-checked proof supplies these steps. To our knowledge no part of this paper has been formalized before. The mission also fixes the statement: the printed range of (19) makes the optimality claim false, and the claim needs a start of the run that the paper leaves implicit.

Difficulty

The obvious argument treats (F-OLFC) as a lot-sizing problem with minimum lot sizes and observes that the greedy purchases (30) are optimal. That only solves the relaxation. The difficulty is that MC is not stated through (30): it is a recursion on the replenishment schedule with a positive part in the projected inventory, and one has to show that the MC schedule can carry the greedy purchases within the upper bounds of (19) and (20). Those bounds can bind, and whether they do depends on the previous period's schedule, so the optimality claim is not a one-period statement: it needs an induction over the run, through Lemma 1 and the customer's IR constraints. The admissibility half needs the same induction, with the nonnegativity of the schedules carried along.

Formalization scope

All quantities are real numbers. Parameters are sequences ℕ → ℝ whose index $0$ is unused; schedules are infinite sequences, and the MC recursion runs over all $j$. (6) and (7) are written with $j$ replaced by $j+1$. The standing assumptions $\alpha_q \ge 0$, $0 \le \omega_q \le 1$ ($q \ge 1$) are hypotheses. $G$ is any convex function with $G(0) \le G(y)$ for all $y$; no strict convexity, differentiability or monotonicity is assumed.

The run starts from an arbitrary state $(I(0), r(0))$ (run period $0$); the MC policy acts from period $1$. The following departures from the printed statement are disclosed:

1. (19) is imposed for $j = 0, \dots, h$, not the printed $j = 0, \dots, h-1$. With the printed range optimality fails: with all $\alpha = \omega^{in} = 0$, $\omega^{out}_1 = 1/2$, $I(0) = 0$ and $r(0) = f(0) = f(1) \equiv 10$, take $f_0(2) = 5$ and $h = 0$. Then (F-OLFC) at $t = 2$ has optimum $r_0(2) = 5$ with $I(2) = 0$, while MC orders $r_0(2) = r_1(1) = 10$. With (19) at $j = 0$, the order $r_0(2) \ge 10$ is forced and MC is optimal. Both (21) and (30) already use $r_{h+1}(t-1)$.
2. Input IR and optimality are claimed for $t \ge 2$, coverage for $t \ge 1$. At the first MC period the predecessor schedule is the arbitrary $r(0)$ and (7) can fail.
3. $r(0) \ge 0$ is assumed: with a negative entry the two bounds of (19) cross. Neither $I(0)$ nor $f$ carries a sign hypothesis.

(F-OLFC) ranges over all real schedules and purchases; the only MC-specific object in the goal is the candidate schedule. Optimality is stated as "feasible, and no feasible point has a smaller objective", never as an infimum, so an infeasible program cannot make it vacuous. The MC step is literally (21)–(23), with the carried-over term and the positive part; a run that sets $r(t) := f(t)$ or drops the max is a different policy.

Infrastructure: the model and (F-OLFC) are self-contained over Mathlib (Finset.prod, ConvexOn). Proofs of the three milestones, and of the monotonicity of a convex function minimized at zero on $[0, \infty)$, are welcome as separate contributions.

Selected references

• A. A. Tsay, W. S. Lovejoy, Quantity flexibility contracts and supply chain performance, Manufacturing & Service Operations Management 1(2):89–111, 1999. https://doi.org/10.1287/msom.1.2.89
• D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press, 1976 (open-loop feedback control).
• A. Federgruen, P. Zipkin, An inventory model with limited production capacity and uncertain demands, Mathematics of Operations Research 11(2):193–215, 1986. https://doi.org/10.1287/moor.11.2.193