Missions · Prove2Me

Completed

Economics Operations Research Statistics·Captain: mikedeng1

Herding in Probabilistic Forecasts: The Normal Forecast with the Morris–Shin Mean and Variance a(x−y)²+d Is an Equilibrium, Unique Among Polynomially Bounded ProfilesResearch Paper

Motivation

Panels of professional forecasters — the European Central Bank's Survey of Professional Forecasters, the Federal Reserve's surveys, election and sports forecasters — increasingly report probabilistic forecasts: a whole predictive distribution rather than a single number. Aggregating such panels presumes that each forecast reflects the forecaster's own information. Forecasters, however, are also judged against each other, and an expert who strays far from the consensus risks being wrong alone. This tendency to move toward the crowd is called herding.

For point forecasts, herding has a standard model: the beauty-contest game of Morris and Shin (2002), in which each agent trades off accuracy against closeness to the average action, and whose unique linear equilibrium overweights public information. Jia, Keppo and Satopää (SSRN 3674961) extend this game from point forecasts to normal probabilistic forecasts, scoring accuracy with the logarithmic score and deviation with the Kullback–Leibler divergence. Their Theorem 1 gives the equilibrium in closed form; it drives their analysis of information disclosure and their structural estimation of the herding level from survey data.

Setting

A state $\theta \in \mathbb R$ is unknown, with the improper flat prior $\pi(\theta) \propto 1$ . There are $K \ge 2$ experts. Expert $k$ observes a public signal $y = \theta + \epsilon_y$ and a private signal $x_k = \theta + \epsilon_{x_k}$ , with independent noises $\epsilon_y \sim N(0, \tau_y^{-1})$ and $\epsilon_{x_k} \sim N(0, \tau_x^{-1})$ , precisions $\tau_x, \tau_y > 0$ . Expert $k$ 's posterior of $\theta$ given $(x_k, y)$ is the normalized likelihood; its mean and variance are

\hat\theta_k = \frac{\tau_x}{\tau_y+\tau_x}x_k + \frac{\tau_y}{\tau_y+\tau_x}y, \qquad \hat\sigma^2_\theta = (\tau_y+\tau_x)^{-1}.

Given $(x_k, y)$ , another expert's private signal $x_j$ follows the predictive law, the posterior convolved with $N(0, \tau_x^{-1})$ .

Each expert reports a forecast $a_k = (\mu_k, \sigma_k^2)$ , $\sigma_k^2 > 0$ , standing for $N(\mu_k, \sigma_k^2)$ , as a function of $(x_k, y)$ ; such an assignment for all experts is a strategy profile $s$ . The negative log score of $a = (\mu, \sigma^2)$ at $\theta$ is

E(a;\theta) = \frac{(\mu-\theta)^2}{2\sigma^2} + \tfrac12\log\sigma^2 + \tfrac12\log 2\pi,

and the KL deviation of $a_k$ from $a_j$ is

D_{KL}(a_j, a_k) = \tfrac12\Big[\frac{\sigma_j^2}{\sigma_k^2} + \frac{(\mu_k-\mu_j)^2}{\sigma_k^2} - 1 + \log\sigma_k^2 - \log\sigma_j^2\Big].

With herding level $r$ , expert $k$ chooses $a_k$ to minimize

\mathbb E\Big[(1-r)E(a;\theta) + r\,\frac{1}{K-1}\sum_{j\ne k}D_{KL}(a_j, a)\ \Big|\ x_k, y\Big]. \tag{9}

A (Bayesian Nash) equilibrium is a profile in which every expert's forecast minimizes (9) at every signal pair, given the others' strategies.

Formalization targets

Goal: Theorem 1, true part

For $0 \le r < 1$ , let

\mu^{MS}_k = \frac{(1-r)\tau_x}{(1-r)\tau_x+\tau_y}x_k + \frac{\tau_y}{(1-r)\tau_x+\tau_y}y, \qquad \sigma_k^2 = a(x_k-y)^2 + d,

a = \frac{r(1-r)\tau_x^2\tau_y^2}{[(\tau_x+\tau_y)^2 - r\tau_x^2][(1-r)\tau_x+\tau_y]^2}, \qquad d = \frac{(1+r)\tau_x+\tau_y}{(\tau_x+\tau_y)^2 - r\tau_x^2}.

The goal asserts three things: the profile $(\mu^{MS}_k, a(x_k-y)^2+d)$ is an equilibrium; every equilibrium reports the means $\mu^{MS}_k$ ; and every equilibrium whose variances grow at most polynomially in the private signal is this profile.

Milestones

(3): the flat-prior posterior is $N(\hat\theta_k, \hat\sigma^2_\theta)$ .
(EC.11)–(EC.12): against admissible opponents, the objective (9) has a unique minimizer, the forecast given by the first-order conditions.
(EC.14): the closed-form profile is admissible and solves (EC.11)–(EC.12); supporting it, the coefficient identities (EC.15)–(EC.16).
EC.5.1 uniqueness: every admissible solution of (EC.11)–(EC.12) has the means (10), and is the closed form when its variances grow polynomially.

Significance

The theorem says that herding acts on a probabilistic forecast in two separate ways. The mean shifts toward the public signal exactly as in Morris and Shin (2002), independently of the variance. The variance is inflated above the Bayesian posterior variance by a term quadratic in $x_k - y$ , so experts whose private information disagrees with the public signal report more uncertainty. Neither the mean nor the variance depends on $K$ . The paper's comparative statics, its analysis of public information disclosure (Theorem 2), and the structural estimator of $r$ (Theorem 3) all start from this closed form.

The result is proved in the paper's electronic companion by a first-order-condition argument and a reference to Morris and Shin's uniqueness argument. As printed the uniqueness claim is false (see Formalization scope), so the mission states what is true. No part of it is formalized anywhere known: the work is the Gaussian posterior under an improper prior, the best-response computation with an explicit unequal-variance KL term, and a uniqueness argument for a linear fixed-point equation driven by a Gaussian Markov kernel.

Difficulty

The best response is not a convex problem: the objective is not jointly convex in $(\mu, \sigma^2)$ , though it has a unique minimizer, and the minimizer must be found against arbitrary measurable, possibly asymmetric opponents. The main obstacle is uniqueness. The mean equation (EC.11) is a fixed point $f = rQf$ of an averaged predictive-expectation operator $Q$ . The obvious argument iterates $Q$ and uses $r < 1$ , but $Q$ is not a contraction on unbounded functions: with $u = x - y$ and $\alpha = \tau_x/(\tau_x+\tau_y)$ , $Q$ maps $e^{\gamma u^2}$ to $e^{\gamma u^2}/\alpha$ for a specific $\gamma > 0$ . At $r = \alpha$ this produces non-closed-form solutions. The means are still pinned down, but only through the variance equation (EC.12); the variances need an extra growth condition.

Formalization scope

Everything lives in the namespace HerdingForecast.Equilibrium, in one definitions file and six theorem files. Signals, states, means and variances are real numbers; experts are Fin K; a profile is a function Fin K → ℝ → ℝ → ℝ × ℝ. The improper prior gives no joint probability measure, so " $\mathbb E[\cdot \mid x_k, y]$ " is integration against two explicit laws, the normalized likelihood (posterior) and its convolution with $N(0, \tau_x^{-1})$ (predictive). The deviation is the paper's explicit KL formula, not Mathlib's klDiv. Logarithms are natural.

The following hypotheses and conventions are not printed in the paper and are disclosed in each statement:

$K \ge 2$ and $\tau_x, \tau_y > 0$ , which the model presumes.
$r < 1$ instead of $r \in [0, 1]$ . At $r = 1$ every constant profile is an equilibrium, and the paper's proof assumes $0 < r < 1$ ; $r = 0$ is included.
Admissibility: strategies are measurable, report positive variances, and have integrable mean, squared mean, variance and log-variance under the predictive law at every signal pair, so that (9) is finite. Without it Lean's integral of a non-integrable function is $0$ and spurious equilibria appear.
Best response at every signal pair, over every forecast with positive variance.
The printed uniqueness clause is false. With $\hat\sigma^2_{x_{-i}} = \hat\sigma^2_\theta + \tau_x^{-1}$ and $\gamma = (1-\alpha^2)/(2\hat\sigma^2_{x_{-i}})$ , at $r = \alpha$ the profile with means (10) and variances $a(x_k-y)^2 + d + c\,e^{\gamma(x_k-y)^2}$ , any $c > 0$ , is a second admissible equilibrium, for instance at $\tau_x = \tau_y = 1$ , $r = 1/2$ . The mission therefore poses uniqueness of the means over all equilibria, and uniqueness of the whole profile among equilibria whose variances satisfy $\sigma_k^2(x, y) \le C(1+|x|^N)$ for each $k$ and $y$ .

Two formalizations would trivialize the goal and are ruled out. The equilibrium is not defined by the first-order conditions: it is defined by minimization of (9), so the best-response milestone carries content. Uniqueness is not restricted to linear, symmetric or continuous profiles: it ranges over all admissible profiles. The paper restricts attention to symmetric equilibria (§2.2, p. 10); uniqueness over all admissible profiles contains that case.

A complete development needs Gaussian integrals of polynomials and of $\log$ of a quadratic, the convolution of Gaussians (in Mathlib), the posterior computation for a product of Gaussian densities, and an iteration argument for $f = rQf$ with Jensen's inequality and Tonelli. The posterior and predictive laws, and the Gaussian Markov-kernel argument, apply to other Gaussian beauty-contest games beyond this mission. Proofs of the milestones in any order are welcome, as is a proof of the variance-uniqueness clause under a weaker growth condition than polynomial.

Selected references

Y. Jia, J. Keppo, V. Satopää, Herding in Probabilistic Forecasts, Management Science (SSRN preprint 3674961 is the version formalized here). https://ssrn.com/abstract=3674961, DOI https://doi.org/10.1287/mnsc.2022.4487
S. Morris, H. S. Shin, Social Value of Public Information, American Economic Review 92(5), 2002, 1521–1534. https://doi.org/10.1257/000282802762024610
T. Gneiting, A. E. Raftery, Strictly Proper Scoring Rules, Prediction, and Estimation, Journal of the American Statistical Association 102(477), 2007, 359–378. https://doi.org/10.1198/016214506000001437

6 thms2 active usersReviewed

Algebraic Topology Algorithmic Game Theory Combinatorics·Captain: mikedeng1

Envy-Free Division of Multilayered Cakes: For a Prime-Power Number q of Groups with m ≤ q ≤ n, a Feasible Contiguous Group-Birthday Envy-Free Multi-Division by q − 1 Long Knives ExistsResearch Paper

Fair division of layered resources

Envy-free cake cutting asks for a division of a divisible resource, modelled as the interval $[0,1]$ , among agents with individual preferences so that no agent prefers another agent's share to its own. For a single cake and contiguous pieces, the existence of envy-free divisions goes back to Stromquist (1980) and to Su's Sperner-lemma proof (1999).

Multi-layered cake cutting, introduced by Hosseini, Igarashi and Searns (2020), models resources made of several parallel copies of a time line: meeting rooms booked over a day, or a facility with several machines shared in time slots. A bundle receives a piece of every layer, and it is feasible only if its pieces in different layers do not overlap in time, since one group cannot use two rooms at once. Igarashi and Meunier (arXiv:2106.02262v4, Mathematics of Operations Research, 2025) prove that envy-free feasible divisions exist when the number of bundles is a prime power, and they divide the agents into groups of almost equal size, each group sharing one bundle.

Timeline:

1980, Stromquist; 1999, Su: envy-free contiguous divisions of one cake for hungry agents.
2018, Segal-Halevi: envy-free division without the hungry assumption for three agents; Meunier and Zerbib (2019): for a prime number of agents.
2020, Avvakumov and Karasev: for a prime-power number of agents, and not beyond.
2020, Hosseini, Igarashi and Searns: the multi-layered model and its first existence results in special cases.
2021 (arXiv), 2025 (Mathematics of Operations Research), Igarashi and Meunier: Theorem 1 below, for any number of layers $m\le q$ .

Setting

A piece is a finite union of pairwise disjoint closed subintervals of $[0,1]$ . An $m$ -layered cake has layers $\ell\in[m]$ , each a copy of $[0,1]$ . A layered piece $\mathcal L=(L_\ell)_{\ell\in[m]}$ has one piece per layer; it is non-overlapping if $L_\ell\cap L_{\ell'}$ is empty or finite whenever $\ell\neq\ell'$ . A multi-division $\mathcal A=(\mathcal A_1,\dots,\mathcal A_q)$ is a $q$ -tuple of layered pieces covering every layer, with entries meeting in at most finitely many points of each layer. It is contiguous if each $\mathcal A_{j,\ell}$ is an interval, feasible if each $\mathcal A_j$ is non-overlapping, and obtained with $q-1$ long knives if there are positions $0=t_0\le t_1\le\dots\le t_q=1$ , the same in every layer, such that every $\mathcal A_{j,\ell}$ is one of the intervals $[t_k,t_{k+1}]$ .

Each agent $i\in[n]$ has a choice function $c_i$ that returns, for a multi-division $\mathcal A$ , the set $c_i(\mathcal A)$ of preferred layered pieces. It is invariant under permuting the entries of $\mathcal A$ , and it prefers at least one entry of $\mathcal A$ . Layered pieces are compared by the pseudo-metric $d(\mathcal L,\mathcal L')=\sum_\ell\lambda(L_\ell\triangle L'_\ell)$ , where $\lambda$ is Lebesgue measure. An agent has closed preferences if, whenever multi-divisions $\mathcal A^{(t)}$ converge entrywise to a multi-division $\mathcal A^{(\infty)}$ and $\mathcal A^{(t)}_j\in c_i(\mathcal A^{(t)})$ for all $t$ , also $\mathcal A^{(\infty)}_j\in c_i(\mathcal A^{(\infty)})$ . One agent is the birthday agent $b$ : the division is computed without its preferences, and it may pick any bundle afterwards.

Formalization targets

Goal: Theorem 1 (p. 5)

Let $m\le q\le n$ with $q$ a prime power, and let all agents have closed preferences. Then there is a feasible, contiguous multi-division $\mathcal A$ into $q$ layered pieces, obtained with $q-1$ long knives, such that for every $j^*\in[q]$ there is an assignment $\pi_{j^*}:[n]\to[q]$ with

\pi_{j^*}(b)=j^*,\qquad \mathcal A_{\pi_{j^*}(i)}\in c_i(\mathcal A)\ \ (i\neq b),\qquad \Big\lfloor\tfrac nq\Big\rfloor\le|\pi_{j^*}^{-1}(j)|\le\Big\lceil\tfrac nq\Big\rceil\ \ (j\in[q]).

The multi-division is fixed before the birthday agent chooses. The group sizes count the birthday agent.

Milestones

Lemma 2 (p. 7): the encoding $x\mapsto\mathcal A(x)$ of multi-divisions by points of the chessboard complex is equivariant, $\mathcal A_j(x)=\mathcal A_{g+j}(g\cdot x)$ .
Lemma 1 (p. 6): for $G=((\mathbb Z_p)^k,+)$ and $q=p^k$ , every $G$ -equivariant continuous map $\|\Delta_{2q-1,q}\|\to\Delta^G$ takes the value $\frac1q\sum_{g}e_g$ .
Lemma 4 (p. 10): a fractional assignment of $n-1$ agents to $q$ bundles with column sums $a_j$ rounds to an integral one supported on the same edges, with $\lfloor a_{j^*}\rfloor+1$ agents at $j^*$ (the birthday agent included) and $\lfloor a_j\rfloor$ or $\lceil a_j\rceil$ at every other $j$ .
Counting claim (proof of Theorem 1, p. 11): these sizes, for $a_j=(n-1)/q$ , lie in $\{\lfloor n/q\rfloor,\lceil n/q\rceil\}$ .
Lemma 3 (p. 8): the encoding is continuous for the pseudo-metric $d$ .

Significance

For $m=1$ and $q=n$ , Theorem 1 is the Avvakumov–Karasev theorem: an envy-free division exists even when agents may prefer empty pieces, provided the number of agents is a prime power. For general $q\le n$ it gives envy-free divisions among groups, and for $m\ge2$ a feasible schedule of $m$ parallel resources. The paper derives from it the existence of proportional feasible multi-divisions for every $q$ with $m\le q\le n$ (Theorem 5).

None of these results has been machine-checked. A formalization would add, beyond Theorem 1 itself, a Lean model of multi-layered cake cutting with choice-function preferences, the chessboard complex with its free group action, and an integral rounding lemma for bipartite assignments with a reserved slot. No statement of Volovikov's theorem or of its consequences exists on the platform yet; Lemma 1 would be the first.

Difficulty

The classical route encodes divisions by points of a simplex and applies Sperner's lemma. In the layered setting the induced coloring need not satisfy Sperner's boundary condition, even for monotone preferences (p. 6), and without hungriness it fails already for one layer. The proof therefore relies on Volovikov's Borsuk–Ulam-type theorem for $(\mathbb Z_p)^k$ -actions and on the $(q-2)$ -connectivity of the chessboard complex $\Delta_{2q-1,q}$ ; Mathlib has neither. The prime-power hypothesis is essential: for one layer and $q=n$ not a prime power, Avvakumov and Karasev show that envy-free divisions need not exist without hungriness, and Lemma 1 itself fails already for $G=\mathbb Z_6$ . Passing from triangulations to the limit needs closedness of preferences and the continuity of the encoding (Lemma 3), whose proof must handle several simplices of the configuration space accumulating at the same limit point.

Formalization scope

Layered pieces are Fin m → Set ℝ, multi-divisions Fin q → Fin m → Set ℝ, choice functions maps from multi-divisions to sets of layered pieces. "Disjoint interiors" and "non-overlapping" are encoded as finiteness of intersections, which is equivalent for finite unions of closed intervals. The pseudo-metric sums (volume (symmDiff …)).toReal over the layers. The birthday agent is an arbitrary b : Fin n; "prime power" is IsPrimePow q; group sizes are cardinalities of fibres over all of Fin n.

Three readings are disclosed:

A choice function prefers at least one entry of every multi-division. The page says it "returns the set of preferred layered pieces", and the proof asks each agent for the piece it prefers.
Lemma 4's last bullet is stated for $j\neq j^*$ . As printed, for integral $a_{j^*}$ it contradicts the third bullet; the proof gives the $j\neq j^*$ version, which is all Theorem 1 uses.
The procedure assigning simplices to supports is required to be equivariant and injective only on nonempty rook sets, which are exactly the supports of points of $\|\Delta_{2q-1,q}\|$ .

The chessboard complex is realized concretely in $\mathbb R^{[2q-1]\times G}$ , with columns indexed by $G$ , so the bijection $\eta$ of the page is the identity.

Trivializing formalizations are ruled out. Without the covering clause the empty multi-division would satisfy everything. An agent preferring nothing would make the goal false. Choosing the multi-division after the birthday agent's choice ( $\forall j^*\,\exists\mathcal A$ ) is a weaker theorem. The goal states $\exists\mathcal A\,\forall j^*\,\exists\pi$ .

A complete development needs:

simplicial complexes and their geometric realizations, with group actions;
connectivity of the chessboard complex;
Volovikov's theorem;
total unimodularity of bipartite incidence matrices, or a flow-rounding argument.

These pieces, and the cake model, are reusable beyond this mission. Contributions are welcome on any milestone.

Selected references

A. Igarashi, F. Meunier, Envy-Free Division of Multi-Layered Cakes, arXiv:2106.02262v4, 2022; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2106.02262v4
S. Avvakumov, R. Karasev, Envy-free division using mapping degree, Mathematika 67(1):36–53, 2020. https://arxiv.org/abs/1907.11183
A. Yu. Volovikov, On a topological generalization of the Tverberg theorem, Mathematical Notes 59(3):324–326, 1996 (reference [30] of the paper).
H. Hosseini, A. Igarashi, A. Searns, Fair division of time: multi-layered cake cutting, IJCAI 2020. https://arxiv.org/abs/2004.13397
F. E. Su, Rental harmony: Sperner's lemma in fair division, American Mathematical Monthly 106 (1999). https://doi.org/10.2307/2589068
J. Matoušek, Using the Borsuk–Ulam Theorem, Springer, 2003. https://doi.org/10.1007/978-3-540-76649-0

7 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Projectively Self-Concordant Barriers: Projective Self-Concordance with γ = (ν − 2)/√(ν − 1) Is Equivalent to Self-Concordance of the Logarithmically Homogeneous Extension ν(−log t + f(x/t))Research Paper

Motivation

Interior-point methods for convex programming, introduced in their modern form by Nesterov and Nemirovski, run Newton's method on a barrier function of the feasible set. Their complexity analysis rests on a single analytic property of the barrier, self-concordance: the third derivative is controlled by the second, $|F'''(x)[h,h,h]|\le 2\,(F''(x)[h,h])^{3/2}$ . This inequality is invariant under affine changes of coordinates, and it is tied to the affine structure of the space.

Hildebrand (arXiv:1909.01883v2) observes that the feasible sets of conic programs carry more structure than that. A feasible set $X=\{x : Ax=b\}\cap K$ of a conic program is a slice of a cone, and the barrier used on it is the restriction of a logarithmically homogeneous barrier of the cone. Restricted barriers of this kind satisfy a sharper, projectively invariant inequality, which the paper calls projective self-concordance. Estimates used in the analysis of interior-point methods (Dikin ellipsoids, outer approximations of the feasible set, short-step path-following parameters) improve when this extra information is used; Sections 3–8 of the paper develop those consequences.

All of those developments rest on one characterization, Theorem 1.5: a function on a convex set is projectively self-concordant with parameter $\gamma$ exactly when its logarithmically homogeneous extension to the cone over the set is self-concordant, with the sharp relation $\gamma=(\nu-2)/\sqrt{\nu-1}$ . This mission formalizes that theorem and the steps of its proof.

Setting

Let $D\subset\mathbb R^n$ be an open convex set and $f:D\to\mathbb R$ a $C^3$ function. Write $f'(x)[h]$ , $f''(x)[h,h]$ and $f'''(x)[h,h,h]$ for the first three derivatives of $f$ at $x$ in direction $h$ .

The affine metric of $f$ is the quadratic form $G(x)[h,h]=f''(x)[h,h]-(f'(x)[h])^2$ , and the cubic form is $C(x)[h,h,h]=f'''(x)[h,h,h]-6f''(x)[h,h]f'(x)[h]+4(f'(x)[h])^3$ .
Projective conditions (Definition 1.4, conditions (1) and (3)), with parameter $\gamma$ : for all $x\in D$ , $G(x)[h,h]>0$ for every $h\neq0$ , and $|C(x)[h,h,h]|\le 2\gamma\,(G(x)[h,h])^{3/2}$ for every $h$ .
The conic extension of $D$ is the open cone $K=\{(t,x)\in\mathbb R^{n+1} : t>0,\ t^{-1}x\in D\}$ .
For a real $\nu\ge2$ , the logarithmically homogeneous extension of $f$ is $F(t,x)=\nu\bigl(-\log t+f(t^{-1}x)\bigr)$ on $K$ . It satisfies $F(\tau y)=F(y)-\nu\log\tau$ for $\tau>0$ .
Affine conditions (Definition 1.1, conditions (1) and (3)): for all $y\in K$ , $F''(y)[h,h]>0$ for every $h\ne0$ , and $|F'''(y)[h,h,h]|\le 2\,(F''(y)[h,h])^{3/2}$ for every $h$ .
The proof uses the sextic $p_\mu(t)=4(\nu-1)t^6+12(\nu-2)t^4+4\mu t^3+12(\nu-3)t^2+12\mu t+4\nu-\mu^2$ in a real parameter $\mu$ .

In the Lean development these are ProjCond1, ProjCond3, AffCond1, AffCond3, conicExt, homExt and pmu in the namespace ProjSelfConcordant.ConicExt, with derivatives dk k g x h.

Formalization targets

Goal: Theorem 1.5

With $\gamma=(\nu-2)/\sqrt{\nu-1}$ and $\nu\ge2$ ,

\Bigl(f \text{ satisfies (1), (3) of Def. 1.4 on } D \text{ with } \gamma\Bigr)\iff\Bigl(F \text{ satisfies (1), (3) of Def. 1.1 on } K\Bigr).

Both directions are required, and each side is the conjunction of the two conditions, as on the page.

Milestones (Section 2, p. 5)

At $x=(1,\tilde x)$ and $h=(0,\tilde v)+\alpha(1,\tilde x)$ :

F''(x)[h,h]=\nu(\alpha^2-2\alpha f'[\tilde v]+f''[\tilde v,\tilde v]),\quad F'''(x)[h,h,h]=\nu(-2\alpha^3+6\alpha^2f'[\tilde v]-6\alpha f''[\tilde v,\tilde v]+f'''[\tilde v,\tilde v,\tilde v]).

Condition (1) of Definition 1.4 for $f$ is equivalent to condition (1) of Definition 1.1 for $F$ .
With $c_2=G[\tilde v,\tilde v]>0$ and $\mu=c_2^{-3/2}C[\tilde v,\tilde v,\tilde v]$ , the cubic inequality in $\alpha$ is equivalent to $p_\mu(t)\ge0$ for all $t$ .
For $\nu=\kappa^2+1$ , $\kappa\ge1$ : closed forms of $p_\mu(\mp\kappa^{-1})$ as products of two factors linear in $\mu$ .
Both $p_\mu(\pm\kappa^{-1})\ge0$ if and only if $|\mu|\le 2(\kappa^2-1)/\kappa=2\gamma$ .
$F''(\tau y)[\tau h,\tau h]=F''(y)[h,h]$ and $F'''(\tau y)[\tau h,\tau h,\tau h]=F'''(y)[h,h,h]$ for $\tau>0$ .
Factorizations of $p_{\pm2\gamma}(t)$ , showing both are nonnegative.
$|\mu|\le2\gamma$ implies $p_\mu(t)\ge0$ for all $t$ .

Significance

Theorem 1.5 identifies projective self-concordance with a familiar object, so every later result of the paper can be read either on the set or on the cone. Corollary 1.6 derives from it the passage between projectively and affinely self-concordant barriers on the same set. The improved inner and outer approximations of Section 3 and the duality theory of Section 5 are stated for projectively self-concordant functions, and Theorem 1.5 is what makes them applicable to the restrictions of standard conic barriers (log-det, logarithmic barriers of the orthant, the second-order cone barrier). The constant $\gamma=(\nu-2)/\sqrt{\nu-1}$ is sharp: for $|\mu|$ slightly above $2\gamma$ the sextic $p_\mu$ takes negative values.

The result is proved in the paper. As far as is known, neither it nor the general theory of projective self-concordance has a machine-checked proof; the platform's self-concordance vocabulary covers the affine notion only. A formal proof contributes reusable calculus for logarithmically homogeneous functions on cones (the derivatives of $(t,x)\mapsto f(t^{-1}x)$ , and the homogeneity of $F''$ and $F'''$ ) and a certified treatment of the sextic inequality that fixes the sharp constant.

Difficulty

The argument has two different parts. The first is multivariable calculus: computing the second and third Fréchet derivatives of $F(t,x)=\nu(-\log t+f(t^{-1}x))$ at points of the slice $t=1$ , along directions with a component in $t$ , and transferring them along rays by homogeneity. In Lean this means iterated derivatives of compositions with the nonlinear map $(t,x)\mapsto t^{-1}x$ , restricted to an open set on which $f$ is only $C^3$ , and with derivatives taken in a product space.

The second is real algebra. The affine condition (3) along a two-dimensional slice is a degree-six polynomial inequality in $\alpha$ ; after normalization it becomes nonnegativity of $p_\mu$ for all $t$ , and the content of the theorem is that the set of $\mu$ for which this holds is exactly $[-2\gamma,2\gamma]$ . Checking finitely many values of $t$ gives only necessity; sufficiency needs a certificate of nonnegativity at the endpoints and an argument for the interval in between. Direct expansion produces sextics whose nonnegativity is not visible term by term.

The equivalence is between conjunctions of conditions (1) and (3). Splitting it into one equivalence for each condition is not what the page claims: the conditions (3) are only meaningful where the forms of condition (1) are nonnegative.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and $\mathbb R^{n+1}$ is ℝ × EuclideanSpace ℝ (Fin n), first coordinate $t$ . The product carries the sup norm; Fréchet derivatives do not depend on the choice of norm in finite dimensions.
$f:\mathbb R^n\to\mathbb R$ and $F:\mathbb R^{n+1}\to\mathbb R$ are total functions. Since $D$ and $K$ are open, derivatives at their points depend only on values inside them. Regularity is ContDiffOn ℝ 3 f D.
Derivatives are iterated Fréchet derivatives evaluated on the diagonal, iteratedFDeriv ℝ k g x (fun _ => h). Positive definiteness is strict positivity of the quadratic form on nonzero vectors. Tangent vectors range over the whole ambient space.
$(\cdot)^{3/2}$ is Real.rpow. Condition (3) appears only in conjunction with condition (1), under which its bases are nonnegative.
Only conditions (1) and (3) of Definitions 1.1 and 1.4 enter. The barrier condition (2), the parameter condition (4), regularity of a closed set, and convexity of $F$ are not hypotheses. No nonemptiness of $D$ and no $n\ge1$ is assumed; the statement holds as written in those cases.
A trivializing formalization is ruled out: $\gamma$ is not a free parameter but the explicit $(\nu-2)/\sqrt{\nu-1}$ with $\nu\ge2$ , both directions of the equivalence are required, and $F$ is the explicit extension of $f$ , not a function constrained by hypotheses.
The algebraic milestones 3–5, 7, 8 are stated on abstract reals (the page's $c_2$ , $c_3$ , $t$ , $\mu$ are exactly those expressions) and need no calculus. Milestones 1, 2 and 6 need derivative computations on product spaces that are reusable for any logarithmically homogeneous extension.

Contributions are welcome on either layer, and alternative proofs of the sextic bounds (for example sum-of-squares certificates) are as useful as transcriptions of the paper's argument.

Selected references

R. Hildebrand, Projectively self-concordant barriers, Mathematics of Operations Research, 2022; preprint arXiv:1909.01883v2 (2021). https://arxiv.org/abs/1909.01883
Y. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791
J. Renegar, A Mathematical View of Interior-Point Methods in Convex Optimization, MPS-SIAM Series on Optimization, 2001. https://doi.org/10.1137/1.9780898718812

10 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Coordinating Project Outsourcing Through Bilateral Contract Negotiations: Bargaining Powers Under Which Each Contract Form Coordinates a Single-Task ProjectResearch Paper

Why contract forms matter in project outsourcing

Large projects such as buildings, infrastructure and software systems are routinely outsourced. The client who owns the project pays a subcontractor to execute it, and the subcontractor privately chooses how hard to work. Faster work costs him more, while the benefit of early completion goes mainly to the client. The paper notes that the fixed-price and cost-plus contracts are the two most widely used contract forms in practice, and that their terms are typically negotiated rather than dictated by one side.

Hou, Lu, Deng and Shen ask which contract forms align the subcontractor's choice of work rate with the system optimum once the terms are set by bilateral bargaining, and how the answer depends on the two firms' bargaining powers. Most earlier project-contracting models (Bayiz and Corbett, 2005; Kwon, Lippman and Tang, 2010; Chen, Klastorin and Wagner, 2015) let one party make a take-it-or-leave-it (Stackelberg) offer; Lippman, McCardle and Tang (2013) is a bargaining exception. That is the extreme case of a Nash bargaining framework with all the power on one side. This mission formalizes the single-task part of the paper (Section 3), whose main result is Proposition 1.

Setting

A client receives a one-time reward $Q>0$ when the project is completed. The subcontractor chooses a constant work rate $r\ge0$ . Let $Z\ge0$ be a random variable with a density, cdf $F$ and mean $\mathbb E[Z]=1$ ; at work rate $r>0$ the task duration is $T=Z/r$ . Both firms discount at rate $\alpha>0$ . The subcontractor's realized total discounted cost is $C(r,T)$ , with expectation $c(r)=\mathbb E[C(r,T)]$ . The standing assumptions are:

Assumption 1: $F$ is strictly concave;
Assumption 2: $c$ is differentiable, increasing and strictly convex, with $c(0)=0$ and $c'(0)=0$ .

The system profit is

\Pi(r)=Q\,\mathbb E_Z[e^{-\alpha Z/r}]-c(r),

and $r^*$ denotes its maximizer, with $\Pi^*=\Pi(r^*)$ .

A contract form $m$ specifies a payment $\rho^m$ , valued at completion, as a function of a term $\Psi^m=(p,\beta)$ , of $T$ and of the realized cost $C$ :

form	payment	parameter
fixed-price FP	$p$	—
two-part fixed-price TF+, TF	$p+\beta e^{\alpha T}$	$\beta\ge0$ (TF+), $\beta\in\mathbb R$ (TF)
time-based incentive TB	$pe^{-\beta T}$	$\beta\ge0$
cost-sharing CS	$p+\beta Ce^{\alpha T}$	$\beta\in[0,1]$
cost-plus C+	$p+Ce^{\alpha T}$	—

In the two-part contract, $\beta$ is a down payment made at the start of the task. The subcontractor's profit $\Pi^m_S(\Psi,r)$ is his expected discounted payment minus $c(r)$ , and the client's profit $\Pi^m_C(\Psi,r)$ is the expected discounted reward minus the payment. Given a term $\Psi$ , the subcontractor chooses a rate $\hat r^m(\Psi)$ maximizing $\Pi^m_S(\Psi,\cdot)$ . When his profit is flat in $r$ , he chooses the system-optimal rate (footnote 1 of the paper).

The term is fixed by Problem B, the generalized Nash bargaining problem with disagreement points $0$ :

\max_{\Psi}\ \big[\Pi^m_S(\Psi,\hat r^m(\Psi))\big]^{\theta}\big[\Pi^m_C(\Psi,\hat r^m(\Psi))\big]^{1-\theta}\quad\text{s.t. both profits}\ \ge0,

where $\theta\in[0,1]$ is the subcontractor's bargaining power. Form $m$ coordinates the system at $\theta$ if Problem B has a solution and every solution induces $\hat r^m=r^*$ . The set of such $\theta$ is $\Phi^m$ . Finally,

\delta^{TB}_S(\beta)=\frac{\alpha Q\,\mathbb E_Z[Ze^{-\alpha Z/r^*}]\,\mathbb E_Z[e^{-(\alpha+\beta)Z/r^*}]}{(\alpha+\beta)\,\mathbb E_Z[Ze^{-(\alpha+\beta)Z/r^*}]}-c(r^*)

is the subcontractor's profit under the TB term with parameter $\beta$ that induces $r^*$ .

Formalization targets

Goal: Proposition 1

\Phi^{FP}=\Phi^{TF+}=\{1\},\qquad \Phi^{TB}=\{\theta\in[0,1]:\theta\Pi^*\in\delta^{TB}_S([0,\infty))\},\qquad \Phi^{TF}=\Phi^{CS}=[0,1],\qquad \Phi^{C+}=\{0\},

and every bargaining solution at $\theta\in\Phi^m$ has the negotiated terms

\hat p^{FP}=Q;\quad (\hat p^{TF+},\hat\beta^{TF+})=(Q,0);\quad (\hat p^{TF},\hat\beta^{TF})=(Q,-(1-\theta)\Pi^*);\quad (\hat p^{CS},\hat\beta^{CS})=(\theta Q,1-\theta);\quad (\hat p^{C+},\hat\beta^{C+})=(0,1),

with $\delta^{TB}_S(\hat\beta^{TB})=\theta\Pi^*$ and $\hat p^{TB}=\alpha\mathbb E_Z[Ze^{-\alpha Z/r^*}]Q/\big((\alpha+\hat\beta^{TB})\mathbb E_Z[Ze^{-(\alpha+\hat\beta^{TB})Z/r^*}]\big)$ . The goal also states that the TB set equals the printed interval $[\underline\delta^{TB}_S/\Pi^*,1]$ when the minimum of $\delta^{TB}_S$ is attained, and that for FP, TF+ and TB no bargaining solution outside $\Phi^m$ induces $r^*$ .

Milestones

§3, p. 7: $\mathbb E_Z[e^{-sZ/r}]=s\int_0^\infty e^{-st}F(rt)\,dt$ for $s,r>0$ .
§3, p. 8, (2): $\Pi$ is concave, $r^*$ exists and is unique, and $\Pi'(r^*)=Q\frac{\alpha}{(r^*)^2}\mathbb E_Z[Ze^{-\alpha Z/r^*}]-c'(r^*)=0$ .
§3.2, p. 10: for $p\ge0$ the subcontractor's profit is concave in $r$ , and every best response satisfies the first-order condition (as a right derivative at the corner $\hat r=0$ ).
to 7. Proposition 1 split by contract form: (TF, CS), (FP, TF+), (C+), (TB).

Significance

Proposition 1 separates the contract forms by how much bargaining power they tolerate. The fixed-price and cost-plus contracts, the two forms most used in practice, coordinate the project only when one party holds all the power. The two-part fixed-price contract and the cost-sharing contract coordinate for every $\theta$ , at the price of a participation fee or of cost verification. The time-based incentive contract coordinates above a threshold. This classification is the base case for the paper's multi-task results (parallel and serial tasks, Propositions 2–4), which show that coordination degrades further when several subcontractors bargain separately. It also explains a common practical observation: commonplace contracts leave efficiency on the table whenever power is shared.

The proofs are in the paper's online appendix and have not been machine-checked. A formal proof would check the "only if" directions, which rest on an argument (following Horn and Wolinsky, 1988, and Feng and Lu, 2013b) that the upper frontier of the feasible set is that of a convex set. It would also settle the boundary of the TB set (see below) and produce a reusable Lean layer for Nash bargaining over contract terms with an induced best response.

Difficulty

The bargaining is over a contract term, and the payoffs depend on the subcontractor's induced work rate. The feasible set of profit pairs is therefore not convex in general, and Nash's theorem cannot be applied to it directly. Showing that the Nash product is maximized exactly at the coordinating terms needs global control of the best-response map $\Psi\mapsto\hat r^m(\Psi)$ : its existence, uniqueness and continuity, and the envelope behaviour of both profits along it. The naive argument "coordinating terms put the total profit at $\Pi^*$ , so they must be optimal" fails twice. Under FP and TB the coordinating terms cannot reach every split of $\Pi^*$ . Under C+ with $\theta>0$ every feasible outcome gives the subcontractor zero profit, so maximizing the Nash product selects nothing. The expectations involve a general scale family, so no closed forms are available. Concavity in $r$ has to come from Assumption 1 through the integration-by-parts identity of milestone 1.

Formalization scope

The model is a structure holding $Q$ , $\alpha$ , the law $\mu$ of $Z$ as a measure on $\mathbb R$ , the realized cost $C$ and the expected cost $c$ , together with a validity predicate for the standing assumptions. Contract terms are pairs $(p,\beta)\in\mathbb R^2$ . For FP the dummy $\beta$ is pinned to $0$ , and for C+ to $1$ . Expectations are Bochner integrals. Conventions and added hypotheses:

$\alpha>0$ is added; the page only says "discount rate".
Integrability of the realized cost $C(r,Z/r)$ is added, so that $c(r)=\mathbb E[C]$ is meaningful.
Every discounted quantity is $0$ at $r=0$ , except the TF/TF+ down payment, which is still received. This is the limit $r\downarrow0$ , and it avoids Lean's $z/0=0$ .
The best response is a relation with footnote 1's tie-break. Problem B is posed over pairs (term, induced rate), so a term without a best response is infeasible.
The Nash product uses Real.rpow on nonnegative profits, so $0^0=1$ makes it $\Pi_S$ at $\theta=1$ and $\Pi_C$ at $\theta=0$ .
Milestone 3 adds $p\ge0$ : for $p<0$ the page's concavity claim can fail.
$r^*$ is a variable satisfying the optimality predicate; milestone 2 supplies its existence and uniqueness.
The TB set is corrected. The printed $[\underline\delta^{TB}_S/\Pi^*,1]$ fails at its left endpoint in the paper's own Example 1, where $\delta^{TB}_S$ is strictly decreasing and never attains its infimum. The goal states the set through $\exists\beta\ge0,\ \delta^{TB}_S(\beta)=\theta\Pi^*$ and recovers the printed interval when the minimum is attained.

Weaker readings do not discharge the goal. Exhibiting one $\theta$ at which a form coordinates, showing that the printed terms are a Nash solution, or defining coordination as "some solution induces $r^*$ " all fall short: the goal fixes each $\Phi^m$ exactly and asserts the terms of every solution.

The development needs concavity of Laplace-type integrals in the scale parameter, differentiation under the integral sign, and existence and continuity of maximizers of strictly concave functions on $[0,\infty)$ . The Nash-bargaining-over-terms layer is reusable beyond this paper. Contributions are welcome on each contract form separately: the four Proposition 1 milestones share no argument beyond milestones 1–3.

Selected references

C. Hou, M. Lu, T. Deng, Z.-J. M. Shen, Coordinating Project Outsourcing through Bilateral Contract Negotiations, Manufacturing & Service Operations Management, 2020. Author manuscript: SSRN 3443865, https://ssrn.com/abstract=3443865; https://doi.org/10.1287/msom.2020.0911
M. Bayiz, C. J. Corbett, Coordination and incentive contracts in project management under asymmetric information, working paper, 2005. https://ssrn.com/abstract=914227
H. D. Kwon, S. A. Lippman, C. S. Tang, Optimal time-based and cost-based coordinated project contracts with unobservable work rates, International Journal of Production Economics 126(2):247–254, 2010.
T. Chen, T. Klastorin, M. R. Wagner, Incentive contracts in serial stochastic projects, Manufacturing & Service Operations Management 17(3):290–301, 2015.
S. A. Lippman, K. F. McCardle, C. S. Tang, Using Nash bargaining to design project management contracts under cost uncertainty, International Journal of Production Economics 145(1):199–207, 2013.
H. Horn, A. Wolinsky, Bilateral monopolies and incentives for merger, RAND Journal of Economics 19(3):408–419, 1988. https://doi.org/10.2307/2555667
Q. Feng, L. X. Lu, The role of contract negotiation and industry structure in production outsourcing, Production and Operations Management 22(5):1299–1319, 2013.
J. F. Nash, The bargaining problem, Econometrica 18(2):155–162, 1950. https://doi.org/10.2307/1907266

10 thms2 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

If It Is Surely Better, Do It More? Implications for Preferences Under Ambiguity: Ambiguity Aversion Toward an Event Breaks Monotonicity in Optimal Mixtures for c-Linearly Biseparable PreferencesResearch Paper

Motivation

Many economic and managerial decisions are choices of a mixing weight: how much effort to put on one sale rather than another, how much wealth to put in a risky asset, how to split a portfolio between two contracts. A natural comparative-statics requirement is that if one of the two options is improved in every state of the world, the decision maker should put at least as much weight on it. Ghili and Klibanoff (Management Science 67(12), 2021) call this property monotonicity in optimal mixtures and ask which models of decision making under ambiguity satisfy it.

Subjective expected utility satisfies it. The models used to describe ambiguity-averse behavior, such as the maxmin expected utility model of Gilboa and Schmeidler (1989), Choquet expected utility of Schmeidler (1989) and α-MEU of Ghirardato, Maccheroni and Marinacci (2004), are widely applied in contracting, finance and operations. Whether they predict that "surely better" options receive more weight is a basic question for any such application. The paper's first main finding is that, for the c-linearly biseparable class of Ghirardato and Marinacci (2001), which contains all three, the answer is negative as soon as the decision maker is ambiguity averse toward a single event.

Setting

The setting is an Anscombe–Aumann framework. $S$ is a finite set of states; an event is a subset $E\subseteq S$ and $E^c$ is its complement. $X$ is the set of simple lotteries over prizes. An act is a map $f:S\to X$ , and acts are mixed statewise: $(\alpha f+(1-\alpha)g)(s)=\alpha f(s)+(1-\alpha)g(s)$ . For lotteries $x,y$ , the binary act $xEy$ gives $x$ on $E$ and $y$ off $E$ .

All preferences are in the MBA class of Cerreia-Vioglio et al. (2011): an act $f$ is evaluated by $V\big((u(f(s)))_{s\in S}\big)$ , where $u:X\to\mathbb R$ is a nonconstant affine utility and $V:u(X)^S\to\mathbb R$ is normalized, monotone and sup-norm continuous. Under this representation an act may be identified with its utility profile $u\circ f:S\to U$ , where $U=u(X)$ is a convex subset of $\mathbb R$ with at least two points.

A capacity is a set function $\rho:2^S\to\mathbb R$ with $\rho(\emptyset)=0$ , $\rho(S)=1$ and $\rho(E)\le\rho(F)$ whenever $E\subseteq F$ . A preference is c-linearly biseparable if there is a capacity $\rho$ such that

W(xEy)=u(x)\rho(E)+u(y)(1-\rho(E))

represents the preference over all binary acts $xEy$ with $x\succsim y$ , for all events $E$ . The number $\rho(E)+\rho(E^c)$ classifies the attitude toward bets on $E$ : below $1$ is ambiguity aversion, equal to $1$ is neutrality, above $1$ is ambiguity loving.

For acts $f,g$ , the set of optimal mixtures $\alpha^*_{f,g}$ is the set of all $\alpha\in[0,1]$ such that $\alpha f+(1-\alpha)g$ is optimal in $\{\beta f+(1-\beta)g:\beta\in[0,1]\}$ . For $A,B\subseteq\mathbb R$ , $A\le_s B$ in the set order if $a\in A$ , $b\in B$ imply $\min\{a,b\}\in A$ and $\max\{a,b\}\in B$ . Monotonicity in optimal mixtures restricted to a set of acts $\mathcal G$ requires $\alpha^*_{f,g}\le_s\alpha^*_{f',g}$ for all $f,f',g\in\mathcal G$ with $f'(s)\succsim f(s)$ in every state $s$ .

Formalization targets

Goal: Theorem 2

Fix any event $E$ and a c-linearly biseparable preference with capacity $\rho$ .

\rho(E)+\rho(E^c)<1\ \Longrightarrow\ \text{monotonicity in optimal mixtures fails on }\{E,E^c\}\text{-measurable acts},

\big(\max\{\rho(E),\rho(E^c)\}<1\ \text{or}\ \min\{\rho(E),\rho(E^c)\}=0\big)\ \text{and}\ \rho(E)+\rho(E^c)\ge1\ \Longrightarrow\ \text{it holds there}.

Milestones

§5, p. 7625: given state-by-state monotonicity, the independence axiom implies monotonicity in optimal mixtures.
Proof of Theorem 2, p. 7627: if $\rho(E)+\rho(E^c)<1$ , the preference over $\{E,E^c\}$ -measurable acts is represented by $\min\{\rho(E)a+(1-\rho(E))b,\ (1-\rho(E^c))a+\rho(E^c)b\}$ , with $a$ , $b$ the utilities on $E$ and $E^c$ .
Proof of Theorem 2, p. 7627: for $f=xEy$ , $g=wEz$ whose connecting segment has slope strictly between the two linear pieces, the unique optimal mixture is $\alpha^*=1/\big(1+(u(x)-u(y))/(u(z)-u(w))\big)$ .
Theorem 2, first direction.
Proof of Theorem 2, p. 7628: if $\rho(E)+\rho(E^c)\ge1$ , the same acts are represented by the maximum of the two linear functionals.
Theorem 2, converse direction.

Significance

The theorem gives a sharp dividing line inside a large and heavily used family of ambiguity models. Ambiguity aversion toward even one event is incompatible with monotonicity in optimal mixtures for MEU, Choquet EU and α-MEU. The immediate corollary in the paper (Proposition 1) is that an MEU preference satisfies the property on bets on $E$ exactly when all its priors agree on the probability of $E$ . In applications such as the paper's sales-agent model, this means that improving the compensation for one task in every state can lead an ambiguity-averse agent to reduce effort on it. The result also separates these models from the smooth ambiguity model, for which the paper proves a compatibility result (Theorems 3–4).

Theorem 2 is proved in the paper; it has not been machine-checked. The mission produces a Lean development of the Anscombe–Aumann setting in utility space, capacities, MBA and c-linearly biseparable preferences, optimal-mixture sets and the set order, together with a checked proof of both directions. This layer is reusable for Proposition 1 and for other results on comparative statics under ambiguity.

Difficulty

The obvious route through comparative statics does not apply. The Milgrom–Shannon monotonicity theorem needs a single-crossing or supermodularity property of the objective in $(\alpha,f)$ , and the c-linearly biseparable functional restricted to a segment is only piecewise linear, with a kink where utilities on $E$ and $E^c$ coincide. Exhibiting a violation requires solving the maximization of a minimum of two affine functions on $[0,1]$ exactly, and constructing acts whose slope falls strictly inside a window determined by $\rho(E)$ and $\rho(E^c)$ , inside an arbitrary convex utility range.

The converse is not the mirror image of the first direction: the functional is then convex along segments, optimal sets can be whole intervals, and indifferences among $f$ , $f'$ and $g$ are where the argument is delicate. Remark 2 of the paper gives a capacity with $\rho(E)=1$ , $\rho(E^c)=1/2$ for which the converse fails, so the condition cannot be dropped.

Formalization scope

Acts are represented by utility profiles v : S → ℝ with values in a set U : Set ℝ. U is assumed convex and to contain two distinct points, which is exactly the range of a nonconstant affine utility on simple lotteries. Mixtures are α • f + (1 - α) • g, and " $f'(s)\succsim f(s)$ for all $s$ " is ∀ s, f s ≤ f' s.
S is a Fintype. An empty S makes the capacity conditions unsatisfiable, as on the page.
MBA is encoded as normalization on constants ( $V(c,\dots,c)=c$ ), monotonicity and continuity on U^S. On a finite S the product topology is the sup-norm topology.
c-linear biseparability is used through its representation (7), as in the paper. It is encoded as an order equivalence between comparisons of V and of W over binary profiles of all events, together with a capacity. The Ghirardato–Marinacci axioms are not encoded.
Optimal mixtures range over the closed interval $[0,1]$ for both the candidate and the competitors. The set order is the published Supermodularity.Lattices.InducedSetOrder on ℝ.
In milestone 3 the slope window is stated cross-multiplied, because $\rho(E^c)=0$ is allowed.
The min-representation is stated as a representation; the paper's strict inequality between the two pieces fails only on the diagonal $u(h(E))=u(h(E^c))$ , where the pieces coincide.
Ruled out: monotonicity with $\subseteq$ , or with a comparison of single chosen optima, in place of the set order; optimal mixtures over an open interval; (7) stated only one way or only for the event $E$ ; the converse without its side condition; and a preference class that is empty. A sorry-free sanity file exhibits a c-linearly biseparable preference with $\rho(E)+\rho(E^c)<1$ , and the Remark 2 preference, which satisfies all hypotheses except the side condition and violates the conclusion.
Not in scope: Theorem 1 (sales agent), Proposition 1 (MEU), Theorems 3–5 (smooth ambiguity and general MBA bounds), Axiom 3 and the remarks.

Contributions welcome: proofs of the milestones, and reusable lemmas on maximizers of minima and maxima of affine functions on intervals.

Selected references

S. Ghili and P. Klibanoff, If It Is Surely Better, Do It More? Implications for Preferences Under Ambiguity, Management Science 67(12):7619–7636, 2021. https://doi.org/10.1287/mnsc.2020.3890
P. Ghirardato and M. Marinacci, Risk, Ambiguity, and the Separation of Utility and Beliefs, Mathematics of Operations Research 26(4):864–890, 2001. https://doi.org/10.1287/moor.26.4.864.10002
S. Cerreia-Vioglio, P. Ghirardato, F. Maccheroni, M. Marinacci and M. Siniscalchi, Rational Preferences Under Ambiguity, Economic Theory 48(2–3):341–375, 2011. https://doi.org/10.1007/s00199-011-0643-3
I. Gilboa and D. Schmeidler, Maxmin Expected Utility with Non-Unique Prior, Journal of Mathematical Economics 18(2):141–153, 1989. https://doi.org/10.1016/0304-4068(89)90018-9
D. Schmeidler, Subjective Probability and Expected Utility without Additivity, Econometrica 57(3):571–587, 1989. https://doi.org/10.2307/1911053
P. Ghirardato, F. Maccheroni and M. Marinacci, Differentiating Ambiguity and Ambiguity Attitude, Journal of Economic Theory 118(2):133–173, 2004. https://doi.org/10.1016/j.jet.2003.12.004
P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1):157–180, 1994. https://doi.org/10.2307/2951479
F. J. Anscombe and R. J. Aumann, A Definition of Subjective Probability, Annals of Mathematical Statistics 34(1):199–205, 1963. https://doi.org/10.1214/aoms/1177704255

9 thms2 active usersReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Sufficiency of Markov Policies for Continuous-Time Jump Markov Decision Processes: The Induced Markov Policy Has State-Action Marginals No Larger than the Policy, Equal When NonexplosiveResearch Paper

Markov policies in continuous-time decision processes

In a Markov decision process a controller chooses actions over time to influence a random system. A basic question for every such model is whether the controller loses anything by ignoring the past: whether, for every policy that uses the full history, some Markov policy (one that looks only at the current state and time) performs equally well. For discrete-time models the answer goes back to Derman and Strauch (1966): the Markov policy that randomizes according to the conditional distribution of the action given the current state has the same state-action marginals as the original policy, and therefore the same expected costs for any criterion that depends on these marginals.

In continuous-time jump Markov decision processes (CTJMDPs) with unbounded transition rates the question is harder, because the process may explode: infinitely many jumps can accumulate in finite time, after which the process leaves the state space. Earlier sufficiency results assumed bounded rates or nonexplosive processes (Kitaev 1985; Kitaev and Rykov 1995; Guo and Song 2011; Piunovskiy and Zhang 2014). Feinberg, Mandava and Shiryaev (arXiv:2003.01342) proved the continuous-time analogue of Derman and Strauch's result with no such assumption: the induced Markov policy has state-action marginals no larger than those of the original policy, and equal ones as long as it does not explode.

Setting

A CTJMDP is given by a state space $X$ and an action space $A$ , both standard Borel spaces; nonempty sets $A(x)\subseteq A$ of actions available at each state $x$ , whose graph $\mathrm{Gr}(A)$ is measurable and contains the graph of a measurable selector; and transition rates $\tilde q(x,a,\cdot)$ , where $Z\mapsto\tilde q(x,a,Z\setminus\{x\})$ is a finite measure, measurable in $(x,a)$ . The jump intensity is $\tilde q(x,a)=\tilde q(x,a,X\setminus\{x\})$ , and Assumption 2.1 requires $\bar q(x)=\sup_{a\in A(x)}\tilde q(x,a)<\infty$ for every $x$ . A probability measure $p$ on $A$ acts through $\tilde q(x,p)=\int\tilde q(x,a)\,p(da)$ and $\tilde q(x,p,Z)=\int\tilde q(x,a,Z)\,p(da)$ .

A trajectory is $\omega=(x_0,t_1,x_1,t_2,x_2,\dots)$ , with jump epochs $0=t_0<t_1<t_2<\cdots\le\infty$ and post-jump states $x_n$ ; the process is $\xi_t=x_n$ for $t_n\le t<t_{n+1}$ and leaves $X$ at $t_\infty=\lim_nt_n$ . A policy $\pi$ chooses, between the $n$ th and $(n+1)$ st jump, the action distribution $\pi_n(\cdot\mid x_0,t_1,\dots,t_n,x_n,t-t_n)$ , concentrated on $A(x_n)$ . A Markov policy is a transition probability $\phi(\cdot\mid z,t)$ from $X\times(0,\infty)$ to $A$ with $\phi(A(z)\mid z,t)=1$ . An initial distribution $\gamma$ and a policy $\pi$ define the law $\mathbb P^\pi_\gamma$ of the process: from $x_n$ the next jump occurs at hazard rate $\tilde q(x_n,\pi_s)$ and lands in $dy$ with intensity $\tilde q(x_n,\pi_s,dy\setminus\{x_n\})$ .

The state marginal and the state-action marginal are

P^\pi_\gamma(t,Z)=\mathbb P^\pi_\gamma(\xi_t\in Z),\qquad P^\pi_\gamma(t,Z,B)=\mathbb E^\pi_\gamma\big[I\{\xi_{t-}\in Z\}\,\pi(B\mid\omega,t)\big],

for $t>0$ , $Z\subseteq X$ , $B\subseteq A$ . A Markov policy $\phi$ satisfies (16) for $(\gamma,\pi)$ if

P^\pi_\gamma(t,Z,B)=\int_Z\phi(B\mid z,t)\,P^\pi_\gamma(t,dz)\qquad\text{for all }t>0,\ Z,\ B,

that is, $\phi(\cdot\mid z,t)$ is the conditional distribution of the action given $\xi_{t-}=z$ under $\pi$ . The process under $\phi$ is nonexplosive when $P^\phi_\gamma(t,X)=1$ for all $t>0$ .

Formalization targets

Goal: Theorem 1

If $\phi$ is a Markov policy satisfying (16) for $(\gamma,\pi)$ , then

P^\phi_\gamma(t,Z,B)\le P^\pi_\gamma(t,Z,B)\qquad\text{for all }t>0,\ Z,\ B,

with equality for $t\in\,]0,s]$ whenever $P^\phi_\gamma(s,X)=1$ , and equality for all $t>0$ when the process under $\phi$ is nonexplosive.

Milestones

The milestones follow the paper's proof: existence and uniqueness of $\mathbb P^\pi_\gamma$ (§2); the compensator identities (8) and Lemma 3; the forward identity (37) for $(x,\pi)$ -bounded sets (Lemma 4); Feller's minimal solution of Kolmogorov's forward equation (Theorem 3), its identification with the marginal of a Markov policy ((31), Corollary 5); the occupation identities (49)–(50); the state-marginal comparison (Lemma 2) and Theorem 1 for one initial state (Lemma 5); the characterization (19) of (16) (Corollary 1); the scaling identity (58)–(59) and the claim (19) for the extended model (p. 16); and the existence of $\phi$ (Lemma 1).

Significance

Theorem 1 with Lemma 1 shows that Markov policies are sufficient in CTJMDPs with unbounded rates. Every cost criterion that is a monotone functional of state-action marginals with nonnegative costs (expected total discounted costs, finite-horizon costs, average costs per unit time, and the corresponding constrained problems) is no larger under the Markov policy, which is the content of §6 of the paper. Equality holds whenever the Markov policy does not explode, for example when the rates are bounded (Corollary 2), and two Markov policies satisfying (16) have the same law (Corollary 3). The intermediate results, in particular Lemma 4 (the forward identity for possibly explosive processes) and Feller's minimal-solution theorem, are tools in their own right for continuous-time Markov chains on general state spaces.

The result is proved in the paper; nothing here is open mathematically. No part of it is formalized: Mathlib has no jump processes, compensators of point processes, Kolmogorov forward equations on general state spaces, or Feller's construction of minimal transition functions. The mission produces a machine-checked account of these foundations and of the sufficiency theorem built on them, with every measure-theoretic step (the law of the process, the disintegration, the minimality argument) made explicit.

Difficulty

The direct argument for discrete time compares the two marginals step by step through the one-step transition law. In continuous time there is no first step, and the natural replacement, comparing the forward equations satisfied by the two marginals, breaks down twice. First, with unbounded rates the integrals in the forward equation (37) can be infinite, so the equation is not even well defined for all sets, and the standard derivations assume nonexplosiveness. Second, forward equations need not have unique solutions when the process can explode, so showing that both marginals solve the same equation does not make them equal. The paper handles the first point with the class of $(x,\pi)$ -bounded sets and the second with Feller's minimal solution, which yields only an inequality in general; equality needs the probability-one condition. Passing from an initial state to an initial distribution is a further step: the forward equation is stated for a point initial condition, and the reduction goes through an extended model with an added state.

Formalization scope

All quantities take values in $[0,\infty]$ . Rates are given by off-diagonal finite jump measures, with $\tilde q:=0$ off $\mathrm{Gr}(A)$ . A trajectory is an element of X × (ℕ → ℝ≥0∞ × X); the cemetery point is not a separate state, and $x_n$ is ignored once $t_n=\infty$ . A policy is a family $\pi_n(\cdot\mid\omega,s)$ that depends only on the history up to the $n$ th jump. Marginals read the process at $\xi_{t-}$ , which equals $\xi_t$ almost surely at each fixed $t$ .

The law $\mathbb P^\pi_\gamma$ is a hypothesis of each statement: any probability measure on trajectories with initial law $\gamma$ whose one-step conditional laws are the explicit sojourn/jump kernel (the Ionescu-Tulcea construction (75)–(76) of the paper) is admitted, and a milestone states that exactly one such measure exists. The paper characterizes the same measure through Jacod's compensator theorem. The compensator properties (8) and Lemma 3 are stated as (8) for every stopping time of the natural filtration $\sigma(\xi_s: 0\le s\le t)$ . Kolmogorov's forward equations are written additively, with the subtracted integral finite, which is equivalent to the real equation. In the extended model of the proof the added state and actions are Sum.inr points of X ⊕ Unit and A ⊕ Bool; the policy (55) is evaluated on the observed part of the path and chooses the absorbing action off the set $\Omega'(u)$ , which is a null set.

A formalization in which the law is never shown to exist, or in which (16) cannot be satisfied, would make Theorem 1 vacuous; the existence-and-uniqueness milestone and Lemma 1 rule this out.

A complete development needs the Ionescu-Tulcea construction of the law, compensators of multivariate point processes, the forward equation and Feller's series on a standard Borel space, and disintegration of measures. The first three are reusable for any continuous-time Markov chain or CTJMDP on a general state space, and contributions to them are welcome on their own.

Selected references

E. A. Feinberg, M. Mandava, A. N. Shiryaev, Sufficiency of Markov policies for continuous-time jump Markov decision processes, Mathematics of Operations Research, 2022; arXiv:2003.01342v3. https://arxiv.org/abs/2003.01342
E. A. Feinberg, M. Mandava, A. N. Shiryaev, Kolmogorov's equations for jump Markov processes with unbounded jump rates, Annals of Operations Research, 2017. https://doi.org/10.1007/s10479-017-2538-8
E. A. Feinberg, M. Mandava, A. N. Shiryaev, On solutions of Kolmogorov's equations for nonhomogeneous jump Markov processes, Journal of Mathematical Analysis and Applications 411(1):261–270, 2014.
J. Jacod, Multivariate point processes: predictable projection, Radon–Nikodym derivatives, representation of martingales, Probability Theory and Related Fields 31:235–253, 1975.
M. Kitaev, V. Rykov, Controlled Queueing Systems, CRC Press, 1995.
X. Guo, X. Song, Discounted continuous-time constrained Markov decision processes in Polish spaces, Annals of Applied Probability 21(5):2016–2049, 2011.
A. Piunovskiy, Y. Zhang, Discounted continuous-time Markov decision processes with unbounded rates and randomized history-dependent policies: the dynamic programming approach, 4OR 12:49–75, 2014.
C. Derman, R. Strauch, A note on memoryless rules for controlling sequential control processes, Annals of Mathematical Statistics 37:276–278, 1966.
W. Feller, On the integro-differential equations of purely-discontinuous Markoff processes, Transactions of the AMS 48:488–515, 1940.

17 thms2 active usersReviewed

Completed

Machine Learning Operations Research Optimization·Captain: mikedeng1

A Single-Loop Algorithm for Decentralized Bilevel Optimization: O(1/K) Stationarity and Consensus Rates of SLDBO without Heterogeneity AssumptionsResearch Paper

Bilevel problems on a network

Bilevel optimization chooses an upper-level variable $x$ to minimize an objective that depends on the solution $y^*(x)$ of a lower-level problem. Hyperparameter tuning and meta-learning are the standard examples (Franceschi et al. 2018; Ghadimi and Wang 2018). In the decentralized version the data are split among $n$ agents. Each agent sees only its own upper- and lower-level functions $F_i$ and $f_i$ , and it can talk only to its neighbours in a communication network. The paper's example is $n$ hospitals tuning a regularization weight of a logistic-regression model. No hospital may share its patients' data, but the hyperparameter has to be good for the pooled data.

Decentralized bilevel algorithms before this paper converged only under a heterogeneity assumption, a bound on how much the agents' functions may differ. DSBO (Chen, Huang and Ma 2024) assumes i.i.d. local data, MA-DSBO (Chen et al. 2023) a uniform bound on $\|\nabla_2 f_i - \nabla_2 f\|$ , and SLAM (Lu et al. 2022) Lipschitz-type closeness of the local Hessians. Such assumptions fail exactly when the agents' data differ, which is the case that motivates decentralization in the first place. Dong, Ma, Yang and Yin propose SLDBO, a single-loop method that needs no such assumption, and prove an $O(1/K)$ rate for it.

Setting

There are $n\ge1$ agents. Agent $i$ holds $F_i,f_i:\mathbb R^p\times\mathbb R^q\to\mathbb R$ . Write $F=\frac1n\sum_iF_i$ and $f=\frac1n\sum_if_i$ . Problem (6) is

\min_{x\in\mathbb R^p}\ \Phi(x)=F(x,y^*(x)),\qquad y^*(x)=\arg\min_{y\in\mathbb R^q}f(x,y).

Assumption 2.1 gives constants $\sigma>0$ and $L_{F,0},L_{F,1},L_{f,1},L_{f,2}\ge0$ . Each $f_i(x,\cdot)$ is $\sigma$ -strongly convex. $F_i$ is $L_{F,0}$ -Lipschitz with an $L_{F,1}$ -Lipschitz gradient. $f_i$ is twice differentiable with an $L_{f,1}$ -Lipschitz gradient and an $L_{f,2}$ -Lipschitz Hessian. Under these conditions $y^*$ is well defined and $\Phi$ is differentiable, with the hypergradient (7)

\nabla\Phi(x)=\nabla_1F(x,y^*(x))-\nabla^2_{12}f(x,y^*(x))\,v^*(x),\qquad v^*(x)=\big[\nabla^2_{22}f(x,y^*(x))\big]^{-1}\nabla_2F(x,y^*(x)).

Here $\nabla_1,\nabla_2$ are the partial gradients, $\nabla^2_{22}f$ is the Hessian of $f$ in $y$ , and $\nabla^2_{12}f$ is the Jacobian of $\nabla_1f$ in $y$ .

Assumption 2.2. The agents communicate through a nonnegative, symmetric, doubly stochastic mixing matrix $W=(w_{ij})$ , and $\rho<1$ bounds the contraction of $W$ away from consensus.

SLDBO (Algorithm 1) keeps three local iterates $x^k_i,y^k_i,v^k_i$ per agent. Agent $i$ computes the local directions $d^k_{y,i}=\nabla_2f_i$ , $d^k_{v,i}=\nabla_2F_i-\nabla^2_{22}f_i\,v^k_i$ and $d^k_{x,i}=\nabla_1F_i-\nabla^2_{12}f_i\,v^k_i$ at $(x^k_i,y^k_i)$ . It feeds them into gradient-tracking variables $t^k_{\cdot,i}=\sum_jw_{ij}t^{k-1}_{\cdot,j}+d^k_{\cdot,i}-d^{k-1}_{\cdot,i}$ , which estimate the network averages of the directions. It then takes one mixed step on each iterate with constant step sizes $\beta,\eta,\alpha$ . The step on $v$ is followed by the projection $\mathcal P_{r_v}$ onto the ball of radius $r_v=L_{F,0}/\sigma$ , which contains every $v^*(x)$ . All agents start from common points with $t^{-1}=d^{-1}=0$ (BOX 1). Bars denote averages over agents, e.g. $\bar x^k=\frac1n\sum_ix^k_i$ .

Formalization targets

Goal: Theorem 3.1

The step sizes have thresholds depending only on $(\sigma,L_{F,0},L_{F,1},L_{f,1},L_{f,2},\rho)$ : first $\bar\beta$ , then $\bar\eta$ given $\beta$ , then $\bar\alpha$ given $\beta,\eta$ . Below these thresholds, every instance with $\Phi$ bounded below has a constant $C$ such that for all $K\ge1$

\min_{0\le k\le K-1}\|\nabla\Phi(\bar x^k)\|^2\le\frac CK,\qquad \min_{0\le k\le K-1}\frac1n\sum_{i=1}^n\|z^k_i-\bar z^k\|^2\le\frac CK\quad(z\in\{x,y,v\}).

The goal fixes no explicit step sizes and no explicit constant $C$ ; it asserts the rate.

Milestones

These are the paper's own statements, in attack order:

the hypergradient formula (7);
the mixing and projection lemmas A.1–A.2;
the tracking identity (25);
the consensus recursions A.3–A.4 with Remarks A.1–A.2;
the bounds A.5–A.7 with Remark A.3 (A.5 and A.7 are included as supporting statements rather than milestones);
the Lipschitz continuity of $y^*$ and $v^*$ (A.11) and of $\nabla\Phi$ ;
the descent inequality for $\Phi$ (A.8);
the contractions of $\|\bar y^k-y^*(\bar x^k)\|$ and $\|\bar v^k-v^*(\bar x^k)\|$ (A.9–A.10).

Significance

The theorem shows that a single-loop decentralized method reaches the $O(1/K)$ stationarity rate known for centralized single-loop bilevel methods (Ji et al. 2022; Dagréou et al. 2022). Each iteration needs $\Theta(1)$ communication rounds and one Hessian- and one Jacobian-vector product, with no heterogeneity bound. The consensus clauses add that the agents agree at the same rate.

The result is proved in the paper; nothing about it is formalized. The mission adds three things. First, a machine-checked statement with explicit conventions. Second, a check of the constants. The printed $L_\Phi$ in (8) has a term that is not homogeneous in the scale of $F$ , and the explicit step-size bounds (62) do not make the Lyapunov coefficient $A_2$ nonnegative (checked numerically). The goal is therefore stated in a form the argument supports. Third, reusable lemmas for gradient-tracking analyses: the mixing-matrix contraction, the projected-consensus inequality, the tracking identity and the hypergradient formula.

Difficulty

The obvious analysis of a decentralized SOBA-type method bounds the change of the directions $d^k_{x,i}$ and $d^k_{v,i}$ between iterations by the change of the iterates. Those directions contain $\nabla^2f_i\,v^k_i$ . Without control of $\|v^k_i\|$ , their variation is bounded only by assuming the local Hessians are close, which is the heterogeneity assumption. The projection removes the need for it. The price is that $\bar v^k$ no longer follows the averaged direction, so the consensus and error recursions for $v$ have to be derived separately. All of these recursions are then combined into one Lyapunov function (15) whose coefficients must be balanced against three coupled step sizes. Most of the work, and the published constants' main failure, is in that balancing.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d). Lipschitz conditions in $(x,y)$ use $\sqrt{\|x-x'\|^2+\|y-y'\|^2}$ , never Lean's sup norm on a product. The model and the added hypotheses:

Hessian condition. It is imposed on the two blocks $\nabla^2_{12}f_i$ and $\nabla^2_{22}f_i$ in the operator norm. This is weaker than the paper's Frobenius-Lipschitz full Hessian.
Mixing rate. $\rho$ is any bound of $W$ on $\mathbf 1^\perp$ ; the paper's eigenvalue $\rho$ is the least one.
Lower-level solution. $y^*$ is a given map with $y^*(x)$ minimizing $f(x,\cdot)$ for every $x$ .
Hypergradient. $v^*$ is defined through ContinuousLinearMap.inverse, and $\nabla\Phi$ is the formula (7). A milestone proves that (7) is the gradient of $\Phi$ .
Algorithm. Algorithm 1 with BOX 1 is one deterministic function run. Its state at index $k$ holds $(x^k,y^k,v^k,t^{k-1},d^{k-1})$ .
Rate. " $O(1/K)$ " is one constant $C$ , fixed after the instance and before $K$ ; the minimum over $0\le k\le K-1$ is an existential $k<K$ .
$\Phi$ bounded below. This is added to the goal. Without it the claim fails: $F_i(x,y)=-x$ and $f_i(x,y)=y^2/2$ satisfy Assumption 2.1, yet $\nabla\Phi\equiv-1$ .
Lemma A.5 is posed for $k\ge1$ . At $k=0$ it would claim $d^0=0$ .
Lemmas A.9 and A.10 carry the two bounds of (62) their proofs use, $\beta L_{f,1}<1$ and $\eta L_{f,1}<1$ .
$L_\Phi$ is $(L_{F,1}+L_{f,2}r_v)(1+L_{f,1}/\sigma)^2$ , which is (8) with $L_{F,0}^2$ corrected to $L_{F,0}$ .
Step sizes. The goal is stated with nested thresholds instead of (62).

The goal would become trivial if the thresholds were chosen after the instance or $C$ after $K$ , and false without $\Phi$ bounded below; the statement rules both out. All hypotheses are satisfiable: a two-agent instance with $\rho=0$ and $f_i=\|y\|^2/2$ is checked in Lean.

A complete development needs the implicit-function theorem for $y^*$ , the descent lemma, strong-convexity inequalities for gradient steps, and the gradient-tracking bookkeeping. The mixing-matrix and tracking lemmas are reusable for other gradient-tracking methods. Proofs of any milestone, and repaired explicit step-size conditions, are welcome.

Selected references

Y. Dong, S. Ma, J. Yang, C. Yin, A Single-Loop Algorithm for Decentralized Bilevel Optimization, Mathematics of Operations Research, 2025; arXiv:2311.08945v3. https://arxiv.org/abs/2311.08945
M. Dagréou, P. Ablin, S. Vaiter, T. Moreau, A framework for bilevel optimization that enables stochastic and global variance reduction algorithms, NeurIPS 35, 2022. https://arxiv.org/abs/2201.13409
S. Ghadimi, M. Wang, Approximation methods for bilevel programming, arXiv:1802.02246, 2018. https://arxiv.org/abs/1802.02246
X. Chen, M. Huang, S. Ma, Decentralized bilevel optimization, Optimization Letters, 2024. https://arxiv.org/abs/2206.05670
X. Chen, M. Huang, S. Ma, K. Balasubramanian, Decentralized stochastic bilevel optimization with improved per-iteration complexity, ICML 2023. https://arxiv.org/abs/2210.12839
S. Lu, S. Zeng, X. Cui, M. Squillante, L. Horesh, B. Kingsbury, J. Liu, M. Hong, A stochastic linearized augmented Lagrangian method for decentralized bilevel optimization, NeurIPS 35, 2022. https://proceedings.neurips.cc/paper_files/paper/2022 (pp. 30638–30650)
K. Ji, M. Liu, Y. Liang, L. Ying, Will bilevel optimizers benefit from loops, NeurIPS 35, 2022. https://arxiv.org/abs/2205.14224
S. Pu, A. Nedić, Distributed stochastic gradient tracking methods, Mathematical Programming 187, 409–457, 2021. https://arxiv.org/abs/1805.11454
L. Franceschi, P. Frasconi, S. Salzo, R. Grazzi, M. Pontil, Bilevel programming for hyperparameter optimization and meta-learning, ICML 2018. https://arxiv.org/abs/1806.04910

17 thms2 active usersReviewed

Completed

Operations Research Probability Reinforcement Learning·Captain: mikedeng1

Relaxed Equilibria for Time-Inconsistent Markov Decision Processes: A Relaxed Equilibrium Exists in Discrete Time without Convexity, via Vanishing Entropy RegularizationResearch Paper

Time inconsistency and equilibrium controls

An agent who maximizes an expected sum of rewards over time is time-inconsistent when the plan that is optimal today stops being optimal tomorrow. This happens as soon as discounting is not exponential: with hyperbolic or quasi-hyperbolic discounting, a reward far in the future is weighed differently at time 0 and at time 1, and the agent's future selves want to revise today's plan. Strotz (Strotz 1955) proposed to treat the problem as a game between the current self and all future selves and to look for a strategy that no self wants to deviate from: an equilibrium. Non-exponential discounting is documented in experimental economics (Laibson 1997), and equilibrium controls are the standard solution concept for such problems in mathematical finance and stochastic control (Björk, Khapko, Murgoci 2017).

The basic question is whether an equilibrium exists. For a Markov decision process on a finite state space with a general action set, Huang and Zhou proved existence when the actions available in each state form a closed convex set and the reward is concave in the action. Without convexity there need not be an equilibrium among deterministic feedback controls. Bayraktar, Huang, Wang and Zhou show that existence is restored for relaxed (randomized) controls, under only Lipschitz continuity and a geometric condition on the action space. This mission formalizes their discrete-time result.

Setting

The action space is a compact set $U\subset\mathbb R^\ell$ with positive Lebesgue measure $\mathrm{Leb}(U)>0$ , and the state space is $\mathcal S=\{1,\dots,d\}$ . Each action $u\in U$ has a transition matrix $p^u=(p^u_{ij})$ , with $i$ -th row $p^u_i$ . A reward function $f(t,i,u)$ depends on the time difference $t\in\mathbb N_0$ , the state and the action.

A relaxed feedback control is a map $\pi:\mathcal S\to\mathcal P(U)$ : in state $i$ the agent samples an action from the probability measure $\pi(i)$ . The set of relaxed controls is $\Pi$ . The chain then moves with the averaged matrix $p^\pi_{ij}=\int_U p^u_{ij}\,(\pi(i))(du)$ , and the value is

J^\pi(i)=\mathbb E_i\Big[\sum_{k\ge0}f^{\pi(X_k)}(k,X_k)\Big],\qquad f^\mu(t,i)=\int_U f(t,i,u)\,\mu(du).

For $\pi,\pi'\in\Pi$ , the concatenation $\pi'\otimes_1\pi$ uses $\pi'$ at time $0$ and $\pi$ afterwards. A control $\pi\in\Pi$ is a relaxed equilibrium if

J^{\pi'\otimes_1\pi}(i)-J^\pi(i)\le0\qquad\text{for all } i\in\mathcal S,\ \pi'\in\Pi .

The paper also uses an entropy-regularized problem. A control is regular ( $\pi\in\Pi_r$ ) if each $\pi(i)$ has a density $\rho_i$ on $U$ whose differential entropy $\mathcal H(\rho_i)=-\int_U\rho_i\ln\rho_i\,du$ is finite. For $\lambda>0$ and a discount function $\delta$ , the regularized value $J^\pi_\lambda$ adds $\lambda\delta(k)\mathcal H(\pi(X_k))$ to the reward at time $k$ . A regular control is a regular relaxed equilibrium if no regular deviation $\pi'$ improves $J_\lambda$ . The Gibbs density

\Gamma_\lambda(y,i)(u)=\frac{e^{\frac1\lambda(f(0,i,u)+p^u_i\cdot y)}}{\int_U e^{\frac1\lambda(f(0,i,v)+p^v_i\cdot y)}\,dv},\qquad y\in\mathbb R^d,

defines the map $\Psi_\lambda(y)=V_\lambda^{\Gamma_\lambda(y,\cdot)}$ , where $V_\lambda$ is the continuation value from time $1$ .

The assumptions are the following.

Assumption 2.1: $\sum_t\big(\sup_{i,u}|f(t,i,u)|+\delta(t)\big)<\infty$ .
Assumption 2.2: $u\mapsto f(t,i,u)$ and $u\mapsto p^u_i$ are Lipschitz, uniformly in $(t,i)$ , with constant $\Theta$ .
Assumption 2.3: a uniform cone condition. Some cone of fixed angle $\iota$ and fixed height $\vartheta$ with vertex at any point of $U$ lies in $U$ . Polyhedra and ellipsoids satisfy it.

Formalization targets

Goal: Theorem 2.2

Under Assumptions 2.1–2.3, there exists $\pi\in\Pi$ with

J^{\pi'\otimes_1\pi}(i)\le J^\pi(i)\qquad\forall i\in\mathcal S,\ \forall\pi'\in\Pi.

The statement fixes no constants and assumes no convexity.

Regularized problem (milestones, in attack order)

The one-step decomposition $J^{\pi'\otimes_1\pi}_\lambda(i)=f^{\pi'(i)}(0,i)+\lambda\mathcal H(\pi'(i))+\mathbb E_i[V^\pi_\lambda(X^{\pi'}_1)]$ (p. 6).
$\Gamma_\lambda(y,i)$ is the unique maximizer of the one-step objective (2.11)–(2.12).
Proposition 2.1 and Corollary 2.1: regular relaxed equilibria correspond to fixed points $\Phi_\lambda(\pi)=\pi$ , and their values to fixed points $\Psi_\lambda(y)=y$ .
Lemma 2.1: $\sup_i|\mathcal H(\Gamma_\lambda(y,i))|\le\kappa+\ell\ln(1+|y|)$ (2.17), and $\le\kappa_1+\kappa_2|\ln\lambda|+\ell\ln(1+|y|)$ for small $\lambda$ (2.18).
Continuity of $\Psi_\lambda$ , then Theorem 2.1: for every $\lambda>0$ , $\Psi_\lambda$ has a fixed point, which gives a regular relaxed equilibrium.

Vanishing regularization

Lemma 2.2: fixed points $y^n=\Psi_{\lambda_n}(y^n)$ stay bounded as $\lambda_n\downarrow0$ .
Proposition 2.2: $\pi$ is a relaxed equilibrium iff $\pi\in\Phi(\pi)=\Gamma(V^\pi)$ , where $\Gamma(y)$ collects the controls carried by $\arg\max_u\{f(0,i,u)+p^u_i\cdot y\}$ .
Two steps of the limit argument (pp. 22–23). Weak limits of Gibbs controls lie in $\Gamma(y^\infty)$ , and their regularized values converge, $V^{\Gamma_{\lambda_n}(y^n,\cdot)}_{\lambda_n}\to V^{\pi^*}$ (A.12)–(A.13).

Significance

The result. Theorem 2.2 removes the convexity and concavity assumptions of the earlier existence theorem for discrete-time time-inconsistent MDPs. Its price is randomization. The action space may be a finite union of polytopes, for example, and the reward need not be concave in the action. Theorem 2.1 is of independent interest for reinforcement learning, where entropy-regularized objectives are the standard way to encourage exploration (Ziebart et al. 2008). With non-exponential discounting, the theorem guarantees a randomized policy that all future selves uphold. The regularized equilibria are fixed points of a single-valued map, and the paper (Remark 2.6) points to them as a computational route to relaxed equilibria.

The formalization. The results are proved in the paper. None of them has a machine-checked proof, and this mission produces the first. Along the way it requires a formal treatment of relaxed controls as measure-valued maps, of the differential entropy of densities on a subset of $\mathbb R^\ell$ , and of Gibbs variational principles for such densities.

Difficulty

The obvious route to existence is a fixed-point theorem for the best-response correspondence on deterministic controls. It needs convex values, hence a convex action set and a concave reward, and both are absent here. Relaxing to measures restores convexity of each best-response set. However, the unregularized best response $\pi\mapsto\Gamma(V^\pi)$ is set-valued on an infinite-dimensional space, and the value $V^\pi$ depends nonlinearly on $\pi$ through the whole future of the chain. The regularized problem has a single-valued best response, but a fixed point needs a uniform bound on entropies of Gibbs densities. That bound must grow only logarithmically in $|y|$ (otherwise no ball is invariant) and stay controlled as $\lambda\to0$ . The geometric Assumption 2.3 enters exactly there, and again in the limit, where Gibbs measures must concentrate on maximizers that a cusp or isolated point of $U$ would otherwise hide.

Formalization scope

Actions are points of EuclideanSpace ℝ (Fin ℓ) with $\ell>0$ . The state space is Fin d, value vectors are Fin d → ℝ, and every norm $|y|$ on $\mathbb R^d$ (and $|p^{u_1}_i-p^{u_2}_i|$ ) is Euclidean. A control is a family of measures on $\mathbb R^\ell$ :

relaxed means probability measures carried by $U$ ;
regular adds absolute continuity with respect to Lebesgue measure on $U$ and integrability of $\rho\ln\rho$ for the Radon–Nikodym density $\rho$ .

Expected values are infinite sums through products of the averaged transition matrices (Remark 2.1), and the concatenation $\pi'\otimes_1\pi$ is the control sequence $(\pi',\pi,\pi,\dots)$ . The p. 6 decomposition is therefore a theorem, not a definition. Weak convergence is tested against bounded continuous functions on $\mathbb R^\ell$ . Constants that the paper says depend on $(\ell,\lambda,\mathrm{Leb}(U),\iota,\vartheta,\Theta)$ are quantified before $d$ , $U$ , $f$ , $p$ and $y$ .

Disclosed conventions:

each $p^u$ is a stochastic matrix;
$\Theta>0$ ;
the cone of Assumption 2.3 has one nappe and the ball is open (weaker than the printed double cone, which no polyhedron vertex satisfies);
measurability of $f$ and $p$ is assumed where only Assumption 2.1 is cited;
$\operatorname{supp}\pi(i)\subseteq E$ is written $\pi(i)(E^c)=0$ .

A trivializing formalization is ruled out. Equilibria quantify over all relaxed deviations, Dirac controls included. $J^{\pi'\otimes_1\pi}$ is computed from the process, not from the one-step formula. The hypotheses of the goal are satisfiable: a verified instance with $\ell=d=1$ and $U=[-1,1]$ exists in the development.

Needed infrastructure, reusable beyond this mission:

entropy and Gibbs principles for densities on subsets of $\mathbb R^\ell$ ;
lower bounds on Lebesgue measure of cone sections;
weak convergence on compact metric spaces;
Brouwer's fixed-point theorem.

Proofs of any milestone and of reusable lemmas are welcome.

Selected references

E. Bayraktar, Y.-J. Huang, Z. Wang, Z. Zhou, Relaxed Equilibria for Time-Inconsistent Markov Decision Processes, Mathematics of Operations Research, 2025; arXiv:2307.04227v2. https://arxiv.org/abs/2307.04227
Y.-J. Huang, Z. Zhou, Strong and weak equilibria for time-inconsistent stochastic control in continuous time, Mathematics of Operations Research 46(2), 2021. https://arxiv.org/abs/1809.09243
R. H. Strotz, Myopia and inconsistency in dynamic utility maximization, Review of Economic Studies 23(3), 1955. https://doi.org/10.2307/2295722
D. Laibson, Golden eggs and hyperbolic discounting, Quarterly Journal of Economics 112(2), 1997. https://doi.org/10.1162/003355397555253
T. Björk, M. Khapko, A. Murgoci, On time-inconsistent stochastic control in continuous time, Finance and Stochastics 21(2), 2017. https://doi.org/10.1007/s00780-017-0327-5
B. D. Ziebart, A. Maas, J. A. Bagnell, A. K. Dey, Maximum entropy inverse reinforcement learning, AAAI 2008. https://cdn.aaai.org/AAAI/2008/AAAI08-227.pdf

15 thms2 active usersReviewed

Completed

Mechanism Design Operations Research Probability·Captain: mikedeng1

Optimal Subscription Planning for Digital Goods: Under Condition 2, a Single Grand Subscription Set With a Suitable Fee Achieves the Optimal RevenueResearch Paper

Motivation

Digital-goods platforms (video, music, e-books, software) sell access in two ways at once: subscriptions, which give unlimited use of a set of items for a period, and rentals, which charge per use. A platform with a large catalogue could offer many subscription sets at different fees, but most platforms offer a single all-inclusive subscription. Alaei, Makhdoumi and Malekian (Optimal Subscription Planning for Digital Goods, Operations Research 2023; working paper SSRN 3476296) ask when that practice is revenue-optimal. Users differ not only in how they value items but in how often they consume (their usage rate), and it is this second dimension that makes the question nontrivial: a frequent user values unlimited access more, even with the same per-use tastes.

The paper's first main result, Theorem 2, gives a condition on the value distributions under which a single grand subscription (all items, one fee), together with the rental prices, earns as much as any menu of subscription sets, whatever the masses and usage rates of the user types.

Setting

There are $n$ user types $i \in \mathcal N$ and $m$ item types $j \in \mathcal M$ . On a probability space, $V_{ij}$ is the value of one watch of item $j$ to a user of type $i$ and $V_0$ is the value of an outside option. Type $i$ has mass $q_i \ge 0$ with $\sum_i q_i = 1$ , and watches at usage rate $\lambda_i > 0$ over a period of length $T > 0$ .

A subscription planning (Definition 1) is a pair $(p, \mathbf r)$ : a fee $p(S)$ for each subscription set $S \subseteq \mathcal M$ , and a rental price $r_j$ for each item. A user subscribed to $S$ gets utility $V_{ij}$ from an item $j \in S$ , $V_{ij} - r_j$ from an item $j \notin S$ , and $V_0$ from the outside option, and takes the best of these on each watch. Two per-watch quantities summarise this choice:

the subscription gain $\mathrm{SubGain}(i,S,\mathbf r)$ , the expected best utility under $S$ minus the expected best utility without a subscription;
the rental revenue $\mathrm{Rent}(i,S,\mathbf r)$ , the expected rental price paid.

By Proposition 2, for fixed $\mathbf r$ the platform chooses fees and an assignment $i \mapsto S_i$ to maximise the revenue

\sum_{i} q_i\big(p(S_i) + \lambda_i T\,\mathrm{Rent}(i,S_i,\mathbf r)\big)

subject to the incentive constraints $\lambda_i T\,\mathrm{SubGain}(i,S_i,\mathbf r) - p(S_i) \ge \lambda_i T\,\mathrm{SubGain}(i,S,\mathbf r) - p(S)$ for all $i$ and $S$ . Such $(p, S)$ with $p(\emptyset) = 0$ is a feasible planning. In the grand subscription only $\mathcal M$ is offered, at a fee $P$ , and each type subscribes or not according to its incentive.

Condition 2 (p. 12) requires, for every $i, i'$ and $S$ ,

\frac{\mathrm{SubGain}(i,S,\mathbf r)}{\mathrm{Rent}(i,\emptyset,\mathbf r) - \mathrm{Rent}(i,S,\mathbf r)} \le \frac{\mathrm{SubGain}(i,\mathcal M,\mathbf r)}{\mathrm{Rent}(i,\emptyset,\mathbf r)}, \qquad \frac{\mathrm{SubGain}(i,S,\mathbf r)}{\mathrm{SubGain}(i,\mathcal M,\mathbf r)} = \frac{\mathrm{SubGain}(i',S,\mathbf r)}{\mathrm{SubGain}(i',\mathcal M,\mathbf r)}.

The first part says the grand set has the best trade-off between subscription gain and lost rentals; the second says all types rank sets by the same relative gain.

Formalization targets

Goal: Theorem 2, first bullet (p. 13)

If $\mathbf r \ge 0$ satisfies Condition 2, then for all $\mathbf q$ and $\boldsymbol\lambda$ there are a fee $P$ and incentive-compatible subscription decisions $\sigma$ such that

\mathrm{revenue}(p, S) \le \mathrm{grandRevenue}(P, \sigma) \quad\text{for every feasible planning } (p, S).

Since the grand subscription is itself feasible, it achieves the optimal revenue.

Milestones

In attack order:

Lemma 2 (p. 10): $\mathrm{SubGain}(i,\mathcal M,\mathbf r) \ge \mathrm{SubGain}(i,S,\mathbf r) + \mathrm{Rent}(i,S,\mathbf r)$ .
Lemma 5 (pp. 21–22): $\mathrm{Rent}(i,\emptyset,\mathbf r) \ge \mathrm{Rent}(i,S,\mathbf r)$ and $\mathrm{SubGain}(i,\mathcal M,\mathbf r) \ge \mathrm{Rent}(i,\emptyset,\mathbf r)$ .
Claim 1 of the proof of Lemma 3 (p. 28): a type choosing a set of larger relative gain pays a weakly larger fee.
Lemma 3 (p. 13), with a strict hypothesis: types with larger $\lambda_i\,\mathrm{SubGain}(i,\mathcal M,\mathbf r)$ choose larger relative gains and pay larger fees.
Lemma 4 (p. 13): at an optimum, each type is indifferent between its set and the next lower type's set.
Mechanism 1 (p. 14): a lottery over the grand fees $\lambda_k T\,\mathrm{SubGain}(k,\mathcal M,\mathbf r)$ earns at least the revenue of any feasible planning.

Significance

The result separates what a menu of subscription sets can do from what the grand subscription does. Under Condition 2, which holds for instance for values with item-dependent Gumbel distributions (Example 2 of the paper), a platform loses nothing by offering a single subscription at a single fee, whatever the distribution of usage rates. The optimal fee is then one of $n$ candidates, $\lambda_k T\,\mathrm{SubGain}(k,\mathcal M,\mathbf r)$ , so the platform's problem collapses from a menu over $2^m$ sets to a one-dimensional choice.

The theorem has a published proof; this mission formalizes it. No part of it is machine-checked yet. A formal development would also settle the boundary cases the printed argument passes over: ties in the per-watch choice, ties among usage-weighted gains, and types with zero subscription gain.

Difficulty

The obvious argument is the single-type one: with one user type, Lemma 2 shows the grand set dominates. With several types, a menu can screen them by usage rate: frequent users buy large sets at high fees, infrequent users buy small sets or rent. The grand subscription cannot screen, and any single grand fee either excludes infrequent users (losing their fees) or undercharges frequent ones. So no single grand fee can be compared with a screening menu type by type. Any comparison has to cover rental revenue as well as fees: a menu that sells small sets keeps collecting rentals from the types it screens, while the grand subscription collects rentals only from non-subscribers. The menu's structure is also not explicit: the sets chosen by different types need not be nested, and without a common ranking of sets across types (part 2 of Condition 2) the menu's revenue does not decompose along the order of usage rates at all.

Formalization scope

All statements live in the namespace SubscriptionPlanning.GrandOptimal. User types are Fin n, item types Fin m, sets Finset (Fin m), and the values are real random variables on a probability space $(\Omega, P)$ , measurable and integrable. The model bundles $q_i \ge 0$ , $\sum_i q_i = 1$ , $\lambda_i > 0$ and $T > 0$ (the paper's standing assumptions, p. 4). The values may have any joint law; the paper draws them independently, and nothing in Theorem 2 uses independence.

Committed conventions, each disclosed in the item statements:

Tie-break. The per-watch choice is the first maximizer in a fixed order (outside option, then items by index). $\mathrm{Rent}$ is the expected rental price of the chosen item. This equals the printed formula when ties have probability zero; the printed " $\ge$ " counts every tied maximizer and makes Lemma 2 false for atomic laws.
Added hypotheses. $\mathbf r \ge 0$ (Lemmas 2 and 5 fail for negative prices) and $p(\emptyset) = 0$ (the paper's convention in the proof of Theorem 2).
Condition 2 cross-multiplied. With positive denominators it is the printed condition. Relative gains are real divisions with Lean's $x/0 = 0$ .
No supremum. Optimality is domination of every feasible planning.
The factor $T$ . It is kept wherever (3) has it, including Lemma 4 and Mechanism 1, where the page drops it.
Lemma 3 is posed with a strict hypothesis, since it is false on ties as printed. Lemma 4 adds $q_i > 0$ .
Mechanism 1 is posed as a revenue inequality for every feasible planning, under the orderings the paper assumes without loss of generality.

Trivializing readings. The goal is not "some grand fee beats some planning"; it is not stated with feasibility lacking any incentive constraint; and it does not fix all types to subscribe or let $\sigma$ ignore incentives. The goal quantifies the fee before every feasible planning, and $\sigma$ must respect each type's incentive.

Not posed. Theorem 2 opens with "if and only if", but only the first bullet (sufficiency) is posed. The second bullet (necessity) is false as printed. With a single user type the grand subscription is always optimal by Lemmas 2 and 5, yet part 1 of Condition 2 can fail. Theorem 3, Propositions 1–3 and Lemma 6 are also out of scope.

Infrastructure and contributions. A complete development needs expectations of maxima of finitely many integrable random variables, measurability of the first-maximizer choice, and finite telescoping sums; the per-watch choice lemmas (Lemmas 2 and 5) are reusable for any model of menus with per-use prices. Proofs of the milestones, alternative arguments for the goal, and sanity examples (e.g. Gumbel values) are welcome.

Selected references

S. Alaei, A. Makhdoumi, A. Malekian, Optimal Subscription Planning for Digital Goods, Operations Research, 2023. https://doi.org/10.1287/opre.2023.2468 ; working paper SSRN 3476296, https://ssrn.com/abstract=3476296

8 thms2 active usersReviewed

Completed

Dynamic Programming Linear algebra Operations Research·Captain: mikedeng1

Analytical Solution to a Discrete-Time Model for Dynamic Learning and Decision Making: the two-action frontier difference equations have a unique closed-form solution with explicit det YResearch Paper

Learning while doing, and the frontier of continuation values

Many sequential decisions trade off immediate reward against information: a firm prices without knowing which demand regime it faces, a clinician treats without knowing a patient's type, a bandit player pulls a risky arm to learn its mean. Formally these are partially observed Markov decision problems (POMDPs) with a hidden but fixed state. Their value function is the upper envelope of a set of linear functions of the belief, one continuation-value vector per policy. The efficient frontier of these vectors describes the optimal policy for every prior at once. Except for special cases, the frontier of a POMDP has to be computed numerically.

Hao Zhang (Management Science, 2021; accepted version SSRN 3847049) treats the case of two states, two actions and two signals. Under a commensurability condition on the signals, the extreme points of the frontier satisfy linear difference equations with constant coefficients (Theorems 2 and 4 of the paper). The paper solves these equations in closed form. Theorem 3 covers the case where the second action reveals nothing, so that it acts as a stopping action. Theorem 6 covers the case where both actions are informative. This mission formalizes the solution of the difference equations, including the explicit determinant of the coupling matrix that Appendix B states as Theorem 6 (Complete).

Setting

The hidden state is $\theta \in \{1, 2\}$ , the actions are $A$ and $B$ , and the signals are $\gamma$ and $\bar\gamma$ . In each period, action $a$ in state $\theta$ produces signal $\gamma$ with probability $p_\theta(a, \gamma)$ and an expected reward $r_\theta(a)$ , and rewards are discounted by $\delta \in (0, 1)$ . The anchor points $\hat u^a_\theta = (1-\delta)^{-1} r_\theta(a)$ are the values of always playing $a$ . Write $p^A_\theta = p_\theta(A,\gamma)$ and $p^B_\theta = p_\theta(B,\gamma)$ .

The signal quality indices are integers $n(A,\gamma) = n^A > 0$ , $n(A,\bar\gamma) = -\bar n^A < 0$ , $n(B,\gamma) = n^B > 0$ and $n(B,\bar\gamma) = -\bar n^B < 0$ . Their absolute values are relatively prime, and for some $\mu > 1$ each log-likelihood ratio $\ln(p_1(a,s)/p_2(a,s))$ equals $n(a,s) \ln\mu$ (Definition 3).

For each $\theta$ the paper's boundary-value problem (28)–(31) asks for real sequences $v^A, v^B$ on $k = 0, 1, 2, \dots$ satisfying four conditions:

v^A(k+n^A) - \delta^{-1}(p^A_\theta)^{-1} v^A(k) + (p^A_\theta)^{-1}(1-p^A_\theta)\, v^A(k-\bar n^A) = 0 \quad (k \ge \bar n^A),

v^B(k+\bar n^B) - \delta^{-1}(1-p^B_\theta)^{-1} v^B(k) + (1-p^B_\theta)^{-1} p^B_\theta\, v^B(k-n^B) = 0 \quad (k \ge n^B),

the coupling condition $v^A(k) + \hat u^A_\theta = v^B(\bar n^A + n^B - 1 - k) + \hat u^B_\theta$ for $k = 0, \dots, \bar n^A + n^B - 1$ , and decay, $v^A(k), v^B(k) \to 0$ .

The characteristic polynomials are

f^A_\theta(z) = z^{n^A+\bar n^A} - \delta^{-1}(p^A_\theta)^{-1} z^{\bar n^A} + (p^A_\theta)^{-1}(1-p^A_\theta), \qquad f^B_\theta(z) = z^{n^B+\bar n^B} - \delta^{-1}(1-p^B_\theta)^{-1} z^{n^B} + (1-p^B_\theta)^{-1}p^B_\theta.

$Z^a_{unit}$ is the set of their roots with $|z| < 1$ , and $m^a_z$ is the multiplicity of the root $z$ . From these roots the paper builds a square matrix $Y = (Y^A, Y^B)$ . Its A-columns are $\binom{k}{\tau}z^{k-\tau}$ and its B-columns are $\binom{\bar n^A+n^B-1-k}{\tau}z^{\bar n^A+n^B-1-k-\tau}$ , in a fixed column order.

Formalization targets

Goal: Theorem 6 (Complete), EC p. 11

For each $\theta$ , under the standing assumptions of §5, the goal asserts four things:

$\sum_{z\in Z^A_{unit}} m^A_z = \bar n^A$ and $\sum_{z\in Z^B_{unit}} m^B_z = n^B$ .
For every enumeration of the roots,

\det Y = \prod_{i<l}(z^A_l - z^A_i)^{m^A_i m^A_l}\prod_{i,l}(1 - z^A_i z^B_l)^{m^A_i m^B_l}\prod_{i<l}(z^B_i - z^B_l)^{m^B_i m^B_l}.

$\det Y \ne 0$ .
The problem (28)–(31) has exactly one real solution. That solution is the root expansion $v^a_\theta(k) = \sum_{z \in Z^a_{unit}}\sum_{\tau<m^a_z}\alpha^a_{z,\tau}\binom{k}{\tau}z^{k-\tau}$ , whose coefficients are given by $(\boldsymbol\alpha^A; -\boldsymbol\alpha^B) = (\hat u^B_\theta - \hat u^A_\theta)Y^{-1}\mathbf 1$ .

Milestones

Eq. (18): the general solution of a constant-coefficient linear recurrence with repeated characteristic roots.
Eq. (19): the determinant of the generalized (confluent) Vandermonde matrix.
From the proof of Theorem 3: $z^{n+\bar n} - \delta^{-1}p^{-1}z^{\bar n} + p^{-1}(1-p)$ has exactly $\bar n$ roots in the open unit disk, counted with multiplicity.
From the proof of Theorem 3: decay of an exponential polynomial forces zero coefficients on every root with $|z| \ge 1$ .
Theorem 3: the one-sided problem (13)–(15), when action $B$ is uninformative.
The base case and the inductive step of the determinant computation in the proof of Theorem 6 (Complete).

Significance

The result turns the efficient frontier of this class of POMDPs into explicit algebra. Each extreme point is a finite sum over the roots of two trinomials in the unit disk, and the coefficients come from one linear solve. The paper uses this to explain the shape of the frontier: how many extreme points the two actions contribute, and how quickly they accumulate at the anchor points. It also shows that the coupled two-sided problem is always well posed, because $Y$ is nonsingular.

The paper proves the results in prose; none of them is machine-checked. The mission contributes a checked proof of the solution formula and of the determinant identity. The identity is a confluent Vandermonde-type evaluation with a reflected second block. Several pieces are general mathematics that Mathlib lacks: the solution space of a linear recurrence with repeated roots in binomial form, the confluent Vandermonde determinant, root counting in the unit disk, and the decay lemma for exponential polynomials.

Difficulty

The obvious argument is to write down the general solution, discard the growing modes and match the boundary data. It runs into three problems. First, the count of roots in the disk is what makes $Y$ square. It comes from Rouché's theorem, which Mathlib does not have, so it must be proved or replaced by a polynomial argument. Second, roots on the unit circle are not excluded a priori, so the decay argument has to handle polynomially weighted unimodular terms. Third, and hardest, is $\det Y \ne 0$ . $Y$ is not a confluent Vandermonde matrix: its B-block is reflected ( $N-1-k$ in place of $k$ ). The paper reduces the simple-root case to a Vandermonde matrix in the inverted points $1/z^B_j$ , and then handles each repeated B-root by differentiating with respect to a "nominal root". Making that induction precise requires care with column orders and signs.

Formalization scope

The Lean development lives in the namespace LearnDoFrontier.TwoAction. A Model carries $\delta$ , $p^A_\theta$ , $p^B_\theta$ , the rewards $r_\theta(a,s)$ and the four indices, with the negative indices stored as the positive naturals $\bar n^A, \bar n^B$ . States, actions and signals are Fin 2, and index 0 stands for $\theta = 1$ , $A$ and $\gamma$ . Model.Standing collects the assumptions of §5: $0<\delta<1$ , General Position, Informative Actions A and B, and Definition 3, with "relatively prime" read as a joint gcd of $1$ . Sequences are real and indexed by $\mathbb N$ , while the roots, coefficients and $Y$ are complex. The solution formula is an equality in $\mathbb C$ . Root enumerations are arbitrary bijections onto $Z^a_{unit}$ , universally quantified, and the columns of $Y$ follow the paper's order: A-columns first, roots first, then $\tau$ ascending for A and descending for B. Exponents use natural-number subtraction, which is harmless because the binomial factor vanishes whenever $k<\tau$ . The determinant milestones are stated for arbitrary distinct points rather than roots, as the paper's induction uses them.

No formalization may make the targets hold by definition. $Z_{unit}$ and $m_z$ are the actual roots and multiplicities, never "the first $\bar n^A$ roots". Uniqueness ranges over all real sequences satisfying (28)–(31), not only over root expansions. The coefficients are given by $Y^{-1}$ , not chosen to fit the boundary.

The link from the POMDP's efficient frontier to (13)–(15) and (28)–(31) (Theorems 2 and 4) is not formalized. Its proofs are geometric sketches, and Theorem 4 assumes a two-segment frontier structure that the paper itself calls a conjecture. The mission is about the difference equations exactly as the paper poses them. Proofs of any milestone are welcome, and the recurrence, Vandermonde and root-count lemmas are reusable well beyond this mission.

Selected references

Hao Zhang, Analytical Solution to a Discrete-Time Model for Dynamic Learning and Decision Making, Management Science, 2021. https://doi.org/10.1287/mnsc.2021.4194 ; accepted version with E-Companion: https://ssrn.com/abstract=3847049
Saber Elaydi, An Introduction to Difference Equations, 3rd ed., Springer, 2005. https://doi.org/10.1007/0-387-27602-5
Richard D. Smallwood and Edward J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5), 1973. https://doi.org/10.1287/opre.21.5.1071

10 thms2 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

What Is the Impact of Nonrandomness on Random Choice Models?: Revenue-Ordered Assortments Are Optimal When One Product's Utility Is DeterministicResearch Paper

Motivation

Retailers choose which products to show a customer, and the customer chooses at most one of them. The assortment problem asks for the offer set that maximizes expected revenue, given a model of how customers choose. Under the multinomial logit (MNL) model every alternative, the no-purchase option included, carries an independent Gumbel noise term of the same scale, and Talluri and van Ryzin (2004) showed that the optimal set is then a revenue-ordered assortment: the $n$ most expensive products, for some $n$ . This structure turns an exponential search over subsets into a comparison of $N$ candidates, and it is the reason MNL-based assortment optimization is used in practice.

Equal randomness for all alternatives is a strong assumption. A product a consumer has bought many times, or a well-advertised one, is known; its utility carries little or no noise. Wang (SSRN 3579781; published in Manufacturing & Service Operations Management, 2021) studies the extreme case in which exactly one alternative has a deterministic utility. The choice probabilities for that case go back to Besanko, Perry and Spady (1990) and are no longer MNL once that alternative is offered. The paper asks what this does to the standard operations problems. Its answer for assortment planning splits in two: if the deterministic alternative is a product, revenue-ordered assortments remain optimal (Theorem 5); if it is the no-purchase option, the feasibility version of the assortment problem is NP-complete (Theorem 6). This mission formalizes the first half.

Setting

Let $\mathcal N=\{1,\dots,N\}$ be the products and $0$ the no-purchase option, always available. Utilities are $U_i=u_i+\xi_i$ for $i\in\mathcal N\setminus\{i'\}$ and $U_0=u_0+\xi_0$ , with the $\xi$ 's independent Gumbel of scale $\mu>0$ and mean zero; one product $i'$ has deterministic utility $U_{i'}=u_{i'}$ . Product $i$ has price $p_i$ . Write

$a_i=\exp(u_i/\mu)$ and $a_0=\exp(u_0/\mu)$ for the attraction values;
$\Lambda=\exp(-u_{i'}/\mu-\gamma)$ , with $\gamma$ the Euler–Mascheroni constant;
$\Psi(S^+/\{i'\})=a_0+\sum_{j\in S\setminus\{i'\}}a_j$ for an offer set $S\subseteq\mathcal N$ .

If $i'\notin S$ the choice probabilities are MNL: $q_i(S)=a_i/(a_0+\sum_{j\in S}a_j)$ . If $i'\in S$ , with $\Psi=\Psi(S^+/\{i'\})$ , they are given by model (1):

q_i(S)=\frac{a_i}{\Psi}\bigl[1-e^{-\Lambda\Psi}\bigr]\ (i\in S\setminus\{i'\}),\qquad q_{i'}(S)=e^{-\Lambda\Psi},

and $q_0(S)=1-\sum_{i\in S}q_i(S)$ . The expected revenue (12) is $R(S)=\sum_{i\in S}p_iq_i(S)$ , which on the page reads

R(S)=\begin{cases}\dfrac{\sum_{i\in S}p_ia_i}{a_0+\sum_{j\in S}a_j}, & i'\notin S,\\[1.5ex]\dfrac{\sum_{i\in S\setminus\{i'\}}p_ia_i}{\Psi}\bigl[1-e^{-\Lambda\Psi}\bigr]+p_{i'}e^{-\Lambda\Psi}, & i'\in S.\end{cases}

The assortment problem (13) is $\max_{S\subseteq\mathcal N}R(S)$ . When the products, $i'$ included, are labelled so that $p_1\ge p_2\ge\dots\ge p_N$ , the sets $S_n=\{1,\dots,n\}$ are the revenue-ordered assortments.

In Lean the products are Fin N, and attr, attr0, Lam, Psi, choiceProb, revenue12 and roSet N n are $a_i$ , $a_0$ , $\Lambda$ , $\Psi$ , $q_i(S)$ , $R(S)$ and $S_n$ .

Formalization targets

Goal: Theorem 5 (p. 14)

For $\mu>0$ and prices $p_1\ge\dots\ge p_N\ge0$ ,

\exists\,n\in\{1,\dots,N\}:\qquad R(S)\le R(S_n)\quad\text{for all }S\subseteq\mathcal N .

The statement fixes no constants; it asserts only the structure of an optimal set.

Milestones

Lemma 1 (p. 28). For any regular choice model in which each $q_i(S)$ , $i\in S$ , is a nonnegative convex function of $q_0(S)$ , and prices $p_1\ge\dots\ge p_N$ , some $S_n$ , $n\in\{0,\dots,N\}$ , maximizes $R(S)=\sum_{i\in S}p_iq_i(S)$ .
$q_0$ is increasing and concave in $q_{i'}$ (p. 29). With $a_0=1$ , $q_0=h_\Lambda(q_{i'})$ where $h_\Lambda(y)=\Lambda(1-y)/(-\log y)$ , increasing and concave on $(0,1)$ .
$q_{i'}$ is increasing and convex in $q_0$ (p. 29). The inverse of $h_\Lambda$ is increasing and convex on the range of $h_\Lambda$ .
The model satisfies Lemma 1 (pp. 14, 29). The model above is regular, each $q_i$ is a nonnegative convex function of $q_0$ , and (12) equals $\sum_{i\in S}p_iq_i(S)$ .

Significance

Theorem 5 says that a deterministic product utility, which destroys the MNL form of the choice probabilities, does not destroy the nested structure of the optimal assortment. The problem therefore stays solvable by checking $N$ sets, in contrast with the companion case of a deterministic no-purchase utility, whose feasibility version is NP-complete. Lemma 1 is a criterion of independent use: any regular choice model whose choice probabilities are convex functions of the no-purchase probability has a revenue-ordered optimal assortment, and the MNL model is the case of linear functions.

The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. The mission produces a checked version of the convex-in- $q_0$ criterion on top of the platform's published regular-choice-model definitions, and a checked treatment of model (1), which is also the model of truncated utilities (Corollary 2 of the paper).

Difficulty

The classical MNL argument uses the fact that $R(S)$ is a ratio of sums linear in the attraction values, so optimality reduces to a threshold on prices. Model (1) is not of that form once $i'$ is offered: $q_{i'}=e^{-\Lambda\Psi}$ and the other probabilities carry the factor $(1-e^{-\Lambda\Psi})/\Psi$ , so a direct exchange argument on the revenue fails. The work lies in the analytic step: expressing $q_{i'}$ as a function of $q_0$ only through the implicit relation $q_0=\Lambda(1-q_{i'})/(-\log q_{i'})$ , and establishing that this function is convex, which requires sign control of a second derivative involving $\log$ near both ends of $(0,1)$ . A formal proof must also check regularity of the model, which the printed proof uses but does not verify.

Formalization scope

The model is encoded as in the Setting: products Fin N (the label $k$ is index $k-1$ ), the deterministic product as a parameter ip, and the no-purchase option outside Fin N. $R$ is the two-branch revenue (12), written literally, not the MNL revenue, and optimality is over all subsets of $\mathcal N$ ; the MNL special case alone is not the goal. Committed conventions:

$\mu>0$ (implicit on p. 5) and the Euler–Mascheroni constant Real.eulerMascheroniConstant in $\Lambda$ ; $a_{i'}$ plays no role;
$p_1\ge\dots\ge p_N$ is Antitone p, and $S_n$ is the set of the first $n$ indices (ties in prices do not change $S_n$ );
the goal adds $p_i\ge0$ : with all prices negative, $\emptyset$ is the unique optimum and no $S_n$ with $n\ge1$ is optimal;
Lemma 1 uses the published RevenueOrdered.Ratio.IsRegular, whose monotonicity includes the no-purchase option, as the proof uses; " $q_i=q_i(q_0)$ convex" means $f_i$ nonnegative and convex on a convex set $D_i$ containing $q_0(S)$ for every $S\ni i$ ; its conclusion allows $S_0=\emptyset$ ;
milestones 2 and 3 are stated on the open interval $0<q_{i'}<1$ , since the formula is $0/0$ at $q_{i'}=1$ .

A complete development needs elementary real analysis of $\log$ and $\exp$ (monotonicity and concavity via derivatives, inverse functions on intervals) and finite-sum algebra; Lemma 1 is reusable for any regular choice model. Contributions on the analytic lemmas and on regularity of model (1) are welcome.

Selected references

R. Wang, What Is the Impact of Non-Randomness on Random Choice Models?, SSRN 3579781; Manufacturing & Service Operations Management, 2021. https://ssrn.com/abstract=3579781, doi:10.1287/msom.2020.0951
D. Besanko, M. K. Perry, R. H. Spady, The logit model of monopolistic competition: Brand diversity, The Journal of Industrial Economics 38(4), 397–415, 1990 (reference as listed in Wang's bibliography, p. 31).
K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
G. Berbeglia, G. Joret, Assortment optimisation under a general discrete choice model: a tight analysis of revenue-ordered assortments, Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371

7 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Coordination for Assembly: With at Most M − 1 Feedback Periods, the Subgame-Perfect Secure Equilibrium Has Every Contractor Exert the Minimum Effort in Every PeriodResearch Paper

Motivation

Assembly projects such as aircraft programs or large software releases split work among several contractors, each responsible for one component. The finished product can only be as advanced as its least-developed component, so the contractors play a minimum-effort game (also called a weakest-link game): the project's value depends on the minimum of the efforts, while each contractor pays for its own effort. Such games have a continuum of Nash equilibria, ranked by payoff, and laboratory evidence since Van Huyck, Battalio and Beil (1990) shows that groups often settle on low-effort equilibria, with larger groups faring worse.

An original-equipment manufacturer (OEM) can affect coordination through the information it shares. Zhang, Shokoohyar, Qi and Katok, Coordination for Assembly (Manufacturing & Service Operations Management, doi:10.1287/msom.2023.0342), study a periodic information-feedback mechanism: the project runs over $N$ periods, and at the start of each period every contractor sees every contractor's progress. Their theoretical prediction, tested in the laboratory, is that the number of feedback periods relative to the number of contractors decides whether coordination succeeds. This mission formalizes the negative half of that prediction: with too few feedback periods, the selected equilibrium is the worst one.

Setting

There are $M$ contractors and $N$ periods. Each contractor's total effort lies in $[\underline q, \bar q]$ and its effort in each period lies in $[\underline q/N, \bar q/N]$ , with $0 \le \underline q < q^* < \bar q$ , where $q^*$ is the OEM's target level. All contractors start at zero effort. In period $n$ each contractor observes all efforts so far and then all simultaneously choose $q_{i,n}$ ; the effort level of contractor $i$ after period $n$ is $\hat q_{i,n} = \sum_{t \le n} q_{i,t}$ .

The project level is $q_{\min}(\hat{\mathbf q}_N) = \min_i \hat q_{i,N}$ , the OEM's payoff is $S = p \min\{q_{\min}(\hat{\mathbf q}_N), q^*\}$ , and contractor $i$ receives the share $\gamma$ of it and pays $c$ per unit of effort:

\pi_i(\hat{\mathbf q}_N) = \gamma\, p\min\{q_{\min}(\hat{\mathbf q}_N), q^*\} - c\, \hat q_{i,N}.

The parameters satisfy $p, \gamma, c > 0$ .

A history is the list of effort profiles played so far; a strategy maps each history to the current period's effort. A subgame-perfect equilibrium (SPE) is a strategy profile from which no contractor gains by deviating after any history. For a history $h$ , write $\hat E(h)$ for the set of final level vectors reached by continuing some SPE from $h$ .

A subgame-perfect secure equilibrium (SPSE) (Definition 2 of the paper's Online Appendix) is an SPE $\sigma^\dagger$ such that, at the start of every period along its own path, each contractor's own final level $y$ maximizes its worst-case profit

\inf_{x \in \hat E(h)} \pi_i(y;\, x_{-i})

among the levels $y$ that contractor $i$ attains in some SPE continuation. This is the paper's condition (24): among equilibria, contractors favour the one that protects them against the other contractors' least favourable equilibrium behaviour.

Formalization targets

Goal: Proposition 2(i)

If $N \le M - 1$ , then an SPSE exists in which every contractor exerts the minimum effort in every period, every SPSE has this property along its path, and the project level is minimal:

q_{i,n} = \frac{\underline q}{N}\quad (i \le M,\ n \le N), \qquad q_{\min}(\hat{\mathbf q}_N) = \underline q .

Milestones

Lemma OA2(i). If $N \le M-1$ and at least $N+1$ contractors share the lowest initial effort level, some SPE has every contractor exert $\underline q/N$ in every period.
Proof of Proposition 2, Step 1. Along a path on which every contractor exerts $\underline q/N$ , continuing that path gives each contractor the minimum profit among all SPE continuations of each subgame (the paper's condition (25)).
Proof of Proposition 2, Step 1 (uniqueness). In an SPE where one contractor exerts $\underline q/N$ in every period, all contractors do.

Significance

The result says that frequent progress reports are not enough by themselves: when there are fewer feedback periods than contractors minus one, the secure refinement of subgame perfection selects the lowest project level, the same outcome as without feedback. It is the theoretical half of the paper's comparison between feedback regimes, which the laboratory experiment then tests with groups of two and four contractors and 1 to 6 feedback periods.

The result has a printed proof in the paper's Online Appendix. No machine-checked version exists. Formalizing it pins down a solution concept (an SPE refined by a maxmin criterion over the set of equilibrium outcomes of each subgame) whose verbal definition admits several inequivalent readings, and fixes which one the proposition holds for.

The companion part (ii) of Proposition 2, for $N > M - 1$ , is false as printed and is not part of this mission: with $M = 2$ , $N = 3$ , $\underline q = 3$ , $\bar q = 9$ , $q^* = 7$ , $\gamma = p = 1$ , $c = 3/4$ , the profile with path $(1,1), (1,1), (3,3)$ is an SPE with project level $5$ , and no SPSE reaches $q^* = 7$ , although part (ii) predicts that level at $N = N^* = 3$ . Corollary 2 and Proposition 3, which rest on part (ii), are omitted for the same reason.

Difficulty

The existence half is a statement about whole strategy profiles, including play after every history off the equilibrium path. The constant profile that plays $\underline q/N$ after every history is not an SPE when $\gamma p > c$ : after a history that leaves one contractor strictly behind with one period to go, that contractor gains by catching up. An SPE with the all-minimum path must therefore prescribe different, history-dependent behaviour off the path, and the count $N + 1 \le M$ of tied contractors is what keeps a single deviation from breaking the tie at the bottom.

The SPSE condition quantifies over the set of all SPE outcomes of each subgame, so neither half can be checked by looking at one profile: both existence and uniqueness require knowing that the all-minimum outcome lies in that set at the relevant histories.

Formalization scope

All quantities are real numbers; there is no probability. Contractors are indexed by Fin M and periods are 0-based (pathHist σ n is the history before the paper's period $n+1$ ). A history is a List (Fin M → ℝ) and strategies are arbitrary functions of the history: under feedback every past effort is observed, and restricting to state-dependent or open-loop strategies would change the set of SPEs that the definition compares against.

Committed conventions:

the standing assumptions $1 \le M$ , $1 \le N$ , $0 \le \underline q < q^* < \bar q$ , $p, \gamma, c > 0$ are explicit hypotheses; $\gamma p > c$ is not assumed;
$N \le M-1$ is written N + 1 ≤ M;
(24) is stated with final level vectors rather than the totals of periods $n$ to $N$ (a bijection once the history is fixed), its "min" as an infimum and its " $=$ arg max" as membership in the argmax;
(24) is imposed only at the SPSE's own on-path histories, as Definition 2 says ("with the state of period $n$ , $\hat{\mathbf q}^\dagger_{n-1}$ ");
"unique SPSE" is stated as "every SPSE has the all-minimum path"; the off-path part of an SPSE is never unique.

Trivializing encodings are ruled out: the SPSE carries the SPE clause, the condition is neither dropped nor imposed at every history (under which no SPSE would exist), and the goal includes an existence conjunct, so it cannot hold vacuously.

The development needs the game, its SPE and SPSE (one definition file in the mission), and arguments about backward induction in a finite-horizon game with continuous actions. Proofs of the milestones, of the goal, and reusable lemmas about cumulative-effort games are all welcome.

Selected references

W. Zhang, S. Shokoohyar, A. Qi, E. Katok, Coordination for Assembly, Manufacturing & Service Operations Management, 2025. doi:10.1287/msom.2023.0342 (cited from the authors' manuscript of 10 July 2025).
J. B. Van Huyck, R. C. Battalio, R. O. Beil, Tacit Coordination Games, Strategic Uncertainty, and Coordination Failure, American Economic Review 80(1), 1990, 234–248.

5 thms2 active usersReviewed

Algorithmic Game Theory Linear Optimization Mechanism Design+1·Captain: mikedeng1

Spatio-Temporal Pricing for Ridesharing Platforms: The STP Mechanism Is Subgame-Perfect Incentive Compatible, Welfare-Optimal, Envy-Free and Core-Selecting from Any HistoryResearch Paper

Motivation

Ridesharing platforms set prices and dispatch drivers over a road network whose demand changes within minutes: a stadium empties, rush hour starts, a neighbourhood goes quiet. Drivers are not employees. They may decline a dispatch, drive somewhere else, or stop working, and the platform pays no one in advance for staying in place. Prices that look only at the current moment (myopic pricing) jump sharply in space and time and reward drivers who wait for a surge instead of taking the dispatch they are given (Ma, Fang, Parkes 2022, §2).

H. Ma, F. Fang and D. C. Parkes ask for a dynamic mechanism under which following the platform's dispatches is in every driver's interest at every moment, including after other drivers have deviated, while the outcome stays efficient and fair. Their answer, the spatio-temporal pricing (STP) mechanism, was published in Operations Research in 2022 and builds on the competitive-equilibrium theory of assignment and flow markets (Shapley and Shubik 1971; Murota 2003).

Setting

Time runs over $t = 0, 1, \dots, T$ . There is a finite set $\mathcal L$ of locations and travel times $\delta(a,b) \ge 1$ with $\delta(a,a) = 1$ . A trip $(a,b,t)$ leaves $a$ at time $t$ and arrives at $b$ at time $t + \delta(a,b)$ ; it costs the driver $c_{a,b,t} \ge 0$ , and the trips that end by $T$ form the set $\mathcal T$ . A driver who stops working $\Delta$ periods before $T$ pays $\kappa_\Delta \ge 0$ , with $\kappa_0 = 0$ .

Each driver $i$ has a type $(\beta_i, \ell_i, \tau_i)$ : she can start at location $\ell_i$ at time $\tau_i$ , and $\beta_i = 1$ if she is already working, $\beta_i = 0$ if she still decides whether to enter (not entering costs nothing). Each rider $j$ asks for the single trip $(o_j, d_j, \tau_j) \in \mathcal T$ and values it at $v_j \ge 0$ . A path of driver $i$ is a chain of trips starting at $(\ell_i,\tau_i)$ ; its cost $\lambda$ is the sum of its trip costs plus the early-exit cost at its end. A dispatching assigns each driver a path and each picked-up rider to a driver whose path covers her trip; its welfare is the value of the riders picked up minus the drivers' costs, and $W(\mathcal D, \mathcal R)$ is the largest welfare over all dispatchings.

Anonymous trip prices $p_{a,b,t}$ charge every picked-up rider the price of her trip and pay it to the driver who carries her. Together with a dispatching they form a competitive equilibrium (CE) when every rider who values her trip above its price is picked up, nobody pays more than her value, and every driver's utility is the best that any of her paths could earn at these prices. The welfare gain from an additional driver at $(a,t)$ is

\Phi_{a,t} = W(\mathcal D \cup \{(1,a,t)\}) - W(\mathcal D).

The STP mechanism computes a welfare-optimal dispatching, dispatches every available driver along it, and prices every trip by

p_{a,b,t} = \Phi_{a,t} - \Phi_{b,\,t+\delta(a,b)} + c_{a,b,t}.

It recomputes the dispatching and the prices on the remaining economy $E^{(t)}(s_t)$ whenever some driver has deviated at time $t-1$ . A driver who declines a dispatch is paid nothing in that period and pays no penalty.

Formalization targets

Goal: Theorem 2

For every rule that picks a welfare-optimal dispatching, the STP mechanism

is temporally consistent: after a deviation, the new plan is the plan the mechanism would compute at time $0$ for the remaining economy;
is subgame-perfect incentive compatible (SPIC): from every history, no driver gains from any strategy while the others follow the dispatches,

\sum_{t'=t}^{T-1} \hat\pi_{i,t'}(\sigma^*_i|_{h_t}, \sigma^*_{-i}|_{h_t}) \ \ge\ \sum_{t'=t}^{T-1} \hat\pi_{i,t'}(\sigma_i|_{h_t}, \sigma^*_{-i}|_{h_t});

is individually rational for riders and strictly budget balanced for every strategy profile;
produces, from every history onward, an outcome that is welfare-optimal, in the core, envy-free for drivers and riders, and individually rational for drivers.

Milestones

The static theory of §3 comes first: Lemma 1 (non-negative prices), Lemma 6 (relocation trips have non-positive price), Lemma 2 (integrality of the LP relaxation), Lemma 3 (welfare theorem), Lemma 7 (correspondence of the two dual LPs), Lemma 4 (CE driver utilities form a lattice with bottom $\Phi_{D_i}$ and top $\Psi_{D_i}$ ) and Lemma 5 (core equivalence). The proof of Theorem 2 then contributes:

Step 1: the STP prices make every welfare-optimal plan a CE in which driver $i$ earns $\Phi_{D_i}$ ;
its consequence, a driver's continuation utility under the current plan;
the three inequalities (i)–(iii) of Step 2 between replica gains $\Phi^{(t)}_{a,t}(s_t)$ of successive time-shifted economies.

Significance

Theorem 2 shows that a platform can align incentives without long-term contracts, penalties or the threat of firing: the deviating driver's payoff is computed from a re-planned economy, and the replica-gain prices make that payoff no larger than the payoff of following the dispatch. The paper also proves that no mechanism with these properties makes following the dispatch a dominant-strategy equilibrium (Theorem 3), so subgame perfection is the right notion here.

The result is proved in the paper; it has not been formalized. A search of the Prove2Me library found no machine-checked statement of a dynamic ridesharing mechanism, of the CE lattice of a path economy, or of the replica-gain characterization of the driver-pessimal CE. A complete development would give a checked welfare theorem and core equivalence for a flow-based market, a lattice of CE utilities identified with marginal welfare gains, and a subgame-perfection argument for a re-planning mechanism.

Difficulty

The static part reduces to linear programming over paths, whose number grows exponentially with $|\mathcal L|$ and $T$ . Integrality and the lattice structure come from a translation to a minimum-cost flow problem and its dual, which has to be set up and connected back to paths.

The dynamic part is harder. A naive argument would compare a deviating driver's payoff against prices fixed at time $0$ , but STP re-plans after the deviation: the deviator's later payments come from a different economy, computed with different prices. Recomputing a driver-pessimal CE at every step breaks incentive compatibility (Example 3). STP is incentive compatible only because of an exchange inequality between replica gains (part (iii)). It says that adding a driver at the node a deviator drives to lowers the marginal value of another driver there at least as much as the deviator's planned position does. This is a local exchange property of M♮-concave functions, the optimal values of flow problems (Murota 2016), and has no counterpart in Mathlib.

Formalization scope

Lean represents an economy by a finite type of locations, drivers indexed by a finite type ι, riders indexed by a finite type κ, times in ℕ with explicit ≤ T guards, and money in ℝ. The replica of a driver is the index none of Option ι, removal is the subtype {k // k ≠ i}, and a coalition is a pair of subsets. W is the supremum of the welfares of feasible integral dispatchings, a finite nonempty set for every valid economy.

The conventions that the formalization commits to:

Under assumption (S1) every driver stays until $T$ , so the exit time $\bar\tau_i$ is dropped and the replica in $\Phi_{a,t}$ is the type $(1,a,t)$ .
Every requested trip lies in $\mathcal T$ , part of a valid economy.
A blocking coalition must use a budget-balanced plan among its members.
In the time-shifted economy, an available driver who has not entered keeps $\beta = 0$ . This corrects a slip on p. 20, and the proof uses it.
Definitions 8–10 bundle SPIC as condition (i). Here SPIC is stated once and the other properties state their condition (ii).
Rider envy-freeness (26) is read from the history $h_{\tau_j}$ .
Theorem 2 is claimed for every selector of welfare-optimal dispatchings, since Definition 12 leaves the choice of optimum open.

The goal must not be trivialized. It is not satisfied by some unspecified mechanism, by SPIC only at time $0$ , by SPIC only against one-shot deviations along the equilibrium path, or by one fixed selector. Temporal consistency compares the mechanism's plan after a deviation with its own time- $0$ plan of a different economy, so it is not a comparison of STP with itself.

A complete development needs:

path enumeration and the reduction to minimum-cost flow;
LP duality and complementary slackness for the flow problem;
integrality of flows;
the M♮-concavity of flow values;
a principle of optimality for continuations of optimal plans.

The CE, core and lattice layers do not depend on ridesharing. Contributions to any milestone, or to these general tools, are welcome.

Selected references

H. Ma, F. Fang, D. C. Parkes, Spatio-Temporal Pricing for Ridesharing Platforms, Operations Research, 2022; read here as arXiv:1801.04015v5, 2021. https://arxiv.org/abs/1801.04015v5
L. S. Shapley, M. Shubik, The assignment game I: The core, International Journal of Game Theory 1, 1971. https://doi.org/10.1007/BF01753437
K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
K. Murota, Discrete convex analysis: A tool for economics and game theory, Journal of Mechanism and Institution Design 1(1), 2016. https://doi.org/10.22574/jmid.2016.12.005
M. J. Osborne, A. Rubinstein, A Course in Game Theory, MIT Press, 1994.

25 thms2 active usersReviewed

Algorithmic Game Theory Machine Learning Optimization·Captain: mikedeng1

Greedy Adversarial Equilibrium: An Efficient Alternative to Nonconvex–Nonconcave Min-Max Optimization: Every Bounded Function with Lipschitz Hessian Has a Greedy Adversarial EquilibriumResearch Paper

Motivation

Min-max problems $\min_x\max_y f(x,y)$ model two-player zero-sum games and appear across machine learning and operations research: adversarial training of classifiers, generative adversarial networks, and robust optimization against an adversarial perturbation. When $f$ is convex in $x$ and concave in $y$ , von Neumann's minimax theorem gives a saddle point, and first-order methods find approximate ones. In the nonconvex–nonconcave case, which is the case of every neural-network objective, a global min-max point is intractable to find, and local notions such as local min-max points or local Nash equilibria need not exist at all (Jin, Netrapalli and Jordan, ICML 2020; Daskalakis, Skoulakis and Zampetakis, STOC 2021). Without existence there is nothing for an algorithm to converge to.

Mangoubi and Vishnoi propose an equilibrium notion that exists for every smooth bounded objective and can be computed in time polynomial in the dimension and the accuracy (arXiv:2006.12363). The max-player is modelled as an adversary that can only improve $f$ by local, "greedy" moves, and the min-player minimizes the value the adversary can reach this way.

Setting

Write $\mathbb R^d$ for each player's strategy space, with the Euclidean norm, and give $\mathbb R^d\times\mathbb R^d$ the norm $\sqrt{\|x\|^2+\|y\|^2}$ . Throughout, $f:\mathbb R^d\times\mathbb R^d\to\mathbb R$ is $C^2$ , $b$ -bounded ( $|f(x,y)|\le b$ ) and has an $L$ -Lipschitz Hessian, $\|\nabla^2f(x,y)-\nabla^2f(\tilde x,\tilde y)\|_{\mathrm{op}}\le L\sqrt{\|x-\tilde x\|^2+\|y-\tilde y\|^2}$ .

A point $y$ is an $(\varepsilon,\sqrt{L\varepsilon})$ -approximate local maximum of $f(x,\cdot)$ if $\|\nabla_yf(x,y)\|\le\varepsilon$ and $\lambda_{\max}(\nabla_y^2f(x,y))\le\sqrt{L\varepsilon}$ .

An $\varepsilon$ -greedy path for $f(x,\cdot)$ is a continuous path $\varphi:[0,\tau]\to\mathbb R^d$ , differentiable at all but finitely many points, travelling at unit speed, along which $\frac{d}{dt}f(x,\varphi_t)\ge-\varepsilon$ and, at every point, either $f$ increases at rate more than $\varepsilon$ or its second derivative in the direction of travel exceeds $\sqrt{L\varepsilon}$ . Let $S_{\varepsilon,x,y}$ be the set of endpoints of $\varepsilon$ -greedy paths starting at $y$ . The greedy max is

g_\varepsilon(x,y)=\sup\{f(x,z):z\in S_{\varepsilon,x,y}\}.

The greedy max is in general discontinuous in $x$ , so the min-player's stationarity is defined after truncation and Gaussian smoothing. For a bounded $\psi$ , a point $x^\star$ is an $(\varepsilon,\sigma)$ -approximate local minimum of $\psi$ if

\mathcal S(x)=\mathbb E_{\zeta\sim N(0,I_d)}\big[\min(\psi(x+\sigma\zeta),\psi(x^\star))\big]

satisfies $\|\nabla\mathcal S(x^\star)\|\le\varepsilon$ and $\lambda_{\min}(\nabla^2\mathcal S(x^\star))\ge-\sqrt\varepsilon$ .

A pair $(x^\star,y^\star)$ is an $(\varepsilon,\sigma)$ -greedy adversarial equilibrium if $y^\star$ is an $(\varepsilon,\sqrt{L\varepsilon})$ -approximate local maximum of $f(x^\star,\cdot)$ and $x^\star$ is an $(\varepsilon,\sigma)$ -approximate local minimum of $g_\varepsilon(\cdot,y^\star)$ .

Formalization targets

Goal: existence (Theorem 3.1, first two sentences, p. 10)

For every $d\ge1$ , $\varepsilon,\sigma>0$ with $\sigma\le1/\sqrt{\varepsilon d}$ , and every $f$ as above,

\exists\,\varepsilon^\star\in(0,\varepsilon]\ \ \exists\,(x^\star,y^\star):\quad (x^\star,y^\star)\text{ is an }(\varepsilon^\star,\sigma)\text{-greedy adversarial equilibrium of }f.

The accuracy $\varepsilon^\star$ is not fixed in advance; the theorem asserts that some accuracy at least as fine as $\varepsilon$ is attained.

Milestones

Lemma 7.2 (24)–(25): the output $y_{\mathrm{LocalMax}}$ of the greedy-path subroutine (Algorithm 1) satisfies $\|\nabla_yf\|\le\varepsilon'$ and $\lambda_{\max}(\nabla_y^2f)\le\sqrt{L\varepsilon'}+\mu_4$ .
Proposition 7.4: the polygonal path traced by Algorithm 1 is a $\frac1{1+\delta}\varepsilon'$ -greedy path.
Proposition 7.5: the computable lower bound $h_{\varepsilon^\circ}(x,y)=f(x,y_{\mathrm{LocalMax}})$ satisfies $h_{\varepsilon^\circ}\le g_{\varepsilon^\circ}$ .
Proposition 7.7: the zeroth-order estimator $\hat\Gamma=[\mathbb h(x+\sigma u)-c]\frac1\sigma u$ is unbiased for $\nabla_x\mathfrak h$ and has a sub-Gaussian tail.
Lemma 7.3: if $h_\varepsilon$ is a lower bound for $g_\varepsilon$ that agrees with it at $(x^\star,y^\star)$ , and the smoothed truncated $h_\varepsilon$ is very nearly second-order stationary at $x^\star$ with a small stochastic gradient, then $x^\star$ is an $(\varepsilon,\sigma)$ -approximate local minimum of $g_\varepsilon(\cdot,y^\star)$ .

Significance

The theorem gives the first equilibrium notion for nonconvex–nonconcave min-max optimization that is both guaranteed to exist for every $C^2$ bounded objective with Lipschitz Hessian and computable with polynomially many gradient, Hessian and function evaluations. It requires no convexity, monotonicity, bilinearity or initialization near an equilibrium. At an equilibrium, neither player can improve by a local move of the kind second-order methods make: the max-player cannot climb by a greedy path, and the min-player cannot decrease the value the adversary will reach. Appendix A of the paper shows that in the strongly convex–strongly concave case the duality gap at such a point is small, so the notion refines the classical saddle point.

The result is proved on paper and has not been machine-checked. A formalization adds three things beyond the paper. First, a verified calculus of second-order approximate stationarity for discontinuous functions through truncated Gaussian smoothing, reusable for other nonsmooth objectives. Second, a precise account of the paper's conventions: Definition 2.1's second derivative has to be read directionally, (25) holds only with an added $\mu_4$ , and Lemma 7.3 holds only for $\sigma,\varepsilon\le1$ , as its proof requires. Third, it settles whether the existence statement holds for every $\sigma\le1/\sqrt{\varepsilon d}$ , including $\sigma>1$ , which the printed proof does not cover.

Difficulty

The obvious approach is to minimize $x\mapsto\max_zf(x,z)$ , but that function is intractable to evaluate and need not have approximate local minima reachable by local moves. The greedy max $g_\varepsilon$ replaces it, but $g_\varepsilon$ is a supremum over an uncountable family of paths, cannot be computed exactly, and jumps as $x$ moves: Example 2.4 shows a smooth $f$ whose greedy max is discontinuous. Convolution with a Gaussian restores smoothness but moves local minima (Example 5.5), which is why the definition truncates at $\psi(x^\star)$ before smoothing. The central difficulty is to obtain second-order information about the smoothed truncated $g_\varepsilon$ while only ever evaluating a computable lower bound $h_\varepsilon$ ; Lemma 7.3 is the step that transfers stationarity from one to the other, and its constants are tight enough that the transfer fails if any hypothesis is weakened.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) and the joint variable lives in WithLp 2 (ℝᵈ × ℝᵈ), so that the Lipschitz-Hessian condition uses the paper's Euclidean norm rather than Lean's sup norm on products. Eigenvalue bounds are quadratic-form bounds on the second Fréchet derivative. Expectations over $N(0,I_d)$ are integrals against stdGaussian, and Gaussian smoothing is the published definition RandomGradFree.Shared.smoothing.

Conventions and readings, each disclosed in the item it affects:

Definition 2.1 is read with the second derivative of $f(x,\cdot)$ along the direction of travel, $\dot\varphi^\top\nabla_y^2f\,\dot\varphi$ , as the paper's proofs use it; "points of differentiability" are interior points.
$d\ge1$ is added to every statement involving $\sqrt d$ or $1/\sqrt{\varepsilon d}$ .
Definition 2.3 requires the Gaussian integrand to be integrable and asserts the first and second derivatives of $\mathcal S$ before bounding them.
Algorithm 1 takes an eigen-oracle with $\lambda\ge\lambda_{\max}-\mu_4$ and its hyperparameters $\delta,\mu_1,\mu_3,\mu_4$ as parameters; each milestone assumes exactly the step-size inequalities its proof uses, with $L_2$ a Lipschitz constant of $\nabla f$ .
Lemma 7.2's (25) carries $+\mu_4$ , as in the proof's (29).
Lemma 7.3 carries $\sigma\le1$ , $\varepsilon\le1$ and $b\ge1$ , which its proof uses; the printed form fails for $\sigma>1$ .

The goal cannot be satisfied through Lean's junk values: a non-integrable truncated greedy max would make $\mathcal S\equiv0$ , and fderiv of a non-differentiable function is $0$ , so Definition 2.3 demands integrability and asserted derivatives, and the supremum defining $g_\varepsilon$ ranges over a set that contains $y$ and is bounded by $b$ .

Not formalized: the algorithmic sentences of Theorem 3.1 (success probability $9/10$ , polynomial oracle complexity), Algorithm 2 and the milestones about its randomized run (Lemma 7.1, Lemma 7.2 (26)–(27), Propositions 7.6, 7.8–7.10), Lemma 5.1, Corollary 5.2, Appendix A and Appendix B. Algorithm 2 and Propositions 7.8–7.10 are natural follow-up contributions, as is the strongly convex–strongly concave duality-gap bound (Theorem A.1), which reuses this mission's definitions. A complete development needs Gaussian integration by parts in $\mathbb R^d$ , differentiation under the integral for Gaussian convolutions of bounded measurable functions, and concentration of $\|\zeta\|$ for $\zeta\sim N(0,I_d)$ ; all three are reusable beyond this mission.

Selected references

O. Mangoubi, N. K. Vishnoi, Greedy Adversarial Equilibrium: An Efficient Alternative to Nonconvex–Nonconcave Min-Max Optimization, Mathematics of Operations Research, 2025; read as arXiv:2006.12363v4, 2021. https://arxiv.org/abs/2006.12363
C. Jin, P. Netrapalli, M. I. Jordan, What is Local Optimality in Nonconvex–Nonconcave Minimax Optimization?, ICML 2020. https://arxiv.org/abs/1902.00618
C. Daskalakis, S. Skoulakis, M. Zampetakis, The Complexity of Constrained Min-Max Optimization, STOC 2021. https://arxiv.org/abs/2009.09623
Y. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming 108, 2006. https://doi.org/10.1007/s10107-006-0706-8
Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17, 2017. https://doi.org/10.1007/s10208-015-9296-2

9 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

On Policies for Single-Leg Revenue Management with Limited Demand Information: the Valuation Tracking Pricing Policy Is c*(P)-CompetitiveResearch Paper

Motivation

Single-leg revenue management asks how a seller holding $k$ units of a perishable item (seats on one flight leg, rooms for one night) should price or ration them to customers who arrive one at a time. The classical theory assumes a demand forecast. When no forecast is available, a standard robust criterion is competitiveness: an online policy is $c$ -competitive if, on every arrival sequence, its expected revenue is at least $c$ times the revenue of an offline optimum that knows the whole sequence in advance.

Two earlier lines of work found the best possible constant $c^*(\mathcal P)$ for a discrete price set $\mathcal P$ , each in a model that gives the seller more power than posted pricing. Ball and Queyranne (2009) studied booking limits: customers arrive with a fare class that the seller observes before accepting or rejecting. Eren and Maglaras (2010) studied price skimming with a known number of customers. Both show that no online algorithm can be more than $c^*(\mathcal P)$ -competitive. Ma, Simchi-Levi and Teo (arXiv:1810.10900v2; Operations Research 2021) ask whether the same ratio is achievable by dynamic posted pricing, where the seller commits to a price before seeing the customer's valuation and does not know the horizon. Their answer is yes, through a randomized policy built on a new valuation tracking subroutine.

Setting

Fix $m\ge1$ prices $0<r^{(1)}<\dots<r^{(m)}$ and set $r^{(0)}=0$ (no customer) and $r^{(m+1)}=\infty$ (shutting off demand). The firm holds $k\ge1$ units. Customers $t=1,\dots,T$ arrive in order; $T$ is unknown to the firm. Customer $t$ has a deterministic valuation $V_t=r^{(j_t)}$ , $j_t\in\{0,\dots,m\}$ , chosen by an adversary. Before seeing $V_t$ , the firm posts a price $P_t\in\{r^{(1)},\dots,r^{(m+1)}\}$ that may depend only on $V_1,\dots,V_{t-1}$ and the past prices; the customer buys ( $X_t=1$ ) iff $V_t\ge P_t$ . The revenue is $\mathsf{ALG}=\sum_{t=1}^T P_tX_t$ . The offline optimum $\mathrm{OPT}$ is the sum of the $\min\{k,T\}$ largest valuations. An online algorithm is $c$ -competitive if

\mathbb E[\mathsf{ALG}(V_1,\dots,V_T)]\ \ge\ c\cdot \mathrm{OPT}(V_1,\dots,V_T)\qquad\text{for all }T\ge1,\ (V_1,\dots,V_T)\in(\mathcal P\cup\{0\})^T .

Definition 1 sets $q^{(j)}=1-r^{(j-1)}/r^{(j)}$ for $j\in[m]$ , $q=\sum_{j=1}^m q^{(j)}$ and $c^*(\mathcal P)=1/q$ .

Algorithm 1 (valuation tracking). Each unit $i$ carries a level $\ell_{i}\in\{0,\dots,m\}$ (initially $0$ ) and a flag $\mathtt{sold}[i]$ (initially false). Customer $t$ is assigned to a unit $i_t$ of minimal level; let $\ell=\ell_{i_t}$ . If $\mathtt{sold}[i_t]$ is false, the algorithm posts $r^{(p)}$ , $\ell<p\le m$ , with probability $q^{(p)}/\sum_{j=\ell+1}^m q^{(j)}$ ; otherwise it posts $\infty$ . After observing $V_t$ it sets $\ell_{i_t}\leftarrow\max\{\ell,j_t\}$ and marks $i_t$ sold if a sale occurred. The levels $\ell_{i,t}$ and the assignments $i_t$ are deterministic functions of the valuations; only the sold vector $(S_{1,t},\dots,S_{k,t})$ is random.

Formalization targets

Goal: Theorem 1 (p. 14)

\mathbb E[\mathsf{ALG}(V_1,\dots,V_T)]\ \ge\ \frac1q\,\mathrm{OPT}(V_1,\dots,V_T)\quad\text{for every valuation sequence},

i.e. Algorithm 1 is $c^*(\mathcal P)$ -competitive, for every price grid, every inventory $k$ , and every minimal-level tie-break.

Milestones (Appendix B, pp. ec1–ec5)

The remark of §3.3 (p. 13): a unit at level $m$ is sold with probability $1$ , so line 8 is never reached with $\ell_t=m$ .
Lemma EC.1: $\mathbb E[S_{i,t}]=\frac1q\sum_{j=1}^{\ell_{i,t}}q^{(j)}$ .
Lemma EC.2: if $j_t>\ell_{i_t,t-1}$ then $\mathbb E[P_tX_t]=\frac1q\bigl(r^{(j_t)}-r^{(\ell_{i_t,t-1})}\bigr)$ , and $\mathbb E[P_tX_t]=0$ otherwise.
Lemma EC.3: $\sum_{t'=1}^t\mathbb E[P_{t'}X_{t'}]=\frac1q\sum_{i=1}^k r^{(\ell_{i,t})}$ .
$\mathrm{OPT}=\sum_{i=1}^k M^k_i(T)$ , where $M^k(t)$ lists the $k$ largest of $V_1,\dots,V_t$ padded with zeros (Definition EC.2).
Lemma EC.4: $(r^{(\ell_{1,t})},\dots,r^{(\ell_{k,t})})$ is a permutation of $M^k(t)$ .
The closing display of the proof: $\mathrm{OPT}=\sum_{i=1}^k r^{(\ell_{i,T})}=q\cdot\mathbb E[\mathsf{ALG}]$ , the exact-ratio form of Theorem 1.

Significance

Theorem 1 shows that the competitive ratio of single-leg revenue management under public posted pricing with deterministic valuations equals $c^*(\mathcal P)$ , the same constant as for booking limits and for price skimming with a known horizon. The seller loses nothing, in the worst case, by committing to a price before seeing the customer and by not knowing $T$ . The paper builds on Theorem 1 directly: an inventory-state version of Algorithm 1 (Theorem 2), the structural monotonicity of its prices (Theorem 3), and the extension to stochastic valuations (Theorems 4 and 5) all start from it.

The result is proved in the paper. This mission produces a machine-checked version of the full argument of Appendix B: an explicit model of a randomized online pricing policy as a finite Markov chain on the sold vector, the probability invariant of Lemma EC.1, the per-step revenue identity, and the combinatorial fact that the levels of the algorithm track the $k$ largest valuations. None of these has a formal proof on the platform.

Difficulty

The obvious policies fail: booking limits implemented by price, or price skimming with an unknown horizon, lose a constant factor against a single high-value customer who arrives while the price is low (§3.1). The difficulty of Theorem 1 is that the algorithm must earn, in each step, exactly $1/q$ of the increase of $\mathrm{OPT}$ without seeing $V_t$ . In the formal proof the two hard parts are: maintaining Lemma EC.1 as an exact identity on the law of the sold vector (a statement about a distribution on $\{0,1\}^k$ pushed forward through a randomized transition), and Lemma EC.4, a permutation invariant between the level vector and a sorted, zero-padded list, which holds only because each customer is assigned to a unit of minimal level.

Formalization scope

Prices are a function $r:\mathbb N\to\mathbb R$ with hypotheses $r(0)=0$ and $r(j)<r(j+1)$ for $j<m$ ; values above $m$ are never used, and $r^{(m+1)}=\infty$ is encoded as "no offer".
Valuations are indices: a sequence is a list over $\{0,\dots,m\}$ . $T$ is the list length and is never read by the algorithm. Every theorem holds for every list, including the empty one; this is a strengthening of the paper's $T\ge1$ .
Units are $\mathrm{Fin}\,k$ with $k\ge1$ , $m\ge1$ .
Tie-break. Line 4's $\arg\min$ is a selector function on level vectors; theorems quantify over every selector that returns a unit of minimal level.
Randomness. The law of the sold vector is an explicit probability mass function on $\mathrm{Fin}\,k\to\mathrm{Bool}$ , built by one transition per customer. $\mathbb E[P_tX_t]$ is computed from the law after $t-1$ customers and from $V_t$ only, so the price is online. $\mathbb E[\mathsf{ALG}]=\sum_{t=1}^T\mathbb E[P_tX_t]$ .
Line 8. The printed last offer probability ℓt+1/q_tot is a typo; the definition uses $q^{(m)}/q_{\mathrm{tot}}$ , as the text and proofs do. At a unit of level $m$ the step is a rejection; milestone 1 shows this case never matters.
OPT is the offline maximum of $\sum_{t\in S}V_t$ over sets $S$ of at most $k$ customers; $M^k(t)$ is a sorted, zero-padded list.
$q>0$ is not assumed; it follows from $q^{(1)}=1$ .

A trivializing formalization is ruled out: $\mathbb E[\mathsf{ALG}]$ must be computed from the law of Algorithm 1's random prices and purchases, and $\mathrm{OPT}$ as the offline maximum. Defining either through the levels (e.g. $\mathbb E[\mathsf{ALG}]:=\frac1q\sum_i r^{(\ell_{i,T})}$ ) would make the goal true by definition.

The mission covers only Section 3: public pricing with deterministic valuations. The stochastic-valuation algorithms of Section 4 (Theorems 4–5), the continuous-price variant of §5.1, and the structural results (Theorems 2–3, Corollary 1) are not formalized. The finite-distribution machinery (pushing a mass function through a randomized transition, top- $k$ sums of lists) is reusable for other online-algorithm missions. Proofs of the milestones in any order are welcome; Lemma EC.4 is pure combinatorics and independent of the probabilistic milestones.

Selected references

W. Ma, D. Simchi-Levi, C.-P. Teo, On Policies for Single-Leg Revenue Management with Limited Demand Information, Operations Research, 2021; preprint arXiv:1810.10900v2, 2020 (the version cited throughout). https://arxiv.org/abs/1810.10900v2
M. O. Ball, M. Queyranne, Toward Robust Revenue Management: Competitive Analysis of Online Booking, Operations Research 57(4):950–963, 2009.
S. S. Eren, C. Maglaras, Monopoly Pricing with Limited Demand Information, Journal of Revenue and Pricing Management 9(1–2):23–48, 2010.

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Forewarned Is Forearmed? Contingent Sourcing, Shipment Information and Supplier Competition: Contingent Sourcing Makes Both Suppliers Weakly Better Off but Can Make the Buyer Worse OffResearch Paper

Motivation

Firms that source from a low-cost but unreliable supplier often hedge with a second, reliable supplier. A recent development is that buyers can now track a shipment in transit (temperature loggers for perishables, GPS and inspection reports) and learn, before the selling season, whether the cheap order has been damaged. With that information the buyer can wait and place an emergency order with the reliable supplier only when the shipment is spoiled. This is contingent sourcing. The operational value of such information is clear for a buyer facing fixed prices. Lu and Tomlin (MSOM, doi:10.1287/msom.2021.0540; author manuscript SSRN 4260604) ask what happens when the suppliers set their prices strategically, anticipating how the buyer will use the information. Their answer is that shipment information softens the price competition between the suppliers, and the buyer can end up worse off with the information than without it.

The model without shipment information reduces to the model of Shan, Li and Sethi (2022), in which a responsive-pricing retailer sources from competing suppliers facing disruptions; Lu and Tomlin add the Time-1 signal and the emergency price.

Setting

A buyer sells a product at the price $p(q)=m-q$ , with market potential $m>0$ ; with an available quantity $Q$ its revenue is $R(Q)=mQ-Q^2$ for $Q\le m/2$ and $m^2/4$ otherwise. Supplier U has unit cost $c_U$ and delivers successfully with probability $P_1\in(0,1)$ ( $P_0=1-P_1$ ); the buyer pays U only on delivery. Supplier R is reliable with unit cost $c_R$ . Standing assumptions: $0\le c_U\le P_1m$ , $0\le c_R\le m$ .

Timing: at Time 0 the suppliers simultaneously set prices, $w_U$ for U and a regular price $w_R$ and emergency price $w_E\ge w_R$ for R, within the strategy spaces $c_U/P_1\le w_U\le m$ and $c_R\le w_R\le w_E\le m$ . The buyer then orders $Q_U$ and $Q_R$ . At Time 1 it observes a signal $s\in\{B,G\}$ of accuracy $\rho$ : a spoiled shipment shows $B$ with probability $\rho$ , an intact one always shows $G$ . It may then order $Q_E(s)$ from R at price $w_E$ . The buyer maximizes its expected profit (2) over the four nonnegative quantities; its value is the optimum.

Supplier R's payoff is $\pi_R=(w_R-c_R)Q_R+P_B(w_E-c_R)Q_E$ and U's is $\pi_U=(P_1w_U-c_U)Q_U$ , evaluated at the buyer's optimal order (Table 1 of the paper, with footnote 11's tie-break: an indifferent buyer sources contingently). An equilibrium is a Pareto-dominant Nash equilibrium: a Nash equilibrium that no other Nash equilibrium improves for both suppliers. Scenario I is $\rho=1$ (perfect information, contingent sourcing possible); Scenario N is $\rho=0$ (no information). The thresholds are

\psi_2=\frac{P_0m+2c_U/P_1}{P_0+2},\qquad \phi_1=\frac{(1+P_0)m+c_U}{2},\qquad t=m-\frac{P_1m-c_U}{\sqrt{4-P_1+P_1^2}} .

Formalization targets

Goal: Proposition 4(i)–(iii)

For $c_R>\psi_2$ equilibria exist in both scenarios, and for every equilibrium $w^I$ at $\rho=1$ and every equilibrium $w^N$ at $\rho=0$ , writing $\pi_B$ for the buyer's value:

\begin{aligned} &c_R\ge\phi_1: && \pi_U(w^I)=\pi_U(w^N),\ \pi_B(w^I)\ge\pi_B(w^N),\ \pi_R(w^I)\ge\pi_R(w^N)\ \text{(strict for } c_R<m),\\ &t<c_R<\phi_1: && \pi_B,\pi_U,\pi_R \text{ all strictly larger at } w^I,\\ &\psi_2<c_R\le t: && \pi_B(w^I)\le\pi_B(w^N)\ (\text{strict for } c_R<t),\quad \pi_U,\pi_R \text{ strictly larger at } w^I. \end{aligned}

The third case is the headline: the buyer loses from information while both suppliers gain.

Milestones

Lemma 1 and Proposition 1 (the buyer's optimal orders), Lemma A.1 (supplier R's best response at $\rho=1$ ), Proposition 2(i) (the equilibria at $\rho=1$ for $c_R>\psi_2$ : contingent sourcing at the prices of Table 2) and Proposition 3(i)–(ii) (the equilibria at $\rho=0$ for $c_R>\psi_3$ : sole sourcing from U or diversification at the prices of Table 3).

Significance

The result separates two effects of shipment information: the operational value of reacting to spoilage, and a strategic effect, since the option of a later emergency order lets supplier U raise its price without losing the buyer. The interval $(\psi_2,t]$ is where the second effect dominates. The managerial reading in the paper is that a buyer should make sure the unreliable supplier is cost-efficient enough relative to the reliable one before investing in monitoring.

The mission produces a machine-checked version of the equilibrium analysis of a two-supplier pricing game with a discontinuous buyer response. The paper's results are proved on paper only; nothing in this model is formalized elsewhere. The formal statements also fix a reading of the printed results where the printing is wrong: Proposition 2(ii), Proposition 4(iv) and Lemma A.2(ii)–(iii) of the paper are false as printed (see below), and the mission states only the parts that hold.

Difficulty

The buyer's response is piecewise: four ordering regimes, with boundaries $w_R=w_U$ , $w_R=\eta_1$ and $w_R=\eta_2$ , and the suppliers' payoffs jump across them. Best responses therefore are not first-order conditions of a smooth payoff; each supplier compares the best interior price in each regime with limit prices that push the buyer to a regime boundary. At $\rho=1$ the boundary between contingent sourcing and diversification is a tie for the buyer, and the equilibrium (i-b) exists only because of the tie-break. The selection of Pareto-dominant equilibria adds a further layer: at $\rho=1$ there is a continuum of Nash equilibria (lower $w_U$ with the same R-payoff), and the goal quantifies over all undominated ones. A natural first idea, comparing the closed-form Table 2 and Table 3 payoffs, proves the inequalities only for those particular profiles; the goal also needs that every equilibrium has those payoffs, which is Propositions 2(i) and 3(i)–(ii).

Formalization scope

Everything is real-valued and deterministic: yield and signal enter only through $P_1$ , $P_B=P_0\rho$ , $P_G=1-P_0\rho$ and the posteriors $P_{0G},P_{1G}$ , with $P_{0B}=1$ , $P_{1B}=0$ . The accuracy $\rho$ is an argument; the literals $1$ and $0$ give the two scenarios, and Proposition 3 is the same game at $\rho=0$ . Parameters are a structure Params with a Standing predicate ( $0<m$ , $0<P_1<1$ , $0\le c_U\le P_1m$ , $0\le c_R\le m$ ; the nonnegativity of $m$ and the costs is implicit in the paper). The buyer's value is sSup of (2) over feasible orders, which is meaningful at nonnegative prices, in particular at every equilibrium. The buyer's response in the payoffs is Table 1 by case in the order (iv), (i) with $\eta_1\le w_R$ , (ii), (iii), which is footnote 11's tie-break. Pareto dominance is weak dominance, as in the proof of Proposition 2. Lemma 1 and Proposition 1 add nonnegative $w_U,w_R$ and $0\le\rho\le1$ .

Departures from the printed statements, all disclosed in the items:

Proposition 4 is stated weakly at three endpoints where the printed strict claims fail ( $c_R=m$ : R and the buyer tie; $c_R=\phi_1$ : U is unaffected, covered by case (i); $c_R=t$ : the buyer ties).
Proposition 4(iv), Proposition 2(ii) and Lemma A.2(ii)–(iii) are false and omitted. Counterexample: $m=10$ , $P_1=1/2$ , $c_U=0$ , $c_R=3/2<\psi_2=2$ . At $\rho=1$ the profile $(w_U,w_R,w_E)=(3/2,29/8,23/4)$ is an equilibrium (the buyer is contingent at the tie $\eta_1=w_R$ ) with payoffs U $51/16$ , R $289/64$ , alongside the diversification equilibrium $(13/7,26/7,\cdot)$ with payoffs U $169/98$ , R $961/196$ , which is the unique equilibrium at $\rho=0$ . Neither dominates the other, so contingent sourcing does change payoffs below $\psi_2$ .

Trivializing formalizations are ruled out: the payoffs and equilibria are defined from the game, not from the Table 2/3 profiles; the goal quantifies over all equilibria and asserts their existence, so it is neither a statement about closed forms nor vacuous; R chooses $w_E$ freely; and the strategy spaces are exactly those of p. 16.

All objects live in one definitions file, ContingentSourcing.Competition.Model. Proofs of any milestone are welcome, as are proofs of the omitted Proposition 2(iii) and Proposition 3(iii). A reusable byproduct would be lemmas on piecewise-quadratic two-stage newsvendor-type programs with linear demand.

Selected references

T. Lu and B. Tomlin, Forewarned Is Forearmed? Contingent Sourcing, Shipment Information and Supplier Competition, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2021.0540 (author manuscript: https://ssrn.com/abstract=4260604)
B. Tomlin, On the value of mitigation and contingency strategies for managing supply chain disruption risks, Management Science 52(5), 2006. https://doi.org/10.1287/mnsc.1060.0515
X. Shan, T. Li and S. P. Sethi, A responsive-pricing retailer sourcing from competing suppliers facing disruptions, Manufacturing & Service Operations Management 24(1):196–213, 2022 (cited by the paper for Proposition 3).
V. Babich, A. N. Burnetas and P. H. Ritchken, Competition and diversification effects in supply chains with supplier default risk, Manufacturing & Service Operations Management 9(2), 2007. https://doi.org/10.1287/msom.1060.0122

10 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Probability+1·Captain: mikedeng1

Near-Optimal Bayesian Online Assortment of Reusable Resources: the hybrid simulation-based algorithm is (1 − min{1/2, ε*(c_min)})-competitive against the Bayesian expected LPResearch Paper

Motivation

Rental platforms, cloud computing, hotel and car-rental systems, and on-demand services all sell access to reusable resources: a unit that is rented comes back after a random rental duration and can be rented again. When such a platform displays a menu of products (an assortment) to each arriving customer, it faces an online decision problem: offering a product now earns a fee, but ties up a unit that a later, more valuable customer might have wanted. Feng, Niazadeh and Saberi study this problem in a Bayesian setting, where customer types are drawn from known distributions, and give an algorithm whose expected revenue is within a factor $1 - \min\{1/2, \varepsilon^*(c_{\min})\}$ of an LP upper bound on any online policy (arXiv:2512.06997; Operations Research, 2024). The factor tends to $1$ as the smallest inventory grows and never drops below $1/2$ .

Earlier work on online assortment of reusable resources (Gong, Goyal, Iyengar, Simchi-Levi, Udwani and Wang, Management Science 2021; Goyal, Iyengar and Udwani, arXiv:2002.02430) studied the prior-free, adversarial setting, in which fees and rental-duration distributions are type-independent and identical across time. The Bayesian model here lets both depend on the customer type.

Setting

There are $n$ products; product $i$ has $c_i \ge 1$ identical units, and $c_{\min} = \min_i c_i$ . Customers arrive at times $t = 1, \dots, T$ . Customer $t$ has a type $z_t$ , drawn independently from a known distribution $F_t$ on a finite set. A type $z$ fixes

a choice model $\phi^z(S, i)$ : the probability that a customer of type $z$ rents product $i$ when offered the assortment $S$ (with probability $1 - \sum_{i \in S}\phi^z(S,i)$ she rents nothing);
fees $r^z_i \ge 0$ ;
rental-duration distributions $g^z_i$ on $\{1, \dots, T\}$ ; write $\bar G^z_i(k) = \Pr[d > k]$ .

Assortments come from a family $\mathcal S$ that is downward closed (Assumption 2), and choice models are weakly substitutable (Assumption 1): $\phi^z(\emptyset, i) = 0$ , and adding a product to an assortment never increases the choice probability of another. A rented unit with duration $d$ is unavailable at times $t, \dots, t+d-1$ ; a product with no unit on hand cannot be offered.

The benchmark is the Bayesian expected LP Expected-LP $[\{F_t\}]$ : with $y_{S,t,z}$ the probability of offering $S$ to type $z$ at time $t$ , maximize $\sum_{t,z,S,i} F_t(z)\, r^z_i\, \phi^z(S,i)\, y_{S,t,z}$ subject to each product's inventory holding in expectation at every time, $\sum_{\tau \le t}\sum_{z,S} F_\tau(z)\, \bar G^z_i(t-\tau)\, \phi^z(S,i)\, y_{S,\tau,z} \le c_i$ , and $\sum_S y_{S,t,z} \le 1$ . Let $y^*$ be an optimal solution with $\sum_S y^*_{S,t,z} = 1$ , and

\varepsilon^*(x) = \min_{\gamma \in [0,1]}\ 1 - (1-\gamma)\Big(1 - e^{-\gamma^2 x/(2-\gamma)}\Big).

All algorithms of the paper follow one template: at time $t$ , sample $\hat S \sim y^*_{\cdot,t,z_t}$ ; for each $i \in \hat S$ , discard $i$ if it has no unit on hand and otherwise according to a per-product discarding rule; then offer a random subset of the survivors drawn by sub-assortment sampling (Procedure 1). Algorithm 2 discards at random with probability $\gamma$ . Algorithm 3 keeps $i$ only if its fee exceeds a threshold computed from an optimistic per-unit dynamic program $\mathcal V_{i,t}$ (equation (3)). Sim+Hybrid(i) chooses, product by product, between the two rules by comparing $\mathcal R_i = c_i\mathcal V_{i,1}/(\text{LP contribution of } i)$ with $1 - \varepsilon^*(c_i)$ .

Formalization targets

Goal: Theorem 3

For every instance and every optimal normalized $y^*$ ,

\mathbb E\big[\mathrm{Rev}(\texttt{Sim+Hybrid(i)})\big] \ \ge\ \Big(1 - \min\Big\{\tfrac12, \varepsilon^*(c_{\min})\Big\}\Big)\, \mathrm{LP}(y^*).

Milestones

Proposition 3: sub-assortment sampling returns $\tilde S \subseteq S$ with $\mathbb E[\phi(\tilde S, i)] = p_i$ for every $i \in S$ .
Lemma EC.2: the multiplicative Chernoff bound (already posed on the platform; referenced).
(EC.2): a randomly discarded product has no unit on hand with probability at most $\exp(-\gamma^2 c_i/(2-\gamma))$ .
Per-product bound in the proof of Theorem 1: $\mathbb E[r^{z_t}_i I_{i,t}] \ge (1-\gamma)(1 - e^{-\gamma^2 c_i/(2-\gamma)})\sum_{z,S} F_t(z)\, r^z_i\, \phi^z(S,i)\, y_{S,t,z}$ .
Theorem 1: Algorithm 2 with $\gamma = \gamma^*(c_{\min})$ is $(1 - \varepsilon^*(c_{\min}))$ -competitive.
$\varepsilon^*(x)$ and its minimizers are $O(\sqrt{\log x / x})$ .
Lemma EC.3: the per-unit revenue-to-go of Algorithm 3 from any inventory state is at least $\mathcal V_{i,t}$ .
Part (ii) of the proof of Theorem 2: $c_i \mathcal V_{i,1} \ge \frac12$ (LP contribution of $i$ ).
Theorem 2: Algorithm 3 is $\frac12$ -competitive.
$\varepsilon^*$ is continuous and nonincreasing, $\varepsilon^*(0) = 1$ , $\varepsilon^*(\infty) = 0$ .

Significance

The result gives a single polynomial-time policy that is simultaneously $\frac12$ -competitive, which is optimal for small inventories (a two-period example on p. 17 shows no online policy does better against this LP), and asymptotically optimal as inventories grow. Its analysis is modular: each product is treated separately, which is what allows mixing two discarding rules in one algorithm. Sub-assortment sampling is of independent use whenever an assortment must be thinned without distorting the choice probabilities of the remaining products.

The paper's proofs are on paper only; the per-product decoupling, which the paper invokes in a few lines for Theorem 3, is exactly the kind of step a formal proof makes explicit. A complete development produces a reusable finite model of a Bayesian online rental process (types, simulated assortments, discarding, choices and durations), a verified sub-assortment sampler, and an LP-duality certificate for the optimistic DP. None of these results is formalized elsewhere.

Difficulty

The obvious argument fails at the first step: whether product $i$ is available at time $t$ depends on all earlier rentals, and the offer probabilities of different products are correlated through the shared assortment and through substitution, so rental indicators are neither independent nor product-separable. Two ingredients are needed. Sub-assortment sampling must make each product's selection probability exactly its LP target, whatever happened to the other products; only then can the rentals of product $i$ be coupled with an independent sequence for a concentration bound (EC.2). For small inventories, a concentration bound is too weak, and the analysis instead compares the true process with the optimistic DP by backward induction over inventory states (Lemma EC.3), then bounds the DP against the LP with an explicit dual solution (Part (ii)).

Formalization scope

Everything is finite: products are Fin n (the paper's product $i$ is index $i-1$ ), times are $1, \dots, T$ , types range over one finite type space (the paper's $\mathcal Z_t$ as subsets), and durations lie in $\{1, \dots, T\}$ . The online process is a product of explicit per-step kernels over finite sample paths; probabilities and expectations are finite sums, with no measure theory. Conventions committed to:

$\phi^z(S,\cdot)$ is a sub-probability supported on $S$ for $S \in \mathcal S$ ; weak substitutability is required when $S \cup \{j\} \in \mathcal S$ ; $\mathcal S$ is nonempty and downward closed;
$r \ge 0$ , $c_i \ge 1$ , $n \ge 1$ ;
a unit rented at $\tau$ is out at $t$ iff its duration exceeds $t - \tau$ , matching $\bar G(k) = \Pr[d > k]$ in the LP; $\mathcal V_{i,s} = 0$ for $s > T$ ;
the competitive ratio is $\alpha \cdot \mathrm{LP}(y^*) \le \mathbb E[\mathrm{Rev}]$ for every optimal $y^*$ with $\sum_S y^*_{S,t,z} = 1$ ;
Procedure 1 breaks ties among equal ratios by product index, and its recursive step uses the $j^*$ products of largest ratio;
the page does not say which discarding probability a "large inventory" product uses; it is a minimizer $\gamma^*(c_i)$ of (1) at $x = c_i$ ;
the page calls $\varepsilon^*$ "monotone increasing"; the formalized statement is nonincreasing, which is what the proof uses;
running-time claims are not formalized.

The process is not allowed to rent a unit that is not on hand, the post-processing targets are $\phi^{z}(\hat S, i)$ (not $\phi^z(\bar S, i)$ , which would make sub-assortment sampling the identity), and the path law uses the same $y^*$ as the benchmark; any formalization that drops one of these makes the goal a statement about a different process. Milestones 3, 4, 7 and 8 are stated for any feasible normalized $y$ and arbitrary rules for the other products, which is the generality Theorem 3's proof needs.

Contributions welcome: lemmas on the process (normalization of the path law, the marginal law of one product's rentals), the Chernoff bound, and analytic facts about $\varepsilon^*$ .

Selected references

Y. Feng, R. Niazadeh, A. Saberi, Near-Optimal Bayesian Online Assortment of Reusable Resources, Operations Research (Technical Note), 2024; arXiv:2512.06997v1. https://arxiv.org/abs/2512.06997
V. Goyal, G. Iyengar, R. Udwani, Online Allocation of Reusable Resources: Achieving Optimal Competitive Ratio, arXiv preprint, 2020. https://arxiv.org/abs/2002.02430
V. Goyal, G. Iyengar, R. Udwani, Online Allocation of Reusable Resources via Algorithms Guided by Fluid Approximations, arXiv preprint, 2020 (an idea similar to sub-assortment sampling, found concurrently). https://arxiv.org/abs/2010.03983
H. Chernoff, A Measure of Asymptotic Efficiency for Tests of a Hypothesis Based on the Sum of Observations, Annals of Mathematical Statistics, 1952. https://doi.org/10.1214/aoms/1177729330

15 thms2 active usersReviewed

Analysis Quantum Information Representation Theory·Captain: mikedeng1

The Rate of Optimal Purification procedures: At Output Rate M/N → μ the Optimal All-Qubit Fidelity Tends to 2λ²/(2λ²+μ(1−λ)) for μ ≤ λ and 2λ²/(μ(1+λ)) for μ ≥ λResearch Paper

Motivation

A qubit stored or transmitted in the presence of noise loses purity. If many copies of the same unknown pure state $\sigma = |\varphi\rangle\langle\varphi|$ have each passed through the same noisy channel, one may try to undo the noise collectively: feed the $N$ noisy copies into a quantum device and ask for $M$ output qubits that are as close as possible to $M$ perfect copies $\sigma^{\otimes M}$ . The noise map itself is invertible as a linear map, but its inverse is not completely positive, so this purification problem is a genuine optimization over physical devices, closely related to optimal quantum cloning (Werner 1998, Keyl–Werner 1999).

Cirac, Ekert and Macchiavello (1999) found the optimal device for a single output qubit. Keyl and Werner (arXiv:quant-ph/9910124, 1999) solved the problem for an arbitrary number $M$ of outputs and two figures of merit, and computed the trade-off between output number and quality. For the figure of merit that tests all outputs jointly, the best fidelity is a function of the output rate $M/N$ alone in the limit, and that function is explicit. This mission formalizes that rate formula.

Setting

A qubit is $\mathbb C^2$ with basis $|0\rangle, |1\rangle$ ; $n$ qubits are $(\mathbb C^2)^{\otimes n}$ , with basis indexed by words $x : \{0,\dots,n-1\} \to \{0,1\}$ . Fix a noise parameter $\lambda$ with $0 < \lambda < 1$ . The depolarizing channel acts on a one-qubit density matrix $\sigma$ by

R_*\sigma = \lambda\,\sigma + (1-\lambda)\,\tfrac{1}{2}\mathbb 1 .

A device from $N$ to $M$ qubits is a quantum channel $T_*$ , i.e. a trace-preserving completely positive linear map from $2^N\times 2^N$ to $2^M\times 2^M$ complex matrices. Its all-qubit fidelity is the worst case over pure inputs:

F_{\mathrm{all}}(T) = \inf_{\|\varphi\|=1}\ \operatorname{tr}\Big(\sigma^{\otimes M}\, T_*\big((R_*\sigma)^{\otimes N}\big)\Big), \qquad \sigma = |\varphi\rangle\langle\varphi| .

The optimal all-qubit fidelity is $F^{\max}_{\mathrm{all}}(N,M) = \sup_T F_{\mathrm{all}}(T)$ , the supremum over all channels from $N$ to $M$ qubits. Finally, the rate function is

\Phi(\mu) = \begin{cases} \dfrac{2\lambda^2}{2\lambda^2 + \mu(1-\lambda)} & \mu \le \lambda,\\[2mm] \dfrac{2\lambda^2}{\mu(1+\lambda)} & \mu \ge \lambda. \end{cases}

The proof works with the parametrization $\lambda = \tanh\beta$ , $\beta > 0$ , and with the decomposition of $(\mathbb C^2)^{\otimes N}$ into spin- $s$ blocks, $s \in I[N] = \{N/2, N/2-1, \dots\}\cap[0,\infty)$ . Each block carries a weight $w_N(s)$ (eq. (14)), an explicit probability vector built from $\sinh$ , $\cosh$ and binomial coefficients, and a state $\rho_s(\beta)$ on the symmetric subspace of $2s$ qubits.

Formalization targets

Goal: eq. (10)

For every sequence $N_k \to \infty$ and every sequence $M_k$ with $M_k/N_k \to \mu > 0$ ,

\lim_{k\to\infty} F^{\max}_{\mathrm{all}}(N_k, M_k) = \Phi(\mu).

Milestones

Multiplicities (p. 9). $\sinh\beta\,(2\cosh\beta)^N = \sum_{s\in I[N]}\sinh((2s+1)\beta)\dim\mathcal K_{N,s}$ with $\dim\mathcal K_{N,s} = \frac{2s+1}{N/2+s+1}\binom{N}{N/2-s}$ , and $w_N$ is a probability vector.
Natural purifier block (p. 14). $\operatorname{tr}\rho_s(\beta) = 1$ and $\operatorname{tr}(\sigma^{\otimes 2s}\rho_s(\beta)) = \frac{1-e^{-2\beta}}{1-e^{-(4s+2)\beta}}$ .
Proposition 4.2, corrected (p. 15). The fidelity of one block of the optimal purifier is the closed form $f_{\mathrm{all}}(M,\beta,s)$ .
Theorem 5.1, all-qubit half (p. 15). $F^{\max}_{\mathrm{all}}(N,M) = \sum_{s} w_N(s)\,f_{\mathrm{all}}(M,\beta,s)$ , and the supremum is attained.
Lemma 6.1, corrected (pp. 18–19). $\sum_s w_N(s) f_N(2s/N) \to f_\infty(\lambda)$ for uniformly bounded $f_N$ converging uniformly near $\lambda$ .
Lemma 6.2, corrected (pp. 21–22). $\binom{K}{M}^{-1}\sum_{R=M}^{K}\binom{R}{M}z^{K-R} \to \frac{1}{1-(1-c)z}$ for $|z|<1$ , $M/K \to c \in [0,1]$ .

Significance

The result. Formula (10) says that $\Phi(\mu) < 1$ for every $\mu > 0$ : in the all-qubit sense no purification procedure with a positive output rate approaches perfect fidelity, so optimal purification "works with zero rate". At the same time every fidelity level below one is achieved at a positive rate, and $\Phi$ gives the exact trade-off. This contrasts with the one-qubit figure of merit treated in the same paper, where the fidelity of each output tends to one at any rate. Theorem 5.1 reduces an optimization over all channels between exponentially large spaces to a sum of $\lfloor N/2\rfloor + 1$ explicit terms.

Formalizing it. The results are proved in the paper; none of them, to our knowledge, has a machine-checked proof. The paper's statement of Proposition 4.2 contains printing errors (swapped cases, a missing normalization factor, $f_{\mathrm{one}}$ for $f_{\mathrm{all}}$ ), and Lemmas 6.1 and 6.2 are stated with an incorrect domain and range; the milestones state the corrected versions, which were checked numerically against a semidefinite program for small $N, M$ . A formal proof would certify the corrected formulas. Related platform items, not posed again here: uniqueness of the optimal cloner (Support21.P16.unique_optimal_cloner, open) and covariance averaging for cloners (Renew46.P45.symmetrization, open), both used in the optimality argument of Theorem 5.1.

Difficulty

The obvious route to the goal is to evaluate the fidelity of one good device. That gives only a lower bound: the goal is about the supremum over all channels, and the upper bound requires the optimality theorem (Theorem 5.1), whose proof needs a reduction to covariant, permutation-symmetric channels, the decomposition of tensor-power representations of $SU(2)$ , and the optimality and uniqueness of the cloning maps on each spin block. The asymptotic part is also not a direct substitution: the weights $w_N(s)$ must be shown to concentrate at $2s/N = \lambda$ , and on the side $\mu < \lambda$ the dominant blocks need the binomial-sum branch of $f_{\mathrm{all}}$ , whose limit is Lemma 6.2. Near $\mu = \lambda$ the two branches meet, and the limit must be controlled uniformly in the block index.

Formalization scope

Representation. $n$ -qubit operators are complex matrices indexed by words Fin n → Fin 2; tensor powers are QAlgorithms.piKron; a pure state is QAlgorithms.pureDensity φ with ‖φ‖ = 1; a channel is a superoperator with a finite normalized Kraus family (QAlgorithms.IsChannel), which in finite dimension is exactly a CPTP map. The infimum and supremum are sInf/sSup on ℝ over sets that are nonempty and contained in $[0,1]$ .
Committed conventions. The noise is applied to each input copy before the tensor power, and the target is $\sigma^{\otimes M}$ for the same $\sigma$ . The worst case is over all unit vectors in $\mathbb C^2$ . The supremum is over all channels, not over covariant channels or the paper's purifiers. The goal assumes $0 < \lambda < 1$ and $\mu > 0$ , and the limit is taken along every pair of sequences with $N_k \to \infty$ , $M_k/N_k \to \mu$ . Milestones are stated in $\beta > 0$ with $\lambda = \tanh\beta$ . Spins are encoded by $k = N/2 - s \in \{0,\dots,\lfloor N/2\rfloor\}$ , so $2s = N - 2k \in \mathbb N$ ; $\psi = (1,0)$ is basis vector $0$ .
Ruled out. Fixing the input state to $|0\rangle$ trivializes the problem (the channel that outputs $|0\cdots0\rangle$ has fidelity one); the infimum over all $\varphi$ is essential. Restricting the supremum to symmetric channels would make Theorem 5.1 a different statement.
Infrastructure. A full development needs: Kraus-form channels and their compactness, the symmetric-subspace projector (boseProjector) and the optimal cloner (canonicalCloner), the $SU(2)$ decomposition of $(\mathbb C^2)^{\otimes N}$ with multiplicities, and concentration of the weights $w_N$ . The binomial-sum limit (Lemma 6.2) and the weight concentration (Lemma 6.1) are reusable outside this mission. Contributions of any milestone, or of lemmas toward the $SU(2)$ decomposition, are welcome.

Selected references

M. Keyl, R. F. Werner, The rate of optimal purification procedures, arXiv:quant-ph/9910124v1, 1999; Ann. Henri Poincaré 2 (2001) 1–26. https://arxiv.org/abs/quant-ph/9910124
J. I. Cirac, A. K. Ekert, C. Macchiavello, Optimal purification of single qubits, Phys. Rev. Lett. 82 (1999) 4344. https://arxiv.org/abs/quant-ph/9812075
R. F. Werner, Optimal cloning of pure states, Phys. Rev. A 58 (1998) 1827. https://arxiv.org/abs/quant-ph/9804001
M. Keyl, R. F. Werner, Optimal cloning of pure states, testing single clones, J. Math. Phys. 40 (1999) 3283. https://arxiv.org/abs/quant-ph/9807010

14 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Information Disclosure and Promotion Policy Design for Platforms: Under Myopic Pricing, the Long-Run Average Optimal Consumer Surplus Equals the Concavification of the Best Confounding SurplusResearch Paper

Motivation

Online marketplaces decide which products to show first. A promotion puts a seller's product in front of consumers who will not search further, so it changes both the seller's sales and the surplus of the consumers who see it. A seller who is uncertain about the market sets prices from the sales they observe, and the platform's promotion decisions shape what those sales reveal. Gur, Macnamara, Morgenstern and Saban (arXiv:1911.09256, Management Science 2023) study how a platform that maximizes consumer surplus should combine an initial disclosure of information with a dynamic promotion policy when the seller learns and prices myopically.

The question joins two literatures. Bayesian persuasion (Kamenica and Gentzkow 2011) describes the value of a one-shot signal by the concave envelope of a value function. Learning-and-earning in dynamic pricing (Harrison, Keskin and Zeevi 2012) studies how a seller's beliefs converge when sales are informative. The paper's central result says what the platform can achieve in the long run when it controls both the starting point and the drift of the seller's belief.

Setting

A fraction $\phi\in\{\phi_L,\phi_H\}$ of consumers is impatient, with $0<\phi_L<\phi_H<1$ ; the platform observes $\phi$ and the seller holds the prior $\mu_0=\mathbb P(\phi=\phi_H)$ . The seller sets prices in a compact interval $\mathcal P$ containing $0$ . In each period $t=1,\dots,T$ one consumer arrives. A patient consumer buys with probability $\bar\rho_c(p)$ . An impatient consumer buys with probability $\bar\rho_0(p)$ if the seller is promoted and with probability $0$ otherwise. Consumer surplus is $\bar W_c(p)$ , $\bar W_0(p)$ or $\bar W_{\mathrm{out}}$ in the three cases. The purchase probabilities are decreasing and Lipschitz, the revenues $p\bar\rho_c(p)$ and $p\bar\rho_0(p)$ are strictly concave, $\bar\rho_0\ge\bar\rho_c$ , and $\bar W_c,\bar W_0$ are decreasing and Lipschitz.

Before the first period the platform commits to a signaling mechanism $\sigma$ , a distribution over signals for each value of $\phi$ , and to a promotion policy $\alpha$ , where $\alpha_t(p,\phi,\bar h_t)\in[0,1]$ is the probability of promoting the seller at price $p$ after the history $\bar h_t$ of the signal, past prices and past sales. The seller updates a belief $\mu_t$ about $\phi$ by Bayes' rule and follows a myopic Bayesian pricing policy $\pi^*$ : in each period they choose a price that maximizes the current expected revenue, breaking ties in favour of the current consumer surplus. The platform's payoff is the expected total consumer surplus $W_T^{\alpha,\sigma,\pi^*}(\mu_0)$ .

A promotion policy is confounding if it keeps the seller's belief constant, which requires the probability of a sale to be the same under $\phi_H$ and $\phi_L$ at the price the seller sets. Let $W^C(\mu)$ be the largest one-period expected consumer surplus of a confounding policy at belief $\mu$ , and let $co(W^C)$ be its concavification, the smallest concave function above $W^C$ on $[0,1]$ .

Formalization targets

Goal: Theorem 1

For every prior $\mu_0\in[0,1]$ ,

\lim_{T\to\infty}\ \sup_{\alpha,\sigma}\ \frac1T W_T^{\alpha,\sigma,\pi^*}(\mu_0)=co(W^C)(\mu_0),

and for every $T$ some signal and confounding policy achieve average surplus exactly $co(W^C)(\mu_0)$ . The goal is stated as a uniform upper bound for large $T$ together with exact attainment at every $T$ .

Milestones

Lemma 1 and Proposition 1: under myopic pricing it is without loss to use promotion policies that depend on the history only through the belief, that promote a single price, and two signals.
Proposition 3: for every belief a confounding policy exists.
Lemma 2: a period whose surplus exceeds $co(W^C)(\mu)+\epsilon$ separates the purchase probabilities under $\phi_H$ and $\phi_L$ by some $\delta(\epsilon)>0$ .
Lemma 3: the belief converges to the truth exponentially fast in the number of such periods.
Lemma 4: $co(W^{\max})-co(W^C)$ is bounded by $\epsilon/2+\bar C\mu$ and by $\epsilon/2+\bar C(1-\mu)$ .
Step (a) of (31): beliefs are a martingale and $\mathbb E[co(W^C)(\mu_t)]\le co(W^C)(\mu_0)$ .
The finite-horizon bound $\frac1T W_T<co(W^C)(\mu)+\frac54\epsilon$ for $T>\bar T$ .
The two existence steps: a repeated one-period confounding rule realizes its surplus in every period, and a two-signal mechanism attains $co(W^C)(\mu_0)$ .

Significance

The theorem identifies the long-run value of the platform's joint design problem with a static object. The platform's levers act on the belief process: the signal sets its starting point and the promotion policy its drift. The theorem says that, in the long run, the best use of the second lever is to stop the drift. Information is then disclosed only once, as in a persuasion problem with value function $W^C$ . A consequence is that a policy maximizing the current surplus in every period, which lets the seller learn $\phi$ , is generally not long-run optimal. The paper quantifies the gap on its uniform-willingness-to-pay example. The characterization is also the basis of the paper's later results on approximately optimal policies without signals and on equilibria with a forward-looking seller.

The result is proved in the paper; no part of it has been machine-checked. The formalization produces a finite, measure-free encoding of a dynamic Bayesian game with history-dependent policies, reusable for other learning-and-earning models, and makes the uniformity of every constant explicit.

Difficulty

The obvious argument treats each period separately: the surplus of a period is at most $W^{\max}(\mu_t)$ , and by Jensen's inequality the average is at most $co(W^{\max})(\mu_0)$ . This bound is too weak, because $W^{\max}$ exceeds $W^C$ at interior beliefs. The proof must show that periods whose surplus exceeds $co(W^C)$ by $\epsilon$ cannot recur often. This requires two quantitative statements that hold uniformly over all beliefs, policies and signals: each such period reveals information about $\phi$ by a fixed amount, and beliefs then concentrate exponentially fast. The surplus gained before concentration must also be controlled near the degenerate beliefs. The myopic tie-break makes the one-period problems discontinuous in the policy, so the compactness arguments behind $W^C$ need care.

Formalization scope

The game is encoded without measure theory. The state is a Boolean, the signal set is Fin n for an arbitrary $n$ , pricing policies are deterministic, and the expectation $W_T$ is a finite sum over the state, the signal and the sale outcomes, with path probabilities given by products of the sale probabilities. Beliefs follow Bayes' rule, and a probability-zero observation leaves the belief unchanged. Definitions 1–3 quantify over histories whose recorded prices lie in $\mathcal P$ . The tie-break of Definition 1 uses the current expected surplus under the seller's belief. $W^C$ and $W^{\max}$ are real suprema over one-period rules and myopic responses. $co$ is the supremum over the convex hull of the hypograph restricted to $[0,1]$ and is used only on $[0,1]$ . The standing assumptions add $0\le\bar\rho_c$ and $\bar\rho_0\le1$ , since these are probabilities. Only policies admitting a myopic response are considered, as the paper presumes. Constants in Lemmas 2 and 3 and in the finite-horizon bound are chosen before the horizon, the signal and the policies.

$W^C$ is the one-period version of (10) under myopic pricing with the tie-break, not the static program (11). The goal quantifies over all history-dependent promotion policies, all finite signals and all myopic pricing policies, so it cannot be trivialized by restricting the policy class or stating only the upper bound. The attainment conjunct requires a confounding policy with a myopic response at every history.

The paper asserts that $T\cdot W^C(\mu_1)$ is attained for every $\mu_1$ . Under the tie-break the supremum defining $W^C(\mu_1)$ can fail to be attained, so the corresponding milestone states only the repetition step. Proposition 1 is stated with the prior fixed before the policies are chosen.

A complete development needs Bayesian updating on finite trees, the martingale property and Jensen's inequality for finite mixtures, concave envelopes on an interval and their attainment by two-point splits, Berge-type continuity of constrained one-period optima, and exponential concentration of posteriors under separated likelihoods. The last three are reusable beyond this mission. Contributions to any milestone, and to general lemmas on concave envelopes and posterior concentration, are welcome.

Selected references

Y. Gur, G. Macnamara, I. Morgenstern, D. Saban, Information Disclosure and Promotion Policy Design for Platforms, Management Science, 2023; arXiv:1911.09256v5. https://arxiv.org/abs/1911.09256
E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
J. M. Harrison, N. B. Keskin, A. Zeevi, Bayesian Dynamic Pricing Policies: Learning and Earning Under a Binary Prior Distribution, Management Science 58(3), 2012. https://doi.org/10.1287/mnsc.1110.1426
R. J. Aumann, M. Maschler, Repeated Games with Incomplete Information, MIT Press, 1995. https://mitpress.mit.edu/9780262011471/

13 thms2 active usersReviewed

Combinatorics Group Theory Representation Theory·Captain: mikedeng1

Comparison of Gelfand-Tsetlin Bases for Alternating and Symmetric Groups: The Recursively Defined Vectors u_α Form a Gelfand–Tsetlin Basis of Each Irreducible Representation of A_nResearch Paper

Motivation

A Gelfand–Tsetlin basis of a representation of the last group in a tower $G_1 \subset G_2 \subset \cdots \subset G_n$ is a basis adapted to every restriction at once: each basis vector spans a line that is cut out by the isotypic decompositions at all levels $k = 1, \dots, n$ . When every restriction $G_k \downarrow G_{k-1}$ is multiplicity-free, these lines are canonical, and the basis vectors are indexed by paths in the branching graph. For the symmetric groups, Young's orthogonal form gives such a basis with completely explicit matrices for the simple transpositions (Young, 1932; see Headley, 1996, Theorem 2.1), and the Vershik–Okounkov approach (arXiv:math/0503040) builds the representation theory of $S_n$ around it.

The alternating groups $A_n$ also form a multiplicity-free tower, so their irreducible representations have Gelfand–Tsetlin bases too. Geetha and Prasad (arXiv:1606.04424) write these bases down explicitly inside Young's orthogonal form, so that the Gelfand–Tsetlin bases of $A_n$ and $S_n$ can be compared vector by vector. The branching rules of $A_n$ were known before (Ruff, Algebra Colloquium 2008, Theorem 6.1); the new ingredient is a sign normalisation of the associator that identifies the two halves $V_\lambda^{\pm}$ of a self-conjugate $V_\lambda$ consistently along the whole tower.

Setting

For a partition $\lambda$ of $n$ , $V_\lambda$ is the complex vector space with basis $\{v_T\}$ indexed by the standard Young tableaux $T$ of shape $\lambda$ . Tableaux are written inline row by row, e.g. $[1\,2\,4/3/5]$ . The simple transposition $s_i = (i, i+1)$ acts by Young's formulas (2): if $i$ lies in row $j$ , column $k$ of $T$ and $i+1$ in row $j'$ , column $k'$ , and $r = (k'-j') - (k-j)$ , then $\rho_\lambda(s_i) v_T$ is $v_T$ (same row), $-v_T$ (same column), and otherwise $r^{-1} v_T + \sqrt{1-r^{-2}}\, v_{s_iT}$ . For $\mu \in \lambda^{\downarrow}$ (one box fewer), $V_\mu$ embeds in $V_\lambda$ by $v_T \mapsto v_{T^\lambda}$ , with $n$ written in the new box (4).

For self-conjugate $\lambda = \lambda'$ , the associator $\varphi_\lambda$ is the operator

\varphi_\lambda(v_T) = i^{(n-d(\lambda))/2}\,\epsilon(w_T)\,v_{T'} \qquad (9),

where $T'$ is the transposed tableau, $d(\lambda)$ the number of diagonal boxes, and $\epsilon(w_T)$ the sign of the permutation carrying a fixed reference tableau $T_\lambda$ to $T$ . The reference tableau is chosen through self-conjugate covers $(\mu, \lambda)$ ( $\mu \in \lambda^\downarrow$ , both self-conjugate): the smaller partition gets the row superstandard tableau, and the larger one the same tableau with $n$ added on the diagonal. $V_\lambda^{\pm}$ are the $\pm 1$ eigenspaces of $\varphi_\lambda$ .

Labels $\alpha \in \tilde\Theta(n)$ are non-self-conjugate partitions $\lambda$ , with $V_\alpha = V_\lambda$ , and symbols $\lambda^{\pm}$ for self-conjugate $\lambda$ , with $V_\alpha = V_\lambda^{\pm}$ . Conjugate non-self-conjugate labels are equivalent, $\lambda \sim \lambda'$ . A path $\underline\alpha = (\alpha^{(2)}, \dots, \alpha^{(n)}) \in \tilde{\mathcal S}(\alpha)$ has each $\alpha^{(i)}$ obtained from $\alpha^{(i+1)}$ by removing one box, with equal signs whenever both are self-conjugate. Definition 2 builds a vector $u_{\underline\alpha} \in V_\alpha$ recursively from $u_{(2)} = v_{[1\,2]}$ and $u_{(1^2)} = v_{[1/2]}$ . At each step the previous vector $x$ is embedded by (4), and when the path passes from a non-self-conjugate shape to $\lambda^{\pm}$ it is replaced by $x \pm \varphi_\lambda(x)$ .

Formalization targets

Goal: Theorem 4 (Main Theorem), p. 14

For $n \ge 2$ and $\alpha \in \tilde\Theta(n)$ :

u_{\underline\alpha} \ne 0,\quad u_{\underline\alpha} \in V_\alpha \cap \bigcap_{k=2}^{n-1} \mathrm{Iso}_{A_k}\big(V_{\alpha^{(k)}}\big) \quad\text{for every } \underline\alpha \in \tilde{\mathcal S}(\alpha),

and for any set $R$ of paths ending at $\alpha$ containing one path from each equivalence class,

V_\alpha = \bigoplus_{\underline\alpha \in R} \mathbb C\, u_{\underline\alpha}.

Milestones

Lemma 1 (p. 4): the recursive characterisation of Gelfand–Tsetlin subspaces.
Lemma 2 (p. 6): every associator maps $v_T$ to a multiple of $v_{T'}$ .
§3, (7)–(9) (pp. 7–9): for every partition, reference tableau $T_\lambda$ and scalar $c_{T_\lambda}$ , the map $v_T \mapsto c_{T_\lambda}\epsilon(w_T)v_{T'}$ satisfies (5); the normalised self-conjugate $\varphi_\lambda$ of (9) also satisfies $\varphi_\lambda^2 = \mathrm{id}$ .
Theorem 1 (1)–(2) (p. 9): $V_\lambda \cong V_{\lambda'}$ irreducible on $A_n$ for $\lambda \ne \lambda'$ ; $V_\lambda^\pm$ non-isomorphic irreducibles for $\lambda = \lambda'$ .
Lemma 3 (p. 9): for self-conjugate $\mu \in \lambda^\downarrow$ , the embedding (4) is $A_{n-1}$ -equivariant and maps $V_\mu^{\pm}$ into $V_\lambda^{\pm}$ .
Theorem 2 (p. 10): the branching table of $A_{n-1} \subset A_n$ .
Theorem 3 (p. 12): each equivalence class of paths has $2^{r+1}$ elements.

Significance

The theorem gives closed-form Gelfand–Tsetlin bases for every irreducible representation of every alternating group. Each vector is a combination of Young's orthogonal basis vectors with Gaussian-integer coefficients; Example 2 of the paper shows one with four terms and coefficients $1, i, -1, i$ . The matrices of $A_n$ in this basis then follow directly from Young's formulas. It also shows exactly how the two Gelfand–Tsetlin bases compare: on non-self-conjugate shapes they coincide, and on self-conjugate shapes the $A_n$ -vectors are the $\pm$ -symmetrisations $x \pm \varphi_\lambda(x)$ under the associator.

The result is proved in the paper; nothing about it is formalized. Lean's Mathlib has Young diagrams and the platform has standard tableaux, but there is no Young orthogonal form, no associator, no representation of $A_n$ built from partitions, and no Gelfand–Tsetlin basis for any group. A complete development would give the first machine-checked Gelfand–Tsetlin basis for $A_n$ . Along the way it would give a machine-checked Young orthogonal form with its sign calculus, which is reusable for any later work on symmetric-group representations.

Difficulty

The Gelfand–Tsetlin property is a statement about isotypic components at every level. Checking it needs, at each level, the branching rule and an argument that the recursively built vector lands in the right isotypic component. For non-self-conjugate shapes this is inherited from $S_n$ . The difficulty is the self-conjugate case. A path through two consecutive self-conjugate shapes $\mu^{\pm} \to \lambda^{\pm}$ keeps the sign only if $\varphi_\lambda$ restricts exactly to $\varphi_\mu$ on $V_\mu$ , so the bare existence of an associator for each $\lambda$ , unique up to scalar by Schur's lemma, is not enough. The sign of each $\varphi_\lambda$ has to be fixed coherently along self-conjugate covers, and this is what the choice of $T_\lambda$ and the factor $i^{(n-d(\lambda))/2}$ do. The basis half needs, in addition, the count of how many paths share a geodesic (Theorem 3) and the fact that distinct classes give distinct lines.

Formalization scope

Tableaux. Standard tableaux are the published YoungTableau of QAlgorithms_Papers_Independent_Renew46_P26. Labels are $0, \dots, n-1$ (the paper's entry $i$ is label $i-1$ ) and boxes are 0-based (row, column).
Spaces and operators. $V_\lambda$ is the space of finitely supported functions on standard tableaux of shape $\lambda$ . Young's formulas (2), the embedding (4) and the associator (9) are explicit linear operators. That (2) defines a representation of $S_n$ is the cited [5, Theorem 2.1], not a result of the paper.
Equivariance. " $A_k$ -equivariant" means commuting with every product $\rho(s_i)\rho(s_j)$ , $1 \le i, j \le k-1$ . These products generate $A_k$ , so this is equivalent to $A_k$ -equivariance once (2) defines a representation.
Isotypic subspaces. The $A_k$ -isotypic subspace of type $W$ is the sum of the images of $W$ under all $A_k$ -equivariant linear maps.
Gelfand–Tsetlin vectors. A Gelfand–Tsetlin vector for a path is a nonzero vector of $V_\alpha$ lying in the isotypic subspace of type $V_{\alpha^{(k)}}$ at every level $k$ .
Standing hypothesis. The goal assumes $n \ge 2$ , as the paper's paths start at $\tilde\Theta(2)$ .

Ruled out. The Gelfand–Tsetlin predicate is defined intrinsically through isotypic components. It is never defined as membership in a span of the vectors that Definition 2 produces, and $u_{\underline\alpha}$ is never replaced by a formula that makes Theorem 4 hold by definition.

Not formalized. Corollary 1, the completeness clause of Theorem 1, the bijection clause of Theorem 3, Examples 1–3 and Remarks 1–4.

Solvers will need several pieces of infrastructure:

that Young's formulas satisfy the Coxeter relations;
the sign calculus $c_{s_iT} = -c_T$ for $\epsilon(w_T)$ ;
multiplicity-freeness of $S_n \downarrow S_{n-1}$ in this model;
the passage from generator-wise equivariance to isotypic decompositions.

The Coxeter relations and the sign calculus are reusable beyond this mission. Contributions proving any milestone, or proving that Young's operators define a representation, are welcome.

Selected references

T. Geetha, A. Prasad, Comparison of Gelfand-Tsetlin bases for alternating and symmetric groups, arXiv:1606.04424v2, 2017 (published in Algebras and Representation Theory). https://arxiv.org/abs/1606.04424
P. Headley, On Young's orthogonal form and the characters of the alternating group, Journal of Algebraic Combinatorics 5(2):127–134, 1996.
A. M. Vershik, A. Yu. Okounkov, A new approach to the representation theory of the symmetric groups. II, Journal of Mathematical Sciences 131(2):5471–5494, 2005. https://arxiv.org/abs/math/0503040
O. Ruff, Weight theory for alternating groups, Algebra Colloquium 15(3):391–404, 2008.
A. Young, On quantitative substitutional analysis, Proceedings of the London Mathematical Society 2(1):196–230, 1932.
A. Prasad, Representation Theory: A Combinatorial Viewpoint, Cambridge Studies in Advanced Mathematics 147, Cambridge University Press, 2015.

10 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

On the Learning Benefits of Resource Flexibility: At the Break-Even Cost of Flexibility, the Flexible System Is More Profitable Below a Profit-Margin Threshold and Less Profitable Above ItResearch Paper

Motivation

A firm that sells several products must decide, before demand is known, how much capacity to build. It can build dedicated capacity, one resource per product, or a single flexible resource that can serve any product but costs more per unit. The classical argument for flexibility is risk pooling: one pooled resource absorbs the fluctuations of several demands, as studied by Fine and Freund (1990) and Van Mieghem (1998).

Chod, Markakis and Trichakis (SSRN 3212177, published in Management Science, 2021) identify a second, independent benefit. A firm usually observes its sales, not its demand: when a product stocks out, the firm learns only that demand exceeded capacity. This is demand censoring. Because flexible capacity can be shifted to whichever product is in demand, it stocks out less often for each product, and so the firm learns more about demand from a flexible system than from a dedicated one. When demand is correlated over time, that information is worth money in later periods. The paper calls this the learning benefits of flexibility and asks when they are positive.

To separate learning from pooling, the paper compares the two systems at the break-even cost of flexibility, the unit cost of flexible capacity at which both systems earn the same profit in a single period. Any difference that remains in a two-period model is then due to learning alone (Eq. (14) of the paper).

Setting

There are two products with a common unit price $p$ . Dedicated capacity costs $c$ per unit and flexible capacity costs $c_F$ per unit, with $0 \le c < p$ . The first-period demands $D^1_1, D^1_2$ are independent and each uniform on $[x, x+U]$ , with $x \ge 0$ and $U > 0$ . The profit margin is $(p-c)/p$ .

Static model. With dedicated capacities $\mathbf Q = (Q_1, Q_2)$ , product $i$ sells $\min\{D_i, Q_i\}$ , and the expected profit is $\pi_N(\mathbf Q) = p\,\mathbb E[\min\{D_1,Q_1\} + \min\{D_2,Q_2\}] - c(Q_1+Q_2)$ . With flexible capacity $Q_F$ , product 1 is served first: it sells $S_{F,1} = \min\{D_1, Q_F\}$ and product 2 sells $S_{F,2} = \min\{D_2, Q_F - S_{F,1}\}$ ; the expected profit is $\pi_F(c_F)(Q_F) = p\,\mathbb E[S_{F,1} + S_{F,2}] - c_F Q_F$ . The optimal static profits are

\bar\pi_N = \sup_{\mathbf Q \in \mathbb R^2_+} \pi_N(\mathbf Q), \qquad \bar\pi_F(c_F) = \sup_{Q_F \ge 0} \pi_F(c_F)(Q_F),

and $c_F$ is a break-even cost when $\bar\pi_F(c_F) = \bar\pi_N$ .

Learning. A product that had $q$ units available and demand $d$ reveals $d$ exactly if $d < q$ ; otherwise the firm learns only that $D \ge q$ and conditions its prior on that event. The firm's belief after period 1 is the product of the two products' posteriors. In period 2 demand repeats ( $D^2_i = D^1_i$ ), and both systems build dedicated capacity against the posterior belief $\mathbb G$ , earning

V^2(\mathbb G) = \sup_{\mathbf Q \in \mathbb R^2_+} \mathbb E_{\mathbb G}\big[p\min\{D_1,Q_1\} + p\min\{D_2,Q_2\} - c(Q_1+Q_2)\big].

The two-period optimal profits are

V_N = \sup_{\mathbf Q \in \mathbb R^2_+} \Big(\pi_N(\mathbf Q) + \mathbb E\big[V^2(\mathbb P(\cdot \mid \mathbf S^1_N))\big]\Big), \qquad V_F(c_F) = \sup_{Q_F \ge 0} \Big(\pi_F(c_F)(Q_F) + \mathbb E\big[V^2(\mathbb P(\cdot \mid \mathbf S^1_F))\big]\Big).

Formalization targets

Goal: Proposition 1

Take $x = 0$ . There is a threshold $\zeta \in (0,1)$ such that for all $p, c, U, c_F$ with $0 \le c < p$ , $U > 0$ , $c \le c_F < p$ and $\bar\pi_F(c_F) = \bar\pi_N$ ,

\frac{p-c}{p} \le \zeta \implies V_F(c_F) \ge V_N, \qquad \frac{p-c}{p} > \zeta \implies V_F(c_F) \le V_N.

The goal fixes no numerical value of $\zeta$ ; the paper reports $\zeta \approx 0.5904$ .

Milestones

Lemma 3: the uniform newsvendor optimum $\bar Q = x + U(p-c)/p$ with profit $(p-c)x + \tfrac U2 (p-c)^2/p$ .
The static non-flexible optimum $\bar\pi_N = 2(p-c)x + U(p-c)^2/p$ .
The static flexible optimum $\bar Q_F(c_F)$ , $\bar\pi_F(c_F)$ in the two branches $p \ge 2c_F$ and $p < 2c_F$ .
Eq. (8): the pooling benefits $\bar\pi_F(c_F) - \bar\pi_N$ are strictly decreasing in $c_F$ , and the break-even cost exists and is unique in $[c, p)$ .
The two-period non-flexible optimum: $V_N = 4x(p-c) + U(p-c)^2(3c+2p)/\Delta$ with $\Delta = (p-c)(p+c) + cp$ .
The flexible case $Q_F \ge 2x + U$ : concavity, the right derivative $(-c^2 + cp + p(p-2c_F))/(2p)$ at $2x+U$ , and the price threshold $\tilde p$ .

Significance

Proposition 1 says that learning favours flexibility when margins are low or moderate and favours dedicated capacity when margins are high. Combined with the risk-pooling analysis, it shows that the value of flexibility in a dynamic setting is not captured by static pooling models: a firm choosing a technology by comparing single-period profits misjudges it in both directions, depending on the margin. The comparison at the break-even cost is the cleanest available measurement of the information value of a capacity structure under censored demand.

The paper proves Proposition 1 by computing closed forms of all the value functions and then certifying a polynomial inequality over a semialgebraic parameter set with sum-of-squares methods (p. A8). No machine-checked proof exists. A formalization would replace a computer-algebra certificate whose details are not printed with a checked argument, and would fix the value-function closed forms (milestones 2–6), which the paper derives in a few lines each. The milestones are of independent use: Lemma 3 and the censored-sales posterior are standard in inventory learning models.

Difficulty

The value functions $V_N$ and $V_F(c_F)$ are suprema of first-period profit plus the expectation of a second-period value under a posterior that depends on whether each product stocked out. In the flexible system the capacity left for product 2 depends on product 1's realized demand, so the posterior of product 2 depends on product 1's demand, and the objective $v_F$ splits into regimes with different formulas; it is not concave in general (the paper notes "optimization of non-concave functions", p. 12). The break-even cost is defined implicitly by an equation involving square roots, so the final comparison is between two functions of $(p, c)$ along an implicit curve; the obvious approach of comparing closed forms branch by branch needs a sign certificate for a polynomial system rather than a one-line inequality.

Formalization scope

Everything is real-valued. The uniform prior is $U^{-1}$ times Lebesgue measure on $[x, x+U]$ ; the joint prior is the product measure. The stock-out posterior is Mathlib's conditional measure cond of the prior on $\{D \ge q\}$ , an exact observation is a Dirac measure, and a demand is observed exactly iff it is strictly below the available capacity (p. 9). The joint posterior is the product of the per-product posteriors, which is exact because the observation is a product event given product 1's demand. All optima are real suprema of images over nonnegative capacities, never closed forms. The symmetric case of §3 is built in ( $p_1 = p_2 = p$ , common $c$ , i.i.d. uniform demands), as is $\xi = 0$ (second-period demand equals first-period demand); at $x = 0$ the paper's noise $U[-\xi x, \xi x]$ is zero for every $\xi$ , so the goal loses nothing. Added hypotheses, disclosed in each statement: $U > 0$ , $0 \le c < p$ , $c \le c_F < p$ , and in the goal $0 < \zeta < 1$ .

The values must not be defined by their closed forms or by the paper's case split $j = 1, 2, 3$ ; that would make the goal a statement about polynomials rather than about the Bellman problems.

A complete development needs: integrals of piecewise-linear functions against uniform laws and their products, conditional uniform laws, measurability of the posterior-dependent second-period value, and a sign certificate for the final polynomial comparison. The newsvendor and censored-posterior lemmas are reusable in other inventory-learning models. Contributions are welcome on any milestone, on alternative proofs of the final comparison, and on the regime $j = 3$ of the flexible objective, which the milestones do not cover.

Selected references

J. Chod, M. G. Markakis, N. Trichakis, On the Learning Benefits of Resource Flexibility, SSRN preprint 3212177 (December 6, 2019); published in Management Science, 2021. https://ssrn.com/abstract=3212177, https://doi.org/10.1287/mnsc.2020.3795
C. H. Fine, R. M. Freund, Optimal Investment in Product-Flexible Manufacturing Capacity, Management Science 36(4), 1990. https://doi.org/10.1287/mnsc.36.4.449
J. A. Van Mieghem, Investment Strategies for Flexible Resources, Management Science 44(8), 1998. https://doi.org/10.1287/mnsc.44.8.1071
P. A. Parrilo, Semidefinite programming relaxations for semialgebraic problems, Mathematical Programming 96, 2003. https://doi.org/10.1007/s10107-003-0387-5

10 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Surge Pricing and Its Spatial Supply Response: Within an Attraction Region, Supply Fills the Congestion Bound Outward from the Sink at Locally Optimal Prices Without Loss of RevenueResearch Paper

Spatial pricing on ride-hailing platforms

Ride-hailing platforms change prices by location in real time, and drivers respond by moving. A price increase at one location changes where drivers go, how congested each location becomes, and therefore what every driver earns everywhere else. Besbes, Castro and Lobel, Surge Pricing and its Spatial Supply Response (SSRN 3124571, version of May 17, 2019; later published in Management Science, DOI 10.1287/mnsc.2020.3622), model this as a platform choosing prices over a continuous two-dimensional city, with non-atomic drivers who then relocate in equilibrium. Earlier work on ride-hailing pricing took space into account only in reduced form (e.g. Castillo, Knoepfle and Weyl, EC 2017) or on a finite network (Bimpikis, Candogan and Saban, Operations Research 2019). The platform's problem in this model is an infinite-dimensional optimization problem with equilibrium constraints. The paper's main result, the goal of this mission, characterizes optimal prices and supply locally, inside the regions drivers move into.

This mission formalizes that result from the SSRN preprint of May 17, 2019. Its online appendix contains the proofs, and every page and label cited here refers to it.

Setting

The city $\mathcal C\subseteq\mathbb R^2$ is convex and compact. It carries a finite city measure $\Gamma$ , a finite potential demand measure $\Lambda$ and a finite initial supply measure $\Theta$ , all concentrated on $\mathcal C$ , with $\Lambda,\Theta\ll\Gamma$ . The demand density is $\lambda=d\Lambda/d\Gamma$ , which is positive $\Gamma$ -a.e. At location $y$ the riders' willingness to pay has CDF $F_y$ , strictly increasing on its support $[0,\bar V]$ , with $\bar F_y=1-F_y$ and a continuous, unimodal revenue curve $q\mapsto q\bar F_y(q)$ . The driver receives a fraction $\alpha\in(0,1)$ of each fare.

The platform chooses a measurable price mapping $p:\mathcal C\to[0,\bar V]$ . Drivers relocate according to a flow $\mathcal T$ , a measure on $\mathcal C\times\mathcal C$ with first marginal $\Theta$ and second marginal $\mathcal T_2\ll\Gamma$ . The post-relocation supply is $s^{\mathcal T}=d\mathcal T_2/d\Gamma$ . A driver who ends at $y$ is matched with probability $R=\min\{1,\lambda(y)\bar F_y(p(y))/s^{\mathcal T}(y)\}$ (with conventions at zero supply), earns $U(y,p(y),s^{\mathcal T}(y))=\alpha\,p(y)\,R$ , and pays travel cost $\|y-x\|$ when coming from $x$ . The best utility available from $x$ is the $\Gamma$ -essential supremum

V(x\mid p,\mathcal T)=\operatorname*{ess\,sup}_{y\in\mathcal C}\big(U(y,p(y),s^{\mathcal T}(y))-\|y-x\|\big).

$\mathcal T$ is a supply equilibrium if almost every driver goes to a destination attaining this value. Problem (P2) maximizes $\gamma\int_{\mathcal C}V(x\mid p,\mathcal T)\,s^{\mathcal T}(x)\,d\Gamma(x)$ , with $\gamma=(1-\alpha)/\alpha$ , over price–equilibrium pairs; the paper shows (P2) is equivalent to maximizing platform revenue.

A single location run as a capacitated monopoly with supply $s$ has revenue $R^{loc}_x(s)=\max_{q\in[0,\bar V]}q\min\{s,\lambda(x)\bar F_x(q)\}$ and optimal price $\rho^{loc}_x(s)$ . The congestion function $\psi_x(s)=\alpha R^{loc}_x(s)/s$ , with $\psi_x(0)=\alpha\bar V$ , is the utility per driver at that location. The indifference region of $x$ is $\mathcal{IR}(x)=\{y\in\mathcal C:V(y)-\|y-x\|=V(x)\}$ . The attraction region of $z$ is $A(z\mid p,\mathcal T)=\{x\in\mathcal C:z\in\mathcal{IR}(x)\}$ . The point $z$ is a sink if $A(z)\neq\emptyset$ and $z\notin A(z')$ for every $z'\neq z$ . Along each ray $a$ from $z$ , $X_a(z\mid p,\mathcal T)$ is the last point of $A(z)$ .

Formalization targets

Goal: Theorem 1 (p. 18)

For every feasible $(p,\mathcal T)$ of (P2) and every sink $z$ , there are a feasible $(\hat p,\hat{\mathcal T})$ with at least the same (P2) value, points $r_a\in[z,X_a(z\mid p,\mathcal T)]$ and numbers $s_a\ge0$ , such that on $A(z\mid p,\mathcal T)$

s^{\hat{\mathcal T}}(x)=\begin{cases}\psi_x^{-1}\big(V(z\mid p,\mathcal T)-\|x-z\|\big)&x\in\bigcup_a[z,r_a),\\ s_a&x=r_a,\\0&\text{otherwise},\end{cases}\qquad \hat p(x)=\begin{cases}\rho^{loc}_x(s^{\hat{\mathcal T}}(x))&x\notin\bigcup_a\{r_a\},\\ p_a&x=r_a,\end{cases}

where $U(r_a,p_a,s_a)=V(r_a\mid p,\mathcal T)$ .

Milestones

In order: Lemma 1 (p. 13, $V_B$ is 1-Lipschitz); Lemma A-1 (bounds $[-H,\alpha\bar V]$ on $V_B$ ; $V\ge0$ on the support of $\Gamma$ ); Lemma A-2 (equilibrium utilities); Lemma A-3 ( $\psi_x$ strictly decreasing); Proposition 2 (p. 15, the congestion bound $V(x)\le\psi_x(s^{\mathcal T}(x))$ $\Gamma$ -a.e.); Lemma B-2 (indifference propagates along segments); Lemma B-1 (attraction regions are closed unions of segments $[z,X_a]$ ); Lemma B-3 (positive flow contains an indifferent pair); Proposition B-1 (flow separation at the endpoints and at the sink); Proposition B-2 (pasting a local equilibrium into an attraction region).

Significance

Theorem 1 shows that, within any attraction region, an optimal solution has a simple structure. Supply is filled ray by ray outward from the sink up to the congestion bound, and each location is priced as a local monopolist given its supply. It reduces the platform's infinite-dimensional problem with equilibrium constraints to a choice of one cutoff point per ray. In the paper it is an ingredient of the explicit global solution of the one-dimensional demand-shock family of §8 (Theorem 3).

The result is proved in the paper (Appendix C). None of it has been formalized. A formal proof would check a long measure-theoretic argument (Appendix C, about nine pages) that works with densities, essential suprema and a.e. statements throughout. The milestones are smaller results with short proofs, and are self-contained targets.

Difficulty

The goal is an existence statement over flows, so the new equilibrium $\hat{\mathcal T}$ must be constructed and its equilibrium property checked. Changing supply inside $A(z)$ changes utilities at every location whose drivers could move there. The supply and prices therefore cannot be optimized pointwise and pasted back without controlling flows that cross the boundary of the region. Matching the drivers available in $A(z)$ to the congestion bound along each ray must work for an arbitrary finite $\Gamma$ , which may have atoms or be concentrated on curves. Every density identity holds only $\Gamma$ -a.e., and the region boundaries $\bigcup_a\{X_a\}$ or $\bigcup_a\{r_a\}$ can carry positive measure.

Formalization scope

The plane is EuclideanSpace ℝ (Fin 2). The paper says "a norm", but the ray geometry of Appendix B needs a strictly convex one. Measures are measures on $\mathbb R^2$ concentrated on $\mathcal C$ , and flows are measures on $\mathbb R^2\times\mathbb R^2$ . Densities are Radon–Nikodym derivatives converted to reals, so every pointwise claim about $s^{\mathcal T}$ , $\lambda$ or prices built from them is stated $\Gamma$ -a.e. $V_B$ is the Mathlib essSup with respect to $\Gamma|_B$ ; it is finite under the standing assumptions, so no boundedness hypothesis is added. Rays are indexed by unit vectors.

The standing assumptions of §3.1 are one hypothesis, Market.Standing, of every theorem. It contains: convex compact city; finite measures concentrated on it, with $\Lambda,\Theta\ll\Gamma$ ; $\bar V>0$ ; $0<\alpha<1$ ; $F_y$ a CDF supported on $[0,\bar V]$ and strictly increasing there; continuous, unimodal revenue; $\lambda>0$ $\Gamma$ -a.e.; joint measurability of $(y,q)\mapsto F_y(q)$ . The last assumption and the CDF properties are implicit in the paper and are added openly. A sanity file shows that these assumptions hold for a one-point city.

In Theorem 1, $\psi_x^{-1}(v)$ is written as $\psi_x(s^{\hat{\mathcal T}}(x))=v$ . The supply cases are read in the printed order at the sink. Prices $\rho^{loc}_x$ come from (5), so $\rho^{loc}_x(0)=\bar V$ . In Proposition B-1, the printed $\bigcup_a[z,X_a$ is read as the half-open $\{z\}\cup\bigcup_a[z,X_a)$ used in its proof. Proposition B-2 adds $\Gamma(A)>0$ , the precondition of Definition 3.

Two formalizations would make the goal trivial, and both are excluded. Dropping the equilibrium condition from feasibility would let any flow "dominate". Taking $V$ as a pointwise supremum or $s^{\mathcal T}$ as a free function would decouple the objective from the flow. Feasibility includes Definition 1, $V$ is an essential supremum, and $s^{\mathcal T}$ is the density of the flow.

Contributions welcome: proofs of the milestones, general lemmas on essential suprema of Lipschitz families, and general measure-theoretic results about finite planar measures and rays from a point, which can be reused outside this mission.

Selected references

O. Besbes, F. Castro, I. Lobel, Surge Pricing and its Spatial Supply Response, SSRN 3124571, version of May 17, 2019. https://ssrn.com/abstract=3124571 (published: Management Science, 2021, https://doi.org/10.1287/mnsc.2020.3622)
K. Bimpikis, O. Candogan, D. Saban, Spatial pricing in ride-sharing networks, Operations Research, 2019. https://doi.org/10.1287/opre.2018.1800
J. C. Castillo, D. Knoepfle, G. Weyl, Surge pricing solves the wild goose chase, Proceedings of EC, 2017, pp. 241–242. https://doi.org/10.1145/3033274.3085098
L. Ambrosio, A. Pratelli, Existence and stability results in the L¹ theory of optimal transportation, in Optimal Transportation and Applications, Springer LNM 1813, 2003, pp. 123–160. https://doi.org/10.1007/978-3-540-44857-0_5

12 thms2 active usersReviewed

Algorithmic Game Theory Graph Theory Probability·Captain: mikedeng1

Pure Nash Equilibria and Best-Response Dynamics in Random Games: Best-Response Dynamics Reaches a Pure Nash Equilibrium for All Large N When the Tie Probability Is SmallResearch Paper

Why random games, and why ties

A pure Nash equilibrium (PNE) of a game is a strategy profile from which no player gains by a unilateral deviation. Unlike mixed equilibria, pure equilibria need not exist, and even when they do they can be hard to find: computing an equilibrium is PPAD-complete in general (Daskalakis, Goldberg & Papadimitriou 2009). The simplest learning procedure that searches for a PNE is best-response dynamics (BRD): repeatedly let some player who can strictly improve switch strategy. BRD is guaranteed to stop at a PNE only for special classes such as potential games (Monderer & Shapley 1996); in general it can wander forever inside a trap, the "sink equilibrium" of Goemans, Mirrokni & Vetta 2005.

A way to measure how often these failures occur is to draw the payoffs at random. The classical line of work, from Goldman (1957) and Goldberg, Goldman & Newman (1968) to Powers (1990) and Rinott & Scarsini 2000, studies the number of PNE when the payoffs are i.i.d. with a continuous law, so that ties have probability zero. The number of PNE then has mean one and is asymptotically Poisson. Amiet, Collevecchio, Scarsini & Zhong (2021) drop the continuity assumption. They show that the single parameter governing the asymptotics is the tie probability $\alpha$ , and they relate the game to bond percolation on the hypercube. Their headline result is that, for $N$ binary players and small positive $\alpha$ , BRD started from a fixed profile reaches a PNE with a failure probability that is summable in $N$ .

Setting

There are $N$ players $[N]=\{1,\dots,N\}$ , each with strategies $\{0,1\}$ . A profile is $\boldsymbol s\in\{0,1\}^N$ , and $\mathbf 0=(0,\dots,0)$ . In the random game $\Xi_N$ the payoff of player $i$ at profile $\boldsymbol s$ is $Z^{\boldsymbol s}_i$ , and the family $(Z^{\boldsymbol s}_i)_{i,\boldsymbol s}$ is i.i.d. with a law $\mu$ on $\mathbb R$ that may have atoms. With $Z_1,Z_2$ i.i.d. of law $\mu$ ,

\alpha=\mathsf P(Z_1=Z_2),\qquad \beta=\mathsf P(Z_1<Z_2)=\tfrac{1-\alpha}{2}.

Two profiles that differ only in coordinate $i$ are joined by an edge of the hypercube $\mathscr H_N$ . The edge is oriented from $\boldsymbol s$ to $\boldsymbol t$ when $Z^{\boldsymbol s}_i<Z^{\boldsymbol t}_i$ , and is unoriented when the two payoffs tie; this gives the random partially oriented hypercube $\vec{\mathscr H}^\beta_N$ . The set $\mathscr D(\boldsymbol s)$ of strictly profitable deviations consists of the heads of the arrows leaving $\boldsymbol s$ , and $\boldsymbol s$ is a PNE iff $\mathscr D(\boldsymbol s)=\varnothing$ . BRD, $\mathsf{BR}^{(N)}$ , starts at $\mathbf 0$ and at each step moves to a uniformly random element of $\mathscr D$ of the current profile. It converges to a PNE if $\mathscr D(\mathsf{BR}^{(N)}_k)=\varnothing$ for all large $k$ .

A profile is accessible from $\boldsymbol s$ if an oriented path leads to it, and $\vec{\mathscr L}^{\beta,\mathbf 0}_N$ is the set of profiles accessible from $\mathbf 0$ . A trap is a set of at least two profiles that is strongly connected and that no oriented path leaves. In bond percolation $\mathscr B^\beta_N$ each edge of $\mathscr H_N$ is open independently with probability $\beta$ . Its giant component is the largest open cluster, and its fragment $\mathscr M^\beta_N$ is the set of vertices outside the giant component.

Formalization targets

Goal: Theorem 3.4

If $\alpha>0$ and $\lfloor -1/\log_2(1/2+\alpha/2)\rfloor\le 3$ (equivalently $0<\alpha<2^{3/4}-1\approx0.68$ ), then

\sum_{N=1}^\infty \mathsf P\bigl(\mathsf{BR}^{(N)}\text{ does not converge to a PNE}\bigr)<\infty .

Milestones

Proposition 4.1: a coupling under which the open cluster of $\mathbf 0$ in a percolation $\mathscr B^\beta_N$ equals $\vec{\mathscr L}^{\beta,\mathbf 0}_N$ .
Lemma 4.3: concentration of $\mathsf{card}(\mathscr M^\beta_N)$ around $(2(1-\beta))^N(1+O(N(1-\beta)^N))$ , summably in $N$ , for $\beta\in(0,1/2)$ .
Proposition 4.2, form (4.7): $\sum_N\mathsf P(\mathbf 0\notin\text{giant component})<\infty$ for $\beta\in(0,1/2]$ .
Lemma 4.4: for some $\bar\delta>0$ and all $\delta<\bar\delta$ , summably in $N$ , no Hamming ball of radius $\lceil\delta N\rceil$ contains more than $m_\beta=\lfloor 1/(-\log_2(1-\beta))\rfloor$ profiles outside $\vec{\mathscr L}^{\beta,\mathbf 0}_N$ .
(5.8): $\rho_{\mathsf{TV}}(\mathsf{card}(\mathsf{PNE}(\Xi_N)),\mathsf{Poisson}(2^N(1-\beta)^N))\le K_{1,\alpha}N(1-\beta)^N$ .
Theorem 2.3: a central limit theorem for $\mathsf{card}(\mathsf{PNE}(\Xi_N))$ , centred at $(1+\alpha)^N$ and scaled by $(1+\alpha)^{N/2}$ , with Kolmogorov error $K_\alpha N\max((1+\alpha)/2,(1+\alpha)^{-1/2})^N$ .
(5.13): $\sum_N\mathsf P(\mathsf{card}(\mathsf{PNE}(\Xi_N))<(1+\alpha)^N-(1+\varepsilon)^N(1+\alpha)^{N/2})<\infty$ whenever $1+\varepsilon<(1+\alpha)^{1/2}$ .
Trap reduction: if there is no trap, BRD converges to a PNE with probability one.
(5.29): summably in $N$ , $\vec{\mathscr L}^{\beta,\mathbf 0}_N$ contains a PNE.
(5.24): summably in $N$ , $\vec{\mathscr H}^\beta_N$ contains no trap.

Significance

The theorem shows that the failure of BRD described in the game-theory literature, cycling in a trap, is asymptotically rare when payoffs tie with small positive probability. By Borel–Cantelli there is then a finite random $N^*$ beyond which BRD always reaches a PNE. The threshold $2^{3/4}-1$ is where the expected number of trapping 4-cycles stops being summable. The percolation coupling (Proposition 4.1) is the paper's new tool: it turns questions about accessibility under BRD into questions about clusters of the hypercube, where the results of McDiarmid, Scott & Withers apply. The same coupling yields the paper's phase transition at $\alpha=1/2$ for the accessibility of all PNE (Theorem 3.3, not part of this mission).

The paper results are proved on paper, except for one gap. The paper derives (5.8), and through it Theorem 2.3, from the claim that the number of PNE has the same law as the number of isolated vertices of the percolation. That identity is false: the two laws already differ at $N=2$ . Statement (5.8) and Theorem 2.3 are nevertheless true; (5.8) follows from the Chen–Stein method (Arratia, Goldstein & Gordon 1989). Both are posed here as printed, and a correct proof of them is a contribution in its own right. None of these results has a machine-checked proof.

Difficulty

The obvious argument is a first-moment bound: count expected traps and sum over $N$ . The 4-cycles that are traps alone have expected number of order $N^2((1+\alpha)^4/8)^N$ , summable exactly when $\alpha<2^{3/4}-1$ , but traps can have any size up to $2^N$ , and the number of candidate vertex sets grows far faster than any single-shape first moment decays. Controlling traps of every size requires global information about which profiles BRD can reach from $\mathbf 0$ , and about how the exponentially many PNE sit relative to that set. That information comes from the component structure of percolation on the hypercube at a fixed edge probability, a deep theory (McDiarmid–Scott–Withers) of which nothing is in Mathlib.

Formalization scope

Players are Fin N and profiles are Fin N → Bool; the payoffs of $\Xi_N$ live on Fin N → Profile N → ℝ with the product law gameMeasure μ N. Each $N$ has its own probability space; every target is a per- $N$ bound or a sum over $N$ of per- $N$ probabilities, so no coupling across $N$ is needed. Sums of probabilities are ∑' in ℝ≥0∞ and are required to be ≠ ⊤. The BRD chain is built from the PMF iterates of its one-step kernel. At a PNE, where the page leaves the step undefined, the chain stays put. The probability of non-convergence is then $1-\sup_k\mathsf P(\mathsf{BR}^{(N)}_k\in\mathsf{PNE})$ , averaged with a lower Lebesgue integral. Percolation configurations are Edge N → Bool under a product of Bernoulli laws. " $\mathbf 0$ is not in the giant component" is read conservatively: on a tie for the largest cluster, $\mathbf 0$ counts as outside. Theorem 2.3 and (5.8) assume $N\ge 1$ , as the page's $[N]$ does (both fail at $N=0$ ). Their constants are uniform over all payoff laws with the given $\alpha$ . Lemma 4.3's $O(\cdot)$ is two-sided.

Trivializing encodings are excluded: no probability is a Bochner integral of a possibly non-measurable integrand, convergence is not defined by fiat, and a trap needs at least two vertices and closedness, so a single PNE is not a trap. The hypothesis (3.8) is kept literally. At $\alpha=1$ it holds through Lean's $-1/0=0$ , but the goal is then true for a genuine reason (every profile is a PNE).

A complete development needs the theory of finite Markov chains (absorption), Poisson approximation by Chen–Stein, a Berry–Esseen bound, and the component structure of percolation on the hypercube. The last of these is reusable well beyond this mission. Contributions of independent pieces, such as the trap reduction or the first-moment bounds, are welcome.

Selected references

B. Amiet, A. Collevecchio, M. Scarsini, Z. Zhong, Pure Nash Equilibria and Best-Response Dynamics in Random Games, Mathematics of Operations Research 46(4), 2021; arXiv:1905.10758v4. https://arxiv.org/abs/1905.10758
C. McDiarmid, A. Scott, P. Withers, The component structure of dense random subgraphs of the hypercube, arXiv:1806.06433, 2018 (cited by the paper as 2020). https://arxiv.org/abs/1806.06433
R. Arratia, L. Goldstein, L. Gordon, Two moments suffice for Poisson approximations: the Chen–Stein method, Annals of Probability 17(1), 1989. https://doi.org/10.1214/aop/1176991491
Y. Rinott, M. Scarsini, On the number of pure strategy Nash equilibria in random games, Games and Economic Behavior 33(2), 2000. https://doi.org/10.1006/game.1999.0775
M. Goemans, V. Mirrokni, A. Vetta, Sink equilibria and convergence, FOCS 2005. https://doi.org/10.1109/SFCS.2005.68
D. Monderer, L. S. Shapley, Potential games, Games and Economic Behavior 14(1), 1996. https://doi.org/10.1006/game.1996.0044

15 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Linear Optimization+1·Captain: mikedeng1

Fully Polynomial-Time Approximation Schemes for Fair Rent Division: Algorithm 1 on the Slope-Rounded Instance Halts in Polynomially Many Iterations with an ε-Envy-Free SolutionResearch Paper

Fair rent division beyond quasilinear utilities

Housemates who share a house must decide who gets which room and how the total rent is split. A solution pairs an assignment of rooms to agents with a rent for each room, and it is envy-free if no agent prefers another room at that room's rent. Envy-free rent division is the textbook example of fair division with money and is the mathematical core of two-sided matching markets with transfers, where an envy-free solution is a competitive equilibrium.

For quasilinear utilities (a room's value minus its rent) envy-free solutions are computed by an assignment problem and a linear program (Aragones, 1995), and this method is in practical use. Real preferences are often not quasilinear: an agent may have a budget, or be less sensitive to rent at low prices. Existence of envy-free solutions for general continuous, decreasing utilities was established by Svensson (1983) and by Alkan, Demange and Gale (1991), whose perturbation lemma lowers the rents of an envy-free solution while keeping it envy-free. Alkan (1989) gave an algorithm that finds an equilibrium in finite time, with no polynomial bound. Arunachaleswaran, Barman and Rathi (arXiv:1807.04163; Mathematics of Operations Research, 2022) give the first fully polynomial-time approximation scheme for continuous, decreasing piecewise-linear utilities. They also show that the exact problem lies in PPAD ∩ PLS.

Setting

There are $n$ agents and $n$ rooms. Agent $a$ 's utility for room $r$ at rent $x\ge0$ is $v_a(r,x)$ , given by a base value $v_a(r,0)$ (of either sign), break points $0=b_1<b_2<\dots<b_t$ and slope magnitudes $\lambda_1,\dots,\lambda_t>0$ , so that $v_a(r,\cdot)$ is continuous, strictly decreasing and linear with slope $-\lambda_i$ on $[b_i,b_{i+1}]$ (the last piece is unbounded). The total number of pieces is $\ell$ , and $\beta$ bounds $|\log\lambda|$ over all slopes. A solution $(\pi,p)$ is a bijection $\pi$ from agents to rooms and a rent vector $p$ . It is envy-free if $v_a(\pi(a),p_{\pi(a)})\ge v_a(r,p_r)$ for all $a,r$ . For $\varepsilon>0$ it is $\varepsilon$ -EF (Definition 2) if every agent with nonnegative utility satisfies $(1+\varepsilon)\,v_a(\pi(a),p_{\pi(a)})\ge v_a(r,p_r)$ for all $r$ , and every agent with negative utility satisfies $v_a(\pi(a),p_{\pi(a)})\ge(1+\varepsilon)\,v_a(r,p_r)$ for all $r$ .

Algorithm 1 works on a modified instance $\hat{\mathcal I}$ : above a threshold $M$ with $v_a(r,M)<v_a(r',0)$ for all $a,r,r'$ , every utility is continued with slope $1$ (equation (1)). It starts from any envy-free solution of $\hat{\mathcal I}$ with all rents at least $M$ . While all rents are positive it (i) takes a maximum-weight perfect matching $\pi^{i}$ of the first-choice graph at $p^{i-1}$ , with the weight of edge $(a,r)$ equal to $\log$ of the current slope of $v_a(r,\cdot)$ ; (ii) sets $p^{i}$ to a minimum-total-rent solution of the linear program that keeps $\pi^i$ envy-free, keeps the rents nonnegative, and keeps them inside the current linear domain (the box of rents between consecutive slope changes, Definition 1).

The approximation scheme rounds every slope up to a power of $(1+\varepsilon)$ , $\bar\lambda=(1+\varepsilon)^{\lceil\log_{1+\varepsilon}\lambda\rceil}$ . Each piece is replaced by two pieces of slopes $\bar\lambda/(1+\varepsilon)$ and $\bar\lambda$ that meet the original function at the piece's end points, after the zero of each utility has been made a break point. The resulting instance is $\bar{\mathcal I}$ .

Formalization targets

Goal: Theorem 2 (p. 9, restated p. 18)

There is a constant $c$ such that for every instance with $n\ge1$ , every $\varepsilon\in(0,1)$ and every admissible threshold $M$ for $\bar{\mathcal I}$ , Algorithm 1 run on $\bar{\mathcal I}$

has a run that halts;
halts in every run after at most

T\le c\,(n+\ell+\beta+1/\varepsilon+1)^c

iterations, whatever Step 2 solution, matchings and LP optima are chosen; 3. outputs rents $p^T\ge0$ such that $(\pi^T,p^T)$ is an $\varepsilon$ -EF solution of the original instance.

The polynomial is left unspecified; the paper's proof gives a small explicit one, and any polynomial establishes the scheme.

Milestones

The proof has two halves. Theorem 1 (p. 9, proof pp. 13–14) is the same statement with "envy-free" in place of " $\varepsilon$ -EF" for any instance whose slopes are already powers of $(1+\varepsilon)$ . It rests on Lemma 16 (quasilinear envy-free allocations are the maximum-weight matchings), Lemma 18 (its multiplicative form), the perturbation Lemma 2, the run invariants Lemmas 3–5 and the per-domain count (3), $|S|\le 6\beta n/\varepsilon$ . Lemma 9 (p. 17) states that every envy-free solution of $\bar{\mathcal I}$ with nonnegative rents is $\varepsilon$ -EF for the original instance, through Lemmas 6–8 on the rounded functions.

Significance

Theorem 2 gives an efficient algorithm for approximately fair rent division under general piecewise-linear utilities: budgets, rent-sensitive valuations and concave utilities. Exact envy-free solutions for this class are only known to lie in PPAD ∩ PLS. Because envy-free solutions are equilibria of unit-demand markets with money, the theorem also yields approximate equilibria for such markets with non-quasilinear utilities. Theorem 1 gives an exact polynomial algorithm whenever slopes are powers of $(1+\varepsilon)$ .

The result is proved in the paper. None of it has been machine-checked: there is no formal model of envy-free rent division, of the perturbation lemma, or of a price-descent algorithm of this kind in Mathlib or on the platform. A complete development would give a checked proof that a fair-division algorithm terminates within a polynomial number of iterations with a fairness guarantee.

Difficulty

Envy-freeness of the output is not the hard part: every iterate of Algorithm 1 is envy-free for $\hat{\mathcal I}$ by construction, and the rounding lemmas are elementary inequalities on single pieces. The difficulty is termination with a polynomial bound. Lowering rents by the perturbation lemma alone need not stop: Alkan gives an instance in which the perturbations do not converge. A bound has to control how many iterations the algorithm spends inside one linear domain and how many domains it visits. The first count fails for arbitrary slopes, where up to $n!$ matchings of distinct weight can occur in one domain; the power-of- $(1+\varepsilon)$ structure is what the rounding provides. The perturbation lemma is also needed in the form of Lemma 2, for every maximum-weight matching of the weighted first-choice graph, not only for one matching it produces. A formal proof must further show that each step can be carried out: the matching exists and each linear program attains its minimum.

Formalization scope

Representation. A utility is a base value and a list of (start, slope) pieces. Standing requires first start $0$ , strictly increasing starts and positive slopes. Agents and rooms are Fin n, allocations are Equiv.Perm (Fin n), rents are real. $\log$ is the natural logarithm. $\beta$ bounds $|\log\lambda|$ and stands in for the bit complexity of the slopes. Base values may be negative.
The run. Algorithm 1 is a predicate on sequences $(\pi^i,p^i)$ . Every choice the pseudocode leaves open (the Step 2 solution, the maximum-weight matching, the LP optimum) is quantified universally in the bound and the output guarantee. Halting means some rent is $\le0$ . Only the number of while-iterations is bounded. The cost of one iteration (computing $\bar{\mathcal I}$ and $M$ , a matching, a linear program) and the bit length of the input are not formalized.
Conventions. Linear-domain boundaries are the break points where some slope actually changes, plus the rent $0$ . Below rent $0$ (used only by Lemma 2, whose rents may be negative) each utility continues its first piece. The paper describes the rounding only for bounded pieces. The unbounded last piece is rounded down to slope $\bar\lambda/(1+\varepsilon)$ ; after the zero split its utility is nonpositive, and this choice keeps Lemmas 6, 7 and 9 true. Lemmas 6 and 9 are stated for nonnegative rents, the paper's convention for solutions. Lemma 7 (d), (e) are stated on the open piece, because the printed closed-interval form fails at an end point equal to the zero of the utility. Lemma 4 and (3) assume the next iteration exists, which the page takes for granted. $n\ge1$ and $\varepsilon\in(0,1)$ are assumed where the paper assumes them.
Ruled out. The goal is about Algorithm 1 run on the explicitly constructed $\bar{\mathcal I}$ . The bare existence of an $\varepsilon$ -EF solution (which follows from exact existence theorems) does not establish it, and the constant $c$ is fixed before the instance.
Infrastructure. Piecewise-linear functions on lists of pieces, assignment duality for permutations (Lemmas 16 and 18) and existence of optima of linear programs over closed sets are reusable beyond this mission. Proofs of any milestone are welcome, and so are independent proofs of Lemma 16 from LP duality.

Selected references

E. R. Arunachaleswaran, S. Barman, N. Rathi, Fully Polynomial-Time Approximation Schemes for Fair Rent Division, arXiv:1807.04163v1, 2018; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1807.04163
A. Alkan, G. Demange, D. Gale, Fair allocation of indivisible goods and criteria of justice, Econometrica 59(4):1023–1039, 1991 (reference [ADG91] of the paper above).
A. Alkan, Existence and computation of matching equilibria, European Journal of Political Economy, 1989 (reference [Alk89]).
E. Aragones, A derivation of the money Rawlsian solution, Social Choice and Welfare 12(3):267–276, 1995 (reference [Ara95]).
L.-G. Svensson, Large indivisibles: an analysis with respect to price equilibrium and fairness, Econometrica 51(4):939–954, 1983 (reference [Sve83]).

14 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Inner Moreau Envelope of Nonsmooth Conic Chance-Constrained Optimization Problems: Optimal Values and Solutions of the Moreau-Regularized Problems Converge to Those of the Original ProblemResearch Paper

Motivation

A chance constraint asks that a random inequality system hold with at least a prescribed probability $p$ . Such constraints appear throughout engineering and energy optimization: reservoir and power-system management, network design, and any decision that must stay feasible against uncertain demand or inflow with high reliability. The function $x\mapsto\mathbb P(\text{constraint holds at }x)$ is called a probability function. It is in general neither convex nor smooth, even when the underlying random inequality is convex in the random vector, and this is what makes chance-constrained problems hard to solve with standard nonlinear-programming methods.

One remedy is to replace the probability function by a regular approximation and to solve a sequence of approximate problems. van Ackooij, Pérez-Aros, Soto and Vilches (arXiv:2301.09803, Mathematics of Operations Research, 2024) propose an inner regularization built from the Moreau envelope of a scalarized constraint function, for conic constraints in infinite-dimensional decision spaces. The approximate feasible sets contain the original one, and the approximate problems have smooth data. A regularization is useful only if solving the approximate problems recovers the original problem in the limit. This mission formalizes that consistency statement, Theorem 5.4 of the paper.

Setting

Let $\mathcal H$ be a separable real Hilbert space (the decision space), $\mathcal Y$ a real Banach space with dual $\mathcal Y^*$ , and $\xi:\Omega\to\mathbb R^m$ a random vector on a probability space $(\Omega,\mathbb P)$ whose law has a density with respect to Lebesgue measure. A continuous map $\Phi:\mathcal H\times\mathbb R^m\to\mathcal Y$ and a nonempty closed convex cone $\mathcal K\subseteq\mathcal Y$ define the probability function

\varphi(x)=\mathbb P\big(\omega:\Phi(x,\xi(\omega))\in-\mathcal K\big).

The conic constraint is scalarized by a convex, weak $^*$ -compact set $\mathcal C\subseteq\mathcal Y^*$ whose generated cone has weak $^*$ closure equal to the positive polar cone $\mathcal K^+=\{v^*:\langle v^*,v\rangle\ge0\ \forall v\in\mathcal K\}$ . A convex, continuously differentiable $h:\mathcal H\to\mathbb R$ is assumed to make every scalarization $(x,z)\mapsto\langle v^*,\Phi(x,z)\rangle+h(x)$ , $v^*\in\mathcal C$ , jointly convex. The supremum function is $S^h_\Phi(x,z)=\sup_{v^*\in\mathcal C}\{\langle v^*,\Phi(x,z)\rangle+h(x)\}$ .

For $\lambda>0$ and $\psi:\mathcal H\to\mathbb R\cup\{+\infty\}$ , the Moreau envelope is $\mathrm e_\lambda\psi(x)=\inf_z\{\psi(z)+\frac1{2\lambda}\|x-z\|^2\}$ . The inner regularization of $\varphi$ is

\varphi_\lambda(x)=\mathbb P\big(\omega:\mathrm e_\lambda S^h_\Phi(x,\xi(\omega))\le h(x)\big),

the envelope being taken on $\mathcal H\times\mathbb R^m$ with the Hilbert norm. For $p\in[0,1]$ put $M(p)=\{x:\varphi(x)\ge p\}$ and $M_\lambda(p)=\{x:\varphi_\lambda(x)\ge p\}$ . Given a proper, convex, lower semicontinuous objective $\psi$ , problem (P) minimizes $\psi$ over $M(p)$ and the regularized problem (Pλ) minimizes $\mathrm e_\lambda\psi$ over $M_\lambda(p)$ , with optimal values $v(P)$ and $v(P_\lambda)$ .

Formalization targets

Goal: Theorem 5.4 (p. 21)

If $\psi$ is moreover coercive and $M(p)\cap\operatorname{dom}\psi\neq\emptyset$ , then

v(P),\ v(P_\lambda)\in\mathbb R\ \ (\lambda>0),\qquad v(P_\lambda)\xrightarrow[\lambda\to0^+]{}v(P),

and for $\lambda_k\to0^+$ and optimal solutions $x_k$ of $(P_{\lambda_k})$ with $x_k\rightharpoonup x_0$ , the point $x_0$ is optimal for (P). If moreover $\operatorname{dom}\psi=\mathcal H$ and $\psi^*$ is Fréchet differentiable on $\operatorname{dom}\partial\psi^*$ , then $x_k\to x_0$ in norm.

Milestones

Proposition 2.1 a), c) (p. 5): $\mathrm e_\lambda g\nearrow g$ as $\lambda\searrow0$ , and $g(x)\le\liminf_k\mathrm e_{\lambda_k}g(x_k)$ for $x_k\rightharpoonup x$ , $\lambda_k\searrow0$ .
Proposition 2.6 (p. 8): $\varphi(x)=\mathbb P(S^h_\Phi(x,\xi)\le h(x))$ .
Theorem 3.1 a), b), d) (p. 9): $\inf_{\lambda>0}\varphi_\lambda=\varphi$ monotonically; $\limsup_k\varphi_{\lambda_k}(x_k)\le\varphi(x)$ ; weak upper semicontinuity of $\varphi$ and $\varphi_\lambda$ .
Proposition 5.1 (p. 19): $M_\lambda(p)\to M(p)$ in the Painlevé–Kuratowski sense, and in the Mosco sense when $h$ is sequentially weakly continuous.

Significance

Theorem 5.4 justifies the regularization as a solution method: optimal values converge, and weak limits of regularized optimal solutions solve the original problem, with strong convergence under a smoothness condition on $\psi^*$ . Combined with the paper's differentiability results for $\varphi_\lambda$ (§4, not part of this mission), it reduces a nonsmooth chance-constrained problem to a sequence of problems with smooth data whose solutions approximate the true ones. The intermediate results (monotone convergence of $\varphi_\lambda$ , the limsup estimate, convergence of feasible sets) are reusable for any analysis of envelope-based approximations of probability functions.

All statements are proved in the paper. None of them, and none of the general facts used (monotone and lower epi-convergence of Moreau envelopes in Hilbert space, Painlevé–Kuratowski and Mosco convergence), has a machine-checked proof on the platform at the time of writing. The mission produces a formal account of the conic scalarization, of the inner regularization, and of the consistency argument.

Difficulty

The obvious approach, "the regularized feasible sets converge, the regularized objectives converge, hence the minima converge", fails in two places. First, the decision space is infinite-dimensional, so bounded minimizing sequences only converge weakly, and the probability function must be controlled along weakly convergent sequences. This requires weak upper semicontinuity of $\varphi$ and a limsup estimate for $\varphi_{\lambda_k}(x_k)$ along weakly convergent $x_k$ , which do not follow from continuity of $\Phi$ . Second, convergence of values needs a liminf inequality for $\mathrm e_{\lambda_k}\psi(x_k)$ along weakly convergent sequences together with Mosco, not merely Painlevé–Kuratowski, convergence of the feasible sets. The probability function is not convex, so the usual convex-analytic route to Mosco convergence is unavailable.

Formalization scope

The Lean development uses H with [InnerProductSpace ℝ H] [CompleteSpace H] [SeparableSpace H], Y a real Banach space with dual StrongDual ℝ Y, and weak $^*$ notions through WeakDual ℝ Y. Extended-valued functions ( $\psi$ , $\mathrm e_\lambda\psi$ , $S^h_\Phi$ , $\psi^*$ , $v(P)$ , $v(P_\lambda)$ ) are EReal-valued, and infima and suprema are taken there, so no default value enters. Probabilities are ℝ≥0∞-valued. The product $\mathcal H\times\mathbb R^m$ carries the ℓ² norm (WithLp 2), as the paper requires. Weak convergence is defined through inner products. The limit $\lambda\to0^+$ is the filter of right neighbourhoods of $0$ for values and positive sequences for solutions and feasible sets.

The definitions file contains $\mathrm e_\lambda$ , $\Gamma_0$ , coercivity, conjugate, subdifferential, Fréchet differentiability of an extended-valued function, weak convergence, sequential weak continuity, Painlevé–Kuratowski and Mosco convergence, the conic setting (9)–(10), $S^h_\Phi$ , $\varphi$ , $\varphi_\lambda$ , $M(p)$ , $M_\lambda(p)$ , $v(P)$ , $v(P_\lambda)$ and optimality for (P) and (Pλ).

Two hypotheses are added to the printed statements, each used by the paper's own proofs: $\mathcal K$ is closed (the bipolar step of Proposition 2.6), and $h$ is sequentially weakly continuous in Theorem 3.1 d) and throughout Theorem 5.4. The second is automatic when $\mathcal H$ is finite-dimensional. Both are disclosed in the statements.

Trivializing readings are excluded: the feasible set meets $\operatorname{dom}\psi$ ; $\psi$ is proper; the envelope uses the Hilbert, not the sup, norm on the product; $S^h_\Phi$ is an extended-real supremum over a nonempty set, not a real supremum with a default value; every $\lambda$ is positive. Item b) of the goal is vacuous only when some regularized problem has no optimal solution, exactly as in the paper.

Contributions welcome: Moreau-envelope convergence in Hilbert space, the bipolar theorem for closed convex cones in Banach spaces, measure-theoretic continuity arguments for $\varphi_\lambda$ , and the existence argument for optimal solutions of (P).

Selected references

W. van Ackooij, P. Pérez-Aros, C. Soto, E. Vilches, Inner Moreau envelope of nonsmooth conic chance constrained optimization problems, Mathematics of Operations Research, 2024; arXiv:2301.09803v1, 2023. https://arxiv.org/abs/2301.09803
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

10 thms2 active usersReviewed

All missions

Herding in Probabilistic Forecasts: The Normal Forecast with the Morris–Shin Mean and Variance a(x−y)²+d Is an Equilibrium, Unique Among Polynomially Bounded ProfilesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1, true part

Milestones

Significance

Difficulty

Formalization scope

Selected references

Envy-Free Division of Multilayered Cakes: For a Prime-Power Number q of Groups with m ≤ q ≤ n, a Feasible Contiguous Group-Birthday Envy-Free Multi-Division by q − 1 Long Knives ExistsResearch Paper

Fair division of layered resources

Setting

Formalization targets

Goal: Theorem 1 (p. 5)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Projectively Self-Concordant Barriers: Projective Self-Concordance with γ = (ν − 2)/√(ν − 1) Is Equivalent to Self-Concordance of the Logarithmically Homogeneous Extension ν(−log t + f(x/t))Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.5

Milestones (Section 2, p. 5)

Significance

Difficulty

Formalization scope

Selected references

Coordinating Project Outsourcing Through Bilateral Contract Negotiations: Bargaining Powers Under Which Each Contract Form Coordinates a Single-Task ProjectResearch Paper

Why contract forms matter in project outsourcing

Setting

Formalization targets

Goal: Proposition 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

If It Is Surely Better, Do It More? Implications for Preferences Under Ambiguity: Ambiguity Aversion Toward an Event Breaks Monotonicity in Optimal Mixtures for c-Linearly Biseparable PreferencesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Sufficiency of Markov Policies for Continuous-Time Jump Markov Decision Processes: The Induced Markov Policy Has State-Action Marginals No Larger than the Policy, Equal When NonexplosiveResearch Paper

Markov policies in continuous-time decision processes

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Single-Loop Algorithm for Decentralized Bilevel Optimization: O(1/K) Stationarity and Consensus Rates of SLDBO without Heterogeneity AssumptionsResearch Paper

Bilevel problems on a network

Setting

Formalization targets

Goal: Theorem 3.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Relaxed Equilibria for Time-Inconsistent Markov Decision Processes: A Relaxed Equilibrium Exists in Discrete Time without Convexity, via Vanishing Entropy RegularizationResearch Paper

Time inconsistency and equilibrium controls

Setting

Formalization targets

Goal: Theorem 2.2

Regularized problem (milestones, in attack order)

Vanishing regularization

Significance

Difficulty