Optimization

Motivation

Large optimization models often split their variables into blocks that can be handled separately. A method can then solve one smaller approximation problem per iteration instead of the full problem. The block successive convex approximation (BSCA) method of Razaviyayn, Hong and Luo allows the block approximation to guide the search without requiring it to be a global upper bound on the original objective. This matters when an upper bound is awkward to construct but a locally accurate convex model is available. The question is what such a run can approach: a small objective value by itself does not certify first-order optimality.

The paper develops this result after its successive upper-bound minimization methods. Theorem 4 of the pinned preprint gives the limit-point guarantee for BSCA with an Armijo step search. The mission records that result and the numbered relations (31)–(34) and (39) that organize the argument, using the 2012 preprint as the sole source for statement indices and page numbers.

Setting

The decision vector is a block vector $x=(x_1,\ldots,x_N)$, with block $x_i$ in a nonempty, closed, convex set $X_i\subseteq\mathbb R^{m_i}$. The feasible set is $X=\prod_{i=1}^{N}X_i$. A continuously differentiable objective $f$ assigns each feasible vector a real value. A point $z\in X$ is stationary when $f'(z;d)\ge0$ for every direction $d$ whose full step $z+d$ lies in $X$. For a smooth objective, $f'(z;d)$ is the derivative of $f$ in direction $d$.

For block $i$, the function $h_i(y_i,x)$ approximates the objective as the trial block $y_i$ varies around a current point $x$. Its directional derivative at $y_i=x_i$ agrees with the objective derivative in the corresponding one-block direction, as in equation (30). Each $h_i(\cdot,x)$ is strictly convex on $X_i$, and $h_i$ varies continuously with its trial block and feasible base point. Strict convexity is a condition in the trial block for each fixed $x$; it does not say that $h_i$ is jointly convex in both arguments.

At iteration $r$, a cyclic schedule chooses one block $i$. A minimizer $y_i^r$ of $h_i(\cdot,x^r)$ over $X_i$ replaces that block in $y^r$; all other blocks of $y^r$ equal those of $x^r$. The search direction is $d^r=y^r-x^r$. With $\sigma,\beta\in(0,1)$ and an initial trial length $\alpha^{\rm init}>0$, the Armijo rule chooses the largest member $\alpha^r$ of $\{\alpha^{\rm init}\beta^j:j=0,1,\ldots\}$ satisfying

$$f(x^r)-f(x^r+\alpha^r d^r)\ge-\sigma\alpha^r f'(x^r;d^r),$$

then sets $x^{r+1}=x^r+\alpha^r d^r$. The selected minimizer can be any one of the block minimizers; the definition does not prescribe a hidden tie-breaking rule.

Formalization targets

The first targets identify descent and line-search existence. Equation (31) says the chosen block direction has a nonpositive derivative. Equation (32) says a strict descent direction admits a trial index. The later milestones state the vanishing scaled derivative (33), a subsequence with vanishing search directions (34), and limiting block optimality following (39).

The goal is Theorem 4: for every limit point $z$ of the sequence generated by cyclic BSCA,

$$z\in X,\qquad f'(z;d)\ge0\quad\text{for every }d\text{ with }z+d\in X.$$

This is a limit-point assertion. It does not assert convergence of the entire iterate sequence, a convergence rate, or global optimality of a stationary point.

Significance

Theorem 4 identifies what an accumulation point of BSCA must satisfy even though its block models need only local first-order agreement rather than global upper bounds. In a nonconvex problem, stationarity is a meaningful first-order conclusion but need not be a global minimum. The exact role of the step search is important: accepting some Armijo step gives decrease, whereas the theorem's limit-point claim uses the largest acceptable member of the geometric trial sequence.

This mission asks solvers to supply machine-checked proofs for a known paper theorem and its stated supporting relations. The draft statements compile as open theorems; they are not proofs. The reusable output includes a block run predicate, an explicit first-order agreement predicate, and a bridge between feasible-direction stationarity and an extended-real objective on the full block space. These objects also make subsequent variants of cyclic block methods easier to state precisely.

Difficulty

A simple decrease argument shows that objective values do not increase, but the accepted step sizes may approach zero. Therefore decrease alone does not imply $d^r\to0$ or that a limit point minimizes every block model. The paper's key limit statement singles out a convergent subsequence on which a fixed block is updated and finds a further subsequence with vanishing directions. Passing block optimality to the limit then requires continuity of the approximation and feasible limit points. The cyclic schedule is needed to cover all blocks, while first-order agreement turns block optimality into stationarity for the original smooth objective.

Formalization scope

Lean uses the published TsengBCD.Stationary.X for the finite product of Euclidean block spaces, its extended-real lower directional derivative, and its stationary-point predicate. The product has the sup norm rather than the paper's Euclidean product norm; in finite dimension the notions of convergence used here agree. Blocks and iterations are indexed from zero. The paper's cyclic choice $i=(r\bmod N)+1$ is reindexed so the step from $x^r$ to $x^{r+1}$ updates block $r\bmod N$. The existence of the schedule already rules out zero blocks.

The objective is a real function on the full block space, with ContDiff ℝ 1 expressing the paper's continuous differentiability. This makes the Fréchet derivative used in the Armijo test equal to the paper's lower directional derivative at the points in question. For stationarity, the objective is extended by $+\infty$ outside $X$, so infeasible directions cannot silently become admissible. The approximation derivative remains extended-real because the paper assumes only convexity for that function. ContinuousOn is taken on the product of a feasible trial block and a feasible base point.

Two points are explicit in the formalization. First, $0<\alpha^{\rm init}\le1$ ensures that a convex combination of $x^r$ and $y^r$ stays in $X$; the paper prints only positivity. Whether Theorem 4 holds without this restriction under a different global interpretation of $f$ and $h_i$ remains a separate question. Second, Figure 4 mixes $r$ and $r-1$ in the approximation, direction, and update lines. The run follows the adjacent prose and proof, all of which construct the direction at the current iterate. For (33), the existence of a limit point makes explicit the proof's standing situation and gives the decreasing objective a finite limit. An arbitrary unrelated sequence, an Armijo step that is not the largest accepted trial, or an objective extension that gives a default zero derivative off $X$ is outside this scope.

The remaining proof work includes feasibility of every iterate, first-order agreement along the selected block, the Armijo existence statement, the subsequence claim, passage of block minimization to the limit, and the final stationary-point equivalence. The finite-dimensional convex analysis and topology involved are reusable beyond this one algorithm.

Selected references

• M. Razaviyayn, M. Hong and Z.-Q. Luo, A Unified Convergence Analysis of Block Successive Minimization Methods for Nonsmooth Optimization, SIAM Journal on Optimization 23(2), 2013, 1126–1153. arXiv:1209.2385v1; DOI:10.1137/120891009.
• P. Tseng, Convergence of a Block Coordinate Descent Method for Nondifferentiable Minimization, Journal of Optimization Theory and Applications 109(3), 2001, 475–494. DOI:10.1023/A:1017501703105.

Why channel quality matters

A manufacturer that sells through a retailer can also open a direct sales channel. The direct channel lets the manufacturer reach consumers, but it competes with the retailer, whose orders generate wholesale revenue. The manufacturer can further choose whether the two channels carry products of the same quality. These decisions interact because quality changes both consumer demand and the retailer's response. Ha, Long and Nasiry study this interaction in a sequential supply-chain game. Their fixed-quality-cost extension asks what happens when a high-quality design can be converted into a lower-quality variant without paying a separate production cost for each unit (Ha, Long and Nasiry, §6.2).

The main result is specific to this cost regime. With a cost per unit that rises with quality, different products can be attractive across the channels; with the paper's one-time cost of creating quality, Proposition 6(i) asserts equal qualities when the direct channel makes positive sales. This mission targets that fixed-cost proposition in the authors' manuscript, including its game and the reduced-profit claims used in the e-Companion (Ha, Long and Nasiry, pp. 20, 36–37).

The sequential market

The market has mass one of consumers, indexed by a taste for quality $\theta$ uniformly distributed on $[0,1]$. A consumer buying a product of quality $v>0$ at price $p$ receives surplus $\theta v-p$. The manufacturer offers quality $u>0$ through her own direct channel and quality $tu>0$ through the retailer. The ratio $t$ therefore records which channel has higher quality. The manufacturer pays a fixed cost of quality $\max\{ku^2,k(tu)^2\}$, with $k>0$, and a direct selling cost $c\ge0$ per unit. The retailer has zero selling cost. Unlike a unit production cost, this fixed cost is paid once and does not scale with either channel's quantity (Ha, Long and Nasiry, pp. 7–8, 20).

The manufacturer first chooses wholesale price $w$ and qualities $u,tu$. After observing them, the retailer chooses its order $q_R\ge0$. The manufacturer observes that order and chooses her direct quantity $q_M\ge0$. When $0<t\le1$, market-clearing prices are

$$p_M=u(1-q_M-tq_R),\qquad p_R=tu(1-q_M-q_R).$$

When $t\ge1$, the retailer's product has higher quality, and the corresponding prices are

$$p_M=u(1-q_M-q_R),\qquad p_R=tu(1-q_R)-uq_M.$$

The manufacturer receives wholesale revenue plus direct-channel revenue, less the direct selling cost and fixed quality cost. The retailer receives its retail margin times $q_R$. Encroachment means $q_M>0$ on the equilibrium path, rather than the mere existence of a direct channel (Ha, Long and Nasiry, pp. 8, 11, 15, 36).

Formalization targets

Equal quality under encroachment

For a subgame-perfect equilibrium $\sigma$ of the fixed-cost game, the goal is Proposition 6(i):

$$q_M(\sigma)>0\quad\Longrightarrow\quad t(\sigma)=1.$$

The formal statement assumes $c>0$. At $c=0$, the high-direct-quality reduced profit is independent of $t$, so the printed claim fails to force $t=1$; this is a substantive qualification of the manuscript's standing $c\ge0$ convention. The goal concerns the complete game, with contingent actions at every decision node, rather than only the closed-form optimization problem (Ha, Long and Nasiry, pp. 20, 36).

Subgame and optimization claims

The milestone list follows the authors' two quality regimes. The e-Companion gives best responses, wholesale prices, and reduced profits in each regime. In the high-direct-quality regime, Claim 3 concludes that an optimum with positive direct sales has $t=1$. In the low-direct-quality regime, Lemma 2 concludes that an optimum either has $t=1$ or lies at no encroachment. The latter alternative is outside the strict encroachment-feasible set used by the Lean milestone. Footnote 2 supplies a one-variable sign inequality used in the analysis of that regime (Ha, Long and Nasiry, pp. 36–37).

What the result gives

Proposition 6(i) determines the manufacturer's quality choice conditional on active direct sales: both channels carry quality $u$. It narrows the set of equilibrium outcomes that the fixed-cost model can support and distinguishes the role of a one-time design cost from the paper's earlier variable-cost model. The paper states a separate profit comparison in Proposition 6(ii); this mission does not formalize it because the e-Companion omits its proof and the fixed-cost no-encroachment benchmark for that comparison is not stated (Ha, Long and Nasiry, pp. 20, 37).

A complete Lean development would connect the reduced-profit calculations on page 36 to subgame-perfect play in the three-stage game, and establish the optimization claims over their stated feasible sets. The definitions of two-quality inverse demand, contingent strategies, and nodewise optimality are reusable for related channel games. The goal and milestones here are draft statements, without machine-checked proofs of their economic conclusions.

Central difficulty

The manufacturer chooses quality and wholesale price before the retailer's order, yet the direct quantity is chosen only after that order. Consequently, the retailer's payoff depends on the manufacturer's continuation response, and the first-stage choice must account for both later decisions. The reduced profit also changes at $t=1$, where the higher-quality channel switches. A calculation for one regime alone does not establish the full-game claim. The strict $q_M>0$ region matters: its boundary represents no encroachment and supports a different alternative in Lemma 2 (Ha, Long and Nasiry, p. 36).

Formalization scope

Lean uses real wholesale prices and qualities, positive $u$ and $t$, and nonnegative quantities. Wholesale price has no sign restriction in the manuscript. The market has unit size and the retailer's selling cost is zero. The two inverse-demand expressions are applied to all nonnegative quantities, following the paper's algebraic game model. A profile contains a stage-one action, a retailer order rule for every observed $(w,u,t)$, and a direct-quantity rule for every observed $(w,u,t,q_R)$. Subgame perfection requires feasible best replies at every such history, including histories off the equilibrium path. Fixed cost is $\max\{ku^2,k(tu)^2\}$, paid once, while $cq_M$ is a per-unit selling cost.

The reduced profits $\Pi_{\mathrm{Hi}}$ and $\Pi_{\mathrm{Lo}}$ are used only on their respective open encroachment-feasible domains, where the displayed denominators are positive. Claim 3 is stated for a joint maximizer in $(t,u)$; keeping $u$ fixed while moving to $t=1$ can leave that feasible set. Lemma 2 excludes the no-encroachment boundary in its Lean statement. Neither reduced profit replaces the full-game payoff in the goal. Contributions that connect the subgame formulas to arbitrary equilibrium profiles, prove the sign inequality, or establish the two optimization results are within scope (Ha, Long and Nasiry, pp. 36–37).

Selected references

• A. Ha, X. Long and J. Nasiry, Quality in Supply Chain Encroachment, authors' manuscript, SSRN 3970373, published in Manufacturing & Service Operations Management 18(2), 2016. Manuscript. Journal DOI.

Motivation

Linear convergence of first-order methods is usually proved through an error bound: near a solution, the distance to the solution set is controlled by the size of a computable residual, such as the length of a proximal-gradient step. For the prox-linear method, which minimizes a composition $h(c(x))$ of a nonsmooth outer function $h$ with a smooth map $c$ by repeatedly solving the subproblem obtained from linearizing $c$, Drusvyatskiy and Lewis showed in §5 of their paper (arXiv:1602.06661, Theorem 5.10) that the error bound is equivalent to subregularity of the subdifferential $\partial\varphi$, a property of the objective alone and closely tied to quadratic growth. That result needs $h$ convex and finite-valued.

Many composite models violate both assumptions: constraints enter as indicator functions ($h=+\infty$ off a set), and outer functions such as truncated or concave-composite penalties are nonconvex. §8 of the paper extends the equivalence to closed, extended-real-valued, prox-regular $h$. This mission formalizes that extension (Theorem 8.11) together with the results of §8 its proof rests on.

Setting

Fix a $C^1$-smooth map $c:\mathbb R^n\to\mathbb R^m$ and a closed (lower semicontinuous) function $h:\mathbb R^m\to\overline{\mathbb R}=\mathbb R\cup\{\pm\infty\}$, and consider

$$\min_x\ \varphi(x)=h(c(x)).\qquad(8.2)$$

The linearized function is $\varphi(x;y)=h\big(c(x)+\nabla c(x)(y-x)\big)$ and, for $t>0$, $\varphi_t(x;y)=\varphi(x;y)+\frac1{2t}\|x-y\|^2$.

Subgradients are built in three layers (Definition 8.1). A vector $v$ is a proximal subgradient of $f$ at $\bar x$ ($f(\bar x)$ finite) if $f(x)\ge f(\bar x)+\langle v,x-\bar x\rangle-\frac r2\|x-\bar x\|^2$ for some $r>0$ and all $x$ near $\bar x$. The limiting subdifferential $\partial f(\bar x)$ collects limits of proximal subgradients $v_i\in\partial_pf(x_i)$ with $(x_i,f(x_i),v_i)\to(\bar x,f(\bar x),v)$; $\bar x$ is stationary if $0\in\partial f(\bar x)$. The horizon subdifferential $\partial^\infty f(\bar x)$ collects limits of $t_iv_i$ with $v_i\in\partial f(x_i)$, $t_i\searrow0$, $(x_i,f(x_i))\to(\bar x,f(\bar x))$.

The map $c$ is transverse to $h$ at $\bar x$, written $c\pitchfork_{\bar x}h$, if $\partial^\infty h(c(\bar x))\cap\operatorname{Null}(\nabla c(\bar x)^*)=\{0\}$ (8.3). The stationary point map $\mathcal S_t(x)$ is the set of stationary points of $\varphi_t(x;\cdot)$, and the prox-gradient mapping is $\mathcal G_t(x)=t^{-1}(x-\mathcal S_t(x))$; both are set-valued.

A set-valued map $F$ is subregular at $(\bar x,\bar y)\in\operatorname{gph}F$ with constant $l>0$ if $\operatorname{dist}(x;F^{-1}(\bar y))\le l\operatorname{dist}(\bar y;F(x))$ for $x$ near $\bar x$ (Definition 5.7), and metrically regular around $(\bar x,\bar y)$ if the same holds with $\bar y$ replaced by every $y$ near $\bar y$ (Definition 8.3). A closed $f$ is prox-regular at $\bar x$ for $\bar v\in\partial f(\bar x)$ if the quadratic minorant $f(y)\ge f(x)+\langle v,y-x\rangle-\frac r2\|y-x\|^2$ holds uniformly for $x,y$ near $\bar x$ with $f(x)$ near $f(\bar x)$ and $v\in\partial f(x)$ near $\bar v$ (Definition 8.7). Finally, a $\varphi$-attentive localization of $\partial\varphi$ around $(\bar x,0)$ is a map $W$ agreeing with $\partial\varphi(x)$ near $0$ whenever $x$ is near $\bar x$ and $\varphi(x)$ is near $\varphi(\bar x)$; a $\varphi(\cdot,\cdot)$-attentive localization of $\mathcal S_t$ agrees with $\mathcal S_t(x)$ at points $y$ near $\bar x$ with $\varphi(x;y)$ near $\varphi(\bar x)$, and one of $\mathcal G_t$ has the form $t^{-1}(I-\widehat W)$ with $\widehat W$ such a localization of $\mathcal S_t$ (Definition 8.10).

Formalization targets

Goal: Theorem 8.11 (p. 31)

Assume $c\pitchfork_{\bar x}h$, $0\in\partial\varphi(\bar x)$, $\nabla c$ Lipschitz around $\bar x$, and $h$ prox-regular at $c(\bar x)$ for every $w\in\partial h(c(\bar x))$ with $\nabla c(\bar x)^*w=0$. Let (i) be "some $\varphi$-attentive localization of $\partial\varphi$ is subregular at $(\bar x,0)$" and (ii) "some $\varphi(\cdot,\cdot)$-attentive localization of $\mathcal G_t$ is subregular at $(\bar x,0)$". Then

$$\text{(i)}\Rightarrow\text{(ii) for all }t>0,\qquad \exists\,\bar t>0:\ \text{(ii)}\Rightarrow\text{(i) for all }t\in(0,\bar t),$$

and, when $h$ is convex, $\partial\varphi$ is subregular at $(\bar x,0)$ if and only if $\mathcal G_t$ is, for every $t>0$. The constants of subregularity are left existential: the goal asserts the shape of the equivalence, not a particular constant.

Milestones

1. Theorem 8.4 (p. 26): metric regularity of a closed set-valued map is preserved, with uniform constants, under affine perturbations $H$ with small $\|\nabla H\|$.
2. Corollary 8.5 (p. 26): a constraint system $F(x)\in Q$ transverse at $\bar x$ is uniformly metrically regular under small affine perturbations.
3. Theorem 8.6 (p. 27): the comparison inequalities between $\varphi(y)$ and $\varphi(x;\cdot)$ after moving $y$ by $O(\|y-x\|^2)$.
4. Proposition 8.8 (p. 28): the linearized maps inherit transversality, and $\varphi(x;\cdot)$ is prox-regular at $\bar x$ uniformly in $x$ (8.4).
5. Theorem 8.9 (p. 29): every stationary point $x^t$ of the subproblem lies near a point $\hat x$ that is nearly stationary for $\varphi$, with $\operatorname{dist}(0;\partial\varphi(\hat x))\le(a+b/t)\|x^t-x\|$.

Significance

Subregularity of $\mathcal G_t$ at $(\bar x,0)$ is exactly the error bound property of the prox-linear step, the hypothesis under which linear convergence arguments run. Theorem 8.11 says that, for the attentive parts of the graphs, this property is equivalent to subregularity of $\partial\varphi$, which does not refer to any algorithm or step size. It therefore covers constrained composite problems (indicator functions $h$), nonconvex prox-regular penalties, and, in the convex case, removes the finite-valuedness assumption of Theorem 5.10.

The results are proved in the paper, partly by citation to Dontchev, Lewis and Rockafellar and to Lewis and Wright's analysis of prox-linear subproblems (arXiv:0812.0423). None of them is formalized: Mathlib has no proximal, limiting or horizon subdifferential, no metric regularity, and no prox-regularity. A formalization supplies these notions, checks the constant-chasing in Theorems 8.9 and 8.11, and fixes the precise quantifier order the prose leaves implicit.

Difficulty

The obvious route, copying the §5 argument, fails at its first step: §5 starts from the inequalities $|\varphi(y)-\varphi(x;y)|\le\frac{L\beta}2\|x-y\|^2$, and when $h$ takes the value $+\infty$ one of $\varphi(y)$, $\varphi(x;y)$ can be finite while the other is infinite, so no such inequality holds. Theorem 8.6 replaces it by a comparison after perturbing $y$, which needs the stability of metric regularity (Theorem 8.4) and the epigraphical description of subgradients. A second obstacle is that $\mathcal S_t$ collects stationary points of nonconvex subproblems, so it is set-valued and possibly empty; the proofs need prox-regularity that is uniform over the family $\varphi(x;\cdot)$ (Proposition 8.8) and a local existence result for $\mathcal S_t$ to obtain the threshold $\bar t$. The limiting-subdifferential calculus (the chain rule $\partial\varphi(\bar x)\subseteq\nabla c(\bar x)^*\partial h(c(\bar x))$ under transversality) is itself a substantial piece of variational analysis.

Formalization scope

Points are in EuclideanSpace ℝ (Fin n); $h$, $\varphi$, $\varphi(x;\cdot)$ and $\varphi_t(x;\cdot)$ are EReal-valued. Standing assumptions on every statement: $c$ is $C^1$ (ContDiff ℝ 1 c), $h$ is lower semicontinuous and never $-\infty$ (the page's closed functions are only ever evaluated where finite or $+\infty$; this is a disclosed addition). $\nabla c(x)$ is fderiv ℝ c x and $\nabla c(x)^*$ its adjoint. "$|a-\varphi(\bar x)|<\epsilon$" requires $a$ finite. $\operatorname{dist}(\bar y;\varnothing)=+\infty$, so (sub)regularity inequalities are stated for every element of $F(x)$, and metric regularity carries nonemptiness of $F^{-1}(y)$; $\operatorname{dist}(0;\partial\varphi(\hat x))\le r$ is the existence of a subgradient of norm at most $r$. $\mathcal S_t$ and $\mathcal G_t$ are sets defined by stationarity, never a chosen minimizer. Two printed slips are corrected and disclosed: in Definition 8.10 (2) the neighbourhood $\mathcal Y$ is a neighbourhood of $\bar x$, and in Theorem 8.11 the threshold satisfies $\bar t>0$ (with $\bar t=0$ the converse would be vacuous). "When $h$ is convex" is the convexity inequality in $\overline{\mathbb R}$, with the theorem's other hypotheses kept.

A trivializing formalization is ruled out: subregularity always includes $0\in F(\bar x)$, a constant $l>0$ and a neighbourhood, so the content of (i) and (ii) cannot collapse into the trivial existence of a localization (any map is a localization of itself); and distances to empty sets are never junk zeros.

A complete development needs the three subdifferentials and their basic calculus (sum rule with a smooth function, chain rule under transversality, closedness of the limiting subdifferential), metric regularity and its perturbation stability, Ekeland's variational principle (on the platform as EkelandVP.General.ekeland_variational_principle), and a local existence result for stationary points of the subproblems. The subdifferential and regularity layer is reusable well beyond this mission. Proofs of any milestone, and of supporting lemmas on the variational-analysis substrate, are welcome.

Selected references

• D. Drusvyatskiy and A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Math. Oper. Res. 43(3), 2018; arXiv:1602.06661v2. https://arxiv.org/abs/1602.06661
• A. L. Dontchev, A. S. Lewis and R. T. Rockafellar, The radius of metric regularity, Trans. Amer. Math. Soc. 355(2), 2003. https://doi.org/10.1090/S0002-9947-02-03088-X
• A. S. Lewis and S. J. Wright, A proximal method for composite minimization, Math. Program. 158, 2016. https://arxiv.org/abs/0812.0423
• R. A. Poliquin and R. T. Rockafellar, Prox-regular functions in variational analysis, Trans. Amer. Math. Soc. 348(5), 1996. https://doi.org/10.1090/S0002-9947-96-01544-9
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Grundlehren 317, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

The convex feasibility problem asks for a point in the intersection of closed convex sets. It underlies signal and image reconstruction, phase retrieval relaxations, and the constraint handling inside larger optimization methods. The workhorse algorithms are projection methods: the method of alternating projections (MAP), going back to von Neumann for subspaces, and the Douglas–Rachford and Peaceman–Rachford splitting schemes, which can be applied to the indicator, distance or squared-distance functions of the sets.

Without a regularity condition on how the sets meet, projection methods can converge arbitrarily slowly. Bounded linear regularity, an error bound saying that a point close to every set is close to their intersection, is the standard condition under which linear rates are obtained (Bauschke and Borwein, SIAM Review, 1996, doi:10.1137/S0036144593251710). Section 5 of D. Davis and W. Yin, Faster convergence rates of relaxed Peaceman–Rachford and ADMM under regularity assumptions (arXiv:1407.5210v3, Math. Oper. Res. 42(3), 2017) applies relaxed Peaceman–Rachford splitting (PRS) to the squared distance functions of two sets and proves that, under bounded linear regularity, the distance of the iterates to the intersection contracts by an explicit factor at every step, with step sizes and relaxation parameters allowed to vary between iterations. MAP is the special case of step size $1/2$ and relaxation $1$.

Setting

Let $\mathcal H$ be a real Hilbert space and $C_f, C_g \subseteq \mathcal H$ closed convex sets with $C_f\cap C_g\neq\emptyset$. For $C\subseteq\mathcal H$ the distance function is $d_C(x)=\inf_{y\in C}\|x-y\|$, and $P_C$ is the metric projection, the nearest point of $C$. The problem is modelled with

$$f(x)=d^2_{C_f}(x),\qquad g(x)=d^2_{C_g}(x).$$

For $\gamma>0$ the proximal map $\mathbf{prox}_{\gamma h}(x)$ is the minimiser of $h(y)+\frac1{2\gamma}\|y-x\|^2$, and the reflection is $\mathbf{refl}_{\gamma h}=2\,\mathbf{prox}_{\gamma h}-I$. With two step sizes, $T^{\gamma_f,\gamma_g}_{\mathrm{PRS}}=\mathbf{refl}_{\gamma_f f}\circ\mathbf{refl}_{\gamma_g g}$, and $(T)_\lambda=(1-\lambda)I+\lambda T$.

Given $z^0$, step sizes $\gamma_{f,k},\gamma_{g,k}>0$ and relaxation parameters $\lambda_k\in(0,1]$, iteration (5.1) is

$$x_g^k=\mathbf{prox}_{\gamma_{g,k}d^2_{C_g}}(z^k),\quad x_f^k=\mathbf{prox}_{\gamma_{f,k}d^2_{C_f}}(2x_g^k-z^k),\quad z^{k+1}=z^k+2\lambda_k(x_f^k-x_g^k).$$

The pair $\{C_f,C_g\}$ is boundedly linearly regular (Definition 5.1) if for every $\rho>0$ there is $\mu_\rho>0$ such that

$$d_{C_f\cap C_g}(x)\le\mu_\rho\max\{d_{C_f}(x),d_{C_g}(x)\}\qquad\text{for all }x\in B(0,\rho),$$

where $B(0,\rho)$ is the open ball. The rate function is

$$C(\gamma_f,\gamma_g,\lambda,\mu)=\left(1-\frac{4\lambda\min\{\gamma_g/(2\gamma_g+1)^2,\ \gamma_f/(2\gamma_f+1)^2\}}{\mu^2\max\{16\gamma_g^2/(2\gamma_g+1)^2,\ 1\}}\right)^{1/2}.$$

Formalization targets

Goal: Theorem 5.1

Suppose $\{C_f,C_g\}$ is boundedly linearly regular, $(z^k)$ is generated by (5.1), every $z^j$ lies in $B(0,\rho)$, and $d_{C_f\cap C_g}\le\mu_\rho\max\{d_{C_f},d_{C_g}\}$ on $B(0,\rho)$. Then for all $k\ge0$

$$d_{C_f\cap C_g}(z^{k+1})\le C(\gamma_{f,k},\gamma_{g,k},\lambda_k,\mu_\rho)\,d_{C_f\cap C_g}(z^k), \tag{5.3}$$

and if $\overline C=\sup_j C(\gamma_{f,j},\gamma_{g,j},\lambda_j,\mu_\rho)<1$, the iterates converge to a point $x\in C_f\cap C_g$ with

$$\|z^k-x\|\le 2\,d_{C_f\cap C_g}(z^0)\prod_{i=0}^{k-1}C(\gamma_{f,i},\gamma_{g,i},\lambda_i,\mu_\rho). \tag{5.4}$$

Milestones

The milestones follow the paper's own argument: Proposition 5.1 Parts 2 and 3 (the gradient of $d_C^2$ and the closed form $\mathbf{prox}_{\gamma d_C^2}=\frac1{2\gamma+1}I+\frac{2\gamma}{2\gamma+1}P_C$); Proposition 5.2, the fundamental inequality specialised to squared distances; Propositions C.1 and C.2 (the fixed-point set of $T^{\gamma_f,\gamma_g}_{\mathrm{PRS}}$ is $C_f\cap C_g$, and the iterates are Fejér monotone for $\lambda_k\in(0,1]$); and the displays (5.5)–(5.7), (5.8), (5.10) and (5.11) of the proof of Theorem 5.1, ending with the one-step contraction at a single point.

Companion: Corollary 5.1

With $\gamma_{f,k}\equiv\gamma_{g,k}\equiv\frac12$ and $\lambda_k\equiv1$, iteration (5.1) is MAP, $z^{k+1}=P_{C_f}P_{C_g}z^k$, and under the assumptions of Theorem 5.1 it contracts the distance to $C_f\cap C_g$ by $(1-1/\mu_\rho^2)^{1/2}$ from the second iterate on, converging linearly to a point of the intersection.

Significance

Theorem 5.1 gives an explicit, iteration-wise linear rate for relaxed PRS on the two-set feasibility problem with step sizes and relaxation parameters that may change from step to step. Its specialisation, Corollary 5.1, recovers linear convergence of MAP under bounded linear regularity with rate $(1-1/\mu_\rho^2)^{1/2}$, better than the $(1-1/(8\mu^2))^{1/2}$ derived in earlier work on cyclic projections. Remark 5.1 of the paper notes that Douglas–Rachford on indicator functions is a limiting case of the scheme as the step sizes grow, though the rate degenerates in that limit.

The results are proved in the paper; the proof of the convergence statement cites Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Theorem 5.12 (Fejér monotone sequences whose distance to a closed convex set decays converge strongly). No machine-checked proof of these statements was found on Prove2Me (search of 2026-10-07). A formalization produces a checked chain from the closed form of the prox of $d_C^2$ through the fundamental inequality to the linear rate, and with it reusable facts about squared distance functions, metric projections onto closed convex sets in Hilbert space, and Fejér monotone sequences.

Difficulty

The obvious argument would contract the distance to $C_f\cap C_g$ directly, but one PRS step measures only $d_{C_g}$ at $z$ and $d_{C_f}$ at the reflected point $\mathbf{refl}_{\gamma_g g}(z)$, never $d_{C_f}(z)$. Transferring the second distance back to $z$ costs a factor $\max\{c_1^2,1\}$ with $c_1=4\gamma_g/(2\gamma_g+1)$, and only after that does the regularity inequality turn $\max\{d_{C_f}(z),d_{C_g}(z)\}$ into $d_{C_f\cap C_g}(z)$. The fundamental inequality (5.2) itself rests on the prox-gradient calculus of the earlier sections, specialised to functions whose gradients $2(I-P_C)$ are Lipschitz. Passing from a contracting distance to convergence of the iterates to one point needs Fejér monotonicity and a completeness argument; a contracting distance alone does not give a limit.

Formalization scope

Everything lives in a real Hilbert space (InnerProductSpace ℝ H with CompleteSpace H); $d_C$ is Mathlib's Metric.infDist. The squared distance is viewed as an extended-real function so that the published proximal predicate ThreeOpSplitting.ConvexRates.IsProx applies, and prox maps are arbitrary maps satisfying it (unique here). Metric projections are maps satisfying the published RandomGradFree.Nonsmooth.IsMetricProjection. Step sizes and prox maps are indexed by the iteration. The hypotheses of the goal are: $C_f,C_g$ closed and convex with nonempty intersection; bounded linear regularity of the pair; $\gamma_{f,k},\gamma_{g,k}>0$; $\lambda_k\in(0,1]$; iterates in an open ball $B(0,\rho)$ on which the regularity inequality holds with $\mu_\rho>0$. The range $\lambda_k\in(0,1]$ is Algorithm 1's standing assumption, used in the proof but not restated in (5.1). The condition $\overline C<1$ is stated as a uniform bound $c<1$ on all rate factors. The product in (5.4) runs over $i=0,\dots,k-1$; the page prints the upper index $k$, which claims an extra factor that the proof does not give. In the proof's (5.9)–(5.10) the page swaps $\gamma_f$ and $\gamma_g$ relative to (5.2); the milestone states the pairing that (5.2) produces. Corollary 5.1's improved rate is stated for $k\ge1$, since it uses $z^k\in C_f$.

A trivializing formalization is ruled out: the goal mentions none of the proof's intermediate quantities, takes the prox maps as genuine minimisers of the squared-distance objective rather than chosen points, and measures distances to a nonempty intersection, so the junk value of infDist on the empty set never arises.

A complete development needs the closed form of $\mathbf{prox}_{\gamma d^2_C}$, differentiability of $d_C^2$, the fundamental inequality of the paper's §1 specialised to these functions, and the convergence theorem for Fejér monotone sequences. The last three are reusable well beyond this mission. Proofs of any milestone, and of Mathlib-level lemmas on metric projections, are welcome.

Selected references

• D. Davis, W. Yin, Faster convergence rates of relaxed Peaceman–Rachford and ADMM under regularity assumptions, Mathematics of Operations Research 42(3), 2017; arXiv version used here: arXiv:1407.5210v3.
• H. H. Bauschke, J. M. Borwein, On projection algorithms for solving convex feasibility problems, SIAM Review 38(3), 1996. doi:10.1137/S0036144593251710
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. doi:10.1007/978-1-4419-9467-7
• P.-L. Lions, B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM Journal on Numerical Analysis 16(6), 1979. doi:10.1137/0716071

Motivation

Many large optimization problems in signal processing, statistics and machine learning have a variable that splits naturally into blocks, and are solved by updating one block at a time. The classical method of this kind, block coordinate descent (BCD), minimises the objective exactly in one block while the others are held fixed. In practice the exact block subproblem is often too expensive, and one minimises instead a simpler function that upper-bounds the objective and touches it at the current point. The EM algorithm, DC (difference of convex) programming, proximal and linearised block updates and several alternating schemes for matrix factorisation and transceiver design are all of this form.

Razaviyayn, Hong and Luo (arXiv:1209.2385, SIAM J. Optim. 23 (2013)) gave one convergence analysis for this whole family, the block successive upper-bound minimization (BSUM) method, without convexity or smoothness of the objective. This mission formalizes the block part of that analysis: the cyclic BSUM method (Theorem 2) and its maximum-improvement variant MISUM (Theorem 3).

Timeline. Bertsekas (Nonlinear Programming, 1999, Prop. 2.7.1) proved that limit points of cyclic BCD are stationary for continuously differentiable objectives over a product of closed convex sets when each block minimiser is unique. Tseng (J. Optim. Theory Appl. 109, 2001) treated nondifferentiable objectives using regularity and coordinatewise minima. Chen, He, Li and Zhang (SIAM J. Optim. 22, 2012) introduced maximum block improvement, which drops the uniqueness assumption. The 2013 paper extends these results from exact block minimisation of $f$ to minimisation of block upper bounds.

Setting

The problem is

$$\min_x\ f(x)\quad\text{s.t.}\quad x\in\mathcal X=\mathcal X_1\times\cdots\times\mathcal X_n,\qquad (12)$$

where each $\mathcal X_i\subseteq\mathbb R^{m_i}$ is a closed convex set and $f$ is a continuous real function on $\mathcal X$. A point is $x=(x_1,\dots,x_n)$ with $x_i\in\mathbb R^{m_i}$. The directional derivative is $f'(x;d)=\liminf_{\lambda\downarrow0}\,(f(x+\lambda d)-f(x))/\lambda$, a value in $[-\infty,+\infty]$. A point $z\in\mathcal X$ is stationary for (12) if $f'(z;d)\ge0$ for every $d$ with $z+d\in\mathcal X$. The function $f$ is regular at $z$ if $f'(z;d)\ge0$ holds for every $d=(d_1,\dots,d_n)$ such that $f'(z;(0,\dots,d_k,\dots,0))\ge0$ for every block $k$. A point $z\in\mathcal X$ is coordinatewise stationary if $f'(z;d)\ge0$ for every $d=(0,\dots,d_k,\dots,0)$ with $z_k+d_k\in\mathcal X_k$, for every $k$.

For each block $i$ an approximation function $u_i(x_i,y)$ is given, with $x_i\in\mathbb R^{m_i}$ and $y\in\mathcal X$. Assumption 2 requires:

• (B1) $u_i(y_i,y)=f(y)$ for $y\in\mathcal X$;
• (B2) $u_i(x_i,y)\ge f(y_1,\dots,y_{i-1},x_i,y_{i+1},\dots,y_n)$ for $x_i\in\mathcal X_i$, $y\in\mathcal X$;
• (B3) $u_i'(x_i,y;d_i)\big|_{x_i=y_i}=f'(y;(0,\dots,d_i,\dots,0))$ whenever $y_i+d_i\in\mathcal X_i$, the left side being the derivative in $x_i$ only;
• (B4) $u_i$ is continuous in $(x_i,y)$.

The BSUM algorithm (Fig. 2) starts at $x^0\in\mathcal X$ and, at each iteration, picks a block $i$ by the cyclic rule, replaces $x_i$ by any minimiser of $u_i(\cdot,x^{r-1})$ over $\mathcal X_i$, and keeps the other blocks. The MISUM algorithm (Fig. 3) instead updates a block $k$ attaining $\min_i\min_{x_i\in\mathcal X_i}u_i(x_i,x^{r-1})$.

Formalization targets

Goal: Theorem 2(a)

If each $u_i(x_i,y)$ is quasi-convex in $x_i$, Assumption 2 holds and every block subproblem $\min_{x_i\in\mathcal X_i}u_i(x_i,y)$, $y\in\mathcal X$, has a unique solution, then every limit point $z$ of the cyclic BSUM iterates satisfies

$$f'(z;d)\ge0\qquad\forall\,d=(0,\dots,d_k,\dots,0),\ z_k+d_k\in\mathcal X_k,\ k=1,\dots,n,$$

and $z$ is a stationary point of (12) if $f$ is regular at $z$.

Milestones

The proof passes through the monotonicity $f(x^0)\ge f(x^1)\ge\cdots$ (14); the limit $\lim_r f(x^r)=f(z)$ at a limit point $z$ (15); the claim that $x^{r_j}\to z$ forces $x^{r_j+1}\to z$; block minimality $u_k(z_k,z)\le u_k(x_k,z)$ for all $x_k\in\mathcal X_k$ and every $k$; and the first-order condition $u_k'(x_k,z;d_k)|_{x_k=z_k}\ge0$ for feasible $d_k$ (22).

Companions

Theorem 2(b): if the level set $\mathcal X^0=\{x\in\mathcal X: f(x)\le f(x^0)\}$ is compact, block minimisers are unique in at least $n-1$ blocks and $f$ is regular on $\mathcal X^0$, then $d(x^r,\mathcal X^*)\to0$, where $\mathcal X^*$ is the set of stationary points. Theorem 3: under Assumption 2 alone, every limit point of the MISUM iterates is coordinatewise stationary, and stationary where $f$ is regular.

Significance

Theorem 2 is the stationarity guarantee for every method that can be written as cyclic block minimisation of tight upper bounds: block EM, alternating DC iterations, proximal block updates, and the matrix-factorisation and beamforming schemes of Section VIII of the paper. Each such method needs only a check of (B1)–(B4) to inherit it. Theorem 3 shows that the uniqueness assumption, which part (a) needs and BCD needs too, can be traded for a greedy block choice.

The results are proved in the paper. As far as the platform's catalogue shows, none of them has been formalized; the related published work is the formalization of Tseng's 2001 setting (directional derivative, stationarity, regularity, cyclic rule), which this mission reuses. Formalizing the analysis checks the "without loss of generality" and "by further restricting to a subsequence" steps, which carry most of the argument, and gives reusable statements about limit points of block methods.

Difficulty

The obvious argument shows that $f(x^r)$ decreases and that a limit point $z$ satisfies the block optimality condition for the block updated along the convergent subsequence. It does not say anything about the other blocks: consecutive iterates may stay a fixed distance apart, so the next iterate need not converge to $z$, and then nothing is known about $z$ in the next block. Showing that $x^{r_j+1}\to z$ is the central step, and it is exactly where quasi-convexity and uniqueness of the block minimisers are used. Without uniqueness, limit points of even exact cyclic BCD need not be stationary (Powell's examples, which the paper cites), which is why Theorem 2(b) needs compactness and Theorem 3 needs a different update rule.

The step from block minimality to stationarity is a second gap: (B3) only matches derivatives in coordinate directions, and passing to all directions requires regularity of $f$.

Formalization scope

The space $\mathbb R^{m_1}\times\cdots\times\mathbb R^{m_n}$ is the dependent product X n of the referenced Tseng setting, with blocks indexed $0,\dots,N-1$ (paper block $k$ is index $k-1$). It carries the sup norm over blocks, which matters only for distances; convergence statements do not depend on the norm. The block sets are closed and convex, $f$ is a real function continuous on $\mathcal X$, and $x^0\in\mathcal X$; these standing hypotheses of Section IV appear in every statement.

The paper assumes $\operatorname{dom}f=\mathcal X$. Accordingly $f$ is extended by $+\infty$ off $\mathcal X$, and stationarity and regularity are those of the extension. Directional derivatives are extended-real liminfs, never real-valued limits with a junk value. A run is a predicate on a sequence: each new block is a minimiser of the block subproblem, but existence of minimisers is not assumed. The cyclic rule updates block $r \bmod N$ on the step $x^r\to x^{r+1}$, a relabelling of Fig. 2's $i=(r\bmod n)+1$. Limit points are cluster points of the sequence.

Deviations from the printed statements, each disclosed in the items:

• Theorems 2(a) and 3 say "coordinatewise minimum". Their proofs establish coordinatewise stationarity and call it that, and the literal minimum claim is false (one block, $\mathcal X=[-1,1]$, $f(x)=-x^2$, a quadratic upper bound tight at the iterate; the run stays at $0$ while $f(1)<f(0)$). The statements assert coordinatewise stationarity.
• Theorem 2(b) assumes regularity "at every point in the set of stationary points"; the proof applies it at a limit point not yet known to be stationary. The statement assumes regularity on the level set $\mathcal X^0$, as Tseng's Theorem 4.1 does.
• $d(x^r,\mathcal X^*)\to0$ is stated as "for every $\varepsilon>0$, eventually $x^r$ is within $\varepsilon$ of a stationary point", so an empty $\mathcal X^*$ cannot make it true.

Trivializing formalizations are ruled out: hypotheses on $u_i$ are required on all of $\mathcal X$, not just along the run; uniqueness is required at every $y\in\mathcal X$; and a sorry-free check shows that all hypotheses of Theorem 2(a) hold together for a one-block instance.

Not formalized: Proposition 2 (a sufficient condition for (B3)), Corollaries 2 and 3 (essentially cyclic and overlapping rules) and the applications of Section VIII. Contributions of reusable lemmas about cluster points of block methods and first-order conditions for constrained minimisers in a single block are welcome.

Selected references

• M. Razaviyayn, M. Hong, Z.-Q. Luo, A unified convergence analysis of block successive minimization methods for nonsmooth optimization, arXiv:1209.2385v1, 2012; SIAM J. Optim. 23(2) (2013) 1126–1153. https://arxiv.org/abs/1209.2385
• P. Tseng, Convergence of a block coordinate descent method for nondifferentiable minimization, J. Optim. Theory Appl. 109 (2001) 475–494. https://doi.org/10.1023/A:1017501703105
• D. P. Bertsekas, Nonlinear Programming, 2nd ed., Athena Scientific, 1999.
• B. Chen, S. He, Z. Li, S. Zhang, Maximum block improvement and polynomial optimization, SIAM J. Optim. 22(1) (2012) 87–107. https://doi.org/10.1137/110834858
• M. J. D. Powell, On search directions for minimization algorithms, Math. Program. 4 (1973) 193–201. https://doi.org/10.1007/BF01584660

Motivation

Manufacturers increasingly sell directly to consumers while continuing to supply independent retailers, a practice known as supply chain encroachment. The direct channel competes with the retailer for the same consumers, and the conventional advice for easing that conflict is to sell different products in the two channels. Ha, Long and Nasiry (MSOM 18(2), 2016; authors' manuscript SSRN 3970373) study this advice in a model where the manufacturer chooses product quality herself. This mission formalizes their Section 5: when the manufacturer may offer one quality directly and another through the retailer, which channel gets the better product, when is differentiation worth it, and who gains from encroachment.

The model builds on two lines of work. With exogenous quality, Arya, Mittendorf and Sappington (Marketing Science, 2007) showed that encroachment can benefit both firms, through a lower wholesale price. Vertical differentiation with a convex cost of quality goes back to Mussa and Rosen (JET, 1978), Moorthy (1988) and Motta (1993), where differentiation lets firms segment the market. The paper combines the two and finds that, once quality is endogenous, the retailer never gains.

Setting

A market of size $1$ consists of consumers with types $\theta$ uniformly distributed on $[0,1]$; a consumer of type $\theta$ obtains surplus $\theta v-p$ from a product of quality $v$ at price $p$. A manufacturer sells a product of quality $u>0$ through her direct channel and a product of quality $tu$, with quality ratio $t>0$, through a retailer. Producing one unit of quality $v$ costs $kv^2$ ($k>0$); every unit sold directly costs a further direct selling cost $c\ge 0$; the retailer's selling cost is $0$.

With quantities $q_M$ (direct) and $q_R$ (retailer), the market-clearing prices are, for $t\le 1$ (direct channel carries the higher quality),

$$p_M=u(1-q_M-t\,q_R),\qquad p_R=tu(1-q_M-q_R),$$

and for $t>1$ (retailer carries the higher quality)

$$p_M=u(1-q_M-q_R),\qquad p_R=tu(1-q_R)-u\,q_M .$$

The profits are $\Pi_R=(p_R-w)q_R$ and $\Pi_M=(w-k(tu)^2)q_R+(p_M-c-ku^2)q_M$.

The game has three stages: (i) the manufacturer chooses a wholesale price $w$, the quality $u$ and the ratio $t$; (ii) the retailer orders $q_R\ge0$; (iii) the manufacturer chooses $q_M\ge0$. Solutions are subgame-perfect equilibria. The manufacturer encroaches when $q^*_M>0$ on the equilibrium path. Fixing $t=1$ gives the uniform-quality game of §4.1. The benchmark of §3.2 has no direct channel; its equilibrium profits are $\Pi^N_M=\frac1{54k}$ and $\Pi^N_R=\frac1{108k}$.

Formalization targets

Goal: Proposition 4(ii)

In every subgame-perfect equilibrium with $q^*_M>0$,

$$\Pi^*_M>\frac{1}{54k}=\Pi^N_M\qquad\text{and}\qquad \Pi^*_R<\frac{1}{108k}=\Pi^N_R .$$

The statement makes no assumption on which quality the manufacturer chooses, on the size of $c$ or on the form of the equilibrium; the constants are the benchmark's.

Milestones

1. The benchmark equilibrium ($u^N=\frac1{3k}$, $w^N=\frac2{9k}$, $q^N_R=\frac16$ and the two profits), p. 9.
2. The quantity subgame (7) for $t<1$, p. 16, and the reduced profit $\Pi_M(t,u)$ obtained by optimizing $w$, p. 29.
3. Lemma 1(i)–(ii): the manufacturer's optimal ratio $t(u)$ for given $u$, when the retailer's product is lower ($t\le1$) or higher ($t\ge1$) quality.
4. Claim 1 and Lemma 1(iii): for $c<\frac1{12k}$ the profits of the two kinds of differentiation cross exactly once in $u$.
5. Proposition 3: under encroachment, $t^*\le1$.
6. Proposition 1(iii) in the uniform-quality game.
7. Claim 2 and Proposition 4(i): thresholds $0<c_1<c_2$ such that the manufacturer differentiates ($t^*<1$) for $c<c_1$, uses uniform quality for $c_1<c<c_2$, and does not encroach for $c>c_2$.

Companions

The §6.1 benchmark in which both qualities go through the retailer ($\Pi^{N2}_M=\frac1{50k}$, $\Pi^{N2}_R=\frac1{100k}$), Proposition 5 (the win–lose outcome against that benchmark), and the existence of an equilibrium. The threshold milestones assert existence for each cost, so their conclusions have an equilibrium to describe.

Significance

Proposition 4(ii) says that letting the manufacturer differentiate quality across channels does not change who wins: the manufacturer still gains from encroachment and the retailer still loses, although one might expect the retailer to benefit from not facing an identical product. Proposition 3 adds that differentiation, when used, puts the higher quality in the direct channel, and Proposition 4(i) shows that for intermediate selling costs the manufacturer prefers no differentiation at all, contrary to the monopoly intuition that segmentation always pays. Proposition 5 shows the conclusion persists against a benchmark in which the retailer already carries a two-product line.

The results are proved in the paper, in part with numerical verification (e.g. the bounds on $\hat u$ in the proof of Proposition 3, and the location of $c_1$ and $c_2$). None of them has been machine-checked. A formal development would turn these numerical steps into proofs and would leave a reusable, explicit model of a three-stage Stackelberg game with a vertically differentiated linear demand.

Difficulty

The equilibrium analysis is not a single concave program. Backward induction produces closed forms only on regions (the retailer's order must leave the manufacturer a positive direct quantity, and the retailer's quantity must stay positive), and the manufacturer's stage-1 problem is a comparison across these regions and across $t<1$, $t=1$ and $t>1$. The profit of low-quality encroachment, $\Pi^L_M(u)$, involves a square root in $u$, and the paper controls its critical points by a case analysis on polynomial derivatives with numerically located crossing points (pp. 39–40). The thresholds $c_1\approx0.0973/k$ and $c_2\approx0.1019/k$ are defined implicitly by the equality of maximized profits. Comparing the equilibrium profit with $\frac1{54k}$ therefore requires bounding a maximum taken over a piecewise-defined family, not evaluating one formula.

Formalization scope

The game is defined in QualityEncroach.Differ.Game. Quantities are restricted to be nonnegative; the wholesale price is unrestricted, as in the paper; qualities satisfy $u>0$, $t>0$. The price formulas are used for all nonnegative quantities, as in the paper; the $t>1$ case, which the paper says "can be derived similarly", is that derivation. The equilibrium notion is subgame perfection written in one-shot-deviation form at every history, on and off the path. Benchmark profits appear as the constants $\frac1{54k}$, $\frac1{108k}$ (and $\frac1{50k}$, $\frac1{100k}$); separate items derive them from the benchmark games. Threshold statements give $c_2>0$ and $0<c_1<c_2$ depending only on $k$, assert equilibrium existence at every $c\ge0$, and say nothing at $c=c_2$, where the paper's statements disagree. Lemma 1 and Claim 1 are stated about the paper's reduced-form profits, defined by the displayed formulas in QualityEncroach.Differ.Reduced; the item reduced_profit_high links $\Pi_M(t,u)$ for $t\le1$ to the game. Claim 1 retains $c=0$ and quantifies only over positive qualities, so no reduced form is evaluated at $u=0$.

The goal is about subgame-perfect equilibria of the game, not about the reduced forms: a proof that only compares closed-form profits does not prove it without the milestones linking those forms to equilibrium play. The goal is not vacuous only if an equilibrium with $q^*_M>0$ exists; the companion spe_exists asserts existence.

Contributions are welcome at every level: the benchmark and the quantity subgame are routine calculus on quadratics; Lemma 1(i)–(ii) are one-variable sign analyses; Claim 1, Lemma 1(iii), Proposition 3 and the thresholds require the case analyses of the appendix.

Selected references

• A. Ha, X. Long, J. Nasiry, Quality in Supply Chain Encroachment, Manufacturing & Service Operations Management 18(2), 2016. https://doi.org/10.1287/msom.2015.0562 (authors' manuscript: https://ssrn.com/abstract=3970373)
• A. Arya, B. Mittendorf, D. Sappington, The Bright Side of Supplier Encroachment, Marketing Science 26(5), 2007. https://doi.org/10.1287/mksc.1060.0228
• M. Mussa, S. Rosen, Monopoly and Product Quality, Journal of Economic Theory 18(2), 1978. https://doi.org/10.1016/0022-0531(78)90085-6
• K. S. Moorthy, Product and Price Competition in a Duopoly, Marketing Science 7(2), 1988. https://doi.org/10.1287/mksc.7.2.141
• M. Motta, Endogenous Quality Choice: Price vs. Quantity Competition, Journal of Industrial Economics 41(2), 1993. https://doi.org/10.2307/2950430

Motivation

Many problems in statistics, signal processing and machine learning minimize a smooth loss plus a nonsmooth regularizer over a set with manifold structure: sparse principal component analysis over the Stiefel manifold, sparse blind deconvolution over the sphere, and clustering and dictionary-learning models with orthogonality constraints. In Euclidean space the standard method for such composite problems is the proximal gradient method, whose $O(1/k)$ rate for convex problems is classical (Beck–Teboulle 2009). Huang and Wei (arXiv:1909.06065v4, Mathematical Programming 2021) propose a Riemannian proximal gradient method (RPG) that solves its proximal subproblem on the tangent space and returns to the manifold through a retraction. They prove three things about it: global convergence, an $O(1/k)$ rate under a convexity notion adapted to retractions, and local rates under a Riemannian Kurdyka–Łojasiewicz property. This mission covers the second result, Theorem 3.2.

Earlier Riemannian proximal methods either required the exponential map and parallel transport, or solved a Euclidean proximal problem in the ambient space (Chen, Ma, So, Zhang 2020, ManPG). Theorem 3.2 is stated for a general retraction, with an explicit constant.

Setting

Let $\mathcal M$ be a finite-dimensional Riemannian manifold, with inner product $\langle\cdot,\cdot\rangle_x$ and norm $\|\cdot\|_x$ on each tangent space $T_x\mathcal M$. A retraction is a family of smooth maps $R_x:T_x\mathcal M\to\mathcal M$ with $R_x(0_x)=x$ and $\mathrm DR_x(0_x)=\mathrm{id}$. The problem is

$$\min_{x\in\mathcal M} F(x)=f(x)+g(x),$$

where $f$ is differentiable with Riemannian gradient $\operatorname{grad} f$, and $g$ is continuous and possibly nonsmooth.

For a function $h$ on a real inner-product space $V$, the Clarke generalized directional derivative is $h^\circ(\eta;v)=\limsup_{\xi\to\eta,\,t\downarrow0}(h(\xi+tv)-h(\xi))/t$. The generalized subdifferential is $\partial h(\eta)=\{\zeta\mid\langle\zeta,v\rangle\le h^\circ(\eta;v)\ \forall v\}$. A point $\eta$ is stationary for $h$ if $0\in\partial h(\eta)$.

Given a constant $\tilde L$, the RPG method (Algorithm 1) produces iterates $x_k$ and steps $\eta^*_{x_k}\in T_{x_k}\mathcal M$ as follows. Set

$$\ell_{x_k}(\eta)=\langle\operatorname{grad} f(x_k),\eta\rangle_{x_k}+\frac{\tilde L}{2}\|\eta\|_{x_k}^2+g(R_{x_k}(\eta)).$$

Choose a stationary point $\eta^*_{x_k}$ of $\ell_{x_k}$ on $T_{x_k}\mathcal M$ with $\ell_{x_k}(0)\ge\ell_{x_k}(\eta^*_{x_k})$, and set $x_{k+1}=R_{x_k}(\eta^*_{x_k})$.

The assumptions involve the sublevel set $\Omega_{x_0}=\{x\mid F(x)\le F(x_0)\}$ and two notions defined with respect to $R$ on a set $\mathcal N$:

• $L$-retraction-smoothness: $h(R_x(\eta))\le h(x)+\langle\operatorname{grad} h(x),\eta\rangle_x+\frac L2\|\eta\|_x^2$;
• retraction-convexity: $q_x=h\circ R_x$ satisfies $q_x(\eta)\ge q_x(\xi)+\langle\zeta,\eta-\xi\rangle_x$, where $\zeta$ is the gradient of $q_x$ at $\xi$, or any Riemannian subgradient of $q_x$ at $\xi$ when $h$ is nonsmooth.

Assumption 3.1 asks that $F$ be bounded below and $\Omega_{x_0}$ compact. Assumption 3.3 provides an open $\Omega\supseteq\Omega_{x_0}$ on which $f$ is $L$-retraction-smooth and retraction-convex and $g$ is retraction-convex. Assumption 3.4 bounds how far the retraction is from Euclidean: for all $x,y,z\in\Omega$,

$$\bigl|\|R_x^{-1}(z)-R_x^{-1}(y)\|_x^2-\|R_y^{-1}(z)\|_y^2\bigr|\le\kappa_\Omega\|R_x^{-1}(y)\|_x^2 .$$

Finally, $\beta=(\tilde L-L)/2$.

Formalization targets

Goal: Theorem 3.2

Let $\tilde L>\max(L,0)$, suppose Assumptions 3.1, 3.3 and 3.4 hold, and let $x_*$ be any accumulation point of $\{x_k\}$. Then for every $k\ge1$

$$F(x_k)-F(x_*)\le\frac1k\left(\frac{\tilde L}{2}\|R_{x_0}^{-1}(x_*)\|_{x_0}^2+\frac{\tilde L\kappa_\Omega}{2\beta}\bigl(F(x_0)-F(x_*)\bigr)\right).\tag{3.16}$$

The constants are those of the paper.

Milestones

1. Lemma 3.1 (descent): $F(x_k)-F(x_{k+1})\ge\beta\|\eta^*_{x_k}\|_{x_k}^2$.
2. Lemma 3.4 (Riemannian three-point inequality): for one step $z=R_x(\eta^*_x)$ and any $y=R_x(\xi_x)\in\Omega$, $F(z)\le F(y)+\frac{\tilde L}{2}(\|\xi_x\|_x^2-\|\xi_x-\eta^*_x\|_x^2)$.
3. (3.17): the one-step estimate obtained from Lemma 3.4 with $y=x_*$ and from Assumption 3.4.
4. (3.18): the one-step estimate with $\|\eta^*_{x_k}\|^2$ replaced by the decrease of $F$.
5. (3.19): the averaged estimate over the first $k$ steps.

Significance

Theorem 3.2 extends the $O(1/k)$ function-value rate of the proximal gradient method to manifolds and general retractions. The constant is explicit: it combines the initial distance $\|R_{x_0}^{-1}(x_*)\|$ with a correction proportional to $\kappa_\Omega$, which measures how far the retraction is from Euclidean. In the Euclidean case $R_x(\eta)=x+\eta$ one can take $\kappa_\Omega=0$, and the bound reduces to the classical one. The rate concerns $F(x_k)-F(x_*)$, which the iteration bound of Theorem 3.1 (the norm of $\eta^*_{x_k}$) does not control.

The result is proved in the paper. None of it is formalized, and no machine-checked version of the Euclidean proximal-gradient rate is on the platform either. A formalization would supply the first checked version of Clarke stationarity on tangent spaces, of the retraction-based convexity and smoothness notions, and of a rate proof for a nonsmooth Riemannian algorithm. These pieces carry over to other retraction-based methods, such as the accelerated variants of §4 of the paper.

Difficulty

The arithmetic of the rate proof is a telescoping sum, so the work lies elsewhere. First, Lemma 3.4 needs a usable form of the stationarity condition $0\in\partial\ell_x(\eta^*_x)$: a subgradient of $g\circ R_x$ at $\eta^*_x$ equal to $-(\operatorname{grad} f(x)+\tilde L\eta^*_x)$. This requires a sum rule for the Clarke subdifferential of a $C^1$ function plus a locally Lipschitz one, on a tangent space whose norm comes from the Riemannian metric rather than from the model space. Second, the gradient of $f\circ R_x$ at $0_x$ has to be identified with $\operatorname{grad} f(x)$ through $\mathrm DR_x(0_x)=\mathrm{id}$. In Mathlib this mixes manifold derivatives (mfderiv) with Fréchet derivatives on a space carrying two equivalent norms. Third, it has to be shown that the iterates and the accumulation point remain in $\Omega$, so that Assumptions 3.3 and 3.4 apply at every step.

Formalization scope

Theorem numbers and pages are those of arXiv:1909.06065v4. $\mathcal M$ is a smooth manifold modelled on a finite-dimensional real inner-product space $E$, with Mathlib's RiemannianBundle on the tangent bundle. All norms and inner products on $T_x\mathcal M$ are the Riemannian ones. Retractions and gradients are the published RiemOpt.BFGS.IsRetraction and RiemOpt.FR.IsGradient. The Clarke derivative is an EReal-valued limit superior along $\mathcal N(\eta)\times\mathcal N_{>0}(0)$. Algorithm 1 is modelled as a run (sequences $x_k$, $\eta^*_{x_k}$ with the three defining properties), and every statement holds for every run. Indices start at $0$, accumulation points are cluster points of the sequence, and the bounds divided by $k$ are stated for $k\ge1$.

The formalization commits to the following readings:

1. $L$-retraction-smoothness is required for every tangent vector at the points of the set. This is a strengthening of Definition 3.1, which only covers $\eta$ with $R_x(\eta)$ in the set, and it is needed because Lemma 3.1 fails under the literal reading.
2. In retraction-convexity the vector $\zeta$ depends on $\xi$. It is the gradient of $f\circ R_x$, respectively any Clarke subgradient of $g\circ R_x$, as the sentence after (3.10) states.
3. $\kappa_\Omega$ is a single constant.
4. $R^{-1}$ is data with $R_x(R_x^{-1}(y))=y$ on $\Omega$, together with the identification $R_{x_k}^{-1}(x_{k+1})=\eta^*_{x_k}$ that the proof uses.
5. Local Lipschitz continuity of $g\circ R_x$ is assumed, as p. 5 presupposes when it defines the subdifferential.

A single $\zeta$ for all $\eta,\xi$ in (3.10) would make retraction-convexity force $q_x$ to be affine, and the theorem would only cover affine problems. That reading is excluded. Statements with the case $k=0$, where Lean's $1/0=0$ makes (3.16) false, are excluded as well.

Contributions welcome: a Clarke sum rule for $C^1$ plus locally Lipschitz functions, the identification of the Fréchet derivative of $f\circ R_x$ at $0$ with the Riemannian gradient, and the five milestones in order. The Clarke layer and the derivative identification are reusable beyond this mission.

Selected references

• W. Huang, K. Wei, Riemannian proximal gradient methods, Mathematical Programming, 2021; extended version arXiv:1909.06065v4. https://arxiv.org/abs/1909.06065v4, https://doi.org/10.1007/s10107-021-01632-3
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sciences, 2009. https://doi.org/10.1137/080716542
• S. Chen, S. Ma, A. M.-C. So, T. Zhang, Proximal gradient method for nonsmooth optimization over the Stiefel manifold, SIAM J. Optimization, 2020. https://doi.org/10.1137/18M122457X
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244