Probability

Motivation

Sums of independent random matrices appear wherever a large matrix is built from random pieces: sample covariance matrices in statistics, random sparsification and sampling in numerical linear algebra, random graphs and their Laplacians, and compressed sensing. The basic question is how far the largest eigenvalue of such a sum can stray above its typical value. For sums of independent real random variables the answer is given by the classical inequalities of Chernoff, Hoeffding and Bernstein, all derived by the Laplace transform method: bound the tail by the moment generating function, and use independence to factor the moment generating function of the sum.

Ahlswede and Winter (2002) showed that a matrix analogue of the Laplace transform method exists, and Oliveira (2010) refined the starting inequality. Tropp's paper (arXiv:1004.4389) replaced the Ahlswede–Winter decoupling step by a consequence of Lieb's concavity theorem (Lieb 1973) and obtained a single master tail bound from which matrix versions of the Gaussian-series, Chernoff, Bernstein and Azuma inequalities follow with sharp variance parameters. This mission formalizes that master bound, the first of five missions covering the paper.

Timeline:

• 1973: Lieb proves concavity of $A\mapsto \operatorname{tr}\exp(H+\log A)$ on positive-definite matrices; Epstein gives a second proof (Epstein 1973).
• 2002: Ahlswede and Winter introduce the matrix Laplace transform method, decoupling summands with the Golden–Thompson inequality.
• 2010: Oliveira's variant of the matrix Laplace transform bound.
• 2010–2012: Tropp derives the master bound for independent sums from Lieb's theorem (journal version: Found. Comput. Math. 12 (2012)); in 2011 he also derives Lieb's theorem from the joint convexity of quantum relative entropy (arXiv:1101.1070).

Setting

All matrices are $d\times d$ arrays of complex numbers with $d\ge1$. A matrix $A$ is self-adjoint (Hermitian) when $A=A^*$; it then has real eigenvalues, and $\lambda_{\max}(A)$ denotes the largest one. For a function $f:\mathbb R\to\mathbb R$ and a self-adjoint $A=Q\Lambda Q^*$ with $Q$ unitary and $\Lambda$ diagonal, $f(A):=Qf(\Lambda)Q^*$. This defines the matrix exponential $e^{A}$ of every self-adjoint matrix and the matrix logarithm $\log A$ of every positive-definite matrix, with $\log(e^A)=A$. The trace exponential is $A\mapsto\operatorname{tr}e^{A}$.

A random self-adjoint matrix is a measurable map $X$ from a probability space $(\Omega,\mathcal F,\mathbb P)$ to the self-adjoint matrices. Its expectation $\mathbb E X$ is the matrix of the expectations of its entries. A finite sequence $X_1,\dots,X_n$ is independent when the maps are jointly independent. The matrix moment generating function and matrix cumulant generating function of $X$ are

$$M_X(\theta):=\mathbb E\,e^{\theta X},\qquad \Xi_X(\theta):=\log\mathbb E\,e^{\theta X},\qquad\theta\in\mathbb R,$$

which may fail to exist for some $\theta$. In the Lean development these objects are lambdaMax, mexp, mlog, trExp and mean in the namespace MatrixTail.Master.

Formalization targets

Goal: the master tail bound (Theorem 3.6)

For independent random self-adjoint matrices $X_1,\dots,X_n$ and every $t\in\mathbb R$,

$$\mathbb P\Bigl\{\lambda_{\max}\Bigl(\sum_k X_k\Bigr)\ge t\Bigr\}\le\inf_{\theta>0}\Bigl\{e^{-\theta t}\cdot\operatorname{tr}\exp\Bigl(\sum_k\log\mathbb E\,e^{\theta X_k}\Bigr)\Bigr\}.$$

It contains no constants and no assumption beyond independence: every later inequality of the paper specializes it.

Milestones

1. Proposition 3.1 (Laplace transform method): $\mathbb P\{\lambda_{\max}(Y)\ge t\}\le\inf_{\theta>0}\{e^{-\theta t}\,\mathbb E\operatorname{tr}e^{\theta Y}\}$.
2. Theorem 3.2 (Lieb): for fixed self-adjoint $H$, $A\mapsto\operatorname{tr}\exp(H+\log A)$ is concave on the positive-definite cone.
3. Corollary 3.3: $\mathbb E\operatorname{tr}\exp(H+X)\le\operatorname{tr}\exp(H+\log\mathbb E\,e^{X})$.
4. Lemma 3.4 (subadditivity of matrix cgfs): $\mathbb E\operatorname{tr}\exp(\sum_k\theta X_k)\le\operatorname{tr}\exp(\sum_k\log\mathbb E\,e^{\theta X_k})$ for $\theta\in\mathbb R$.

Significance

The master bound reduces every tail estimate for $\lambda_{\max}$ of an independent sum to semidefinite bounds on the individual cumulant generating functions. The paper's matrix Gaussian and Rademacher series bound, matrix Chernoff inequality and matrix Bernstein inequality are each one such bound away from it, and the matrix Bernstein inequality in particular is a standard tool in randomized numerical linear algebra, matrix completion and covariance estimation. Missions II–IV of this series take the master bound as their first milestone.

All results here are proved in the literature. What remains is formalization: none of Lieb's concavity theorem, the matrix Laplace transform bound or the subadditivity of matrix cumulant generating functions is in Mathlib, and a machine-checked Lieb theorem would be reusable throughout quantum information theory (strong subadditivity of entropy, joint convexity of relative entropy).

Difficulty

The scalar argument factors $\mathbb E\exp(\sum_k\theta X_k)=\prod_k\mathbb E\,e^{\theta X_k}$, which needs $e^{a+b}=e^ae^b$. For non-commuting matrices $e^{A+B}\ne e^Ae^B$, so this step fails. The Golden–Thompson inequality $\operatorname{tr}e^{A+H}\le\operatorname{tr}(e^Ae^H)$ handles two summands but its three-matrix analogue is false, so it does not iterate. Lieb's concavity theorem is the deep input; it does not follow from elementary properties of the exponential, which is neither operator monotone nor operator convex. On the formal side, the matrix functional calculus of Mathlib carries little of the trace-function theory the statements rely on.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d] wherever $\lambda_{\max}$ appears; for $d=0$ the largest eigenvalue would be $0$ and the bound would fail at $t\le0$. Exponential and logarithm are Mathlib's continuous functional calculus cfc. Random matrices are measurable maps for the Borel σ-algebra on the entries, independence is iIndepFun, and P is a probability measure. Expectation is entrywise.

The paper's standing assumption that expectations exist is made explicit and only where an expectation is taken: every entry of $e^{\theta X_k}$ is integrable for the $\theta$ in question. The infimum over $\theta>0$ is stated as the bound for every $\theta>0$ at which the moment generating functions exist; since an inequality $p\le\inf_\theta F(\theta)$ is equivalent to $p\le F(\theta)$ for every $\theta$, and the paper treats a non-existent moment generating function as $+\infty$, this is exact. A real-valued infimum over $\theta$, or dropping the integrability hypotheses, would make the statements trivially true through Lean's default values ($\inf$ of an unbounded set and the integral of a non-integrable function are $0$); the formalization rules both out.

Useful infrastructure beyond this mission: trace inequalities for cfc on Hermitian matrices, monotonicity of the trace exponential in the semidefinite order, and Lieb's concavity theorem itself. Contributions of any of these as standalone lemmas are welcome.

Selected references

• J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, arXiv:1004.4389v7 (2011); Found. Comput. Math. 12 (2012) 389–434. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
• R. Ahlswede and A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48(3) (2002) 569–579. https://arxiv.org/abs/quant-ph/0012127
• R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X
• H. Epstein, Remarks on two theorems of E. Lieb, Comm. Math. Phys. 31 (1973) 317–325. https://doi.org/10.1007/BF01646492
• J. A. Tropp, From joint convexity of quantum relative entropy to a concavity theorem of Lieb, Proc. Amer. Math. Soc. 140 (2012) 1757–1760. https://arxiv.org/abs/1101.1070

Motivation

Online learning and stochastic learning ask different questions. An online learner faces an arbitrary sequence of loss functions and is judged by its regret: the excess of its cumulative loss over that of the best fixed hypothesis in hindsight. A stochastic learner receives independent samples from an unknown distribution and is judged by the risk of a single hypothesis it outputs. Regret bounds hold without any probabilistic assumption, so they are strong guarantees; risk bounds are what statistical learning and stochastic optimization actually need.

The online-to-batch conversion connects the two: run any online learner on losses built from i.i.d. samples and output either the average of its predictions or one prediction chosen at random. The expected excess risk of the output is then at most the expected regret divided by the number of rounds. A general form of the conversion is due to Cesa-Bianchi, Conconi and Gentile (IEEE Trans. Inf. Theory 2004). Shalev-Shwartz's survey (Found. Trends Mach. Learn. 2011) states it in expectation, in Vapnik's general setting of learning, as Theorem 5.1 and Corollary 5.2 (§5, pp. 186–189). Every stochastic-gradient analysis that goes "regret bound, then online-to-batch" rests on this statement.

Setting

Fix a dimension $d$ and a hypothesis class $S \subseteq \mathbb R^d$. Examples range over a measurable space $\Psi$ and are drawn from a probability distribution $Q$ on $\Psi$, which the learner does not know. A cost $c(w,\psi) \ge 0$ measures how badly hypothesis $w\in S$ does on example $\psi$, and the risk of $w$ is

$$C(w) = \mathbb E_{\psi\sim Q}\,[c(w,\psi)].$$

This is Vapnik's general setting of learning (Definition 5.1); supervised classification, regression and stochastic convex optimization are special cases.

The conversion draws $\psi_0,\dots,\psi_{T-1}$ independently from $Q$ and runs an online learner on the losses $f_t(w) = c(w,\psi_t)$. Its prediction in round $t$, $w_t\in S$, may depend only on $\psi_0,\dots,\psi_{t-1}$. The output $\bar w$ is either the average $\frac1T\sum_t w_t$ or the randomized choice $w_r$, with $r$ uniform on the $T$ rounds and independent of the sample.

Formalization targets

Goal: Corollary 5.2

For every comparator $u\in S$, under the conditions of Theorem 5.1,

$$\mathbb E\big[C(\bar w)\big] - C(u) \;\le\; \mathbb E\Big[\frac1T\sum_{t}\big(f_t(w_t)-f_t(u)\big)\Big],$$

for the randomized output, and for the averaged output when $S$ and $C$ are convex. The right side is the expected regret divided by $T$. The statement contains no constant: it is an exact reduction, valid for every online learner.

Milestones

1. The round-$t$ identity $\mathbb E[c(w_t,\psi_t)] = \mathbb E[C(w_t)]$ (§5, p. 188).
2. Equation (5.1): $\mathbb E\big[\frac1T\sum_t C(w_t)\big] = \mathbb E\big[\frac1T\sum_t c(w_t,\psi_t)\big]$.
3. Theorem 5.1: $\mathbb E[C(\bar w)] = \mathbb E\big[\frac1T\sum_t f_t(w_t)\big]$ for randomization, and $\le$ for averaging when $C$ is convex.
4. The comparator identity $\mathbb E\big[\frac1T\sum_t c(u,\psi_t)\big] = C(u)$ (p. 189).

Significance

Corollary 5.2 makes every regret bound a risk bound. Combined with the $O(\sqrt T)$ regret of online gradient descent or online mirror descent, it gives the $O(1/\sqrt T)$ excess-risk rate of stochastic gradient methods for convex Lipschitz problems; combined with logarithmic regret for strongly convex losses, it gives $O(\log T / T)$ rates. The survey's own "Stochastic Online Mirror Descent" box (p. 189) is exactly this composition.

The result is proved in the paper. What this mission adds is a machine-checked version in a measure-theoretic model with honest non-anticipation and a genuine model of the randomized output. The platform has a related statement, Mohri, Rostamizadeh and Talwalkar's Theorem 8.15 (FoundationsML.OnlineLearning.online_to_batch_conversion), which is a high-probability bound for bounded convex losses in supervised learning; it is a different statement and neither implies the other. The expectation form here is the one stochastic-optimization arguments use.

Difficulty

The result is short on paper; the formal content is the conditional-expectation step. The prediction $w_t$ is a random variable built from $\psi_0,\dots,\psi_{t-1}$, while $\psi_t$ is a fresh draw, so $\mathbb E[c(w_t,\psi_t)]$ must be computed by integrating out $\psi_t$ first, which means a Fubini–Tonelli argument on a product of $T$ copies of $Q$ split into the past, the present and the future of round $t$. The first idea, that $c(w_t,\psi_t)$ has the same law as $c(w,\psi)$ for a fixed $w$, is wrong: $w_t$ is random. The identity also fails as soon as $w_t$ may look at $\psi_t$ (take $w_t$ a minimizer of $c(\cdot,\psi_t)$), so the argument must use the information structure, not only the marginal laws. The averaging part additionally needs Jensen's inequality for $C$ and the measurability of $C$ as a function of the hypothesis.

Formalization scope

• Hypotheses live in EuclideanSpace ℝ (Fin d) with $S$ a set, because averaging needs a vector space. Rounds are numbered $0,\dots,T-1$, and $T \ge 1$.
• The sample is ψ : Fin T → Ψ under Measure.pi (fun _ => Q), with Q a probability measure: independent draws from $Q$.
• The online learner is a family A t : (Fin t → Ψ) → ℝ^d of measurable maps with values in $S$, so non-anticipation holds by typing: $w_t = A_t(\psi_0,\dots,\psi_{t-1})$. The learner may read the examples, not only the losses; this class contains the paper's learners, so the statements are at least as strong.
• The randomized output is modelled on the product of the sample law with the uniform law on Fin T. The expectation over $r$ is not replaced by the average over rounds (that replacement is the first line of the proof).
• Standing assumptions on the cost (footnote 1, made explicit): $c\ge0$ on $S\times\Psi$, jointly measurable on $S\times\Psi$, and $c(w,\cdot)$ integrable for each $w\in S$, so that $C(w)$ is a real number.
• Added hypotheses, each recorded in the statements: $u\in S$ for "$u$ any vector"; $S$ convex for the averaged output, so that $\bar w\in S$; for the averaged output, the online losses $c(w_t,\psi_t)$ have finite expectation (otherwise the paper's inequality has an infinite right side, which Lean's Bochner integral would read as $0$).
• No $O(\cdot)$ appears in this section, so there are no constants to instantiate, and no erratum was found.
• A trivializing formalization is ruled out: a prediction allowed to depend on the whole sample would make the identity false, and integrals of non-integrable functions, which Lean evaluates to $0$, appear only on sides where the hypotheses or nonnegativity make them meaningful.
• Out of scope: the high-probability version (footnote 2, p. 187), empirical risk minimization (p. 187), and the "Stochastic Online Mirror Descent" box (p. 189), which carries no theorem.

Infrastructure needed: Tonelli/Fubini on finite products split at a coordinate (Mathlib's Measure.pi), measurability of parametric integrals, and Jensen's inequality for a convex function of a finite average. The round-$t$ identity is reusable for any non-anticipating stochastic process; contributions of proofs of any milestone are welcome.

Selected references

• S. Shalev-Shwartz, Online Learning and Online Convex Optimization, Foundations and Trends in Machine Learning 4(2), 107–194, 2011. https://doi.org/10.1561/2200000018
• N. Cesa-Bianchi, A. Conconi, C. Gentile, On the generalization ability of on-line learning algorithms, IEEE Transactions on Information Theory 50(9), 2050–2057, 2004. https://doi.org/10.1109/TIT.2004.833339
• V. Vapnik, Statistical Learning Theory, Wiley, 1998. ISBN 978-0-471-03003-4

Motivation

A directed polymer in a random environment is a random up-right lattice path whose law is reweighted by random site weights. Its free energy, the logarithm of the partition function, is believed to belong to the Kardar–Parisi–Zhang (KPZ) universality class: for a path of length of order $N$, the free energy fluctuates on the scale $N^{1/3}$ and the path wanders on the scale $N^{2/3}$. For zero-temperature analogues (last-passage percolation with exponential or geometric weights) these exponents were established through exact formulas from random matrix theory (Johansson 2000) and later through a probabilistic coupling argument based on the Burke property of queues (Balázs–Cator–Seppäläinen 2006).

For directed polymers at positive temperature no model with the KPZ exponents was known until Seppäläinen (arXiv:0911.2446, Ann. Probab. 2012) introduced the log-gamma polymer, whose weights are reciprocals of gamma variables, and proved that its free energy has variance of order $N^{2/3}$ in the characteristic direction. The model has since become a basic exactly solvable polymer:

• 2009: Seppäläinen, the log-gamma polymer with boundary conditions; variance bounds of order $N^{2/3}$ and path fluctuation exponent $2/3$, by a Burke property and a variance identity.
• 2013: Borodin, Corwin and Remenik, Fredholm determinant formula and Tracy–Widom GUE limit of the free energy, for a range of parameters.
• 2014: Corwin, O'Connell, Seppäläinen and Zygouras, Tropical combinatorics and Whittaker functions, an exact formula for the law of the partition function via the geometric RSK correspondence.

The present mission formalizes the 2009 variance theorem, which needs neither of the later exact formulas.

Setting

Sites are $\mathbb Z_+^2=\{0,1,2,\dots\}^2$ and $\mathbb N=\{1,2,\dots\}$. A weight configuration assigns a positive number $Y_{i,j}$ to each site. On the axes, $U_{i,0}=Y_{i,0}$ and $V_{0,j}=Y_{0,j}$ for $i,j\in\mathbb N$ are the boundary weights, and $Y_{i,j}$, $i,j\in\mathbb N$, are the bulk weights.

An up-right path from $(0,0)$ to $(m,n)$ is a sequence $x_0=(0,0),x_1,\dots,x_{m+n}=(m,n)$ whose steps are $(1,0)$ or $(0,1)$. The partition function is

$$Z_{m,n}=\sum_{x}\prod_{k=1}^{m+n}Y_{x_k},$$

the weight of the origin excluded, $Z_{0,0}=1$. The quenched polymer measure gives the path $x$ probability $Q^\omega_{m,n}(x)=Z_{m,n}^{-1}\prod_{k=1}^{m+n}Y_{x_k}$, and the annealed measure is its average $P_{m,n}=\mathbb E\,Q^\omega_{m,n}$ over the environment. The exit points $\xi_x$ and $\xi_y$ are the numbers of initial steps the path takes along the $x$-axis and along the $y$-axis.

Assumption (2.4). Fix $0<\theta<\mu$. The weights $\{U_{i,0},V_{0,j},Y_{i,j}: i,j\in\mathbb N\}$ are independent with

$$U_{i,0}^{-1}\sim\mathrm{Gamma}(\theta,1),\qquad V_{0,j}^{-1}\sim\mathrm{Gamma}(\mu-\theta,1),\qquad Y_{i,j}^{-1}\sim\mathrm{Gamma}(\mu,1).$$

Let $\Psi_0=(\log\Gamma)'$ and $\Psi_1=\Psi_0'$ be the digamma and trigamma functions. The characteristic direction is $(\Psi_1(\mu-\theta),\Psi_1(\theta))$. For a real scaling parameter $N$ and a constant $\gamma$, the endpoint satisfies

$$|m-N\Psi_1(\mu-\theta)|\le\gamma N^{2/3}\quad\text{and}\quad|n-N\Psi_1(\theta)|\le\gamma N^{2/3}\qquad(2.6).$$

Formalization targets

Goal: Theorem 2.1

There are constants $0<C_1,C_2<\infty$ and $N_0$, depending on $\theta,\mu,\gamma$, such that under (2.4) and (2.6)

$$\mathrm{Var}(\log Z_{m,n})\le C_2N^{2/3}\quad(N\ge1),\qquad C_1N^{2/3}\le\mathrm{Var}(\log Z_{m,n})\quad(N\ge N_0).$$

Milestones

The upper bound runs through the Burke property and the variance identity:

• Lemma 3.1 (monotonicity of the recursion (3.2)), Lemma 3.2 (gamma reversibility), Theorem 3.3 (Burke property), the mean (2.5), $\mathbb E\log Z_{m,n}=-m\Psi_0(\theta)-n\Psi_0(\mu-\theta)$.
• Theorem 3.7, the variance identity

$$\mathrm{Var}[\log Z_{m,n}]=n\Psi_1(\mu-\theta)-m\Psi_1(\theta)+2E_{m,n}\Bigl[\sum_{i=1}^{\xi_x}L(\theta,Y_{i,0}^{-1})\Bigr].$$

• Lemma 4.1 (variance comparison in $\theta$), Lemma 4.2, the exit-point bound (4.32) $E(\xi_x)\le CN^{2/3}$, Lemma 4.3 (quenched exit-point tails).

The lower bound runs through partition-function comparisons:

• Lemma 5.1, Lemma 5.4 (coupling), Lemma 5.5(i), Proposition 5.3 ($\lim_{\delta\searrow0}\varlimsup_NP\{1\le\xi_x\le\delta N^{2/3}\}=0$), Corollary 5.6 ($\mathrm{Var}\ge cN^{2/3}$, $c>0$).

Significance

The result. Theorem 2.1 was the first proof of the KPZ fluctuation exponent $1/3$ for a directed polymer at positive temperature. Its upper bound also yields a strong law of large numbers for $N^{-1}\log Z_{m,n}$ (2.7) and, with Theorem 3.3, a central limit theorem off the characteristic direction (Corollary 2.2). The exit-point estimates of Sections 4 and 5 give the path fluctuation exponent $2/3$ (Theorem 2.3) and are reused for the polymer without boundaries and the point-to-line polymer (Theorems 2.4–2.6).

Formalizing it. The theorem has been proved since 2009; no formal proof of it in a proof assistant is known. A formalization checks a proof with many interacting estimates and two corrected slips (below). The definitions made here (the lattice-path partition function, the inverse-gamma environment, the recursion (3.2), exit points, quenched and annealed measures) are the base for later missions on Theorems 2.3–2.7 of the same paper. Lemma 3.2 contains a gamma-distribution characterization (Lukacs' theorem) of independent interest.

Difficulty

The obvious route to a variance bound, a martingale decomposition of $\log Z_{m,n}$ over the $mn$ independent weights, gives only $\mathrm{Var}=O(m+n)$, i.e. order $N$; it cannot see the cancellation that produces $N^{2/3}$. The order $N^{2/3}$ is specific to the characteristic direction: off it, $\log Z_{m,n}$ satisfies a central limit theorem with variance of larger order (Corollary 2.2), so any argument must use the exact relation between the boundary parameters $\theta,\mu-\theta$ and the endpoint $(m,n)$. The upper bound requires controlling the annealed exit point $E(\xi_x)$ at the scale $N^{2/3}$, with tail estimates whose constants are uniform in the parameters. The lower bound is a separate statement: the path must not exit an axis at distance $o(N^{2/3})$ from the origin with non-vanishing probability, which no upper-bound estimate implies.

Formalization scope

Source: arXiv:0911.2446v4 (26 Aug 2015, revised version); its printed page numbers equal the PDF's. All declarations are in the namespace LogGammaPolymer.Variance.

• Sites are ℕ × ℕ; a path is a step sequence with a fixed number of east steps; $Z$ is a finite sum over these paths with the starting weight excluded. The environment Env θ μ P bundles one weight family Y : ℕ × ℕ → Ω → ℝ, measurability, mutual independence of every weight off the origin, and the three laws as images under $y\mapsto y^{-1}$ equal to Mathlib's gammaMeasure (shape, rate $1$). Positivity of the weights is not assumed pointwise in the probabilistic statements; it holds almost surely. The deterministic lemmas (3.1, 5.1, 5.4) are stated for every weight function positive off the origin.
• $N$ is real and $N^{2/3}$ is a real power. Variances use Mathlib's variance, and every upper bound or identity also asserts $\log Z_{m,n}\in L^2$ (or integrability of the averaged quantity), so that the junk value $0$ of variance and of the Bochner integral cannot satisfy it.
• Constants come after the parameters $(\theta,\mu,\gamma)$ and before the probability space (universe Type), the environment, $N$ and $(m,n)$. Upper limits in $N$ are stated as "for every $\eta>0$ there is $N_0$ with the bound $+\eta$ for $N\ge N_0$". The compact-set uniformity of Lemmas 4.1, 4.3 and (4.32) is formalized. The remark after Theorem 2.1 on uniform constants is not.
• Corrected slips. (i) Theorem 2.1 prints the lower bound for all $N\ge1$. It fails at $N=1$, $\theta=1$, $\mu=2$, $\gamma=2$ with $(m,n)=(0,0)$, where the variance is $0$. The lower bound is stated for $N\ge N_0$, which is what Corollary 5.6 proves. (ii) The "only if" of Lemma 3.2 fails for the constants $U=V=1$, $Y=1/2$. The hypothesis "$U$ is not a.s. constant" is added. (iii) Corollary 5.6 states $c>0$ explicitly.
• Theorem 3.3 is stated for down-right paths that coincide with the axes outside a finite portion. The paper reduces the general case to these.
• Not included: Lemma 3.5 (reversal), Proposition 3.4, Lemma 5.5(ii).

A formalization in which $Z$ includes the origin's weight, the laws are not exactly the inverse gammas with shapes $\theta,\mu-\theta,\mu$ and rate $1$, independence is dropped, $C_1=0$ is allowed, or the constants depend on the environment or on $N$ does not state Theorem 2.1.

Needed infrastructure: gamma–beta algebra and a Lukacs-type characterization, independence of finite families built by the recursion (3.2), differentiation of expectations in the shape parameter, and moment bounds for sums of i.i.d. variables. All of these are reusable beyond this mission. Proofs of any milestone, and of supporting lemmas such as (3.3)–(3.4), are welcome.

Selected references

• T. Seppäläinen, Scaling for a one-dimensional directed polymer with boundary conditions, Ann. Probab. 40 (2012) 19–73; revised version arXiv:0911.2446v4. https://arxiv.org/abs/0911.2446
• K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209 (2000) 437–476. https://arxiv.org/abs/math/9903134
• M. Balázs, E. Cator, T. Seppäläinen, Cube root fluctuations for the corner growth model associated to the exclusion process, Electron. J. Probab. 11 (2006) 1094–1132. https://arxiv.org/abs/math/0603306
• I. Corwin, N. O'Connell, T. Seppäläinen, N. Zygouras, Tropical combinatorics and Whittaker functions, Duke Math. J. 163 (2014) 513–563. https://arxiv.org/abs/1110.3489
• A. Borodin, I. Corwin, D. Remenik, Log-gamma polymer free energy fluctuations via a Fredholm determinant identity, Comm. Math. Phys. 324 (2013) 215–232. https://arxiv.org/abs/1206.4573
• E. Lukacs, A characterization of the gamma distribution, Ann. Math. Statist. 26 (1955) 319–324. https://doi.org/10.1214/aoms/1177728549

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).