Operations Research

Motivation

Retailers that carry a limited range of products often know something about a customer before choosing which of those products to display. The customized assortment problem asks which products to carry when the displayed assortment may be tailored to the arriving customer's type. This separates the first-stage capacity decision from the later offer decision. El Housni and Topaloglu study the problem under a mixture of multinomial logit choice models and develop an approximation framework for it in their SSRN paper. This mission isolates their structural guarantee for Augmented Greedy, Theorem 4.2 of the PDF version dated 7 December 2021. The theorem identifies the revenue recovered from customer types whose optimal personalized offers agree with a chosen product subset.

The paper contrasts this setting with ordinary assortment optimization, where every type sees the same products. Its later approximation results use the structural guarantee here as a component. The classical comparison is the cardinality-constrained greedy bound for monotone submodular functions, associated with Nemhauser, Wolsey and Fisher (1978). The paper's Appendix B gives an instance in which the customized revenue function lacks global submodularity, so that classical result does not apply directly. El Housni and Topaloglu, §§4 and App. B.

Setting

Let $N=\{1,\ldots,n\}$ be a finite product set. Product $i$ has positive revenue $r_i$, and products are indexed with $r_1\ge\cdots\ge r_n>0$. Let $M=\{1,\ldots,m\}$ be customer types. A type-$j$ customer arrives with probability $\theta_j\ge0$, with $\sum_{j\in M}\theta_j=1$, and assigns each product $i$ a nonnegative preference weight $v_{ij}$. The no-purchase option has weight one. Offering an assortment $T\subseteq N$ to that customer gives MNL expected revenue

$$\operatorname{Rev}_j(T)= \frac{\sum_{i\in T}r_i v_{ij}}{1+\sum_{i\in T}v_{ij}}.$$

If the retailer initially carries only $S\subseteq N$, it can still choose the best offer to each customer type. Thus $f_j(S)=\max_{T\subseteq S}\operatorname{Rev}_j(T)$. For $C\subseteq M$, write $f^C(S)=\sum_{j\in C}\theta_j f_j(S)$, and abbreviate $f=f^M$. The first-stage capacity is $K$; an optimal solution $S^*$ of CAP maximizes $f(S)$ among sets with at most $K$ products. These definitions and the standing data assumptions are stated in §2 and §4 of the paper.

For each product $i$, the prefix $V_i=\{1,\ldots,i\}$ contains products at least as early in the revenue ordering. Greedy starts at the empty set, repeatedly adds an available product that maximizes the new objective value, and stops at cardinality $k$ or when the prefix is exhausted. Augmented Greedy runs Greedy on $V_i$ for each $i$, using $S\mapsto\sum_{j\in C}\theta_j\min(f_j(S),r_i)$, and returns whichever candidate has the greatest $f^C$ value. Both stages may break ties arbitrarily. El Housni and Topaloglu, §4.1.

For type $j$, use the optimal personalized assortment $S_j^*=\{i\in S^*:r_i\ge f_j(S^*)\}$, characterized by Lemma E.1. A type $j\in C$ is complete with respect to $P\subseteq N$ when $P\cap S_j^*=P\cap S^*$; let $C_P$ collect these types. The threshold choice matters because zero-weight products can be present in other optimal offers without helping a customer. El Housni and Topaloglu, Definition 4.1 and App. E.

Formalization targets

Theorem 4.2: complete-type revenue

For every $C\subseteq M$, $P\subseteq N$, $k$ with $|P\cap S^*|\le k$, and every output $\Delta$ of Augmented Greedy on $C,k$,

$$f^C(\Delta)\ge(1-1/e)\,f^{C_P}(P\cap S^*).$$

This is the mission goal, the structural performance statement of Theorem 4.2, p. 11. It does not assert a constant-factor approximation to all of CAP: it identifies the contribution from complete customer types.

Supporting targets

The milestone list follows the results used with this bound: monotonicity of $f_j$ from Appendix C; the MNL threshold assortment of Lemma E.1; submodularity of $S\mapsto\min(f_j(S),r_i)$ on $V_i$ from Lemma 4.3; and the cited $1-1/e$ Greedy guarantee for a nonnegative monotone submodular objective. The greedy milestone compares its output against every feasible set of cardinality at most $k$.

Significance

The theorem says that one algorithmic output captures a fixed fraction of the benchmark supplied by complete types, despite the absence of global submodularity of $f$. It connects the local behavior of truncated type revenues to the full customized assortment objective. The paper uses this result in the development of later algorithms; without it, the standard submodular greedy theorem gives no immediate conclusion for CAP. El Housni and Topaloglu, §§4–5.

The mathematical results are proved in the 2021 paper. The formalization work here is to give machine-checkable statements for the objective, the algorithm with all its legal tie choices, and the four supporting targets, then supply proofs. The MNL revenue formula is already available as a published platform definition; the local CAP and algorithm definitions specify the extra model needed by this theorem. A completed development could also support later CAP missions that use the same threshold and submodularity properties.

Difficulty

The tempting argument applies the classical greedy guarantee directly to $f$, since $f$ increases when more products are carried. Appendix B of the paper shows that this fails: even for one customer type, $f$ need not be submodular. Restricting the ground set to a revenue prefix and truncating each $f_j$ at that prefix's revenue level changes the submodularity question, but the final guarantee must still concern the untruncated $f^C$ objective. The threshold condition in the definition of $C_P$ is what makes that comparison meaningful. El Housni and Topaloglu, App. B, Lemma 4.3 and Theorem 4.2.

Formalization scope

Products and types are Fin n and Fin m; their zero-based Lean indices correspond to the paper's indices plus one. Assortments and type groups are finite sets. The model assumes $r_i>0$, $v_{ij}\ge0$, $\theta_j\ge0$, $\sum_j\theta_j=1$, and decreasing revenue order. The no-purchase weight is exactly one. CAP and personalized revenue use maxima over nonempty finite powersets, so empty input sets have their intended value rather than an arbitrary real supremum. The theorem keeps the source's optimality assumption on $S^*$, even though its particular inequality uses less.

The Greedy predicate describes each successive maximizer and the exact stopping rule. Augmented Greedy requires a Greedy output at every prefix and an $f^C$-maximizing choice among them. Thus the output is constrained by the printed algorithm, and the statement covers every tie-break. The type-$j$ assortment is defined from $S^*$ by the Lemma E.1 threshold, rather than supplied as a free set. These choices rule out a size-only output condition, an arbitrarily chosen $S_j^*$, a vacuous run predicate, and real supremum defaults. The target includes the corner cases $k=0$, $C=\varnothing$, and $P\cap S^*=\varnothing$, where its right side is zero. Arrival probabilities summing to one force $m\ge1$; Augmented Greedy has an output only when at least one product exists.

The reusable parts are the MNL threshold characterization, finite-set submodularity and the general Greedy bound. Contributions toward those lemmas, the paper's case analysis for Lemma 4.3, and the final structural theorem are in scope. Runtime claims, the paper's later logarithmic approximation theorems and its computational experiments are outside this mission.

Selected references

• Omar El Housni and Huseyin Topaloglu, Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models: Value of Personalized Assortments, SSRN 3830082, version of 7 December 2021; published as Operations Research 71(4), 2023. SSRN preprint. The mission's numbering and page citations use the pinned 2021 PDF.
• George L. Nemhauser, Laurence A. Wolsey and Marshall L. Fisher, An Analysis of Approximations for Maximizing Submodular Set Functions—I, Mathematical Programming 14, 265–294, 1978. DOI.

Motivation

Posted prices turn an offline allocation problem into a sequential choice process: each agent sees a menu of outcomes and prices, then chooses an outcome without revealing its full valuation. The balanced prices framework of Dütting, Feldman, Kesselheim, and Lucier gives welfare guarantees by comparing the revenue collected from an allocation with the welfare that remains feasible after it. Its appeal is that the comparison can be checked in a deterministic full-information setting before any probability distribution over valuations enters the analysis. Dütting et al., 2020

One valuation class at a time would make that framework difficult to reuse. Combinatorial auction valuations are often built by taking pointwise maxima of simpler valuations or by adding values from separate markets. Section 5 of the paper asks whether a price construction balanced for the simple class remains balanced after these operations. Theorem 5.3 gives the maximum closure result; Theorem 5.4 gives addition across markets. Appendix B extends both to the weaker balancing condition used elsewhere in the paper. Dütting et al., 2020, §5 and Appendix B

Setting

There are $n$ agents in a fixed order. Agent $i$ receives an outcome $x_i$ from a space $X_i$ containing a null outcome. A profile $x=(x_i)_i$ is feasible when it lies in $\mathcal F$. The model assumes downward closure: removing the outcomes of any group of agents from a feasible profile keeps it feasible. For a set of agents $S$, write $x_S$ for the profile retaining $x_i$ on $S$ and assigning the null outcome elsewhere. The prefix $x_{[i-1]}$ retains only the agents before $i$. Dütting et al., 2020, §2

A valuation profile $v$ assigns each agent a function $v_i:X_i\to\mathbb R$. The welfare of $x$ is $v(x)=\sum_i v_i(x_i)$. Every base valuation takes values in $[0,1]$, the normalization stated in §2. For any set $S$ of profiles, $v(\operatorname{OPT}(v,S))$ denotes the best welfare achievable in $S$. An allocation rule ALG chooses a feasible profile from a valuation profile. A pricing rule assigns a nonnegative, possibly infinite price $p_i(x_i\mid y)$ to outcome $x_i$ when the partial profile is $y$; an infeasible extension has infinite price. Dütting et al., 2020, pp. 547–548

An exchange-compatible family $(\mathcal F_x)_{x\in X}$ specifies a set of comparison profiles for each profile $x$. It is exchange compatible when replacing any one coordinate of $x$ by the corresponding coordinate of any $y\in\mathcal F_x$ gives a feasible profile. This property is required for every $x$ in the full outcome space. A rule $p^v$ is $(\alpha,\beta)$-balanced for valuation $v$, ALG, and that family, for constants $\alpha>0$ and $\beta\ge0$ (Definition 3.1), when both inequalities hold for every feasible $x$ and every $x'\in\mathcal F_x$:

$$\frac{v(\operatorname{ALG}(v))-v(\operatorname{OPT}(v,\mathcal F_x))}{\alpha} \le \sum_i p_i^v(x_i\mid x_{[i-1]}), \qquad \sum_i p_i^v(x'_i\mid x_{[i-1]}) \le \beta v(\operatorname{OPT}(v,\mathcal F_x)).$$

The maximum extension $V_i^{\max}$ of a base valuation space $V_i$ consists of nonempty finite pointwise maxima of elements of $V_i$. A base profile $\tilde v$ supports an extended profile $v$ at $x$ if $\tilde v_i\le v_i$ at every outcome and $\tilde v_i(x_i)=v_i(x_i)$ for every agent. ALG is consistent when $\tilde v(\operatorname{ALG}(\tilde v))\ge\tilde v(\operatorname{ALG}(v))$ whenever $\tilde v$ supports $v$ at $\operatorname{ALG}(v)$. The optimal allocation rule has this property by Lemma 5.2. Dütting et al., 2020, p. 554

Formalization targets

Closure under maxima

The goal is Theorem 5.3. Given one exchange-compatible family and a collection $(p^w)_{w\in V}$ balanced for every base profile, consistency of ALG preserves the same constants for every extended profile and every corresponding supporting base profile:

$$v\in V^{\max},\quad \tilde v\in V\text{ supports }v\text{ at }\operatorname{ALG}(v) \quad\Longrightarrow\quad p^{\tilde v}\text{ is }(\alpha,\beta)\text{-balanced for }v.$$

The milestone list records the welfare supremum comparison and the two price inequalities in the paper's proof. The family $\mathcal F_x$ remains the same for all base and extended profiles. Dütting et al., 2020, Theorem 5.3 and proof

Closure under addition and weak balancedness

Theorem 5.4 treats $m$ separate allocation problems. The joint outcome and feasible set are products; values and prices add across components; ALG applies each component's rule. It asserts balancedness with the same $\alpha$ and $\beta$. Appendix B changes the second balancedness bound to $\beta_1v(\operatorname{OPT}(v,\mathcal F_x))+\beta_2v(\operatorname{ALG}(v))$ and requires strong consistency for maximum closure. Theorems B.2 and B.3 preserve $\alpha,\beta_1,\beta_2$ under maxima and addition, respectively. Dütting et al., 2020, Theorems 5.4, B.2, B.3

Significance

The maximum closure theorem lets a balanced-price construction for a simple valuation class cover finite maxima of that class without worsening its balancing constants. The addition theorem lets separately priced markets be combined by summing prices. Together these two operations account for the XOS composition discussed immediately after Theorem 5.4; the paper uses the results to connect its general framework to combinatorial auctions and multidimensional matroid settings. Dütting et al., 2020, p. 555

These results have paper proofs. The work here is to state their exact deterministic content in Lean so later formalizations of the price constructions can import the closure theorems. The definitions of supporting valuations, exchange-compatible families, and extended-real prices are reusable beyond this mission. The companion statements keep the product-market and weak-balancedness variants alongside the central theorem, while their proofs remain to be formalized.

Difficulty

For maximum closure, the prices are indexed by a base profile $\tilde v$ but must be balanced for a different profile $v$ that is pointwise larger. A supporting profile agrees with $v$ only at ALG's outcome $\operatorname{ALG}(v)$, while condition (a) refers to $\operatorname{ALG}(\tilde v)$, an outcome ALG chooses for a different input, and both conditions refer to optimal welfare over $\mathcal F_x$, where $\tilde v$ and $v$ can differ. Balancedness of $p^{\tilde v}$ for $\tilde v$ therefore says nothing about $v$ on its own; without a hypothesis tying ALG's choices for $v$ and $\tilde v$ together the statement is false, which is why consistency (Definition 5.1) is part of the theorem. The formal statement must keep the real-valued optimum meaningful for maxima of base valuations, so the $[0,1]$ normalization of §2 is carried through to $V^{\max}$. Dütting et al., 2020, Definition 5.1 and Theorem 5.3

For addition, a direct product of the component comparison families has an edge case: a component family can be empty while another is nonempty. The paper's displayed product family then makes the lower balancedness inequality too strong. The theorem statements ask for an exchange-compatible family to exist, as the printed theorems do; they do not require that failing product family. This discrepancy is recorded for review. Dütting et al., 2020, proof of Theorem 5.4

Formalization scope

Agents and markets use zero-based finite indices; the paper writes agent indices from one. A profile's prefix contains exactly the agents with smaller indices. Valuations are functions to $\mathbb R$ with base values in $[0,1]$. The maximum extension uses a nonempty finite set of base functions, so its maximum is defined at every outcome. Optimal welfare is a real supremum; bounded valuations keep it finite, and the empty set has value zero. Prices are extended nonnegative reals so $+\infty$ is retained. The lower balancedness inequality embeds its real right side using ofReal, which handles a negative lower bound consistently with nonnegative prices. The upper inequality keeps the price sum in extended reals.

The maximum theorem quantifies over every extended profile and every supporting base profile, including genuinely new maxima. It keeps one exchange-compatible family for all valuations. The maximum-closure theorems require every base price to satisfy the pricing-rule condition and conclude it for the supporting price. ALG feasibility is assumed on $V^{\max}$, which contains the base profiles. The product theorems construct joint outcomes, additive values, componentwise ALG, and summed prices from the component data; they do not admit an unrelated joint allocation rule. Downward closure and a zero price for the null outcome at feasible partial allocations are included for the product statements. The latter is a disclosed assumption satisfied by the paper's pricing examples and needed to handle empty component families. No distribution or posted-price run is part of this deterministic mission. Lemma 5.2 and the strong-consistency companion take an optimal rule to be one that attains the welfare supremum over $\mathcal F$ on every profile in $V^{\max}$, the profiles to which Definitions 5.1 and B.1 apply it; the product companions additionally conclude that the summed prices form a pricing rule (infinite off $\mathcal F$). Their ALG feasibility premise concerns the component profiles supplied in the theorem.

The development needs finite dependent products and sums, finite maxima, real suprema of bounded sets, and extended nonnegative arithmetic. Contributions proving the three maximum-closure milestones, the goal, or the product-market companions are all within scope. A proof that specializes the supporting profile to $\tilde v=v$ would lose the intended maximum extension and does not satisfy the goal's universal quantification.

Selected references

• P. Dütting, M. Feldman, T. Kesselheim, and B. Lucier, Prophet Inequalities Made Easy: Stochastic Optimization by Pricing Nonstochastic Inputs, SIAM Journal on Computing 49(3):540–582, 2020. DOI: 10.1137/20M1323850.

Motivation

Stochastic optimization methods often see only noisy gradients. For a nonconvex objective, a useful guarantee is that an output point has a small gradient: this is a first-order stationarity certificate, even when there is no claim that the point is globally optimal. A guarantee on the expected squared gradient leaves open how often one particular run succeeds. The two-phase randomized stochastic gradient method of Ghadimi and Lan (2013) addresses that question by generating several candidates and using further oracle calls to select one. The paper gives an explicit bound on the probability of failure and on the number of oracle calls needed for a prescribed accuracy and confidence.

The work sits within stochastic approximation, where the objective may be a population expectation or another function accessible through noisy observations. The 2013 paper develops first- and zeroth-order methods for smooth nonconvex problems. This mission concerns its two-phase first-order result, Theorem 2.4, rather than the Gaussian smoothing results in its later section. The source for every index here is the arXiv v1 preprint; the printed page and PDF page coincide.

Setting

The objective is a differentiable function $f:\mathbb R^n\to\mathbb R$ bounded below, with true optimal value $f^*=\inf_x f(x)$. Its gradient map $g=\nabla f$ is $L$-Lipschitz: $\|g(y)-g(x)\|\le L\|y-x\|$ for all $x,y$. The mission uses $L>0$. No convexity is assumed.

A stochastic first-order oracle returns a vector $G(x_k,\xi_k)$ when called at the current iterate $x_k$. Assumption A1 says that the oracle is unbiased at that iterate and has squared error of expectation at most $\sigma^2$. The noise may depend on earlier calls. In the formal model, the mean is conditional on the past, and the oracle and squared-error random variables are integrable. This makes explicit the probabilistic assumptions used when the paper takes expectations. The model takes $\sigma>0$ because the paper's displayed stepsize and post-optimization sample size otherwise degenerate under Lean's total division convention.

A randomized stochastic gradient run starts at $x_1$ and uses $x_{k+1}=x_k-\gamma_k G(x_k,\xi_k)$. It chooses an output index $R\in\{1,\ldots,N\}$ with the probability mass function in equation (2.3), independently of that run's oracle noise, and outputs $x_R$. For a parameter $\widetilde D>0$, the constant stepsize in equation (2.13) is $\gamma_k=\min\{1/L,\widetilde D/(\sigma\sqrt N)\}$. The paper writes $D_f=\sqrt{2(f(x_1)-f^*)/L}$ and

$$\mathcal B_N=\frac{LD_f^2}{N}+\left(\widetilde D+\frac{D_f^2}{\widetilde D}\right)\frac{\sigma}{\sqrt N}.$$

The two-phase method makes $S$ independent RSG runs, yielding $\bar x_1,\ldots,\bar x_S$. For each candidate it averages $T$ fresh oracle outputs into an estimated gradient $\widehat g_s$. It selects a candidate $\bar x^*$ whose estimated-gradient norm is minimal. The post-optimization samples for different candidates may be recycled; the paper explicitly permits this. The candidate itself is known when its post-optimization samples are taken, so the conditional oracle assumption is stated relative to a filtration that contains it at time zero.

Formalization targets

The first target is the one-run mean bound of Corollary 2.2, $L^{-1}\mathbb E\|g(x_R)\|^2\le\mathcal B_N$, followed by the one-run tail bound (2.19). Lemma 2.3(a) controls the squared norm of a sum of vector martingale differences. Equation (2.28) relates a selected candidate's true gradient to the best candidate and the estimation errors. Equation (2.29) factors the probability of simultaneous failure across independent runs and bounds it, while (2.30) bounds the other source of failure: every optimization run performing poorly, and at least one estimated gradient being inaccurate.

For arbitrary positive $S,N,T$, Theorem 2.4(a) states the stronger quantitative tail bound

$$\Pr\left\{\|g(\bar x^*)\|^2\ge2\left(4L\mathcal B_N+\frac{3\lambda\sigma^2}{T}\right)\right\}\le\frac{S+1}{\lambda}+2^{-S}\qquad(\lambda>0).$$

The goal, Theorem 2.4(b), specializes those parameters to an accuracy $\varepsilon>0$ and failure probability $0<\Lambda<1$. It sets

$$S=\left\lceil\log_2\frac2\Lambda\right\rceil,\qquad N=\left\lceil\max\left\{\frac{32L^2D_f^2}{\varepsilon},\left(\frac{32L(\widetilde D+D_f^2/\widetilde D)\sigma}{\varepsilon}\right)^2\right\}\right\rceil,\qquad T=\left\lceil\frac{24(S+1)\sigma^2}{\Lambda\varepsilon}\right\rceil.$$

An $(\varepsilon,\Lambda)$-solution is a point satisfying $\Pr\{\|g(\bar x^*)\|^2\le\varepsilon\}\ge1-\Lambda$. With those parameter values, the method computes such a point using at most $S(N+T)$ stochastic first-order oracle calls. The formulas and constants above are those of equations (2.24)–(2.27) of the preprint.

Significance

The result turns a mean stationarity bound into a confidence guarantee for one returned point, with an explicit accounting of both candidate generation and candidate assessment. It identifies how the number of independent runs, iterations per run, and gradient estimates scale with the requested accuracy and failure probability. Without the post-optimization phase, the paper's direct Markov estimate (2.19) gives a less favorable dependence on the failure probability for a single run.

The mathematical theorem is proved in the 2013 paper; the Lean declarations in this proposal are statements awaiting machine-checked proofs. A completed formalization would give reusable definitions for a dependent-noise gradient oracle, a random-output stochastic-gradient run, and a post-optimization selection procedure. The vector martingale estimate and finite-candidate inequality could also serve later stochastic-optimization developments. Contributions to the probability and measurability infrastructure, as well as the final rate proof, are within scope.

Difficulty

Selecting the candidate with the smallest estimated gradient need not select the one with the smallest true gradient. The estimates are random and are evaluated at candidates that are themselves random outputs of earlier oracle runs. A bound for a fixed point does not address this dependence. The argument needs a conditional oracle contract at each candidate and a separate guarantee that the optimization runs supply a sufficiently good candidate. The paper's intermediate display (2.31) applies a fixed-candidate tail estimate to the selected candidate even though the selection examines the same estimates; that step is not justified by the stated assumptions. The final bound can be phrased without treating (2.31) as a separate target.

Formalization scope

The space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Iterations and oracle samples retain the paper's one-based indexing; candidate runs use Fin S, which reindexes the paper's $1,\ldots,S$. The objective's true infimum is carried by IsGLB (Set.range f) fstar, so $D_f$ cannot be weakened by substituting an arbitrary lower bound. Each candidate is generated by the RSG recursion and the mass function (2.3); the one-run performance bound is a theorem, not a hypothesis of the two-phase model. Independent candidate outputs are required for (2.29). The selected candidate may be any minimizer of the estimated-gradient norm, with any tie rule; no measurability of the selection is assumed.

All expectations are Bochner integrals, with integrability included in the oracle assumptions and in the one-run conclusion. Probabilities are ℝ≥0∞ values. The noise carrier is generalized from the paper's Borel subsets of Euclidean space to a measurable type. The general vector martingale lemma omits the paper's Polish-space and trivial-time-zero conditions; neither is needed for its squared-norm bound, and the latter would conflict with a candidate known at time zero. Its non-strict tail statement is restricted to a positive sum of variance bounds, because the printed version is false when every bound is zero. The goal reads the logarithm in (2.24) as base two, matching the paper's final $2^{-S}\le\Lambda/2$ comparison. Positive $\sigma$ and $\widetilde D$ avoid zero steps and an empty post-optimization average.

The formal goal states the probability guarantee. The $S(N+T)$ oracle-call bound follows directly from the algorithm's two loops and is recorded in the theorem's prose rather than in a separate operational semantics for calls. A complete proof may use Mathlib's conditional expectations, independent random variables, finite sums, and real logarithm and ceiling libraries. No assumption may simply postulate the one-run gradient bound or the final success probability.

Selected references

• Saeed Ghadimi and Guanghui Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. arXiv:1309.5549v1.

Motivation

Stochastic programs and chance-constrained models in operations research contain expectations of the form

$$Z_0(x)=\mathbb E_0[h(x;\xi)],$$

where $\xi$ is a random input under an unknown distribution $P_0$, $x$ is a decision and $h$ is a known loss. In practice $P_0$ is seen only through i.i.d. data $\xi_1,\dots,\xi_n$. Distributionally robust optimization (DRO) replaces the unknown expectation by the worst case over a set of plausible distributions, and a recurring question is how large that set should be so that the robust value is a statistically valid bound, without being needlessly conservative.

The usual answer, for divergence-based sets on a finite support of size $k$, sets the radius from a $\chi^2_{k-1}$ quantile (Ben-Tal et al. 2013). This guarantee holds simultaneously for every function of the distribution, and so it is loose for a single expectation, and it degrades as $k$ grows. H. Lam (arXiv:1605.09349, Operations Research 2019) observed that if the ball is placed around the empirical distribution and measured with the Burg entropy, the right radius uses one degree of freedom, whatever the support. The DRO bounds then form an asymptotically exact confidence interval for $Z_0(x)$. The mechanism is the empirical likelihood method of Owen (Owen 1988; Owen 2001).

Timeline:

• 1988: Owen proves the empirical likelihood theorem for a mean (−2 log of the profile likelihood ratio tends to $\chi^2_1$), the nonparametric analogue of Wilks' theorem.
• 2013: Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen calibrate $\varphi$-divergence balls on a finite support with $\chi^2_{k-1}$ quantiles.
• 2016: Lam (this paper) connects the empirical Burg-ball DRO to empirical likelihood, with pointwise (Theorem 2) and uniform (Theorem 4) coverage.
• 2016–2021: Duchi, Glynn and Namkoong (arXiv:1610.03425) develop the general $f$-divergence version and exact coverage of optimal values.

Setting

Data: $\xi_1,\xi_2,\dots$ are i.i.d. random elements of a measurable space $\Xi$ under $P_0$. A decision $x\in\mathbb R^m$ is fixed, and $h(x;\cdot):\Xi\to\mathbb R$ is measurable with $0<\operatorname{Var}_0 h(x;\xi)<\infty$.

The empirical Burg-entropy divergence ball of radius $\eta$ is the set of weight vectors on the $n$ data points

$$\mathcal U_n(\eta)=\Big\{w\in\mathbb R^n:\ -\frac1n\sum_{i=1}^n\log(nw_i)\le\eta,\ \sum_{i=1}^n w_i=1,\ w_i\ge0\Big\},$$

with $\log 0=-\infty$. It is the $\varphi$-divergence ball around the uniform weights $1/n$ for the Burg generator $\varphi(t)=-\log t+t-1$. Let $\chi^2_{1,1-\alpha}$ be the $(1-\alpha)$-quantile of the $\chi^2_1$ law, i.e. $P(Y^2\le\chi^2_{1,1-\alpha})=1-\alpha$ for $Y\sim N(0,1)$. The empirical DRO bounds are

$$\underline Z_n(x)=\min_{w\in\mathcal U_n(\chi^2_{1,1-\alpha}/(2n))}\sum_{i=1}^n h(x;\xi_i)w_i,\qquad \overline Z_n(x)=\max_{w\in\mathcal U_n(\chi^2_{1,1-\alpha}/(2n))}\sum_{i=1}^n h(x;\xi_i)w_i .$$

For a sample $z\in\mathbb R^n$ and a value $\mu$, the profile empirical likelihood statistic is

$$-2\log R(\mu)=\min\Big\{-2\sum_{i=1}^n\log(nw_i):\ \sum_i w_iz_i=\mu,\ \sum_i w_i=1,\ w_i\ge0\Big\},$$

equal to $+\infty$ when no weight vector is feasible.

Formalization targets

Goal: Theorem 2 (p. 11)

$$\lim_{n\to\infty}P\big(\underline Z_n(x)\le Z_0(x)\le\overline Z_n(x)\big)=1-\alpha .$$

The event is two-sided and joint. No rate is claimed.

Milestones

• Proposition 2 (p. 23). For every data vector and $\kappa\ge0$,

$$\min_{\mathcal U_n(\kappa/(2n))}\textstyle\sum_i w_iz_i\le\mu\le\max_{\mathcal U_n(\kappa/(2n))}\sum_i w_iz_i\iff -2\log R(\mu)\le\kappa .$$

• Theorem 1, the empirical likelihood theorem (p. 10). $-2\log R(Z_0(x))\Rightarrow\chi^2_1$.
• The pointwise steps of the paper's proof of Theorem 1 (the proof of Theorem 5 with a one-point index set): Lemma 3 (p. 38), $\max_{i\le n}|Y_i|=o(n^{1/2})$ a.s. for square-integrable i.i.d. $Y_i$; the closed form (49)–(50) (pp. 25–26) of the optimal weights; the multiplier bound (52) (p. 27); the expansion (68) (p. 30), $-2\log R=n s^{-1}\bar h^2+o_p(1)$.

Significance

Theorem 2 says that a robust optimization formulation with a data-driven Burg ball of radius $\chi^2_{1,1-\alpha}/(2n)$ yields an asymptotically exact $(1-\alpha)$ confidence interval for an expected loss, independently of the support size of $\xi$. Proposition 2 is the bridge: it identifies the DRO interval with the empirical likelihood confidence region, so any distributional result on $-2\log R$ transfers to the DRO bounds. This is the pointwise basis of the paper's later results on feasibility of chance and expectation constraints.

The result is proved in the paper, and Theorem 1 is classical. To our knowledge none of these statements has a machine-checked proof. Formalizing them requires the empirical likelihood theorem in Lean, which is reusable well beyond DRO (empirical likelihood tests and intervals for means). The Open platform theorem GenEmpLik.Coverage.theorem_3 (Duchi, Glynn and Namkoong) implies the goal when its decision set is the single point $\{x\}$ and its generator is $2\varphi$ with radius $\chi^2_{1,1-\alpha}$; it is a different, more general statement and is not proved. Likewise the Open GenEmpLik.Expansion.lemma_7 implies Lemma 3, and the Proved NumStochOpt.ListScheduling.lemma_8_1_i_max_over_sqrt_ae gives Lemma 3 after passing to $|Y_i|$.

Difficulty

Proposition 2 is a finite-dimensional convexity statement, but it needs attainment of the minimum defining $-2\log R$, which holds only because the objective blows up at the boundary of the simplex. The central difficulty is Theorem 1. The optimal weights are explicit only through a Lagrange multiplier $\lambda$ that solves a nonlinear equation; to expand $-2\log R$ one must first show $\lambda=O_p(n^{-1/2})$, which requires controlling the largest observation by Lemma 3 together with the law of large numbers for $s$, and then bound the cubic Taylor remainder of $\log(1+\lambda\tilde h_i)$ uniformly in $i$. A direct appeal to the central limit theorem for the sample mean does not suffice, since $-2\log R$ is an implicitly defined optimal value, not a smooth function of the mean.

Formalization scope

• The sample is a sequence ξ : ℕ → Ω → Ξ, measurable, mutually independent and identically distributed, indexed from $0$; the size-$n$ sample is fun i : Fin n => h x (ξ i ω).
• The moment assumption is MemLp (h x ∘ ξ 0) 2 together with 0 < variance. Positive variance cannot be dropped: for a constant loss the coverage is $1$.
• The quantile is pinned by gaussianReal 0 1 {y | y^2 ≤ q} = ofReal (1 - α) with $0<\alpha<1$; it is not a free parameter, and it is not the normal quantile.
• The upper bound is the published GenEmpLik.Expansion.robustMean burg (q/2) (its ball has radius $\rho/n$, so $\rho=q/2$); the lower bound is its infimum twin robustLower. The ball uses the published probUncertaintySet and phiDiv.
• The Burg generator is $+\infty$ at $t\le0$, and the statistic elStat minimizes over strictly positive weights with the empty infimum equal to $+\infty$. Lean's junk value $\log 0=0$ therefore never enters: a formalization with $w_i\ge0$ and real logarithms would admit boundary weights with spurious finite divergence and is ruled out. For $n\ge1$ the value sets of the DRO bounds are nonempty and bounded, so the real infimum and supremum are not junk values.
• The decision set $\Theta$ is dropped (the statements are pointwise in $x$). Theorem 1 is stated as convergence of distribution functions at every $t$, which is equivalent to $\Rightarrow\chi^2_1$ since the limit is continuous. Proposition 2 is stated for general $\kappa\ge0$ and every data vector, as displayed on p. 11. Milestones (49)–(50), (52), (68) are the one-point ($\Theta=\{x\}$) specialisations of the proof of Theorem 5.
• Probabilities of events are outer probabilities; no measurability of events is assumed, as the paper ignores these issues (p. 14).
• Not posed: the headline Theorem 4 (uniform calibration over $\Theta$ by the quantile of a $\chi^2$-process supremum), Theorem 5 and Lemma 2, which need Donsker classes and weak convergence in $\ell^\infty(\Theta)$, for which Mathlib has no substrate.

Contributions welcome: proofs of Proposition 2 and Lemma 3 (from the Proved reference), the KKT analysis (49)–(52), and a Lean empirical likelihood theorem.

Selected references

• H. Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization, arXiv:1605.09349v1, 2016; Operations Research 67(4), 2019. https://arxiv.org/abs/1605.09349v1
• A. B. Owen, Empirical likelihood ratio confidence intervals for a single functional, Biometrika 75(2), 1988. https://doi.org/10.1093/biomet/75.2.237
• A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• J. C. Duchi, P. W. Glynn, H. Namkoong, Statistics of robust optimization: a generalized empirical likelihood approach, Mathematics of Operations Research 46(3), 2021. https://arxiv.org/abs/1610.03425

Why this market matters

An intermediary such as a ride platform must attract buyers and sellers who arrive at different times. A buyer may wait for a seller; a seller may wait for a buyer. Both sides can choose when to request a match, so an ask price and a bid price affect participation as well as the intermediary's margin. Chen and Hu study whether a simple posted-price policy remains profitable despite this waiting and the uncertainty of arrivals. Their submitted manuscript proves a finite-market guarantee and an asymptotic rate for the policy used here. The proof appears in its Supplemental Note, while the model and theorem are in the main text.

Market and benchmarks

Buyers arrive during a horizon $[0,T]$ as a Poisson process of rate $\lambda^d>0$, and sellers arrive independently at rate $\lambda^s>0$. A buyer's valuation $v$ has density $f^d$ on $[\underline v,\overline v]$ and a seller's cost $c$ has density $f^s$ on $[\underline c,\overline c]$. Marks are independent of arrival times. A buyer and a seller each trade at most one unit. If they wait after arrival, they incur costs $b$ and $h$ per unit time, respectively. The paper assumes regularity: the buyer's virtual value $V^d(v)=v-\bar F^d(v)/f^d(v)$ and the seller's virtual cost $V^s(c)=c+F^s(c)/f^s(c)$ are weakly increasing on their supports. Here $\bar F^d=1-F^d$.

A clairvoyant assignment knows all arrivals through $T$. For each possible buyer–seller pair it assigns virtual surplus $V^d(v)-V^s(c)$ less the waiting cost determined by their arrival order. It chooses a partial matching with greatest total value, denoted $\bar J(H^T)$. A separate fluid program chooses a measurable, nonnegative pair of price trajectories that clears demand and supply at every time. Its optimal value is $\bar J^*$. These are different objects: $\bar J(H^T)$ is random and uses indivisible agents, whereas $\bar J^*$ is a deterministic continuous-flow optimum. Lemma 2 of the manuscript compares their values in expectation.

Let $\mu^*$ be the greatest volume in $[0,\min\{\lambda^dT,\lambda^sT\}]$ with nonnegative marginal virtual surplus. The buyer and seller prices $p^*,w^*$ are inverse-distribution prices at that volume. Proposition 1 states that these constant prices attain the fluid optimum and $\bar J^*=(p^*-w^*)\mu^*$.

Formalization targets

The greedy matching policy pairs requests first come, first served. Under the waiting-adjusted fixed-price policy, a buyer's posted ask is $p^*$ minus $b$ times a conditional expected wait per match probability; the seller's posted bid is $w^*$ plus the corresponding $h$ term. The buyer adjustment is conditioned on the observed pre-arrival inventory signal. Agents request immediately exactly when their valuation or cost crosses the base-price threshold. The policy's expected profit $J$ is computed from posted prices paid by successfully matched agents.

The first target is the paper's finite-market bound:

$$\frac{J}{\bar J^*}\ge 1-\left(1+\frac{2(b+h)T}{3(p^*-w^*)}\right)\frac{1}{\sqrt{\mu^*}}.$$

When $J\ge0$, the benchmark comparison also gives $J/\mathbb E[\bar J(H^T)]\ge J/\bar J^*$. For scaled systems with arrival rates $n^{\alpha_d}\lambda^d$ and $n^{\alpha_s}\lambda^s$, where both exponents are positive, the second target is a constant $C$ independent of $n$ such that

$$\frac{J^{(n)}}{\bar J^{*,(n)}}\ge 1-\frac{C}{\sqrt{n^{\min\{\alpha_d,\alpha_s\}}}}\qquad(n\ge1).$$

The milestone list follows the source's Proposition 1, Lagrangian relaxation, Lemma 2, Poisson request counts, policy profit identity, Gallego–van Ryzin moment bound, and Lemma S.5 on arrival-rate monotonicity. The last three supply the finite bound and its scaling statement in the Supplemental Note.

What the result gives

The finite bound quantifies the cost of using fixed base prices and greedy matching instead of the fluid ideal. Its two terms separate the loss from random mismatch and the extra waiting adjustment. The scaled bound says that, as both sides' arrival rates grow, the fraction of the fluid value lost by this policy vanishes at a rate governed by the slower-growing side. This offers a concrete reason to use a simple policy when the market is large, while keeping the smaller-market correction visible.

The paper already proves these claims. This mission asks for machine-checked proofs of their precise statements. The fluid optimizer, the clairvoyant matching problem, the marked Poisson arrival model, and the policy-profit identity are reusable mathematical objects beyond this theorem. The positive-part moment bound is an already published theorem and is referenced rather than posed again.

Where the argument is difficult

The obvious comparison between posted-price profit and fluid revenue misses the cost of requests that wait or never match. The price corrections themselves are conditional expectations divided by conditional match probabilities; their effect cannot be captured by simply subtracting a constant waiting charge. The proof must connect those corrections to the time integral of the queue imbalance, then control the imbalance of two Poisson request streams. A second difficulty is that the fluid optimum and the expected clairvoyant optimum are defined through different feasible sets, so their comparison needs a separate relaxation argument. These obstacles are visible in the source's proof of Lemma 2 and Theorem 2.

Formalization scope

The density and virtual-value environment is the published bilateral-trade definition, imported through a local name alias required by the frozen shared market module. Lean represents arrivals by independent Poisson counts and independent identically distributed time-and-value marks. This is equal in law to the paper's homogeneous marked Poisson processes on $[0,T]$. Arrival time marks are uniform probability laws, and valuation and cost marks use the source densities. Simultaneous requests are ordered by index; such ties have probability zero. The deterministic program ranges over measurable, nonnegative, market-clearing paths with interval-integrable objective terms. Its value is the supremum of their objectives, not a formula involving $p^*$ and $w^*$; Proposition 1 must establish that formula. The clairvoyant value uses the published partial-assignment-game worth, so negative-weight pairs may remain unmatched.

The density functions are continuous on their supports, an explicit addition needed for the inverse prices and maximum volume used by Proposition 1. The lower support endpoints are nonnegative so the constant prices belong to the nonnegative fluid price domain; this fills an implicit domain convention in the manuscript. For Theorem 2 the overlap condition is strict, $\underline c<\overline v$, ensuring positive $\mu^*$ and $p^*-w^*$. The printed chain comparing $J/\mathbb E[\bar J]$ and $J/\bar J^*$ is stated under $J\ge0$: when the numerator is negative, the claimed direction fails. Both expectations used as finite numbers are accompanied by integrability conclusions. Division by a zero match probability at the terminal time uses a zero convention on a set of arrival times with probability zero.

The policy model builds in the myopic request behavior that Theorem 1 identifies as an equilibrium; its strategic proof is outside this mission. The policy profit is the expectation of actual posted-price payments, and the waiting compensations are literal tagged-arrival conditional ratios. Contributions that prove the inverse-distribution properties, Poisson thinning, queue profit identity, fluid optimization, or final moment estimate all address parts of the stated target.

Selected references

• Y. Chen and M. Hu, Pricing and Matching with Forward-Looking Buyers and Sellers, Manufacturing & Service Operations Management 22(4), 2020; submitted manuscript, SSRN 2859864.

Motivation

Large optimization problems often split into blocks owned by different agents (subsystems of a power grid, vehicles in a formation, scenarios of a stochastic program) that are coupled only through a few linear constraints. Distributed optimization methods solve such problems by letting each agent work on its own block and exchanging a small amount of information, typically a vector of prices for the coupling constraints. The classical method of this kind is dual decomposition (Everett 1963; Bertsekas and Tsitsiklis, Parallel and Distributed Computation, 1989): fix the prices, let every agent solve its own subproblem, then update the prices by a gradient or Newton step on the concave dual function. Dual decomposition is reliable for strictly convex problems but has no convergence guarantee for nonconvex ones.

Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton), which adds a proximal term to the agents' subproblems and replaces the price update by a coupled equality-constrained quadratic program. ALADIN is used in distributed model predictive control and in power-system optimization. Remark 4.2 and Appendix A of the paper explain where it sits relative to the classical method: if the proximal term is switched off ($\rho = 0$), the price update of ALADIN is exactly a regularized Newton step of dual decomposition. Lemma 5 is the precise statement of that equivalence, and it is the goal of this mission.

Setting

The problem (1.1) has $N$ blocks $x_i\in\mathbb R^n$:

$$\min_x\ \sum_{i=1}^N f_i(x_i)\quad\text{s.t.}\quad \sum_{i=1}^N A_i x_i = b,\qquad h_i(x_i)\le 0,$$

with $f_i:\mathbb R^n\to\mathbb R$, $h_i:\mathbb R^n\to\mathbb R^{n_h}$ twice continuously differentiable, $A_i\in\mathbb R^{m\times n}$ and $b\in\mathbb R^m$. One iteration of Algorithm 2 (ALADIN) starts from a primal point $x$ and prices $\lambda\in\mathbb R^m$ and does the following.

1. Each agent solves the decoupled problem $\min_{y_i} f_i(y_i) + \lambda^\top A_i y_i + \frac\rho2\|y_i-x_i\|^2_{\Sigma_i}$ subject to $h_i(y_i)\le 0$, returning a minimizer $y_i$ and a multiplier $\kappa_i\ge 0$. With $\rho = 0$ this is the dual-decomposition subproblem (A.2).
2. Each agent forms the active-constraint Jacobian $C^*_i$ (rows $\nabla(h_i)_j(y_i)^\top$ for active $j$, zero rows otherwise), chooses an approximation $C_i$ and a symmetric Hessian approximation $H_i$, and computes the modified gradient $g_i = \nabla f_i(y_i) + (C^*_i - C_i)^\top\kappa_i$.
3. For a parameter $\mu>0$, a coordinator solves the coupled QP (3.3)

$$\min_{\Delta y, s}\ \sum_i\Big\{\tfrac12\Delta y_i^\top H_i\Delta y_i + g_i^\top\Delta y_i\Big\} + \lambda^\top s + \tfrac\mu2\|s\|_2^2\ \ \text{s.t.}\ \ \sum_i A_i(y_i+\Delta y_i) = b + s\ \mid\ \lambda_{\mathrm{QP}},\quad C_i\Delta y_i = 0,$$

and the new prices are $\lambda^+ = \lambda + \alpha_3(\lambda_{\mathrm{QP}}-\lambda)$.

On the dual-decomposition side, $\nabla V(\lambda) = \sum_i A_i y_i - b$ (A.3) is the gradient of the dual function at $\lambda$, and the (inexact) dual Newton step (A.4) with a symmetric negative semidefinite scaling matrix $M$ and step size $\alpha\in(0,1]$ is

$$\lambda^+_{\mathrm{DD}} = \lambda - \alpha\Big(M - \frac1\mu I\Big)^{-1}\nabla V(\lambda),$$

where $1/\mu$ plays the role of a Levenberg–Marquardt regularization parameter.

Formalization targets

Goal: Lemma 5 (p. 1123)

Assume every $f_i$ strictly convex, every $h_i$ convex, $C_i$ of full row rank, $H_i$ positive definite, $\rho = 0$ and $\alpha_3 = \alpha$. Then for every $\mu>0$, with

$$M = -\sum_{i=1}^N A_i\Big[H_i^{-1} - H_i^{-1}C_i^\top\big[C_iH_i^{-1}C_i^\top\big]^{-1}C_iH_i^{-1}\Big]A_i^\top,$$

the matrix $M - \frac1\mu I$ is invertible and

$$\lambda^+ = \lambda^+_{\mathrm{DD}} .$$

Milestones (the steps of the proof, pp. 1123–1124)

1. Slack elimination: $\min_s \frac\mu2\|s\|_2^2 - (\lambda_{\mathrm{QP}}-\lambda)^\top s = -\frac1{2\mu}\|\lambda_{\mathrm{QP}}-\lambda\|_2^2$, attained only at $s = (\lambda_{\mathrm{QP}}-\lambda)/\mu$.
2. Stationarity: with $\rho = 0$, $0 = \nabla f_i(y_i) + A_i^\top\lambda + (C^*_i)^\top\kappa_i = g_i + A_i^\top\lambda + C_i^\top\kappa_i$.
3. Explicit minimization over $\Delta y$: for $H\succ 0$ and $C$ of full row rank, $-Pw$ with $P = H^{-1} - H^{-1}C^\top(CH^{-1}C^\top)^{-1}CH^{-1}$ minimizes $\frac12\Delta^\top H\Delta + w^\top\Delta$ on $\{C\Delta = 0\}$, with value $-\frac12 w^\top Pw\le 0$.
4. Argmax display: for $M$ symmetric negative semidefinite, $\lambda - (M - \frac1\mu I)^{-1}g$ is the unique maximizer of $\frac12(\nu-\lambda)^\top M(\nu-\lambda) + \nu^\top g - \frac1{2\mu}\|\nu-\lambda\|_2^2$.

Significance

The result. Lemma 5 places ALADIN on a known map. With $\rho=0$ it inherits the convergence theory of dual decomposition for strictly convex problems for small step sizes, independently of how crude the approximations $H_i$, $C_i$ are, as long as $H_i\succ 0$. It also reinterprets the augmented-Lagrangian parameter $\mu$ as the inverse of a dual Levenberg–Marquardt parameter, and it isolates the proximal term $\frac\rho2\|y_i - x_i\|^2_{\Sigma_i}$ as the only ingredient that distinguishes ALADIN from dual decomposition and makes the nonconvex analysis of the paper possible.

Formalizing it. The lemma is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof certifies an identity whose printed form contains a typo (see below), and produces reusable linear-algebra facts: the closed-form solution of an equality-constrained strictly convex quadratic program via the reduced inverse $P$, the semidefiniteness of $P$, and the closed-form maximizer of a regularized concave quadratic.

Difficulty

The proof is a chain of exact eliminations, and the work is in carrying each one out without losing a sign or a hypothesis. The step most easily done wrong is the minimization over $\Delta y$: the constraint $C_i\Delta y_i = 0$ couples the block coordinates, the minimizer is expressed through the inverse of $C_iH_i^{-1}C_i^\top$ (invertible only because $C_i$ has full row rank). A second trap is the sign convention for $\lambda_{\mathrm{QP}}$: it must agree with footnote 4 ($\lambda + \mu s - \lambda_{\mathrm{QP}} = 0$), or the conclusion flips. The tempting shortcut of treating the max–min dual of (3.3) abstractly runs into the fact that strong duality and attainment are not free; working from the KKT system of (3.3) avoids that.

Formalization scope

Vectors are Fin n → ℝ; blocks are indexed by Fin N; matrices are Mathlib Matrix over Fin index types; the gradient is the vector of partial derivatives computed with fderiv. The step-1 output $(y_i,\kappa_i)$ is a local minimizer of the decoupled problem together with KKT multipliers (the paper assumes LICQ for the lower-level constraints). The QP (3.3) and $\lambda_{\mathrm{QP}}$ enter through the KKT system of (3.3), not through a closed-form expression: defining $\lambda_{\mathrm{QP}}$ or $\Delta y$ by the formula of the conclusion would make the goal true by definition and is ruled out. $\nabla V(\lambda)$ is the formula (A.3); that it is the gradient of the dual function is a cited fact the lemma does not use. The invertibility of $M - \frac1\mu I$ is part of the conclusion, because Mathlib's matrix inverse returns $0$ on a singular matrix.

Correction of (A.6). As printed, (A.6) has the bracket $[C_iH_iC_i^\top]^\dagger$. This is a typo for $[C_iH_i^{-1}C_i^\top]^\dagger$, as in (A.5) on the same page and as the explicit minimization over $\Delta y$ forces; with the printed bracket the identity fails already for $N = 1$, $H_1 = \mathrm{diag}(1,2)$, $C_1 = (1,1)$, $A_1 = I$. The mission uses the corrected matrix and writes the pseudo-inverse as an inverse, which it is under the hypotheses.

The hypotheses of strict convexity of $f_i$, convexity of $h_i$ and $\alpha\in(0,1]$ are kept as on the page although the identity does not use them. The related platform draft GoldfarbIdnani.DualQP.properties_2_6_to_2_9 (not proved) states properties of the same reduced inverse; it is not imported. Proofs of the four milestones and of the goal are welcome; the milestones are self-contained matrix and calculus facts and can be attacked independently.

Selected references

• B. Houska, J. Frasch, M. Diehl, An augmented Lagrangian based algorithm for distributed nonconvex optimization, SIAM J. Optim. 26(2) (2016), 1101–1127. https://doi.org/10.1137/140975991
• D. P. Bertsekas, J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice-Hall, 1989.
• H. Everett, Generalized Lagrange multiplier method for solving problems of optimum allocation of resources, Oper. Res. 11(3) (1963), 399–417. https://doi.org/10.1287/opre.11.3.399
• D. P. Bertsekas, Nonlinear Programming, 2nd ed., Athena Scientific, 1999.

Motivation

Quasi-Newton methods minimize a smooth function $f:\mathbb R^n\to\mathbb R$ using gradients only, while building up an approximation to the inverse of the Hessian matrix from the changes of gradient they observe. They are the default algorithms of unconstrained nonlinear optimization: BFGS and its limited-memory variant L-BFGS sit inside most numerical optimization libraries and most large-scale fitting codes in statistics and machine learning.

The family starts with William C. Davidon's Argonne report ANL-5990 of 1959, Variable Metric Method for Minimization, rejected by a journal in 1957 and published only in 1991 as the first article of the SIAM Journal on Optimization, with a preface by the author (DOI 10.1137/0801001). The report's body describes a flowchart algorithm; its Appendix describes "a simplified method embodying some of the ideas" of that algorithm, in one and a half pages. That simplified method is what is now called the symmetric rank-one (SR1) update, and the Appendix contains its quadratic-termination property: on a quadratic, after at most $n$ steps the trial matrix equals the inverse Hessian, and the next step lands at the minimum.

Timeline.

• 1952: Hestenes and Stiefel's conjugate gradient method minimizes a strictly convex quadratic in at most $n$ steps (J. Res. NBS 49); Davidon cites it as [2].
• 1959: Davidon's ANL-5990, including the Appendix method treated here.
• 1963: Fletcher and Powell simplify the body's method into the DFP update and prove its quadratic termination with exact line searches (Comput. J. 6).
• 1967: Broyden's survey of quasi-Newton methods discusses the symmetric rank-one update (Math. Comp. 21); textbooks later analyse it under the name SR1.
• 1980: Nocedal's limited-storage BFGS, whose termination on quadratics with exact line searches is a separate Prove2Me mission (Math. Comp. 35).

Setting

Vectors are elements of $\mathbb R^n$ and matrices are real $n\times n$. Fix a symmetric positive definite matrix $G$ and a point $\xi$, and let

$$f(x)=\tfrac12\,(x-\xi)^{\mathsf T}G\,(x-\xi)+c ,$$

a quadratic with constant Hessian $G$ and minimum point $\xi$. Its gradient is $\nabla(x)=G(x-\xi)$, display (6) of the Appendix.

The method keeps a point $x_k$ and a symmetric trial matrix $H_k$, which plays the role of $G^{-1}$. Write $\nabla_k=\nabla(x_k)$. One iteration is

$$x_{k+1}=x_k-H_k\nabla_k \quad\text{(2)},\qquad H_{k+1}=H_k+a_k\,(H_k\nabla_{k+1})(H_k\nabla_{k+1})^{\mathsf T}\quad\text{(3)},$$

a full step with no line search followed by a symmetric rank-one update. With the two scalars

$$N_k=\nabla_{k+1}^{\mathsf T}H_k\nabla_{k+1},\qquad M_k=\nabla_{k+1}^{\mathsf T}H_k\nabla_k ,$$

footnote 2 of the Appendix fixes the coefficient on a quadratic to $a_k=(M_k-N_k)^{-1}$, which makes the paper's quality measure $\Delta$ of (4) vanish. Write $S_k=x_{k+1}-x_k$ for the step and $D_k=\nabla_{k+1}-\nabla_k$ for the change of gradient. The paper writes $x$, $H$, $\nabla$ for the current quantities and $x^{+}$, $H^{+}$, $\nabla^{+}$ for the updated ones, and uses the letter $N$ both for the number of variables and for the scalar $N_k$; here the number of variables is $n$.

Formalization targets

Goal: termination in $n$ steps

If $H_0$ is symmetric and $M_k\ne N_k$ for every $k<n$, then

$$H_n=G^{-1}\qquad\text{and}\qquad x_{n+1}=\xi .$$

This is the sentence after (8) on p. 17: "After no more than $N$ steps (for which $\Delta=0$), $H$ will equal $G^{-1}$ and the following step will be to the exact minimum."

Milestones

1. Display (6): the gradient of $f$ is $G(x-\xi)$.
2. Display (8): with $a=(M-N)^{-1}$ and $M\ne N$, $H^{+}GS=H^{+}D=S$.
3. Display (7): if $HGu=u$ then $H^{+}Gu=u$, for any coefficient $a$.
4. The sentence "so that $S$ becomes another such eigenvector", read along the run: if $M_i\ne N_i$ for $i<k$, then $H_kGS_j=S_j$ for every $j<k$.

Further statements of the Appendix

• Condition 1 (p. 16): if $H$ is positive definite and $R^{-1}\le\det H^{+}/\det H\le R$ with $R>1$, then $H^{+}$ is positive definite.
• The constraint remark (p. 17): for any function and any coefficients, if $H_0$ is symmetric and $H_0b=0$, then every step is perpendicular to $b$ and $b\cdot x_k$ is conserved.
• Table (5) (p. 16): for general (non-quadratic) $f$, the coefficient $a$ that minimizes $\Delta$ subject to condition 1, and the minimum value, on each of five ranges of $M$.

Significance

The termination theorem says that on a quadratic the rank-one update recovers the exact inverse Hessian from $n$ gradient differences, without line searches and without positive definiteness of the trial matrix, and then takes the Newton step. This is the property that justifies the name "variable metric": the metric $H_k$ converges to the one that makes the problem trivial. The secant equation (8) and the persistence of earlier secant equations (7) are the template for the analysis of every later quasi-Newton update, and the SR1 update remains in use in trust-region methods because it does not force positive definiteness.

The result is classical and its proof is short; what this mission adds is a machine-checked version stated in the paper's own form. In particular the hypothesis is the paper's: only that each of the first $n$ coefficients is defined. Textbook statements of SR1 termination often assume in addition that the steps are linearly independent; the paper does not, and the formal goal does not either. No Lean formalization of SR1, DFP or BFGS termination was found in Mathlib or on Prove2Me. On Prove2Me, the related open targets are L-BFGS termination (Nocedal 1980) and conjugate-gradient termination (Hestenes–Stiefel 1952); the definitions here are independent of theirs.

Difficulty

Each update changes $H$ by a rank-one term, and nothing in a single step forces $H_n$ to be $G^{-1}$: the coefficient $a_k$ depends on the current iterate and the update could, a priori, destroy what earlier steps achieved, as general rank-one updates do. The obvious count — $n$ steps, $n$ conditions — does not by itself give $n$ independent conditions on $H_n$; the steps produced by the method are not chosen to be independent, and the only hypothesis available is that the denominators $M_k-N_k$ are nonzero. The difficulty is to get the full conclusion from that hypothesis alone, without assuming independence, positive definiteness of $H_0$, or a line search.

Formalization scope

Vectors are Fin n → ℝ with 0-based indices, matrices Matrix (Fin n) (Fin n) ℝ; $u^{\mathsf T}Hv$ is u ⬝ᵥ (H *ᵥ v) and $(Hg)(Hg)^{\mathsf T}$ is vecMulVec (H *ᵥ g) (H *ᵥ g). The definition file DavidonVM.Termination.Method provides quad, grad, Nval, Mval, the run predicate IsRunWith for an arbitrary gradient field and coefficients, and IsQuadRun for the quadratic with $a_k=(M_k-N_k)^{-1}$; DavidonVM.Termination.Delta provides the update and the quantity $\Delta$ of (4).

Committed conventions, each a reading of something the paper leaves implicit:

• The function is an explicit quadratic with constant symmetric positive definite $G$ ("in the neighborhood of a minimum"); the run's gradient field is $G(x-\xi)$, and milestone 1 ties it to the quadratic. The goal uses positive definiteness; milestones use only symmetry where that suffices; the secant milestone needs nothing on $G$.
• Only $H_0$ is assumed symmetric (the paper, p. 4: "It is to be symmetric"); positive definiteness of $H_0$ is not assumed.
• "Steps for which $\Delta=0$" is read through footnote 2 as $M_k\ne N_k$. Lean's real inverse gives $0^{-1}=0$, so without this hypothesis the update would silently leave $H$ unchanged.
• The stopping rule "provided that $N$ is greater than some preassigned $\varepsilon$" is not modelled; the run continues for every $k$, and the goal looks at steps $0,\dots,n$ only.
• $G^{-1}$ is Mathlib's matrix inverse, the true inverse since $G$ is positive definite.

A statement of the goal with the extra hypothesis "$S_0,\dots,S_{n-1}$ are linearly independent", or with $H_k G S_j=S_j$ assumed, would be a weaker theorem than the paper's and is ruled out. The case $n=0$ is trivial; the hypotheses are jointly satisfiable for $n=1$ (checked locally).

Welcome contributions: proofs of the four milestones and the goal; general facts about rank-one updates (determinant and positive definiteness, Sherman–Morrison form of the inverse) that the further statements need and that are reusable for DFP, BFGS and trust-region analyses.

Selected references

• W. C. Davidon, Variable Metric Method for Minimization, SIAM J. Optim. 1(1) (1991) 1–17 (Argonne report ANL-5990, 1959). https://doi.org/10.1137/0801001
• M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, J. Res. Nat. Bur. Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
• R. Fletcher and M. J. D. Powell, A rapidly convergent descent method for minimization, Comput. J. 6 (1963) 163–168. https://doi.org/10.1093/comjnl/6.2.163
• C. G. Broyden, Quasi-Newton methods and their application to function minimisation, Math. Comp. 21 (1967) 368–381. https://doi.org/10.1090/S0025-5718-1967-0224273-2
• J. Nocedal, Updating quasi-Newton matrices with limited storage, Math. Comp. 35 (1980) 773–782. https://doi.org/10.1090/S0025-5718-1980-0572855-7

Why lower bounds matter for progressive hedging

Progressive hedging separates a stochastic optimization problem by scenario, solves those smaller problems, and coordinates their first-stage decisions through weighted aggregation and price updates. It is useful when the full extensive formulation is too large to solve directly. For stochastic mixed-integer programs, its iterates can provide feasible decisions, but a feasible cost alone does not reveal how far that cost is from the global optimum. A lower bound gives the missing comparison: the difference between a feasible cost and a valid lower bound is an optimality gap. Branch-and-bound methods also use lower bounds to discard regions whose best possible cost cannot improve the current solution. These are the reasons the authors seek a bound available during a progressive-hedging run, rather than only after convergence. Gade et al., author manuscript, §§1–3.

The paper establishes lower bounds for two-stage stochastic mixed-integer programs, extends them to scenario bundles, and studies their behavior computationally. The mission concerns the mathematical statement that the price vector produced at each completed iteration is eligible for a decomposed lower bound. The paper was published in Mathematical Programming in 2016; the theorem and page labels here follow the authors' SAND2013-9195J manuscript. Gade et al., author manuscript.

Finite-scenario two-stage setting

Let $\Xi$ be a finite set of scenarios and let $p_\xi>0$ be their probabilities, with $\sum_{\xi\in\Xi}p_\xi=1$. A first-stage decision $x\in\mathbb R^{n_1}$ is made before the scenario is known. Its first $p_1$ coordinates are nonnegative integers; the others are unrestricted reals. It incurs cost $c^\top x$ and must satisfy $Ax\ge b$. After scenario $\xi$ is observed, a second-stage decision $y(\xi)\in\mathbb R^{n_2}$ incurs cost $g(\xi)^\top y(\xi)$. Its first $p_2$ coordinates are nonnegative integers, and it must satisfy $Wy(\xi)\ge r(\xi)-T(\xi)x$. The recourse matrix $W$ is common to all scenarios. The scenario feasible set $X(\xi)$ contains pairs $(x,y)$ satisfying these restrictions for one $\xi$. Gade et al., §2, pp. 3–5.

In the extensive scenario formulation, each scenario has a copy $x(\xi)$ of the first-stage vector, and a common vector $\hat x$ enforces implementability through $p_\xi x(\xi)-p_\xi\hat x=0$. Its optimum is $z^*$. Algorithm 1 starts with zero prices $w^0(\xi)=0$, solves unpenalized scenario problems, and at iteration $\nu$ computes $\hat x^\nu=\sum_\xi p_\xi x^\nu(\xi)$ and $w^\nu(\xi)=w^{\nu-1}(\xi)+\rho(x^\nu(\xi)-\hat x^\nu)$. Later scenario solves add both $w^\nu(\xi)^\top x$ and $(\rho/2)\|x-\hat x^\nu\|_2^2$ to their objectives. Here $\rho$ is the algorithm's scalar parameter. Gade et al., Algorithm 1, p. 6.

Formalization targets

Scenario price bound

For any scenario prices $w(\xi)$, define the decomposed dual value by

$$D_\xi(w(\xi))=\inf_{(x,y)\in X(\xi)}\left(c^\top x+g(\xi)^\top y+w(\xi)^\top x\right),\qquad D(w)=\sum_{\xi\in\Xi}p_\xi D_\xi(w(\xi)).$$

Proposition 1 states that prices with $\sum_\xi p_\xi w(\xi)=0$ satisfy $D(w)\le z^*$. The price invariant in §3.1 states that the update maintains this weighted zero sum. The mission's goal combines these source claims at every completed iteration $N\ge1$ of Algorithm 1:

$$\sum_{\xi\in\Xi}p_\xi w^N(\xi)=0,\qquad D(w^N)\le z^*.$$

The formal goal is the lower-bound inequality; the zero-sum statement and Proposition 1 are its two milestones. Gade et al., Proposition 1, p. 6, and §3.1, p. 7.

Bundle extension

For a partition $B$ of the scenarios, a bundle $\beta$ has probability $P_\beta=\sum_{\xi\in\beta}p_\xi$. A bundle subproblem uses one first-stage vector for its scenarios and second-stage weights $p_\xi/P_\beta$. Proposition 3 gives the corresponding inequality $D_B(w)\le z^*$ when $\sum_{\beta\in B}P_\beta w(\beta)=0$. The proposal also records the bundle price invariant and the resulting inequality at each completed bundled iteration as companion statements. Gade et al., §3.3, pp. 9–10.

What the results provide

The scenario bound turns each price vector into an independent set of optimization problems whose weighted values certify a lower bound on the original mixed-integer optimum. The bound does not require the scenario first-stage decisions to agree at that iteration. The bundle result gives the same kind of certificate when several scenarios are solved together. These are the paper's known results, not new open mathematical conjectures. Gade et al., §§3.1 and 3.3.

Formalizing them requires a reusable interface for finite-support stochastic mixed-integer models, their scenario feasible sets, implementability equations, price systems, and finite prefixes of both algorithms. It also separates the general price-feasibility inequality from the algorithmic invariant. The mission currently proposes statements with open Lean proofs; it does not claim a machine-checked proof of these paper results.

Main mathematical difficulty

An iteration of progressive hedging solves scenario problems with a quadratic proximal term, while the lower-bound calculation uses scenario problems without that term. Their objective values cannot simply be identified. The relevant connection is the price vector: to apply Proposition 1 at an arbitrary iteration, its weighted zero-sum condition must follow from the actual aggregation and price-update rules. The bundle version adds normalization by $P_\beta$, so every bundle must have positive mass and the bundle weights must cover the full scenario distribution. Gade et al., §§3.1 and 3.3.

Formalization scope

Lean represents vectors as Fin n → ℝ, linear constraints componentwise, and the extensive formulation with the weighted implementability equation printed in (15). The dimensions satisfy $p_1\le n_1$ and $p_2\le n_2$, as required by the paper's spaces $\mathbb Z_+^{p_i}\times\mathbb R^{n_i-p_i}$. The finite scenario weights are positive and sum to one. The first integer coordinates are nonnegative; every remaining real coordinate is free. The paper's assumptions that the SMIP has an attained finite optimum and each $X(\xi)$ is nonempty are explicit in the goal and Propositions 1 and 3. The scenario and bundle subproblem values, and $z^*$, live in the extended reals: an unbounded-below subproblem retains $-\infty$ rather than acquiring an arbitrary real infimum. Gade et al., §§2–3.

An algorithm run is a finite prefix through its last aggregation and price update, with exact minimizers recorded as conditions on its sequences; a stopping test truncates the prefix. The proximal term is the Euclidean sum of squared coordinate differences. No positivity condition on $\rho$ is added to the lower-bound statements, since the page does not require one for these claims. Bundles form a partition, but equal bundle sizes are not required for the inequalities. Algorithm 2's printed w^ν(i) at initialization and Σ_i P_β x^ν(β) at aggregation are read with bundle indices. A bundle recourse vector is represented as a function on all scenarios, with only its coordinates inside the bundle constrained or used.

The exact equations of the scenario model and runs prevent a trivial encoding that assumes dual feasibility or the desired bound as part of a run. Contributions to the model, the price invariants, the extended-real weak-duality arguments, and the bundle extension are all within scope. The paper's convexified limit result (Proposition 2), its cited Theorem 1, and multi-stage Algorithm 3 are outside this mission.

Selected references

• D. Gade, G. Hackebeil, S. M. Ryan, J.-P. Watson, R. J-B Wets, and D. L. Woodruff, Obtaining Lower Bounds from the Progressive Hedging Algorithm for Stochastic Mixed-Integer Programs, author manuscript SAND2013-9195J; published in Mathematical Programming, 2016. OSTI manuscript; DOI.