Optimization

Motivation

A chance constraint limits the probability of violating a requirement rather than requiring that requirement to hold for every realization of uncertain data. Charnes and Cooper developed deterministic optimization problems for several ways of judging decisions under such constraints. Their P model gives a satisficing objective: increase the probability of reaching a specified aspiration level while meeting prescribed reliability levels for the resource constraints. The paper's concrete decision rule makes the decision vector depend linearly on the random right-hand side, and its P-model section moves from a fractional deterministic program to a convex one. The result explains how a risk-adjusted ratio can be optimized without retaining a fractional objective. The source is Charnes and Cooper, 1963, pp. 30–33, especially equations (35) and (38)–(39b).

The related linear-fractional change of variables was already being used for linear programs Charnes and Cooper, 1962; the present section applies it to constraints built from second moments rather than linear equations. That distinction matters because the normalized feasible set contains a boundary at zero scale, and because second-moment inequalities require their own convexity claim. The paper cites fractional programming results for its local-to-global assertion about (38); the mission focuses on its explicit transformed program (39). Charnes and Cooper, 1963, p. 32.

Setting

Let $m,n$ be positive integers and $(\Omega,P)$ a probability space. A fixed real $m\times n$ matrix $A$ has rows $a_i'$. Random vectors $b:\Omega\to\mathbb R^m$ and $c:\Omega\to\mathbb R^n$ give the right-hand side and objective coefficients. The paper restricts decisions to the linear decision rule $x=Db$, where the real $n\times m$ matrix $D$ is chosen before $b$ is realized. Write $\mu_b=E[b]$ and $\mu_c=E[c]$. A number $z_0$ is the given aspiration value. For each row $i$, its reliability level $\alpha_i$ is strictly between $1/2$ and $1$, and $K_i=\Phi^{-1}(\alpha_i)>0$ is the corresponding standard-normal quantile. These are the objects of equations (5), (19b), (21), and (27) in Charnes and Cooper, 1963.

The residual $a_i'Db-b_i$ has raw second moment $\sigma_i^2(D)=E[(a_i'Db-b_i)^2]$ and negative mean $\mu_i(D)=\mu_{b_i}-a_i'D\mu_b$. The aspiration error has raw second moment $V(D)=E[(c'Db-z_0)^2]$. These definitions come from equations (30) and (34). The expected linear objective appearing in the deterministic programs is $\mu_c'D\mu_b$; the model records the paper's assumption that the components of $b$ and $c$ are uncorrelated. Charnes and Cooper, 1963, pp. 26, 28, 30.

Program (38) chooses $(D,v,v_0,w_0)$ and maximizes $v_0/w_0$. Its inequalities bound the mean objective below by $z_0+v_0$, bound $w_0$ below by the root-mean-square aspiration error, and bound each nonnegative $v_i$ between the row's risk term and $\mu_i(D)$. The denominator satisfies $w_0>0$. Program (39) introduces a nonnegative scale $t$ and barred variables. It fixes $\bar w_0=1$ and maximizes the linear objective $\bar v_0$. The barred moments are calculated from $\bar D$ and $t$ by equation (39b), rather than declared to be scaled copies of the unbarred moments. Charnes and Cooper, 1963, pp. 32–33.

Formalization targets

Convex transformed program

Let $F_{39}$ contain every point satisfying all of (39), including $t=0$. The paper's convex-programming claim becomes

$$F_{39}\text{ is convex}.$$

The source states the claim after displaying the barred moments, in the paragraph following (39b). Charnes and Cooper, 1963, p. 33.

Equal optimal values

Let $F_{38}$ be the feasible set of (38). Provided $F_{38}$ is nonempty, the mission goal states that the normalized substitution sends each point of $F_{38}$ to a point of $F_{39}$ with the same objective, and that

$$\sup_{(D,v,v_0,w_0)\in F_{38}}\frac{v_0}{w_0} =\sup_{(\bar D,\bar v,\bar v_0,\bar w_0,t)\in F_{39}}\bar v_0.$$

The suprema may be infinite. The equality concerns the complete program (39), including $t=0$. Positive-scale points have an inverse substitution; zero-scale points are retained in the comparison. This is the precise optimal-value reading of the paper's statement that (38) can be replaced by one convex program. Charnes and Cooper, 1963, pp. 32–33.

Significance

The result places the P model alongside the paper's E and V models as an optimization problem with convex feasible constraints and a nonfractional objective. A solver of (39) can compare aspiration and resource reliability within the same matrix decision rule. Equality of suprema says the transformed model has the same best attainable value even when the best value is only approached, and even when points at $t=0$ occur in the transformed feasible set. The forward and inverse substitution statements identify how positive-scale solutions correspond. Charnes and Cooper, 1963, pp. 30–33.

The paper result is a published mathematical claim. The present formalization states its definitions and assertions in Lean; its theorem proofs are still open. The standard Gaussian CDF and its inverse are available as a separately published Prove2Me definition, while the model-specific second moments and feasible sets must be formalized for this mission. The previously published Derman linear-fractional lemma concerns a polyhedral linear program and does not assert this P-model result. Completing the mission would add reusable formal machinery for expected-square constraints, a normalized perspective program, and equality of optimal values at a scale boundary.

Difficulty

The pointwise substitution $t=1/w_0$ only reaches points of (39) with $t>0$, while (39) explicitly permits $t=0$. Therefore a bijection of feasible points at positive scale alone does not establish equality of the displayed suprema. The proof also has to reconcile the squared form of the row constraints with convexity: $\bar\sigma_i^2$ is a raw second moment and $\bar\mu_i^2$ is the square of its mean, so their difference is the variance term relevant to the risk bound. Taking the fourth inequality as a generic difference of quadratics would obscure that claim. The paper prints a conflicting square and sign in (38), which must be resolved against its earlier (29) and later (39). Charnes and Cooper, 1963, pp. 28, 32–33.

Formalization scope

Lean uses finite index types Fin m and Fin n, real matrices and scalars, a probability measure $P$, and Bochner integrals for the moments. Square integrability is stated for every component of $b$ and $c$ and every product $c_jb_k$; this keeps the expected squares meaningful. The paper assumes $b$ and $c$ are uncorrelated, so the same componentwise equalities are recorded. It also assumes that each row residual has a Gaussian law under a decision matrix; the Lean theorem retains this standing assumption even though the substitution from (38) to (39) is algebraic. The quantile $K_i$ is imported from the published Cohen2019.Robust.PhiInvReal, with $1/2<\alpha_i<1$ excluding its junk endpoint values. The theorem concerns (38) onward; it does not assert the paper's analogous reduction from the original probability model (35), because the text does not establish a distributional theorem for its random objective. Charnes and Cooper, 1963, pp. 26–27, 31–33.

The source phrase “replace ... by one convex programming problem” is made explicit as convexity of the (39) feasible set, feasibility and value preservation of the forward scaling, and equality of extended-real suprema. The normalization $\bar w_0=1$, strict $w_0>0$, and weak $t\ge0$ are separate conditions. The $t=0$ slice is included, and the main theorem assumes $F_{38}$ nonempty. The barred functions are genuine expectations of the homogenized expressions of (39b). The square-and-sign discrepancy in printed (38) is resolved in favor of the form printed in (29) and (39), consistent with the nearby statement that the row constraints are the same as before. These choices exclude a vacuous denominator, an artificially smaller transformed set, and a trivially defined scaling identity. Reusable contributions include moment lemmas, convexity results for expected-square constraints, and supremum comparison for normalized programs.

Selected references

• A. Charnes and W. W. Cooper, Deterministic Equivalents for Optimizing and Satisficing under Chance Constraints, Operations Research 11(1), 1963, pp. 18–39. DOI.
• A. Charnes and W. W. Cooper, Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly 9(3–4), 1962, pp. 181–186. DOI.
• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1), 1962, pp. 16–24. DOI.
• J. Cohen, E. Rosenfeld, and Z. Kolter, Certified Adversarial Robustness via Randomized Smoothing, ICML, 2019. arXiv.

Motivation

A game without side payments (an NTU game) describes cooperation in which utility cannot be transferred between players: each coalition $A$ of players is assigned the set $V(A)$ of payoff vectors it can secure on its own. The core is the set of payoffs to the grand coalition that no coalition can improve upon. Whether the core is nonempty is the basic stability question of cooperative game theory. For games with side payments the answer is the Bondareva–Shapley theorem. For NTU games it is Scarf's theorem (Scarf 1967): a balanced game has a nonempty core. Billera (1970) gave a convex version, in which the payoff sets are convex and balancedness is stated with weighted Minkowski sums.

Aubin's paper (Aubin 1981) obtains Billera's version of the theorem by a different route. Players may join coalitions at fractional rates of participation, and the paper first proves a core existence theorem for these fuzzy games. The game on ordinary coalitions is then embedded into a fuzzy game whose core lies inside the core of the original game.

Setting

The players are $N = \{1,\dots,n\}$. A coalition $A \subseteq N$ is identified with its characteristic vector $\tau^A \in \{0,1\}^n$, and $\tau^N = (1,\dots,1)$. A fuzzy coalition is a vector $\tau \in [0,1]^n$ of participation rates with support $A_\tau = \{i : \tau_i > 0\}$. Write $(\tau\cdot c)_i = \tau_i c_i$, $\mathbb{R}^\tau = \tau\cdot\mathbb{R}^n$ for the vectors vanishing off $A_\tau$, $\mathbb{R}^\tau_+$ for its nonnegative part, and $\mathring{\mathbb{R}}^\tau_+$ for the vectors strictly positive on $A_\tau$.

A fuzzy game without side payments assigns to each $\tau \ge 0$ a nonempty, closed, convex set $V(\tau)\subseteq\mathbb{R}^\tau$. Each $V(\tau)$ is comprehensive, meaning $V(\tau) = V(\tau)-\mathbb{R}^\tau_+$, and bounded above, meaning $V(\tau)\subseteq C-\mathbb{R}^\tau_+$ for some $C$. The map is positively homogeneous: $V(t\tau) = tV(\tau)$ for every $t>0$. Its core is the set of $c\in V(\tau^N)$ such that $\tau\cdot c\notin V(\tau)-\mathring{\mathbb{R}}^\tau_+$ for every fuzzy coalition $\tau\neq 0$. With the support function $v(\tau,\lambda)=\sup_{c\in V(\tau)}\sum_i\lambda_i c_i$ and the simplex $M^n$, a weak (resp. strong) canonical cooperative equilibrium is a $c\in V(\tau^N)$ together with a $\bar\lambda\in M^n$ (resp. $\bar\lambda$ with all coordinates positive) satisfying $\sum_i\bar\lambda^i\tau_ic_i\ge v(\tau,\bar\lambda)$ for every $\tau\in[0,1]^n$.

A usual NTU game lives on a family $\mathcal{C}$ of coalitions that contains $N$ and every singleton. For each $A\in\mathcal{C}$, the set $V(A)\subseteq\mathbb{R}^A$ is nonempty, closed, convex, comprehensive and bounded above. A balance of $\tau$ is a vector of weights $m\ge 0$ on $\mathcal{C}$ with $\sum_{A\ni i}m(A)=\tau_i$ for every $i$, and $\mathcal{C}(\tau)$ is the set of balances of $\tau$. The fuzzy extension of the game is

$$\pi V(\tau)=\bigcup_{m\in\mathcal{C}(\tau)}\ \sum_{A\in\mathcal{C}} m(A)\,V(A),$$

and the game is balanced if $V(N)=\pi V(\tau^N)$.

Formalization targets

Goal: Theorem 7.1

For a balanced game without side payments,

$$\emptyset\neq\operatorname{core}(\pi V)\subseteq\operatorname{core}(V),\qquad \mathrm{CCE}_{\rm strong}(V)\subseteq\operatorname{core}(\pi V)\subseteq\mathrm{CCE}_{\rm weak}(V),$$

and in particular $\operatorname{core}(V)\neq\emptyset$.

Milestones

• Proposition 3.1: $c\in V(\tau^N)$ is in the core iff the maximum complaint $\alpha(c)=\sup_{\tau\neq0}\inf_{\lambda\in M^\tau}[v(\tau,\lambda)-\sum_i\lambda^i\tau_ic_i]$ is $\le 0$.
• Proof of Theorem 3.1(b): if $V$ is superadditive, $V(\tau)+V(\sigma)\subseteq V(\tau+\sigma)$, then $\tau\mapsto v(\tau,\lambda)$ is concave on $\mathbb{R}^n_+$.
• Theorem 3.1: strong equilibria lie in the core, and for a superadditive game the core lies in the set of weak equilibria.
• Theorem 5.1: a superadditive fuzzy game has a nonempty core.
• §7, (6), (7), (11): $\pi V$ is a superadditive fuzzy game that extends $V$, and its support function is $\pi v(\tau,\lambda)=\sup_{m\in\mathcal{C}(\tau)}\sum_A m(A)v(A,\lambda)$.
• §7 and the proof of Theorem 7.1: under balancedness, $\operatorname{core}(\pi V)\subseteq\operatorname{core}(V)$, and the equilibria of $V$ coincide with those of $\pi V$.

Significance

Theorem 7.1 gives the core existence result for convex NTU games under Billera's balancedness condition. Its proof goes through a statement about fuzzy coalitions, Theorem 5.1, which uses no combinatorial pivoting. That theorem also has independent uses. Its fuzzy core is the solution concept that §4 of the paper identifies with Walras equilibria of exchange economies. The canonical cooperative equilibria give a price-like certificate, a common rate of transfer $\bar\lambda$, that sandwiches the core.

The results are classical and proved. Prove2Me holds no statement of Scarf's or Billera's theorem, of NTU cores, or of balancedness for games without side payments, and Mathlib has none of these notions. The mission produces faithful statements of the paper's chain of results, and their proofs once solvers close them. It also builds reusable infrastructure: support functions of comprehensive sets, Minkowski combinations indexed by balances, and positively homogeneous set-valued maps.

Difficulty

Most of §7 is bookkeeping with Minkowski sums. The hard part is Theorem 5.1, the existence of a point in the fuzzy core. The core is defined by infinitely many exclusion conditions, one for each $\tau\in[0,1]^n$, so a finite intersection argument does not apply directly. The paper's route works with prices: it uses the superdifferential of the concave map $\tau\mapsto v(\tau,\lambda)$ at $\tau^N$, Ky Fan's inequality on a truncated simplex where all $\lambda_i\ge\varepsilon$, and a limit as $\varepsilon\to0$. That limit requires compactness of the approximating payoffs, and at the boundary of the simplex the superdifferential map is not upper semicontinuous. Theorem 3.1(b) needs a minisup theorem for a function that is concave in $\tau$ and convex and lower semicontinuous in $\lambda$. Mathlib has neither Ky Fan's inequality nor this minimax theorem in that form.

Formalization scope

All statements import one definitions file, FuzzyGames.NTUCore.Basic. The formalization commits to the following conventions.

• Players are Fin n, and payoffs, fuzzy coalitions and rates of transfer are Fin n → ℝ, ordered coordinatewise. $\mathbb{R}^\tau$ is encoded as "vanishes where $\tau_i=0$", which equals $\tau\cdot\mathbb{R}^n$ for $\tau\ge0$.
• Fuzzy games are defined directly on the orthant $\tau\ge0$, the paper's extension of $V$ from $[0,1]^n$ by homogeneity. Homogeneity holds for every $t>0$, and superadditivity holds on $\mathbb{R}^n_+$.
• Support functions, $\alpha$ and $\pi v$ take values in EReal, so an unbounded supremum is $+\infty$ and never a junk $0$.
• The supremum defining $\alpha(c)$ ranges over $\tau\neq0$. Since $M^0=\emptyset$, including $\tau=0$ would make $\alpha\equiv+\infty$ and Proposition 3.1 false. Blocking coalitions are likewise $\tau\neq0$, as in §3 (4).
• $\mathcal{C}$ is a finite family of nonempty coalitions that contains $N$ and every singleton. "$\forall A\neq\emptyset$" in §7 ranges over $\mathcal{C}$.
• The paper leaves $n\ge1$ implicit. Theorem 3.1(b) and Theorem 5.1 carry $0<n$: for $n=0$ the simplex is empty while the core is not.
• In §7 (11), $\pi v(\tau,\lambda)$, which the paper uses without defining it, is taken to be the extension §6 (2) applied to $A\mapsto v(A,\lambda)$, for $\lambda\ge0$.
• The §7 sentence after (5) is stated with two extra conclusions: $\pi V(\tau)$ is nonempty and contained in $\mathbb{R}^\tau$. These are the remaining requirements of §3 (3) that are needed to apply Theorem 5.1.
• Sums and scalings of sets are Mathlib's pointwise operations.

The fuzzy-game axioms are a Prop-valued structure and are hypotheses of every theorem. The core and the equilibria are defined for an arbitrary set-valued map, so the theorems about $\pi V$ do not presuppose that it is a fuzzy game. That fact is the content of the §7 milestones and is not assumed. Non-vacuity has been checked locally on a concrete instance: $V(\tau)=\{c\in\mathbb{R}^\tau: c\le\tau\}$ is a superadditive fuzzy game, and $V(A)=\{c\in\mathbb{R}^A:c\le\tau^A\}$ is a balanced game on every admissible $\mathcal{C}$, with $(1,\dots,1)$ in both cores.

Contributions are welcome at every level: the §7 Minkowski-sum lemmas, the support-function identities, and a minisup or Ky Fan theorem in the form the proofs need. Reusable pieces include support functions of comprehensive sets and Sion-type minimax.

Selected references

• J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
• H. E. Scarf, The Core of an N Person Game, Econometrica 35(1) (1967) 50–69. https://doi.org/10.2307/1909888
• L. J. Billera, Some Theorems on the Core of an n-Person Game without Side-Payments, SIAM Journal on Applied Mathematics 18(3) (1970) 567–579. https://doi.org/10.1137/0118053
• K. Fan, A Minimax Inequality and Applications, in O. Shisha (ed.), Inequalities III, Academic Press (1972) 103–113.

Motivation

Large scale unconstrained optimization often makes an exact Newton step expensive. At each iterate, Newton's method asks for a solution of a linear system involving the Hessian, and the cost of solving that system can dominate the cost of evaluating the objective. Dembo and Steihaug's 1983 truncated Newton method uses conjugate gradients to stop the linear solve early, either when the residual is small enough or when the current direction has insufficient positive curvature. The resulting direction is paired with a line search. The question for this mission is whether those early exits still give a globally reliable optimization method under the paper's assumptions. The answer, in Theorem 2.1, is that every resulting run has gradient norm tending to zero, and a positive definite Hessian at one limit point makes the whole sequence converge to that point.

Setting

The objective is a twice continuously differentiable function $f:\mathbb R^n\to\mathbb R$. Write $g(x)=\nabla f(x)$ for its gradient and $H(x)=Dg(x)$ for its Hessian. For every initial point $x_0$, the paper assumes that the sublevel set $L(x_0)=\{x:f(x)\le f(x_0)\}$ is bounded. The formalization uses the Euclidean norm and its inner product, so the operator norm of $H$ is also Euclidean.

At a major iterate $x_k$, the minor conjugate-gradient iteration starts at $p_0=0$ with residual and direction $r_0=d_0=-g(x_k)$. It maintains a scalar $\delta_i$, initialized to $\|r_0\|^2$, alongside the usual conjugate-gradient state. Before taking its next conjugate-gradient step, it checks whether $\langle d_i,H(x_k)d_i\rangle\le\varepsilon\delta_i$. If so, it returns $d_0=-g(x_k)$ when $i=0$ and the current approximation $p_i$ otherwise. If this first test fails, it takes a conjugate-gradient step and checks whether $\|r_{i+1}\|\le\eta_k\|g(x_k)\|$. If so, it returns $p_{i+1}$. A TNCG direction is the direction returned by the first exit that occurs. The forcing value $\eta_k$ sets the residual tolerance.

The major iteration chooses a positive step length $\lambda_k$. With $p_k$ the minor iteration's output and $0<\alpha<1/2$, $\alpha<\beta<1$, the line search requires both sufficient decrease and a curvature condition:

$$f(x_k+\lambda_k p_k)\le f(x_k)+\alpha\lambda_k\langle g(x_k),p_k\rangle, \qquad \langle g(x_k+\lambda_kp_k),p_k\rangle\ge\beta\langle g(x_k),p_k\rangle.$$

The update is $x_{k+1}=x_k+\lambda_kp_k$. A run is a sequence satisfying this rule from its specified starting point. The paper also states an alternative function-value curvature condition; this mission defines it because the local unit-step theorem discusses both choices, although the main run uses the displayed gradient condition.

Formalization targets

Global convergence

For every starting point there is a TNCG run, and every run satisfies

$$\|g(x_k)\|\longrightarrow0.$$

If $x^*$ is a limit point of that run and $H(x^*)$ is positive definite, then

$$x_k\longrightarrow x^*.$$

The existence clause is the formal meaning of the paper's assertion that the iterates are well defined. The six milestones follow the paper's appendix: the conjugate-gradient relations of Theorem A.1; the uniform descent and direction bounds of Lemma A.2; the line-search existence and directional-derivative limit used in the proof of Theorem A.3; Theorem A.3 itself; and eventual unit-step admissibility in Theorem A.4. The companion Theorem 2.2 addresses the eventual residual exit and unit-step behavior when a run converges to a point with positive definite Hessian. These results are all stated in the original paper.

Significance

The target shows that the computational shortcut in the inner linear solve preserves a global first-order guarantee: no TNCG run can maintain a gradient norm bounded away from zero. It also identifies when the sequence has one limit, rather than merely having stationary accumulation points. The local companion result describes the regime where the truncated method can take full steps and the residual stopping test governs the minor iteration.

The mathematical results are proved in the 1983 paper, while this mission's Lean statements are open proof targets. A complete formalization would connect the finite-dimensional conjugate-gradient recurrence, the line-search argument on bounded sublevel sets, and the convergence statement in one machine-checked development. The conjugate-gradient identities and line-search facts could be reused in other optimization algorithms; the exact first-exit model and the global conclusion are specific to this method.

Difficulty

The minor iteration is not an ordinary positive definite conjugate-gradient solve. The Hessian may be indefinite away from a solution, and the iteration must stop at insufficient curvature before using a later residual state. A convergence argument that assumes positive definiteness at every iterate would therefore miss the case the algorithm was designed to handle. The line search must work for the returned direction, including the first iteration's steepest-descent fallback. The limit-point conclusion adds a separate issue: a vanishing gradient norm alone does not force an entire sequence to converge to a chosen limit point.

Formalization scope

Lean represents $\mathbb R^n$ as EuclideanSpace ℝ (Fin n), uses its Euclidean norm and inner product, and defines $H(x)$ as the derivative of the gradient. The objective is $C^2$ and every sublevel set is bounded, as specified at the start of the paper. The TNCG recurrence is total, but an admissible direction must come from its first actual exit, with the curvature test preceding the residual test. At $i=0$, the curvature exit returns $-g$, not the zero initial approximation. This prevents a false stationary run. The residual test is written as a product inequality, equivalent to the paper's quotient when the residual test is reached.

Step lengths are positive. A run is extended through stationary points by zero directions, giving an infinite sequence on which a limit can be stated. Theorem 2.1 imposes no extra restriction on the forcing sequence and no upper bound on step lengths. Theorem A.1 corrects the printed Krylov-space index from $H^{k-1}g$ to $H^kg$. Theorem A.4 adds $g(x^*)=0$, needed for the conclusion and true in the paper's applications. Theorem 2.2 requires nonnegative forcing values and guards its residual-exit conclusion at stationary iterates. These corrections are recorded item by item in the moderation notes. Contributions to the conjugate-gradient identities, bounded-level-set line search, and isolated-limit-point argument are all within scope.

Selected references

• R. S. Dembo and T. Steihaug, Truncated-Newton algorithms for large-scale unconstrained optimization, Mathematical Programming 26 (1983), 190–212. DOI: 10.1007/BF02592055.

Motivation

Truncated-Newton methods minimize a smooth function $f:\mathbb{R}^n\to\mathbb{R}$ by taking, at each iterate $x_k$, a search direction obtained by solving the Newton equation $H(x_k)p=-g(x_k)$ only approximately, with the linear conjugate gradient (CG) method. Here $g$ is the gradient and $H$ the Hessian of $f$. The approach was analysed by Dembo and Steihaug (Math. Programming 26, 1983), building on the inexact Newton framework of Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19, 1982), and Newton–CG with curvature tests remains a standard large-scale method (Nocedal and Wright, Numerical Optimization, Ch. 7).

Away from a minimizer the Hessian need not be positive definite, and CG on an indefinite system can produce directions along which $f$ curves downward. The Dembo–Steihaug method stops CG when it meets such a direction. A practical question follows: started at or near a stationary point that is not a local minimizer, will the method ever notice the nonpositive curvature? Theorem 2.4 of the paper answers it for exact CG: it does, except in a degenerate case described by the eigenspaces of $H$.

Setting

Fix a symmetric linear operator $H$ on $\mathbb{R}^n$, with the Euclidean inner product $u^{\mathsf T}v$ and norm $\|\cdot\|$, and a vector $g\in\mathbb{R}^n$. In the paper these are $H(x_k)$ and $g(x_k)$ at the current iterate.

The TNCG minor iteration (p. 194) runs CG on $Hp=-g$ from $p_0=0$. Its state at iteration $i$ is $(p_i,r_i,d_i,\delta_i)$:

$$p_0=0,\quad r_0=-g,\quad d_0=r_0,\quad \delta_0=r_0^{\mathsf T}r_0,$$

and, writing $q_i=Hd_i$,

$$\alpha_i=\frac{r_i^{\mathsf T}r_i}{d_i^{\mathsf T}q_i},\ \ p_{i+1}=p_i+\alpha_id_i,\ \ r_{i+1}=r_i-\alpha_iq_i,\ \ \beta_i=\frac{r_{i+1}^{\mathsf T}r_{i+1}}{r_i^{\mathsf T}r_i},\ \ d_{i+1}=r_{i+1}+\beta_id_i,\ \ \delta_{i+1}=r_{i+1}^{\mathsf T}r_{i+1}+\beta_i^2\delta_i .$$

At iteration $i$ the method first applies the curvature test (2.1), $d_i^{\mathsf T}Hd_i\le\varepsilon\,\delta_i$, and stops if it holds; otherwise it computes $r_{i+1}$ and applies the truncation test (2.2), $\|r_{i+1}\|/\|g\|\le\eta$, and stops if it holds. With $\varepsilon=\eta=0$, (2.1) reads $d_i^{\mathsf T}Hd_i\le0$ and (2.2) reads $r_{i+1}=0$. The method exits through (2.1) at $i$ when no test fired at any iteration $j<i$ and (2.1) holds at $i$.

For $\mu\in\mathbb{R}$ the eigenspace is $E(\mu,H)=\{v: Hv=\mu v\}$ (A.21). The span of vectors $v_1,\dots,v_m$ is written $[v_1,\dots,v_m]$; the Krylov space of $g$ is $[g,Hg,\dots,H^{m}g]$.

Formalization targets

Goal: Theorem 2.4 (p. 197)

Let $\eta_k=\varepsilon=0$. If $H$ is not positive definite, then either the minor iteration exits through (2.1) at some iteration $i$, so that

$$d_i^{\mathsf T}Hd_i\le 0 \quad\text{at an iteration } i \text{ the method reaches},$$

or

$$g^{\mathsf T}v=0\quad\text{for every } v \text{ with } Hv=\mu v,\ \mu\le0 .$$

Milestones

1. Theorem A.1, (A.2) and (A.5), at $\varepsilon=0$ (p. 206). If $d_i^{\mathsf T}Hd_i>0$ for $i=0,\dots,k$, then $d_i^{\mathsf T}Hd_j=0$ for $i\ne j\le k$, and $[d_0,\dots,d_k]=[g,Hg,\dots,H^kg]$.
2. Theorem A.5 (p. 210). If $g$ has a nonzero projection on each eigenspace of $H$, $k$ is the number of distinct eigenvalues, and vectors $d_0,\dots,d_{k-1}$ are $H$-conjugate with $(d_i,Hd_i)>0$ and span $[g,\dots,H^{k-1}g]$, then $H$ is positive definite.
3. The first sentence of the proof of Theorem 2.4 (p. 211). If $g$ is not orthogonal to any eigenspace of $H$, and exact CG passes the curvature test up to iteration $i$ and ends with $r_{i+1}=0$, then $H$ is positive definite.

Significance

The theorem is the theoretical justification, given in the paper on p. 197, for using the direction of negative curvature $d_i$ produced in case (ii) of the minor iteration: with exact arithmetic and no truncation, CG either produces a direction of nonpositive curvature or the gradient lies entirely in the span of eigenvectors with positive eigenvalues. The paper draws the consequence that if $x_k\to x^*$ and the method terminates through (2.2), then, outside this rare case, $x^*$ is a strong local minimizer. Theorem A.5 is a self-contained statement about conjugate families in Krylov spaces, usable in any analysis of CG on indefinite systems.

The result is proved in the paper (Appendix, pp. 206–211), with the CG relations of Theorem A.1 cited from Hestenes and Stiefel. No machine-checked proof of these statements is known to this mission. Formalizing them produces a Lean development of CG on a symmetric, possibly indefinite operator, with its conjugacy and Krylov-span relations, which classical treatments state only for positive definite systems.

Difficulty

The CG relations of Theorem A.1 are usually proved for positive definite $H$, where every denominator is positive. Here $H$ is indefinite, and the relations hold only as long as the curvature along the directions has stayed positive; the induction must carry that hypothesis and must also show the residuals do not vanish early. The passage from "CG ended with $r=0$" to a statement about all eigenspaces is the second obstacle: the CG run sees only the Krylov space of $g$, so one must relate that space to the eigenspaces that $g$ meets, using symmetry of $H$ and a count of distinct eigenvalues. A direct argument via "the directions span $\mathbb{R}^n$" fails, because when $g$ misses an eigenspace the Krylov space is a proper subspace.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n); $H$ is a continuous linear map that is self-adjoint (IsSelfAdjoint H), as the paper's $H$ is a Hessian. Positive definiteness is $v^{\mathsf T}Hv>0$ for all $v\ne0$. The CG recursion is total and carries no stopping test; division by zero returns $0$ in Lean, so states after a would-be stop are junk, and the statements read the iteration only through first-exit predicates. The test (2.2) is encoded in the product form $\|r_{i+1}\|\le\eta\|g\|$.

Theorem 2.4 is stated for an arbitrary symmetric $H$ and vector $g$ rather than at an iterate of a run of the full algorithm. It uses nothing else about $f$ or the run, and every such pair occurs as the Hessian and gradient of an admissible objective. The paper's (A.5) prints $H^{k-1}g$ as the last Krylov vector; the correct $H^kg$ is used.

A trivializing formalization exists and is ruled out: the first alternative is not "$d_i^{\mathsf T}Hd_i\le0$ for some $i$" over the unstopped recursion, which holds automatically once a residual vanishes (the recursion then continues with $d=0$); it requires that iteration $i$ is reached with no earlier exit. The goal does not assume conjugacy, the Krylov span identity, or the hypotheses of Theorem A.5.

A complete development needs the spectral theorem for self-adjoint operators on finite-dimensional spaces (in Mathlib), finiteness of the set of eigenvalues, and the CG invariants. The CG lemmas are reusable for any Newton–CG or trust-region CG analysis. Proofs of the milestones, and of auxiliary CG invariants such as (A.3)–(A.4), are welcome.

Selected references

• R. S. Dembo and T. Steihaug, Truncated-Newton algorithms for large-scale unconstrained optimization, Mathematical Programming 26 (1983) 190–212. https://doi.org/10.1007/BF02592055
• R. S. Dembo, S. C. Eisenstat and T. Steihaug, Inexact Newton methods, SIAM Journal on Numerical Analysis 19 (1982) 400–408. https://doi.org/10.1137/0719025
• M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, Journal of Research of the National Bureau of Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
• T. Steihaug, The conjugate gradient method and trust regions in large scale optimization, SIAM Journal on Numerical Analysis 20 (1983) 626–637. https://doi.org/10.1137/0720042
• J. Nocedal and S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006. https://doi.org/10.1007/978-0-387-40065-5

Motivation

Minimizing a smooth function subject to simple bounds on the variables, $l\le x\le u$, is one of the most common problems in nonlinear optimization: it arises on its own (nonnegativity constraints, box-constrained least squares, parameter estimation with physical ranges) and as the subproblem of augmented Lagrangian and penalty methods. The classical approaches are active-set methods, which follow the boundary of the box and must guess which bounds are tight, and projected-gradient methods, which project trial points onto the box.

Coleman and Li proposed an alternative that never touches the boundary: an interior-reflective Newton method. Every iterate is strictly feasible; a new affine scaling $D(x)$ measures how far each variable is from the bound its gradient points toward; and the line search follows a reflective path, which bounces off the faces of the box instead of stopping at them or being projected back. The method is the basis of the trust-region-reflective algorithm in MATLAB's Optimization Toolbox (fmincon, lsqnonlin), so its convergence theory underlies a widely used solver.

Timeline:

• 1992–1994: Coleman and Li introduce the interior-reflective approach and analyse its convergence (Math. Programming 67, 1994), proving first-order global convergence (Theorem 8) and local quadratic convergence (Theorem 13).
• 1996: Coleman and Li extend the approach to trust-region subproblems (SIAM J. Optim. 6, 1996), the version implemented in MATLAB.

This mission is the first of two drawn from the 1994 paper; the second treats the local quadratic rate.

Setting

The problem (1.1) is

$$\min_{x\in\mathbb R^n} f(x)\quad\text{subject to}\quad l\le x\le u,$$

with $l\in(\mathbb R\cup\{-\infty\})^n$, $u\in(\mathbb R\cup\{+\infty\})^n$, $l\le u$. The feasible box is $\mathcal F=\{x:l\le x\le u\}$ and its strict interior is $\operatorname{int}(\mathcal F)=\{x:l<x<u\}$. Write $g(x)=\nabla f(x)$ and $H(x)=\nabla^2 f(x)$, and $g_k=g(x_k)$, $H_k=H(x_k)$ along a sequence.

The standing assumption (p. 191): for the starting point $x_1$, the level set $\mathcal L=\{x\in\mathcal F: f(x)\le f(x_1)\}$ is compact, and $f$ is twice continuously differentiable on an open set $D\supseteq\mathcal F$.

The scaling vector $v(x)$ (Definition 2) has components $v_i=x_i-u_i$ if $g_i<0$ and $u_i<\infty$; $v_i=x_i-l_i$ if $g_i\ge0$ and $l_i>-\infty$; $v_i=-1$ if $g_i<0$ and $u_i=\infty$; $v_i=1$ if $g_i\ge0$ and $l_i=-\infty$. The scaling matrix is $D(x)=\operatorname{diag}(|v(x)|^{1/2})$, and $D_k=D(x_k)$. The system $D(x)^2g(x)=0$ is equivalent to the first-order optimality conditions of (1.1).

The reflective transformation $R$ (Fig. 6) folds $\mathbb R^n$ onto $\mathcal F$ coordinate by coordinate: a coordinate with one finite bound is reflected about it, and a coordinate with two finite bounds is folded periodically (a triangle wave between $l_i$ and $u_i$). The reflective path from $x$ in the direction $s$ is $p(\alpha)=R(x+\alpha s)-x$: it moves along $s$ and reverses the corresponding component of the direction whenever it meets a face. A breakpoint is a stepsize at which the path lies on the boundary.

The interior-reflective algorithm (Fig. 9), with $0<\sigma_l<\sigma_u<1$ and $\rho>0$, starts at $x_1\in\operatorname{int}(\mathcal F)$; at each step it chooses a descent direction $s_k$ and a stepsize $\alpha_k>0$ that is not a breakpoint and satisfies

$$f(x_{k+1})<f(x_k)+\sigma_l\big(\alpha_kg_k^{T}s_k+\tfrac12\alpha_k^2\min(s_k^{T}H_ks_k,0)\big)\qquad(3.4)$$

and either

$$f(x_{k+1})>f(x_k)+\sigma_u\big(\alpha_kg_k^{T}s_k+\tfrac12\alpha_k^2\min(s_k^{T}H_ks_k,0)\big)\qquad(3.5)$$

or $\alpha_k>\rho$; then $x_{k+1}=x_k+p_k(\alpha_k)$.

The directions $\{s_k\}$ are constraint-compatible (Definition 3) if $\{D_k^{-2}s_k\}$ is bounded, and consistent (Definition 4) if $s_k^{T}g_k\to0$ implies $D_kg_k\to0$.

Formalization targets

Goal: Theorem 8

If $\{x_k\}$ is generated by the algorithm of Fig. 9 and $\{s_k\}$ is both consistent and constraint-compatible, then

$$D_k^2g_k\to0\qquad\text{and}\qquad\alpha_k^2\min(s_k^{T}H_ks_k,0)\to0 .$$

No constants are involved; the statement is the paper's.

Milestones

1. The iterates stay in $\mathcal L$ and $f(x_k)$ strictly decreases (proof of Theorem 8, p. 207).
2. Theorem 3: constraint compatibility bounds the breakpoints $BR_k(j)=|v_{kj}|/|s_{kj}|$ away from zero.
3. Lemma 7, in its one-sided form: if $\alpha_k\to0$, then $f(x_{k+1})-f(x_k)\le\alpha_kg_k^{T}s_k+C\alpha_k^2$ eventually.
4. $\alpha_kg_k^{T}s_k\to0$ and $\alpha_k^2\min(s_k^{T}H_ks_k,0)\to0$ (proof of Theorem 8, p. 208).
5. $g_k^{T}s_k\to0$ for constraint-compatible directions (proof of Theorem 8, p. 208).

Companion results: Theorem 2 (the acceptable stepsize interval exists, so the algorithm is well defined), and Theorems 5 (1)–(2) and 6 (1)–(2) (the scaled steepest-descent directions $-D_k^2g_k$ and $-D_k^2\operatorname{sgn}(g_k)$ are constraint-compatible and consistent).

Significance

Theorem 8 is the global first-order convergence theorem of the interior-reflective approach. With Theorems 5 and 6 it shows that the simplest instance, scaled steepest descent along the reflective path, reaches first-order points from any strictly feasible start; the paper's later second-order and quadratic results for the trust-region variant are built on it. Constraint compatibility and consistency isolate exactly what a search direction must satisfy, so the theorem applies to any direction rule that can be checked against these two conditions.

The result has been proved since 1994 but, to our knowledge, not machine-checked. A formalization requires a precise model of the reflective path, which the paper describes by an algorithm (Fig. 4) and a coordinate formula (Fig. 6), and a careful treatment of points where the scaling degenerates. The formal statements also make explicit a point the printed text leaves loose: Lemma 7 is printed as an equality but only an inequality holds, and only the inequality is used.

Difficulty

The argument has the shape of a standard sufficient-decrease proof, but the step that is routine for straight-line searches fails here. The path is not a line: as $\alpha$ grows, components of the direction are reversed at breakpoints, so $f(x_k+p_k(\alpha))-f(x_k)$ is not $\alpha g_k^{T}s_k+O(\alpha^2)$ in general, since a reflected component changes the linear term by an amount of order $\alpha$. Lemma 7 must show that, for constraint-compatible directions, only components whose reflection decreases the linear term can be reflected at small steps, and the Taylor remainders must be controlled uniformly over a run, on a neighbourhood of the compact level set inside the open set where $f$ is $C^2$. The scaling also degenerates at the boundary, where $v$ vanishes; the iterates must be kept strictly interior for $D_k^{-2}$ to be meaningful.

Formalization scope

Points are EuclideanSpace ℝ (Fin n); the bounds are EReal vectors with $l_i\neq+\infty$, $u_i\neq-\infty$ and $l\le u$. The box and the level set are the published LewisTorczon.BoundPS.box and levelSet. The gradient is Mathlib's gradient, and $s^{T}H(x)s$ is the inner product of the derivative of the gradient map applied to $s$ with $s$. $D(x)$ is never formed as a matrix: $D^2g$, $Dg$, $D^{-2}s$ and $D^2\operatorname{sgn}(g)$ are written componentwise. The reflective path is $R(x+\alpha s)-x$ with $R$ the transformation of Fig. 6, which the paper describes as the same method as Fig. 4 in another notation (p. 199); "not a breakpoint" is the requirement that the new iterate be interior. Descent direction is footnote 3's: strict decrease along the path for all small $\alpha>0$. Sequences start at index 0, which is the paper's $x_1$. The standing compactness and smoothness assumption is carried as explicit hypotheses.

The goal does not assume $g_k^{T}s_k\to0$, $\alpha_k\to0$, or anything about breakpoints; a version of Theorem 8 that did, or one whose algorithm projected onto the box instead of reflecting, or whose run predicate no sequence can satisfy, would not be the paper's theorem. Lemma 7 keeps the paper's assumption $\alpha_k\to0$ and records the one-sided upper bound established by its proof. Theorem 3 uses the breakpoint distance in the direction of motion and applies its bound when that distance equals $|v_{kj}|/|s_{kj}|$.

A complete development needs Taylor's theorem with uniform remainder along piecewise linear paths in a box, and basic facts about the reflection $R$ (it maps into $\mathcal F$, is the identity on $\mathcal F$, and is continuous). These are reusable for any reflective or projected line search. Proofs of the milestones in any order are welcome, as are independent proofs of the companion results.

Selected references

• T. F. Coleman and Y. Li, On the convergence of interior-reflective Newton methods for nonlinear minimization subject to bounds, Mathematical Programming 67 (1994), 189–224. https://doi.org/10.1007/BF01582221
• T. F. Coleman and Y. Li, An interior trust region approach for nonlinear minimization subject to bounds, SIAM Journal on Optimization 6 (1996), 418–445. https://doi.org/10.1137/0806023
• R. M. Lewis and V. Torczon, Pattern search algorithms for bound constrained minimization, SIAM Journal on Optimization 9 (1999), 1082–1099 (source of the published box and level-set definitions reused here). https://doi.org/10.1137/S1052623496300507

Motivation

A Markov decision process describes repeated choices whose costs and subsequent states depend on the current state. Such models are used when a decision affects both today's expense and the options available tomorrow. Papadimitriou and Tsitsiklis studied how the computational difficulty of finding an optimal policy changes between stochastic and deterministic transitions. Their general finite-state problems are P-complete, while their deterministic cases admit highly parallel algorithms Papadimitriou and Tsitsiklis, 1987. The contrast makes the deterministic case a useful setting in which to isolate the precise graph problem hidden inside long-run optimization.

This mission concerns their infinite-horizon average-cost case. When transitions are certain, every decision is an arc in a directed graph. The long-run cost of a policy can be related to the mean cost of a cycle reachable from the initial state. That relation is the mathematical claim supporting the algorithm in the paper's Theorem 3, whose headline says that the deterministic average-cost problem is in NC Papadimitriou and Tsitsiklis, p. 446.

Setting

Let $S$ be a finite set of states and $s_0\in S$ the initial state. At each $s\in S$ there is a finite, nonempty decision set $D_s$. A decision $d\in D_s$ has a real cost $c(s,d)$ and moves the process with certainty to $\operatorname{next}(s,d)\in S$. All of these data are stationary: they do not change with time. A policy $\delta(s,t)$ chooses a decision for each state and each time $t=0,1,2,\ldots$. It generates a trajectory by $s_{t+1}=\operatorname{next}(s_t,\delta(s_t,t))$. The corresponding directed graph has a state for each node and a decision for each arc. It may contain loops and parallel arcs, since different decisions can lead to the same next state.

The paper prints the finite average with $T+1$ cost terms and denominator $T$:

$$a_T^\delta(s_0)=\frac{1}{T}\sum_{t=0}^{T}c(s_t,\delta(s_t,t)).$$

A time-dependent policy's averages may fail to converge. We use the upper limit $g^\delta(s_0)=\limsup_{T\to\infty}a_T^\delta(s_0)$ and optimize over all policies, $g^*(s_0)=\inf_\delta g^\delta(s_0)$. A state $u$ is reachable if some finite walk of decision arcs goes from $s_0$ to $u$. A simple cycle $C$ is a positive-length closed sequence of decision arcs with distinct states before it returns to its start; its mean cost is $\operatorname{mean}(C)=c(C)/|C|$. A loop is a one-arc simple cycle.

For states $u,v$, the min-plus adjacency entry $A_{uv}$ is the least cost of a decision arc from $u$ to $v$, or $+\infty$ when no such arc exists. A min-plus product uses addition in place of multiplication and minimum in place of addition. Thus $(A^k)_{uv}$ represents the least cost of a $k$-arc walk from $u$ to $v$, when such a walk exists Papadimitriou and Tsitsiklis, pp. 445–446.

Formalization targets

Reachable cycles

The first target identifies the value of the original policy optimization problem:

$$g^*(s_0)=\min_{\substack{C\text{ simple cycle}\\C\text{ reachable from }s_0}}\operatorname{mean}(C).$$

It also states that a policy attains this value with convergent finite averages. The milestone for following a reachable cycle gives the attainable direction; the milestone saying that no policy can improve the least mean gives the reverse direction. The latter is formulated with $\liminf$, so it applies even when a policy's averages oscillate.

Min-plus calculation

The second target identifies the finite graph calculation used in the paper:

$$g^*(s_0)=\min_{\substack{u\text{ reachable from }s_0\\1\leq k\leq |S|\\(A^k)_{uu}<+\infty}}\frac{(A^k)_{uu}}{k}.$$

The milestones establish what a min-plus power says about decision walks and why closed walks of lengths from $1$ through $|S|$ recover the least simple-cycle mean. The restriction to reachable $u$ is essential: a cheap cycle in a disconnected component cannot be used from $s_0$.

Significance

The result reduces optimization over infinitely many decision times and all state-and-time policies to finitely many closed-walk calculations. It also guarantees that an optimal long-run value is realized by a trajectory with a genuine limiting average, despite the nonconvergence possible for other policies. The finite formula lets one determine the value by comparing graph quantities indexed by states and lengths; it is the correctness statement beneath the paper's parallel algorithm Papadimitriou and Tsitsiklis, p. 446.

Formalizing the identity creates a reusable bridge between deterministic decision processes, weighted directed walks and min-plus powers. Related proved tropical-algebra results on maximum cycle means use dense matrices and a max-plus convention, rather than the reachable, possibly missing-arc, minimum-cost process here; for example, the platform's TropicalLA.tpow_isGreatest concerns greatest walk weights. The present mission keeps the policy optimum and reachability explicit. The paper proves the result mathematically; these Lean statements are open proof targets in the proposal.

Difficulty

An arbitrary policy can keep changing its choices at repeated visits to the same state. Its averages can oscillate, so one cannot simply assume that its infinite trajectory becomes periodic or that its printed limit exists. The lower-bound claim must apply to every such trajectory. There is a second distinction between a closed walk and a simple cycle: a diagonal min-plus entry allows repeated states, whereas the cycle characterization is stated using simple cycles. Finally, an unrestricted matrix calculation would include cycles unreachable from the chosen initial state.

Formalization scope

Lean represents the general finite stationary deterministic process in its own definition, then defines policies, finite walks, simple cycles, average costs and min-plus powers on top of it. Decisions are arcs, so parallel arcs remain distinguishable; $A_{uv}$ takes their least cost and uses WithTop ℝ for a missing arc. Decision sets are explicitly nonempty because a policy has to make a choice at every state. The finite state set is automatically nonempty once $s_0$ is supplied. Policy time starts at zero. The printed $T+1$ terms divided by $T$ are retained; Lean's $T=0$ quotient is zero and has no effect on the limit. The optimum is the infimum over all policies $\delta(s,t)$, not a quantity defined by cycles or by stationary policies. Finite states and finite decision sets bound the one-step costs and hence the averages; this gives real limsup and infimum their intended values.

The paper's Theorem 3 asserts membership in NC. This mission formalizes the exact optimization identity that makes that algorithm correct. Its processor count and parallel-time bound are outside the scope, as are membership in P, log-space computability of reductions, PSPACE membership and the paper's Corollaries 1–2. Contributions to the finite-walk and min-plus lemmas, the lower bound for arbitrary policy paths, and the cycle-attainment statement are all needed; the graph definitions can be reused in other deterministic control problems.

Selected references

• Christos H. Papadimitriou and John N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 1987, pp. 441–450. DOI.

Motivation

A solution of a scenario optimization program is chosen after observing finitely many uncertain constraints. Its future reliability depends on constraints that were not sampled. The usual advance question asks how many samples are needed to make every output reliable. Campi and Garatti instead ask what can be certified after solving the program, when the number of sampled constraints that actually determined its solution is visible. Their wait-and-judge result uses that observed number to set a violation threshold. This mission concerns their extension from convex programs in finite-dimensional spaces to programs over an arbitrary decision set, with no convexity requirement.

The generic extension matters when a dimension bound on the number of influential constraints is unavailable. A decision may be a combinatorial object, a function, or an element of an infinite-dimensional space. The paper allows the support count to range from zero to the full sample size $N$, and its threshold includes the case of $N$ support constraints. The paper's Section 6 gives the model and its two probability guarantees.

Setting

Let $S$ be a set of decisions. A subset $X\subseteq S$ is the domain; a real function $f:S\to\mathbb R$ is the cost. An uncertain outcome $\delta$ belongs to a measurable space $\Delta$ with probability measure $P$, and imposes a constraint set $X_\delta\subseteq S$. For a sample $\omega=(\delta^{(1)},\ldots,\delta^{(N)})$ of $N$ independent outcomes, the program minimizes $f(x)$ over $x\in X$ that belongs to every sampled $X_{\delta^{(i)}}$. The sample law is $P^N$. There is no algebraic or topological condition on the feasible sets or on $f$.

A fixed finite sequence of real tie-break functions is minimized lexicographically after the original cost. This selects one solution $x_N^*(\omega)$ whenever the program has a selected minimizer. Assumption 1 requires existence and uniqueness for every finite sample, including the empty one. A sampled constraint is a support constraint if removing it changes this selected solution. The number of support constraints is $s_N^*(\omega)$. Assumption 2 says that, with probability one, keeping only the support constraints gives the same selected solution. Both assumptions are part of the source's generic setting; they are substantive restrictions even though the sets and cost are otherwise arbitrary.

The violation of a decision is $V(x)=P\{\delta:x\notin X_\delta\}$. Thus $V(x_N^*)$ is the probability that a fresh constraint rejects the computed solution. Since the solution and support count depend on the sample, the wait-and-judge event uses a threshold function $\varepsilon$ evaluated at the observed count, $\{V(x_N^*)>\varepsilon(s_N^*)\}$. For each $k\ge0$, the paper also uses a generalized distribution function $F_k(v)=P^k\{V(x_k^*)\le v,\ s_k^*=k\}$. It need not have total mass one.

Formalization targets

Variational bound, Theorem 3

For any $N\ge1$ and any $[0,1]$-valued $\varepsilon$ on $\{0,\ldots,N\}$, let $\gamma^*$ be the infimum of feasible values $q(1)$ over real polynomials of degree at most $N$ satisfying

$$\frac{q^{(k)}(t)}{k!}\ge {N\choose k}t^{N-k}{\bf1}_{[0,1-\varepsilon(k))}(t),\qquad 0\le k\le N,\quad 0\le t\le1.$$

The goal is the paper's Theorem 3:

$$P^N\{V(x_N^*)>\varepsilon(s_N^*)\}\le\gamma^*.$$

The polynomial value retains the full dependence on the chosen threshold function. The source prints an extraneous $d$ in Theorem 3's range for $k$; its generic setting and variational problem use $0\le k\le N$.

Explicit confidence bound, Theorem 4

For $0<\beta<1$, the paper's Theorem 4 defines $t(k)\in(0,1)$ as the unique root of

$$\frac{\beta}{N+1}\sum_{m=k}^{N}{m\choose k}t^{m-k}-{N\choose k}t^{N-k}=0\qquad(0\le k<N).$$

With $\varepsilon(k)=1-t(k)$ for $k<N$ and $\varepsilon(N)=1$, its conclusion is

$$P^N\{V(x_N^*)>\varepsilon(s_N^*)\}\le\beta.$$

The terminal value $\varepsilon(N)=1$ is essential because the paper gives examples with $s_N^*=N$ and $V(x_N^*)=1$.

Significance

Theorem 3 makes the observed support count a usable statistic for assessing the solution's future constraint violation without a dimension bound. Theorem 4 turns it into a certificate at any chosen confidence parameter $\beta$. The confidence threshold depends on the count seen after the program is solved. These statements do not claim that every generic program satisfies Assumptions 1–2; they say what follows for programs that do.

A formal development must make the statistical objects and the analytic value agree exactly: the solution must come from the feasible set and the fixed tie-break rule, the support count must record changes of solution, and $\gamma^*$ must be the value of the derivative-constrained polynomial problem. The reusable outputs include the generic scenario model, its generalized violation distributions, and the finite moment and dual formulations. The statements are known results of Campi and Garatti; this mission asks for machine-checked proofs of those results and their selected intermediate claims.

Difficulty

The observed support count is data-dependent. Conditioning on $s_N^*=k$ therefore cannot be treated as conditioning on a fixed subset of $k$ sample coordinates. Symmetry across possible support subsets must agree with the selected solution under removal of nonsupport constraints. Assumption 2 is what rules out a degenerate change of solution when only support constraints remain. In the generic setting the possible count grows with $N$, so the distributional characterization has one measure $F_k$ for every $k\ge0$ and moment equations for every sample size. The resulting infinite family must still be related to the finite degree-$N$ polynomial value in (31). No convexity or finite-dimensional geometry is available to supply a fixed support bound.

Formalization scope

Lean represents the decision set by an arbitrary type $S$, with a measurable structure only to state the paper's implicit measurability convention. Samples are functions Fin N → Δ with zero-based indices and product law Measure.pi. The published generic violation definition is reused. The domain, constraint family, cost, finite lexicographic tie-break, selected solution, support set, and $F_k$ are defined locally. A Nonempty S instance provides an unused fallback value to the total solution selector; Assumption 1 already implies that $S$ is nonempty.

The source takes measurability for granted in a footnote. Here the constraint relation is jointly measurable, every solution map is measurable, and each support event is measurable. These pins assign probabilities to the events the paper uses. The $F_k$ are finite measures on $\mathbb R$, so the paper's Stieltjes integrals are represented as integrals over $(\varepsilon(k),1]$ or $[0,1]$ against those measures. The polynomial class $\mathcal P_N$ means degree at most $N$, matching the $N+1$ coefficients in (36). The value $\gamma^*$ is a real infimum; a separate sanity proof gives a feasible polynomial and a zero lower bound on all feasible values.

The goal retains Assumptions 1–2 and states the actual tail bound. It does not assume the moment equations or a favorable value of $\gamma^*$, and no support count is fixed in advance. Contributions toward the distributional decomposition, the moment equations, the finite weak-duality inequality, the polynomial identity, and the explicit-root theorem are within scope.

Selected references

• M. C. Campi and S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming, 2018. DOI: 10.1007/s10107-016-1056-9. The mission uses the authors' accepted manuscript, especially Sections 6–7 and Theorems 3–4.

Motivation

In Stackelberg network pricing a leader sets prices on some resources, and a follower then buys the cheapest structure available to them, paying the leader for the priced resources they use. The Stackelberg Minimum Spanning Tree problem, introduced by Cardinal, Demaine, Fiorini, Joret, Langerman, Newman and Weimann (Algorithmica 2011), is the version in which the follower buys a minimum spanning tree. The best known approximation factors for it are those of uniform pricing, which gives every priced edge the same price (Berbeglia–Joret, p. 21).

Independently, revenue management studies assortment optimisation: a seller chooses which products to offer, and customers choose among the offered products according to a discrete choice model. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) analyse the revenue-ordered heuristic (offer every product whose revenue is at least some threshold) under any regular choice model, and prove tight approximation bounds.

§4.6 of that paper shows that the two problems are the same problem: a Stackelberg Matroid pricing instance is an assortment problem under a regular choice model, and uniform pricing is the revenue-ordered heuristic on that model. The bounds of Cardinal et al. on uniform pricing thus become special cases of the general bounds on revenue-ordered assortments. This mission formalizes that correspondence (Theorem 4.16).

Setting

Choice model. Let $\mathcal C$ be a finite set of products. A system of choice probabilities assigns to each offered set $S\subseteq\mathcal C$ and product $x$ a probability $\mathcal P(x,S)$, with no-purchase probability $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. It is regular if (i) all probabilities are nonnegative, (ii) $\mathcal P(x,S)=0$ for $x\notin S$, (iii) $\sum_{x\in S}\mathcal P(x,S)\le1$, and (iv) $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$. With revenues $r:\mathcal C\to\mathbb R_{>0}$, $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)r(x)$ and $\mathrm{OPT}=\max_S\mathrm{rev}(S)$. The revenue-ordered assortment generated by $y$ is $\{y'\in\mathcal C:r(y')\ge r(y)\}$.

Greedy algorithm. Given a family of independent sets, a linear ordering $L$ and a set $F$, $\mathrm{greedy}(F,L)$ scans $F$ in the order induced by $L$, starting from $\emptyset$, and adds each element that keeps the current set independent.

Stackelberg Matroid problem. An instance is a matroid $M=(E,\mathcal X)$, a bipartition $E=R\sqcup B$ into red and blue elements, and red costs $c:R\to\mathbb R_{>0}$; some base of $M$ lies inside $R$. The leader chooses prices $p:B\to\mathbb R_{>0}$. The customer buys a minimum-weight base by running greedy on $R\cup B$ with an ordering $L^*$ that is non-decreasing in weight ($c$ on $R$, $p$ on $B$) and puts blue elements first on ties. The leader earns $\mathrm{rev}_{\mathrm{Stack}}(p,L^*)=\sum_{e\in B\cap\mathrm{greedy}_M(R\cup B,L^*)}p(e)$.

The assortment instance. Let $c_1<\dots<c_k$ be the distinct red costs. Products are $\mathcal C=B\times\{c_1,\dots,c_k\}$ with $r((e,q))=|B|\,q$. The auxiliary matroid $M'$ on $R\cup\mathcal C$ declares $X$ independent when it holds at most one pair $(e,q)$ per blue $e$ and $(R\cap X)\cup\{e:(e,q)\in X\}$ is independent in $M$. With an ordering $L$ of $R\cup\mathcal C$ that is non-decreasing in cost and puts products before red elements on ties, $\mathcal P((e,q),S)=1/|B|$ if $(e,q)\in\mathrm{greedy}_{M'}(R\cup S,L)$ and $0$ otherwise.

Formalization targets

Goal: Theorem 4.16 (p. 24)

For the instance above, with $B\ne\emptyset$ and every admissible $L$:

$$\mathcal P\ \text{is regular},\quad r>0,\qquad \max_{S\subseteq\mathcal C}\mathrm{rev}(S)=\max_{p>0,\ L^*}\mathrm{rev}_{\mathrm{Stack}}(p,L^*),$$

and uniform pricing corresponds to revenue-ordered assortments: for each $c_i$ some revenue-ordered assortment earns the revenue of the uniform price $c_i$, and every revenue-ordered assortment earns the revenue of some uniform price $c_i$.

Milestones

1. Lemma 4.14 (p. 23): for $F\subseteq F'$, $|\mathrm{greedy}_M(F',L)|\ge|\mathrm{greedy}_M(F,L)|$ and $F\cap\mathrm{greedy}_M(F',L)\subseteq\mathrm{greedy}_M(F,L)$.
2. Property (14) (p. 31): orderings agreeing on a block partition make greedy pick the same number of elements per block.
3. Lemma 4.15 (p. 23): the Stackelberg revenue does not depend on the compatible ordering.
4. $M'$ is a matroid (p. 32).
5. Regularity of $\mathcal P$ (pp. 32–33).
6. $\mathrm{rev}(S)$ equals the Stackelberg revenue of $p_S(e)=\min\{q:(e,q)\in S\}$ (pp. 33–34).
7. Rounding prices up to the cost levels does not decrease revenue (p. 34).
8. For prices in $\{c_1,\dots,c_k\}\cup\{+\infty\}$, $\mathrm{rev}(S_p)$ equals the Stackelberg revenue of $p$ (pp. 34–35).

Significance

Theorem 4.16 transfers every guarantee for revenue-ordered assortments under regular models to uniform pricing in Stackelberg Matroid pricing. Specialising Theorems 3.1, 3.2 and 3.3 of the paper through it gives exactly the three bounds on uniform pricing proved by Cardinal et al. for Stackelberg Minimum Spanning Tree (Theorem 3 of their paper), which those authors showed to be tight (p. 24). It also places uniform pricing inside a general picture: it is a threshold policy for a regular choice model whose purchase probabilities come from a matroid greedy algorithm, and the paper notes that the argument extends to polymatroids.

The result is proved in the paper, with two steps left to the reader ($M'$ is a matroid) or justified briefly (rounding prices). No machine-checked proof exists. A formalization also produces a reusable greedy algorithm on finite matroids with its monotonicity properties (Lemma 4.14, (14)), which Mathlib at the pinned revision does not have.

Difficulty

The obvious argument identifies the customer's run of greedy on $(M,R\cup B)$ with the run of greedy on $(M',R\cup S)$ step by step. That identification fails as stated: the choice probabilities are defined with one fixed ordering $L$ of $R\cup\mathcal C$, while the customer's ordering $L^*$ is any ordering compatible with the prices, and ties among blue elements of equal price, or between a product and a red element of equal cost, may be broken differently. Equality of revenues therefore needs the tie-independence property (14) applied to $M'$ as well as to $M$, which in turn needs $M'$ to be a matroid. A second gap is axiom (iv) for the no-purchase option: it requires that offering more products never decreases the number of products greedy selects, which is Lemma 4.14 (i)–(ii) for $M'$ combined, not a pointwise statement. Finally, the paper's "$+\infty$" price must be handled with the red base: without a base inside $R$, a blue element priced above all costs can still be bought and the optimum is unbounded.

Formalization scope

• Elements and orderings. The matroid is a Mathlib Matroid α; $R$, $B$ are Finset α with $R\cup B$ equal to the ground set; costs and prices are functions α → ℝ, used only on $R$ and $B$. A linear ordering is a duplicate-free List covering the set; greedy on $F$ scans the whole list and skips elements outside $F$, so $F$ is never re-sorted.
• Greedy is defined for an arbitrary independence predicate on finite sets, so that it applies to $M'$ before $M'$ is shown to be a matroid.
• Customer model. Compatibility (15a)–(15b), including blue priority on ties, is part of the definition of an admissible customer ordering. The red base is a field of every instance.
• Assortment instance. Elements of $R\cup\mathcal C$ live in α ⊕ (α × ℝ). The paper's conditions (1)–(2) for $M'$ contain two typos (a missing "$\in X$" and $\mathcal X$ for $X$); the intended conditions are formalized. The price $+\infty$ is the real number $1+\sum_{f\in R}c(f)$, strictly above every red cost.
• Goal shape. The theorem is stated for the explicit instance of the proof, for every admissible $L$. The optimum of the Stackelberg side is a maximum (IsGreatest) over positive real prices and all compatible customer orderings. Cost levels are quantified as elements of the set of red costs rather than by index.
• Ruled out. An existential statement ("some regular instance has the same optimum") is met by a single product with revenue $\mathrm{OPT}_{\mathrm{Stack}}$ and is not this theorem; so is a customer model without tie-breaking, a formalization without the red base, or Lemma 4.14 only for $F=F'$.

Contributions welcome: proofs of Lemma 4.14 and (14) for Mathlib matroids (reusable beyond this mission), the matroid property of parallel extensions such as $M'$, and the three revenue identities.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019 (Algorithmica, 2020). https://arxiv.org/abs/1606.01371
• J. Cardinal, E. D. Demaine, S. Fiorini, G. Joret, S. Langerman, I. Newman and O. Weimann, The Stackelberg Minimum Spanning Tree Game, Algorithmica 59(2):129–144, 2011. https://doi.org/10.1007/s00453-009-9299-y
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Vol. B, Algorithms and Combinatorics 24, Springer, 2003 (matroids and the greedy algorithm). https://link.springer.com/book/9783540443896