Operations Research

Motivation

Many stochastic dynamic programs in operations research, such as inventory control with partially observed demand or the pricing of American options, are too large to solve exactly. A heuristic policy gives a lower bound on the optimal expected reward; to judge whether it is good enough one needs an upper bound. Brown, Smith and Sun (Oper. Res. 2010) build such bounds by information relaxation: let the decision maker see more than she would in reality, and charge a penalty for using the extra information. The construction generalizes the martingale duality for optimal stopping of Haugh and Kogan (Oper. Res. 2004), Rogers (Math. Finance 2002) and Andersen and Broadie (Manage. Sci. 2004).

In applications, the analyst chooses both the relaxation and the penalty, trading the quality of the bound against the cost of computing it. Proposition 2.3 of the paper collects four properties that govern this choice. The first is the subject of this mission.

Setting

Uncertainty is a probability space $(\Omega,\mathcal F,\mathbb P)$, and decisions are made in periods $t=0,\dots,T$. The natural filtration $\mathbb F=(\mathcal F_0,\dots,\mathcal F_T)$ records what is known in each period, with $\mathcal F_0=\{\emptyset,\Omega\}$. An action sequence is $a=(a_0,\dots,a_T)$, chosen from feasible sets $A_t(a_0,\dots,a_{t-1})$. Period rewards $r_t(a_0,\dots,a_t)$ are $\mathcal F_t$-measurable random variables and the total reward is $r(a)=\sum_t r_t(a)$.

A policy is a map $\alpha:\Omega\to A$ from outcomes to feasible action sequences. It is adapted to a filtration $\mathbb G$ if the period-$t$ action is $\mathcal G_t$-measurable; $\mathcal A_{\mathbb G}$ denotes these policies. A filtration $\mathbb G$ with $\mathcal F_t\subseteq\mathcal G_t\subseteq\mathcal F$ for all $t$ is a relaxation of $\mathbb F$, written $\mathbb F\subseteq\mathbb G$. A penalty is a function $z(a,\omega)$; it is dual feasible if $\mathbb E[z(\alpha_F)]\le0$ for every $\alpha_F\in\mathcal A_{\mathbb F}$. For any relaxation $\mathbb G$ and dual feasible $z$, the dual bound

$$\sup_{\alpha_G\in\mathcal A_{\mathbb G}}\mathbb E\big[r(\alpha_G)-z(\alpha_G)\big]$$

is at least the optimal value $\sup_{\alpha_F\in\mathcal A_{\mathbb F}}\mathbb E[r(\alpha_F)]$ (weak duality, Lemma 2.1).

The paper's main source of penalties is Proposition 2.2. Given generating functions $w_t(a)$ depending only on $a_0,\dots,a_t$, set

$$z_t(a)=\mathbb E[w_t(a)\mid\mathcal G_t]-\mathbb E[w_t(a)\mid\mathcal F_t],\qquad z(a)=\sum_{t=0}^T z_t(a).$$

Such a penalty has zero mean along every nonanticipative policy, and its dual bound is computed by the backward recursion (10), the Bellman recursion with rewards $r_t-z_t$ and conditional expectations given $\mathcal G_t$.

Formalization targets

Goal: Proposition 2.3(i)

For filtrations $\mathbb F\subseteq\mathbb G^1\subseteq\mathbb G^2$ and one common sequence of generating functions $(w_0,\dots,w_T)$, let $z^i$ be the Proposition 2.2 penalty of $(\mathbb G^i,w)$. Then

$$\sup_{\alpha_G\in\mathcal A_{\mathbb G^1}}\mathbb E\big[r(\alpha_G)-z^1(\alpha_G)\big]\le\sup_{\alpha_G\in\mathcal A_{\mathbb G^2}}\mathbb E\big[r(\alpha_G)-z^2(\alpha_G)\big].\qquad(12)$$

With a common generating function, a looser relaxation gives a weaker bound.

Milestones

1. Equation (10). For a Proposition 2.2 penalty under a relaxation $\mathbb G$, the expectation of the initial dual value function $V^{\mathbb G}_0$ equals the dual bound.
2. Proposition 2.3(ii). For dual feasible $z^1,z^2$ and one relaxation $\mathbb G$, the difference of the two dual bounds lies between $\inf_{\alpha_G}\mathbb E[z^2(\alpha_G)-z^1(\alpha_G)]$ and $\sup_{\alpha_G}\mathbb E[z^2(\alpha_G)-z^1(\alpha_G)]$, eq. (13).
3. Proposition 2.3(iii). For $\mathbb F\subseteq\mathbb F'\subseteq\mathbb G$, the penalty $z_t(a)=\mathbb E[w_t(a)\mid\mathcal G_t]-\mathbb E[w_t(a)\mid\mathcal F'_t]$ still satisfies the conclusions of Proposition 2.2.
4. Proposition 2.3(iv). If $\hat z_t(a)$ are unbiased estimates of the terms $z_t(a)$ of a dual feasible penalty, $\mathbb E[\hat z_t(a)\mid\mathcal G_t]=z_t(a)$, and the relaxation $\widehat{\mathbb G}$ additionally reveals the estimates, then the dual bound of $(\mathbb G,z)$ is at most that of $(\widehat{\mathbb G},\hat z)$, eq. (14).

Milestone 1 is on the goal's path; milestones 2–4 are the remaining parts of the same proposition.

Significance

Proposition 2.3(i) tells the analyst how to read a weak bound. If a cheap generating function (for instance $w_t=0$, the zero penalty) gives a satisfactory bound under some relaxation, it will give a bound at least as tight under any less informative relaxation that still contains $\mathbb F$; conversely, moving to a looser relaxation without improving the generating function can only weaken the bound. Part (ii) is a continuity statement: penalties close to the ideal penalty give bounds close to the optimal value. Part (iii) permits the subtracted conditional expectation to be computed under an intermediate filtration, which the paper uses when volatility is unobserved in its option-pricing example. Part (iv) is the justification for estimating penalties by nested simulation, as in the methods of Haugh–Kogan and Andersen–Broadie: unbiased estimates yield valid, if weaker, upper bounds.

The results are proved in the paper's electronic companion. To our knowledge none of them, nor the information-relaxation duality framework itself, has a machine-checked proof. Formalizing them requires a usable theory of policies adapted to a filtration, penalties evaluated along random action sequences, and backward recursions with conditional expectations, all of which are reusable for other duality results in stochastic dynamic programming.

Difficulty

The obvious argument for (12) compares the two suprema policy by policy: $\mathcal A_{\mathbb G^1}\subseteq\mathcal A_{\mathbb G^2}$. This fails, because the two bounds use different penalties: for a fixed $\mathbb G^1$-adapted policy, $\mathbb E[z^1(\alpha)]$ and $\mathbb E[z^2(\alpha)]$ need not agree, so the larger policy set alone does not order the bounds. The penalty changes with the relaxation exactly so as to remove part of the value of the extra information, and the statement asserts that it never removes more than that information is worth. Even the representation (10) of a dual bound by a backward recursion is nontrivial: it requires near-optimal actions to be selected measurably in every period.

In Lean, the further difficulty is the composition of an action-indexed family of conditional expectations with a random action: $\omega\mapsto z_t(\alpha(\omega))(\omega)$, where each $z_t(a)$ is only defined almost surely. Countability of the action set is what makes this composite well defined up to null sets.

Formalization scope

Periods are Fin (T + 1); an action sequence is a function Fin (T + 1) → X for one countable action type X with the discrete σ-algebra (the disjoint union of the per-period action sets). Filtrations are Mathlib Filtrations of the ambient σ-algebra; a relaxation is 𝔽 ≤ 𝔾. Policies are maps Ω → (Fin (T + 1) → X) with values in the feasible set, adapted when each action is measurable for the corresponding σ-algebra. Conditional expectations are Mathlib's μ[f | m], so identities between them hold almost surely. Dual bounds are suprema in EReal over the adapted policy sets, so an infinite bound is represented and no junk value $0$ arises from an unbounded supremum.

Pinned regularity, beyond the paper's text: period rewards and generating functions are uniformly bounded (almost surely for the latter) and measurable, so that every expectation exists; in part (iv), the estimates are measurable and uniformly bounded. In part (ii), the difference of two dual bounds is taken in EReal, and the case where both bounds are $+\infty$ (where the page's difference is undefined) is excluded.

The penalties $z^1,z^2$ of the goal are computed from $w$ by the formula of Proposition 2.2; stating the goal for arbitrary penalties with Proposition 2.2's properties would be a different and false claim. Likewise $\widehat{\mathbb G}$ in part (iv) is constructed from $\mathbb G$ and the estimates.

The definitions duplicate those of mission 1 of this series (the framework, the recursive model, the penalty construction); they are expected to be merged. Contributions of reusable lemmas about adapted policies over countable action sets and about backward recursions with conditional expectations are welcome.

Selected references

• D. B. Brown, J. E. Smith, P. Sun, Information Relaxations and Duality in Stochastic Dynamic Programs, Operations Research, Articles in Advance, 2010. https://doi.org/10.1287/opre.1090.0796
• M. B. Haugh, L. Kogan, Pricing American Options: A Duality Approach, Operations Research 52(2), 2004. https://doi.org/10.1287/opre.1030.0070
• L. Andersen, M. Broadie, Primal-Dual Simulation Algorithm for Pricing Multidimensional American Options, Management Science 50(9), 2004. https://doi.org/10.1287/mnsc.1040.0258
• L. C. G. Rogers, Monte Carlo Valuation of American Options, Mathematical Finance 12(3), 2002. https://doi.org/10.1111/1467-9965.02010

Motivation

Bounded-confidence models describe a population of agents who repeatedly average their opinions with those of agents whose opinions are close to their own. They are used to study consensus and polarization in opinion formation, and in control as a primitive for decentralized rendezvous of mobile agents. Simulations of these models show a robust phenomenon: opinions converge to clusters, and the distances between clusters are typically close to twice the confidence radius rather than just above it. For finitely many agents this regularity has resisted proof.

V. D. Blondel, J. M. Hendrickx and J. N. Tsitsiklis (SIAM J. Control Optim. 48 (2010) 5214–5240) study a continuous-time version of the model in two forms: with $n$ discrete agents, and with a continuum of agents indexed by $[0,1]$. For the continuum they prove that regular initial opinions converge to clusters whose separation obeys a lower bound depending on the cluster weights. To transfer such conclusions to finitely many agents one needs to know that the $n$-agent model is close to the continuum model when $n$ is large. Section 4 of the paper proves this on every finite time horizon. This mission formalizes that result.

Setting

Discrete agents. There are $n\ge1$ agents with real opinions $\xi_i(t)$, $t\ge0$. Agents $i$ and $j$ interact when $|\xi_i-\xi_j|<1$. A solution of (2.1) is a continuous $\xi:[0,\infty)\to\mathbb R^n$ with

$$\xi_i(t)=\xi_i(0)+\int_0^t\sum_{j:\,|\xi_i(\tau)-\xi_j(\tau)|<1}\bigl(\xi_j(\tau)-\xi_i(\tau)\bigr)\,d\tau$$

for all $t\ge0$ and all $i$. The right-hand side is discontinuous when the interaction graph changes, so the integral form is used. A solution is proper if it is the unique solution from its initial value, its non-differentiability times have no accumulation point, and two agents that meet stay together.

Continuum agents. Agents are indexed by $\alpha\in I=[0,1]$ with Lebesgue measure. $Y$ is the set of bounded measurable functions $I\to\mathbb R$. For $m,M>0$, $X_m^M$ is the set of nondecreasing $\tilde x$ with $m\le\frac{\tilde x(\beta)-\tilde x(\alpha)}{\beta-\alpha}\le M$ for $\beta\ne\alpha$; such $\tilde x$ are regular. The interaction operator is

$$\mathcal L(\tilde x)(\alpha)=\int_I \mathbf 1\bigl[|\tilde x(\alpha)-\tilde x(\gamma)|<1\bigr]\,\bigl(\tilde x(\gamma)-\tilde x(\alpha)\bigr)\,d\gamma ,$$

and a solution of (3.2) from $\tilde x_0$ is a measurable $x:(\alpha,t)\mapsto x_t(\alpha)$ with every $x_t\in Y$ and $x_t(\alpha)=\tilde x_0(\alpha)+\int_0^t\mathcal L(x_\tau)(\alpha)\,d\tau$ for all $t\ge0$ and all $\alpha\in I$.

The embedding. For $\xi\in\mathbb R^n$, $G(\xi)$ is the step function with $G(\xi)(\alpha)=\xi_i$ on $[\frac{i-1}n,\frac in)$ and $G(\xi)(1)=\xi_n$. It distributes the $n$ agents over $n$ blocks of $I$ of length $1/n$.

Formalization targets

Goal: Theorem 7 (finite-horizon approximation)

Let $\tilde x_0\in X_m^M$, $x$ the solution of (3.2) from $\tilde x_0$, and for each $n\ge1$ let $\xi^{\langle n\rangle}$ be a proper solution of (2.1) with nondecreasing $\xi^{\langle n\rangle}(0)$ and $\|G(\xi^{\langle n\rangle}(0))-\tilde x_0\|_\infty\to0$. Then for every $T$ and $\varepsilon>0$ there is $n'$ with

$$\bigl\|G\bigl(\xi^{\langle n\rangle}(t/n)\bigr)-x_t\bigr\|_\infty\le\varepsilon\qquad(t\in[0,T],\ n\ge n').$$

The statement fixes no rate in $n$ and no dependence of $n'$ on $T$; it asserts only uniform convergence on bounded time intervals.

Milestones

1. Lemma 1: for $\tilde x\in X_m$ and $\tilde y\in Y$, $\|\mathcal L(\tilde x)-\mathcal L(\tilde y)\|_\infty\le(2+8/m)\|\tilde x-\tilde y\|_\infty$.
2. Theorem 4, left inequality of (3.7): a solution from $\tilde x_0\in X_m^M$ satisfies $x_t(\beta)-x_t(\alpha)\ge m e^{-t}(\beta-\alpha)$ for all $t\ge0$, $\alpha<\beta$.
3. Proposition 4: for every $\varepsilon,T>0$ there is $\delta>0$ such that every solution $y$ of (3.2) with $\|y_0-\tilde x_0\|_\infty\le\delta$ satisfies $\|y_t-x_t\|_\infty\le\varepsilon$ on $[0,T]$.
4. Embedding (Section 4): if $\xi$ solves (2.1), then $(\alpha,t)\mapsto G(\xi(t/n))(\alpha)$ solves (3.2) from $G(\xi(0))$.

Significance

The theorem says that the continuum model is the large-population limit of the $n$-agent model over any fixed time window. Combined with the paper's continuum convergence result (Theorem 6), it supports the paper's Conjecture 1 on intercluster distances for finitely many agents, and it is the first step of the paper's Proposition 5, which derives Conjecture 1 for random initial opinions from a stability conjecture for the continuum. It is a mean-field limit for a model whose interaction kernel is discontinuous, where standard Lipschitz mean-field arguments do not apply directly.

All four results and the goal are proved in the paper (with the time-scale correction described below). None of them has a machine-checked proof that this mission is aware of. The formalization contributes a checked continuous-dependence estimate for a discontinuous integral equation, a checked statement that the finite-agent dynamics embed in the continuum dynamics, and a precise record of the time normalization under which the two models agree.

Difficulty

The operator $\mathcal L$ is not Lipschitz on $Y$: moving one opinion across the confidence threshold changes the interaction set discontinuously. The obvious Gronwall argument for continuous dependence therefore fails for two arbitrary solutions. It works only around a trajectory that stays in some $X_{m'}$, where few agents sit near the threshold, which is why the lower slope bound must hold at every time and not only at time $0$. The perturbed trajectory, coming from $n$ agents, is a step function and is never regular, so the estimate must be one-sided in this sense.

A literal reading of the page also fails. The page writes $G(\xi^{\langle n\rangle}(t))$, but for $\alpha$ in block $i$ the continuum interaction $\mathcal L(G(\xi))(\alpha)$ equals $\frac1n$ times the discrete right-hand side of (2.1). With $\tilde x_0(\alpha)=\alpha/2$ and $\xi^{\langle n\rangle}_i(0)=\tilde x_0(i/n)$, both models are linear; at $t=1$ the sup distance between $G(\xi^{\langle n\rangle}(1))$ and $x_1$ tends to $e^{-1}/4$. The discrete time must be rescaled by $1/n$.

Formalization scope

Namespace BHTOpinion.Approx. Agents of the discrete model are Fin n (0-based); the continuum index set is Set.Icc (0:ℝ) 1 with Lebesgue measure. Opinion functions are ℝ → ℝ, of which only the values on $I$ matter; trajectories are written x t α, time first, with time in ℝ and explicit $t\ge0$ guards. In 0-based form, $G(\xi)(\alpha)=\xi_{\min(\lfloor n\alpha\rfloor,n-1)}$ on $I$; for $n=0$ the definition returns $0$, and every statement assumes $n\ge1$.

Explicit readings of the paper's phrases:

• Sup norms are written pointwise over $I$, including $\alpha=1$: a bound at every $\alpha\in I$, never a real supremum.
• "$\lim_{n\to\infty}\|G(\xi^{\langle n\rangle}(0))-\tilde x_0\|_\infty=0$" is: for every $\delta>0$ there is $N$ such that the pointwise bound $\delta$ holds for all $n\ge N$.
• "There exists $n'$" is an explicit $\exists\,n'$ with the bound for all $n\ge n'$, $t\in[0,T]$, $\alpha\in I$.
• "The solution $x$" of (3.2) is any solution from $\tilde x_0$; the theorem holds for each.
• "Proper initial condition, admitting a unique solution" is kept as printed: uniqueness from $\xi^{\langle n\rangle}(0)$, finitely many non-differentiability times on every bounded interval, agents that meet stay together.
• Solutions of (2.1) and (3.2) require the time integrand to be integrable; Lean's integral of a non-integrable function is $0$.
• The labelled correction: the discrete trajectory enters as $\xi^{\langle n\rangle}(t/n)$ in the embedding claim and in Theorem 7. Equivalently, the page's statement holds for the weighted model (2.4) with weights $1/n$; only the rescaled form is stated.
• Only the left inequality of (3.7) is a milestone. The right inequality $Me^{4t/m}$ is not used by Section 4.

A trivializing formalization is ruled out: the hypotheses are satisfied by $\tilde x_0(\alpha)=\alpha\in X_1^1$, the conclusion is not vacuous because $G$ is evaluated at $n\ge1$ only, and the perturbed initial values $y_0$ in Proposition 4 range over all of $Y$, not over regular functions.

Infrastructure needed: Gronwall's inequality for a sup-norm difference, measure-theoretic bookkeeping for $\mathcal L$ on step functions, and a change of variables $\tau\mapsto\tau/n$ in interval integrals. The Lipschitz estimate on $X_m$ and the slope bound are reusable for any continuum bounded-confidence model. Contributions to any milestone are welcome; the embedding milestone is independent of the other three.

Selected references

• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, Continuous-time average-preserving opinion dynamics with opinion-dependent communications, SIAM J. Control Optim. 48(8), 2010, 5214–5240. https://doi.org/10.1137/090766188

Motivation

In many production and service settings a single resource is shared by several parties, each judging the outcome only by how its own work is treated. Multi-agent scheduling studies this situation. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model in which two agents, A and B, each own a set of jobs and each minimize their own objective. Their paper treats two questions: the constrained problem, minimizing A's objective subject to a bound on B's, and the Pareto problem, describing every schedule that cannot be improved for one agent without hurting the other.

For the Pareto problem the first quantity of interest is the number of distinct trade-offs, because the natural way to compute the whole front is to solve the constrained problem repeatedly with a decreasing bound (the paper's scheme PP, Figure 4, p. 239). Enumeration of this kind is polynomial exactly when the number of nondominated pairs is polynomially bounded. This mission formalizes the paper's bound for the case where both agents minimize a maximum of regular cost functions (§11.1, pp. 239–240).

Setting

Agent A owns the jobs $J^A_1,\dots,J^A_{n_A}$ and agent B owns $J^B_1,\dots,J^B_{n_B}$, with $n_A,n_B\ge1$. Every job $j$ has a processing time $p_j\ge0$. All jobs are available at time $0$. A schedule $\sigma$ is an ordering of all $n_A+n_B$ jobs; the machine processes them in that order from time $0$ without idle time, so the completion time $C_j(\sigma)$ of a job is the sum of the processing times of the jobs up to and including it.

Each A-job carries a cost function $f^A_h:\mathbb R\to\mathbb R$ and each B-job a cost function $f^B_k$, all nondecreasing (regular). The agents' objectives are the maximum costs

$$f^A_{\max}(\sigma)=\max_{h} f^A_h\big(C^A_h(\sigma)\big),\qquad f^B_{\max}(\sigma)=\max_{k} f^B_k\big(C^B_k(\sigma)\big).$$

This covers the makespan and maximum lateness of each agent as special cases.

A schedule $\sigma$ is nondominated if no schedule $\bar\sigma$ satisfies $f^A_{\max}(\bar\sigma)\le f^A_{\max}(\sigma)$ and $f^B_{\max}(\bar\sigma)\le f^B_{\max}(\sigma)$ with at least one inequality strict. The pair $(y^A,y^B)=(f^A_{\max}(\sigma),f^B_{\max}(\sigma))$ of a nondominated schedule is a nondominated pair, and the schedule corresponds to that pair. Write $\mathcal N$ for the set of nondominated pairs. Different nondominated schedules can share a pair; the problem $1\|f^A_{\max}\circ f^B_{\max}$ asks for $\mathcal N$, with one schedule per pair. Job $a$ precedes job $b$ in $\sigma$ if $a$ comes before $b$ in the ordering.

Formalization targets

Goal: Theorem 11.3, corrected (p. 240)

$$|\mathcal N|\le n_A\,n_B+1 .$$

The paper prints the bound $n_An_B$. It is off by one: with $n_A=n_B=1$, unit processing times and $f^A(t)=f^B(t)=t$, the schedules AB and BA give the two nondominated pairs $(1,2)$ and $(2,1)$. The goal states $n_An_B+1$, the bound the printed argument supports once the first schedule is counted.

Milestones

1. Lemma 11.1 (p. 239). For nondominated pairs $(y^A,y^B)$, $(\tilde y^A,\tilde y^B)$ with $y^A<\tilde y^A$ and $y^B>\tilde y^B$ and for a fixed A-job $J^A_h$ and B-job $J^B_k$, there are corresponding nondominated schedules $\sigma,\tilde\sigma$ such that if $J^B_k$ precedes $J^A_h$ in $\sigma$, it does so in $\tilde\sigma$.
2. Lemma 11.2 (p. 240). The same, with one pair $\sigma,\tilde\sigma$ serving every A-job and every B-job at once.
3. The exchange claim (proof of Theorem 11.3, p. 240). Two nondominated schedules $\sigma,\tilde\sigma$ with $f^A_{\max}(\sigma)<f^A_{\max}(\tilde\sigma)$ and $f^B_{\max}(\tilde\sigma)<f^B_{\max}(\sigma)$ differ in the relative order of at least one A-job and one B-job: some $J^A_h$ precedes some $J^B_k$ in $\sigma$, and $J^B_k$ precedes $J^A_h$ in $\tilde\sigma$.

Significance

The bound places $1\|f^A_{\max}\circ f^B_{\max}$ among the two-agent problems whose Pareto front has polynomially many points. Combined with the polynomial algorithm for the constrained problem $1\|f^A_{\max}:f^B_{\max}\le Q$ (Theorem 4.1 of the same paper), it means the full front can be listed with polynomially many constrained solves. The structural content is an order statement: as the bound on agent B tightens along the front, B-jobs overtake A-jobs and never fall back, so each of the $n_An_B$ (A-job, B-job) pairs changes order at most once. The same question for other pairs of objectives is the subject of later work on multi-agent scheduling, collected in the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal (Springer 2014).

The result is published but, to our knowledge, has no machine-checked proof. Formalizing it also fixes the printed off-by-one error in the statement. The overtaking lemmas are of independent use for other pairs of regular min-max objectives.

Difficulty

The obvious argument walks along the front and charges each step to one (A-job, B-job) pair that changes order. Two things must be secured. First, the charged pair must change order in a consistent direction; schedules corresponding to a pair are not unique, and nothing forces two arbitrary representatives of different pairs to agree on the order of the jobs they do not charge. Lemma 11.2 asserts that representatives can be chosen so that no B-job falls back behind an A-job, and establishing it requires control over every job pair simultaneously, not one at a time as in Lemma 11.1. Second, a step must change at least one order. The tempting proof looks at a B-job attaining $y^B$ and argues that the jobs it overtakes include an A-job; this fails for an arbitrary choice of that B-job, since another B-job with a flatter cost function can be the one that moves. Finally, the count of reversals bounds the number of steps, not the number of pairs; the first pair has to be added.

Formalization scope

Jobs are Fin nA ⊕ Fin nB (Sum.inl h is $J^A_{h+1}$, Sum.inr k is $J^B_{k+1}$, 0-based). A schedule is a duplicate-free list containing every job, and completion times are prefix sums of processing times; this is the published sequence model MooreLateJobs.Shared.completionTime (Moore 1968), reused as a reference item. Processing times are real and nonnegative; costs are real-valued and Monotone; $n_A,n_B\ge1$ so that both maxima exist. Nondominance compares against all schedules of all jobs. Precedence compares first positions in the list.

The count is over pairs, $\mathcal N\subseteq\mathbb R^2$, measured with Set.encard, so finiteness is part of the goal. Counting nondominated schedules instead would be a different and false statement: permuting jobs inside a block often leaves both maxima unchanged. The printed bound $n_An_B$ is replaced by $n_An_B+1$ and the reason is given in the goal's statement; stating a larger bound "to be safe" or the printed one would make the mission either weaker than the paper's argument or false. The scheme PP and the choice of $\epsilon$ in it are not formalized; they are the paper's computation device, not part of the theorem. In the exchange claim the paper's σ and σ̃ are schedules of consecutive pairs; the milestone states it for any two nondominated schedules with the two strict inequalities, which includes that case. Running times are not formalized.

A complete development needs elementary facts about completion times when one job is moved within a sequence, the simultaneous statement of Lemma 11.2, and a counting argument along the front. Contributions of reusable lemmas about job moves in the sequence model are welcome.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102
• A. Agnetis, J.-C. Billaut, S. Gawiejnowicz, D. Pacciarelli, A. Soukhal, Multiagent Scheduling: Models and Algorithms, Springer, 2014. https://doi.org/10.1007/978-3-642-41880-8

Motivation

Firms that change prices over time face customers who remember past prices. A large empirical literature in marketing documents reference price effects: demand depends not only on the current price but on how that price compares with a price the customer expects, and losses (prices above the reference) weigh more than gains of the same size, the loss aversion of prospect theory (Tversky and Kahneman 1991; Kalyanaram and Winer 1995). Most dynamic pricing models with reference effects form the reference price by exponential smoothing of past prices (Popescu and Wu 2007; Kopalle, Rao and Assunção 1996; Fibich, Gavious and Lowengart 2003).

Psychology suggests a different memory process. Under the peak-end rule (Kahneman et al. 1993), people evaluate a past sequence of experiences mainly by its most extreme and its most recent episode. Nasiry and Popescu (INSEAD Working Paper 2009/20/DS/TOM; published in Operations Research 59(6), 2011) build a dynamic pricing model in which the reference price is a weighted average of the lowest price seen so far and the last price, and characterize the firm's optimal long-run and transient pricing. This mission formalizes the core of that analysis: the steady states (Section 3.1) and the convergence of optimal price paths (Section 3.2).

Setting

A firm sets a price $p_t$ in the price set $\mathbf P = [0,\bar p]$ in every period $t = 1,2,\dots$. The base demand $d_0$ is non-negative, bounded, continuous and decreasing on $\mathbf P$, with $d_0(\bar p) = 0$, and the base profit $\pi_0(p) = p\,d_0(p)$ is non-monotone and strictly concave (Assumption 1). With sensitivities $\lambda\ge\gamma>0$ to surcharges and discounts, demand at price $p$ and reference price $r$ is

$$d(p,r) = d_0(p) - \lambda(p-r)^+ + \gamma(r-p)^+,$$

and the short-term profit is $\pi(p,r) = p\,d(p,r)$. It equals $\min(\pi_\lambda,\pi_\gamma)$ of the two smooth profits $\pi_k(p,r) = \pi_0(p) + k(r-p)p$.

Given an initial minimum price $m_0$ and last price $p_0$, the minimum price evolves as $m_t = \min(m_{t-1},p_t)$ and the peak-end reference price is

$$r_t = \theta m_{t-1} + (1-\theta)p_{t-1},\qquad \theta\in(0,1].$$

With discount factor $\beta\in(0,1)$, the firm's value function is

$$J(m_0,p_0) = \sup_{p_t\in\mathbf P}\ \sum_{t=1}^\infty \beta^{t-1}\pi(p_t,r_t).$$

An optimal price path is a price sequence in $\mathbf P$ attaining $J(m_0,p_0)$; a steady state is a state $(m,p)$, $m\le p$, from which the constant path $p_t\equiv p$ is optimal.

Two thresholds organize the answer. Let $s$ and $S$ be the roots in $\mathbf P$ of

$$\pi_0'(p) - \lambda(1-\beta(1-\theta))p = 0 \quad (9),\qquad \pi_0'(p) - \gamma(1-\beta)p = 0 \quad (10),$$

so that $s\le S$, and let $\mathbf R_1 = [0,s]$, $\mathbf R_2 = [s,S]$, $\mathbf R_3 = [S,\bar p]$. For $m\in\mathbf R_1$, let $p^{**}_\lambda(m)$ be the root of

$$\pi_0'(p) - \lambda(2-(1-\theta)(1+\beta))p + \lambda\theta m = 0. \quad (12)$$

Formalization targets

Goal: Proposition 3

For every initial state $(m_0,p_0)$ with $m_0\le p_0$ in $\mathbf P$, an optimal price path exists, and every optimal price path $\{p_t\}_{t\ge1}$ is monotone and converges:

$$p_t \longrightarrow \begin{cases} p^{**}_\lambda(m_0), & m_0\in\mathbf R_1,\\ m_0, & m_0\in\mathbf R_2,\\ S, & m_0\in\mathbf R_3.\end{cases}$$

The limit depends only on the initial minimum price.

Milestones

In attack order: monotonicity of $J$ (Lemma 1); the identity $\pi=\min(\pi_\lambda,\pi_\gamma)$ and supermodularity of $\pi$ (Lemma 2); the upper bounds $J(m,p)\le J^\nu_m(p)$ by smooth problems with one-dimensional state (Lemma 3); the unique steady state of each smooth problem (Lemma 4); two families of steady states (Lemma 5); the full set of steady states

$$\{(m,p^{**}_\lambda(m)) \mid m\in\mathbf R_1\}\cup\{(m,m)\mid m\in\mathbf R_2\}$$

(Proposition 1); Claims 1–4 and the invariance of the regions (Proposition 2: $p_t\ge m_0$ when $m_0\le S$, and $m_t\ge S$ when $m_0\ge S$); and Claim 5 (for $p_0>m_0\ge S$ the price eventually falls to $m_0$ or below).

Significance

The result gives a complete description of optimal pricing under peak-end anchoring with loss-averse consumers. A continuum of steady states exists, and the one reached is set by the remembered minimum price alone. A firm facing a low minimum price raises prices toward $p^{**}_\lambda(m_0)>m_0$; with an intermediate minimum it settles exactly at that minimum; with a high minimum it cuts prices down to $S$ and then holds them there. Optimal paths are monotone, so the model predicts no cyclical discounting under loss aversion. The comparison with Popescu and Wu (2007) in Section 3.3 of the paper and the robustness results of later sections (heterogeneous markets, non-linear reference effects) build on these statements.

The paper's results are proved on paper; none is formalized. The mission produces a machine-checked model of a non-smooth, two-dimensional dynamic program defined directly as a supremum over price sequences, the reduction of its steady states to smooth one-dimensional bounds, and the convergence theorem.

Difficulty

Both the per-period profit (through the kink at $p=r$) and the state transition (through $\min(m_{t-1},p_t)$) are non-smooth, so neither the Euler equation nor standard concavity arguments for the value function apply directly. The Bellman objective need not be concave in the price, and the value function is not differentiable on the diagonal $m=p$. Supermodularity of $\pi$ yields monotone optimal policies only within a region where the minimum price stays fixed, and showing that the state never leaves its initial region (Proposition 2) is itself a comparison of optimal paths against steady states. Existence of an optimal path is needed in its own right, because the value function is a supremum over an infinite-dimensional set.

Formalization scope

All declarations live in PeakEndPricing.Convergence. Conventions fixed in Lean:

• A price path is a sequence $q:\mathbb N\to\mathbb R$ with $q(n) = p_{n+1}$; $p_0$ is the initial last price. minPrice m0 q n is $m_n$ and refPrice at index $n$ is the reference price $r_{n+1}$ faced by $q(n)$.
• $J$ and the value $J^\nu_m$ of the smooth Problem (8) are suprema over sequences in $[0,\bar p]$ of tsums, never "a solution of the Bellman equation". On the domain of the theorems all series converge and the families are bounded, so the junk values of ⨆ and ∑' are not reached.
• Steady states of (7) and (8) are optimal constant paths; equations (11) and (12) appear only as conclusions.
• The profit is defined by (4)–(5); $\pi = \min(\pi_\lambda,\pi_\gamma)$ is part of Lemma 2, not a definition.
• Explicit hypotheses the paper uses implicitly: $\pi_0$ is differentiable at every point of $\mathbf P$ (for $\pi_0'$ in (9)–(12)); $m_0,p_0\in\mathbf P$ and $m_0\le p_0$ (the state space, p. 12); $s$ and $S$ are given roots in $\mathbf P$ of (9) and (10), and $p^{**}_\lambda(m)$ is represented as a root in $\mathbf P$ of (12).
• "The optimal path": the paper treats the optimal policy as single-valued. The goal asserts existence of an optimal path and states monotonicity and convergence for every optimal path; the claims and Proposition 2 are likewise stated for every optimal path.
• Correction: the regions $\overline{\mathbf R}_{1a}$ and $\overline{\mathbf R}_{1b}$ printed on p. 11 have their inequalities swapped relative to their use in the proofs of Claims 1–2 and on p. 14. Claims 1 and 2 are stated with explicit inequalities, $m_0\le p_0\le p^{**}_\lambda(m_0)$ and $p_0\ge p^{**}_\lambda(m_0)$, and the regions are not defined.
• Monotonicity ("increasing", "monotonically") is weak throughout. The "in particular" sentence of Proposition 1 is read as comparative statics of the steady-state price p**_λ(m) for a fixed m ∈ R_1 (the reading of its proof on p. 45). Corollary 1 is not formalized.

A goal stated without the existence of an optimal path would hold vacuously if no path attained $J$; existence is therefore part of the goal. Contributions are welcome on general infrastructure that is reusable beyond this mission: existence of optimal paths for discounted problems over compact action sets, the principle of optimality for sequence formulations, and Topkis-type monotonicity of optimal paths for supermodular objectives.

Selected references

• J. Nasiry and I. Popescu, Dynamic Pricing with Loss Averse Consumers and Peak-End Anchoring, INSEAD Working Paper 2009/20/DS/TOM, 2009; Operations Research 59(6), 2011. https://doi.org/10.1287/opre.1110.0952
• I. Popescu and Y. Wu, Dynamic Pricing Strategies with Reference Effects, Operations Research 55(3):413–429, 2007. https://doi.org/10.1287/opre.1070.0383
• D. Kahneman, B. L. Fredrickson, C. A. Schreiber and D. A. Redelmeier, When More Pain Is Preferred to Less: Adding a Better End, Psychological Science 4(6):401–405, 1993. https://doi.org/10.1111/j.1467-9280.1993.tb00589.x
• A. Tversky and D. Kahneman, Loss Aversion in Riskless Choice: A Reference-Dependent Model, Quarterly Journal of Economics 106(4):1039–1061, 1991. https://doi.org/10.2307/2937956
• G. Kalyanaram and R. S. Winer, Empirical Generalizations from Reference Price Research, Marketing Science 14(3):G161–G169, 1995. https://doi.org/10.1287/mksc.14.3.G161
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Pricing while learning demand

A vendor holding a finite stock of a product must set prices over time without knowing how many customers will come. Each price does two things: it earns revenue now, and through the sales it generates it reveals information about demand that improves future prices. This tension between earning and learning is central in revenue management with demand uncertainty, in retail markdown pricing, and in online selling. Optimal Bayesian policies for such problems are characterized by a Hamilton–Jacobi–Bellman equation that has no closed-form solution, so practice relies on heuristics, and the question is which heuristics come with guarantees.

Farias and Van Roy introduced decay balancing and proved that, for exponentially distributed reservation prices and a Gamma prior on the arrival rate, it earns at least one third of the optimal expected discounted revenue, uniformly over all problem parameters (V. F. Farias, B. Van Roy, Dynamic Pricing with a Prior on Market Response, Operations Research 58(1):16–29, 2010, doi:10.1287/opre.1090.0729). They describe it as the first heuristic for problems of this type with a uniform performance guarantee. This mission formalizes that guarantee and the chain of results leading to it. The source is the authors' manuscript of January 20, 2009 (MIT DSpace); its printed page numbers coincide with the PDF page numbers, and all theorem and page numbers below refer to it.

The model

Customers arrive according to a Poisson process with rate $\lambda$. Each has an independent reservation price with density $f$ and tail $\bar F(p) = 1-F(p)$; a customer facing price $p$ buys one unit if it is available and $p$ is at most his reservation price, and otherwise leaves. The hazard rate is $\rho(p) = f(p)/\bar F(p)$. Assumption 1 (p. 5) asks that $f$ be differentiable with support $\mathbb R_+$ and that $\rho$ be non-decreasing. The exponential law with mean $r$ has $\bar F(p) = e^{-p/r}$.

The vendor starts with $x$ units and a Gamma prior on $\lambda$ with shape $a$ and rate $b$ (density $b^a\lambda^{a-1}e^{-\lambda b}/\Gamma(a)$, mean $\mu(z) = a/b$). After $n_t$ sales the posterior is Gamma with $a_t = a+n_t$ and $b_t = b+\int_0^t\bar F(p_s)\,ds$, so the state is $z = (x,a,b)$. A policy $\pi(x,a,b)\ge0$ sets the price; the expected discounted revenue at rate $\alpha>0$ is

$$J^\pi(z) = E_{z,\pi}\Big[\sum_{k:\,t_k\le\tau_0}e^{-\alpha t_k}p_{t_k-}\Big],\qquad J^*(z) = \sup_\pi J^\pi(z),$$

the supremum over all measurable non-negative policies. With $\lambda$ known, the same problem has value $J^*_\lambda(x)$. Assumption 2 (p. 9) asks that $J^*_\lambda(x)$ be differentiable in $\lambda$.

Decay balancing uses the approximation $\tilde J(z) = E[J^*_\lambda(x)]$, $\lambda\sim\mathrm{Gamma}(a,b)$, and posts the price $\pi_{\rm db}(z)$ solving the balance equation (5), p. 13,

$$\frac{\bar F(\pi_{\rm db}(z))}{\rho(\pi_{\rm db}(z))}\,\mu(z) = \alpha\tilde J(z).$$

The optimal price $\pi^*(z)$ solves the same equation with $J^*(z)$ in place of $\tilde J(z)$. The constant

$$\kappa(a) = \frac{a\Gamma(a)}{\Gamma(a+1)-\Gamma(a+1,a)+a\Gamma(a,a)},\qquad \Gamma(s,y) = \int_y^\infty t^{s-1}e^{-t}\,dt,$$

measures the cost of uncertainty for a prior of shape $a$.

Formalization targets

Goal: Theorem 3 (p. 24)

For exponential reservation prices with mean $r>0$, every $\alpha>0$, $x>1$, $a>0$, $b>0$:

$$J^*(z)<\infty\qquad\text{and}\qquad \frac{J^{\pi_{\rm db}}(z)}{J^*(z)}\ \ge\ \frac13 .$$

Milestones

In attack order:

1. Known-rate value. Lemma 2: $J^*_\lambda(x)$ is increasing and concave in $\lambda$.
2. Bounds and well-posedness. Lemma 3 gives $J^*\le\tilde J\le J^*_{\mu(z)}(x)\le\bar F(p^*)p^*\mu(z)/\alpha$. Lemma 4 says the balance equation has a unique solution. Lemma E.6(2), with Theorems E.1–E.2, says the balance-price policy $\pi^*$ is optimal.
3. Normalizations. Lemma 5 rescales the discount rate and Lemma 10 rescales the mean reservation price.
4. No-learning comparison. Lemmas 7 and 8, and Theorem 1: $J^{nl}(z)\ge J^*_{a/b}(x)/\kappa(a)$.
5. Quality of the approximation. $1\ge J^*(z)/\tilde J(z)\ge1/\kappa(a)$, and $\kappa$ is decreasing.
6. Prices and revenues. Corollary 1: $1/(1+\log\kappa(a))\le\pi_{\rm db}/\pi^*\le1$. Lemma 9: $J^{ub}\ge J^*$. Theorem 2: $1/(1+\log\kappa(a))\le J^{\pi_{\rm db}}/J^*\le1$.
7. Inventory. Lemma 12: $J^*(x,a,b)\le2.05\,J^*(x-1,a,b)$ for $x>1$, $a>1$.

Significance

Theorem 2 gives a guarantee that depends only on the coefficient of variation $1/\sqrt a$ of the prior. Theorem 3 removes even that dependence for exponential reservation prices: whatever the inventory, prior, discount rate and price scale, decay balancing loses at most a factor of three. The analysis also yields reusable facts about Bayesian pricing: knowing the rate helps ($J^*\le\tilde J$), the decay-balance characterization of optimal prices, and comparison with a vendor who does not learn.

All results are proved in the source, using Dynkin's formula, an HJB verification argument (Appendix E) and a coupling of sales processes. None of them is machine-checked. The mission asks for a formal development of the known proofs.

Difficulty

The obvious route to Theorem 3 would chain Theorem 2 at the initial state. That fails because $\kappa(a)$ blows up as $a\to0$, so for a diffuse prior Theorem 2 gives no constant bound. The paper instead compares the two systems only up to the first sale, after which the shape parameter is at least $a+1>1$. This needs two things: a coupling in which the optimal system never sells first, and Lemma 12, which bounds the value of one extra unit without a decreasing-returns property in $x$ (none is known). Lemma 12 itself rests on a numerical inequality involving the Lambert $W$ function.

At the foundational level, neither Mathlib nor the platform has a counting process whose intensity is a random rate times a state-feedback price. Defining $J^\pi$ and $J^*$ faithfully is part of the mission.

Formalization scope

• Sales process. The process is built exactly in the b-clock. Given $\lambda$, sales are a rate-$\lambda$ Poisson process in the variable $b$, so $\lambda\sim\mathrm{Gamma}(a,b)$ and i.i.d. $\mathrm{Exp}(1)$ clocks $E_j$ give the $b$-values of the sales, $B_{j+1} = B_j + E_{j+1}/\lambda$. The real-time length of each stage is $\int d\beta/\bar F(\pi(\cdot,\beta))$.
• Values. Revenue is the sum over sales of the discounted pre-sale price (p. 6; the compensated-integral form of p. 7 is equal to it). Values and suprema live in $[0,\infty]$. $J^*$ and $J^*_\lambda$ are suprema over policies; they are never defined by the HJB equation or by the Lambert-$W$ formula (2). Such a definition would trivialize the mission and is ruled out.
• Policies. Policies are non-negative, measurable in $(a,b)$, and Markov in $z$. $\pi^*$ and $\pi_{\rm db}$ are the balance prices of p. 13, not "some optimal policy".
• Prior and normalizations. The prior is a single Gamma, the case of §6; $b$ is a rate. The general statements carry Assumptions 1 and 2. Statements are made for general $\alpha>0$ and $r>0$, as p. 18 claims, not under the normalizations $\alpha = e^{-1}$, $r = 1$.
• Ratios. Ratio bounds are stated multiplicatively, together with finiteness of $J^*$. This rules out the vacuous reading $J^* = \infty$.
• Added hypotheses and corrections.
  • Lemma 4 is false as printed at $x = 0$ ($\tilde J = 0$ while $\bar F/\rho>0$), so $x\ge1$ is added. Its location claim $p\ge p^*$ (proof, p. 35) is included.
  • Corollary 1 needs $x\ge1$, because the prices are undefined at $x=0$.
  • The logit halves of Corollary 1 and Theorem 2 are not stated: the logit family is never defined, contradicts Assumption 1, and comes with the rounded constant 1.27.
  • Lemma 9 uses general $\alpha$ where p. 21 has $\alpha = e^{-1}$.
  • Lemma 2's "increasing" is strict for $x\ge1$.
  • Appendix E is represented by Lemma E.6(2), p. 47: the balance-price (greedy) policy attains $J^*$. The if-and-only-if of Theorem E.2 over all policies is not stated, since the generator $H^\pi$ is not formalized.
• Not included. The integrated form of Lemma 11 (the first-sale coupling bound) is not a milestone; it is the natural next target. Lemma 6, Appendix D and the Lambert-$W$ identities are out of scope.

Reusable pieces are the Gamma–Poisson sales process in the b-clock, the incomplete Gamma function, and the known-rate pricing problem. Proofs of any milestone, of the p. 6 revenue identity, and of Assumptions 1–2 for the exponential law are welcome.

Related platform work in other models: Gallego–van Ryzin known-demand pricing (GVRPricing), Talluri–van Ryzin (RevenueManagement), Bitran–Caldentey (PricingRM.DetHeuristic), and the Bayesian bounds of Satia–Lave (SatiaLave.Bayes).

Selected references

• V. F. Farias, B. Van Roy, Dynamic Pricing with a Prior on Market Response, Operations Research 58(1):16–29, 2010. https://doi.org/10.1287/opre.1090.0729 (manuscript of January 20, 2009, MIT DSpace: https://dspace.mit.edu)
• G. Gallego, 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
• V. F. Araman, R. Caldentey, Dynamic Pricing for Nonperishable Products with Demand Learning, Operations Research 57(5):1169–1188, 2009. https://doi.org/10.1287/opre.1090.0669
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. https://doi.org/10.1007/978-1-4684-9477-8

Motivation

Many large optimization problems arising in networked control, smart grids, distributed estimation and resource allocation have a separable objective with coupled affine constraints: $N$ agents each own a variable $x_i$ and a private cost $f_i$, and only a linear constraint $\sum_i A_ix_i=b$ ties them together. Distributed algorithms for such problems let each agent solve a small local problem and exchange only a few aggregated quantities. For convex problems the standard method is the alternating direction method of multipliers (ADMM), which converges at a linear rate; for nonconvex problems ADMM can diverge (Houska, Frasch and Diehl give a two-variable example in §2 of their paper).

Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton method), which combines the decoupled augmented-Lagrangian subproblems of ADMM with a coupled equality-constrained quadratic program borrowed from sequential quadratic programming (SQP). Their local convergence analysis (§7) rests on one stability result for the decoupled subproblems, Lemma 3, which this mission formalizes. Similar statements are classical for augmented Lagrangian methods: Bertsekas analyzes minimizers of augmented Lagrangians under perturbation of the multiplier (Constrained Optimization and Lagrange Multiplier Methods, 1982, Prop. 4.2.3), and Nocedal and Wright give a related analysis (Numerical Optimization, 2nd ed., 2006, Thm. 17.6).

Setting

Problem (1.1). Given $f_i:\mathbb R^n\to\mathbb R$, $h_i:\mathbb R^n\to\mathbb R^{n_h}$, $A_i\in\mathbb R^{m\times n}$ ($i=1,\dots,N$) and $b\in\mathbb R^m$,

$$\min_{x}\ \sum_{i=1}^N f_i(x_i)\qquad\text{s.t.}\qquad \sum_{i=1}^N A_ix_i=b,\qquad h_i(x_i)\le 0\ \ (i=1,\dots,N).$$

All $f_i$ and $h_i$ are twice continuously differentiable (the paper's standing assumption in §3). The multiplier of the coupling constraint is $\lambda\in\mathbb R^m$, that of $h_i(x_i)\le0$ is $\kappa_i\in\mathbb R^{n_h}$.

A KKT point $(x^*,\lambda^*,\kappa)$ is feasible, satisfies $\nabla f_i(x^*_i)+A_i^\top\lambda^*+\sum_j\kappa_{ij}\nabla h_{ij}(x^*_i)=0$ for every $i$, and has $\kappa\ge0$ with $\kappa_{ij}h_{ij}(x^*_i)=0$. It is regular if

• LICQ holds: the rows of $[A_1\cdots A_N]$ and the block gradients of the active constraints $h_{ij}(x^*_i)=0$ are linearly independent in $\mathbb R^{Nn}$;
• strict complementarity holds: $\kappa_{ij}>0$ on every active constraint;
• the second-order sufficient condition holds: $\sum_i d_i^\top\nabla^2[f_i+\kappa_i^\top h_i](x^*_i)d_i>0$ for every nonzero $d$ in the critical subspace $\{\sum_iA_id_i=0,\ \nabla h_{ij}(x^*_i)^\top d_i=0 \text{ on active }(i,j)\}$.

The decoupled subproblems. In step 1 of ALADIN, given the current primal and dual iterates $(x,\lambda)$, a penalty $\rho>0$ and positive semidefinite scaling matrices $\Sigma_i$, agent $i$ solves

$$\min_{y_i}\ f_i(y_i)+\lambda^\top A_iy_i+\frac\rho2\|y_i-x_i\|_{\Sigma_i}^2\qquad\text{s.t.}\qquad h_i(y_i)\le 0, \tag{3.2}$$

with $\|v\|_{\Sigma}^2=v^\top\Sigma v$. These problems are nonconvex in general and are solved to local optimality.

Formalization targets

Goal: Lemma 3 (p. 1117)

Let $x^*$ be a local minimizer of (1.1) with $(x^*,\lambda^*,\kappa)$ a regular KKT point, and let $\rho>0$ satisfy

$$\nabla^2\big[f_i+\kappa_i^\top h_i\big](x^*_i)+\rho\Sigma_i\succ 0\qquad(i=1,\dots,N).$$

Then for every sufficiently small ball $\mathcal N$ of radius $\varepsilon$ around the origin of $\mathbb R^{Nn}\times\mathbb R^m$ there are constants $\chi,\chi_1,\chi_2<\infty$ such that for all $(x,\lambda)$ with $(x-x^*,\lambda-\lambda^*)\in\mathcal N$ the problems (3.2) have local minimizers $y=(y_1,\dots,y_N)$, unique in $\{x^*\}\oplus\chi\mathcal N$, with

$$\|y-x^*\|\ \le\ \chi_1\|x-x^*\|+\chi_2\|\lambda-\lambda^*\| .$$

The constants are not specified: the goal asserts only the shape of the estimate, not values of $\chi_1,\chi_2$.

Milestones (steps of the paper's proof, p. 1117)

1. The Hessians $\nabla^2[f_i+\kappa'^\top h_i](\xi)+\rho\Sigma_i$ remain positive definite for $(\xi,\kappa')$ near $(x^*_i,\kappa_i)$.
2. At $(x,\lambda)=(x^*,\lambda^*)$, $x^*_i$ is a stationary point with multiplier $\kappa_i$ and a strict local minimizer of the $i$-th subproblem: $\xi_i(x^*,\lambda^*)=x^*_i$.
3. Near $(x^*,\lambda^*)$ the subproblems have locally unique local minimizers $\xi_i(x,\lambda)$ depending continuously differentiably on $(x,\lambda)$.
4. If $\chi_1>\|\partial_x\xi\|$ and $\chi_2>\|\partial_\lambda\xi\|$ at $(x^*,\lambda^*)$, then $\|\xi(x,\lambda)-\xi(x^*,\lambda^*)\|\le\chi_1\|x-x^*\|+\chi_2\|\lambda-\lambda^*\|$ locally.

Significance

Lemma 3 is the bridge between ALADIN and the local theory of SQP. Once the decoupled minimizers are known to exist, to be locally unique, and to stay within a linear distance of $x^*$, the full-step variant of ALADIN behaves locally like an inexact SQP method, and the paper derives its local quadratic convergence estimates (with exact Hessians and a suitably large $\mu$) from this. Without the lemma the local subproblems could jump between distant local minimizers of a nonconvex objective, and no local rate could be claimed.

The result is proved in the paper, in a short paragraph that delegates the main step to the regularity of the KKT point. No machine-checked version of this lemma, of the sensitivity theory of parametric nonlinear programs it rests on, or of ALADIN exists, as far as a search of the Prove2Me catalogue and Mathlib shows. Formalizing it means supplying the argument the paper leaves implicit: a parametric local-minimizer theorem for inequality-constrained problems under LICQ, strict complementarity and a second-order condition.

Difficulty

The obvious argument applies the implicit function theorem to the stationarity condition of (3.2), $\nabla f_i(y_i)+A_i^\top\lambda+\rho\Sigma_i(y_i-x_i)=0$. That works only without inequality constraints. With constraints, the local minimizer satisfies a KKT system involving the multipliers and complementarity, which is not a smooth equation; one has to fix the active set, use strict complementarity to show that it does not change nearby, and use LICQ of the active constraints to make the reduced KKT matrix invertible. The second difficulty is uniqueness: the implicit function theorem gives a unique KKT point near $(x^*_i,\kappa_i)$, but the lemma claims uniqueness among local minimizers within a ball in the primal variable alone, so the multipliers of any nearby local minimizer must be shown to lie near $\kappa_i$. Third, the hypothesis is the positive definiteness of $\nabla^2[f_i+\kappa_i^\top h_i]+\rho\Sigma_i$ on all of $\mathbb R^n$, not only on the critical cone; the subproblems inherit their second-order condition from it rather than from the SOSC of (1.1).

Formalization scope

Vectors are Fin n → ℝ with Mathlib's sup norm, blocks are indexed by Fin N, matrices are Mathlib Matrix over Fin index types, and $\lambda\in$ Fin m → ℝ. Gradients and Hessians enter through Fréchet derivatives (fderiv), with $d^\top\nabla^2g(z)d$ written fderiv ℝ (fderiv ℝ g) z d d. LICQ is stated as linear independence of the active gradients in $\mathbb R^{Nn}$. The "sufficiently small open set $\mathcal N$" is read as every ball of radius $\varepsilon\in(0,\varepsilon_0]$ in the sup norm of $\mathbb R^{Nn}\times\mathbb R^m$, with $\chi,\chi_1,\chi_2$ allowed to depend on $\varepsilon$ but not on $(x,\lambda)$; $y\in\{x^*\}\oplus\chi\mathcal N$ is read through the $x$-component, $\|y-x^*\|<\chi\varepsilon$. Local minimizers are local minimizers on the feasible set and are required to be feasible. The hypotheses $h_i\in C^2$ and $\Sigma_i\succeq0$ come from the paper's standing assumptions (§3 and Algorithm 2, step 1).

A trivializing formalization is ruled out: the goal keeps all four conclusions (local minimality, membership in the $\chi\varepsilon$-ball, uniqueness in that same ball, and the bound), since the bound alone is satisfied by $y=x^*$; and it quantifies over every small ball rather than asserting the result for one neighbourhood. The hypotheses are satisfiable: a sorry-free check with $N=n=m=n_h=1$, $f=0$, $h=-1$, $A=1$, $b=0$, $\Sigma=1$, $\rho=1$ is in the development.

Needed infrastructure: a parametric implicit-function argument for KKT systems with a fixed active set, persistence of LICQ and of strict complementarity under perturbation, and second-order sufficiency for inequality-constrained problems. These pieces are reusable well beyond this mission, for any sensitivity or local-convergence analysis of nonlinear programs (SQP, augmented Lagrangian, interior-point methods). Proofs of any milestone, alternative routes (for instance via Robinson's strong regularity), and general lemmas on second-order sufficient conditions are welcome.

Selected references

• B. Houska, J. Frasch, M. Diehl, An augmented Lagrangian based algorithm for distributed nonconvex optimization, SIAM J. Optim. 26(2), 1101–1127, 2016. https://doi.org/10.1137/140975991
• J. Nocedal, S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006. https://doi.org/10.1007/978-0-387-40065-5
• D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982, Proposition 4.2.3.
• S. M. Robinson, Strongly regular generalized equations, Math. Oper. Res. 5(1), 43–62, 1980. https://doi.org/10.1287/moor.5.1.43