Optimization

Motivation

Retailers of seasonal goods (fashion, electronics, holiday items) sell a fixed stock over a short season and routinely cut prices toward its end. A markdown of this kind segments the market over time: customers with high valuations buy early at a premium price, and customers with lower valuations are served later at a discount price. Aviv and Pazgal (MSOM 2008) study how much such two-price schemes are worth when customers arrive over time, differ in their valuations, and may or may not anticipate the discount.

To measure the value of price segmentation, the paper compares every two-price scheme with the best fixed-price policy, a single price held for the whole season. Its benchmark is the case of myopic customers, who never delay a purchase strategically. Proposition 3 of the paper computes this benchmark in closed form in the simplest nontrivial setting: exponentially distributed valuations that do not decline over the season, and unlimited inventory. The resulting formula explains the pattern of the paper's Table 1, where the benefit of segmentation grows with the heterogeneity of valuations and with a late discount time.

Setting

A seller offers a product during the season $[0, H]$; throughout this mission $H = 1$, so time is measured as a fraction of the season. Customers arrive as a Poisson process with rate $\lambda > 0$. Customer $j$ has a base valuation $V_j$ drawn independently from a distribution $F$ with tail $\bar F(x) = 1 - F(x)$, and values the product at $V_j e^{-\alpha t}$ at time $t$, where $\alpha \ge 0$ is the decline factor. The paper reparametrizes it as $\rho = e^{-\alpha H}$, the fraction of the base valuation left at the end of the season.

In the numerical study, $F$ is a Gamma law with mean $\mu$ and coefficient of variation $c$ (standard deviation over mean): shape $1/c^2$ and rate $1/(\mu c^2)$. The paper sets $\mu = 1$. For $c = 1$ this is the exponential law with mean one, $\bar F(x) = e^{-x}$ for $x \ge 0$.

A contingent two-price policy posts the premium price $p_1$ on $[0, T)$, where $0 < T \le 1$ is fixed, and a discount price $p_2 \le p_1$ from time $T$ on. A myopic customer arriving at $t < T$ buys at $p_1$ if his valuation is at least $p_1$; otherwise he waits and buys at $T$ if his valuation is then at least $p_2$. Customers arriving at or after $T$ buy if their valuation is at least $p_2$. The numbers of customers in these groups are Poisson with means

$$\Lambda_I(p_1) = \lambda\int_0^T \bar F(p_1 e^{\alpha t})\,dt, \quad \Lambda_W(p_1,p_2) = \lambda\int_0^T \big[\bar F(\min\{p_1e^{\alpha t}, p_2e^{\alpha T}\}) - \bar F(p_1e^{\alpha t})\big]dt, \quad \Lambda_L(p_2) = \lambda\int_T^H \bar F(p_2e^{\alpha t})\,dt .$$

With unlimited inventory, the expected revenue of the policy is

$$R_{C/N}(p_1, p_2) = p_1\Lambda_I(p_1) + p_2\big(\Lambda_W(p_1,p_2) + \Lambda_L(p_2)\big),$$

and the expected revenue of a single price $p$ is $R_F(p) = p\,\lambda\int_0^H \bar F(p e^{\alpha t})\,dt$ (Eq. (9) of the paper). The optimal values are $\pi^*_{C/N} = \max_{p_2 \le p_1} R_{C/N}(p_1,p_2)$ and $\pi^*_F = \max_p R_F(p)$.

Formalization targets

Goal: Proposition 3

Suppose $c = 1$, $\rho = 1$ and $Q/\lambda \to \infty$ (unlimited inventory), with $\mu = 1$ and $H = 1$. Then

$$\pi^*_{C/N} = (\lambda e^{-1})\cdot e^{T/e} = \pi^*_F \cdot e^{T/e}.$$

Both maxima are attained. The goal states the two optimal values; it does not fix the optimal prices.

Milestones from the paper's proof

1. The reduced problem: for $0 \le p_2 \le p_1$, $R_{C/N}(p_1,p_2) = p_2\cdot\lambda e^{-p_2} + (p_1-p_2)\cdot\lambda T e^{-p_1}$.
2. Its solution: over $p_2 \le p_1$ the maximum is $\lambda e^{-1+T/e}$, attained exactly at $p_1^* = 2 - T/e \ge 1$, $p_2^* = p_1^* - 1 \le 1$.
3. The fixed-price optimum (a supporting item of the goal, stated in the proof on pp. 358–359): $p^* = \mu = 1$ is the unique optimal single price and $\pi^*_F = \lambda e^{-1}$.

Significance

Proposition 3 gives the relative benefit of contingent pricing over a single price, $e^{T/e} - 1$, as a function of the discount time alone. It increases in $T$ and is largest at $T = 1$, where it equals $e^{1/e} - 1 \approx 44.46\%$. This is the paper's analytic anchor for its numerical findings: segmentation is most valuable when valuations are heterogeneous and customers are carried to the discount at little cost, and a late discount exposes more customers to the premium price. Under strategic customers the same quantity serves as an upper bound on the benefit of segmentation (§6.1 of the paper).

The result is proved in the paper, in a short appendix argument that states the reduced problem and its solution without the calculus. No machine-checked version exists. Formalizing it produces a reusable Lean encoding of the paper's segment rates $\Lambda_I, \Lambda_W, \Lambda_L$ as integrals of a valuation tail, a Gamma valuation law through Mathlib's gammaMeasure, and a complete verification that the integral model reduces to the two-variable problem and that the stated prices are its unique maximizer.

Difficulty

The obvious route is to write the revenue in closed form and set the gradient to zero. Two steps of that route are not automatic. First, the reduction requires evaluating the three integrals with the piecewise tail of the exponential law, including the $\min$ inside $\Lambda_W$, and the reduced formula is valid only for nonnegative prices; negative prices must be handled separately in the model itself, where the tail equals one. Second, the reduced objective $p_2\lambda e^{-p_2} + (p_1-p_2)\lambda T e^{-p_1}$ is not concave on the region $p_2 \le p_1$, so a stationary point is not automatically a global maximizer, and the boundary $p_2 = p_1$ and unbounded directions have to be ruled out. Uniqueness of the maximizer, which the paper asserts, fails at $T = 0$ and needs $T > 0$.

Formalization scope

All declarations sit in the namespace SeasonalPricing.MyopicExp. Time, prices and rates are real numbers. The season is $[0, 1]$ with $0 < T \le 1$ and $\lambda > 0$. Integrals are interval integrals. The valuation tail is gammaValuationTail μ c x = 1 - cdf (gammaMeasure (1/c^2) (1/(μ c^2))) x, used at $\mu = c = 1$. The hypothesis $\rho = 1$ is decayRatio α 1 = 1 with $\alpha \ge 0$.

Readings of the paper's informal words:

• "$Q/\lambda \to \infty$" is read as unlimited inventory: the truncated Poisson mean $N(q,\Lambda)$ of §4.2 is replaced by $\Lambda$ and stock-outs never occur. This is what the proof computes, what p. 348 writes as $Q = \infty$, and what §7.1 calls inventory that is "practically unlimited". A limit of finite-inventory optimal revenues is not stated.
• "max" is an attained maximum (IsGreatest), not a supremum.
• The optimum is taken over all real prices with $p_2 \le p_1$, as printed; the paper never restricts signs, and negative prices are never optimal in the model.
• The seller's discount at $T$ is a best response to $p_1$ in the paper ($R(q \mid p_1)$, p. 349). With unlimited inventory it does not depend on the realized sales, and the nested maximum equals the joint maximum over $(p_1, p_2)$, which is what the goal states.
• "The solution … is" (milestone 2) and "the optimal single price is given by $p^* = \mu = 1$" (the fixed-price item) are read as unique maximizers.

The Gamma density printed on p. 349 has the exponent $1/(sc^2-1)$, a misprint for $1/c^2 - 1$; at $c = 1$ the exponent is $0$ either way.

A trivializing formalization would state the goal on the reduced two-variable function, dropping the model: the goal here is about $R_{C/N}$ built from $\Lambda_I, \Lambda_W, \Lambda_L$ and the Gamma tail, and about $R_F$ built from Eq. (9). The platform's BuyingToBundle.monopolyRevenue (definition monopoly_pricing) is a related object, $\sup_p p\,\nu([p,\infty))$; with $\rho = 1$ and $H = 1$, $\pi^*_F$ equals $\lambda$ times it for the exponential law, but it is a supremum without arrivals or time and is not reused.

Contributions welcome: closed forms of the segment rates for the exponential tail, a general lemma that negative prices are dominated, and the two-variable maximization.

Selected references

• Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• D. Besanko and W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999

Motivation

Retailers of fashion and seasonal goods sell at a premium price early in the season and mark the remaining stock down later. When customers anticipate the markdown, some of them who would buy at the premium price instead wait, trading a lower price against the risk that the item sells out and against the decline of their own valuation over the season. How forward-looking ("strategic") customers respond to a markdown policy is the first question any model of such pricing has to answer, because the seller's optimal prices depend on it.

Aviv and Pazgal (MSOM 2008) model a seller with a fixed inventory, Poisson arrivals of customers with heterogeneous, exponentially declining valuations, and two pricing regimes: contingent pricing, where the discount depends on the inventory left at the markdown time, and announced fixed discounts. The first step of their analysis of contingent pricing is Theorem 1: whatever the other customers do, a customer's best response is a threshold rule on his current valuation, with a threshold that rises as the markdown approaches. Their numerical study of equilibria and of the value of price commitment (§§4.2–7) is built on this reduction.

Setting

A seller holds $Q$ units over a season $[0, H]$ split at a fixed time $T$ with $0 < T \le H$. On $[0, T)$ the premium price $p_1$ applies. At time $T$ the seller observes the remaining inventory $Q_T \in \{0, 1, \dots, Q\}$ and charges the discount menu price $p_2(Q_T)$, where $p_2(q) \le p_1$ for $q = 1, \dots, Q$. Customer $j$ has a base valuation $V_j$ and valuation $V_j(t) = V_j e^{-\alpha t}$ at time $t$, with a common decline factor $\alpha \ge 0$.

A customer arriving at $t < T$ either buys immediately at $p_1$ or waits until $T$, when he requests a unit if the discounted price leaves him a nonnegative surplus. Waiting is uncertain in two ways: the remaining inventory $Q_T$ is random, and when fewer units remain than customers request them, units are rationed at random. A belief is a probability mass function $\pi$ of $Q_T$ on $\{0, \dots, Q\}$ together with allocation probabilities $a(q) = \Pr\{\mathcal A \mid Q_T = q\} \in [0,1]$, $a(0) = 0$, where $\mathcal A$ is the event that the customer is allocated a unit. It is determined by the other customers' strategies, which are arbitrary.

With $\delta = e^{-\alpha(T-t)}$, the expected surplus of waiting of a customer with current valuation $\psi$ is

$$W_t(\psi) = \mathrm E_{Q_T}\!\left[\max\{\psi\delta - p_2(Q_T), 0\}\cdot \mathbf 1\{\mathcal A \mid Q_T\}\right] = \sum_{q=0}^{Q}\pi(q)\,a(q)\,\max\{\psi\delta - p_2(q), 0\}.$$

The paper's purchase rule (p. 344): buy immediately iff the current surplus $V(t) - p_1$ is nonnegative and at least $W_t(V(t))$.

Formalization targets

Goal: Theorem 1 and Corollary 1

Assume $p_1 \ge 0$, and $\alpha > 0$ or $\sum_q \pi(q)a(q) < 1$. For every $t \in [0,T)$ the equation

$$\psi - p_1 = W_t(\psi) \tag{2}$$

has a unique solution $\psi(t) \ge p_1$; a customer arriving at $t$ buys immediately under the purchase rule if and only if $V(t) \ge \psi(t)$; and the threshold function $\psi : [0, T) \to [p_1, \infty)$ is nondecreasing in $t$.

Milestones

1. The right-hand side of (2) is nonnegative and nondecreasing in $\psi$, with increments bracketed by $\delta\,\Pr\{\psi\delta \ge p_2(Q_T), \mathcal A\}$ at the two endpoints, and this slope is below one.
2. Equation (2) has a unique solution $\psi \ge p_1$.

Significance

Theorem 1 reduces a customer's strategy, a function of arrival time and valuation, to one threshold function $\psi$ on $[0, T)$. The segment sizes $\Lambda_I, \Lambda_S, \Lambda_W, \Lambda_L$ of §4.2, the seller's menu problem (3), the equilibrium iteration (4) and the closed form of Proposition 2 are all written in terms of $\psi$; without Theorem 1 none of them is defined. Corollary 1, that the threshold rises toward the markdown, is what the paper calls "useful in our analyses below"; the customer segments of Figure 1 are drawn with it.

The result is proved in the paper, with a short appendix argument. No machine-checked version exists. The mission produces a formal statement and proof of the reduction for an arbitrary belief, which fixes the exact hypotheses under which it holds: the paper's slope bound needs either valuation decline ($\alpha > 0$) or imperfect availability, and the monotonicity of the threshold needs a nonnegative premium price. A formal $W_t$ and threshold are the starting point for formalizing the equilibrium and pricing results of the paper.

Difficulty

The mathematics is one-dimensional. The difficulty is in stating it exactly. $W_t$ is piecewise linear with a kink wherever $\psi\delta$ crosses a menu price, so the paper's derivative is only a one-sided derivative, and the uniqueness argument has to use increments. The paper's bound "slope $< 1$" is false when $\alpha = 0$ and a unit is allocated with certainty; then (2) has either no finite solution or a half-line of them. The threshold's monotonicity in $t$ rests on $W_t(\psi)$ increasing in $t$ for fixed $\psi$, which needs $\psi \ge 0$; with a negative premium price the threshold can decrease. The naive reading of "optimal to use a threshold" as an abstract fixed-point fact about any monotone function with slope below one discards the model and is not the goal.

Formalization scope

Lean namespace SeasonalPricing.Contingent. Time, prices and valuations are real numbers. The belief is a pair pmf alloc : ℕ → ℝ restricted to {0, …, Q} (IsInventoryBelief), not a random variable on a probability space; only the law of $(Q_T, \mathbf 1\{\mathcal A\})$ enters (2). The menu is p2 : ℕ → ℝ with $p_2(q) \le p_1$ required on $\{1, \dots, Q\}$ only; $p_2(0)$ never matters because $a(0) = 0$. The belief does not depend on the arrival time, as in Eq. (4) of the paper. waitingSurplus is $W_t$ with $e^{-\alpha(T-t)}$ written Real.exp (-(α * (T - t))); buysNow is the purchase rule, stated on the current valuation $V(t)$.

Readings of the paper's words:

• "the unique solution" of (2): existence and uniqueness of a real $\psi \ge p_1$ (∃!). The paper's "$\psi \in [p_1, \infty]$" includes $\infty$ only in the case excluded by the added hypothesis.
• "it is optimal to base purchasing decisions on a threshold function": the purchase rule of p. 344 holds exactly when $V(t) \ge \psi(t)$.
• "derivative … $< 1$": a two-sided bracket on increments of $W_t$, with right slope $\delta\Pr\{\psi\delta \ge p_2(Q_T), \mathcal A\}$, below one.
• "increasing" (Corollary 1): nondecreasing (MonotoneOn), since $\psi$ is constant on an initial interval whenever no menu price is reachable (p. 347).

Added hypotheses, both named in the statements: $\alpha > 0$ or $\sum_q \pi(q)a(q) < 1$, the one hypothesis the paper's proof uses without stating it; and $p_1 \ge 0$, the model's convention that prices are nonnegative. Only the branch $0 \le t < T$ of the threshold $\theta$ is stated: for $t \ge T$ the paper's $\theta(t) = p_2$ is the model's rule for late customers. The belief enters through the explicit sum; a formalization with an unspecified monotone $W$, or with $\psi(t)$ defined by choice inside a definition, is not the target.

No new library is needed beyond finite sums, max and Real.exp. A lemma on unique roots of $\psi \mapsto \psi - c - f(\psi)$ for $f$ with increments bounded by $k(\psi' - \psi)$, $k < 1$, is reusable. Proofs of the milestones and the goal, in any order, are welcome.

Selected references

• Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• X. Su, Intertemporal Pricing with Strategic Customer Behavior, Management Science 53(5):726–741, 2007. https://doi.org/10.1287/mnsc.1060.0667
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999

Motivation

In the contextual bandit problem a learner repeatedly observes a context, picks one of $K$ actions, and sees the reward of that action only. Against a finite class $\Pi$ of policies, statistically optimal regret of order $\sqrt{KT\ln|\Pi|}$ has been known since EXP4 (Auer et al., 2002), but EXP4 maintains a weight per policy and costs $\Omega(|\Pi|)$ time per round. For the large policy classes used in practice (linear classifiers, trees), that is prohibitive.

The oracle-efficient line of work accesses $\Pi$ only through a cost-sensitive classification oracle (an arg max oracle, AMO). The RandomizedUCB algorithm of Dudík et al. (2011) obtains optimal regret with polynomially many oracle calls by solving a convex program in each round, but the number of calls is large. Agarwal, Hsu, Kale, Langford, Li and Schapire (2014) replace that solver by a coordinate descent method whose number of iterations, and hence of oracle calls, is bounded independently of $|\Pi|$. Their algorithm, ILOVETOCONBANDITS, and its practical variant are now standard references for oracle-based exploration.

This mission formalizes the optimization half of that paper: Algorithm 2 solves the per-epoch problem (OP) after at most $4\ln(1/(K\mu))/\mu$ coordinate steps.

Setting

Let $A=\{0,\dots,K-1\}$ be the actions, $X$ any set of contexts, and $\Pi\subseteq A^X$ a finite nonempty set of policies. A history $H_t$ is a sequence of $t\ge1$ records $(x_i,a_i,r_i(a_i),p_i(a_i))$ with $r_i(a_i)\in[0,1]$ the observed reward and $p_i(a_i)\in(0,1]$ the probability with which $a_i$ was chosen. Write $\widehat{\mathbb E}_{x\sim H_t}[f(x)]=\frac1t\sum_i f(x_i)$.

The inverse propensity scoring estimate (Eq. (1)) is

$$\widehat{\mathcal R}_t(\pi)=\frac1t\sum_{i=1}^t\frac{r_i(a_i)\,\mathbb 1\{\pi(x_i)=a_i\}}{p_i(a_i)},$$

the estimated regret is $\widehat{\mathrm{Reg}}_t(\pi)=\max_{\pi'\in\Pi}\widehat{\mathcal R}_t(\pi')-\widehat{\mathcal R}_t(\pi)$, and for a minimum probability $\mu$ one sets $b_\pi=\widehat{\mathrm{Reg}}_t(\pi)/(\psi\mu)$ with $\psi=100$.

Weights are vectors $Q\in\mathbb R^\Pi$; $\Delta^\Pi$ is the set of nonnegative $Q$ with $\sum_\pi Q(\pi)\le1$. The smoothed projection of $Q$ is

$$Q^\mu(a\mid x)=(1-K\mu)\sum_{\pi:\ \pi(x)=a}Q(\pi)+\mu .$$

The optimization problem (OP) asks for $Q\in\Delta^\Pi$ with

$$\sum_{\pi\in\Pi}Q(\pi)b_\pi\le2K\quad(2),\qquad \widehat{\mathbb E}_{x\sim H_t}\Bigl[\frac1{Q^\mu(\pi(x)\mid x)}\Bigr]\le2K+b_\pi\ \ \forall\pi\in\Pi\quad(3).$$

Algorithm 2 starts from $Q_{\mathrm{init}}$ and loops. With $V_\pi(Q)=\widehat{\mathbb E}[1/Q^\mu(\pi(x)\mid x)]$, $S_\pi(Q)=\widehat{\mathbb E}[1/Q^\mu(\pi(x)\mid x)^2]$ and $D_\pi(Q)=V_\pi(Q)-(2K+b_\pi)$: if $\sum_\pi Q(\pi)(2K+b_\pi)>2K$ it rescales $Q$ by $c=2K/\sum_\pi Q(\pi)(2K+b_\pi)$ (Eq. (4)); then, if some $\pi$ has $D_\pi(Q)>0$, it adds

$$\alpha_\pi(Q)=\frac{V_\pi(Q)+D_\pi(Q)}{2(1-K\mu)S_\pi(Q)}$$

to $Q(\pi)$ (Step 8) and repeats; otherwise it halts and outputs $Q$.

The analysis uses the potential (Eq. (6)), with $\tau=t$ and $\mathcal U_A$ uniform on $A$,

$$\Phi_m(Q)=\tau\mu\left(\frac{\widehat{\mathbb E}_x[\mathrm{RE}(\mathcal U_A\,\|\,Q^\mu(\cdot\mid x))]}{1-K\mu}+\frac{\sum_\pi Q(\pi)b_\pi}{2K}\right),\qquad \mathrm{RE}(p\|q)=\sum_a\bigl(p_a\ln\tfrac{p_a}{q_a}+q_a-p_a\bigr).$$

Formalization targets

Goal: Theorem 3 (p. 6)

For $0<\mu\le1/(2K)$, Algorithm 2 with $Q_{\mathrm{init}}=\mathbf 0$ satisfies: every run executes Step 8 at most

$$\frac{4\ln(1/(K\mu))}{\mu}$$

times, whatever policy each Step 8 chooses among those with $D_\pi>0$; and when it halts, its output solves (OP). The bound depends on $K\mu$ only, not on $|\Pi|$ or $t$.

Milestones

1. Lemma 5 (p. 10). If Algorithm 2 halts and outputs $Q$, then $Q$ satisfies (2), (3) and $\sum_\pi Q(\pi)\le1$.
2. Lemma 6 (p. 10). If $\sum_\pi Q(\pi)(2K+b_\pi)>2K$ and $c$ is as in Eq. (4), then $\Phi_m(cQ)\le\Phi_m(Q)$.
3. Lemma 7 (p. 10). If $D_\pi(Q)>0$ and $Q'$ adds $\alpha_\pi(Q)$ to $Q(\pi)$, then

$$\Phi_m(Q)-\Phi_m(Q')\ge\frac{\tau\mu^2}{4(1-K\mu)}.$$

Significance

The result. Theorem 3 is what makes ILOVETOCONBANDITS computationally efficient: each call of Algorithm 2 is implemented with one AMO call per iteration (Lemma 1 of the paper), so the oracle complexity of an epoch is $O(\ln(1/(K\mu))/\mu)$. Combined with the epoch schedule and warm start, this gives the paper's total of $\tilde O(\sqrt{KT/\ln(|\Pi|/\delta)})$ oracle calls over $T$ rounds. Theorem 3 also gives a constructive proof that (OP) is feasible for every history, which the regret analysis (a separate mission in this series) assumes.

Formalizing it. The result is proved in the paper, with complete proofs of Lemmas 5–7 in Appendix D. No machine-checked version is known. The formalization would give a checked termination bound for a coordinate descent method on a non-smooth feasibility problem, with a fully explicit constant, and a verified definition of the unnormalized relative entropy potential that is reusable for other smoothed-projection analyses (e.g. RandomizedUCB-type convex programs).

Difficulty

Termination cannot be read off the constraints. Step 8 raises one weight and can push the total weight above 1, after which Step 5 shrinks every coordinate, so no constraint and no single weight moves monotonically along a run. The number of policies that violate (3) can also go up after a step. Bounding the number of iterations therefore needs a global quantity that tracks progress through both kinds of step. The rescaling step is the harder of the two: it lowers every $Q^\mu(a\mid x)$ at once, which pushes the relative-entropy term the wrong way, and it must be offset by the drop in the regret term. Knowing that (OP) is feasible, or that some convex function has a minimizer, bounds nothing about how many steps a particular method takes; that is the obvious approach, and it gives no count.

Formalization scope

• Actions are Fin K with $K\ge1$; contexts form an arbitrary type (no measure is needed: Theorem 3 is deterministic). $\Pi$ is a nonempty Finset (X → Fin K); weights are real functions on its subtype.
• Histories are indexed by Fin t with $t\ge1$ (0-based indices). The paper allows $p_i(a_i)\in[0,1]$; the formalization requires $p_i(a_i)\in(0,1]$, since Eq. (1) divides by it.
• $\widehat{\mathrm{Reg}}_t(\pi)$ is written as $\max_{\pi'}\widehat{\mathcal R}_t(\pi')-\widehat{\mathcal R}_t(\pi)$, which equals $\widehat{\mathcal R}_t(\pi_t)-\widehat{\mathcal R}_t(\pi)$ for any maximizer $\pi_t$; $\psi=100$ is hard-wired in $b_\pi$.
• $Q^\mu$, $V_\pi$, $S_\pi$, (OP) and $\Phi_m$ all use the smoothed projection of the unnormalized weights; there is no default policy in this mission.
• $\mu$ ranges over $(0,1/(2K)]$, the range of $\mu_m$ in Algorithm 1 that the printed theorem refers to. $\tau$ in $\Phi_m$ is the history length $t$.
• Algorithm 2 is encoded relationally. A run of length $n$ from $Q_{\mathrm{init}}$ is a sequence $Q^{(0)}=Q_{\mathrm{init}},\dots,Q^{(n)}$ in which each $Q^{(k+1)}$ is Step 8, for some policy with $D_\pi>0$, applied to the rescaled $Q^{(k)}$. It halts at $Q^{(n)}$ when no policy has $D_\pi>0$ after rescaling, and it then outputs the rescaled $Q^{(n)}$. "Iterations" means executions of Step 8. The last pass, which halts at Step 10, is not counted: the paper's proof bounds "the number of times Step 8 is executed". The bound is compared in $\mathbb R$, without rounding.
• Lemmas 5–7 are stated for nonnegative weight vectors without a bound on their sum, because Algorithm 2 rescales vectors whose sum may exceed 1. Lemma 7's "$\alpha=\alpha_\pi(Q)>0$" is part of its conclusion.
• A trivializing formalization is ruled out: the goal quantifies over every run from $\mathbf 0$ and every choice in Step 8, not over some run, and the potential, $b_\pi$ and $D_\pi$ are computed from the history rather than taken as free parameters.
• The auxiliary facts $\Phi_m\ge0$ and $\Phi_m(\mathbf 0)\le\tau\mu\ln(1/(K\mu))/(1-K\mu)$ are inline claims in the paper and are not stated separately; contributions stating and proving them are welcome, as are general lemmas on the unnormalized relative entropy.
• Out of scope: the regret bound (Theorem 2) and the probabilistic model (mission I of this series), the AMO implementation (Lemma 1), warm start and epoch-level oracle counts (Lemmas 2, 3, 8), and the support lower bound (Theorem 4).

Selected references

• A. Agarwal, D. Hsu, S. Kale, J. Langford, L. Li, R. E. Schapire, Taming the Monster: A Fast and Simple Algorithm for Contextual Bandits, ICML 2014; arXiv:1402.0555v2. https://arxiv.org/abs/1402.0555
• M. Dudík, D. Hsu, S. Kale, N. Karampatziakis, J. Langford, L. Reyzin, T. Zhang, Efficient Optimal Learning for Contextual Bandits, UAI 2011. https://arxiv.org/abs/1106.2369
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM J. Comput. 32(1), 2002. https://doi.org/10.1137/S0097539701398375

Motivation

A polyhedral cone can be described in two ways: as the set of nonnegative combinations of finitely many vectors (a finitely generated cone), or as the intersection of finitely many closed half-spaces through the origin. That the two descriptions give the same class of sets is the Minkowski–Weyl theorem. It is the structural basis of linear programming: the simplex method, LP duality, Farkas' lemma, and the vertex/facet description of polytopes used throughout combinatorial optimization all rest on it.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv. 7, 290–306) gives an elementary, self-contained proof of both directions. Its first result, which Weyl calls the Hauptsatz (main theorem, Satz 1), is the direction "finitely generated ⇒ finite intersection of half-spaces", in a sharp form: the half-spaces needed are exactly the extreme supports of the generating set, i.e. its facets. Its sharpening, Satz 2, bounds the number of generators needed to represent a point by the dimension $n$. This mission formalizes §§1–2 of the paper (pp. 290–295): the Hauptsatz, its sharpening, and the steps of Weyl's inductive proof.

Timeline:

• 1896, H. Minkowski, Geometrie der Zahlen: polytopes as bounded intersections of half-spaces and as convex hulls of finitely many points.
• 1911, C. Carathéodory: a point in the convex hull of a set in $\mathbb{R}^d$ is a convex combination of at most $d+1$ of its points (Rend. Circ. Mat. Palermo 32).
• 1935, H. Weyl: the present paper; Satz 1 and Satz 2 for cones, with the dual statements in §3 and the polytope theorem in §4.

Setting

Points of $\mathbb{R}^n$ are $n$-tuples $x = (x_1, \ldots, x_n)$, and $\langle \alpha, x \rangle = \alpha_1 x_1 + \cdots + \alpha_n x_n$. A vector $\alpha \ne 0$ determines the half-space $\{x : \langle\alpha,x\rangle \ge 0\}$; positive multiples of $\alpha$ give the same half-space.

A point system $S$ is a finite set of points of $\mathbb{R}^n$. It is non-degenerate if its points do not all satisfy one equation $\langle\alpha,x\rangle = 0$ with $\alpha \neq 0$, i.e. the only $\alpha$ orthogonal to every point of $S$ is $0$.

A half-space $\langle\alpha,x\rangle\ge 0$ ($\alpha\ne 0$) is a support of $S$ if every point of $S$ lies in it. It is an extreme support if, in addition, equality $\langle\alpha,x\rangle = 0$ holds at $n-1$ linearly independent points $x$ of $S$.

A point $x$ is representable by $S$ if it is a nonnegative combination of the points of $S$:

$$x = \sum_{s\in S} c_s\, s, \qquad c_s \ge 0 .$$

The set of points lying in all extreme supports of $S$ is Weyl's konvexe Pyramide. In the Lean development these objects are Representable, NonDegenerate, IsSupport and IsExtremeSupport in the namespace WeylPolyhedra.Pyramid, with points of type Fin n → ℝ and $\langle\alpha,x\rangle$ written α ⬝ᵥ x.

Formalization targets

Goal: Satz 2 (Verschärfung des Hauptsatzes), p. 295

For a finite non-degenerate $S \subset \mathbb{R}^n$ and a point $x$ with $\langle\alpha,x\rangle\ge 0$ for every extreme support $\alpha$ of $S$,

$$\exists\, T \subseteq S,\quad |T| \le n,\quad x = \sum_{t\in T} c_t\, t,\ \ c_t \ge 0 .$$

Satz 1 (Hauptsatz), p. 291

Under the same hypotheses, $x$ is representable by $S$. Satz 2 contains Satz 1.

Steps of the proof (§1–§2)

1. A finite non-degenerate $S$ has only finitely many extreme supports, up to positive scaling (p. 291).
2. The reduction step of case a) (p. 292): if $S$ has an extreme support $\beta$ and $p$ satisfies all extreme supports, there are $e \in S$ with $\langle\beta,e\rangle>0$ and $\lambda\ge 0$ such that $q = p-\lambda e$ still satisfies all extreme supports and lies on the plane of one of them.
3. The lifting step (p. 293): with $x_n \ge 0$ an extreme support of $S$ and $S_0$ the points on $x_n = 0$, every extreme support $\beta$ of $S_0$ in $\mathbb{R}^{n-1}$ lifts to the extreme support $\beta_1x_1+\cdots+\beta_{n-1}x_{n-1} - \mu x_n \ge 0$ of $S$ (inequality (6)).
4. Case b) (p. 291, proved pp. 293–294): if $S$ has no extreme support, every point of $\mathbb{R}^n$ is representable by $S$.

Significance

Satz 1 together with its trivial converse identifies the cone generated by $S$ with the intersection of its extreme-support half-spaces. This is one half of the Minkowski–Weyl theorem for cones, and it names the half-spaces: they are the facets of the cone. Satz 2 adds the conic form of Carathéodory's theorem: every point of a cone generated by a finite spanning set in $\mathbb{R}^n$ is a nonnegative combination of at most $n$ generators. In linear programming this is the statement that a feasible system has a basic feasible solution. The second mission in this series, on §§3–4 of the paper, uses Satz 1 to prove that a bounded region cut out by finitely many inequalities is the convex hull of finitely many points, and conversely.

On formalization status: Mathlib defines finitely generated and dually finitely generated pointed cones (PointedCone, PointedCone.DualFG) and proves Carathéodory's theorem for convex hulls (convexHull_eq_union), but, at the pinned revision, it does not prove the Minkowski–Weyl theorem or the facet description of a finitely generated cone. The results are classical and proved in the paper; this mission produces machine-checked proofs of them, in Weyl's formulation with extreme supports, together with the intermediate steps of his induction.

Difficulty

The hypothesis only controls $x$ against the extreme supports, not against every support. Showing that $x$ lies in the cone generated by $S$ whenever $\langle\alpha,x\rangle\ge 0$ holds for every support is the conic Farkas lemma, which follows from a separating hyperplane argument. Here that argument is not enough: a separating hyperplane is a support, but in general not an extreme one, and the statement is about the finitely many extreme ones. The proof has to produce, for a point outside the cone, a violated extreme support, which requires control over the facet structure of the cone.

The dimension count of Satz 2 is a second difficulty. An induction on the dimension naturally gives $n$ generators in one case and $n+1$ in another (a point of a half-space needs one generator on each side), and Weyl notes that he could not avoid a detour to recover the bound $n$. The case where $S$ has no extreme support at all must also be handled separately; it is not vacuous, since $S$ can then generate all of $\mathbb{R}^n$.

Formalization scope

Conventions committed to in Lean:

• $\mathbb{R}^n$ is Fin n → ℝ; points and normals share this type (the dual space is identified with $\mathbb{R}^n$, as in the paper). The pairing is dotProduct, written α ⬝ᵥ x.
• A point system is a Finset (Fin n → ℝ). The zero vector is not excluded.
• A support normal satisfies α ≠ 0. Extreme supports require a subset T ⊆ S with T.card = n - 1 whose elements are linearly independent in the vector space $\mathbb{R}^n$.
• "All extreme support equations are satisfied" in Satz 1 is read as the inequalities $\langle\alpha,x\rangle\ge0$ for every extreme normal $\alpha$, as the proof and Satz 2 make explicit. The hypothesis quantifies over all extreme normals, so no representatives are chosen.
• "Positive-linear" combinations have nonnegative coefficients (display (3)). In Satz 2 the subset $T$ is not required to be linearly independent.
• Finiteness of extreme supports is stated up to positive scaling.
• The lifting step is stated in the coordinates Weyl fixes on p. 293: $\mathbb{R}^n$ is Fin (m+1) → ℝ, the extreme support is $x_n \ge 0$ (Fin.last m), $S_0$ is projected by Fin.init, and $\mu$ is given together with hypotheses that it is the attained minimum. The hypothesis $n \ge 2$ is made explicit.

Replacing extreme supports by all supports in the hypothesis of Satz 1 or Satz 2 would turn the goal into a much weaker theorem (the conic Farkas lemma plus Carathéodory) and is not an admissible formalization. Dropping non-degeneracy makes Satz 1 false: for $S = \{e_1\} \subset \mathbb{R}^2$ the extreme supports are $\pm x_2 \ge 0$, and $x = (-1, 0)$ satisfies both without being a nonnegative multiple of $e_1$.

A complete development needs basic linear algebra over Fin n → ℝ (hyperplanes through $n-1$ independent points, projection to a coordinate hyperplane) and finite minimisation. The facet description of finitely generated cones, conic Carathéodory and the finiteness of facets are reusable beyond this mission, including for the second mission of the series. Contributions of lemmas on PointedCone that connect Representable with PointedCone.span are welcome.

Selected references

• H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici 7 (1935), 290–306. https://doi.org/10.1007/BF01292722
• C. Carathéodory, Über den Variabilitätsbereich der Fourier'schen Konstanten von positiven harmonischen Funktionen, Rendiconti del Circolo Matematico di Palermo 32 (1911), 193–217. https://doi.org/10.1007/BF03014795
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (the Farkas–Minkowski–Weyl theorem). ISBN 978-0-471-98232-6
• G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995, Lecture 1. https://doi.org/10.1007/978-1-4613-8431-1

Motivation

The traveling salesman problem asks for a shortest closed route visiting every node of a weighted complete graph exactly once. It is NP-hard, so practitioners use fast heuristics, and the basic question about a heuristic is how far from optimal its tour can be. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the simple constructive heuristics under the triangle inequality: nearest neighbor, the family of insertion methods, and several variants.

Insertion methods build a tour by growing it one node at a time. They are among the most widely used construction heuristics in practice and in textbooks, and they differ only in the rule that chooses which node to insert next: the nearest one, the cheapest one, the farthest one, a random one, or any other. This mission formalizes the paper's result that holds for the whole family at once, regardless of that rule: every insertion method produces a tour at most $\lceil \lg n\rceil + 1$ times longer than an optimal one (Theorem 3, p. 571).

Timeline. 1977: Rosenkrantz, Stearns and Lewis prove $\lceil\lg n\rceil+1$ for every insertion method (Theorem 3), $\tfrac12(\lceil\lg n\rceil+1)$ for nearest neighbor (Theorem 1), both from a shared counting lemma (Lemma 1), and the constant $2$ for nearest and cheapest insertion (Theorem 4). 1994: Bafna, Kalyanasundaram and Pruhs (Theoretical Computer Science 125, 1994) give instances on which some insertion methods reach ratio $\Omega(\log n/\log\log n)$, so the logarithmic growth cannot be replaced by a constant for the family as a whole.

Setting

A traveling salesman graph with $n$ nodes consists of a finite node set $N$ with $|N|=n$ and a distance $d:N\times N\to\mathbb R$ with $d(i,j)=d(j,i)$, $d(i,j)\ge 0$ and $d(i,j)+d(j,k)\ge d(i,k)$ for all nodes (the triangle inequality). A tour visits every node once and returns to its start; its length is the sum of its edge lengths, and OPTIMAL is the least length of a tour.

A subtour is a tour on a subset of the nodes; a single node is a tour without edges. Given a subtour $T$ and a node $k\notin T$, TOUR$(T,k)$ is obtained by choosing an edge $(x,y)$ of $T$ minimizing

$$d(x,k)+d(k,y)-d(x,y)$$

and replacing it by the edges $(x,k)$ and $(k,y)$; if $T$ is a single node $i$, TOUR$(T,k)$ is the two-node tour $(i,k),(k,i)$. COST$(T,k)$ is the length of TOUR$(T,k)$ minus the length of $T$.

An insertion method constructs subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ a single node and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some node $a_i\notin T_i$, $1\le i<n$. The final tour $T_n$ is the approximation, and INSERT denotes its length. No rule for choosing the $a_i$ is fixed, and ties between minimizing edges are broken arbitrarily.

Write $\lg$ for the logarithm to base 2 and $\lceil x\rceil$ for the least integer $\ge x$.

Formalization targets

Goal: Theorem 3

For every traveling salesman graph with $n\ge 1$ nodes and every run of every insertion method,

$$\mathrm{INSERT}\ \le\ \bigl(\lceil\lg n\rceil+1\bigr)\cdot\mathrm{OPTIMAL}.$$

Milestones

1. (2.2), shortcutting: visiting a subset of the nodes in the order of a tour gives a tour of the subset that is no longer.
2. (2.1): if the numbers $l_1\ge\dots\ge l_n$ satisfy $d(p,q)\ge\min(l_p,l_q)$ for distinct $p,q$, then $\mathrm{OPTIMAL}\ge 2\sum_{i=k+1}^{\min(2k,n)} l_i$ for $1\le k\le n$.
3. Lemma 1: if $d(p,q)\ge\min(l_p,l_q)$ for distinct nodes and $l_p\le\frac12\mathrm{OPTIMAL}$ for all $p$, then

$$\sum_p l_p\le\tfrac12\bigl(\lceil\lg n\rceil+1\bigr)\mathrm{OPTIMAL}.$$

4. Lemma 2: $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for every node $j$ of $T$.
5. (3.7): $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$.
6. (3.10): $\mathrm{COST}(T_i,a_i)\le 2\,d(a_i,a_j)$ whenever $j<i$.
7. (3.12): $\mathrm{COST}(T_i,a_i)\le\mathrm{OPTIMAL}$ for $1\le i<n$.

Significance

The result. Theorem 3 is a guarantee for an entire class of algorithms rather than for one. Any rule for choosing the next node, including rules designed for speed or for empirical quality, inherits a worst-case ratio of $\lceil\lg n\rceil+1$ from the insertion step alone. The rule matters only for improving on that: nearest and cheapest insertion achieve the constant $2(1-1/n)$ (Theorem 4 and its corollary, the subject of the third mission of this series), while the logarithmic bound remains the best general statement for other rules, such as farthest or arbitrary insertion. Lemma 1 is reusable on its own: it converts "every node carries a charge bounded by half the optimum and by its distance to other nodes" into a logarithmic bound, and the same lemma yields the nearest neighbor bound of Theorem 1.

Formalizing it. The theorem has been proved since 1977; the work here is a machine-checked proof of the known argument together with a reusable library for subtours, insertion and insertion costs. The companion nearest neighbor bound (Theorem 1) is already on the platform as SupplyChainTheory.nearest_neighbor_bound (proved), and nearest insertion with constant 2 as SupplyChainTheory.nearest_insertion_bound; neither covers arbitrary insertion methods or states Lemma 1 separately.

Difficulty

The per-step facts are local: each insertion is cheap relative to a node already present (Lemma 2) and relative to OPTIMAL (3.12). The obvious way to combine them, adding up $n-1$ costs each at most OPTIMAL, gives only the ratio $n-1$. The logarithm comes from a global counting argument over all nodes simultaneously (Lemma 1), in which OPTIMAL is compared with tours on nested subsets of nodes of doubling size, and the per-node charges must be matched against the edges of those tours. Formally, the delicate parts are the bookkeeping of subtours as they grow (that every earlier node lies on the current subtour, and that the insertion cost equals the length increase), the shortcutting of a tour to an arbitrary subset, and the ceiling-of-logarithm arithmetic.

Formalization scope

Nodes are Fin n; a tour of all nodes is a permutation τ : Equiv.Perm (Fin n), and OPTIMAL is the minimum of the tour length over the finite, nonempty set of permutations. Subtours are duplicate-free lists of nodes, with closed length $d(x_0,x_1)+\dots+d(x_{m-1},x_0)$. TOUR$(T,k)$ is encoded as inserting $k$ at a list position whose resulting length is minimal among all positions; inserting at a position removes exactly one edge of $T$ and raises the length by exactly $d(x,k)+d(k,y)-d(x,y)$, so this is the paper's rule, with every tie-breaking allowed. COST is the minimum length increase over positions. The paper's 1-based subtour index is kept ($T_1=[a_0]$, $T_n$ final). $\lceil\lg n\rceil$ is Nat.clog 2 n. All quantities are real.

Conventions and deviations, each disclosed in the item statements:

• The distance satisfies $d(i,i)=0$, a normalization not in the paper; a loop never enters any length.
• Ratios are multiplied out ($\mathrm{INSERT}\le c\cdot\mathrm{OPTIMAL}$), so the paper's exclusion of the identically zero distance (1.1) is not needed.
• Condition a) of Lemma 1 is required for distinct nodes only. The page says "for all nodes $p$ and $q$", which for $p=q$ would force every $l_p\le 0$ and make the lemma inapplicable in the proof of Theorem 3; the proof uses the condition only on edges of a tour.
• (2.2) is stated for every subset of the nodes and every tour, which is what the shortcut argument shows; the paper applies it to one specific subset and an optimal tour.
• (2.1) uses 0-based node labels, so its range $k+1,\dots,\min(2k,n)$ becomes $k,\dots,\min(2k,n)-1$.

The goal quantifies over every run: any choice of the inserted nodes $a_i$ and any minimizing insertion position. Adding a selection rule (nearest, cheapest) or fixing a tie-breaking would state a weaker, different theorem; restricting to instances with OPTIMAL $=0$ or to a fixed small $n$ would trivialize it.

Reusable beyond this mission: the subtour and insertion library (closed length of a list, TOUR, COST, insertion runs) and Lemma 1, which also yields Theorem 1. Contributions welcome: proofs of the milestones, general lemmas about the closed length of List.insertIdx and of filtered lists, and a proof of Theorem 1 from this mission's Lemma 1.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• V. Bafna, B. Kalyanasundaram, K. Pruhs, Not all insertion methods yield constant approximate tours in the Euclidean plane, Theoretical Computer Science 125(2):345–353, 1994.

Motivation

Many problems in optimization and equilibrium modelling reduce to a system of equations $F(x) = 0$ with $F : \mathbb{R}^n \to \mathbb{R}^n$ that is continuous and locally Lipschitz but not differentiable. Complementarity problems rewritten through the min or Fischer–Burmeister functions, Karush–Kuhn–Tucker systems of nonlinear programs, and the gradients of augmented Lagrangians all have this form. Newton's method $x^{k+1} = x^k - F'(x^k)^{-1}F(x^k)$ cannot be applied verbatim, because $F'(x^k)$ need not exist.

Qi and Sun (Math. Programming 58 (1993) 353–367) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and proved that the resulting method converges under a condition they called semismoothness, extending Mifflin's notion (SIAM J. Control Optim. 15 (1977)) from functionals to maps. The paper has two convergence results. Theorem 3.2 is local: near a semismooth root with nonsingular generalized Jacobian the method converges superlinearly. Theorem 3.3, the target of this mission, is global in the Newton–Kantorovich sense: explicit constants on a ball $S$ around the starting point guarantee that the iteration never leaves $S$, that $F$ has exactly one zero in $S$, and that the iterates converge to it with a computable error bound. The authors describe it as "an extension of the classical Newton-Kantorovich theorem" (p. 361), which is stated for smooth maps in Ortega and Rheinboldt's monograph.

Timeline.

• 1948: Kantorovich proves semilocal convergence of Newton's method for smooth operators in Banach spaces.
• 1975–1983: Clarke introduces the generalized gradient and generalized Jacobian of a locally Lipschitz map (Optimization and Nonsmooth Analysis, Wiley 1983).
• 1977: Mifflin defines semismooth functionals.
• 1990: Pang proves convergence of a B-derivative Newton method under a strong Fréchet derivative at the solution.
• 1993: Qi and Sun (this paper) prove local and global convergence of the generalized-Jacobian Newton method for semismooth maps.

Setting

Work in $\mathbb{R}^n$ with the Euclidean norm $\|\cdot\|$; for a linear map $V$, $\|V\|$ is the induced operator norm. Let $F : \mathbb{R}^n \to \mathbb{R}^n$ be locally Lipschitz. Write $D_F$ for the set of points where $F$ is differentiable and $JF(y)$ for the derivative at $y \in D_F$.

• The generalized Jacobian of $F$ at $x$ is

$$\partial F(x) = \mathrm{co}\Big\{\lim_{i\to\infty} JF(x_i) : x_i \to x,\ x_i \in D_F\Big\}.$$

• The directional derivative is $F'(x;h) = \lim_{t\downarrow 0}\,(F(x+th)-F(x))/t$.
• $F$ is semismooth at $x$ if it is Lipschitz near $x$ and, for every $h$, $V h'$ has a limit as $V \in \partial F(x+th')$, $h' \to h$, $t \downarrow 0$. Semismoothness implies that $F'(x;h)$ exists.
• A run of the nonsmooth Newton method (3.2) from $x^0$ is a pair of sequences $(x^k)$, $(V_k)$ with $V_k \in \partial F(x^k)$ and $V_k(x^{k+1} - x^k) = -F(x^k)$ for all $k$; any element of $\partial F(x^k)$ may be chosen.

In Lean these are NonsmoothNewton.Global.clarkeJac, dirDeriv, SemismoothAt and IsNewtonRun, over EuclideanSpace ℝ (Fin n).

Fix $x^0$, $r \ge 0$, the closed ball $S = \{x : \|x - x^0\| \le r\}$, and constants $\beta, \gamma, \delta$ with $\alpha = \beta(\gamma+\delta)$.

Formalization targets

Goal: Theorem 3.3 (global convergence)

Assume $F$ is semismooth at every point of $S$ and, for all $x, y \in S$ and $V \in \partial F(x)$: $V$ is nonsingular,

$$\|V^{-1}\| \le \beta,\qquad \|V(y-x) - F'(x;y-x)\| \le \gamma\|y-x\|,\qquad \|F(y)-F(x)-F'(x;y-x)\| \le \delta\|y-x\|,$$

with $\alpha < 1$ and $\beta\|F(x^0)\| \le r(1-\alpha)$. Then every run of (3.2) from $x^0$ stays in $S$, every $V_k$ is nonsingular, $F$ has a unique zero $x^*$ in $S$, $x^k \to x^*$, and

$$\|x^k - x^*\| \le \frac{\alpha}{1-\alpha}\,\|x^k - x^{k-1}\|,\qquad k = 1, 2, \dots \tag{3.4}$$

Milestones (steps of the proof, p. 360)

1. The first step: $\|x^1 - x^0\| \le \beta\|F(x^0)\| \le r(1-\alpha)$, so $x^1 \in S$.
2. One-step contraction: for consecutive Newton points with $x^{k-1}, x^k \in S$, $\|x^{k+1} - x^k\| \le \alpha\|x^k - x^{k-1}\|$.
3. All iterates remain in $S$, with $\|x^{k+1} - x^k\| \le r\alpha^k(1-\alpha)$.
4. A run that stays in $S$ and converges has uniformly bounded $\|V_k\|$, and its limit is a zero of $F$.
5. $F$ has at most one zero in $S$.

Significance

The theorem certifies, from data checkable on a single ball, that a solution exists, where it is, that it is unique there, and how far the current iterate is from it; (3.4) is an a-posteriori stopping criterion. It holds for every choice of $V_k \in \partial F(x^k)$, which is what implementations need, since they compute one element of $\partial F$ and not the whole set. The result underlies the global and semilocal analysis of semismooth Newton methods for complementarity problems, variational inequalities and nonsmooth KKT systems, a line that continued through the 1990s and 2000s.

The theorem is proved on paper; no machine-checked version is known. The platform has no Newton–Kantorovich theorem, smooth or nonsmooth, and no Clarke generalized Jacobian. A complete formalization would supply both, and the definitions layer here (generalized Jacobian, one-sided directional derivative, semismoothness, Newton runs) is shared with the two companion missions on Qi and Sun's local convergence theorem and on semismoothness of augmented Lagrangian gradients.

Difficulty

The Newton map is set-valued: $x^{k+1}$ depends on the choice of $V_k$, so the Banach fixed-point theorem for a single contraction does not apply directly, and the argument must hold for every sequence of choices. The contraction estimate needs both consecutive steps to start inside $S$, so containment in $S$ and the geometric decay of the steps must be established together. Identifying the limit as a zero requires a uniform bound on $\|V_k\|$, which is not a hypothesis: it has to come from local Lipschitz continuity through the structure of the generalized Jacobian. Uniqueness uses an element $V^* \in \partial F(x^*)$, whose existence rests on Rademacher's theorem. Finally, the directional derivative in the hypotheses is only meaningful because semismoothness makes it exist.

Formalization scope

The space is EuclideanSpace ℝ (Fin n), so the norm is Euclidean, as in the paper (p. 356), and $\|V^{-1}\|$ is the operator norm. Local Lipschitzness is global (LocallyLipschitz F), the standing assumption of Section 3. Conventions:

• $\partial F(x)$ is the convex hull of limits of fderiv along sequences in $D_F$; no closure is taken (the limit set is compact for locally Lipschitz $F$).
• "$V$ nonsingular, $\|V^{-1}\| \le \beta$" is the existence of a two-sided inverse $W$ with $\|W\| \le \beta$; Ring.inverse is not used.
• $F'(x;h)$ is dirDeriv, a limUnder along $t \to 0^+$, used only at points of $S$, where semismoothness makes the limit exist.
• The run is a relation, not a function; every choice of $V_k$ is covered, and nonsingularity of each $V_k$ is a conclusion.
• The radius condition $r \ge 0$ is an explicit hypothesis. Without it, $r < 0$ and $\beta < 0$ would satisfy all other hypotheses vacuously while $x^0 \notin S$.
• The paper's third inequality sits under "for any $V \in \partial F(x)$"; it is stated without $V$, which is equivalent because $\partial F(x) \ne \emptyset$.
• (3.4) is stated at index $k+1$ for $k \ge 0$, avoiding natural-number subtraction.
• The paper's statements contain no $o(\cdot)$ or $O(\cdot)$; all constants are explicit and fixed before the quantifiers over points of $S$.

The goal is the full four-part conclusion: containment, existence, uniqueness, and convergence with (3.4). A formalization that proves only that the iterates converge to some zero, or that treats $\partial F(x)$ as possibly empty so that the hypotheses become vacuous, is not the theorem. The hypotheses are satisfiable by genuinely nonsmooth maps, e.g. $F(x) = x + \tfrac{1}{10}|x| - c$ on $\mathbb{R}$ with a ball containing the kink.

A complete development needs: nonemptiness and local boundedness of the generalized Jacobian (Rademacher's theorem, available in Mathlib as LipschitzWith.ae_differentiableAt); geometric-series and Cauchy-sequence arguments in a complete space. The generalized-Jacobian facts are reusable well beyond this mission. Contributions of any of the milestones, or of these general facts as separate lemmas, are welcome.

Selected references

• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, New York, 1983. https://doi.org/10.1137/1.9781611971309
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15 (1977) 959–972. https://doi.org/10.1137/0315061
• J. M. Ortega, W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970. https://doi.org/10.1137/1.9780898719468
• J.-S. Pang, Newton's method for B-differentiable equations, Mathematics of Operations Research 15 (1990) 311–341. https://doi.org/10.1287/moor.15.2.311