All missions

Reverse convex sets and intersection cuts

A reverse convex set is the part of a polyhedron that lies outside an open convex set: $P\setminus C$, where $P=\{x\in\mathbb{R}^n_+ : Ax=b\}$ and $C\subseteq\mathbb{R}^n$ is open and convex. Such sets arise whenever a model forbids a convex region: integrality (a lattice-free convex set contains no feasible point in its interior), bilevel programs, where the points with $d^\top y>\Phi(x)$ for a convex value function $\Phi$ are infeasible, and nonconvex quadratic or polynomial constraints. Optimizing over $P\setminus C$ calls for valid inequalities for its closed convex hull.

The classical tool is the intersection cut of Balas (Balas 1971): starting from a basic solution $\bar x$ of the linear relaxation that lies inside $C$, one follows the extreme rays of the basis cone until they leave $C$, and the exit points define a valid inequality. Towle and Luedtke study the opposite case, where the basic solution lies outside the closure of $C$. Then the rays of the basis cone may enter $C$, cross it, or never leave it, and no single inequality captures the structure. They replace the cut by a disjunction: a finite union of simpler sets that contains $P\setminus C$, to which the disjunctive programming machinery of Balas can be applied. The present mission targets their multi-term disjunction (Theorem 5 of the paper), which uses the full recession cone of $C$.

Setting

Let $A\in\mathbb{R}^{m\times n}$ have full row rank and $b\in\mathbb{R}^m$. A basis splits the variables into basic variables $B$ and nonbasic variables $N$, with a tableau $\bar a$ and a basic solution $\bar x$ ($\bar x_j=0$ for $j\in N$) such that $Ax=b$ holds exactly when $x_i=\bar x_i-\sum_{j\in N}\bar a_{ij}x_j$ for all $i\in B$. Dropping the sign constraints on the basic variables gives the basis cone

a translated simplicial cone with apex $\bar x$ and extreme rays $\bar r^j$ ($j\in N$): $\bar r^j_j=1$, $\bar r^j_k=-\bar a_{kj}$ for $k\in B$, and $\bar r^j_k=0$ for the other nonbasic $k$.

The recession cone of $C$ is $\operatorname{recc}(C)=\{d : x+td\in C\text{ for all }x\in C,\ t\ge 0\}$. Along each ray, the halfline $\bar x+\lambda\bar r^j$, $\lambda\ge 0$, meets $C$ in an interval with endpoints

in the extended reals, with $\alpha_j=+\infty$, $\beta_j=-\infty$ when the halfline misses $C$. This sorts the nonbasic indices into $N_0$ (the ray misses $C$), $N_1$ ($\alpha_j$ finite and positive, $\beta_j=+\infty$: the ray enters $C$ and stays) and $N_2$ ($\alpha_j<\beta_j<+\infty$: the ray crosses $C$); write $N_0^{\mathrm c}=N_1\cup N_2$. For extended reals $\alpha<\beta$ and a vector $r$, the segment $(\alpha,\beta)r$ is $\{\lambda r:\lambda\in\mathbb{R},\ \alpha<\lambda<\beta\}$, and $[0,\beta)r$, $(-\infty,0]r$ are defined likewise. The paper builds the inner approximation of $C$

and the sets

Throughout, $\bar x\notin\operatorname{cl}(C)$, and (Assumption 2 of the paper) $\operatorname{recc}(C)\subseteq\operatorname{recc}(P^B)$.

Formalization targets

Goal: Theorem 5

With $N_2^0:=N_2\cup\{0\}$,

The relaxation $P^B\setminus T^C$ of $P^B\setminus C$ is thus a disjunction of $|N_2|+1$ terms.

Milestones

1. (§3, p. 5) $\bar r^j\in\operatorname{recc}(C)$ for every $j\in N_1$.
2. (Proposition 5) For $k\in N_2$, $S^C_k=\{\bar x\}+\operatorname{conv}\big(\bigcup_{j\in N_0^{\mathrm c}}(\alpha_j,\beta_j)\bar r^j\big)+(-\infty,0]\bar r^k+\operatorname{recc}(C)$.
3. (Lemma 2) For $a,c\in\mathbb{R}^s_+$ with $\sum_i a_i>0$ there is $\theta\in\mathbb{R}^{s+1}_+$ with $\sum_{i=0}^s\theta_i=1$ and $a_i\theta_0=c_i\theta_i$ for $i=1,\dots,s$.
4. (Proof of Theorem 5) $T^C\subseteq S^C_k$ for every $k\in N_2^0$.
5. (Proof of Theorem 5) $T^C=\bigcap_{k\in N_2^0}S^C_k$.

Significance

Theorem 5 turns the nonconvex set $P^B\setminus T^C$ into a finite union of sets with explicit generators. By the paper's Theorem 2, $P^B\setminus T^C$ has the same closed convex hull as $P^B\setminus C$, so valid inequalities for the disjunction are valid for the reverse convex set and lose nothing in the limit. The paper then relaxes each term to a polyhedron (§4.4), and a cut-generating linear program over the union separates candidate points; when $C$ is bounded the disjunction collapses to the two-term disjunction of the paper's Theorem 1. The disjunction is therefore the bridge between the geometry of $C$ (its recession cone and the exit parameters along the basis rays) and polyhedral cut generation.

The result is proved in the paper (arXiv:1901.02112v5, pp. 17–18; Mathematics of Operations Research, 2022). It has no machine-checked proof. Formalizing it checks the extended-real conventions for $\alpha_j,\beta_j$, the treatment of empty and unbounded segments, and the role of the recession cone, all of which the paper handles in prose. The definitions of the basis cone, the exit parameters and the recession cone are reusable for other intersection-cut results on the platform.

Difficulty

The inclusion $T^C\subseteq\bigcap_k S^C_k$ is immediate from the definitions. The reverse inclusion is the substance: a point lying in every term $S^C_k$ comes with $|N_2|+1$ unrelated representations, one per term, each using different segment parameters, a different multiple of $-\bar r^k$ and a different recession direction. A point of $T^C$ needs a single representation with all segment parameters inside $(\alpha_j,\beta_j)$ and no negative multiples of the rays. A naive average of the representations keeps the negative components along the rays $\bar r^k$, so it does not land in $T^C$. The rewriting of $S^C_k$ in Proposition 5 also needs care: it replaces $[0,\beta_j)$ by $(\alpha_j,\beta_j)$ inside a convex hull, and absorbs the rays of $N_1$ into the recession cone, which holds only because $C$ is open.

Formalization scope

Vectors are functions $\iota\to\mathbb{R}$ on a finite index type $\iota$ (the paper's $\{1,\dots,n\}$). The basis is the published Disjunctive.GeneralDisjunctions.IsTableau (a genuine tableau of $Ax=b$, with $B,N$ a partition and $\bar x_N=0$) together with $\operatorname{rank}A=m$, and the extreme rays are the published Disjunctive.GeneralDisjunctions.extremeRay. $P^B$ is defined, as on the page, by the tableau equations and $x_N\ge 0$. The exit parameters $\alpha_j,\beta_j$ are EReal-valued infima and suprema over real parameters, so the empty set gives $+\infty$ and $-\infty$ and an unbounded set gives $\beta_j=+\infty$; segments quantify over real $\lambda$ compared with extended-real endpoints. $N_0,N_1,N_2$ are filters of $N$, and $N_0^{\mathrm c}=N_1\cup N_2$. The index $0$ of $N_2^0$ is encoded by stating the term $S^C_0$ separately from the terms $S^C_k$, $k\in N_2$. The recession cone is the universal-quantifier cone, which is the whole space for $C=\emptyset$; in that case every set in the goal is empty or $P^B$ and the identity is $P^B=P^B$.

All hypotheses are the paper's: $C$ open and convex, $A$ of full row rank (§2), $\bar x\notin\operatorname{cl}(C)$ (§3), and Assumption 2 (§4). One generalization: the basic solution need not be feasible ($\bar b\ge 0$ is not imposed); the paper's own Example 2 uses an infeasible basic solution and the proof of Theorem 5 does not use feasibility.

Real-valued $\alpha_j,\beta_j$ (where an empty or unbounded parameter set returns $0$), segments with endpoints converted to reals, or an encoding in which $N_2$ is always empty would trivialize the statement; the extended-real definitions rule these out, and a sorry-free check confirms that the hypotheses are satisfiable with $N_2\neq\emptyset$ (one variable, $C=\{1<x<2\}$).

The development needs Minkowski sums and convex hulls of unions in $\mathbb{R}^n$, recession cones of open convex sets, and a Farkas-type alternative (for Lemma 2); the platform's LinearOptimization.farkas_lemma is available. Proofs of the milestones in any order are welcome; Lemma 2 is self-contained.

Selected references

• E. Towle and J. Luedtke, Intersection disjunctions for reverse convex sets, arXiv:1901.02112v5, 2020; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1901.02112v5
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Operations Research 19(1), 1971. https://doi.org/10.1287/opre.19.1.19
• E. Balas, Disjunctive programming, Annals of Discrete Mathematics 5, 1979. https://doi.org/10.1016/S0167-5060(08)70342-X
• M. Conforti, G. Cornuéjols, G. Zambelli, Integer Programming, Springer, 2014. https://doi.org/10.1007/978-3-319-11008-0

Motivation

A creator-side experiment on a short-video platform may assign treatment to individual videos while measuring outcomes over a viewer's whole session. A treated video can alter what the viewer watches next, so its effect may persist beyond the immediate reward. The paper studies this form of interference using a Markov decision process and asks how well data from a per-video experiment estimate the effect of treating every video instead of none. Its motivating application is an experiment at Douyin, where viewer state includes attention and other factors that need not be observed by the estimator. Farias et al., 2023 give an estimator based on reward-to-go and a quantitative bias bound for an absorbing-session model.

The distinction matters for experimental design: the usual inverse-propensity estimate weights only the reward received immediately after an assigned action. In this setting it can omit the effect of that action on later rewards. The paper's Differences-in-Qs (DQ) statistic instead weights the remaining reward in the session after each assignment. The mission focuses on the theorem that quantifies the resulting bias in the finite absorbing model of Sections 3–5.

Setting

Let $S$ be a finite state set and let the actions be control $0$ and treatment $1$. An action $a$ has a stochastic transition matrix $P_a(s,s')$ and conditional mean reward $r(s,a)$. The initial state has probability law $\rho_{\rm init}$. A stationary policy $\pi$ assigns action probabilities at each state; its induced transition matrix is $P_\pi(s,s')=\sum_a\pi(s,a)P_a(s,s')$. Global control $\pi_0$ always selects $0$, global treatment $\pi_1$ always selects $1$, and the experiment $\pi_{1/2}$ independently selects each action with probability one half at each step. Thus $P_{\pi_{1/2}}=(P_0+P_1)/2$.

A path consists of successive state-action pairs $(s_t,a_t)$. Its law begins with $s_0\sim\rho_{\rm init}$, draws each action from $\pi(s_t)$, and then draws $s_{t+1}$ from $P_{a_t}(s_t,\cdot)$. The total expected reward is $J_\pi=\sum_{t\ge0}\mathbb E_\pi[r(s_t,a_t)]$. The target average treatment effect is ${\rm ATE}=J_{\pi_1}-J_{\pi_0}$.

The session has a common absorbing class $S_{\rm abs}$: under each policy of interest, transitions from this class stay in it, and its mean rewards vanish. Assumption 1 bounds the expected number of steps spent outside that class, from every initial state, strictly by $T_{\rm abs}$. These conditions make the infinite total-reward quantities meaningful. The paper writes a stronger absorbing-row equation that does not define a stochastic row when the class contains more than one state; the formalization uses the closed-class interpretation and records the discrepancy for review.

For a path from the half-treatment policy, the DQ estimator assigns weight $2$ or $-2$ to the reward remaining after each treatment or control action, respectively. With the path stopped at $H$, write that statistic as $\widehat{\rm ATE}^{(H)}_{\rm DQ}$. The infinite-horizon expectation is defined through the limit of its finite-path expectations, not through a value-function identity.

Formalization targets

The goal is Theorem 1 of Farias et al., in the absorbing regime. If every row of $P_1-P_0$ has total-variation norm at most $\delta$ and $r_{\max}=\max_{s,a}|r(s,a)|$, then the estimator expectations converge to $L$ and

The milestone targets include the matrix resolvent identities of Lemmas 1–2, Theorem 2's finite-order expansion of the total-reward value functional, and Corollary 1's absorbing-case remainder bound. They also identify trajectory reward with the value functional and connect the trajectory DQ statistic to the first-order expansion. The listed order follows these mathematical dependencies. The mission does not assert Theorem 2's discounted, average-reward, or finite-horizon cases, which the goal does not need.

Significance

The bound distinguishes the DQ estimator from an immediate-reward estimate: its bias is at most quadratic in the row distance $\delta$, with explicit dependence on expected session length and reward magnitude. It gives a criterion for when a per-video experiment can approximate the all-treatment versus all-control effect despite changes to later states. This is a statement about expected estimator bias; it does not by itself give a variance or finite-sample confidence bound.

The formal development separates three objects that are easy to conflate: the statistic computed from a trajectory, its expectation under the experimental policy, and a value-functional expansion used to analyze that expectation. The matrix identity corresponding to Lemma 1 is already machine checked on Prove2Me as MarkovEntanglement.resolvent_identity. The goal and other mission statements are compilation-checked drafts with proof obligations still open. A completed formalization would establish their convergence and equality claims as well as the printed bias constant, and would leave reusable finite-state path and absorbing-value definitions.

Difficulty

The immediate-reward estimate evaluates outcomes under the experimental state distribution, while ATE compares outcomes under two different state distributions. Weighting each current reward cannot generally account for that mismatch. The DQ statistic incorporates reward-to-go, but its infinite double sum must be related to a convergent trajectory expectation before any bias inequality applies. The central quantitative issue is to control how changing a policy perturbs the total-reward functional across repeated transitions, with the exact $T_{\rm abs}^{3}\delta^{2}$ scale. A direct comparison of one-step rewards alone does not yield that order.

Formalization scope

States and actions are finite. Transitions are nonnegative and row-stochastic, the initial law is a probability vector, and policies are stationary probability kernels. The goal's actions are Fin 2, with $1$ treatment and $0$ control. Path expectations are finite sums; infinite expected rewards and Q-functions use real series. The absorption-time condition asserts convergence with HasSum and a strict bound from every state. Its closed-class, zero-reward conditions apply under $\pi_0$, $\pi_1$, and $\pi_{1/2}$. The reward field records conditional means, sufficient for the expectation claims.

Here $D_{\rm TV}$ is the $\ell_1$ row norm $\sum_{s'}|P(s,s')-Q(s,s')|$. The paper does not define its normalization; with the alternative half-$\ell_1$ convention the printed Theorem 1 constant fails. This choice is part of the statement, not a hidden rescaling. The truncated estimator is formed from path rewards exactly as equation (4) prescribes; defining its expectation as the first-order expansion would erase the mission's main identification step. The paper's Section 5.3 display also places the outer value functionals at $\pi_1$ and $\pi_0$, while its claimed identity and Theorem 2 require $\pi_{1/2}$; the milestone states that corrected reading and retains the printed display in its provenance.

Useful contributions include convergence of finite-path expectations, the absorbing total-reward resolvent theory, and the exact finite-order remainder estimate. These definitions and lemmas can also support other finite absorbing policy-evaluation problems.

Selected references

• Vivek F. Farias, Hao Li, Tianyi Peng, Xinyuanyang Ren, Huawei Zhang, and Andrew Zheng, Correcting for Interference in Experiments: A Case Study at Douyin, RecSys, 2023; arXiv:2305.02542v1.

Motivation

Quadratic hedging chooses a self-financing trading strategy that minimizes the expected squared difference between its terminal value and a payoff $H$; with $H$ constant it becomes mean–variance portfolio selection. The classical theory works in discounted prices: one asset is a risk-free numeraire, and optimal strategies are written in terms of the remaining assets (Černý and Kallsen 2007; the paper refers to Schweizer's 2010 encyclopedia entry Mean–variance hedging for an overview). Černý, Czichowsky and Kallsen drop that assumption. In their market no asset need be risk-free, and they want formulas for the optimal strategy that do not depend on which asset is used as the unit of account (arXiv:2110.09416v4, §1).

In their feedback formula (Theorem 4.1, p. 15) the optimal strategy is built from two processes. One is the adjustment process $a$, which corrects the hedging error accumulated so far. The other is the pure hedge $\xi$, which offsets the fluctuations of the claim's value process. At each time both are minimizers of a finite-dimensional quadratic problem with one linear budget constraint. The covariance-type matrix in that problem may be singular, for instance whenever a risk-free asset is present. So the minimizers are not unique and ordinary matrix inversion does not describe them. Theorem 4.3 of the paper (p. 16) gives explicit formulas for the whole solution sets, and Appendix A (pp. 24–28) proves the linear algebra behind them. That linear algebra is a general result on affinely constrained quadratic minimization with singular data, built on the oblique-projector analysis of Černý 2009.

Setting

Fix a time and a state. The data of the pointwise problem are:

• a symmetric positive semidefinite matrix $C=\tilde c^{S\star}\in\mathbb R^{d\times d}$, the modified second characteristic of the price process $S$ under the opportunity-neutral measure;
• vectors $b=b^{S\star}$ (drift), $s=S_-\neq0$ (current prices) and $u=\tilde c^{SV\star}$ (covariation of prices with the claim's value process) in $\mathbb R^d$, and a scalar $v=V_-$.

Portfolios $\vartheta$ are row vectors and price-type quantities are column vectors, as in the paper (§2, p. 6). $R(\cdot)$ is the column space and $N(\cdot)$ the null space of a matrix. Every matrix exponent $^{-1}$ in the paper denotes the Moore–Penrose pseudoinverse: the unique $X$ with $AXA=A$, $XAX=X$, $(AX)^{\mathsf T}=AX$, $(XA)^{\mathsf T}=XA$ (p. 24, (A.2)). The two problems are

where an $\operatorname{arg\,min}$ is the set of all global minimizers over the whole hyperplane (possibly empty). With $m=I-ss^{\mathsf T}/(s^{\mathsf T}s)$ and $p=(mCm)^{-1}$ the paper defines

The general problem of Appendix A is to minimize $q(x)=x^{\mathsf T}Cx-2x^{\mathsf T}F$ over $\{x: Ax=b\}$ with $b\in R(A)$, where $M=I-A^{-1}A$ and $J=(MCM)^{-1}$.

Formalization targets

Goal: Theorem 4.3

1. $\Xi_a\neq\varnothing$ if and only if $b\in R(C)+R(s)$; in that case $\Xi_a=a+N(C)\cap N(s^{\mathsf T})$ and $a$ is its minimum-norm element.
2. $\Xi_\xi=\xi+N(C)\cap N(s^{\mathsf T})$, and $\xi$ is its minimum-norm element.
3. If $s\in R(C)$: $\;a=b^{\mathsf T}C^{-1}-\bigl(1+b^{\mathsf T}C^{-1}s\bigr)\dfrac{s^{\mathsf T}C^{-1}}{s^{\mathsf T}C^{-1}s}$ and $\xi=u^{\mathsf T}C^{-1}+\bigl(v-u^{\mathsf T}C^{-1}s\bigr)\dfrac{s^{\mathsf T}C^{-1}}{s^{\mathsf T}C^{-1}s}$.
4. If $s\notin R(C)$: with $\bar m=I-CC^{-1}$, $\alpha=s^{\mathsf T}\bar m/(s^{\mathsf T}\bar ms)$, $r=\alpha b$,

and $\alpha s=1$, $\alpha C=0$.

Milestones (Appendix A and the proof of Theorem 4.3)

In attack order: existence and uniqueness of the pseudoinverse (published, proved); Proposition A.1 (pseudoinverse rules); Proposition A.3 (affinely constrained least squares); (A.8) and $JCJ=J$; (A.14)–(A.15); the completed square (A.16); Theorem A.4(1) (bounded below iff $F\in R(A^{\mathsf T})+R(C)$); A.4(2) (all minimizers are $\hat x+N(C)\cap N(A)$ with $\hat x=JF+(I-JC)A^{-1}b$ of minimum norm); A.4(3) (value identities); Lemma A.5; A.4(4) (formulas (A.6)–(A.7) through the oblique projector onto $\bar Y$ along $N(A)$); and the range fact $\tilde c^{SV\star}\in R(\tilde c^{S\star})$ used in the proof of Theorem 4.3.

Significance

Theorem 4.3 gives closed forms for both ingredients of the optimal hedge. It covers markets with and without a risk-free asset in one formula, because $s\in R(C)$ and $s\notin R(C)$ are the only two cases. In the second case $\alpha$ is a fully invested portfolio with zero instantaneous variance. The paper uses them in its efficient-frontier analysis (§5) and its examples (§6). Theorem A.4 does not depend on finance. It gives a complete solution of a positive semidefinite quadratic program with linear equality constraints: when it is solvable, the full set of minimizers, and the minimum-norm minimizer. Its proof needs nothing beyond finite-dimensional linear algebra.

The paper proves all of these results. Proposition A.3 is taken from Černý (2009), and v4 (7 July 2025) strengthened Proposition A.3 and Theorem A.4 after the journal version (doi:10.1287/moor.2023.1374). The mission cites only v4. None of the statements has a machine-checked proof. The Penrose predicate and Penrose's existence and uniqueness theorem are already on Prove2Me as proved results. Mathlib at the pinned revision has no Moore–Penrose pseudoinverse, so the pseudoinverse calculus built here can be reused.

Difficulty

With a singular $C$, completing the square with an inverse is not available. On the affine set, the quadratic part can vanish in some directions while the linear part keeps decreasing. The boundedness criterion has to detect exactly these directions. Under that criterion, a formula has to describe every minimizer, not just one stationary point. The constraint brings in the projector $M=I-A^{-1}A$, and $C$ need not commute with it. As a result, the relevant projector $JC$ is oblique, not orthogonal, and the obvious guess $C^{-1}F$ plus a correction fails. Exhibiting one feasible point with zero gradient does not prove the set equality, the minimum-norm property, or the case formulas (A.7). The case $s\notin R(C)$ needs its own treatment through $\bar m$.

Formalization scope

• Vectors are Fin d → ℝ with ⬝ᵥ, and matrices are Matrix (Fin m) (Fin n) ℝ. A row vector times a matrix is written x ᵥ* M and a matrix times a column vector M *ᵥ x, matching the paper's printed order. Column and null spaces are LinearMap.range/LinearMap.ker of Matrix.toLin'.
• Each pseudoinverse is an explicit matrix with the hypothesis LocalDistanceNetwork.IsMoorePenroseInverse (the four equations (A.2)). Because the pseudoinverse exists and is unique, this is the same as "the" pseudoinverse. Lean's ⁻¹ is used only on real scalars, never on a singular matrix.
• Positive semidefinite means Matrix.PosSemidef, which includes symmetry. Argmin sets range over the whole affine set or hyperplane. Minimum norm compares squared Euclidean norms over the whole set.
• Theorem 4.3 is stated pointwise: arbitrary $C\succeq0$, $b$, $s\neq0$, $u\in R(C)$, $v$. The paper's setting gives $s\neq0$ implicitly; without it, part (1) is false. The paper's "in the setting of Theorem 4.1" gives $u\in R(C)$, and the range-fact milestone derives it from positive semidefiniteness of the joint characteristic. The stochastic construction of Theorem 4.1 is out of scope. Of the last sentence of part (4), only its algebraic content $\alpha s=1$, $\alpha C=0$ is formalized.
• Appendix A states Propositions A.1 and A.3 and Lemma A.5 over $\mathbb C$. They are posed over $\mathbb R$, which is the case Theorems A.4 and 4.3 use. The two cases of (A.7) are not exhaustive when there are two or more constraints, and each is stated under its own hypothesis.
• Ruled out: an argmin defined from the advertised answer, a minimizer taken as a free parameter, and Mathlib's matrix inverse (which is $0$ on singular matrices) in place of the pseudoinverse. Each of these would make the statements trivial or change them.
• Needed infrastructure: a Moore–Penrose calculus for real matrices (Proposition A.1), ranges and kernels of products, orthogonal and oblique projectors, and minimization of quadratic forms on affine sets. All of it is reusable outside this mission, and contributions to any milestone are welcome.

Selected references

• A. Černý, C. Czichowsky, J. Kallsen, Numeraire-invariant quadratic hedging and mean–variance portfolio allocation, arXiv:2110.09416v4, 2025 (journal version: Mathematics of Operations Research 49(2), 2024). https://arxiv.org/abs/2110.09416v4
• A. Černý, Characterization of the oblique projector $U(VU)^\dagger V$ with application to constrained least squares, Linear Algebra and its Applications 431(9), 2009, 1564–1570. https://mathscinet.ams.org/mathscinet-getitem?mr=2555057
• A. Černý, J. Kallsen, On the structure of general mean–variance hedging strategies, Annals of Probability 35(4), 2007, 1479–1531. https://mathscinet.ams.org/mathscinet-getitem?mr=2330978
• A. Ben-Israel, T. N. E. Greville, Generalized Inverses: Theory and Applications, 2nd ed., CMS Books in Mathematics, Springer, 2003. https://doi.org/10.1007/b97366

Motivation

An investor can improve a portfolio by adding a zero-cost combination of long and short positions. Ordinary arbitrage asks whether such a combination pays nonnegatively in every outcome and positively in some outcomes. That test is restrictive when payoffs have both gains and losses. Arvanitis and Post instead ask whether one overlay portfolio raises expected utility for every admissible risk preference and every benchmark portfolio in a specified class. This gives an asset-pricing question that acknowledges uncertainty about investors' preferences and starting positions. The authors use the concept to study factor portfolios and transaction costs in their 2022 working paper Ordering Arbitrage Portfolios and Finding Arbitrage Opportunities (AUEB Department of Economics Working Paper 04-2022), published as Generalized Stochastic Arbitrage Opportunities in Management Science in 2024.

The target is the paper's Theorem 2.3.1, an existence condition for a pricing system. The working-paper statement needs a finite-generation condition on the utility class for its converse. The resulting mission records the corrected theorem and the general direction that does hold for arbitrary admissible utility classes.

Setting

There are finitely many base assets, indexed by $i=1,\ldots,N$. Their one-period payoff vector is $x\in\mathbb R^N$ with probability law $F$, supported on $[\mathrm{lo},\mathrm{hi}]^N$ for finite $\mathrm{lo}<\mathrm{hi}$. A benchmark position $\kappa\in K\subseteq\mathbb R^N$ costs $p^\mathsf T\kappa=c>0$. The benchmark set $K$ is closed and bounded; it can contain many portfolios and need not be convex. An overlay $\delta$ is feasible when $A\delta\leq a$, where $A$ has $R$ rows. Thus $\Delta=\{\delta:A\delta\leq a\}$ is the bounded overlay polytope, and $0\in\Delta$ is the passive choice.

The utility class $U$ contains continuously differentiable, strictly increasing, strictly concave functions $u:\mathbb R\to\mathbb R$. It is convex and uniformly bounded on bounded payoff intervals. For an overlay $\delta$, the expected utility increment relative to benchmark $\kappa$ is

A strict stochastic arbitrage opportunity is a single feasible overlay that improves every benchmark for every admissible utility. The set is

The paper's candidate stochastic discount factors are $M_{U,K}=\{x\mapsto d\,u'(x^\mathsf T\kappa):d>0,\ (u,\kappa)\in U\times K\}$. A factor $m$ assigns the present-value vector $E_F[m(x)x]$ to the base assets. The relevant polar cone is written in the paper's constraint coordinates as $\Delta^*=\{A^\mathsf T\sigma:\sigma\geq0,\ a^\mathsf T\sigma\leq0\}$. This representation encodes the overlay inequalities and their shadow prices.

Formalization targets

General pricing implication

For the paper's general convex class $U$, the existence of a mixture of marginal-utility discount factors whose present value lies in $\Delta^*$ rules out every strict stochastic arbitrage opportunity:

Corrected existential condition

If $U$ is the convex hull of a finite set of admissible utility functions, the converse is also claimed:

This is the mission's goal. The benchmark set remains any closed bounded set satisfying the budget restriction. ### Supporting milestones

The milestones follow the proof of Theorem 2.3.1 (pp. 34–35): the first-order (Karush–Kuhn–Tucker) condition for optimality on the segment $\kappa+\theta\delta$, $\theta\in[0,1]$,

the concavity bound $D(u,\kappa,\delta,F)\le E_F[u'(x^\mathsf T\kappa)x]^\mathsf T\delta$; the convexification step (9)–(10) in its pointwise form; the minimax reversal (10)–(11) and the linear-programming duality (11)–(13), both available as proved platform theorems; and the general pricing implication above.

Significance

The condition translates absence of a portfolio improvement shared by all the specified investors into the existence of a discount factor with constrained asset values. In markets with transaction costs, the cone can permit price intervals rather than one exact price vector. This connects an investor-facing arbitrage test to restrictions that can be checked through the market's linear constraints. The working paper (§2.3, p. 11) discusses that interpretation and its factor-investing application.

The result is a published mathematical claim but, in this representation, still a Lean proof obligation. A formal development would produce reusable definitions of strict utility-based arbitrage and marginal-utility pricing, plus machine-checked proofs of the valid pricing implication and the corrected converse. The two general minimax and linear-duality results referenced here already have proved Prove2Me statements; the paper-specific statements in this mission are draft goals and have no machine-checked proofs yet.

Difficulty

The converse has a quantifier problem: no single overlay can improve every utility and benchmark, even though different utilities may reject different overlays. Treating one failed endpoint comparison as a first-order optimality condition does not resolve that problem. In fact, a concave expected-utility function may end below its starting value at $\theta=1$ while initially increasing as $\theta$ leaves zero. The paper's proof makes that invalid identification. Its unrestricted utility class also permits limiting behavior that defeats the asserted converse. The finite-generation condition in the goal prevents that particular failure while retaining a nontrivial family of preferences and a general compact benchmark set.

Formalization scope

Lean uses Fin N → ℝ for payoffs and portfolio positions, a probability measure for $F$, and Bochner integrals for expectations. The almost-sure box-support condition makes the utility and marginal-utility expressions integrable under the stated continuity assumptions. The matrix inequality $A\delta\leq a$ defines $\Delta$ directly; $\Delta^*$ is the paper's $A^\mathsf T\sigma$ representation, rather than an abstract inequality definition. The set of discount factors allows every positive scale $d$ and takes the ordinary finite convex hull. The utility derivative is deriv u, justified by the continuously differentiable assumption. Lean's lo and hi name the support endpoints and aVec names the constraint right-hand side; the paper uses $a$ for both roles.

The corrected goal's finite generation of $U$ is an explicit addition to the printed Theorem 2.3.1. To see the need, take one riskless payoff $x_1=1$, a second payoff $x_2\in\{2,-1\}$ with equal probabilities, one benchmark $(1,0)$, and overlays $(0,t)$ for $0\leq t\leq1$. A convex class generated by increasingly steep, smooth, strictly concave utilities has no strict SAO, yet every candidate marginal-utility discount factor at that benchmark is a positive constant and assigns positive value to the second asset, outside $\Delta^*$.

The SAO predicate remains the actual difference of two expected utilities. Defining it through the derivative inequality would erase the principal economic question. Supporting work may establish bounded-support integration, finite-dimensional compactness, convex-hull behavior, and the relation between the matrix cone and the overlay inequalities; these are reusable for other one-period pricing models. A result that only assumes the pricing restriction, or changes the benchmark set to a singleton, does not settle this goal.

Selected references

• Stelios Arvanitis and Thierry Post, Ordering Arbitrage Portfolios and Finding Arbitrage Opportunities, Athens University of Economics and Business Department of Economics Working Paper 04-2022, March 2022; published as the Management Science article below. Theorem 2.3.1 is on printed p. 11 (PDF 12), with proof on printed pp. 34–35 (PDF 35–36).
• Stelios Arvanitis and Thierry Post, Generalized Stochastic Arbitrage Opportunities, Management Science, 2024, DOI. The mission uses the working-paper numbering and pagination.

Motivation

Empirical risk minimization (ERM) is the inductive principle behind most of statistical learning: a learning machine picks, from a set of functions, the one with the smallest average loss on the training data, in place of the one with the smallest expected loss under the unknown distribution. Whether this substitution is justified is the first question of learning theory, and Chapter 2 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) answers it.

The history is short. Vapnik and Chervonenkis gave the entropy criterion for uniform convergence of frequencies to probabilities in 1968 and published the proof in 1971 (Theory Probab. Appl. 16, 264–280); in 1981 they extended it to uniformly bounded real functions (Theory Probab. Appl. 26, 532–553); in 1989 they proved the key theorem, which reduces consistency of ERM to uniform one-sided convergence. The book states all of these results without proofs (Preface, p. xi); the proofs are in Vapnik, Statistical Learning Theory (Wiley 1998) and the cited papers.

Setting

Let $F$ be a probability measure on a measurable space $Z$, and let $Q(z,\alpha)$, $\alpha\in\Lambda$, be a set of real functions on $Z$ indexed by an arbitrary parameter set $\Lambda$. The risk of $\alpha$ is $R(\alpha)=\int Q(z,\alpha)\,dF(z)$. For an i.i.d. sample $z_1,\dots,z_\ell$ drawn from $F$, the empirical risk is $R_{\mathrm{emp}}(\alpha)=\frac1\ell\sum_{i=1}^\ell Q(z_i,\alpha)$. Probabilities $P$ are taken under the product measure $F^\ell$.

For $c\in\mathbb R$ let $\Lambda(c)=\{\alpha\in\Lambda : R(\alpha)>c\}$. The ERM method is nontrivially consistent (from p. 38 on simply "consistent") if for every $c$ with $\Lambda(c)$ nonempty,

Removing the functions of smallest risk rules out consistency that is caused only by a single function lying below all the others. Uniform one-sided convergence means $\lim_{\ell\to\infty}P\{\sup_{\alpha}(R(\alpha)-R_{\mathrm{emp}}(\alpha))>\varepsilon\}=0$ for all $\varepsilon>0$ (2.4). Uniform two-sided convergence is the same with $|R(\alpha)-R_{\mathrm{emp}}(\alpha)|$ (2.6).

For a set of bounded functions $A\le Q(z,\alpha)\le B$, the random VC entropy $H^\Lambda(\varepsilon;z_1,\dots,z_\ell)=\ln N^\Lambda(\varepsilon;z_1,\dots,z_\ell)$ is the logarithm of the size of a minimal $\varepsilon$-net, in the metric $C$ (maximum over the sample points), of the vectors $(Q(z_1,\alpha),\dots,Q(z_\ell,\alpha))$. The net is internal: its points are themselves vectors of the set. The VC entropy is $H^\Lambda(\varepsilon,\ell)=E\,H^\Lambda(\varepsilon;z_1,\dots,z_\ell)$. For indicator functions, $N^\Lambda(z_1,\dots,z_\ell)$ is the number of distinct binary vectors on the sample. From it the book defines the entropy $H^\Lambda(\ell)=E\ln N^\Lambda$, the annealed VC entropy $H^\Lambda_{\mathrm{ann}}(\ell)=\ln E N^\Lambda$, and the growth function $G^\Lambda(\ell)=\ln\sup_{z_1,\dots,z_\ell}N^\Lambda$.

Formalization targets

Goal: Theorem 2.1, the key theorem (p. 38)

If $A\le R(\alpha)\le B$ for all $\alpha\in\Lambda$, then

Only the risks are bounded, not the functions. The constants $A$ and $B$ are arbitrary, and they appear only in the hypothesis.

Milestones

1. Section 2.3.1, p. 41. For a finite set of integrable functions, $\xi^\ell=\sup_\alpha|R(\alpha)-R_{\mathrm{emp}}(\alpha)|\to0$ in probability.
2. Section 2.7, pp. 55–56. For indicator functions, $H^\Lambda(\ell)\le H^\Lambda_{\mathrm{ann}}(\ell)\le G^\Lambda(\ell)$ for every $\ell$.
3. Section 2.6.1, p. 50. For indicator functions, $H^\Lambda(\ell)/\ell$ is non-increasing for $\ell\ge1$.
4. Theorem 2.3, p. 45. For bounded real functions, uniform two-sided convergence holds iff $\lim_{\ell\to\infty}H^\Lambda(\varepsilon,\ell)/\ell=0$ for all $\varepsilon>0$ (2.10).
5. Corollary of Theorem 2.3, p. 45. The indicator case, $\lim H^\Lambda(\ell)/\ell=0$. It is already proved on the platform as VapnikChervonenkis.Entropy.theorem4_entropy_criterion and is referenced here.

Significance

The key theorem says that consistency of ERM is decided by the worst function of the set, in the one-sided sense of (2.4). Every analysis of ERM must therefore control a supremum over the whole set, a worst-case analysis (p. 39). This turns the question of consistency into the question of uniform laws of large numbers. Theorem 2.3 and its corollary answer that question through the VC entropy. The three capacity concepts $H^\Lambda\le H^\Lambda_{\mathrm{ann}}\le G^\Lambda$ underlie the "three milestones" of §2.7: consistency, a fast rate of convergence, and distribution-free guarantees. These are also the objects of the later missions of this series.

The platform already has the 1971 indicator-class criterion (Proved) and the related entropy-rate lemmas for event classes. It has no real-valued loss class with a parameter set, no notion of nontrivial consistency, no key theorem, and no VC entropy built from $\varepsilon$-nets of real functions. This mission supplies those definitions with the book's conventions, and states the key theorem and its neighbours as open targets.

Difficulty

The theorem is an equivalence between a statement about infima over the shrinking families $\Lambda(c)$ and a statement about one supremum over all of $\Lambda$. Neither the functions nor the empirical risks are bounded; only the risks are. The empirical infimum over $\Lambda(c)$ may therefore be $-\infty$, and no compactness of $\Lambda$ is available. Single-function laws of large numbers control each $\alpha$ separately, but they do not control the supremum: for an infinite $\Lambda$ they are not enough, and that is the content of the chapter. For Theorem 2.3, the necessity direction is a genuine probabilistic argument about the growth of covering numbers, and the measurability of suprema over an uncountable $\Lambda$ must be handled explicitly.

Formalization scope

All declarations are in the namespace NatureSLT.Consistency. The parameter set $\Lambda$ is an arbitrary Lean type and $Q:\Lambda\to Z\to\mathbb R$. A sample of size $\ell$ is Fin ℓ → Z under Measure.pi (fun _ => F), and a probability is a value of that measure in $[0,\infty]$. The risk is a Bochner integral, and every theorem that uses it assumes each $Q(\cdot,\alpha)$ integrable. Logarithms are natural. The minimal $\varepsilon$-net is internal and uses the metric $C$, as in the book's footnote 3; it is not Mathlib's external covering number. "Monotonically decreases" (p. 50) is read as non-increasing.

Suprema of deviations and the infimum of empirical risks over $\Lambda(c)$ are taken in the extended reals, so they are genuine values and never a junk default. The infimum of the risks is a real infimum over a nonempty $\Lambda(c)$, which is bounded below by $c$. No extended-real subtraction occurs: the event $|X-a|>\varepsilon$ is written as $X<a-\varepsilon$ or $a+\varepsilon<X$.

The book's "some (technical) conditions of measurability" are explicit hypotheses. In Theorem 2.1, $\sup_\alpha(R-R_{\mathrm{emp}})$ and $\inf_{\Lambda(c)}R_{\mathrm{emp}}$ are measurable functions of the sample. In Theorem 2.3, $Q(\cdot,\alpha)$, $\xi^\ell$, the half-sample deviation and the random VC entropy are measurable. For indicator classes, $N^\Lambda$ is measurable.

A trivializing formalization is ruled out. Consistency is the nontrivial notion (2.3), quantified over every nonempty $\Lambda(c)$, not the classical one that a minorizing function satisfies trivially. The probability of a non-measurable event is never read as $0$: Lean evaluates it as an outer measure.

Beyond the paper. One strengthened variant is posed, key_theorem_strong (finding F1). It is Theorem 2.1 with the two measurability hypotheses removed and probabilities read as outer probabilities. The known argument needs only monotonicity and finite subadditivity of the probability of events, together with the weak law of large numbers for a single integrable function, so measurability is never used.

Contributions are welcome on any item. Reusable beyond this mission are the risk and empirical-risk definitions, uniform one- and two-sided convergence, and the VC entropy of a real class. Theorems 2.2 (maximum likelihood), 2.4 (one-sided convergence through minorant classes), 2.5 and 2.6 (nonfalsifiability) are not part of this mission.

Selected references

• V. N. Vapnik, The Nature of Statistical Learning Theory, 2nd ed., Springer, 2000. doi:10.1007/978-1-4757-3264-1
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998. ISBN 978-0-471-03003-4.
• V. N. Vapnik and A. Ya. Chervonenkis, "On the uniform convergence of relative frequencies of events to their probabilities", Theory Probab. Appl. 16 (1971), 264–280. doi:10.1137/1116025
• V. N. Vapnik and A. Ya. Chervonenkis, "Necessary and sufficient conditions for the uniform convergence of means to their expectations", Theory Probab. Appl. 26 (1981), 532–553. doi:10.1137/1126059
• V. N. Vapnik and A. Ya. Chervonenkis, "The necessary and sufficient conditions for consistency of the method of empirical risk minimization", Yearbook of the Academy of Sciences of the USSR on Recognition, Classification, and Forecasting 2 (1989), 217–249; English translation in Pattern Recognition and Image Analysis 1(3) (1991), 284–305.

Motivation

A multi-armed bandit in the sense of Gittins is a sequential allocation problem: several independent Markov reward processes compete for a single resource, at each decision time exactly one of them is operated, and the goal is to maximize the expected total discounted reward. The Gittins index theorem says that it is optimal to operate, at every decision time, a process of largest index, where the index of a process depends only on that process. Chapter 4 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011, doi:10.1002/9780470980033), extends it to superprocesses, precedence constraints and arrivals.

In practice an index is rarely computed exactly. It is approximated numerically, or a heuristic policy is shown to be close to an index policy, so one needs to know how much reward is lost when a policy is only approximately an index policy. Section 4.10 of the book answers this for two notions of approximation. For ε-index* policies, which choose whole stages whose reward rate is within ε of the largest index, Corollary 4.16 bounds the loss by ε times the total discounted time. This mission formalizes Corollary 4.16 and the freezing-rule and promotion-rule lemmas of §4.5 on which its proof rests. The bound goes back to Katehakis and Veinott (Math. Oper. Res. 1987).

This mission continues the public series Multi-armed Bandit Allocation Indices I–VI in the same namespace, AllocationIndices, reusing its model and definitions.

Setting

A bandit process $B$ is a Markov chain $x(0), x(1), \dots$ on a countable state space $S$ with transition kernel $P$. Each time the continuation control is applied it yields the bounded reward $r(x(t))$ and moves one step; under the freeze control it stays put and pays nothing. Decision times are $0, 1, 2, \dots$ and rewards are discounted by $a^t$ with $0 < a < 1$. For a positive stopping time $\tau$ of $B$, $R_\tau(B) = E\sum_{t<\tau} a^t r(x(t))$ and $W_\tau(B) = E\sum_{t<\tau} a^t$ are the expected discounted reward and time before $\tau$, $\nu_\tau(B) = R_\tau(B)/W_\tau(B)$, and the Gittins index is $\nu(B) = \sup_{\tau > 0} \nu_\tau(B)$ (the discrete-time index (2.6), gittinsIndex P r a x).

A freezing rule $f$ for $B$ is a nondecreasing sequence $f_0 \le f_1 \le \cdots$ in $\{0, 1, \dots\} \cup \{\infty\}$, where $f_i$ depends only on $x(0), \dots, x(i)$. The reward of process time $i$ is postponed to time $i + f_i$, and $f_i = \infty$ means it never accrues. Then

A stopping rule $\tau$ is the special freezing rule $f_i = 0$ for $i < \tau$ and $f_i = \infty$ otherwise.

A simple family $F$ of $k$ alternative bandit processes $B_1, \dots, B_k$ is operated by a policy $g$: at each decision time $g$ chooses, possibly at random and on the basis of the whole history, one process to continue, and the others are frozen. Its payoff $R_g(F)$ is the expected total discounted reward, and $R(F) = \sup_g R_g(F)$. For a positive stopping time $\tau$ of the family's history, $R_{g\tau}(F)$ and $W_{g\tau}(F)$ are the reward and discounted time accrued before $\tau$, and the index of the family is

An ε-index* policy $h$ proceeds in stages. At the start of a stage it chooses a process $B$ and a positive stopping time $\tau$ of $B$'s own evolution with $\nu_\tau(B) \ge \max_j \nu(B_j) - \varepsilon$, all indices evaluated at the current states. It continues $B$ up to $\tau$ and then repeats.

Formalization targets

Goal: Corollary 4.16 (p. 112)

For every ε-index* policy $h$, every $\varepsilon \ge 0$ and every initial state-vector $x$,

The book states $R_h(F) \ge R(F) - \varepsilon\gamma^{-1}$ in continuous-time units; $\varepsilon/(1-a)$ is the same bound in the discrete-time units of the index (2.6) (see Formalization scope).

Milestones

1. Eq. (4.8) (p. 91): for every freezing rule, $R_f(B) \le W_f(B)\,\nu(B)$.
2. Lemma 4.5 (p. 93): $\nu_f(B) \le \nu(B)$ whenever $W_f(B) > 0$.
3. Lemma 4.6(i) (p. 94): $\nu(F) = \max_j \nu(B_j)$.
4. Lemma 4.7 (p. 95), in the form (4.13): for a fixed time $\tau$ and a freezing rule with $f_i \le \tau$ (a promotion rule with respect to $\tau$),

where $R(B)$ and $W(B)$ are the reward and discounted time with no freezing. 5. Theorem 2.1 (p. 91, restated in §4.5), referenced: an index policy attains $R(F)$ (BanditAlgorithm.gittins_index_theorem, proved on the platform).

Significance

Corollary 4.16 makes the index theorem robust. Any procedure that certifies, stage by stage, a reward rate within ε of the largest index is guaranteed a payoff within $\varepsilon/(1-a)$ of optimal. Examples are a numerical index computation with error ε, or a heuristic whose stages are near-optimal stopping problems. At $\varepsilon = 0$ it is the statement that modified forwards induction policies are optimal. Lemmas 4.5–4.7 carry the freezing-and-promotion proof of the index theorem, which the book notes "comes into its own" for families that are not simple (§4.6–4.7, jobs with precedence constraints).

Status: the index theorem itself is formalized and proved on the platform (BanditAlgorithm.gittins_index_theorem). The companion bound for ε-index policies, Theorem 4.18 ($\varepsilon/(1-a)^2$ in the same units), is posed and open as AllocationIndices.eps_index_policy_near_optimal. Freezing rules, the family index (4.5) and ε-index* policies have no formal counterpart yet.

Difficulty

The obvious attempt is to repeat the interchange argument of Lemma 2.4 stage by stage. It does not work directly: an arbitrary policy $g$ interleaves the first stage of $h$ with portions of the other processes in a history-dependent way. Moving that stage to the front postpones the other processes' rewards by a random amount and advances $B$'s rewards by another. Comparing the two needs inequalities that hold for every past-measurable postponement or promotion, not just for stopping rules. These are Lemmas 4.5 and 4.7. Lemma 4.6(i) is also needed, to bound the reward rate of the rest of the family by the largest index. The stage-by-stage losses then have to be summed over infinitely many stages, each started at a random time.

Formalization scope

• Model. The published single-arm model of the series: markovChainMeasure P x, trajectory stopping times (ℕ → S) → ℕ∞, gittinsIndex, stoppedReward, stoppedTime, stoppedRatio, IsPositiveStoppingTime, BoundedReward. Families use the published MarkovBanditPolicy k T and markovBanditDiscountedValue P r a π x: all $k$ bandits share one kernel P and reward r on a common state space, which by §2.9 is no loss of generality (disjoint unions). State spaces are countable with measurable singletons, and rewards are bounded (§2.4).
• Units. The book's §4.10 bounds are in the continuous-time units of §2.8, where $W_\tau = \gamma^{-1}E(1 - a^\tau)$ and $a = e^{-\gamma}$. Here time is discrete and every index is the discrete-time index (2.6), with $W_\tau = E\sum_{t<\tau} a^t$. The conversions are:
  • The book's index is $\gamma/(1-a)$ times the discrete index. An ε-index* policy for the discrete index is therefore an $\varepsilon\gamma/(1-a)$-index* policy in the book's units, and the book's $\varepsilon\gamma^{-1}$ becomes $\varepsilon/(1-a)$ in Corollary 4.16. This is the convention of the published Theorem 4.18 item.
  • The book's $W_{f}(B) = E\sum_i a^{f_i}\int_{t_i}^{t_{i+1}} a^t\,dt$ in (4.8) becomes $E\sum_i a^{i+f_i}$.
  • The total discounted time $\int_0^\infty a^t\,dt = \gamma^{-1}$ becomes $\sum_t a^t = (1-a)^{-1}$.
• Conventions.
  • $a^\infty = 0$.
  • Freezing rules are deterministic functions of the process's trajectory (p. 93).
  • Lemma 4.5 assumes $W_f > 0$, where $\nu_f$ is defined.
  • Lemma 4.7 encodes the promotion rule $p$ by the freezing rule $f_i = \tau + p_i \in [0, \tau]$, as the book's proof does.
  • A stopping time of a family is a "still running" flag on histories that is true at time 0 and, once false, stays false.
  • $R(F, x)$ is the supremum of markovBanditDiscountedValue over all MarkovBanditPolicys, a bounded set because rewards are bounded.
• Trivialization ruled out. The class of ε-index* policies is defined structurally, by a staged rule (a process and a positive stopping time of its own trajectory at the start of every stage) that the policy follows after every history. It is never defined through the value the policy attains, which would make the goal a tautology.
• Not stated. Lemma 4.6(ii)–(iii) (they need forwards-induction policies and induced randomized freezing rules) and Corollary 4.17 (mission VIII). Theorem 4.18 is already open on the platform.
• Welcome contributions. The freezing-rule inequalities are reusable for the jobs-with-precedence index theorems of §4.6–4.7. So are a construction of the induced freezing rule of a bandit under a family policy and the stage decomposition of an ε-index* policy.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033
• M. N. Katehakis, A. F. Veinott Jr., The multi-armed bandit problem: decomposition and computation, Mathematics of Operations Research 12(2), 1987, 262–268. https://doi.org/10.1287/moor.12.2.262
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Ch. 35. https://doi.org/10.1017/9781108571401

Prove a block-sensitivity versus sensitivity separation exponent of 2.15.

Motivation

Recommendation platforms and online retailers choose which products to show a customer, and customers often buy more than one of them in a single visit. Classical choice models such as the multinomial logit (MNL) assume a customer buys at most one product, and under MNL the revenue-maximizing set of products to display is easy to find: it is one of the $n$ revenue-ordered sets, so it can be found in linear time. Tulabandhula, Sinha, Karra and Patidar (arXiv:2006.08055, Manufacturing & Service Operations Management, 2023) introduce the BundleMVL-K model, a multivariate logit model in which a customer buys a bundle of up to $K$ products, with pairwise interaction terms that capture complementarity and substitution. They estimate it on retail data and design algorithms for choosing the recommendation set.

The first question for any such model is whether the revenue problem stays tractable once purchases of two products are allowed. Theorem 1 of the paper answers it negatively: already for $K=2$ the unconstrained revenue problem is NP-complete. This mission formalizes that theorem and its proof, a reduction from Max-Cut.

Setting

The products are $W=\{1,\dots,n\}$. Product $i$ has a revenue $r_i>0$. A BundleMVL-2 instance assigns a nonnegative weight $V_{\{i\}}$ to every product and $V_{\{i,j\}}$ to every unordered pair of products, together with a no-purchase weight $v_0>0$. (In the paper $V_S=\exp(\sum_{i\in S}\alpha_i+\sum_{i<j\in S}\beta_{ij})$, and $\beta_{ij}=-\infty$, so $V_{\{i,j\}}=0$, is allowed.) A customer shown the recommendation set $C\subseteq W$ buys the nonempty bundle $S\subseteq C$, $|S|\le 2$, with probability $V_S/(v_0+\sum_{S'}V_{S'})$, and buys nothing with probability $v_0/(v_0+\sum_{S'}V_{S'})$. The expected revenue of $C$ is eq. (4),

With the indicator $x^C_i$ of $C$, the weights $\theta_{ii}=V_{\{i\}}$, $\theta_{ij}=V_{\{i,j\}}/2$ ($i\ne j$) and the revenues $\hat r_{ii}=r_i$, $\hat r_{ij}=r_i+r_j$ ($i\ne j$), both numerator and denominator are quadratic forms in $x^C$.

The revenue problem (5) is $\max_{C\subseteq W}R_2(C)$; its decision version asks, for a threshold $\kappa$, whether some $C$ has $R_2(C)\ge\kappa$. SIMPLE MAX CUT asks, for a simple graph $G$ and an integer $M$, whether the nodes of $G$ split into two parts with at least $M$ edges between them.

Formalization targets

Goal: Theorem 1

NP-completeness is in the sense of Cook's Definition 4: membership in NP and a polynomial-time many-one reduction from every NP language.