Probability

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

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

Fourier analysis of functions on the discrete cube $\{-1,1\}^n$ is the main tool behind tight inapproximability results under the Unique Games Conjecture. In the MAX-CUT reduction of Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 2007), soundness rests on the Majority Is Stablest theorem: among bounded functions in which no coordinate has large influence, the majority function is asymptotically the most noise stable. That theorem was a conjecture when the paper was written and was proved by Mossel, O'Donnell and Oleszkiewicz (Annals of Math. 2010) using an invariance principle.

Section 6.2 of the paper records special cases of Majority Is Stablest that have short, self-contained proofs. Theorem 6 is the case where the noise parameter $\rho$ tends to $0$. There the noise stability is dominated by the Fourier weight at level 1, and the statement says that a bounded function with small influences has level-one weight at most $2/\pi$, up to an explicit error linear in the largest influence. Bounds on the level-one weight also appear in Talagrand's work on correlation of monotone sets (Combinatorica 1996), which the paper compares against (its Theorem 18), and the level-one inequality is a standard chapter of the analysis of Boolean functions (O'Donnell 2014).

Setting

Points of the discrete cube $\{-1,1\}^n$ are sign vectors $x=(x_1,\dots,x_n)$; following the paper, the bit TRUE is read as $-1$ and FALSE as $1$. The cube carries the uniform probability measure, so $\mathbf E[g]=2^{-n}\sum_x g(x)$, and real functions form an inner product space with $\langle f,g\rangle=\mathbf E[fg]$.

For $S\subseteq[n]$ the parity $\chi_S(x)=\prod_{i\in S}x_i$; the parities form an orthonormal basis, and the Fourier coefficient of $f$ at $S$ is $\hat f(S)=\langle f,\chi_S\rangle$. The weight of $f$ at level 1 is

$$W^1(f)=\sum_{|S|=1}\hat f(S)^2=\sum_{i=1}^n\hat f(\{i\})^2 .$$

The influence of coordinate $i$ on $f$ (Definition 2) is

$$\mathrm{Inf}_i(f)=\mathop{\mathbf E}_{x_1,\dots,x_{i-1},x_{i+1},\dots,x_n}\big[\mathrm{Var}_{x_i}[f]\big],$$

the expected variance of $f$ when all coordinates but $x_i$ are fixed at random and $x_i$ is a uniform sign. The linear part of $f$ is $\ell(x)=\sum_i\hat f(\{i\})x_i$, and $\|g\|_1=\mathbf E|g|$, $\|g\|_2=\sqrt{\mathbf E[g^2]}$, $\|g\|_\infty=\max_x|g(x)|$.

Throughout, $C=2\big(1-\sqrt{2/\pi}\big)\approx 0.404$.

Formalization targets

Goal: Theorem 6 (p. 12)

For every $n$, every $f:\{-1,1\}^n\to[-1,1]$ and every $\delta\ge 0$ with $\mathrm{Inf}_i(f)\le\delta$ for all $i$,

$$\sum_{|S|=1}\hat f(S)^2\;\le\;\frac{2}{\pi}+C\delta .$$

The constant $C$ is explicit, and the goal states it exactly as printed.

Milestones (proof of Theorem 6, p. 25, and Proposition 7.2, p. 16)

1. For $f$ with values in $[-1,1]$: $\sum_{|S|=1}\hat f(S)^2=\|\ell\|_2^2=\langle f,\ell\rangle\le\|f\|_\infty\|\ell\|_1\le\|\ell\|_1$.
2. The König–Schütt–Tomczak-Jaegermann bound: if $|a_i|\le\delta$ for all $i$ and $\ell=\sum_i a_ix_i$, then

$$\|\ell\|_1\le\sqrt{2/\pi}\,\|\ell\|_2+\tfrac C2\,\delta .$$

3. The quadratic step: for $X,\delta\ge0$, $X^2\le\sqrt{2/\pi}\,X+\tfrac C2\delta$ implies $X\le\sqrt{1/2\pi}+\sqrt{1/2\pi+C\delta/2}$ and $X^2\le 2/\pi+C\delta$.
4. Proposition 7.2: $\mathrm{Inf}_i(f)=\sum_{S\ni i}\hat f(S)^2$.

Significance

The result. The constant $2/\pi$ is sharp: majority on $n$ variables has influences of order $n^{-1/2}$ and level-one weight tending to $2/\pi$, which is $(\mathbf E|Z|)^2$ for a standard Gaussian $Z$. Theorem 6 thus identifies the extremal level-one weight of low-influence bounded functions and gives a rate linear in the maximal influence. It is the $\rho\to0$ instance of Majority Is Stablest, obtained without the invariance principle, and level-one bounds of this type are used in hardness reductions and in the study of noise sensitivity.

Formalizing it. The milestones together give a complete formal route from bounded functions to the stated bound, except for one step discussed below. They also produce a reusable layer of Boolean Fourier analysis: Fourier coefficients, level weights, influences in their variance form and the Fourier formula for influences. Mathlib contains no development of influences or level weights on the cube, and the platform has none either; the König–Schütt–Tomczak-Jaegermann inequality, a sharp quantitative central limit bound for Rademacher sums (J. Reine Angew. Math. 1999), has no machine-checked proof.

Status. The published proof's first step, $|\hat f(\{i\})|\le\mathrm{Inf}_i(f)$, is valid for Boolean-valued $f$ but not for $[-1,1]$-valued $f$; for $[-1,1]$-valued $f$ the statement is posed as printed. For $f=c\,x_1$ with $0<c<1$ one has $\hat f(\{1\})=c>c^2=\mathrm{Inf}_1(f)$, and the argument as written then yields only $2/\pi+C\sqrt\delta$. Numerical search over small cubes has found no function violating the printed bound. A proof of the goal for bounded $f$, or a counterexample, is therefore a genuine contribution.

Difficulty

The obvious argument replaces $\ell$ by a Gaussian with the same variance and uses $\mathbf E|Z|=\sqrt{2/\pi}$. A central limit theorem with an error term is needed, and generic Berry–Esseen bounds give an additive error with a constant far from $C/2$; the exact constant $1-\sqrt{2/\pi}$ requires the sharp Rademacher-sum inequality, whose proof is a delicate analysis of $\mathbf E|\sum_ia_ix_i|$ as a function of the coefficients. The second obstacle is the passage from influences to coefficients. For bounded $f$ only $\hat f(\{i\})^2\le\mathrm{Inf}_i(f)$ holds, so a bound on influences controls coefficients only at scale $\sqrt\delta$; feeding that into the chain loses the linear dependence on $\delta$. Recovering the printed rate for non-Boolean $f$ needs an idea beyond the published proof.

Formalization scope

A point of the cube is Fin n → Bool, mapped to a sign by pm with pm true = -1 and pm false = 1. Expectations are normalised finite sums, so no measure theory is involved. A function $f:\{-1,1\}^n\to[-1,1]$ is a real function with the hypothesis ∀ x, |f x| ≤ 1. The influence is defined as on the page, as the average over the cube of $\big((f(x^{i\leftarrow1})-f(x^{i\leftarrow-1}))/2\big)^2$, which is the variance in $x_i$; it is not defined by its Fourier formula, which is a milestone. The level-one weight is $\sum_i\hat f(\{i\})^2$. The constant $C$ is written out as 2 * (1 - Real.sqrt (2 / Real.pi)); an existentially quantified constant would be a weaker theorem. The case $n=0$ is allowed.

Two hypotheses are added and disclosed: $\delta\ge0$ in Theorem 6 and in the König–Schütt–Tomczak-Jaegermann bound. For $n\ge1$ each follows from the other hypotheses; for $n=0$ the influence (resp. coefficient) hypothesis is empty and $\delta\ge0$ is what the page assumes.

A trivializing formalization would drop the range hypothesis (then scaled dictators refute the bound and the statement is false), define influence through Fourier coefficients (which makes Proposition 7.2 definitional), or weaken the hypothesis of the goal to a bound on the coefficients $|\hat f(\{i\})|\le\delta$; none of these is used here. In particular, the goal is not strengthened to Boolean-valued $f$, where the published proof applies verbatim.

Contributions welcome: proofs of Parseval-type identities for the linear part, of Proposition 7.2, of the elementary quadratic step, of the König–Schütt–Tomczak-Jaegermann inequality, and of the goal itself. The cube layer is reusable for any later formalization of Boolean function analysis.

Selected references

• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal Inapproximability Results for MAX-CUT and Other 2-Variable CSPs?, SIAM J. Comput. 37(1), 2007. https://doi.org/10.1137/S0097539705447372
• E. Mossel, R. O'Donnell, K. Oleszkiewicz, Noise stability of functions with low influences: invariance and optimality, Annals of Mathematics 171(1), 2010. https://doi.org/10.4007/annals.2010.171.295
• H. König, C. Schütt, N. Tomczak-Jaegermann, Projection constants of symmetric spaces and variants of Khintchine's inequality, J. Reine Angew. Math. 511, 1999. https://doi.org/10.1515/crll.1999.511.1
• M. Talagrand, How much are increasing sets positively correlated?, Combinatorica 16(2), 1996. https://doi.org/10.1007/BF01844850
• R. O'Donnell, Analysis of Boolean Functions, Cambridge University Press, 2014. https://arxiv.org/abs/2105.10386

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

Stochastic differential equations (SDEs) are simulated almost always by time-stepping schemes, and the cheapest and most widely used is the explicit Euler (Euler–Maruyama) scheme. Its strong convergence with order $\tfrac12$ is classical when the coefficients are globally Lipschitz. Many models in applications are not: Langevin dynamics with confining potentials, stochastic Ginzburg–Landau equations, and population or volatility models have drifts such as $\mu(x)=x-x^3$ that grow superlinearly.

For such drifts the explicit Euler scheme fails. Hutzenthaler, Jentzen and Kloeden showed in 2011 (Proc. R. Soc. A 467) that its absolute moments diverge to infinity whenever the drift or the diffusion grows superlinearly, so it does not converge in $L^p$. Implicit schemes do converge (Higham, Mao and Stuart, SIAM J. Numer. Anal. 40, 2002), but each step requires solving a nonlinear equation.

The paper of this mission (Hutzenthaler, Jentzen and Kloeden, Ann. Appl. Probab. 22(4), 2012) introduces a tamed Euler scheme: an explicit method that costs the same as the Euler scheme, modified by a second-order term in the drift. It proves strong convergence with order $\tfrac12$ under a one-sided Lipschitz drift whose derivative grows at most polynomially. The scheme started a line of work on tamed and truncated methods, among them Sabanis's schemes that tame drift and diffusion together for superlinearly growing diffusion coefficients (Ann. Appl. Probab. 26(4), 2016), formalized on this platform in the series "Euler Approximations with Varying Coefficients".

Setting

Fix $T\in(0,\infty)$ and $d,m\in\mathbb N=\{1,2,\dots\}$. Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space with a filtration $(\mathcal F_t)$, and let $W$ be an $m$-dimensional standard $(\mathcal F_t)$-Brownian motion. On $\mathbb R^k$, $\|v\|$ is the Euclidean norm and $\langle v,w\rangle$ the inner product. For a matrix $A$, $\|A\|=\sup_{\|v\|\le1}\|Av\|$ is the operator norm.

The initial value $\xi:\Omega\to\mathbb R^d$ is $\mathcal F_0$-measurable with $\mathbb E\|\xi\|^p<\infty$ for every $p\ge1$. The drift $\mu:\mathbb R^d\to\mathbb R^d$ is continuously differentiable and the diffusion is $\sigma:\mathbb R^d\to\mathbb R^{d\times m}$. There is one constant $c>0$ with

$$\|\mu'(x)\|\le c(1+\|x\|^c),\qquad \|\sigma(x)-\sigma(y)\|\le c\|x-y\|,\qquad \langle x-y,\mu(x)-\mu(y)\rangle\le c\|x-y\|^2$$

for all $x,y$. The exact solution $X$ is an adapted process with continuous paths and

$$X_t=\xi+\int_0^t\mu(X_s)\,ds+\int_0^t\sigma(X_s)\,dW_s,\qquad t\in[0,T],\ \mathbb P\text{-a.s.}$$

For $N\in\mathbb N$, let $\Delta W^N_n=W_{(n+1)T/N}-W_{nT/N}$. The tamed Euler scheme is $Y^N_0=\xi$ and

$$Y^N_{n+1}=Y^N_n+\frac{\tfrac TN\,\mu(Y^N_n)}{1+\tfrac TN\|\mu(Y^N_n)\|}+\sigma(Y^N_n)\,\Delta W^N_n,\qquad n\in\{0,\dots,N-1\}.$$

On $t\in[nT/N,(n+1)T/N]$ its interpolation is

$$\bar Y^N_t=Y^N_n+\frac{(t-nT/N)\,\mu(Y^N_n)}{1+\tfrac TN\|\mu(Y^N_n)\|}+\sigma(Y^N_n)(W_t-W_{nT/N}).$$

In Lean, states live in EthierKurtz.SDEState d, $\sigma$ takes values in Matrix (Fin d) (Fin m) ℝ, the standing hypotheses are the structures Coefficients and Setting, and the scheme is Y, Ybar, all in the namespace TamedEuler.Convergence.

Formalization targets

Goal: Theorem 1.1

There is a family $C_p\in[0,\infty)$, $p\in[1,\infty)$, such that for every solution $X$

$$\Big(\mathbb E\Big[\sup_{t\in[0,T]}\|X_t-\bar Y^N_t\|^p\Big]\Big)^{1/p}\le C_p\,N^{-1/2}\qquad\text{for all }N\in\mathbb N,\ p\in[1,\infty).$$

The constants are left unspecified; only the order $\tfrac12$ is asserted.

Milestones: Lemmas 3.1–3.10

These are the ten lemmas the proof rests on, in the paper's order:

1. the pathwise dominator lemma $\mathbb 1_{\Omega^N_n}\|Y^N_n\|\le D^N_n$ (3.1);
2. Gaussian and Brownian exponential moments (3.2, 3.3, 3.4);
3. moments of the dominating processes $D^N_n$ (3.5);
4. the decay of $\mathbb P[(\Omega^N_N)^c]$ faster than every power of $N$ (3.6);
5. continuous- and discrete-time Burkholder–Davis–Gundy inequalities with constant $p$ (3.7, 3.8);
6. the uniform moment bounds $\sup_N\sup_{n\le N}\mathbb E\|Y^N_n\|^p<\infty$ (3.9), and the same for $\mu(Y^N_n)$ and $\sigma(Y^N_n)$ (3.10).

Significance

The theorem gives an explicit scheme whose cost per step is the Euler cost and whose strong error is $O(N^{-1/2})$ in every $L^p$, uniformly in time, for the superlinear drifts on which the explicit Euler scheme diverges. Strong error bounds of this kind are what multilevel Monte Carlo (Giles 2008) needs, as the paper notes on p. 3: its complexity analysis requires strong convergence of the coarse and fine levels, and the explicit Euler scheme supplies none for these equations. The moment bound of Lemma 3.9 answers, for the tamed scheme, the open problem Higham, Mao and Stuart formulated in 2002 on when moment bounds hold for explicit methods (quoted on p. 8).

The result is proved in the paper; it has not been formalized. The mission formalizes the statement, its ten lemmas and the scheme. The dominator construction (13)–(14) is a pathwise argument that can be checked independently of the probability. The two Burkholder–Davis–Gundy inequalities with the explicit constant $p$ are reusable tools for any numerical analysis of SDEs.

Difficulty

Once the moments of $Y^N_n$ are bounded uniformly in $N$, the convergence proof follows the globally Lipschitz pattern: an Itô or Gronwall argument on $X-\bar Y^N$. The difficulty is the moment bound itself. The obvious approach is a Gronwall recursion for $\mathbb E\|Y^N_{n+1}\|^p$ in terms of $\mathbb E\|Y^N_n\|^p$. For superlinear $\mu$ it does not close: the term $\|\mu(Y^N_n)\|^2(T/N)^2$ grows faster than $\|Y^N_n\|^2$, and for the untamed scheme the moments do in fact diverge. A newcomer's first idea, using the one-sided Lipschitz bound in expectation, fails for the same reason. The paper instead dominates the scheme pathwise on events $\Omega^N_n$ and controls the rare complement separately (Lemmas 3.1, 3.5, 3.6).

Formalization scope

The Lean development commits to the following conventions.

• Normal filtration. Read as a right-continuous filtration (ℱ.IsRightContinuous) together with adaptedness to its $\mathbb P$-completion, which is how the published SabanisEuler.Shared.IsSolution treats completeness.
• Brownian motion. SabanisEuler.Shared.IsWienerMartingale, defined on $[0,\infty)$ rather than $[0,T]$; this is the usual extension. Time is ℝ≥0.
• The solution $X$. Any process satisfying the published IsSolution relation, whose stochastic integral is the Ethier–Kurtz Brownian Itô-integral relation. Existence and uniqueness are cited by the paper, not claimed. $\sigma$ enters IsSolution entrywise through toDiffusion. Every norm of $\sigma$ in a hypothesis or conclusion is the operator norm opNorm.
• The constant $c$. One real $c>0$ is both constant and exponent; $\|x\|^c$ and $N^{1/(2c)}$ are real powers.
• Indices. $\mathbb N=\{1,2,\dots\}$: every statement has $N\ge1$ and $n\le N$, and $d,m\ge1$.
• Interpolation cell. In (10), $t$ uses the cell $n=\min(\lfloor tN/T\rfloor,N-1)$, so $t=T$ uses the last cell.
• (13) and (14). The supremum over $u$ in (13) is a finite maximum. The suprema in (14) are written "for all $k<n$", so $\Omega^N_0=\Omega$.
• Moments. Every expectation, $L^p$ norm and "$<\infty$" is stated in $[0,\infty]$ with lintegral or eLpNorm, never as a Bochner integral that could default to $0$.
• Lemma 3.1. Stated pathwise for every $\omega$ and an arbitrary path $W$.
• Lemma 3.7. The published Itô relation demands pathwise square-integrability of the integrand. This is stronger than the printed almost-sure condition, and the deviation is disclosed.

A trivializing formalization is ruled out: the scheme is (8) exactly, with only the drift tamed and the step size $T/N$. The error is taken against the same Brownian path that drives $X$. The setting is satisfiable for the paper's example $\mu(x)=x-x^3$, $\sigma(x)=x$ with $c=3$ (checked in a sorry-free verification file, given any Brownian motion). Replacing the Itô integral by a postulated operator or a pathwise integral is not admitted.

A complete development needs:

• Gaussian exponential moments;
• discrete and continuous BDG inequalities with explicit constants for the Ethier–Kurtz Itô integral;
• an Itô-type or Gronwall argument for $X-\bar Y^N$.

The BDG inequalities and the Gaussian moment identity are reusable beyond this mission. Contributions to any lemma, or to the stochastic-calculus infrastructure underneath, are welcome.

Selected references

• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong convergence of an explicit numerical method for SDEs with nonglobally Lipschitz continuous coefficients, Ann. Appl. Probab. 22(4), 1611–1641, 2012. https://arxiv.org/abs/1010.3756 (DOI 10.1214/11-AAP803)
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong and weak divergence in finite time of Euler's method for stochastic differential equations with non-globally Lipschitz continuous coefficients, Proc. R. Soc. A 467, 1563–1576, 2011. https://doi.org/10.1098/rspa.2010.0348
• D. J. Higham, X. Mao, A. M. Stuart, Strong convergence of Euler-type methods for nonlinear stochastic differential equations, SIAM J. Numer. Anal. 40(3), 1041–1063, 2002. https://doi.org/10.1137/S0036142901389530
• S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4), 2083–2105, 2016. https://arxiv.org/abs/1308.1796
• X. Mao, Stochastic Differential Equations and Their Applications, Horwood, 1997 (Theorem 2.4.1: existence and uniqueness, cited on p. 2). https://mathscinet.ams.org/mathscinet-getitem?mr=1475218
• M. B. Giles, Multilevel Monte Carlo path simulation, Oper. Res. 56, 607–617, 2008. https://doi.org/10.1287/opre.1070.0496