Convex Optimization

Motivation

A robust linear constraint $f(\mathbf u,\mathbf x)\le 0$ for all $\mathbf u\in\mathcal U$ replaces an uncertain parameter $\tilde{\mathbf u}$ by a deterministic uncertainty set $\mathcal U\subseteq\mathbb R^d$. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets directly from data. Their requirement is a probabilistic guarantee: every robust-feasible decision should satisfy the constraint with probability at least $1-\epsilon$ under the true distribution $\mathbb P^*$, and this should hold with probability at least $1-\alpha$ over the sample. The construction runs a statistical hypothesis test, takes its confidence region of distributions, and turns the worst-case Value at Risk over that region into a set.

This mission covers the case where $\mathbb P^*$ may be continuous but its $d$ coordinates are known to be independent and supported in a known box (§5.1 of the paper). The test is the classical Kolmogorov–Smirnov (KS) goodness-of-fit test, applied separately to each marginal. The result is a convex set $\mathcal U^I_\epsilon$ whose support function has a one-dimensional closed form, (19). The set is representable with exponential cones, and a line search over a single multiplier separates over it (Remarks 6–7).

Setting

Let $d\ge 0$ and $N\ge 1$ (the sample size). For each coordinate $i$ we are given points $\hat u^{(0)}_i<\hat u^{(1)}_i<\cdots<\hat u^{(N)}_i<\hat u^{(N+1)}_i$. The interval $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ is the known box containing the support, and $\hat u^{(1)}_i,\dots,\hat u^{(N)}_i$ are the order statistics of the $i$-th coordinates of the data. Let $\Gamma=\Gamma^{KS}\in(0,1)$ be the KS threshold and $0<\epsilon<1$.

• The Value at Risk of $\mathbb P$ in direction $\mathbf v$ is $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^{\mathsf T}\mathbf v\le t)\ge 1-\epsilon\}$.
• The support function of a set is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^{\mathsf T}\mathbf u$.
• The KS region $\mathcal P^{KS}_i$ is the set of Borel probability measures $\mathbb P_i$ on $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ with $\mathbb P_i(\tilde u_i\le\hat u^{(j)}_i)\ge j/N-\Gamma$ and $\mathbb P_i(\tilde u_i<\hat u^{(j)}_i)\le (j-1)/N+\Gamma$ for $j=1,\dots,N$.
• The independent region $\mathcal P^I$ is the set of product measures $\prod_i\mathbb P_i$ with $\mathbb P_i\in\mathcal P^{KS}_i$.
• The vectors $q^L(\Gamma),q^R(\Gamma)\in\Delta_{N+2}$ of (17) are the two boundary distributions of the KS band. With $k=\lfloor N(1-\Gamma)\rfloor$, $q^L$ puts mass $\Gamma$ at $j=0$, mass $1/N$ at $j=1,\dots,k$, and mass $1-\Gamma-k/N$ at $j=k+1$. Its mirror image is $q^R_j=q^L_{N+1-j}$.
• The relative entropy is $D(\mathbf q,\mathbf p)=\sum_jq_j\log(q_j/p_j)$.
• The uncertainty set (18) is

$$\mathcal U^I_\epsilon=\Big\{\mathbf u:\exists\,\theta_i\in[0,1],\ \mathbf q^i\in\Delta_{N+2},\ \sum_{j=0}^{N+1}\hat u^{(j)}_iq^i_j=u_i,\ \sum_{i=1}^dD\big(\mathbf q^i,\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R\big)\le\log(1/\epsilon)\Big\}.$$

Formalization targets

Goal: Theorem 5 (deterministic content)

For every $\mathbf v\in\mathbb R^d$:

$$\mathcal U^I_\epsilon\ \text{is nonempty, convex and compact},\qquad \mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)\ \ \forall\,\mathbb P\in\mathcal P^I,$$ $$\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)=\inf_{\lambda>0}\Big\{\lambda\log(1/\epsilon)+\lambda\sum_{i=1}^d\log\Big[\max\Big(\sum_{j}q^L_je^{v_i\hat u^{(j)}_i/\lambda},\sum_jq^R_je^{v_i\hat u^{(j)}_i/\lambda}\Big)\Big]\Big\}.\tag{19}$$

Milestones, in attack order

1. The Nemirovski–Shapiro bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\lambda\log(1/\epsilon)+\lambda\sum_i\log\mathbb E^{\mathbb P_i}[e^{v_i\tilde u_i/\lambda}]$ for independent, compactly supported marginals.
2. The boundary laws $q^L$, $q^R$ belong to $\mathcal P^{KS}_i$.
3. Theorem EC.2: for monotone $g$, $\sup_{\mathcal P^{KS}_i}\mathbb E[g(\tilde u_i)]=\max(\sum_jq^L_jg(\hat u^{(j)}_i),\sum_jq^R_jg(\hat u^{(j)}_i))$.
4. (16) combined with EC.2: the Value at Risk over $\mathcal P^I$ is at most the expression in (19), for every $\lambda>0$.
5. The Lagrangian dual of $\max\{\mathbf v^{\mathsf T}\mathbf u:\mathbf u\in\mathcal U^I_\epsilon\}$.
6. (EC.6): $\max_{\mathbf q\in\Delta}\{\mathbf c^{\mathsf T}\mathbf q-D(\mathbf q,\mathbf p)\}=\log\sum_jp_je^{c_j}$.
7. (EC.7): the linear optimization over $\theta_i\in[0,1]$ is solved at an endpoint.

Significance

Theorem 5 gives a data-driven uncertainty set for continuous distributions with independent components. Its guarantee is finite-sample, not asymptotic, and its support function costs one line search over $\lambda$ to evaluate. Theorem 1 of the paper shows that $\mathrm{VaR}\le\delta^*$ for all $\mathbf v$ is equivalent to the probabilistic guarantee for nonempty convex compact sets. So the goal certifies that every robust-feasible solution of a constraint concave in $\mathbf u$ satisfies the chance constraint for every distribution the KS tests cannot reject. Theorem EC.2 is a reusable fact about KS bands: monotone expectations are extremized at the band's two boundary distributions.

The result is proved in the paper, but none of it has been formalized. A formal development would supply:

• worst-case expectations over a KS confidence band;
• the finite Gibbs variational identity with possibly vanishing reference masses;
• a Chernoff-type Value-at-Risk bound for product measures;
• a strong-duality statement for an entropy-constrained convex program.

Difficulty

The obvious route to the VaR bound is a union bound over coordinates. It loses a factor of $d$ in $\epsilon$, which is why the paper uses exponential moments and independence instead. The KS region is infinite dimensional, so the inner supremum of (16) is not a finite linear program. Reducing it to the boundary distributions needs the monotonicity of $u\mapsto e^{v_iu/\lambda}$, and a measure-level comparison of distribution functions against the band. The support-function identity needs strong duality for a jointly convex divergence constraint. The duality holds because $\theta_i\mapsto\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R$ is affine and $D$ is jointly convex. The reference vector can have zero entries (when $N(1-\Gamma)$ is an integer, or in the middle of the band), so the Gibbs step must handle vanishing masses.

Formalization scope

• Data and conventions. Coordinates are Fin d. The points are uhat : Fin d → Fin (N + 2) → ℝ with the page's indices $j=0,\dots,N+1$, and the KS constraints run over j : Fin N, which is the page's $j-1$. The order statistics are data. They are ordered, $\hat u^{(0)}_i\le\hat u^{(1)}_i\le\dots\le\hat u^{(N+1)}_i$ (Monotone (uhat i)), as order statistics of a sample in the box are; ties are allowed.
• Standing assumptions. $N\ge1$, $0<\Gamma<1$ and $0<\epsilon<1$.
• Regions. Measures in $\mathcal P^{KS}_i$ are probability measures on $\mathbb R$ carried by the box, and $\mathcal P^I$ consists of the Measure.pi products of such measures, so independence is built in.
• Relative entropy. $D$ carries an explicit finiteness predicate ($q_j>0\Rightarrow p_j>0$), so Lean's log 0 = 0 cannot make an infinite divergence finite.
• Published definitions. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$, and $\delta^*$ is the published RobustMDP.Shared.supportFunction, a real sSup. The goal proves $\mathcal U^I_\epsilon$ nonempty and compact, so $\delta^*$ is never the junk value $0$ of an empty or unbounded set.
• Infima and the multiplier. Infima over $\lambda$ are over $\lambda>0$ and stated with IsGLB. The page's $\lambda\ge0$ gives the same value.
• Criterion form of the guarantee. The guarantee is stated as $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)$ for all $\mathbb P\in\mathcal P^I$. By Theorem 1 (mission I of this series), this criterion is equivalent to the probabilistic guarantee for nonempty convex compact sets.
• Coverage of the test. The statement "with probability at least $1-\alpha$ over the sample" is the coverage of $\mathcal P^I$. It rests on the distribution-free law of the KS statistic (tables) and on combining $d$ tests at level $1-\sqrt[d]{1-\alpha}$. This part is cited, not formalized.
• Ruled out. The VaR inequality is never checked against a $\delta^*$ that sSup collapses to $0$, and the divergence budget is never relaxed by unguarded logarithms.

Contributions are welcome on any milestone. Milestones 1, 3 and 6 are independent of each other and of the rest; the goal follows from milestones 1–7 together with the convex-analytic facts about $\mathcal U^I_\epsilon$.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17(4):969–996, 2006. https://doi.org/10.1137/050622328
• M. A. Stephens, EDF statistics for goodness of fit and some comparisons, J. Amer. Statist. Assoc. 69(347):730–737, 1974. https://doi.org/10.1080/01621459.1974.10480196
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/

Motivation

The conditional logit model is the workhorse of discrete choice analysis in transportation, marketing, labour and industrial organization. McFadden's 1974 chapter derived it from a theory of population choice behaviour and showed how to estimate it by maximum likelihood; this line of work was recognized by his 2000 Nobel Prize in Economic Sciences, awarded for theory and methods of discrete choice analysis. Every applied logit estimation rests on a basic question: does the maximum likelihood estimate exist for the sample at hand? In small samples it may not. When one alternative is always chosen whenever it is available, the likelihood keeps increasing as a parameter tends to infinity, and numerical optimizers report diverging coefficients. This failure is known in the binary case as complete or quasi-complete separation. McFadden's Lemma 3 gives the exact condition, for the multinomial conditional logit model with general alternative sets, under which a maximizer exists.

Timeline. Berkson (1951, 1955) popularized binomial logit; multinomial versions were developed by Gurland (1960), Bloch (1967), Rassam (1971), McFadden (1968) and Theil (1969, 1970). McFadden (1974) stated the existence criterion for the conditional logit likelihood (Lemma 3) together with a quadratic-programming test for it (Lemma 4). Albert and Anderson (1984) later classified separation patterns for binary and multinomial logistic regression, and Haberman (1974) treated existence for log-linear models.

Setting

A choice experiment has $N \ge 1$ trials. Trial $n$ offers an alternative set of $J_n$ alternatives, indexed $i = 1,\dots,J_n$, each described by an attribute vector $z_{in} \in \mathbb{R}^K$ (the values of $K$ specified functions of the individual's and the alternative's characteristics). Trial $n$ is repeated $R_n \ge 1$ times, and alternative $i$ is chosen $S_{in}$ times, so $R_n = \sum_{j} S_{jn}$.

For a parameter $\theta \in \mathbb{R}^K$, with $z_{in}\theta$ the inner product, the selection probabilities are

$$P_{in}(\theta) = \frac{e^{z_{in}\theta}}{\sum_{j=1}^{J_n} e^{z_{jn}\theta}} \qquad (16)$$

and the log-likelihood of the sample is

$$L(\theta) = C - \sum_{n=1}^N \sum_{i=1}^{J_n} S_{in} \log \sum_{j=1}^{J_n} e^{(z_{jn} - z_{in})\theta}, \qquad C = \sum_{n=1}^N \Big[\log R_n! - \sum_{j=1}^{J_n}\log S_{jn}!\Big]. \qquad (18)$$

Write $\bar z_n(\theta) = \sum_i z_{in}P_{in}(\theta)$ for the probability-weighted mean attribute vector of trial $n$.

Axiom 5 (Full Rank). The $\big(\sum_n J_n\big)\times K$ matrix with rows $z_{in} - \bar z_n$ has rank $K$.

Axiom 6. There is no nonzero $\gamma \in \mathbb{R}^K$ with $S_{in}(z_{jn} - z_{in})\gamma \le 0$ for all $i, j = 1,\dots,J_n$ and $n = 1,\dots,N$. Equivalently, no nonzero direction makes every observed choice weakly best in its alternative set.

Formalization targets

Goal: Lemma 3

Under Axiom 5,

$$\big(\exists\, \hat\theta \in \mathbb{R}^K,\ \forall \theta,\ L(\theta) \le L(\hat\theta)\big) \iff \text{Axiom 6}.$$

Milestones

1. Equation (19): the gradient $\partial L/\partial\theta = \sum_n \sum_j (S_{jn} - R_nP_{jn}) z_{jn}$.
2. Equation (20): the Hessian $\partial^2L/\partial\theta\,\partial\theta' = -\sum_n R_n \sum_j (z_{jn} - \bar z_n)'P_{jn}(z_{jn} - \bar z_n)$.
3. $L$ is concave, and every critical point is a global maximizer.
4. A Hessian that is nonsingular everywhere makes $L$ strictly concave with at most one maximizer.
5. Axiom 5 holds at $\theta$ if and only if the Hessian at $\theta$ is negative definite.
6. Necessity: under Axiom 5, a maximizer forces Axiom 6.
7. Equation (21): under Axiom 6, $b(\gamma) = \max_n \max_{i,j} S_{in}(z_{jn}-z_{in})\gamma$ has a positive lower bound $b^*$ on the unit sphere.
8. The bound $L(\theta) - C \le -b^*|\theta|$ for all $\theta$.
9. Sufficiency: Axiom 6 gives a maximizer.

Significance

Lemma 3 tells the practitioner when the conditional logit maximum likelihood estimate exists, before any numerical optimization is attempted. It is a linear-inequality condition on the data alone, so it can be checked by linear or quadratic programming (Lemma 4 of the same paper). The existence of the estimator is also the first step of McFadden's asymptotic theory: Lemma 5 shows that Axiom 6 holds with probability tending to one, and Lemma 6, consistency and asymptotic normality, concerns the estimator whose existence Lemma 3 characterizes. The concavity and Hessian formulas (19)–(20) are the basis of the Newton–Raphson computation of the estimator and of its asymptotic covariance matrix.

The result has been proved since 1974 and is classical. To our knowledge it has no machine-checked proof; Mathlib has no statement about the existence of logit or softmax-regression maximum likelihood estimates. Formalizing it produces a verified existence criterion for the multinomial logit likelihood, verified gradient and Hessian formulas for log-sum-exp likelihoods with repeated observations, and a verified link between full column rank and strict concavity.

Difficulty

The likelihood is concave, and concave functions on $\mathbb{R}^K$ need not attain their supremum. Concavity alone therefore gives nothing, and existence must come from a growth condition. The obvious approach, "the likelihood is bounded above by $C$, hence attains its maximum", fails: $L$ is bounded but can approach its supremum only at infinity, which is exactly the separation case. Sufficiency needs a quantitative rate at which $L$ decreases, uniform over all directions; a direction-by-direction argument does not suffice. Necessity requires strict concavity, which is where Axiom 5 and the requirement that every trial be observed enter. A trial with $R_n = 0$ can supply the rank of Axiom 5 while contributing nothing to $L$, so with such a trial necessity fails. The calculus part, (19)–(20), involves differentiating sums of log-sum-exp terms over dependent index types and identifying the result with a weighted covariance operator.

Formalization scope

• Representation. $\mathbb{R}^K$ is EuclideanSpace ℝ (Fin K), so $|\theta| = (\theta'\theta)^{1/2}$ is the Euclidean norm and $z\theta$ is the inner product ⟪z, θ⟫. Trials are Fin N, alternatives of trial $n$ are Fin (J n), and the counts $S_{in}$ are natural numbers.
• Data structure. The structure Data K bundles $N$, $J$, $z$, $S$ and the standing assumptions $N \ge 1$ and $R_n = \sum_i S_{in} \ge 1$ for every trial; these make the trial and alternative index sets nonempty.
• Axioms 1–4 are built in. The model is the logit form (16) with $v$ linear in $\theta$ (Axiom 4), so "Suppose Axioms 1–5 hold" becomes "Data plus Axiom 5".
• Axiom 5 is read at every $\theta$. The row space of the matrix does not depend on $\theta$.
• Hessian. The Hessian is the Fréchet derivative of the gradient vector field (19), as a continuous linear map.
• The maximizer is global over all of $\mathbb{R}^K$. Neither a local maximizer nor "$L(\hat\theta) \ge L(0)$" is acceptable as the goal; that would make it trivial.
• Infrastructure. Gradients and Hessians of log-sum-exp with dependent finite index types; positive definiteness from full column rank; attainment of the maximum of a coercive continuous function on a finite-dimensional space. The calculus lemmas are reusable for any multinomial logit or softmax likelihood. Missions 4 and 5 of this series reuse the same model. Contributions of general log-sum-exp lemmas, independent of this mission's definitions, are welcome.

Selected references

• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf
• A. Albert and J. A. Anderson, On the existence of maximum likelihood estimates in logistic regression models, Biometrika 71(1), 1984, pp. 1–10. https://doi.org/10.1093/biomet/71.1.1
• S. J. Haberman, The Analysis of Frequency Data, University of Chicago Press, 1974.
• J. Berkson, Maximum likelihood and minimum χ² estimates of the logistic function, Journal of the American Statistical Association 50, 1955, pp. 130–162. https://doi.org/10.1080/01621459.1955.10501255

Motivation

Many problems in optimization, image reconstruction and statistics reduce to the convex feasibility problem: given closed convex sets $A_i$, $i\in I$, find a point of their intersection $R=\bigcap_{i\in I}A_i$. A classical approach is the relaxation method: from the current point, move to the nearest point of one of the sets, and repeat. For Euclidean distance and half-spaces this is the method of Agmon and of Motzkin and Schoenberg (1954); for hyperplanes it is Kaczmarz's method.

L. M. Bregman's 1967 paper replaced the Euclidean distance by an abstract function $D(x,y)$ satisfying six conditions. The resulting D-projections include what are now called Bregman projections, and the paper is the origin of the Bregman divergence $D(x,y)=f(x)-f(y)-\langle\nabla f(y),x-y\rangle$, used today in mirror descent, entropy maximization and the theory of row-action methods (Censor and Zenios, 1997).

The paper proves convergence for two rules for choosing which set to project onto. This mission covers the second one, Theorem 2: always project onto the set that is farthest from the current point in the sense of $D$ (the "remotest-set" or maximal-distance control).

Setting

Let $X$ be a real linear topological space and $(A_i)_{i\in I}$ a family of closed convex subsets of $X$; the index set $I$ is arbitrary and may be infinite. Let $S\subseteq X$ be convex with $S\cap R\ne\emptyset$, and let $D:S\times S\to\mathbb R$ satisfy:

• (I) $D(x,y)\ge0$, with equality if and only if $x=y$;
• (II) for every $i$ and $y\in S$ there is a point $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$, the D-projection of $y$ onto $A_i$;
• (III) $z\mapsto D(z,y)-D(z,P_iy)$ is convex on $A_i\cap S$;
• (IV) $D(y+tz,y)/t\to0$ as $t\to0$;
• (V) for each $z\in R\cap S$ and real $L$, the set $\{x\in S: D(z,x)\le L\}$ is compact;
• (VI) if $D(x^n,y^n)\to0$, $y^n\to y^*\in\overline S$, and $\{x^n\}$ lies in a compact set, then $x^n\to y^*$.

A relaxation sequence starts at $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$; the sequence of indices $(i_n)$ is the control. The control is remotest-set if at every step $i_n$ realizes

$$\max_{j\in I}\ \min_{x\in A_j}D(x,x^n)=\max_{j\in I}D(P_jx^n,x^n).$$

In the Lean development these objects are DConditions A S D P (conditions I–IV and VI), CondV S D ((⋂ j, A j) ∩ S) (condition V), IsRelaxSeq S P i x (in the series' shared namespace BregmanRelax.Cyclic) and IsRemotestControl D P i x (in BregmanRelax.Remotest).

Formalization targets

Goal: Theorem 2 (p. 203)

For every remotest-set control and every relaxation sequence it generates, every limiting point is a common point:

$$x^{n_k}\to x^*\ \Longrightarrow\ x^*\in\bigcap_{i\in I}A_i .$$

Milestones

• Lemma 1 (pp. 201–202): for $z\in A_i\cap S$ and $y\in S$, $D(P_iy,y)\le D(z,y)-D(z,P_iy)$.
• Lemma 2 (p. 202), for any control: (1) the iterates lie in a compact set; (2) $\lim_n D(z,x^n)$ exists for each $z\in R\cap S$; (3) $D(x^{n+1},x^n)\to0$.

Significance

Theorem 2 is the first convergence result for greedy (most-violated-constraint) selection in projection methods with a non-Euclidean distance. Unlike the cyclic Theorem 1 of the same paper, it applies to infinite families of sets, which covers semi-infinite systems of convex inequalities. Lemma 1, the generalized Pythagorean inequality, is the basic estimate for Bregman projections and recurs throughout mirror-descent and row-action analyses; Lemma 2 records the Fejér-type monotonicity of the iterates with respect to $D$.

The results are classical and proved in the paper. To our knowledge they are not formalized in Lean or another proof assistant at this level of generality. The mission produces a machine-checked version of the abstract D-projection framework, with the conditions stated so that the Bregman divergence of §2 of the paper, and the Euclidean distance, are instances.

Difficulty

The obvious argument for Euclidean projections uses Fejér monotonicity and the fact that a bounded sequence in $\mathbb R^p$ has convergent subsequences. Here neither the triangle inequality nor symmetry of $D$ is available, and $X$ need not be normed or finite-dimensional. The remotest-set rule controls only the D-distance $D(P_jx^n,x^n)$ from the iterate to each projection, in that argument order; turning "these distances tend to zero along a subsequence" into "the limit lies in every $A_j$" requires the interplay of conditions V and VI, and it must hold uniformly over a possibly infinite index set.

Formalization scope

Conventions committed to in Lean:

• The D-projection is a fixed map $P:I\to X\to X$; condition II says $P_iy$ is a minimizer over $A_i\cap S$. The paper's misprint in II ("$\min_{z\in A_i\cap S}D(z,x)$", "$i\in T$") is read as $\min D(z,y)$, $i\in I$.
• Condition IV is assumed only as a vanishing right derivative at $y\in S$ in directions $w-y$ with $w\in S$. The paper's IV implies this, so the theorems are at least as strong as the paper's.
• "Compact" in V, VI and Lemma 2 (1) is sequential compactness (the proofs extract convergent subsequences); "the set of elements of $\{x^n\}$ is compact" means all $x^n$ lie in one sequentially compact set.
• "Limiting point" is the limit of a subsequence $x^{\varphi(k)}$ with $\varphi$ strictly increasing.
• The paper assumes that $\max_i\min_{x\in A_i}D(x,y)$ exists for each $y\in S$, so that a remotest-set control exists. The goal is stated for every control with the maximizing property, which covers every choice of maximizer; the existence assumption is therefore not a hypothesis.
• The index type is arbitrary: no finiteness is assumed. No Hausdorff assumption on $X$ is made.
• $D$ is a total function $X\to X\to\mathbb R$, but every condition and every statement only evaluates it on $S\times S$.

A trivializing formalization is ruled out: the hypotheses are jointly satisfiable with a genuine run (in $\mathbb R$ with $D(x,y)=(x-y)^2$, $A_0=[0,1]$, $A_1=[1,2]$, and $x^0=3$), checked locally without sorry, so neither the goal nor the lemmas holds vacuously.

A complete development needs subsequence extraction from sequentially compact sets, one-sided limits of difference quotients, and monotone convergence of real sequences — all available in Mathlib. The D-projection framework, Lemma 1 and Lemma 2 are shared with the cyclic-control mission of the same paper and are reusable for any Bregman-projection algorithm. Proofs of the lemmas, of Theorem 2, and of the instance showing the Euclidean distance satisfies conditions I–VI are welcome.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics 7(3), 200–217, 1967. https://doi.org/10.1016/0041-5553(67)90040-7
• T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6, 393–404, 1954. https://doi.org/10.4153/CJM-1954-038-x
• S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6, 382–392, 1954. https://doi.org/10.4153/CJM-1954-037-2
• Y. Censor and S. A. Zenios, Parallel Optimization: Theory, Algorithms, and Applications, Oxford University Press, 1997, ISBN 978-0-19-510062-4.

Motivation

In stochastic optimization and statistical learning one chooses a parameter $\theta$ from a set $\Theta\subseteq\mathbb R^d$ to make the risk $R(\theta)=\mathbb E_P[\ell(\theta;X)]$ small, having seen only a sample $X_1,\dots,X_n$ from $P$. Generalization bounds suggest trading empirical risk against its standard deviation, but the variance-penalized objective is non-convex even for convex losses. Duchi and Namkoong (arXiv:1610.02581v3) replace it by the robustly regularized risk, the worst-case expected loss over a $\chi^2$-divergence ball around the empirical distribution. This objective is convex whenever $\ell$ is, and it agrees with the variance-penalized objective up to a small error.

When the risk has curvature near its minimizers, empirical risk minimization attains rates faster than $1/\sqrt n$ (Bartlett, Bousquet and Mendelson 2005; Shapiro, Dentcheva and Ruszczyński 2009). Section 4.1 of the paper asks whether minimizers of the robust risk, which carry an extra variance-dependent penalty of order $\sqrt{\rho/n}$, keep these fast rates. Its Theorem 5 answers yes, and does so for approximate minimizers, which is what iterative solvers return.

Setting

A loss $\ell:\mathbb R^d\times\mathcal X\to\mathbb R$ is fixed, with $\ell(\cdot;x)$ convex and $L$-Lipschitz on a convex set $\Theta$ for every $x$, and $\ell(\theta;\cdot)$ integrable. The risk is $R(\theta)=\mathbb E_P[\ell(\theta;X)]$.

For a radius $\rho\ge0$, the $\chi^2$ ball around the empirical distribution $\widehat P_n$ is the set of weight vectors

$$\mathcal P_n=\Big\{p\in\mathbb R^n_+:\tfrac12\|np-\mathbf 1\|_2^2\le\rho,\ \langle\mathbf 1,p\rangle=1\Big\},$$

and the robust risk is $R_n(\theta,\mathcal P_n)=\sup_{p\in\mathcal P_n}\sum_i p_i\,\ell(\theta;X_i)$.

For $\epsilon\ge0$ the $\epsilon$-suboptimal sets of the risk and of the robust risk are

$$S_\star^\epsilon=\{\theta\in\Theta:R(\theta)\le\inf_\Theta R+\epsilon\},\qquad\widehat S_\star^\epsilon=\{\theta\in\Theta:R_n(\theta,\mathcal P_n)\le\inf_\Theta R_n(\cdot,\mathcal P_n)+\epsilon\},$$

with $S_\star=S_\star^0$ the solution set and $\pi_{S_\star}$ the Euclidean projection onto it. The risk satisfies a growth condition of order $\gamma>1$ if, for some $\lambda>0$ and $r>0$,

$$R(\theta)-\inf_\Theta R\ \ge\ \lambda\,\mathrm{dist}(\theta,S_\star)^\gamma\quad\text{whenever }\mathrm{dist}(\theta,S_\star)\le r.\tag{26}$$

The complexity of the problem enters through the localized class $\{x\mapsto\ell(\theta;x)-\ell(\pi_{S_\star}(\theta);x):\theta\in A\}$ and its empirical Rademacher complexity $\mathfrak R_n(A)=\mathbb E_\varepsilon\big[\sup_{\theta\in A}\frac1n\sum_i\varepsilon_i(\ell(\theta;X_i)-\ell(\pi_{S_\star}(\theta);X_i))\big]$, with independent uniform signs $\varepsilon_i\in\{\pm1\}$.

Formalization targets

Goal: Theorem 5 (p. 19)

For $t>0$, $\rho\ge0$, and $0<\epsilon\le\frac12\lambda r^\gamma$ satisfying

$$\epsilon\ge\Big(2\frac{8^\gamma L^\gamma}{\lambda}\Big)^{\frac1{\gamma-1}}\Big(\frac\rho n\Big)^{\frac\gamma{2(\gamma-1)}}\quad\text{and}\quad\frac\epsilon2\ge2\,\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+L\Big(\frac{2\epsilon}\lambda\Big)^{\frac1\gamma}\sqrt{\frac{2t}n},\tag{27}$$ $$\mathbb P\big(\widehat S_\star^\epsilon\subset S_\star^{2\epsilon}\big)\ \ge\ 1-e^{-t}.$$

Milestones, in attack order

1. Localization (p. 44). Under (26), $S_\star^{2\epsilon}$ lies in $\{\theta\in\Theta:\mathrm{dist}(\theta,S_\star)\le(2\epsilon/\lambda)^{1/\gamma}\}$.
2. Theorem 1, upper half of (10) (p. 7). $\sup_{p\in\mathcal P_n}\langle p,z\rangle-\bar z\le\sqrt{2\rho s_n^2/n}$ for every $z\in\mathbb R^n$.
3. Claim E.1 (p. 44). If $\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon}$, the localized deviation $\Delta_n$ plus a variance term reaches $\epsilon$ somewhere on $S_\star^{2\epsilon}$.
4. Display (43) (p. 45). $\mathbb P(\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon})\le\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge\epsilon/2)$.
5. Concentration (p. 45). $\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge2\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+u)\le\exp(-\frac{nu^2}{2L^2}(\frac\lambda{2\epsilon})^{2/\gamma})$.

Significance

The theorem says that the variance penalty implicit in the robust objective does not cost the fast rates available under curvature. The $\rho$-dependent condition in (27) is of order $(\rho/n)^{\gamma/(2(\gamma-1))}$, which for quadratic growth ($\gamma=2$) is $\rho/n$, the same order as the localized complexity term in typical parametric problems. Corollary 4.1 of the paper derives explicit rates of order $\frac dn\log\frac nd+\frac tn+\frac\rho n$ from it for a unique minimizer. The result applies to $\epsilon$-approximate minimizers, so it covers the output of the stochastic-gradient methods used to solve the robust problem.

The result is proved in the paper (Appendix E). None of it is formalized: no statement about growth conditions, localized deviations of a robust objective, or fast rates for robust minimizers is on Prove2Me. A formal proof would check the printed constants, settle the boundary case $\epsilon=0$ (see below), and produce a localization lemma and a reduction from approximate robust minimizers to empirical processes that apply to other estimators.

Difficulty

The obvious argument fails at two points. First, a uniform deviation bound over all of $\Theta$ gives only the $1/\sqrt n$ rate: the speed-up comes from localizing to $S_\star^{2\epsilon}$, which requires transferring the growth condition, assumed only within distance $r$ of $S_\star$, to every $2\epsilon$-suboptimal point by convexity. Second, the robust risk is not an empirical average, so standard comparisons between empirical and population minimizers do not apply. Claim E.1 handles this by moving along the segment from a bad approximate minimizer to its projection, which needs the projection to be preserved along that segment (a normal-cone property of $\pi_{S_\star}$) and the risk to be continuous there. The robust–empirical gap is then controlled by the variance expansion of Theorem 1. The concentration step needs a bounded-differences inequality for a supremum over an uncountable class, together with symmetrization; neither is in Mathlib in this form.

Formalization scope

Parameters live in EuclideanSpace ℝ (Fin d), so norms, distances and projections are Euclidean. The sample is the coordinate process of the product measure $P^{\otimes n}$ on Fin n → X, $n\ge1$, and probabilities are measures of sample sets (the outer measure for a set that is not measurable). The $\chi^2$ ball is the weight-vector form (8). The suboptimal sets are written without infima ($R(\theta)\le R(\theta')+\epsilon$ for all $\theta'\in\Theta$). Each supremum "$\sup\ge c$" is written as "for every $\delta>0$ some $\theta$ reaches $c-\delta$", so no statement relies on the default value of a real supremum. The Rademacher complexity is the published UnderstandingML.rademacher, and its expectation over the sample is assumed integrable, so that it is the true expectation and not the default value $0$ of a Bochner integral. Lipschitz continuity is required on $\Theta$, as printed.

Corrections and presuppositions:

• $\epsilon>0$. The paper prints $0\le\epsilon$. At $\epsilon=0$, $\rho=0$, both conditions of (27) hold, yet for $\ell(\theta;x)=\frac12(\theta-x)^2$ on $\Theta=[-1,1]$ with $X$ uniform on $[-\frac12,\frac12]$ the robust minimizer is the sample mean, which is almost surely not in $S_\star=\{0\}$. The proof divides by $\epsilon$ (p. 45). The goal is stated for $\epsilon>0$.
• $S_\star$ nonempty and closed are assumed. The projection $\pi_{S_\star}$ presupposes them, and Appendix E calls $S_\star$ closed.
• Only the upper half of Theorem 1's (10) is stated; it needs no boundedness of the values.

The constant $\big(2\cdot8^\gamma L^\gamma/\lambda\big)^{1/(\gamma-1)}$ is the printed one; the proof uses a smaller one, which the printed condition implies. The hypotheses $\epsilon>0$, $\gamma>1$ and $\lambda>0$ make every power well defined. A formalization that assumed (26) vacuously, took $\epsilon=0$, or let the Rademacher term be a non-integrable Bochner integral would trivialize the goal; the statements rule these out.

Infrastructure: Euclidean projection onto closed convex sets and its normal-cone characterization (partly in Mathlib), convexity of integral functionals, McDiarmid's bounded-differences inequality, and symmetrization for suprema of empirical processes. The concentration tools and the localization lemma can be reused beyond this mission. Contributions toward McDiarmid's inequality and symmetrization are especially welcome.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT, 2009. https://arxiv.org/abs/0907.3740

Motivation

Many problems in optimization and numerical analysis reduce to finding a point in the intersection of finitely many closed convex sets: solving a system of linear equations or inequalities, reconstructing an image from projections, or finding a feasible point of a convex program. The classical methods for this convex feasibility problem project the current point onto one set at a time, in Euclidean distance: Kaczmarz (1937) for linear equations, Agmon and Motzkin–Schoenberg (1954) for linear inequalities, and the cyclic projection method for general convex sets studied by Gubin, Polyak and Raik (1967).

L. M. Bregman's 1967 paper replaces the Euclidean distance by a general function $D(x,y)$ satisfying a short list of axioms, and shows that the projection method still works. The functions $D(x,y)=f(x)-f(y)-\langle\nabla f(y),x-y\rangle$ built from a strictly convex $f$ are the ones now called Bregman divergences, and the paper is the origin of Bregman projections, of the row-action methods of Censor and collaborators, and indirectly of mirror descent. Its §2 uses the abstract result to solve convex programs with linear constraints by relaxation.

This mission formalizes §1 of the paper for the cyclic control, in which the sets are visited in a fixed round-robin order. A companion mission treats the remotest-set control of Theorem 2, and two further missions treat the convex-programming results of §2.

Setting

Let $X$ be a real linear topological space and $A_0,\dots,A_{m-1}$ closed convex subsets of $X$, with intersection $R=\bigcap_i A_i$. Let $S\subset X$ be a convex set with $S\cap R\ne\emptyset$, and let $D:S\times S\to\mathbb R$. The paper requires:

• I. $D(x,y)\ge 0$, with equality if and only if $x=y$.
• II. For every $y\in S$ and every $i$ there is a point $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$; it is the $D$-projection of $y$ onto $A_i$.
• III. For every $i$ and $y\in S$, the function $z\mapsto D(z,y)-D(z,P_iy)$ is convex on $A_i\cap S$.
• IV. $D(\cdot,y)$ has derivative $0$ at the point $y$.
• V. For every $z\in R\cap S$ and real $L$, the sublevel set $\{x\in S\mid D(z,x)\le L\}$ is compact.
• VI. If $D(x^n,y^n)\to 0$, $y^n\to y^*\in\bar S$, and $\{x^n\}$ lies in a compact set, then $x^n\to y^*$.

The relaxation sequence with control $(i_n)$ starts at any $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$. Under the cyclic control $i_n=n\bmod m$, the sets are projected onto in the order $A_0,A_1,\dots,A_{m-1},A_0,\dots$. A limiting point of $\{x^n\}$ is the limit of a convergent subsequence $x^{n_k}$.

The Lean development uses the namespace BregmanRelax.Cyclic: DConditions A S D P bundles conditions I–IV and VI together with the closedness and convexity of the sets, CondV S D Z is condition V for the points of $Z$, IsRelaxSeq S P i x is the relaxation sequence with control $i$, and cyclicControl hm is $n\mapsto n\bmod m$.

Formalization targets

Goal: Theorem 1 (p. 203)

Under conditions I–VI, with the cyclic control, every limiting point of every relaxation sequence lies in every set:

$$x^{n_k}\to x^* \quad\Longrightarrow\quad x^*\in\bigcap_{i=0}^{m-1}A_i .$$

The statement is about every starting point $x^0\in S$ and every convergent subsequence. It does not assert that the whole sequence converges.

Milestones

1. Lemma 1 (pp. 201–202): for $z\in A_i\cap S$ and $y\in S$,

$$D(P_iy,y)\le D(z,y)-D(z,P_iy).$$

2. Lemma 2 (2) (p. 202): for any control and any $z\in R\cap S$, $\lim_{n\to\infty}D(z,x^n)$ exists.
3. Lemma 2 (3) (p. 202): for any control, $D(x^{n+1},x^n)\to 0$.
4. Lemma 2 (1) (p. 202): for any control, $\{x^n\}$ lies in a compact set.

Further result: Note 1, condition (1) (pp. 204–205)

For any control whose relaxation sequence has all its limiting points in $R$ (the cyclic control, by Theorem 1), if in addition $S$ is closed and $y\mapsto D(z_1,y)-D(z_2,y)$ is continuous on $S$ for all $z_1,z_2\in R\cap S$, then the relaxation sequence converges to a point of $R$.

Significance

Theorem 1 is the abstract convergence theorem behind cyclic Bregman projections. With $D(x,y)=\|x-y\|^2$ in a Hilbert space it gives the convergence of cyclic orthogonal projections onto finitely many closed convex sets in the weak topology (the paper's Example 1). With $D$ given by a Bregman divergence it gives the method that the paper's §2 turns into an algorithm for convex programs with linear equality and inequality constraints, including entropy maximization. Lemma 1, the generalized Pythagorean inequality, is used throughout the later literature on Bregman projections, mirror descent and online learning.

The results are proved in the paper and are classical. To our knowledge no machine-checked version exists: Mathlib has orthogonal projections onto closed convex sets in Hilbert spaces, but no Bregman projections and no convergence theorem for cyclic projection methods. A formalization supplies an axiomatic interface (conditions I–VI) that does not depend on any particular divergence, so special cases (Euclidean distance, Kullback–Leibler divergence, Bregman divergences of Legendre functions) can be obtained by checking the conditions.

Difficulty

There is no norm and no metric: $D$ is neither symmetric nor subject to a triangle inequality, and $X$ is only a topological vector space. The usual Fejér-monotonicity argument for Euclidean projections, which compares distances to a fixed point of $R$, works only one way in $D$. Convergence of a subsequence $x^{n_k}$ does not by itself say anything about the shifted subsequences $x^{n_k+1},\dots,x^{n_k+m-1}$, and these are needed to reach every set $A_i$. That step requires condition VI together with compactness, and condition VI has a compactness premise that has to be supplied separately. Throughout, convergence is in a general topology where "compact" and "sequentially compact" may differ.

Formalization scope

The formalization commits to the following readings, each recorded in the items' Formalization Notes.

• The projection is a map. $P:\iota\to X\to X$ is fixed, and condition II states that $P_iy$ is a minimizer. Condition III is stated for this map.
• Condition IV, one-sided. The paper asks for $\lim_{t\to0}D(y+tz,y)/t=0$ for every $z\in X$. The formalization assumes only the right-hand limit in the directions $w-y$ with $w\in S$, which is what the proofs use and what the paper's IV implies. Every theorem is therefore at least as strong as the paper's.
• Compactness is sequential. "Compact" in V, VI and Lemma 2 (1) is IsSeqCompact. The set of elements of $\{x^n\}$ being compact is read as $\{x^n\}$ lying in a sequentially compact set.
• Hausdorff space. The proof of Theorem 1 identifies two limits of one sequence, so T2Space X is assumed. $X$ is a real topological vector space (IsTopologicalAddGroup, ContinuousSMul ℝ).
• Limiting point means the limit of x ∘ φ for a strictly increasing φ : ℕ → ℕ.
• Index base. The sets are indexed by Fin m with $0<m$, and the cyclic control is $n\mapsto n\bmod m$, the paper's $i_n=(n\bmod m)+1$ shifted by one.
• Translation typos. Condition II is printed as "$D(x,y)=\min_{z\in A_i\cap S}D(z,x)$" with "$i\in T$". The formalization reads $\min_z D(z,y)$ and $i\in I$. In Lemma 2 (2) the faint set symbol is read as $R$, and $z$ is taken in $R\cap S$, as in the proof.
• Domain of $D$. $D$ is a total function X → X → ℝ; every condition constrains it on $S\times S$ only, and the standing assumption $S\cap R\ne\emptyset$ is an explicit hypothesis.

A trivializing formalization is ruled out: the hypotheses are satisfiable (a sorry-free local check takes $X=\mathbb R$, $D(x,y)=(x-y)^2$, two overlapping closed intervals and the clamp projections), the conclusion concerns every limiting point of every cyclic run, and the goal neither assumes convergence nor restricts the control.

Contributions welcome: proofs of the milestones, a proof of the goal, and instances of DConditions for concrete divergences (squared Euclidean distance in finite dimension, Bregman divergences of strictly convex differentiable functions). These instances are reusable by the companion missions of this paper.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics 7(3) (1967) 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
• L. G. Gubin, B. T. Polyak, E. V. Raik, The method of projections for finding the common point of convex sets, USSR Computational Mathematics and Mathematical Physics 7(6) (1967) 1–24. https://doi.org/10.1016/0041-5553(67)90113-9
• T. S. Motzkin, I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 393–404. https://doi.org/10.4153/CJM-1954-038-x
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, Journal of Optimization Theory and Applications 34 (1981) 321–353. https://doi.org/10.1007/BF00934676

Motivation

A group of $m$ individuals each hold a subjective probability distribution over the same $n$ outcomes, and one wants a single distribution representing their consensus. Averaging and convolution are the obvious candidates. Eisenberg and Gale (Ann. Math. Statist. 30(1), 1959) observe that a real institution already performs such an aggregation: the pari-mutuel method of betting on horse races, in which the final "track's odds" on a horse are proportional to the total amount bet on it.

The difficulty is circular. Each bettor wants to bet where the ratio of their own probability to the track probability is largest, but the track probabilities are only known after everyone has bet. The paper asks whether track probabilities and bets compatible with both the bettors' strategies and the pari-mutuel principle exist, and whether they are determined by the data. It answers yes on both counts for the probabilities, which gives a well-defined notion of pari-mutuel consensus.

The variational problem the paper introduces, maximizing $\sum_i b_i \log(\text{utility}_i)$, is now known as the Eisenberg–Gale convex program. It is the standard tool for computing equilibria of linear Fisher markets, and the pari-mutuel market is the special case in which every bettor's utility for a horse is their subjective win probability.

Setting

There are $m$ bettors $B_1,\dots,B_m$ and $n$ horses $H_1,\dots,H_n$.

• The subjective probability matrix $P=(p_{ij})$ is $m\times n$; $p_{ij}$ is the probability, in the opinion of $B_i$, that $H_j$ wins. Each row is a probability distribution: $p_{ij}\ge 0$ and $\sum_j p_{ij}=1$.
• Bettor $B_i$ has a budget $b_i>0$, with the unit of money chosen so that $\sum_i b_i=1$.
• Each column of $P$ contains at least one positive entry (a horse nobody believes in can be removed).

Unknowns are Greek. $\pi_j$ is the track probability of $H_j$ and $\beta_{ij}$ is the amount $B_i$ bets on $H_j$. Nonnegative $\pi_j,\beta_{ij}$ are equilibrium probabilities and bets when

$$\text{(1)}\ \sum_{j=1}^n\beta_{ij}=b_i,\qquad \text{(2)}\ \sum_{i=1}^m\beta_{ij}=\pi_j,\qquad \text{(3)}\ \text{if } \mu_i=\max_s\frac{p_{is}}{\pi_s}\text{ and }\beta_{ij}>0,\text{ then }\mu_i=\frac{p_{ij}}{\pi_j}.$$

(1) is the budget relation, (2) the pari-mutuel condition, and (3) says each bettor bets only on horses that maximize the subjective expectation $p_{ij}/\pi_j$.

The paper's variational problem is

$$\varphi(\xi)=\sum_{i=1}^m b_i\log\sum_{j=1}^n p_{ij}\xi_{ij}\quad\text{on}\quad D=\Big\{\xi:\ \xi_{ij}\ge0,\ \sum_{i=1}^m\xi_{ij}=1\ \text{for all } j\Big\},$$

with $\varphi=-\infty$ where an inner sum vanishes. From a maximizer $\bar\xi$ it builds $\pi_j=\max_i b_ip_{ij}/\sum_s p_{is}\bar\xi_{is}$ (6) and $\beta_{ij}=\bar\xi_{ij}\pi_j$ (7). In Lean the market is PariMutuel.Consensus.Market m n, equilibrium is Market.IsEquilibrium, and $\varphi$, $D$, the maximizer predicate, (6) and (7) are Market.phi, D m n, Market.IsPhiMaximizer, Market.trackProb, Market.bets.

Formalization targets

Goal: existence and uniqueness of equilibrium probabilities

$$\exists!\,\pi\in\mathbb R^n\ \ \exists\,\beta\in\mathbb R^{m\times n}:\ (\pi,\beta)\ \text{are equilibrium probabilities and bets}.$$

Only $\pi$ is unique; the paper notes that equilibrium bets need not be.

Milestones

1. $\varphi$ attains its maximum on $D$ at a point with every inner sum positive (p. 167).
2. $\partial\varphi/\partial\xi_{ij}=b_ip_{ij}/\sum_s p_{is}\xi_{is}$ wherever the inner sums are positive (p. 167).
3. (8): at a maximizer, $\bar\xi_{ij}>0$ implies $\pi_j=\partial\varphi/\partial\bar\xi_{ij}$ (p. 167).
4. Every $\pi_j$ of (6) is positive (p. 167).
5. EXISTENCE THEOREM: for every maximizer $\bar\xi$, (6)–(7) are equilibrium probabilities and bets (p. 167).
6. Every equilibrium has $\pi_j>0$ (p. 168).
7. For two equilibria, $\sum_k\bar\pi_k\bar\pi_k/\pi_k\le 1$ (p. 168).
8. If $\pi>0$, $\bar\pi\ge0$, both sum to 1 and $\sum_k\bar\pi_k^2/\pi_k\le1$, then $\bar\pi=\pi$ (p. 168).
9. UNIQUENESS THEOREM: equilibrium probabilities are unique (p. 168).

A further, non-milestone item states the referee's example (p. 168): with two bettors of equal budgets and two horses, if the first bettor's distribution is $(\tfrac12,\tfrac12)$, the equilibrium probabilities are $(\tfrac12,\tfrac12)$ whatever the second bettor believes.

Significance

The result makes pari-mutuel odds a well-defined function of the bettors' beliefs and budgets, so the consensus can be studied as a mathematical object; the referee's example shows it behaves very differently from averaging, since a single indifferent bettor can fix it. The existence proof replaces a fixed-point argument by a concave maximization, which is the origin of the Eisenberg–Gale program, later the basis of convex-programming and combinatorial algorithms for Fisher market equilibria.

The theorems are classical and fully proved in the paper. To the knowledge of this mission they have no machine-checked proof. The mission produces a formal pari-mutuel market model, the Eisenberg–Gale program with the correct treatment of $\log 0=-\infty$, and Lean proofs of existence and uniqueness. The platform's Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities missions (Vazirani–Yannakakis) concern a related Fisher-market model with rational piecewise-linear utilities.

Difficulty

The existence statement, as the paper proves it, has two delicate points. $\varphi$ is $-\infty$ on part of the boundary of $D$, so "continuous on a compact set" needs the extended-real reading, and a real-valued formalization must handle the boundary separately. The first-order condition (8) has to be derived from maximality on a polytope with equality constraints on columns, not from an unconstrained critical point.

For uniqueness, the natural first idea, strict concavity of $\varphi$, fails: $\varphi$ is concave but not strictly concave in $\xi$, and indeed equilibrium bets are not unique. Uniqueness has to be proved for the probabilities directly, for arbitrary equilibria and not only those built from a maximizer, and it needs positivity of all $\pi_j$, which the paper uses without proof.

Formalization scope

• Bettors are Fin m and horses Fin n, indexed from 0. All data are real. Every standing assumption (rows of $P$ are probability vectors, no zero column, $b_i>0$, $\sum_i b_i=1$) is a field of Market; $m\ge1$ follows from $\sum_ib_i=1$.
• Condition (3) is written multiplied out: $\beta_{ij}>0\Rightarrow p_{is}\pi_j\le p_{ij}\pi_s$ for all $s$. This equals (3) when $\pi>0$ and encodes the paper's $p/0=+\infty$ when some $\pi_s=0$. Positivity of $\pi$ is not part of the definition of equilibrium; it is milestone 6.
• $D$ has column sums one, as in (5).
• $\varphi$ is real-valued. A maximizer is a point of $D$ with positive inner sums that dominates every point of $D$ with positive inner sums; the excluded points have $\varphi=-\infty$ on the page. The max in (6) is Finset.sup' over the nonempty set of bettors.
• Ruled out: a version of (3) with real division ($x/0=0$) admits spurious equilibria with $\pi_s=0$ and makes uniqueness false; a maximizer defined with the raw real $\varphi$ ($\log0=0$) changes the set of maximizers; adding $\pi>0$ or $\sum_j\pi_j=1$ to the equilibrium definition weakens the goal.
• Needed infrastructure: compactness of $D$ and an argument handling the $-\infty$ boundary, one-variable derivatives of $\log$ of linear forms, and the equality case of the Cauchy–Schwarz inequality. Milestones 7–9 use no analysis and can be attacked independently of 1–5. Proofs of any milestone, and reusable lemmas on the Eisenberg–Gale program, are welcome.

Selected references

• E. Eisenberg and D. Gale, Consensus of subjective probabilities: the pari-mutuel method, The Annals of Mathematical Statistics 30(1):165–168, 1959. https://doi.org/10.1214/aoms/1177706369
• V. V. Vazirani and M. Yannakakis, Market equilibrium under separable, piecewise-linear, concave utilities, Journal of the ACM 58(3), 2011. https://doi.org/10.1145/1970392.1970394