All missions

Motivation

Many strategic systems learn two things at once. Travellers on a road network, firms in a market or bidders in an auction adjust their strategies to each other, and an information platform (a navigation service, a market maker, a public agency) estimates an unknown parameter of the environment from the payoffs those strategies produce. The payoffs are generated by the current strategies, so the data are not i.i.d. The strategies react to the current estimate, so the estimate is not computed from exogenous data. The question is whether this coupled process settles down, and if so, what it settles on.

Wu, Amin and Ozdaglar (arXiv:2206.05637v2, 2023; later in Mathematics of Operations Research, 2025) study this for continuous games with a finite set of candidate parameters. Their first main result, Theorem 1, says that any strategy dynamics that converges when the belief is held fixed still converges when the belief is learned. The limit belief is consistent with the payoff distribution of the limit strategies. It builds on the literature on learning in games (Fudenberg and Kreps 1993; Sandholm 2010) and on Bayesian learning with endogenous data, where a learner may settle on a self-confirming but incorrect belief.

Setting

A finite set $I$ of players repeatedly plays a game. Player $i$ chooses $q_i$ in a convex, closed and bounded set $Q_i\subseteq\mathbb R^{d_i}$, and $Q=\prod_i Q_i$. The payoffs depend on an unknown parameter $s$ in a finite set $S$, with true value $s^*$. At a profile $q$, the payoff vector $y\in\mathbb R^I$ has payoff density $\varphi^s(y\mid q)$, continuous in $q$. Player $i$'s average payoff $u_i^s(q)$ is continuous in $q$.

A belief is $\theta\in\Delta(S)$. In the game $G(\theta)$, player $i$ maximizes the expected utility $\sum_{s}\theta(s)u_i^s(q)$, and $EQ(\theta)$ is its set of pure equilibria in $Q$.

The dynamics runs in stages $k=1,2,\dots$, starting from $\theta^1$ with $\theta^1(s)>0$ for all $s$ and $q^1\in Q$. At stage $k$ the profile $q^k$ is played and $y^k$ is drawn from $\varphi^{s^*}(\cdot\mid q^k)$. At the update stages $k_1<k_2<\cdots$ the belief is updated by Bayes' rule from the strategies and payoffs since the previous update,

$$\theta^{k_{t+1}}(s)\propto\theta^{k_t}(s)\prod_{k=k_t}^{k_{t+1}-1}\varphi^s(y^k\mid q^k),$$

and it is constant in between. Strategies follow a set-valued update $q_i^{k+1}\in F_i(\theta^{k+1},q^k)$ with $F_i(\theta,q)\subseteq Q_i$.

The KL divergence $D_{KL}(\varphi^{s^*}(\cdot\mid q)\,\|\,\varphi^s(\cdot\mid q))$ is defined as usual, with value $\infty$ when absolute continuity fails. The payoff-equivalent set is $S^*(q)=\{s: D_{KL}=0\}$, and the support of a belief is $[\theta]=\{s:\theta(s)>0\}$.

The standing assumptions are:

• Assumption 1: each $F_i$ is upper hemicontinuous.
• Assumption 2: for every $\theta$, $EQ(\theta)\neq\emptyset$, and every run of the update with $\theta$ held fixed converges to a point of $EQ(\theta)$.
• Assumption 3: for every $\theta$, either $EQ(\theta)$ is a singleton, or its points are isolated and $F$ is single-valued near each of them.

Formalization targets

Goal: Theorem 1 (pp.12–13), with corrected sub-clauses

With probability 1, $(\theta^k,q^k)\to(\bar\theta,\bar q)$ with

$$[\bar\theta]\subseteq S^*(\bar q)\quad\text{(2a)},\qquad\bar q\in EQ(\bar\theta)\quad\text{(2b)}.$$

Two further clauses hold for every $s\notin S^*(\bar q)$:

• Rate. If $\varphi^{s^*}(\cdot\mid\bar q)\ll\varphi^s(\cdot\mid\bar q)$, then $\frac1k\log\theta^k(s)\to-D_{KL}(\varphi^{s^*}(\cdot\mid\bar q)\|\varphi^s(\cdot\mid\bar q))$.
• Exclusion. Otherwise $\theta^k(s)=0$ from some finite stage on.

The rate and exclusion clauses are false as printed, and the goal states minimal corrections:

• C0: the rate clause allows $\theta^k(s)$ to reach $0$.
• C1: the rate clause assumes $k_{t+1}/k_t\to1$.
• C2: the rate clause assumes that the KL divergence is continuous at $\bar q$ and that the squared log-likelihood ratio has a locally bounded mean.
• C3: the exclusion clause assumes that $q\mapsto\Pr_{\varphi^{s^*}(\cdot|q)}(\varphi^s(y\mid q)=0)$ is lower semicontinuous at $\bar q$.

Each correction comes with a one-player counterexample that satisfies every assumption of the paper. The convergence and (2a)–(2b) carry no added hypothesis.

Milestones (the proof's three steps, p.22)

1. Identity (7): the belief equals the every-stage auxiliary belief $\tilde\theta^k$ at update stages and is constant in between.
2. Lemma 1: the ratio $\tilde\theta^k(s)/\tilde\theta^k(s^*)$ is a supermartingale, and a martingale when $\varphi^s\ll\varphi^{s^*}$. This is corrected: the printed "martingale" fails when $\varphi^s$ puts mass where $\varphi^{s^*}=0$.
3. Lemma 2: $\theta^k\to\bar\theta\in\Delta(S)$ almost surely.
4. Lemma 3: $q^k\to\bar q\in EQ(\bar\theta)$ almost surely.
5. Lemma 4: (2a), and the corrected rate and exclusion clauses at the limit.

Significance

The theorem turns a known property, convergence of a strategy dynamics under a fixed belief, into convergence of the coupled belief–strategy dynamics. It covers belief-based best responses in Cournot, potential and supermodular games and no-regret learning in concave games (Table 1, p.11). Condition (2a) characterizes where learning can stop. It may stop at an incomplete-information fixed point, where a wrong parameter cannot be distinguished from $s^*$ at the limit strategies. The paper's later results build on this. Global stability (Proposition 1) holds exactly when no such fixed point exists, and the local stability result (Theorem 2) uses Theorem 1 in its proof.

No part of the result has been formalized. A machine-checked proof also settles the status of the printed statement. The rate and exclusion clauses need the corrections above. The strategy-convergence step (Lemma 3) contains a uniformity claim, "$L=\max_{\hat q^1\in Q}L(\hat q^1)$ is finite because $Q$ is compact" (p.24). No counterexample to it is known, and the convergence clause is posed as printed. A proof, or a counterexample that leads to a further correction, is a contribution.

Difficulty

The natural argument has three steps: martingale convergence for the belief, then the static convergence assumption for the strategies, then a law of large numbers for the log-likelihood ratios at the limit. Steps 2 and 3 do not go through as written. In step 2 the belief moves while the strategies move. Comparing the true path with paths of the fixed-belief dynamics needs a stability property that holds uniformly over starting points. Pointwise convergence on a compact set does not provide it, because convergence times blow up near unstable equilibria. In step 3 the payoffs are a non-stationary, adapted sequence. Convergence of $q^k$ alone does not make the log-likelihood ratios obey a law of large numbers: a density can be continuous in $q$ at every $y$ and still have a log-likelihood ratio whose mean jumps at $\bar q$. This is why the rate clause needs a regularity hypothesis at $\bar q$.

Formalization scope

• Strategies and beliefs. Profiles live in $\prod_i\mathbb R^{d_i}$ (EuclideanSpace), with Lean's sup-type distance. Beliefs are vectors in stdSimplex ℝ S. Stages are indexed from $0$.
• Payoffs and KL. Payoff densities are functions on $\mathbb R^I$ with Lebesgue measure. $D_{KL}$ is Mathlib's klDiv of the two density measures, which equals Definition 1 for every pair of densities.
• The process. A realization of the dynamics is a filtered probability space carrying:
  • adapted profiles $q^k$;
  • payoffs $y^k$ with conditional density $\varphi^{s^*}(\cdot\mid q^k)$ given $\mathcal F_k$;
  • a random set of update stages that contains the first stage and is infinite almost surely;
  • the update $q^{k+1}\in F(\theta^{k+1},q^k)$ almost surely.
• The belief is not a free process. $\theta^k$ is the function of $(\theta^1,q,y,T)$ given by (θ-update). If the belief were a free variable, the theorem would be a claim about arbitrary sequences and would be false.
• Generalizations. Two hypotheses of the paper are relaxed. $u_i^s$ is not required to be the mean of $y_i$, since the proof never links them. Strategy updates may be any adapted, possibly randomized, selection.
• Assumptions. Upper hemicontinuity uses the open-set definition, with no closed or nonempty values. Assumption 2 ranges over every selection. In Assumption 3(ii), $\bar\theta$ is read as the $\theta$ of the preamble.

The infrastructure is Mathlib's conditional expectation, (super)martingales and their almost-sure convergence, klDiv, and densities via withDensity. A complete development needs a martingale strong law with a conditional variance bound and a conditional Borel–Cantelli lemma. Both are reusable beyond this mission. Contributions are welcome on any milestone. Identity (7) and Lemma 1 are the natural entry points.

Selected references

• M. Wu, S. Amin, A. Ozdaglar, Convergence and Stability of Coupled Belief–Strategy Learning Dynamics in Continuous Games, arXiv:2206.05637v2, 2023. https://arxiv.org/abs/2206.05637v2
• D. Fudenberg, D. M. Kreps, Learning mixed equilibria, Games and Economic Behavior 5(3), 1993. https://doi.org/10.1006/game.1993.1018
• W. H. Sandholm, Population Games and Evolutionary Dynamics, MIT Press, 2010. https://mitpress.mit.edu/9780262195874/
• D. Fudenberg, J. Tirole, Game Theory, MIT Press, 1991. https://mitpress.mit.edu/9780262061414/

Motivation

Assortment optimization asks a retailer which set $S$ of products to offer, out of a ground set $N$, when customers choose among the offered products according to a choice model; the expected revenue $R(S)$ is a set function of the assortment. Under the multinomial logit model and its mixtures, $R$ is neither monotone nor submodular, so the classical theory of submodular maximization (Nemhauser, Wolsey and Fisher 1978) does not apply, and the field has developed algorithms tailored to individual choice models. The revenue functions of a broad class of random-utility models are, however, subadditive, $f(A)+f(B)\ge f(A\cup B)$.

Subadditivity alone is too weak for optimization: Dobzinski, Nisan and Schapira (2010) show that with polynomially many value queries no algorithm approximates monotone subadditive maximization under a cardinality constraint better than $n^{-\Omega(1)}$. Udwani (arXiv:2107.02743v5) introduces a structural property between subadditivity and submodularity, the submodular order, which several assortment problems satisfy (mixtures of multinomial logit with customization, Markov chain choice models) and which restores constant-factor approximation. This mission formalizes the paper's cardinality-constrained algorithm and its guarantee.

Setting

Let $N$ be a finite ground set of $n$ elements and $f:2^N\to\mathbb R$ a set function with the normalization $f(\emptyset)=0$. It is monotone if $f(A)\ge f(B)$ whenever $B\subseteq A$. The marginal value of $X$ given $S$ is $f(X\mid S)=f(X\cup S)-f(S)$.

An order $\pi$ is a bijection from $N$ to the indices $0,\dots,n-1$; one reads it from left to right. A set $C$ lies to the right of $A$ if every element of $C$ has a larger index than every element of $A$. Sets $B\subseteq A$ are $\pi$-nested if every element of $A\setminus B$ lies to the right of $B$. The order $\pi$ is a submodular order of $f$ if

$$f(C\mid A)\le f(C\mid B)\quad\text{for all } B\subseteq A \text{ and all } C \text{ to the right of } A,$$

and a weak submodular order if this holds whenever, in addition, $B\subseteq A$ are $\pi$-nested. A function is submodular exactly when every order is a submodular order.

The problem is to maximize $f(S)$ subject to $|S|\le k$, with optimal value $\mathrm{OPT}=\max\{f(S):|S|\le k\}$, given access to $f$ only through a value oracle that returns $f(S)$ for a queried set $S$.

Threshold Add$(k,\tau)$ scans the elements once in increasing $\pi$-index, starting from $S=\emptyset$, and adds the current element $e$ whenever $|S|<k$ and $f(e\mid S)\ge\tau$. Algorithm 1 sets $\tau=\frac1k\max_e f(\{e\})$, runs Threshold Add with the thresholds $(1+\varepsilon)^{i-1}\tau$ for $i=1,\dots,L$, $L=\max(1,\lceil\log_{1+\varepsilon}k\rceil)$, and returns the best of the $L$ sets.

Formalization targets

Goal: Theorem 2

There is an absolute constant $C$ such that for every ground set with every order $\pi$, every $k\ge1$, every $\varepsilon\in(0,1)$ and every monotone subadditive $f$ with $f(\emptyset)=0$ for which $\pi$ is a weak submodular order, the output $S$ of Algorithm 1 satisfies

$$|S|\le k,\qquad f(S)\ \ge\ (1-\varepsilon)\cdot\tfrac12\cdot\mathrm{OPT},$$

and Algorithm 1 makes at most $C\,n\,(1+\log k)/\varepsilon$ oracle queries. The constant is left unfixed, so the goal asserts the order of growth $O(\frac n\varepsilon\log k)$ of the paper.

Milestones

1. Lemma 1 and Corollary 2 (pp.19–20): for an interleaved partition $\{O_1,E_1,\dots,O_m,E_m\}$ of $A$,

$$f(A)\le f(E(m))+\sum_{\ell\in[m]}f(O_\ell\mid E(\ell-1)),\qquad E(j)=\textstyle\bigcup_{i\le j}E_i,$$

and the more general family indexed by a permutation $\sigma$. 2. The query count (p.20): Threshold Add makes at most $n$ queries, Algorithm 1 at most $n(1+L)$. 3. The steps of the approximation proof (p.21): $f(S)\ge|S|\tau$ for Threshold Add; the rejection bound $f(O_\ell\mid E(\ell-1))\le\tau|O_\ell|$; inequality (5); the guarantee for a single threshold in $[(1-\varepsilon)\mathrm{OPT}/(2k),\mathrm{OPT}/(2k)]$; the case $\mathrm{OPT}\le2\max_e f(\{e\})$; and the existence of a grid threshold in that window otherwise.

Significance

Theorem 2 is the first constant-factor guarantee for a class of monotone subadditive functions that contains the monotone submodular functions and the revenue functions of several assortment problems. The paper's Theorem 3 shows that $\frac12+\varepsilon$ cannot be beaten with polynomially many queries, even under a strong submodular order, so the factor $\frac12$ is the right one. The same theorem yields the paper's results for assortment optimization under mixtures of multinomial logit models with customization, and for streaming submodular maximization, where the arrival order acts as a submodular order. Lemma 1 and Corollary 2 are the structural bounds behind all the algorithms of the paper, including those for budget and matroid constraints.

The result is proved in the paper; to the best of current knowledge none of it has a machine-checked proof. Formalizing it fixes the definitions of submodular order, nested sets and interleaved partitions, and it pins down three places where the printed text needs a correction: the formula defining interleaved partitions, the loop length of Algorithm 1 at $k=1$, and the last term of inequality (5). Each correction is recorded with a counterexample on the affected item.

Difficulty

The obvious argument for threshold algorithms, as for submodular functions, compares the output with the optimal set element by element using diminishing returns. A submodular order gives diminishing returns only for sets $C$ lying to the right of $A$, and a weak order only for nested pairs, so the familiar inequality $f(A)\le f(E)+f(O\mid E)$ fails in general. The difficulty is that every diminishing-returns step of the comparison must involve a set lying to the right of everything accumulated before it, and the optimal set and the output are interleaved arbitrarily along $\pi$. A second, quieter difficulty is bookkeeping: the guarantee concerns the execution of an algorithm and its number of oracle queries, so the formalization must model the algorithm as an object whose queries can be counted.

Formalization scope

The ground set is a Fintype α with an order π : α ≃ Fin n, subsets are Finset α and $f$ is Finset α → ℝ. "To the right of" and "$\pi$-nested" are ∀-comparisons of indices, vacuous when a set is empty, which is how the paper applies them. $\mathrm{OPT}$ is a finite maximum over the sets with at most $k$ elements.

Algorithms are terms of a value-oracle program type: a program either returns a result or queries a set and continues with a program depending on the answer. Algorithms 1 and 2 are built from $\pi$, $k$, $\varepsilon$ and $\tau$ only and never from $f$; the query count is a function of the program and $f$. A formalization in which the algorithm receives $f$ directly would make the query bound vacuous, and this one rules that out. Threshold Add keeps the value of its current set and uses $f(\emptyset)=0$ without a query; "best of" returns the first maximizer. $\tau$ is $\max(0,\max_e f(\{e\}))/k$, which agrees with the paper whenever $f$ is monotone with $f(\emptyset)=0$.

Interleaved partitions are blocks O E : Fin m → Finset α covering $A$ in which every element of an earlier block precedes every element of a later block; empty blocks are allowed. The query bound reads $O(\frac n\varepsilon\log k)$ as $C\,n(1+\log k)/\varepsilon$, since the printed bound vanishes at $k=1$.

The development needs only Mathlib's finite sets, sums and real logarithms. The program type and its query count are reusable for any value-oracle algorithm, and Lemma 1 for any analysis under a submodular order (budget and matroid constraints in the same paper). Proofs of any milestone, and of further results of the paper (Theorems 4 and 5, Corollary 3), are welcome.

Selected references

• R. Udwani, Submodular Order Functions and Assortment Optimization, arXiv:2107.02743v5, 2024 (Management Science, 2024). https://arxiv.org/abs/2107.02743v5
• S. Dobzinski, N. Nisan, M. Schapira, Approximation algorithms for combinatorial auctions with complement-free bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions—I, Mathematical Programming 14(1):265–294, 1978. https://doi.org/10.1007/BF01588971
• A. Badanidiyuru, J. Vondrák, Fast algorithms for maximizing submodular functions, Proceedings of SODA 2014, 1497–1514. https://doi.org/10.1137/1.9781611973402.110
• A. Badanidiyuru, B. Mirzasoleiman, A. Karbasi, A. Krause, Streaming submodular maximization: massive data summarization on the fly, Proceedings of KDD 2014, 671–680. https://doi.org/10.1145/2623330.2623637

Motivation

A firm that must buy a fixed quantity of a commodity often faces suppliers one at a time: a quote arrives, the firm decides how much to buy at that price, and the decision cannot be revisited. Electricity procurement, cloud capacity and spot markets for raw materials all have this shape. When the marginal cost of buying grows with the amount bought from one supplier (congestion, convex production costs), the natural model charges $C_i x_i^p$ for buying $x_i$ from supplier $i$, with $p>1$.

This is a minimization prophet inequality: the buyer is compared with a prophet who sees every price in advance. The classical prophet inequality (Krengel–Sucheston 1977, Samuel-Cahn 1984) is a maximization problem with a single accepted item. Its minimization version behaves badly: without further assumptions, no online policy is within a bounded factor of the prophet (Esfandiari, HajiAghayi, Liaghat, Monemizadeh 2015). Qin, Vardi and Wierman (MOR 2024, doi:10.1287/moor.2021.0173) allow fractional purchases, monomial costs, and an in-house production option: the buyer can always produce the commodity itself at a known price. Their Theorem 2 computes the exact competitive ratio in that case.

Setting

There are $n\ge1$ sellers, met in the order $1,\dots,n$. Seller $i$'s price coefficient $C_i$ is a random variable with known law $D_i$, and $C_1,\dots,C_n$ are independent. Seller $1$ is the buyer's own production, with $\mathbb P[C_1=1]=1$. The other sellers' laws belong to the class $\mathcal D$ of all probability distributions with support in $[\ell,\infty)$, for a fixed $0<\ell<1$. No upper bound and no moment condition are imposed.

A policy $\pi$ observes $c_1,\dots,c_i$ and then buys $x_i=\pi_i(c_1,\dots,c_i)\in[0,1]$, with $\sum_i x_i=1$. Its cost is

$$\mathrm{ALG}^\pi(c,p)=\sum_{i=1}^n c_i x_i^p .$$

The prophet pays $\mathrm{OPT}(c,p)=\min\{\sum_i c_ix_i^p : x\in[0,1]^n,\ \sum_i x_i=1\}$. The competitive ratio with in-house production is

$$\mathrm{CR}_{\text{in-house}}(F,n)=\inf_{\pi}\ \sup_{D_2,\dots,D_n\in\mathcal D}\frac{\mathbb E[\mathrm{ALG}^\pi(C,p)]}{\mathbb E[\mathrm{OPT}(C,p)]},$$

with the infimum over policies outside the supremum over distributions. Throughout, $q=-1/(p-1)$, and $M_q(c)=\bigl(\tfrac1n\sum_i c_i^q\bigr)^{1/q}$ is the power mean.

Formalization targets

Goal: Theorem 2 (p.11)

$$\mathrm{CR}_{\text{in-house}}(F,n)=\Bigl(1+\frac{n-1}{\ell^{1/(p-1)}}\Bigr)^{p-1}\qquad\text{for all } n\ge1,\ p>1,\ 0<\ell<1 .$$

Both inequalities are needed: no policy does better on every instance, and some policy achieves the value on every instance.

Milestones, in proof order

1. Lemma 1 (p.10): for positive prices, $\mathrm{OPT}(c,p)=\bigl(\sum_i c_i^q\bigr)^{1/q}$, and the minimum is attained.
2. Lemma 2 (p.12): under a mean constraint, $\mathbb E[f(C)]$ with $f$ strictly concave on $[\ell,u]$ is minimized only by the two-point law on $\{\ell,u\}$.
3. Lemma 3 (p.12): the non-adaptive algorithm NA has ratio $M_q(\mathbb E[C])/\mathbb E[M_q(C)]$.
4. Upper bound (p.13): $\sup_D \mathbb E[\mathrm{ALG}^{\mathrm{NA}}]/\mathbb E[\mathrm{OPT}]=(1+(n-1)\ell^q)^{-1/q}$, which is the value in (3).
5. DP optimality (Appendix B.1, p.22): the cost-to-go recursion (21) gives the least expected cost over all causal policies, a policy of the form (22) exists, and every such policy attains it.
6. Lemma 8 (p.22): $J_i(s)=b_i(1-s)^p$ with an explicit scalar recursion for $b_i$, and the optimal allocation (26).
7. Lower bound (p.23): on long-shot sellers (price $\ell$ with probability $1-\varepsilon$, $u$ with probability $\varepsilon$) the optimal cost tends to $1$ as $u\to\infty$, and the ratio tends to (3) as $\varepsilon\to0$.

Significance

The theorem gives an exact, closed-form competitive ratio for a sequential procurement problem with unbounded price risk. Its value depends only on $n$, $p$ and the price floor $\ell$, and it is finite even when the external prices have infinite mean. Without in-house production, the paper's Theorem 3 shows that the ratio grows with the upper end $u$ of the price range. So the in-house option is what makes the problem robust to price spikes, and Theorem 2 measures that effect exactly. The paper's Corollary 1 states the linear-cost value $1/\ell$, obtained as the limit $p\to1$ of (3). The proof also shows that the gap is already achieved by the simple policy that buys everything in-house: on worst-case instances, adaptivity gains nothing.

The paper's proof is informal at two points that a formal development must make precise. The upper bound applies Lemma 2 with $u=\infty$ and with infinite means. The lower bound reads several limits as equalities, and it uses DP optimality by citation. In addition, the recursion (25) is printed with the exponent $1/p-1$, which makes Lemma 8 false as printed; the mission states the corrected exponent $1/(p-1)$ (Lemma 8's title records the correction). None of the results has a machine-checked proof.

Difficulty

The upper bound is the easy half: it only needs a single policy and a pointwise lower bound on $\mathrm{OPT}$. The lower bound carries the weight. It must hold against every measurable causal policy, however adaptive, and comparing a policy with the prophet realization by realization does not work: the policy's loss comes from rare high prices it cannot foresee, not from any single price vector. So the optimal adaptive cost has to be known exactly. That is a finite-horizon dynamic program with continuous controls over arbitrary price laws, whose optimality the paper only cites (milestone 5), and whose closed form needs a backward induction in real powers (milestone 6). The final step takes two limits whose order matters: $u\to\infty$ for fixed $\varepsilon$, then $\varepsilon\to0$. Exchanging them, or treating the page's limit statements as equalities at finite $u$, gives false statements.

Formalization scope

Sellers are Fin n with $n\ge1$; Lean's seller 0 is the paper's in-house seller $1$. Prices are real; an instance is a family of probability measures ν : Fin n → Measure ℝ with ν 0 = dirac 1 and $\nu_i((-\infty,\ell))=0$ for the other sellers, and the joint law is the product measure. Policies are families of measurable maps $x_i:\mathbb R^n\to[0,1]$ that depend only on $c_0,\dots,c_i$ and sum to $1$ for every price vector. Expectations of costs are lower Lebesgue integrals, and the ratio is computed in $[0,\infty]$, so policies with infinite expected cost are allowed and give ratio $\infty$. $\mathrm{OPT}$ is the real infimum over the simplex. The DP objects use 0-based stages.

The trivializing readings are ruled out. The policy class and the instance class are nonempty (the all-in-house policy and the long-shot instance are admissible), and $0<\mathbb E[\mathrm{OPT}]\le1$ on every instance, so the ratio is never a junk value. The infimum is taken outside the supremum, so a policy cannot depend on the instance.

A complete development needs Hölder or Lagrangian arguments in finite dimension (Lemma 1), Jensen with its equality case on an interval (Lemma 2), Fubini on product measures (Lemma 3), a finite-horizon dynamic programming theorem for measurable policies with interval controls (milestone 5), and real-power calculus (Lemma 8). The DP optimality statement and the extremal Lemma 2 are reusable beyond this mission. Contributions that prove any milestone, or that factor out general lemmas (finite-horizon DP over product measures, the Jensen equality case), are welcome.

Selected references

• J. Qin, S. Vardi, A. Wierman, Minimization Fractional Prophet Inequalities for Sequential Procurement, Mathematics of Operations Research, 2024. https://doi.org/10.1287/moor.2021.0173 (this mission cites the author manuscript, sha256 672fa87c…79125d3).
• H. Esfandiari, M. HajiAghayi, V. Liaghat, M. Monemizadeh, Prophet Secretary, ESA 2015. https://doi.org/10.1007/978-3-662-48350-3_42
• U. Krengel, L. Sucheston, Semiamarts and finite values, Bulletin of the AMS 83(4), 1977. https://doi.org/10.1090/S0002-9904-1977-14378-4
• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Annals of Probability 12(4), 1984. https://doi.org/10.1214/aop/1176993150
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, Athena Scientific, 1995 (Proposition 1.3.1).

Why biased simulation outputs need tuning

Many simulation estimators are biased, and the bias is controlled by a tuning parameter that also controls the noise. A central finite difference for the derivative of an expectation is the standard example: a perturbation size $\delta$ gives a bias of order $\delta^2$ and a variance of order $\delta^{-2}$. Simulation budgets are then spent on a trade-off. Choosing $\delta$ as the right power of the number of runs $n$ gives the best order of the mean squared error (Fox and Glynn, 1989; Glynn and Whitt, 1992). The best constant requires the model's bias and noise coefficients, which are unknown in practice. Debiasing methods such as multilevel Monte Carlo (Giles, 2008; Rhee and Glynn, 2015) remove the bias when runs at consecutive levels can be coupled.

Lam, Zhang and Zhang (arXiv:1902.04673v1) ask what can be gained without coupling and without those coefficients, by weighting independent runs made at different tuning parameters. They measure the gain against the plain sample average, in a minimax sense.

Setting

Fix $q_1,q_2>0$. Each run at tuning parameter $\delta>0$ outputs

$$\hat\theta(\delta)=\theta+b(\delta)+\frac{\varepsilon(\delta)}{\delta^{q_2}},\qquad b(\delta)=B\delta^{q_1}+o(\delta^{q_1}),$$

where $B\neq 0$, $\mathbb E\varepsilon(\delta)=0$ and $\mathrm{Var}\,\varepsilon(\delta)\to\sigma^2>0$ as $\delta\to 0$. The class of all such outputs, with arbitrary $B$, $\sigma^2$ and higher-order terms, is $\Theta$ (SimulationOutput q₁ q₂).

Let $\alpha=1/(2(q_1+q_2))$ and $n_0\in\mathbb N$. The baseline $\bar\theta_n$ averages $n$ independent runs at the single value $\delta=d(n+n_0)^{-\alpha}$; its mean squared error is $\mathrm{MSE}_0$. The weighted estimator is $\hat\theta_n^{gen}=\sum_{j=1}^n w_{j,n}\hat\theta_j(\delta_j)$ with $\delta_j=\tilde d(j+n_0)^{-\alpha}$, where $W=(w_{j,n})$ is any real triangular array; its mean squared error is $\mathrm{MSE}_1^{gen}$. The asymptotic risk ratio is

$$R^{gen}(\hat\theta(\cdot),d,\tilde d,W)=\limsup_{n\to\infty}\frac{\mathrm{MSE}_1^{gen}}{\mathrm{MSE}_0}.$$

A designer picks $W$ and a calibration $g$ in $\mathcal F_K=\{g:g(d)\le Kd\}$, and the adversary answers with a model in $\Theta$ and a $d>0$.

Formalization targets

Goal: the value of the game

$$\min_{g\in\mathcal F_K,\ W}\ \max_{\hat\theta(\cdot)\in\Theta,\ d>0}R^{gen}(\hat\theta(\cdot),d,g(d),W)=\frac{q_1}{q_1+q_2}\,\frac1{K^{2q_2}}.$$

This is Theorem 8, part 1, of the paper.

Goal: the optimal configuration

The value is attained at $g(d)=Kd$ and at weights with two decay rates,

$$w^*_{j,n}=\frac{\lambda_1^*}{(j+n_0)^{(q_1+2q_2)/(2(q_1+q_2))}}+\frac{\lambda_2^*}{(j+n_0)^{q_2/(q_1+q_2)}},$$

where $(\lambda_1^*,\lambda_2^*)$ comes from an explicit $2\times 2$ matrix $\Xi$ and an optimal solution $a^*$ of a one-dimensional problem (24). This is Theorem 8, part 2. Both parts form the one goal theorem, theorem_8.

Milestones

In the order of the argument: the asymptotic MSE of the baseline (Theorem 1); the bias-variance form of $\mathrm{MSE}_1^{gen}$ (31); the need for $\sum_j w_{j,n}\to 1$; the closed form of a minimum-norm problem (67); the reduction of (60) to (24); the asymptotics of $\phi$; the scaled limit of $\Xi$ (75); the uniform floor; the limit of (76) with $\eta^*\to K$; the negligibility of errors (81), (82); the lower bound for every configuration; and the value of the ratio at $W^*$.

Significance

The value tells how much an estimator can improve on the sample average with no knowledge of $B$ and $\sigma^2$. For central finite differences ($q_1=2$, $q_2=1$) with $K=1$ it is $2/3$, for every model and every $d$; for forward differences ($q_1=q_2=1$) with $K=1$ it is $1/2$. The form of $W^*$ is a design rule that uses only $q_1$, $q_2$ and $K$. The restricted classes treated earlier in the paper, recursive and averaged estimators, have a minimax ratio above $1$ (Theorems 3 to 7), so the gain comes from the general weighted class.

The theorem is proved in the paper. No machine-checked version is known to exist, and the platform held no statement on this subject when this mission was drafted. The mission produces a reusable formal account of biased simulation outputs and their mean squared errors under independent runs at varying parameters, and a checked minimax value. The array $w^*(0)$ also attains the value, so optimal weights are not unique; the goal does not claim uniqueness.

Difficulty

The obvious route is to replace $\mathrm{MSE}_1^{gen}$ by its leading terms and optimize. That fails to be a proof at three places. The matrix $\Xi$ has entries on different scales, and the remainders of order $1/\log n$ are what decide feasibility in (24). Problem (24) is nonconvex, its feasible set can be disconnected or, at finite $n$, empty, and the claims concern every selection of minimizers, for which there is no formula. The weights take both signs, so the $o(\cdot)$ terms of the model cannot be bounded termwise against the main sum, and they meet the early runs, where $\delta_j$ is not small and nothing is known about the bias beyond finiteness.

Formalization scope

A model is the number $\theta$, the constants $B$, $\sigma^2$, and for each $\delta>0$ a probability law on $\mathbb R$ with finite second moment; the conditions on $b$ and the variance are stated along $\delta\downarrow 0$. Independent runs are coordinates under Measure.pi over Fin n, and index $i$ is run $j=i+1$. $\mathrm{MSE}_0$ and $\mathrm{MSE}_1^{gen}$ are integrals of squared errors. The risk ratio and the value lie in ℝ≥0∞. The inner max is a supremum, which need not be attained for a general array; the outer min is IsLeast. The inverse in $\Xi$ is Matrix's, and it is genuine for $n\ge 2$. Optimality of $a^*$ is required for all large $n$, as (24) can be infeasible at finite $n$.

A trivializing formalization is excluded: the mean squared errors are not defined by a formula, the weights are chosen before the model, $\theta$ is free, and the remainders of the model are arbitrary.

A complete development needs the second-moment calculus for product measures, sharp asymptotics of $\sum_{j\le n}(j+n_0)^{-\kappa}$ for $\kappa\le 1$, and asymptotics of a $2\times 2$ inverse. The first two are reusable beyond this mission. Contributions toward any milestone are welcome, including proofs that take a different route from Appendix C.

Selected references

• H. Lam, X. Zhang, X. Zhang, Enhanced Balancing of Bias-Variance Tradeoff in Stochastic Estimation: A Minimax Perspective, arXiv:1902.04673v1, 2019; published in Operations Research, 2023. https://arxiv.org/abs/1902.04673
• B. L. Fox, P. W. Glynn, Replication schemes for limiting expectations, Probability in the Engineering and Informational Sciences 3(3):299–318, 1989. https://doi.org/10.1017/S0269964800001170
• P. W. Glynn, W. Whitt, The asymptotic efficiency of simulation estimators, Operations Research 40(3):505–520, 1992. https://doi.org/10.1287/opre.40.3.505
• M. B. Giles, Multilevel Monte Carlo path simulation, Operations Research 56(3):607–617, 2008. https://doi.org/10.1287/opre.1070.0496
• C.-H. Rhee, P. W. Glynn, Unbiased estimation with square root convergence for SDE models, Operations Research 63(5):1026–1043, 2015. https://doi.org/10.1287/opre.2015.1404

Motivation

Many estimation problems ask for the solution $v^*$ of a linear fixed-point equation $v=Lv+b$ on a high- or infinite-dimensional space, when only noisy unbiased samples of $L$ and $b$ are available. The leading example is policy evaluation in reinforcement learning: the value function of a Markov reward process solves the Bellman equation $v=r+\gamma Pv$, and temporal-difference (TD) learning with linear function approximation estimates it within a $d$-dimensional subspace $\mathbb S$ of features. Galerkin methods for elliptic equations and linear regression with a misspecified model have the same structure. Because the search is restricted to $\mathbb S$, every such method pays an approximation error in addition to the statistical error of finite data.

Timeline of the approximation-error question:

• Tsitsiklis and Van Roy (1997) analysed TD learning with linear function approximation and bounded the distance of its fixed point to $v^*$ by a multiple of the best approximation error (IEEE TAC). Their argument, recalled on p.13 of the paper, gives $\|\bar v-v^*\|^2\le(1-\gamma^2)^{-1}\inf_{v\in\mathbb S}\|v-v^*\|^2$ whenever $\gamma=|||L|||_{\mathbb X}<1$; the factor depends on $L$ only through its norm.
• Yu and Bertsekas (2010) gave sharper data-dependent bounds on the projected fixed point in terms of the projected operator (Math. Oper. Res.).
• Mou, Pananjady and Wainwright (2020) proved an oracle inequality for a stochastic approximation estimator with an instance-dependent factor $\alpha(M,|||L|||)$ and showed that it, and the leading statistical term, are optimal (arXiv:2012.05299).

Setting

Let $\mathbb X$ be a real Hilbert space, $L:\mathbb X\to\mathbb X$ a bounded linear operator with $I-L$ boundedly invertible, $b\in\mathbb X$, and $v^*$ the unique solution of $v^*=Lv^*+b$. Let $\mathbb S\subseteq\mathbb X$ be a subspace with orthonormal basis $\varphi_1,\dots,\varphi_d$, with coordinate map $\Phi_d(x)=(\langle x,\varphi_j\rangle)_{j=1}^d$ and adjoint $\Phi_d^*(v)=\sum_jv_j\varphi_j$. The projected operator is the $d\times d$ matrix $M=\Phi_dL\Phi_d^*$ (projMat), and

$$\kappa(M)=\tfrac12\lambda_{\max}(M+M^\top)<1$$

is assumed throughout (kappa). The projected fixed point $\bar v\in\mathbb S$ solves $\bar v=\Pi_{\mathbb S}(L\bar v+b)$, so $\bar v=\Phi_d^*(I-M)^{-1}\Phi_db$ (vbar).

The data are i.i.d. pairs $(L_i,b_i)$ with $\mathbb E L_i=L$, $\mathbb E b_i=b$, and the second-moment bounds of Assumption 1(W): $\mathbb E\langle\varphi_j,(L_i-L)u\rangle^2\le\sigma_L^2\|u\|^2$ for unit $u\in\mathbb S$ and $\mathbb E\langle\varphi_j,b_i-b\rangle^2\le\sigma_b^2$. Stochastic approximation with stepsize $\eta$ runs $v_{t+1}=(1-\eta)v_t+\eta\Pi_{\mathbb S}(L_{t+1}v_t+b_{t+1})$ from $v_0\in\mathbb S$, and the Polyak–Ruppert average is $\widehat v_n=\frac1{n-n_0}\sum_{t=n_0+1}^nv_t$ (theta, vIter, vhat). The instance-dependent quantities are the approximation factor

$$\alpha(M,s)=1+\lambda_{\max}\big((I-M)^{-1}(s^2I_d-MM^\top)(I-M)^{-\top}\big)$$

(alphaFactor), the noise covariance $\Sigma^*=\operatorname{cov}(\Phi_d(b_1-b))+\operatorname{cov}(\Phi_d(L_1-L)\bar v)$ (SigmaStar), and

$$\mathcal E_n(M,\Sigma^*)=\frac{\operatorname{trace}((I-M)^{-1}\Sigma^*(I-M)^{-\top})}n,\qquad \mathcal H_n=\frac{\sigma_L}{(1-\kappa)^3}\Big(\frac dn\Big)^{3/2}\big(\|\bar v\|^2\sigma_L^2+\sigma_b^2\big)$$

(En, Hn).

Formalization targets

Approximation error (deterministic)

$$\|\bar v-v^*\|^2\le\alpha(M,|||L|||_{\mathbb X})\inf_{v\in\mathbb S}\|v-v^*\|^2 ,$$

Eq. (45a), obtained from Lemma 3 (a bound through $|||(I-L_{\mathbb S,\mathbb S})^{-1}L_{\mathbb S,\perp}|||$) and Lemma 4 (that norm is at most $\lambda_{\max}$ of the matrix in $\alpha$).

Estimation error (stochastic)

Lemma 5 bounds $\mathbb E\|v_t-\bar v\|^2$ for the raw iterates, Lemma 6 decomposes $\mathbb E\|\widehat v_n-\bar v\|^2$, and Eq. (45b) gives

$$\mathbb E\|\widehat v_n-\bar v\|^2\le c\,\mathcal E_n(M,\Sigma^*)+c\,\mathcal H_n$$

for $\eta=1/(c_0\sigma_L\sqrt{dn})$, $n_0=n/2$ and $n$ above a threshold.

Goal: Theorem 1 (oracle inequality)

There are universal constants $c_0,c>0$ such that, under the conditions above, for every $\omega>0$

$$\mathbb E\|\widehat v_n-v^*\|^2\le(1+\omega)\,\alpha(M,|||L|||_{\mathbb X})\inf_{v\in\mathbb S}\|v-v^*\|^2+c\Big(1+\frac1\omega\Big)\big\{\mathcal E_n(M,\Sigma^*)+\mathcal H_n\big\}.$$

The goal is stated with every printed term, for an arbitrary Hilbert space and subspace. The printed sample-size condition does not suffice, and two hypotheses are added (see Formalization scope).

Significance

Theorem 1 separates the error of averaged stochastic approximation into an approximation part and a statistical part, each with an instance-dependent constant. The factor $\alpha(M,|||L|||_{\mathbb X})$ can be much smaller than worst-case contraction factors, and the paper's lower bounds (Theorems 2–4) show that no estimator using the same information achieves a smaller factor, and that $\mathcal E_n(M,\Sigma^*)$ is the local minimax rate. Applied to TD(0) with linear features, it gives instance-optimal guarantees for policy evaluation; applied to Galerkin approximations and linear regression, it recovers and sharpens known bounds.

On the formal side, the platform has Polyak–Juditsky's asymptotic normality for averaged linear stochastic approximation and asymptotic results for TD, but no finite-sample oracle inequality for projected fixed-point equations. Theorem 1 is proved on paper, not formalized anywhere known. The mission's corrections make the formal target a true statement: the printed version is refuted by one-dimensional examples.

Difficulty

The deterministic part needs operator algebra on $\mathbb S\oplus\mathbb S^\perp$ in a possibly non-separable Hilbert space: inverting $I-L_{\mathbb S,\mathbb S}$ on all of $\mathbb X$ and comparing an operator norm on $\mathbb X$ with an eigenvalue of a $d\times d$ matrix, where $|||L|||_{\mathbb X}$ (not $|||M|||$) enters. The stochastic part is a second-moment analysis of a random linear recursion: the iterate $\vartheta_t$ is a product of $t$ random matrices, and its expectation must be controlled through independence of the next observation from the past. The averaged error requires a martingale orthogonality argument plus a bound on the telescoping remainder, and every constant must be tracked to land on universal $c_0,c$. The obvious route of reading the burn-in step on p.31 as stated fails: with the printed threshold the initialization bias is not dominated by the variance, which is why the corrected goal carries an extra threshold.

Formalization scope

• $\mathbb X$ is a complete real inner product space, not assumed separable; $\mathbb S$ is given by an orthonormal basis φ : OrthonormalBasis (Fin d) ℝ S with $d\ge1$. $I-L$ is a unit and $\kappa(M)<1$ are hypotheses; $\bar v$ is the closed-form projected fixed point.
• Observations enter through $A_i=\Phi_dL_i\Phi_d^*$ and $h_i=\Phi_db_i$: an infinite i.i.d. sequence of square-integrable pairs indexed from $1$ (IsObsModel), with Assumption 1(W) in these coordinates. This covers every instance of the paper.
• $\lambda_{\max}$ is the published LowRankMEG.lam · 1 (largest eigenvalue of a symmetric matrix). $n_0=n/2$ is natural-number division, $v_0=\Phi_d^*\vartheta_0$ is deterministic, expectations of squared norms are lower Lebesgue integrals in $[0,\infty]$.
• $c_0,c$ are quantified before everything else, and the same $c_0$ appears in the stepsize and every threshold.
• Corrections: Theorem 1 and (45b) add (ii) $\eta<(1-\kappa)/(4\sigma_L^2d+2(1+|||L|||^2))$ and (iii) $n\ge\frac{c_0\sigma_L^2d}{(1-\kappa)^2}\log^2\big(e+\frac{\|v_0-\bar v\|^2(1-\kappa)\sigma_L\sqrt n}{\sqrt d(\|\bar v\|^2\sigma_L^2+\sigma_b^2)}\big)$; Lemma 5's stepsize range becomes $(0,(1-\kappa)/(4\sigma_L^2d+2(1+|||L|||^2)))$. Each item lists its counterexample.
• Trivializing readings are ruled out: taking $\mathbb S=\mathbb X$, a symmetric or contractive $L$, bounded noise or a fixed numeric $c_0$ would be a different theorem, and a verification file shows that every hypothesis of the goal can hold at once, for every $c_0>0$, with $L\ne0$ and $v_0\ne\bar v$.
• Contributions welcome: the operator lemmas (3, 4) are reusable for any Galerkin-type projection; a library for second moments of random linear recursions (Lemmas 5, 6) would serve other linear stochastic approximation missions.

Selected references

• W. Mou, A. Pananjady, M. J. Wainwright, Optimal oracle inequalities for solving projected fixed-point equations, arXiv:2012.05299v1, 2020; published as Optimal Oracle Inequalities for Projected Fixed-Point Equations, with Applications to Policy Evaluation, Mathematics of Operations Research, 2022. https://arxiv.org/abs/2012.05299
• J. N. Tsitsiklis, B. Van Roy, An analysis of temporal-difference learning with function approximation, IEEE Transactions on Automatic Control 42(5), 1997. https://doi.org/10.1109/9.580874
• H. Yu, D. P. Bertsekas, Error bounds for approximations from projected linear equations, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0441
• B. T. Polyak, A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM Journal on Control and Optimization 30(4), 1992. https://doi.org/10.1137/0330046

Motivation

Min-sum set cover asks for an order of the elements of a ground set that minimizes the average time at which a hyperedge is first covered. Feige, Lovász and Tetali showed that the greedy algorithm is a 4-approximation and that no better constant is possible unless P = NP (Feige, Lovász, Tetali 2004). Min-sum vertex cover, pipelined set cover, precedence-constrained min-sum set cover and ordinary set cover are relatives of it. Happach and Schulz observe that all of them are single-machine scheduling problems with a mixture of AND-precedence constraints (a job waits for all of its predecessors) and OR-precedence constraints (a job waits for at least one of its predecessors) (Happach, Schulz, arXiv:2001.07011v1, pp.1–3). For min-sum set cover the vertices are jobs of length 1 and weight 0. The hyperedges are jobs of length 0 and weight 1, and each hyperedge has its vertices as OR-predecessors.

The paper gives one LP-based algorithm for this whole class. Its guarantee depends on a single structural parameter: the largest number of OR-predecessors of a job.

Setting

The jobs are $N=A\,\dot\cup\,B$. Job $j$ has a processing time $p_j\ge0$ and a weight $w_j\ge0$. The AND-arcs $E_\wedge\subseteq(A\times A)\cup(B\times B)$ form an acyclic digraph. The OR-arcs $E_\vee\subseteq A\times B$ define $\mathcal P(b)=\{a\in A:(a,b)\in E_\vee\}$, the OR-predecessors of $b\in B$, which may be empty.

A schedule is a vector of completion times $C\in\mathbb R^N$ on one machine. Job $j$ runs without interruption in $[C_j-p_j,C_j]$, no two jobs overlap, and the machine starts at time 0. The schedule is feasible if

$$C_j\ \ge\ C_i+p_j\quad\text{for }(i,j)\in E_\wedge,\qquad C_b\ \ge\ \min_{a\in\mathcal P(b)}C_a+p_b\quad\text{for }b\in B,\ \mathcal P(b)\ne\emptyset.$$

Idle time is allowed. The objective is $\sum_{j\in N}w_jC_j$.

An OR-arc $(a,b)$ is redundant if another OR-predecessor $a'\in\mathcal P(b)$ is a transitive AND-predecessor of $a$, since $a'$ always finishes first. With redundant arcs removed,

$$\Delta\ =\ \max\Bigl(1,\ \max_{b\in B}|\mathcal P(b)|\Bigr).$$

The algorithm works on a normalized instance. Weights on $A$ are moved to new zero-length successors in $B$, the jobs that can complete at time 0 are set aside, and the processing times are scaled to integers. For $p_j\in\{0,1\}$ it solves the time-indexed LP (1) with variables $x_{jt}$, $t\in[T]$, $T=\sum_jp_j$. For general $p$ it solves the interval-indexed LP (5) over the intervals $(\tau_{l-1},\tau_l]$, $\tau_l=(1+\varepsilon')^{l-1}$. For an optimal $\bar x$, the $\alpha$-point of $j$ is $t_j^\alpha=\min\{t:\sum_{s\le t}\bar x_{js}\ge\alpha\}$ (the $\alpha$-interval for LP (5)). For $\beta\in(0,1]$ and $\alpha=\beta/\Delta$, the $\beta$-schedule sorts the $A$-jobs by $t_a^\alpha$ and the $B$-jobs by $t_b^\beta$. Ties are broken along the precedences and otherwise arbitrarily, and the jobs are processed in this order without idle time.

Formalization targets

Goal: Theorem 1 (p.4)

For every instance with $p_j\in\{0,1\}$, LP (1) of the normalized instance has an optimal solution. For every optimal $\bar x$ and every $\beta\in(0,1]$, $\beta$-schedules exist and are feasible. An explicit set of at most $n'T'+1$ candidate values of $\beta$, with $T'\le n'\le2n$, contains a $\beta$ such that every tie-breaking gives

$$\sum_{j\in N}w_jC_j(\beta)\ \le\ 2\Delta\cdot\sum_{j\in N}w_jC^*_j\qquad\text{for every feasible schedule }C^*.$$

For every $\varepsilon>0$ and rational $p_j\ge0$, the same holds with LP (5), $\varepsilon'=\varepsilon/(2\Delta')$, at most $n'L+1$ candidates, $L\le2+(1+\varepsilon')\log T'/\varepsilon'$, and the ratio $2\Delta+\varepsilon$.

The guarantee is stated for every optimal LP solution and every tie-breaking. The cost counts the weights of all jobs of the original instance.

Milestones

The milestones follow the paper's proof:

• the two w.l.o.g. reductions (redundant OR-arcs, p.4; normalization, p.6);
• LP (1) is a relaxation (p.7);
• every $\beta$-schedule is feasible (proof of Lemma 1, p.8);
• displays (2) and (3), and Lemma 1, the randomized $2\Delta$ bound;
• Lemma 2, the finite set of candidate values of $\beta$;
• LP (5) is a relaxation (p.9);
• displays (27) and (28), and Lemma 3, the randomized $(2\Delta+\varepsilon)$ bound;
• the derandomization of Algorithm 2 (p.10).

Significance

For min-sum vertex cover, where every hyperedge has two vertices, the theorem gives a 4-approximation even under precedence constraints (Corollary 1, p.9). For min-sum set cover it gives a $2\Delta$-approximation, where $\Delta$ is the largest hyperedge. The same analysis covers AND-only scheduling ($\Delta=1$, ratio 2) and mixed AND/OR constraints. With release dates added, the bound becomes $2\Delta+2$ (Lemma 4, not in this mission).

Theorem 1 is proved in the paper. To this mission's knowledge it has no machine-checked proof, and Prove2Me has no prior formalization of OR-precedence scheduling. The mission adds a model of AND/OR-precedence schedules, the two LP relaxations, $\alpha$-points of an LP solution, and the derandomization by candidate values of $\beta$. It also corrects constraint (5f): as printed, LP (5) is infeasible on some instances.

Difficulty

The analysis is short, but every object it uses has edges. Three points need care.

• The OR-constraint holds only because $\alpha=\beta/\Delta$ is smaller than $\beta$. The bound $\beta/|\mathcal P(b)|\ge\alpha$ needs $|\mathcal P(b)|\le\Delta$, which is why redundant arcs are removed before $\Delta$ is computed.
• Constraint (1d) is imposed only for $t\in[T-p_b]$, and the proof applies it at $t^\beta_b-p_b$, which can be 0.
• The expectation over the random $\beta$ must turn into one good $\beta$ in a finite candidate set. That step needs the $\beta$-schedules to depend on $\beta$ only through finitely many breakpoints.

The normalization is also not routine. Deleting a zero-length job literally can remove the cheapest OR-predecessor of another job and raise the optimum. The mission therefore sets aside the least closed set of jobs that can complete at time 0.

Formalization scope

• Instances. Finite types A, B, jobs A ⊕ B. Processing times are in ℚ≥0 (part (i) assumes them in $\{0,1\}$) and weights are in ℝ≥0. The AND-arcs are relations inside A and inside B with acyclic transitive closure (Acyclic).
• Schedules. A schedule is C : N → ℝ, feasible as above. The comparison is with every feasible schedule, not with an infimum.
• Orders. An order is σ : N ≃ Fin |N|, and its list schedule is $C_j=\sum_{\sigma(i)\le\sigma(j)}p_i$.
• LP time. Time slots are $1,\dots,T$, $\alpha$-points are sInf over ℕ, and $L\ge1$.
• (5f). The corrected constraint is x_jl = 0 when $\tau_l<p_j$.
• Algorithm. "There is a polynomial-time algorithm" is stated through the paper's algorithm: the guarantee for every LP optimum, and an explicit polynomial number of candidate values of $\beta$. LP solvability is cited from the paper, not formalized. A bare "there is a schedule within $2\Delta$ of optimal" would be trivially true and is not the target.

Contributions are welcome on any milestone. The reusable parts are the LP relaxation lemmas, the $\alpha$-point integral identities (2) and (27), and the derandomization lemma.

Selected references

• F. Happach, A. S. Schulz, Approximation Algorithms and LP Relaxations for Scheduling Problems Related to Min-Sum Set Cover, arXiv:2001.07011v1, 2020. https://arxiv.org/abs/2001.07011v1
• U. Feige, L. Lovász, P. Tetali, Approximating min sum set cover, Algorithmica 40, 2004. https://doi.org/10.1007/s00453-004-1110-5
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Math. Oper. Res. 22, 1997 (journal successor of the paper's [25], the source of α-points). https://doi.org/10.1287/moor.22.3.513

Motivation

Many contracts in finance and insurance give their holder several exercise rights that must be used at distinct dates: swing options in energy markets, flexible interest-rate caps, partial surrender options in life insurance. Valuing such a contract is an optimal multiple stopping problem. When the model itself is uncertain, or when the holder is risk averse, the value is not an expectation but a nonlinear evaluation: a robust (worst-case) expectation over a set of priors, a recursive coherent risk measure, or a $g$-expectation. Laeven, Schoenmakers, Schweizer and Stadje (arXiv:2006.01802v2) treat all of these at once through a dynamic monetary utility functional (DMU) and prove an additive dual representation of the value in terms of martingales, with no stopping times in it.

Timeline of the dual approach this mission builds on:

• Rogers (2002) and Haugh–Kogan (2004): additive (martingale) duality for single optimal stopping under a linear expectation.
• Schoenmakers (2012): a pure martingale dual for multiple stopping under a linear expectation.
• Krätschmer–Schoenmakers (2010) and Krätschmer, Ladkau, Laeven, Schoenmakers and Stadje (2018): additive duality for single stopping under dynamic monetary utility functionals, not in pathwise form.
• Laeven–Schoenmakers–Schweizer–Stadje (2020, revised 2021): pathwise duality for multiple stopping under a DMU, Theorem 3.1, which is the goal here. The authors note that "already when $L\equiv1$, Theorem 3.1 is new" (p.8).

Setting

Let $(\Omega,(\mathcal F_t)_{t\ge0},P)$ be a filtered probability space and $N$ an exercise horizon. Positions form a linear subspace $\mathfrak X$ of $L^0(\Omega,\mathcal F_N,P)$ that is closed under $\wedge$ and $\vee$ and contains every indicator $1_A$, $A\in\mathcal F_N$. A DMU is a family $\rho_t:\mathfrak X\to\mathfrak X\cap L^0(\mathcal F_t)$, $t\le N$, satisfying

• (C1) monotonicity, $X\le Y\Rightarrow\rho_t(X)\le\rho_t(Y)$;
• (C2) regularity, $\rho_t(1_AX)=1_A\rho_t(X)$ for $A\in\mathcal F_t$;
• (C3) recursiveness, $\rho_t=\rho_t\circ\rho_{t+1}$;
• (C4) conditional translation invariance, $\rho_t(X+Y)=\rho_t(X)+Y$ for $\mathcal F_t$-measurable $Y$.

Two further properties are used. (P1) is subadditivity, $\rho_t(X+Y)\le\rho_t(X)+\rho_t(Y)$. (P2) is sensitivity: $X\le0$ and $\rho_t(X)\ge0$ imply $X=0$. All (in)equalities between random variables hold almost surely.

A reward $H=(H_t)$ is adapted with $H_t\in\mathfrak X$; it may take either sign. A $\rho$-martingale is an adapted $M$ with $M_t=\rho_t(M_{t+1})$, and $\mathcal M^\rho_0$ is the set of those with $M_0=0$. The holder of $l$ rights chooses stopping times $r\le\tau_1<\dots<\tau_l\le N$, and the upper Snell envelope is

$$Y^{*,l}_r=\operatorname*{ess\,sup}_{r\le\tau_1<\dots<\tau_l\le N}\rho_r\Big(\sum_{k=1}^{l}H_{\tau_k}\Big),\qquad Y^{*,0}\equiv0 .$$

The $\rho$-Doob martingale $M^{*,l}$ of $Y^{*,l}$ has $M^{*,l}_0=0$ and increments $M^{*,l}_{r+1}-M^{*,l}_r=Y^{*,l}_{r+1}-\rho_r(Y^{*,l}_{r+1})$.

Formalization targets

Goal: Theorem 3.1

Let $\rho$ satisfy (C1)–(C4) and (P1), let $H$ be adapted and $L\ge1$. Then the envelopes exist, satisfy the Bellman principle

$$Y^{*,l}_r=\max\big[H_r+\rho_r(Y^{*,l-1}_{r+1}),\ \rho_r(Y^{*,l}_{r+1})\big],$$

and, for every $t$ with $t+L\le N+1$ and with $j_0=t$,

$$Y^{*,L}_t=\inf_{M^{(1)},\dots,M^{(L)}\in\mathcal M^\rho_0}\rho_t\Big(\max_{t\le j_1<\dots<j_L}\sum_{k=1}^{L}\big(H_{j_k}+M^{(k)}_{j_{k-1}}-M^{(k)}_{j_k}\big)\Big).$$

The infimum is attained at $M^{(k)}=M^{*,L-k+1}$. If $\rho$ is also sensitive, then $Y^{*,L}_t$ equals the pathwise maximum at these martingales almost surely.

Milestones

In proof order: (C5)–(C6); optional sampling for $\rho$-martingales (Lemma 2.1); the stopped functional $\rho_\tau$ (Lemma 2.2); the first display of the proof of Proposition A.2; weak duality for one right (Lemma B.1); its $L$-right version (B.1); weak duality (B.3)–(B.4); the $\rho$-Doob decomposition (2.4)–(2.5); the Bellman principle (3.5) with existence and attainment of the envelopes; the backward recursion (4.13) of Proposition 4.4; and the pathwise upper bound of p.41.

Significance

The theorem replaces a supremum over $L$-tuples of stopping times by an infimum over $L$ martingales, evaluated pathwise. Any choice of martingales therefore gives an upper bound on the value of the contract, and a near-optimal choice gives a tight one. Under sensitivity the optimal martingales are surely optimal: the pathwise maximum is already constant given $\mathcal F_t$. These facts drive the primal–dual algorithm and its convergence analysis in §4 and the explicit upper and lower bounds in a Brownian–Poisson filtration in §5. With $\rho$ the conditional expectation, the theorem recovers the known pathwise dual for linear multiple stopping.

The result is proved in the paper; to the authors' knowledge none of it is formalized. A machine-checked version adds three things. It verifies the Bellman principle (3.5) and the existence of the essential suprema for $L\ge2$, which the paper states without proof. It records the correct reading of the problem after the last date. And it repairs one step of the published argument (next section).

Difficulty

The weak-duality half goes by induction on $L$ through stopped functionals $\rho_\tau$. Each step needs (C2)–(C4) to commute $\rho$ with indicators of events $\{\tau=j\}$, and subadditivity to remove the martingale penalty. Since $\rho$ is nonlinear, no linearity of expectation is available, and every exchange must be justified from the axioms.

The obvious argument for the pathwise upper bound fails. The printed proof (p.41) telescopes the Doob increments and bounds each bracket $H_{j_k}+Y^{*,L-k}_{j_k}-Y^{*,L-k+1}_{j_k}$ by $0$. That inequality is false: take $N=1$, $\rho=\mathrm{id}$, $H=(1,0)$, $L=2$, $j_1=0$; the bracket equals $1$. The theorem itself is unaffected. The bound follows instead by backward induction on the date and the number of rights through the recursion (4.13), using only (3.5) and the definition of the Doob martingales.

A second subtlety is the end of the time grid. If rights may lapse at the last date and $H$ can be negative, two natural readings of the paper's extension "$H_j\equiv0$, $\mathcal F_j\equiv\mathcal F_T$ for $j>T$" disagree, and under one of them (3.5) fails. The mission therefore works on an arbitrary exercise horizon $N$, which covers both the original problem ($N=T$, $L=1$) and the extended problem ($N=T+L$).

Formalization scope

Random variables are classes in Ω →ₘ[P] ℝ, so every (in)equality is almost sure. Essential suprema and infima are IsLUB and IsGLB in this lattice, and the pathwise maximum is a finite lattice supremum Finset.sup' over the tuples $t\le j_1<\dots<j_L\le N$. A stopped value $H_\tau$ is the class of $\sum_{j\le N}1_{\{\tau=j\}}H_j$. Stopping times are $\mathbb N$-valued Mathlib IsStoppingTimes, and stopping vectors are ordered almost surely, with the optimum attained by a surely ordered vector. Rights are indexed from $0$, so the paper's superscript $L-k+1$ becomes L - k. The clause (C2) includes $1_AX\in\mathfrak X$, which the paper presupposes when it evaluates $\rho_t(1_AX)$.

At $r+l=N+1$ the Bellman principle keeps only its first branch: the remaining $l$ rights must be exercised at $r,\dots,N$. This is not a change of the theorem. With $N=T+L$ and $\rho_j=\mathrm{id}$, $H_j=0$ for $j>T$, every date $r\le T$ has $r+l\le N$, and those $\rho_j$ again satisfy (C1)–(C4), (P1) and (P2).

The goal is an existence statement for the envelopes, so it cannot hold vacuously, and the essential supremum is not assumed to exist. The identity functional with the constant filtration satisfies every hypothesis, so none of them is contradictory.

The definitions (DMU, $\rho$-martingale, stopped values, stopping vectors, Snell envelopes, $\rho$-Doob martingale, pathwise dual maximum) are reusable for any discrete-time nonlinear optimal stopping development. Contributions of every milestone are welcome. The Bellman principle with existence and attainment, and the backward recursion (4.13), are the most self-contained.

Selected references

• R. J. A. Laeven, J. G. M. Schoenmakers, N. Schweizer, M. Stadje, Robust Multiple Stopping — A Pathwise Duality Approach, arXiv:2006.01802v2, 2021. https://arxiv.org/abs/2006.01802
• L. C. G. Rogers, Monte Carlo valuation of American options, Mathematical Finance 12, 271–286, 2002. https://doi.org/10.1111/1467-9965.02010
• M. B. Haugh, L. Kogan, Pricing American options: a duality approach, Operations Research 52, 258–270, 2004. https://doi.org/10.1287/opre.1030.0070
• J. Schoenmakers, A pure martingale dual for multiple stopping, Finance and Stochastics 16, 319–334, 2012.
• V. Krätschmer, J. Schoenmakers, Representations for optimal stopping under dynamic monetary utility functionals, SIAM Journal on Financial Mathematics 1, 811–832, 2010.
• V. Krätschmer, M. Ladkau, R. J. A. Laeven, J. G. M. Schoenmakers, M. Stadje, Optimal stopping under uncertainty in drift and jump intensity, Mathematics of Operations Research 43, 1177–1209, 2018.