Probability

Motivation

A probability model $\mu$ for a risk quantity, such as the reserve process of an insurer or the path of a queue, is usually chosen for tractability or fitted to limited data, and the true law of the system is unknown. Distributional model risk asks how large a probability of interest could be if the true law were any model "close" to $\mu$. When closeness is measured by an optimal transport cost rather than a likelihood ratio, the competing models may put mass where $\mu$ puts none, which is the situation for rare events such as ruin or buffer overflow: the event of interest often lies outside the support of the baseline.

Blanchet and Murthy (arXiv:1604.01446, Mathematics of Operations Research 44(2), 2019) prove strong duality for worst-case expectations over an optimal-transport ball on a general Polish space, with a lower semicontinuous cost. Their §2.4 specializes the duality to worst-case probabilities of a closed set and obtains a closed-form answer: the worst-case probability of $A$ is the baseline probability of an inflated version of $A$. This mission formalizes that result, Theorem 3 of the paper, together with the numbered statements its proof uses.

Setting

Let $S$ be a Polish space with its Borel $\sigma$-algebra, $P(S)$ its probability measures, and $\mu \in P(S)$ the baseline. A cost $c : S \times S \to \mathbb R_+$ satisfies Assumption (A1): it is nonnegative, lower semicontinuous, and $c(x,y) = 0$ if and only if $x = y$.

For $\mu_1, \mu_2 \in P(S)$, a coupling of $\mu_1$ and $\mu_2$ is a probability measure $\pi$ on $S \times S$ with marginals $\mu_1$ and $\mu_2$; $\Pi(\mu_1,\mu_2)$ is the set of couplings, and the optimal transport cost is

$$d_c(\mu_1,\mu_2) = \inf\Big\{\int c\,d\pi : \pi \in \Pi(\mu_1,\mu_2)\Big\}.$$

For a budget $\delta > 0$, the primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S \times S$ with first marginal $\mu$ and $\int c\,d\pi \le \delta$.

Fix a nonempty closed set $A \subseteq S$ and let $c(x,A) = \inf\{c(x,y) : y \in A\}$ be the cheapest cost of moving unit mass from $x$ into $A$. The worst-case probability is

$$I = \sup\{P(A) : d_c(\mu,P) \le \delta\}. \tag{12}$$

Its dual is the univariate problem

$$\inf_{\lambda \ge 0}\Big\{\lambda\delta + E_\mu\big[(1 - \lambda c(X,A))^+\big]\Big\}, \tag{13}$$

and for a minimizer $\lambda^* \in [0,\infty)$ of (13) the paper defines

$$\underline c = \int_{\{c(x,A) < 1/\lambda^*\}} c(x,A)\,d\mu(x), \qquad \overline c = \int_{\{c(x,A) \le 1/\lambda^*\}} c(x,A)\,d\mu(x). \tag{14}$$

Formalization targets

Goal: Theorem 3 (p. 10)

If $\lambda^* \in [0,\infty)$ attains the infimum in (13) and $\underline c = \overline c$, then

$$\sup\{P(A) : d_c(\mu,P) \le \delta\} = \mu\{x : c(x,A) \le 1/\lambda^*\}. \tag{15}$$

Milestones, in the order the proof uses them

1. Coupling form (§2.2, p. 5, for $f = 1_A$): $I = \sup\{\pi(S \times A) : \pi \in \Phi_{\mu,\delta}\}$.
2. Indicator supremum (pp. 8–9): $\sup_{y}\{1_A(y) - \lambda c(x,y)\} = (1 - \lambda c(x,A))^+$ for $\lambda \ge 0$.
3. (13) (p. 9): $I$ equals the infimum in (13).
4. Remark 4, (11) for $f = 1_A$ (p. 8): an $\varepsilon$-optimal plan $\pi_\varepsilon$ satisfies $\int(\varphi_{\lambda^*}(x) - (1_A(y) - \lambda^* c(x,y)))\,d\pi_\varepsilon \le \varepsilon$ and, for $\lambda^* > 0$, $(\delta - \varepsilon/\lambda^*)^+ \le \int c\,d\pi_\varepsilon \le \delta$.
5. Lemma 4 (p. 11): plans $\pi_n \in \Phi_{\mu,\delta}$, $n > 1$, with $\pi_n(C_n) \ge 1 - 1/n$, no cost outside the set $C_n$ of §2.4.1, and $\pi_n(S \times A) \ge I - 2/n$.
6. Lemma 2 (p. 10): $\underline c \le \delta \le \overline c$ if $\lambda^* > 0$ attains (13); $\delta \ge \overline c = \underline c$ if $\lambda^* = 0$ does.

Significance

Theorem 3 converts a supremum over an infinite-dimensional ball of probability measures into a single probability under the baseline: $\mu$ of the set of points that can reach $A$ at cost at most $1/\lambda^*$, where $1/\lambda^*$ is determined by $\delta$ through the one-dimensional function $u \mapsto \int_{\{c(x,A) \le u\}} c(x,A)\,d\mu$. For the cost $c = d$ of a metric this is the baseline probability of the $1/\lambda^*$-neighbourhood of $A$. The paper uses it to compute worst-case ruin probabilities for the Cramér–Lundberg model around a Brownian approximation (§3, §6.1), where $S$ is a path space; the result applies there because nothing in it uses local compactness of $S$.

The result is proved in the paper. As far as the platform's corpus shows, neither it nor the strong duality behind it has been formalized. A formal development produces, beyond Theorem 3: a reusable definition of optimal transport costs with lower semicontinuous costs on Polish spaces; the coupling reformulation of the transport ball, which rests on the existence of optimal transport plans (Villani, Optimal Transport, Theorem 4.1), not in Mathlib; and an $\varepsilon$-optimal-plan argument that avoids assuming a primal optimizer exists.

Difficulty

The heuristic derivation on pp. 9–10 constructs an optimal transport plan that moves each $x$ with $c(x,A) \le 1/\lambda^*$ to a nearest point of $A$ and leaves the others in place. It needs a nearest point to exist and to be selectable measurably, which fails for general closed $A$ in a non-locally-compact space, and it needs a primal optimizer, which need not exist. Theorem 3 assumes neither, so the construction is not a proof. A second point is the boundary level $c(x,A) = 1/\lambda^*$: when $\mu$ charges it, as for atomic baselines, the identity (15) can fail (for $\mu$ a point mass at distance $1$ from $A$ and $\delta < 1$, the worst case is $\delta$, not $1$), and the hypothesis $\underline c = \overline c$ is exactly what excludes this. Measurability is a second obstacle: $x \mapsto c(x,A)$ is an infimum of a lower semicontinuous function over $A$ and in general only universally measurable, so integrals of it are taken against the completion of $\mu$.

Formalization scope

All objects live in the namespace ModelRiskOT.WorstProb. $S$ carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]; $\mu$ is a Measure S with IsProbabilityMeasure; the cost is a real-valued c : S → S → ℝ with (A1) bundled as a structure (nonnegativity, lower semicontinuity on $S \times S$, and $c(x,y) = 0 \iff x = y$). Committed conventions:

• Values in $[0,\infty]$. $d_c$, $I$, the objective of (13), $\underline c$ and $\overline c$ are ℝ≥0∞; integrals are lower Lebesgue integrals and the positive part $(\cdot)^+$ is ENNReal.ofReal. For the universally measurable functions and sets that occur, lower integrals and outer measures agree with the completion of $\mu$, which is the paper's reading (p. 4). No Bochner integral is used.
• The threshold $1/\lambda^*$ is written in multiplied form: $c(x,A) \le 1/\lambda^*$ is $\lambda^* c(x,A) \le 1$, and likewise for the strict inequality and for the sets $C_n$. For $\lambda^* > 0$ this is the printed condition; at $\lambda^* = 0$ it is the whole space, the paper's convention $1/0 = \infty$.
• $d_c$ fixes both marginals; $\Phi_{\mu,\delta}$ fixes only the first.
• $c(x,A)$ is a real infimum over the subtype $A$; every statement assumes $A$ nonempty.
• "$\lambda^*$ attains the infimum in (13)" is $\lambda^* \ge 0$ and $g(\lambda^*) \le g(\lambda)$ for all $\lambda \ge 0$.
• Inequalities $X \ge I - t$ are written $I \le X + t$ in $[0,\infty]$; sequences "$n > 1$" are indexed by $n \in \mathbb N$ with $1 < n$.

A formalization in which the transport ball fixes only the first marginal would contain every probability measure and give $I = 1$ for every nonempty $A$; the definitions here fix both marginals of the couplings in $d_c$, and the hypothesis $\underline c = \overline c$ is kept as stated rather than replaced by continuity of $u \mapsto \int_{\{c(x,A) \le u\}} c(x,A)\,d\mu$.

A complete development needs the existence of optimal couplings for lower semicontinuous costs (tightness and Prokhorov's theorem, available in Mathlib), the strong duality of the paper's Theorem 1 specialized to indicators (milestone 3; a separate mission in this series formalizes Theorem 1 in general), and universal measurability of $c(\cdot,A)$ through projections of Borel sets. The transport-cost definitions and the coupling reformulation are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs that derive (13) from the general strong duality once that is published.

Selected references

• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, arXiv:1604.01446v2, 2017; Mathematics of Operations Research 44(2):565–600, 2019. https://arxiv.org/abs/1604.01446, https://doi.org/10.1287/moor.2018.0936
• C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171:115–166, 2018. https://doi.org/10.1007/s10107-017-1172-1
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (universal measurability, Ch. 7).

Motivation

In classical single-machine stochastic scheduling, $N$ jobs with independent random processing requirements $X_i$ are processed one after another, and the makespan (the completion time of the last job) is the same for every schedule that never idles: it is $X_1+\dots+X_N$. Research therefore concentrated on weighted flow times and rewards. Browne and Yechiali (Operations Research 38(3), 1990, 495–498) studied jobs that deteriorate while they wait: the longer a job is delayed, the more processing it needs. Such models arose in the control of queueing and communication systems (Browne 1988; Browne and Yechiali 1989) and in inventory issuing, where stored items lose quality at item-specific rates. Under deterioration the actual processing times depend on the order, so the makespan, and its expectation, become functions of the schedule, and the basic question is which order minimizes the expected makespan.

Setting

There are $N$ jobs, all available at time $0$, and a single processor. Job $i$ has an initial processing requirement $X_i$, a random variable on a probability space $(\Omega,\mathcal F,P)$: the time needed to complete job $i$ if it is processed first. Under linear deterioration, a job whose processing is delayed until time $t$ needs

$$Y_i(t) = X_i + \alpha_i t,$$

where $\alpha_i>0$ is its deterministic growth rate. A job stops deteriorating once it is put on the processor.

Only nonpreemptive strategies without idling are allowed, so a policy is a permutation $\pi$ of $\{1,\dots,N\}$, with $\pi(i)=j$ meaning that job $j$ is the $i$-th processed. The completion times follow the model: $S_0(\pi)=0$, and the job in position $k$ starts at $S_{k-1}(\pi)$ and takes $Y_{\pi(k)}(S_{k-1}(\pi))$, so

$$S_k(\pi) = S_{k-1}(\pi) + X_{\pi(k)} + \alpha_{\pi(k)} S_{k-1}(\pi), \qquad k = 1,\dots,N.$$

The makespan is $S_N(\pi)$ and the expected makespan is $\mathrm E\,S_N(\pi)$. In Lean these are completionTime X α π k ω, makespan X α π ω and expectedMakespan P X α π in the namespace DeterioratingJobs.Makespan.

The paper's Lemma 1 concerns, for real numbers $\mu_i$ and $\gamma_i$, the sum (1)

$$F_{\mu,\gamma}(\pi) = \sum_{i=1}^{N} \mu_{\pi(i)} \prod_{r=i+1}^{N} \gamma_{\pi(r)},$$

the Lean lemma1Sum μ γ π (empty product $=1$).

Formalization targets

Goal: the expected-makespan index rule (§1, p. 496)

If the $X_i$ are integrable, $\alpha_i>0$, and $\pi$ schedules the jobs by increasing values of $\mathrm E(X_i)/\alpha_i$, then

$$\mathrm E\,S_N(\pi) \le \mathrm E\,S_N(\sigma) \qquad\text{for every permutation } \sigma .$$

Milestones

1. Lemma 1 (p. 495). If $\gamma_i>1$ for all $i$, the sum (1) is minimized over all permutations by any permutation ordered by increasing $\mu_i/[\gamma_i-1]$, and maximized by any permutation ordered by decreasing values.
2. Eq. (2) (p. 496). For every $\pi$ and $j\le N$,

$$S_j(\pi) = \sum_{i=1}^{j} X_{\pi(i)} \prod_{r=i+1}^{j} \bigl(1+\alpha_{\pi(r)}\bigr).$$

3. The expected makespan in the form (1) (p. 496, after (2)).

$$\mathrm E\,S_N(\pi) = \sum_{i=1}^{N} \mathrm E(X_{\pi(i)}) \prod_{r=i+1}^{N}\bigl(1+\alpha_{\pi(r)}\bigr) = F_{\mathrm E X,\,1+\alpha}(\pi).$$

Significance

The result is an index rule: each job receives a number computed from its own data, $\mathrm E(X_i)/\alpha_i$, and sorting by that number is optimal. It needs only the means of the initial requirements, not their distributions, and it holds without independence. The same reduction to Lemma 1 gives the paper's other index rules: the variance of the makespan under independent requirements, the Poisson-shock model (5), Lévy-type growth (6) and setup/detach times (7). In inventory issuing, it says which stored item to issue first when items lose value at item-specific linear rates. Lemma 1 itself, which the paper attributes to Rau (1971) and relates to optimal search, is a general statement about ordering products of factors along a sequence.

The result is proved in the paper by an appeal to Lemma 1, whose proof is given there as one sentence ("direct upon an interchange argument"). None of these statements has a machine-checked proof on Prove2Me or in Mathlib. This mission produces a formal model of linear deterioration on a single machine, a formal proof of the interchange lemma with ties handled, and the formal index rule.

Difficulty

The algebra of one adjacent interchange is short. The work is in passing from that local comparison to optimality over all $N!$ permutations, with ties allowed: the paper speaks of "the permutation ordered by increasing values", but with equal indices several permutations qualify, and each of them must be shown optimal. The natural route, "an optimal permutation exists and must be sorted", needs care, because a sorted permutation is not unique and the swap that improves an unsorted permutation may only weakly improve it. On the probabilistic side, the expectation of the makespan must be reduced to the expectations of the $X_i$; the makespan is a polynomial in the $X_i$ with deterministic coefficients, so this is linearity of the integral, but integrability has to be carried through the recursion.

Formalization scope

• Jobs are Fin N (0-based: Lean job i is the paper's job $i+1$); a policy is π : Equiv.Perm (Fin N) with π k the job in position k, as in the paper's $\pi(i)=j$. $N=0$ is allowed.
• The probability space is (Ω, P) with [IsProbabilityMeasure P]; $X_i$ is Ω → ℝ; expectations are Bochner integrals, and every theorem about them assumes each $X_i$ integrable. The growth rates are deterministic reals.
• Completion times are defined by the model recursion $S_{k}=S_{k-1}+Y_{\pi(k)}(S_{k-1})$, never by the closed form (2), so that (2) is a theorem about the model.
• Explicit readings of loose phrases: "the permutation ordered by increasing values of $v_i$" means any permutation with $k\mapsto v_{\pi(k)}$ non-strictly increasing (Monotone), and "decreasing" means Antitone; "is minimized" means $\le$ against every permutation; "expected" means the integral of an integrable random variable.
• Added hypotheses: $\alpha_i>0$ in the goal (the paper divides by $\alpha_i$ without stating it) and $\gamma_i>1$ in Lemma 1 (the paper applies it only with $\gamma_i = 1+\alpha_i$ or $(1+\alpha_i)^2$; for $\gamma_i<1$ the ordering reverses).
• Omitted assumptions: positivity of the $X_i$ and their independence. The goal holds without them, so the formal statement is slightly more general than the paper's.
• Trivializing formalizations are excluded: defining $S$ by formula (2) would make milestone 2 a definition unfolding; a strictly increasing ordering would make the goal vacuous whenever two indices tie; ordering $\pi^{-1}$ instead of $\pi$ states a different theorem; dropping integrability makes all expectations $0$; allowing $\alpha_i=0$ makes $\mathrm E(X_i)/\alpha_i=0$ a meaningless index.
• Not formalized here: the variance result (3), the Poisson model (5), the Lévy model (6), Proposition 1, setup times (7), exponential growth (9), and the NP-hardness conjecture. Proposition 2 (weighted expected completion time) is the companion mission Scheduling Deteriorating Jobs on a Single Processor II.
• Related platform items, none of which states these results: PalmQueueing.Ordering.interchange_permutations (interchange permutations of a GI/GI/1 queue) and the additive, non-deteriorating completion-time models MooreLateJobs.Shared.completionTime and NumStochOpt.ListScheduling.Makespan.

Contributions welcome: proofs of the milestones, a reusable "sorted permutation minimizes a sum of products" lemma, and the variance index (3) as an extension.

Selected references

• S. Browne, U. Yechiali, Scheduling Deteriorating Jobs on a Single Processor, Operations Research 38(3), 1990, 495–498. https://doi.org/10.1287/opre.38.3.495
• J. G. Rau, Minimizing a Function of Permutations of n Integers, Operations Research 19(1), 1971, 237–240. https://doi.org/10.1287/opre.19.1.237
• F. P. Kelly, A Remark on Search and Sequencing Problems, Mathematics of Operations Research 7(1), 1982, 154–157. https://doi.org/10.1287/moor.7.1.154
• R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.

Motivation

A portfolio manager who maximizes expected utility needs the distribution of asset returns, but in practice only estimates of its first two moments are available, and these estimates are themselves noisy. Distributionally robust optimization handles this by optimizing against the worst distribution in a set of plausible ones. Delage and Ye (Operations Research 58(3), 2010) proposed a set of distributions defined by confidence bounds on the mean and on the second-moment matrix, showed that the resulting problems are solvable in polynomial time for a large class of costs, and applied the framework to portfolio selection.

The set contains an upper bound on the covariance but no lower bound. Remark 1 of the paper says a lower bound "leads to important computational difficulties" and argues it should be unnecessary: for a concave utility, a less predictable market can only reduce expected utility, so the worst distribution should already have the largest covariance allowed. Proposition 3 in §5.2 turns this argument into a theorem for piecewise-linear concave utilities and unconstrained support. This mission formalizes Proposition 3 and the steps of its proof.

Setting

Let $n$ assets have a random return vector $\xi\in\mathbb R^n$, and let $x\in\mathbb R^n$ be a portfolio, so the return is $\xi^{\mathsf T}x$. A distribution of $\xi$ is a Borel probability measure on $\mathbb R^n$ with finite second moments. For symmetric matrices, $A\preceq B$ (the Loewner order) means $B-A$ is positive semidefinite.

Given a support set $S$, a centre $\mu_0$, a positive definite matrix $\Sigma_0\succ0$ and $\gamma_1\ge0$, $\gamma_2>0$, the distributional set of Assumption 3 is

$$\mathcal D_1(S,\mu_0,\Sigma_0,\gamma_1,\gamma_2)=\Big\{P\ :\ P(\xi\in S)=1,\ (\mathbb E[\xi]-\mu_0)^{\mathsf T}\Sigma_0^{-1}(\mathbb E[\xi]-\mu_0)\le\gamma_1,\ \mathbb E[(\xi-\mu_0)(\xi-\mu_0)^{\mathsf T}]\preceq\gamma_2\Sigma_0\Big\}.$$

The second constraint, (1b), is the covariance constraint.

The utility is piecewise linear concave, $u(y)=\min_{k\in\{1,\dots,K\}}a_ky+b_k$ with $K\ge1$ pieces, and the cost of a return is $-u$:

$$h(x,\xi)=\max_{k}\ \big(-a_k\,\xi^{\mathsf T}x-b_k\big).$$

With estimates $\hat\mu$, $\hat\Sigma\succ0$ of the mean and covariance, the inner problem of the robust portfolio problem with unconstrained support and an exactly known mean ($\gamma_1=0$) is

$$\max_{P\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,0,\gamma_2)}\ \mathbb E_P\big[h(x,\xi)\big].\tag{18}$$

The proof relates (18) to a semidefinite program in variables $\Lambda_k\in\mathbb R^{n\times n}$, $\lambda_k\in\mathbb R^n$, $\nu_k\in\mathbb R$:

$$\max\ \sum_k\big(-a_k\,x^{\mathsf T}\lambda_k-b_k\nu_k\big)\quad\text{s.t.}\quad \sum_k\Lambda_k\preceq\gamma_2\hat\Sigma+\hat\mu\hat\mu^{\mathsf T},\ \ \sum_k\lambda_k=\hat\mu,\ \ \sum_k\nu_k=1,\ \ \begin{bmatrix}\Lambda_k&\lambda_k\\\lambda_k^{\mathsf T}&\nu_k\end{bmatrix}\succeq0.\tag{19}$$

Formalization targets

Goal: Proposition 3

For every $\gamma_1\ge0$ (the mean-uncertainty radius of the robust portfolio problem (16); (18) is the case $\gamma_1=0$),

$$\exists\,P^*\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2):\quad \mathbb E_{P^*}\big[(\xi-\hat\mu)(\xi-\hat\mu)^{\mathsf T}\big]=\gamma_2\hat\Sigma\quad\text{and}\quad \mathbb E_Q[h(x,\xi)]\le\mathbb E_{P^*}[h(x,\xi)]\ \ \forall\,Q\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2).$$

The worst-case expectation is attained, and at a distribution for which the covariance constraint holds with equality. The statement holds for every portfolio $x$, every $K\ge1$, every $a,b$, every $\hat\mu$, every $\hat\Sigma\succ0$, every $\gamma_1\ge0$ and every $\gamma_2>0$.

Milestones

1. Every value of (18) is dominated by the value of a feasible point of (19).
2. (19) has an optimal solution at which $\sum_k\Lambda_k=\gamma_2\hat\Sigma+\hat\mu\hat\mu^{\mathsf T}$.
3. If $\begin{bmatrix}\Lambda&\lambda\\\lambda^{\mathsf T}&\nu\end{bmatrix}\succeq0$ and $\nu>0$, a random vector with mean $\lambda/\nu$ and second moment $\Lambda/\nu$ exists.
4. The mixture $\sum_k\nu_kP_k$ of such vectors, built from a tight feasible point with all $\nu_k>0$, lies in $\mathcal D_1$ and has second moment $\gamma_2\hat\Sigma$ about $\hat\mu$.
5. The expected cost under that mixture is at least the objective value of (19) at the point.
6. (18) and (19) have the same attained optimal value.

Significance

The proposition justifies a modelling decision of the whole paper: for portfolio problems with piecewise-linear concave utility, adding a lower bound $\gamma_3\Sigma_0\preceq\mathbb E[(\xi-\mu_0)(\xi-\mu_0)^{\mathsf T}]$ (display (2)) to the distributional set cannot change the robust decision, so the computational difficulty that lower bound would cause is avoided at no loss. It also shows that, under these assumptions and with $\gamma_2=1$, the paper's semidefinite formulation solves the known-moment portfolio problem of Popescu (2007) in polynomial time (Remark 4). The worst case is explicit: a finite mixture of distributions with prescribed first and second moments, read off an optimal solution of (19).

The result is proved in the paper; no machine-checked version is known. Formalizing it requires a moment-problem argument (from a distribution to a feasible point of an SDP) and its converse (from an SDP solution to a distribution), both of which are reusable for other moment-based distributionally robust results. The proposition concerns the robust portfolio problem with $\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2)$; the paper's proof writes out only $\gamma_1=0$ "for simplicity of our derivations". The goal states the proposition for every $\gamma_1\ge0$; the milestones follow the written proof and are stated for $\gamma_1=0$.

Difficulty

The obvious argument, "a concave utility prefers less spread, so the adversary maximizes spread", does not prove anything by itself: increasing the second-moment matrix of a given distribution in the Loewner order does not determine its law, and the expected cost depends on the whole law, not on the moments. The proof goes through the semidefinite program (19). Two steps carry the weight. First, every distribution in $\mathcal D_1$ must be mapped to a feasible point of (19) with no smaller value, although the cost is only piecewise affine in $\xi$. Second, an optimal point of (19) must be turned back into a distribution in $\mathcal D_1$; this needs the existence of random vectors with prescribed first and second moments, and care with blocks where $\nu_k=0$, which the paper sets aside "without loss of generality" although such a block can carry a nonzero $\Lambda_k$ that the mixture would lose.

Formalization scope

• Vectors are Fin n → ℝ; all Euclidean quantities are dot products, never the sup norm. Matrices are Matrix (Fin n) (Fin n) ℝ; $A\preceq B$ is (B - A).PosSemidef; $\Sigma_0^{-1}$ is Mathlib's matrix inverse, used only with $\Sigma_0\succ0$.
• A distribution is a Measure (Fin n → ℝ) that is a probability measure and whose coordinates are in $L^2$ (MemLp _ 2). This makes every mean, second moment and expected cost a genuine integral; without it a non-integrable expectation would evaluate to $0$.
• $P(\xi\in S)=1$ is an almost-everywhere statement; the goal uses $S=\mathbb R^n$ ("infinite support constraint"). The convexity of $S$, $\mu_0\in\operatorname{int}S$ and the separation oracle of Assumption 3 concern the paper's algorithms and are not part of the set.
• The maximum of (18) is never a real supremum: the goal asserts a maximizer that dominates every member of the set. The cost uses a finite maximum over $K\ge1$ pieces ([NeZero K]).
• Standing hypotheses: $\hat\Sigma\succ0$ (Assumption 3's $\Sigma_0\succ0$, and endnote 1), $\gamma_2>0$ (§3), $\gamma_1\ge0$ (Assumption 3) in the goal; the milestones fix $\gamma_1=0$ as the proof does. The portfolio $x$ ranges over all of $\mathbb R^n$; the simplex constraint (16b) plays no role in the inner problem, so dropping it only strengthens the statements.
• The objective of (19) has the sign of the proof's final computation (p. 21), $\sum_k(-a_kx^{\mathsf T}\lambda_k-b_k\nu_k)$; display (19a) on p. 19 prints the opposite signs, a misprint.
• Ruling out trivial readings: the goal requires both membership in $\mathcal D_1$ with tight covariance and domination of every member of $\mathcal D_1$. A distribution with covariance $\gamma_2\hat\Sigma$ alone, or a maximizer alone, would not suffice. The goal does not claim that every maximizer is tight; for $K=1$ the cost is linear and every member of $\mathcal D_1$ is a maximizer.
• Infrastructure needed: existence of distributions with prescribed mean and covariance (for instance multivariate Gaussians, or degenerate laws on a subspace), finite mixtures of measures and their moments, Schur complements of positive semidefinite block matrices, and compactness of the feasible set of (19). Proofs of the milestones in any order are welcome.

The source is the authors' draft of 20 February 2008 of the Operations Research paper; every page, display and label in this mission refers to that draft.

Selected references

• E. Delage and Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010 (authors' draft of 20 February 2008 used here). https://doi.org/10.1287/opre.1090.0741
• I. Popescu, Robust mean-covariance solutions for stochastic optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• Y. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Second-order stochastic dominance constraints let a decision maker require that a random outcome of a decision be preferred to a fixed benchmark outcome by every risk-averse expected-utility maximizer, without choosing a utility function in advance. Dentcheva and Ruszczyński introduced optimization under such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim., 2003), for the case where the decision enters the outcome linearly (the pure-dominance case). Their follow-up paper, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program., 2004), allows the decision to affect many random outcomes in a nonlinear, concave way, and derives optimality and duality theory in which the Lagrange multipliers of the dominance constraints are utility functions.

In applications (portfolio selection against a benchmark index is the paper's own example in §6) the probability space is a finite set of scenarios. Section 5 of the paper specialises the theory to that case. This mission formalizes that section: the reduction of the dominance constraints to finitely many inequalities, and the optimality and duality theorems (Theorems 6 and 7) in which the multipliers become piecewise-linear concave utilities.

Setting

There are $n$ scenarios $\omega_1,\dots,\omega_n$ with probabilities $p_j \ge 0$, $\sum_j p_j = 1$, and $m$ benchmark constraints, indexed by $i \in I = \{1,\dots,m\}$; $J = \{1,\dots,n\}$. A decision $z$ ranges over a convex set $Z \subseteq \mathbb R^N$. For each scenario $j$, $h_j:\mathbb R^N\to\mathbb R$ is the objective contribution and $g_{ij}:\mathbb R^N\to\mathbb R$ the $i$th outcome, all concave. The benchmark $Y_i$ has realizations $y_{ij}$. Write $(t)_+=\max(t,0)$.

The second-order dominance of a finitely distributed $X_i$ (realizations $x_{ij}$) over $Y_i$ on an interval $[a_i,b_i]$ reads

$$\sum_{j} p_j(\eta - x_{ij})_+ \le \sum_j p_j(\eta-y_{ij})_+ \quad\text{for all } \eta\in[a_i,b_i]. \tag{36}$$

The split-variable problem (38)–(41) is

$$\max \sum_{j=1}^n p_j h_j(z)\quad\text{s.t.}\quad \sum_{j} p_j(y_{ik}-x_{ij})_+ \le \sum_j p_j(y_{ik}-y_{ij})_+,\quad x_{ik}\le g_{ik}(z),\quad z\in Z,$$

for all $i\in I$, $k\in J$, over $z$ and $X=(x_{ij})\in\mathbb R^{mn}$. The Slater condition asks for $\tilde z \in \operatorname{relint} Z$ and $\tilde X$ satisfying the dominance constraints (39) with $\tilde x_{ik} < g_{ik}(\tilde z)$ for all $i,k$.

The utility set $V_i$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave, nondecreasing, piecewise linear with break points only at the $y_{ik}$, and zero on $[\max_k y_{ik},\infty)$. With $\theta_{ij}\ge 0$ multipliers for the splitting constraints $x_{ij}\le g_{ij}(z)$, the Lagrangian is

$$L(z,X,u,\theta) = \sum_{j=1}^n p_j\Big[h_j(z)+\sum_{i=1}^m\theta_{ij}g_{ij}(z)\Big]+\sum_{i=1}^m\sum_{j=1}^n p_j\big[u_i(x_{ij})-u_i(y_{ij})-\theta_{ij}x_{ij}\big]. \tag{42}$$

Multipliers $\mu_{ik}$ of the inequalities (39) generate the utility $u_i(t)=-\sum_k\mu_{ik}(y_{ik}-t)_+$ (46). The dual functional is $D(u,\theta)=\sup_{z\in Z,\,X}L(z,X,u,\theta)$ (47).

Formalization targets

Goal: Theorem 6

Under the Slater condition, $(\hat z,\hat X)$ optimal for (38)–(41) implies that there are $\hat u_i\in V_i$ and $\hat\theta\ge 0$ with

$$L(\hat z,\hat X,\hat u,\hat\theta)=\max_{(z,X)\in Z\times\mathbb R^{mn}}L(z,X,\hat u,\hat\theta),\qquad \sum_j p_j[\hat u_i(\hat x_{ij})-\hat u_i(y_{ij})]=0,\qquad \hat\theta_{ij}(\hat x_{ij}-g_{ij}(\hat z))=0;$$

conversely, these conditions together with feasibility imply optimality.

Milestones

1. Lemma 2 (p. 15): if $a_i\le y_{ij}\le b_i$, then (36) is equivalent to the $mn$ inequalities (37) at the realizations $\eta=y_{ik}$, and also to (36) on the whole line.
2. Eq. (46) (p. 17): for any $\mu$, the standard Lagrangian $\Lambda(z,X,\mu,\theta)$ equals $L(z,X,u,\theta)$ with $u$ given by (46).
3. p. 18: for $\mu_i\ge0$, the utility (46) lies in $V_i$.
4. pp. 16–17: under Slater, an optimal solution admits Kuhn–Tucker multipliers $\mu\ge0$, $\theta\ge0$ for (38)–(41) with complementarity.
5. p. 18: every $v\in V_i$ is of the form (46) with $\mu_i\ge0$.
6. Theorem 7 (p. 18), after the goal: the dual problem $\min\{D(u,\theta): u\in V_1\times\dots\times V_m,\ \theta\ge0\}$ has a solution and no duality gap.

Significance

Theorem 6 says that, for finitely many scenarios, the infinite-dimensional multiplier of the general theory (a concave utility in a cone of functions, Theorem 2 of the paper) can always be taken piecewise linear with kinks exactly at the benchmark's realizations. The multiplier space becomes finite-dimensional, $V_i$ is a polyhedral cone, and the dual problem of Theorem 7 is a finite-dimensional convex program. The paper's decomposition (49)–(51) of the dual functional and its numerical method in §6 rest on this. Lemma 2 is the standard reduction that makes dominance against a finitely distributed benchmark a finite set of polyhedral constraints, used throughout the later literature on dominance-constrained portfolio optimization.

The results are proved in the paper; none of them is formalized. The mission produces machine-checked statements of the finite-scenario theory, a Lean model of the utility set $V_i$ and of the correspondence between nonnegative multipliers and piecewise-linear utilities, and a Kuhn–Tucker theorem for concave programs with polyhedral constraints and a relative-interior Slater point.

Difficulty

The obvious route to Theorem 6 is to invoke a Kuhn–Tucker theorem. The available formal versions require every inequality constraint to hold strictly at the Slater point and range over all of $\mathbb R^N$. Neither fits: the dominance constraint at the smallest realization $y_{i,[1]}$ has right-hand side $0$ and a nonnegative left-hand side, so it can never hold strictly, and $Z$ may be lower-dimensional (a simplex), so only its relative interior is available. The polyhedral structure of (39) must be used, as in Rockafellar's Theorem 28.2. The second obstacle is the converse direction of the multiplier–utility correspondence: a utility in $V_i$ must be written as a nonnegative combination of the kinks $(y_{ik}-t)_+$, which requires handling repeated realizations and the one-sided slopes at each break point.

Formalization scope

• $\mathbb R^N$ is Fin N → ℝ; $X$, $\theta$, $\mu$ are Fin m → Fin n → ℝ; expectations are finite sums and positive parts are max t 0. No measure theory is used.
• Probabilities satisfy $p_j\ge0$, $\sum_jp_j=1$; $p_j=0$ is allowed, as on the page.
• Standing assumptions of p. 2 are explicit hypotheses: $Z$ convex and $h_j$, $g_{ij}$ concave on $\mathbb R^N$. Continuity is not stated, since finite concave functions on $\mathbb R^N$ are continuous.
• The relative interior is intrinsicInterior ℝ Z, not the topological interior. In the Slater condition only the splitting constraints are strict; the dominance constraints hold non-strictly.
• $V_i$ is defined by concavity, monotonicity, affinity on every interval whose interior contains no $y_{ik}$, and $u=0$ on $[\max_ky_{ik},\infty)$. This last clause is the page's $u(y_{i,[n]})=0$ combined with $V_i\subset\mathcal U_1([a_i,b_i])$. No positive slope is required, because the printed "$c>0$" in $\mathcal U_1$ is a misprint for $c\ge0$.
• "max" in (43) is an attained maximum over all of $Z\times\mathbb R^{mn}$, with no constraints on $X$. The dual functional (47) is an EReal supremum.
• Theorem 6 keeps the Slater condition as a hypothesis of the whole statement, as printed, although its converse part does not use it.
• A trivializing formalization is ruled out. $V_i$ is not defined as the set of functions of the form (46), which would make milestones 3 and 5 true by definition. Slater does not require strict dominance constraints, which would make it unsatisfiable. A sorry-free check confirms that the goal's hypotheses hold on an instance ($n=2$, $Z=[0,1]$).
• Reusable beyond this mission: the Kuhn–Tucker theorem with polyhedral constraints and relative-interior Slater point (milestone 4), and Lemma 2. Proofs of any item, and alternative proofs of the goal that avoid milestone 4, are welcome.
• The pure-dominance case is the earlier paper of Dentcheva–Ruszczyński (2003). The function $F_2$ and its expected-shortfall form are due to Ogryczak–Ruszczyński. The general Lagrange duality on the platform (ConvexOptimization.slater_strong_duality, Boyd–Vandenberghe §5.3.2) assumes a strict Slater point for every constraint and no set constraint, so it does not cover milestone 4.

Selected references

• D. Dentcheva, A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Math. Program., 2004 (cited here from the authors' revised manuscript, April 2003). https://doi.org/10.1007/s10107-003-0453-z
• D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14 (2003) 548–566. https://doi.org/10.1137/S1052623402420528
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13 (2002) 60–78. https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §28. https://doi.org/10.1515/9781400873173

Why throughput matters

A processing network must decide which activities receive scarce processor capacity while jobs move among buffers. Such decisions matter in manufacturing, service systems, and switches: one activity can consume several processors at once, and a job can be routed to another buffer after processing. A policy that sees current buffer levels but does not need to know arrival or routing rates is easier to operate when those rates are difficult to estimate. Dai and Lin's 2005 paper studies whether a maximum pressure policy, which uses the buffer vector and an input-output matrix, can stabilize every network that is stabilizable in their model. Their Theorems 1 and 2 give, respectively, a necessary planning condition for any stabilizing policy and a sufficient condition for maximum pressure under the extreme-allocation-available assumption. Dai and Lin (2005)

Here pathwise stability means that each internal buffer grows sublinearly in time almost surely. This is a rate statement about sample paths. It does not assert positive recurrence of a Markov chain, nor does it require a stationary distribution. The paper allows general primitive processing and routing processes with almost-sure long-run averages. Dai and Lin (2005), §§2–4

Network and allocations

There are $I$ internal buffers, $J$ activities, and $K$ processors. Buffer $0$ represents the outside world. The $K\times J$ matrix $A$ records resource use: $A_{kj}=1$ when activity $j$ requires processor $k$. The $J\times(I+1)$ matrix $B$ records which buffers an activity processes. An input activity processes Buffer $0$; a service activity does not. Input processors serve only input activities and must be fully used, while all processors have at most unit capacity.

For activity $j$, the processing requirements have mean $m_j$ and the routing counts have long-run matrix $P^j$. Write $\mu_j=1/m_j$. The input-output matrix is

$$R_{ij}=\mu_j\left(B_{ji}-\sum_{i'=0}^{I}B_{ji'}P^j_{i'i}\right),\qquad i=1,\ldots,I.$$

Positive $R_{ij}$ means activity $j$ consumes net material from internal buffer $i$; negative means it produces net material there. An allocation $a\in\mathcal A$ assigns nonnegative activity levels subject to the processor capacity bounds and the equality for every input processor. The finite set $\mathcal E$ consists of the extreme points of this allocation set. At buffer vector $z$, allocation $a$ has network pressure $p(a,z)=z\cdot Ra$. The maximum pressure rule chooses an allocation of greatest pressure among the currently feasible members of $\mathcal E$. Feasibility depends on jobs actually available to each constituent buffer. Dai and Lin (2005), §§2–3

The extreme-allocation-available assumption (EAA) says that for every nonnegative $z$, a pressure maximizer in $\mathcal E$ can be chosen whose constituent buffers all have positive levels. It links the static pressure maximization to the jobs that a policy can process. The static planning LP asks for activity fractions $x\ge0$ and a service-processor load $\rho$ such that $Rx=0$, every input processor has load one, and every service processor has load at most $\rho$. Dai and Lin (2005), p. 202

Formalization targets

The goal is Theorem 2. For a network satisfying EAA and run by a preemptive, processor-splitting maximum pressure policy, LP feasibility with $\rho\le1$ implies

$$\mathbb P\!\left(\forall i\in\{1,\ldots,I\},\ \lim_{t\to\infty}\frac{Z_i(t)}{t}=0\right)=1.$$

The milestones follow the paper's route from stochastic paths to deterministic fluid limits. A fluid limit is a uniform-on-compact limit of $(Z(rt),T(rt))/r$ along positive scales $r\to\infty$. The milestones state that fluid limits satisfy (14)–(18), weak stability of the corresponding fluid model transfers to pathwise stability (Theorem 3), maximum pressure adds (52)–(55) and (20) (Lemmas 5 and 4), quadratic fluid energy obeys (22)–(23), and LP feasibility with EAA makes the maximum-pressure fluid model weakly stable (Theorem 4). Dai and Lin (2005), pp. 203, 213–214

What the result gives

Theorem 2 identifies a policy whose almost-sure buffer growth rate vanishes whenever the planning LP permits load at most one and EAA holds. Together with the paper's necessary condition in Theorem 1, it characterizes the feasibility boundary for this policy class under EAA. Its scope includes networks in which an activity uses multiple processors and processes multiple buffers simultaneously. It does not claim that all such networks satisfy EAA. Dai and Lin (2005), Theorems 1–2

The result is proved in the 2005 article. This mission asks for a machine-checked proof of that known theorem and its selected intermediate claims. The Lean statements are open draft targets. Reusable outcomes include a model of cumulative routing and service counts, a uniform-on-compact fluid-limit interface, and the weak-fluid-stability transfer theorem for networks without a Markov assumption.

Why the proof is difficult

Maximizing pressure over the static allocation polytope does not by itself describe an executable service policy. An allocation can demand work from an empty buffer. EAA addresses the existence of a maximizing allocation supported by positive buffer levels, but the stochastic policy acts on actual jobs and completion times. The proof must connect those discrete, pathwise decisions to the limiting differential equation (20). At a regular fluid time, the maximum-pressure equation is decisive; away from regular times, derivatives need not exist. The fluid model therefore carries a time qualifier that cannot simply be dropped. Dai and Lin (2005), pp. 201–203, 214

Formalization scope

The Lean model uses finite index types for buffers, activities, and processors. Internal buffers are Fin I; Buffer 0 is the zero index of Fin (I+1), and an internal buffer maps to its successor index. Activity and processor labels use zero-based Fin. Time is real but all network equations are asserted for nonnegative time. The shared Bell–Williams Paths definition supplies the renewal count in $\mathbb N\cup\{\infty\}$ and uniform-on-compact distance using the $\ell^1$ norm. The completion count is required finite wherever the network equations convert it to a natural number; this prevents infinity from becoming a zero count. Bell and Williams (2001)

The network standing assumptions record binary incidence matrices, nonempty constituencies, processor coverage, activity types, and an input activity. Two refinements are explicit: each input processor has an activity, so its mandatory unit allocation is feasible, and $m_j>0$, so $\mu_j=1/m_j$ is defined as the intended positive rate. Routing counts are cumulative and nonnegative. Their row sums are constrained only for buffers an activity processes: the printed sentence requiring the same sum for every buffer conflicts with its immediately preceding statement that the count vanishes when the activity does not process that buffer. The corresponding rows of $P^j$ sum to one for processed buffers and vanish for unprocessed buffers, as follows from (4). Dai and Lin (2005), pp. 199–200

The policy predicate records allocation-time decomposition (49)–(51) and the non-employment consequence of Definition 1 used in (56)–(58). It checks feasibility of a competing extreme allocation through the paper's threshold $J$ at every time of the interval. Individual job states and tie breaking are outside the pathwise interface. The goal retains EAA, the exact $\rho\le1$ bound, and all network and policy equations, so an empty allocation set or an unconstrained service path cannot make the target automatic. Contributions formalizing the finite extreme-point set, fluid-limit compactness, Lemmas 4–5, and the weak-stability transfer are welcome.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. DOI.
• S. L. Bell and R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Annals of Applied Probability 11(3):608–649, 2001. DOI.

Motivation

In a stochastic multi-armed bandit a player repeatedly chooses one of $K$ arms and receives a random reward drawn from that arm's unknown distribution; the aim is to pull suboptimal arms as rarely as possible. Lai and Robbins (1985) and, for general models, Burnetas and Katehakis (1996) showed that any reasonable strategy must pull a suboptimal arm $a$ at least $(1+o(1))\log T/\mathcal K_{\inf}(\nu_a,\mu^\star)$ times in $T$ rounds, where $\mathcal K_{\inf}$ is a minimal Kullback–Leibler divergence defined below. A strategy whose expected number of pulls matches this constant is asymptotically optimal.

For rewards in $[0,1]$, classical index policies such as UCB (Auer, Cesa-Bianchi and Fischer, 2002) achieve $O(\log T)$ pulls but with a constant governed by the gap of the means, not by $\mathcal K_{\inf}$. Cappé, Garivier, Maillard, Munos and Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3), 2013 (arXiv:1210.1136v4), introduce the KL-UCB family of index policies and prove finite-time bounds whose leading term is the Lai–Robbins/Burnetas–Katehakis constant. This mission formalizes their result for empirical KL-UCB (Algorithm 3, Theorem 2), which is asymptotically optimal in the nonparametric model of finitely supported distributions on $[0,1]$. A companion mission covers kl-UCB in one-parameter exponential families (Theorem 1).

Timeline: Lai and Robbins (1985), lower bound for parametric families; Burnetas and Katehakis (1996), lower bound and asymptotically optimal policies for general models; Honda and Takemura (2010, 2011), the DMED algorithm, asymptotically optimal for finitely supported and bounded rewards; Cappé et al. (2013), the first index policy with a non-asymptotic bound whose leading term is optimal in this model.

Setting

A bandit has $K\ge2$ arms with reward distributions $\nu_1,\dots,\nu_K$ in a known model $\mathcal F$: the set of probability distributions over $[0,1]$ with finite support. Write $\mathrm E(\nu)=\int x\,d\nu(x)$, $\mu_a=\mathrm E(\nu_a)$ and $\mu^\star=\max_a\mu_a$; arm $a$ is suboptimal if $\mu_a<\mu^\star$. At each round $t\ge1$ the player picks an arm $A_t$ based on past observations and observes a reward drawn from $\nu_{A_t}$. $N_a(T)=\sum_{t=1}^T\mathbb I\{A_t=a\}$ is the number of pulls of arm $a$ up to round $T$.

Equivalently, each arm has a reward stack $X_{a,1},X_{a,2},\dots$ of i.i.d. draws from $\nu_a$, all stacks independent, and the $n$-th pull of arm $a$ returns $X_{a,n}$. The empirical distribution of the first $n$ rewards is $\hat\nu_{a,n}=\frac1n\sum_{k=1}^n\delta_{X_{a,k}}$, and $\hat\nu_a(t)=\hat\nu_{a,N_a(t)}$.

The minimal divergence is

$$\mathcal K_{\inf}(\nu,\mu)=\inf\bigl\{\mathrm{KL}(\nu,\nu'):\nu'\in\mathcal F,\ \mathrm E(\nu')>\mu\bigr\}\in[0,+\infty],$$

the smallest Kullback–Leibler divergence from $\nu$ to a distribution of the model whose mean exceeds $\mu$.

Empirical KL-UCB (Algorithm 3) pulls each arm once, then for $t=K,K+1,\dots$ pulls an arm maximizing

$$U_a(t)=\sup\Bigl\{\mathrm E(\nu):\nu\in\mathfrak M_1\bigl(\mathrm{Supp}(\hat\nu_a(t))\cup\{1\}\bigr),\ \mathrm{KL}(\hat\nu_a(t),\nu)\le\frac{f(t)}{N_a(t)}\Bigr\},$$

where $\mathfrak M_1(A)$ is the set of probability distributions carried by $A$ and $f(t)=\log t+\log\log t$. The added point $1$ is essential: without it the index is the empirical-likelihood bound, which equals the empirical mean when every observation is $0$.

Formalization targets

Goal: Theorem 2 (pp. 15–16)

Assume $\mu_a>0$ for all arms and $\mu^\star<1$. There is a constant $M(\nu_a,\mu^\star)>0$ depending only on $\nu_a$ and $\mu^\star$ such that, for every suboptimal arm $a$ and all $T\ge3$,

$$\begin{aligned}\mathbb E[N_a(T)]\le{}&\frac{\log T}{\mathcal K_{\inf}(\nu_a,\mu^\star)}+\frac{36}{(\mu^\star)^4}(\log T)^{4/5}\log\log T+\Bigl(\frac{72}{(\mu^\star)^4}+\frac{2\mu^\star}{(1-\mu^\star)\mathcal K_{\inf}(\nu_a,\mu^\star)^2}\Bigr)(\log T)^{4/5}\\&+\frac{(1-\mu^\star)^2M(\nu_a,\mu^\star)}{2(\mu^\star)^2}(\log T)^{2/5}+\frac{\log\log T}{\mathcal K_{\inf}(\nu_a,\mu^\star)}+\frac{2\mu^\star}{(1-\mu^\star)\mathcal K_{\inf}(\nu_a,\mu^\star)^2}+4.\end{aligned}$$

The constants are the paper's. $M$ is the one quantity the main text does not give; it is existentially quantified, before the bandit, so it may depend on nothing but $(\nu_a,\mu^\star)$.

Milestones

1. (7), p. 9: the sets $\mathcal C_{\mu,\gamma}=\{\nu:\exists\nu'\in\mathcal F,\ \mathrm E(\nu')>\mu,\ \mathrm{KL}(\nu,\nu')\le\gamma\}$ satisfy $\mathcal C_{\mu,\gamma}\subseteq\{\nu:\mathcal K_{\inf}(\nu,\mu)\le\gamma\}$.
2. (5), p. 9: the decomposition $\{A_{t+1}=a\}\subseteq\{\mu^\dagger\ge U_{a^\star}(t)\}\cup\{\mu^\dagger<U_a(t),\ A_{t+1}=a\}$.
3. The display after (7), p. 9: $\mathbb E[N_a(T)]\le1+\sum_{t=K}^{T-1}\mathbb P\{\mu^\dagger\ge U_{a^\star}(t)\}+\sum_{t=K}^{T-1}\mathbb P\{\hat\nu_{a,N_a(t)}\in\mathcal C_{\mu^\dagger,f(t)/N_a(t)},\ A_{t+1}=a\}$.
4. (8), p. 10: the second sum is at most $\sum_{n=1}^{T-K}\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}$.
5. (9)–(10), p. 10: $\mathbb E[N_a(T)]\le f(T)/\mathcal K_{\inf}(\nu_a,\mu^\star)+\sum_{n>n_0}\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}+\sum_t\mathbb P\{\mu^\dagger\ge U_{a^\star}(t)\}+2$ with $n_0=\lceil f(T)/\mathcal K_{\inf}(\nu_a,\mu^\star)\rceil$.
6. p. 15: the supremum defining $U_a(t)$ over $\mathcal F$ equals the supremum over $\mathfrak M_1(\mathrm{Supp}(\hat\nu_a(t))\cup\{1\})$.
7. Implicit in Theorem 2: $0<\mathcal K_{\inf}(\nu,\mu)<\infty$ for $\nu\in\mathcal F$ and $\mathrm E(\nu)<\mu<1$.
8. Proposition 1, p. 20: for $n$ i.i.d. observations from any $\nu_0$ on $[0,1]$ with $\mathrm E(\nu_0)\in(0,1)$ and every $\varepsilon>0$,

$$\mathbb P\{U(\hat\nu_n,\varepsilon)\le\mathrm E(\nu_0)\}\le\mathbb P\{\mathcal K_{\inf}(\hat\nu_n,\mathrm E(\nu_0))\ge\varepsilon\}\le e(n+2)\exp(-n\varepsilon).$$

Significance

Theorem 2 gives a finite-time bound whose leading term, $\log T/\mathcal K_{\inf}(\nu_a,\mu^\star)$, equals the Burnetas–Katehakis lower bound for the model $\mathcal F$. Hence empirical KL-UCB is asymptotically optimal among all strategies for finitely supported rewards in $[0,1]$, and the regret $\sum_a(\mu^\star-\mu_a)\mathbb E[N_a(T)]$ inherits the optimal constant. Since $\mathcal K_{\inf}(\nu_a,\mu^\star)$ is at least the Bernoulli divergence of the means, and usually larger, the bound improves on kl-UCB and UCB for the same rewards. Proposition 1 is a non-asymptotic coverage bound for the empirical-likelihood upper confidence bound with the point $1$ added, valid for every law on $[0,1]$, not only finitely supported ones.

The proofs of Theorem 2 and Proposition 1 are in the paper's supplemental article (Appendix B), not in the main text; no machine-checked proof of either exists. The mission produces formal statements of the theorem and of the proof skeleton (5)–(10) that the paper shares with Theorem 1, and of the two facts about $\mathcal K_{\inf}$ that the bound needs. A formal proof would supply an explicit $M(\nu_a,\mu^\star)$, which the paper defines only inside the supplement.

Difficulty

The skeleton (5)–(10) is elementary bookkeeping; the difficulty lies in the two sums it leaves, both of which must be shown to be $o(\log T)$ with explicit constants. The second, $\sum_n\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}$, needs a deviation estimate for the empirical $\mathcal K_{\inf}$ of a suboptimal arm that is precise enough to keep the leading constant $1/\mathcal K_{\inf}(\nu_a,\mu^\star)$: a bound that only controls the deviation of the empirical mean loses it, since $\mathcal K_{\inf}$ depends on the whole distribution. The first, $\sum_t\mathbb P\{\mu^\dagger\ge U_{a^\star}(t)\}$, concerns the optimal arm after a random number of pulls $N_{a^\star}(t)$, which the algorithm itself determines, so fixed-sample bounds such as Proposition 1 do not apply directly. Both need regularity of $\mathcal K_{\inf}$ as a function of a distribution in an infinite-dimensional model, where none of the closed forms of the exponential-family case is available.

Formalization scope

Arms are Fin K, and arm $a$ of the paper is index $a-1$. The bandit is the platform's stack-of-rewards model RegretBandits.Stochastic.IsStochasticBandit: $X_{a,k}$ (indexed from $0$) are independent, identically distributed within each arm, with mean $\mu_a$. Pull counts and $\mu^\star$ are the platform's pullCount and bestMean. Added to the page, and disclosed in each statement: every reward lies in $[0,1]$ pathwise (a representation of "$\nu_a$ is carried by $[0,1]$"), every arm choice is measurable, and in the goal the strategy is non-anticipating ($A_{t+1}$ is measurable with respect to the arms and rewards of rounds $1,\dots,t$). A run of Algorithm 3 is a pathwise predicate: rounds $1,\dots,K$ pull distinct arms, and every later round pulls a maximizer of $U_\cdot(t)$, with ties broken by any rule. KL is Mathlib's InformationTheory.klDiv in $[0,+\infty]$, with the empirical distribution as first argument. $\mathcal K_{\inf}$ is kept in $[0,+\infty]$ and converted to a real number only in the final bounds, where it is finite and positive. Probabilities of events whose measurability is not asserted are outer probabilities. The page's $\sum_{n\ge n_0+1}$ in (10) is stated as the finite sum over $n_0<n\le T-K$ that (8) produces. The probability space of Theorem 2 lies in Type.

Trivializing formalizations are ruled out. The index is a supremum over a set that is nonempty (it contains $\mathrm E(\hat\nu_a(t))$) and bounded above, so it is never Lean's junk value. $\mathcal K_{\inf}$ and $\mathcal C_{\mu,\gamma}$ range over $\mathcal F$, not over all measures. The run predicate has both the initialization and the argmax clause. $M$ is quantified before the bandit and the horizon.

Reusable beyond this mission: $\mathcal K_{\inf}$ for $\mathcal F$, the empirical-likelihood bound $U$ of (15), and Proposition 1, a concentration inequality for empirical $\mathcal K_{\inf}$ that applies to any bounded i.i.d. sample. Proofs of any milestone are welcome, as are proofs of the skeleton (5)–(10) that also apply to the companion kl-UCB mission.

Selected references

• O. Cappé, A. Garivier, O.-A. Maillard, R. Munos, G. Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3):1516–1541, 2013. arXiv:1210.1136v4, doi:10.1214/13-AOS1119; supplement doi:10.1214/13-AOS1119SUPP.
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6(1):4–22, 1985. doi:10.1016/0196-8858(85)90002-8
• A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Adv. Appl. Math. 17(2):122–142, 1996. doi:10.1006/aama.1996.0007
• J. Honda, A. Takemura, An asymptotically optimal bandit algorithm for bounded support models, COLT 2010, 67–79.
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time analysis of the multiarmed bandit problem, Mach. Learn. 47:235–256, 2002. doi:10.1023/A:1013689704352