All missions

Why market size changes prices

Two-sided intermediaries charge buyers and pay sellers while trying to match the two groups. A larger arrival stream on one side changes both the number of possible matches and the prices that clear the market. Chen and Hu study this in a model of buyers and sellers who arrive over time and may wait before requesting a match. Their market-size theorem concerns the deterministic fluid benchmark used to choose fixed prices for the dynamic system. This mission formalizes that theorem from the submitted manuscript, main text §6, rather than the performance of the waiting-adjusted policy itself.

The fluid benchmark matters because it supplies an interpretable price and quantity for each pair of arrival rates. When buyers become more numerous, the model predicts that both the buyer price and the seller payment rise. When sellers become more numerous, both prices fall. In either direction, more arrivals raise the maximum matching quantity and the fluid profit. These claims concern the same valuation and cost distributions as the rates vary, so they isolate the effect of market size.

The two-sided fluid market

Buyer valuations lie in $[\underline v,\bar v]$, with density $f^d$ and distribution function $F^d$. Seller costs lie in $[\underline c,\bar c]$, with density $f^s$ and distribution function $F^s$. Write $\bar F^d=1-F^d$. Buyer and seller arrival rates are $\lambda^d>0$ and $\lambda^s>0$, and the horizon has length $T>0$. A buyer accepts a fixed ask price $p$ when the valuation is at least $p$; a seller accepts a fixed bid price $w$ when the cost is at most $w$. Thus $\lambda^d\bar F^d(p)$ and $\lambda^s F^s(w)$ are the corresponding acceptance rates.

The buyer virtual value is $V^d(v)=v-\bar F^d(v)/f^d(v)$, and the seller virtual cost is $V^s(c)=c+F^s(c)/f^s(c)$. Assumptions 1 and 2 of the manuscript say these functions are weakly increasing on their respective supports. The supports overlap in the sense $\underline c\le\bar v$. The density assumptions ensure that the survival and cost distribution functions have inverse quantiles on $[0,1]$. For a candidate volume $\mu$, the virtual surplus is

$$V(\mu)=V^d\!\left(\bar F^{d,-1}\!\left(\frac{\mu}{\lambda^dT}\right)\right)-V^s\!\left(F^{s,-1}\!\left(\frac{\mu}{\lambda^sT}\right)\right).$$

The optimal fluid matching quantity $\mu^*$ is the largest $\mu$ in $[0,\min\{\lambda^dT,\lambda^sT\}]$ for which $V(\mu)\ge0$. The corresponding fixed prices are $p^*=\bar F^{d,-1}(\mu^*/(\lambda^dT))$ and $w^*=F^{s,-1}(\mu^*/(\lambda^sT))$.

The fluid program (D) permits any measurable nonnegative ask and bid price path $(\hat\pi^d_t,\hat\pi^s_t)$ on $[0,T]$ that clears the market at every time: $\lambda^d\bar F^d(\hat\pi^d_t)=\lambda^sF^s(\hat\pi^s_t)$. Its value $\bar J^*$ is the supremum of buyer revenue minus seller payments, integrated over the horizon. Proposition 1 states that the constant path $(p^*,w^*)$ attains this value and that $\bar J^*=(p^*-w^*)\mu^*$.

Formalization targets

The goal is Theorem 3, the eight weak comparisons of prices, volume, and fluid profit. For $0<\lambda^d_1\le\lambda^d_2$ with $\lambda^s$ fixed, it asserts

$$p^*_1\le p^*_2,\quad w^*_1\le w^*_2,\quad \mu^*_1\le\mu^*_2,\quad \bar J^*_1\le\bar J^*_2.$$

For $0<\lambda^s_1\le\lambda^s_2$ with $\lambda^d$ fixed, the two price inequalities reverse while the volume and profit inequalities retain their directions. The goal leaves the rates and the two distributions as variables, so it states the market-size result across all systems meeting the paper's assumptions.

The milestones follow the source's dependency structure: Proposition 1 identifies the fluid optimizer; the proof of Lemma S.5 notes that $V(\mu)$ decreases in $\mu$; Lemma S.5 establishes the volume and profit comparisons; and the two parts of the proof of Theorem 3 compare the fractions $\mu^*/(\lambda^dT)$ and $\mu^*/(\lambda^sT)$ served on the growing side. The paper's proofs are in the Supplemental Note, with related proofs in the Online Appendix.

What the result provides

The theorem gives directional predictions without differentiating optimal prices with respect to arrival rates. A platform comparing two otherwise identical markets can infer which way its fluid ask and bid prices move, whether it matches more units, and whether the benchmark profit increases. Proposition 1 also connects the optimization over time-varying paths to a fixed price pair, so the static claims apply to the entire feasible fluid program.

The result is proved in the manuscript; this mission asks for a machine-checked proof of the same statement. The formal development would make the inverse-quantile construction, attainment of the optimal volume, and the nonempty bounded fluid optimization problem explicit. Those objects can be reused in other two-sided pricing or matching models. This mission does not claim that the corresponding stochastic system has identical comparative statics; the manuscript itself focuses on the fluid regime in §6.

Where the proof is difficult

Increasing one arrival rate expands the feasible number of matches, but the two optimal prices do not follow from that fact alone. The buyer price depends on the fraction of buyers served, and the seller price depends on the fraction of sellers served. A growing side can have a larger matched volume yet a smaller matched fraction. The proof must control both quantities under the appropriate inverse distribution function. Profit also needs a comparison of two separate fluid optimization problems, rather than only a comparison of their candidate fixed-price formulas.

Formalization scope

The Lean model reuses the published bilateral-trade environment for the two positive densities, interval supports, cumulative distributions, and virtual values. The new definitions clamp both cumulative distributions to their supports so a price outside the support still has the correct acceptance probability. Inverse quantiles are supported level-set infima, used only at arguments in $[0,1]$. All rates and the horizon are positive; both densities are continuous on their supports; the virtual functions satisfy the paper's regularity assumptions; and $\underline c\le\bar v$. Density continuity is a disclosed addition needed for the asserted inverse-quantile and maximum properties.

The claims involving the value of (D) assume a nonnegative seller cost support. This disclosed domain correction puts the fixed seller price in (D), whose price paths take values in $\mathbb R_+^2$; the imported bilateral-trade environment itself permits negative supports. The virtual-surplus and served-fraction inequalities hold without this condition. Every feasible path is measurable, nonnegative on $[0,T]$, clears the market at every point of that interval, and has integrable buyer and seller revenue terms. The fluid value is defined as the supremum over those paths. It is never defined by Proposition 1's fixed-price identity, which would erase the optimization claim. The volume set is restricted to $[0,\min\{\lambda^dT,\lambda^sT\}]$, so its supremum has the source's intended domain. The source uses “increasing” and “decreasing” in the weak sense.

Useful contributions include lemmas showing the clamped distributions are monotone, their supported inverses have the stated identities, the candidate volume set has a greatest member, the fluid feasible set is nonempty and bounded above, and the two fraction comparisons. These are substantive mathematical obligations: no arbitrary inverse, empty feasible set, non-integrable path, or preassigned fluid value should satisfy the goal by a default value.

Selected references

• Y. Chen and M. Hu, Pricing and Matching with Forward-Looking Buyers and Sellers, submitted manuscript, SSRN 2859864, 2020; published in Manufacturing & Service Operations Management 22(4), 717–734. SSRN manuscript.
• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.4.1. Publisher.

Motivation

Many constrained optimization problems in operations research have objective and constraint functions that are continuous but not differentiable: maxima of finitely many smooth functions, value functions of inner optimization problems, piecewise-linear costs. For such problems the classical Karush–Kuhn–Tucker theory does not apply directly, and algorithms need a nonsmooth replacement for the condition "the gradient of the Lagrangian vanishes". R. Mifflin's report Semismooth and semiconvex functions in constrained optimization (IIASA RR-76-21, 1976; SIAM J. Control Optim. 15(6), 1977) supplies one. It introduces a point-to-set map $M$ built from Clarke's generalized gradients and shows, in §5, that $0 \in M(\bar x)$ is necessary for optimality of locally Lipschitz problems and, for a class of semiconvex functions, also sufficient as soon as a strictly feasible point exists. The map $M$ goes back to Merrill's fixed-point work on differentiable and convex problems; Mifflin's own algorithm for semismooth problems converges to points satisfying $0 \in M(\bar x)$, so the sufficiency result says when such points are actual minimizers.

This mission is the third of three on the report. Mission I treats pointwise maxima of compact families of smooth functions, mission II the chain rule for semismooth compositions.

Setting

Write $\mathbb R^n$ for Euclidean space with inner product $\langle\cdot,\cdot\rangle$. For $F:\mathbb R^n\to\mathbb R$, a point $x$ and a direction $d$, the generalized directional derivative is

$$F^0(x;d)=\limsup_{h\to 0,\ t\downarrow 0}\frac{F(x+h+td)-F(x+h)}{t},$$

and the generalized gradient is the set $\partial F(x)=\{g:\langle g,d\rangle\le F^0(x;d)\text{ for all }d\}$. When $\lim_{t\downarrow 0}[F(x+td)-F(x)]/t$ exists it is the directional derivative $F'(x;d)$; $F$ is quasidifferentiable at $x$ if $F'(x;d)$ exists and equals $F^0(x;d)$ for every $d$.

Let $X\subseteq\mathbb R^n$. $F$ is semiconvex at $x\in X$ with respect to $X$ (Definition 2) if (a) $F$ is Lipschitz on a ball about $x$, (b) $F$ is quasidifferentiable at $x$, and (c) $x+d\in X$ and $F'(x;d)\ge 0$ imply $F(x+d)\ge F(x)$. It is semiconvex on $X$ if this holds at every point of $X$. Convex functions and differentiable pseudoconvex functions are semiconvex.

The problem of §5 is to minimize $f(x)$ subject to $h(x)\le 0$, where $h(x)=\max_{1\le i\le m}h_i(x)$. A point is feasible if $h(x)\le 0$ and strictly feasible if $h(x)<0$; $\bar x$ is optimal if it is feasible and $f(\bar x)\le f(x)$ for every feasible $x$. The map $M$ is

$$M(x)=\begin{cases}\partial f(x) & h(x)<0,\\ \operatorname{conv}\{\partial f(x)\cup\partial h(x)\} & h(x)=0,\\ \partial h(x) & h(x)>0,\end{cases}$$

and $\bar x$ is stationary if $h(\bar x)\le 0$ and $0\in M(\bar x)$. In Lean these are genGrad, HasDirDeriv, QuasidiffAt, SemiconvexAt/SemiconvexOn, IsFeasible, IsOptimal, Mmap and IsStationary in the namespace MifflinSemismooth.Optimality; $F^0$ is the published ClarkeGradients.Shared.genDirDeriv.

Formalization targets

Goal: Theorem 9 (p. 20)

Suppose $f$ and $h$ are semiconvex on $\mathbb R^n$ and $0\in M(\bar x)$. Then

$$h(\bar x)>0\ \Longrightarrow\ h(x)\ge h(\bar x)>0\ \text{ for all }x,$$ $$h(\bar x)\le 0\ \Longrightarrow\ \bar x\text{ is optimal, or } h(x)\ge 0\text{ for all }x.$$

The first alternative says the problem is infeasible, the last that it has no strictly feasible point. The theorem carries no constants and holds for any constraint function $h$, not only a finite maximum.

Milestones

The proof uses, in order: a point with $0\in\partial F(\bar x)$ minimizes a semiconvex $F$ over $\mathbb R^n$ (p. 20); on the boundary $h(\bar x)=0$, the condition $0\in M(\bar x)$ yields $\lambda\in[0,1]$, $\bar g\in\partial f(\bar x)$, $\hat g\in\partial h(\bar x)$ with $\lambda\bar g+(1-\lambda)\hat g=0$ (p. 20); Proposition 1(b), $F^0(x;d)=\max\{\langle g,d\rangle:g\in\partial F(x)\}$ (p. 3); Theorem 8, for $F$ semiconvex on a convex $X$, $F(x+d)\le F(x)$ implies $F'(x;d)\le 0$ (p. 19); and, if $\lambda>0$, $\langle\bar g,x-\bar x\rangle\ge 0$ for every feasible $x$ (p. 21).

Companion results

Theorem 7 (p. 18): for locally Lipschitz $f,h$, an optimal point is stationary. Theorem 6 (p. 17): for locally Lipschitz $h_1,\dots,h_m$, $h=\max_i h_i$ is locally Lipschitz with $\partial h(x)\subseteq\operatorname{conv}\bigcup_{i\in A(x)}\partial h_i(x)$, where $A(x)=\{i:h(x)=h_i(x)\}$; semismoothness, semiconvexity and quasidifferentiability on $X$ pass from the $h_i$ to $h$, and in the last two cases the inclusion is an equality at points of $X$.

Significance

Theorems 7 and 9 together give a nonsmooth Karush–Kuhn–Tucker theory: for semiconvex problem functions with a strictly feasible point, stationarity in the sense of $M$ is equivalent to global optimality. For differentiable functions this recovers the sufficiency of the Fritz John conditions for pseudoconvex objectives and constraints (Mangasarian, Nonlinear Programming, Theorem 10.1.1); for convex functions it recovers the saddle-point characterization. Since Mifflin's algorithm produces stationary points, Theorem 9 is the certificate that turns its output into a global minimizer. Theorem 6 lets the constraint $\max_i h_i\le 0$ stand for a finite system $h_i\le 0$.

The results are proved in the report. None of them, and neither the notion of semiconvexity nor the map $M$, has a machine-checked proof on Prove2Me or in Mathlib as far as the platform search shows; Mathlib has no Clarke generalized gradient. The work is to formalize the known proofs, which also produces reusable facts about $\partial F$ (nonemptiness, compactness, the max formula) and about semiconvex functions on convex sets.

Difficulty

The case analysis of Theorem 9 is short; the weight sits in its ingredients. Theorem 8 is the delicate step. Semiconvexity constrains $F$ only along directions where $F'(x;d)\ge 0$, so it says nothing directly about a direction along which $F$ does not increase; and a mean value inequality along the segment from $x$ to $x+d$ ignores quasidifferentiability and does not determine the sign of $F'(x;d)$. Proposition 1(b) is an attainment statement for a sublinear function whose finiteness rests on the Lipschitz hypothesis, and it fails for the real-valued limsup without that hypothesis. The convex-combination step depends on $\partial f(\bar x)$ and $\partial h(\bar x)$ being nonempty and convex: the convex hull of a union of two sets need not consist of two-point combinations otherwise. Theorem 7 needs $M(\bar x)$ to be closed, which in the boundary case is a statement about the convex hull of two compact sets.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $F^0$ is a real limsup and equals $0$ when the difference quotient is unbounded; every statement therefore has a Lipschitz hypothesis at the points where $F^0$ or $\partial F$ is used, and semiconvexity includes "Lipschitz on a ball". $\partial F$ is the paper's support-set definition, not the hull of gradient limits. $F'(x;d)$ is a relation (HasDirDeriv), never a function with a default value, so Definition 2(c) cannot hold vacuously. "Semiconvex on $\mathbb R^n$" means with respect to $X=\mathbb R^n$. "max" is IsGreatest, which asserts attainment. Lipschitz constants are nonnegative reals, which is equivalent to the page's positive constants.

The goal, Theorems 7, 8 and 9 are stated for an arbitrary constraint function $h$; the paper's $h=\max_i h_i$ is the special case maxConstraint hs with $m\ge 1$, and Theorem 6 is the bridge. Theorem 9's hypothesis is $0\in M(\bar x)$ alone, without feasibility. Theorem 6(c) as printed asserts $\partial h(x)=\operatorname{conv}\bigcup_{i\in A(x)}\partial h_i(x)$ "for each $x\in\mathbb R^n$"; that is false when $X\neq\mathbb R^n$ ($h_1=-|x|$, $h_2=-2|x|$, $X=(1,2)$, $x=0$), so it is stated for $x\in X$. A formalization with the hull-of-limits $\partial$, a junk-valued $F'$, a feasibility hypothesis added to Theorem 9, or semiconvexity with respect to a smaller set would prove a different and weaker theorem, and is ruled out.

A complete development needs the basic theory of the generalized gradient (Proposition 1(a), (b)), a Lebourg-type mean value theorem for case analysis along segments, and the finite-max rule. These are reusable beyond this mission, by missions I and II of the series in particular. Proofs of the milestones in any order are welcome, as are proofs of Proposition 1(a) as an auxiliary lemma.

Selected references

• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, IIASA Research Report RR-76-21, December 1976, https://pure.iiasa.ac.at/id/eprint/524/ ; journal version: SIAM J. Control Optim. 15(6) (1977) 959–972, https://doi.org/10.1137/0315061
• F. H. Clarke, Generalized gradients and applications, Trans. Amer. Math. Soc. 205 (1975) 247–262. https://doi.org/10.1090/S0002-9947-1975-0367131-6
• O. L. Mangasarian, Nonlinear Programming, McGraw-Hill, 1969 (SIAM Classics reprint 1994). https://doi.org/10.1137/1.9781611971255
• G. Lebourg, Valeur moyenne pour gradient généralisé, C. R. Acad. Sci. Paris Sér. A 281 (1975) 795–797.
• B. N. Pshenichnyi, Necessary Conditions for an Extremum, Marcel Dekker, 1971.

Motivation

The paper of Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (2016) has an algorithmic headline. This mission concerns one of its finite graph lemmas, Lemma 2.9. The lemma translates a condition phrased separately for every connected component into a condition on three vertex sets. A reader of graph decompositions encounters both forms: components express what remains connected after deleting vertices, while a small fixed number of parts gives a compact way to state constraints on a partition. Lemma 2.9 identifies exactly when the two forms agree for the half-balance threshold. The same result appears again in the paper as Lemma 6.2, where the authors use it in a later section.

The result does not require a tree decomposition or a treewidth hypothesis. It holds for every finite graph. That generality makes it a useful standalone target: the definitions of deletion, connected components, and the weighted three-partition can be reused wherever graph separators are studied. The mission follows the published SIAM article, with printed page 328 for the main lemma and pages 363–364 for its restatement and the supporting combinatorial observation.

Setting

Let $G$ be a finite simple graph with vertex set $V(G)$. Let $S$ and $X$ be subsets of its vertices. The deleted graph $G\setminus X$ retains precisely the vertices outside $X$ and the edges joining them. Two remaining vertices are in the same connected component when a walk joins them without passing through any vertex of $X$. Write $C_X(u)$ for the vertex set of the component containing $u\notin X$. This interpretation follows the paper's notation on page 320.

A balanced $S$-separator is a set $X$ for which each component of $G\setminus X$ contains at most half the vertices of $S$:

$$|C_X(u)\cap S|\le\frac{|S|}{2}\qquad\text{for every }u\in V(G)\setminus X.$$

The paper introduces this phrase on page 321. Here balance is a property of $X$ relative to $S$; it imposes no bound on the size of $X$. The denominator counts all vertices of $S$, including any that lie in $X$.

A three-part partition of $V(G)\setminus X$ is a triple $(M_1,M_2,M_3)$ of pairwise disjoint sets whose union is $V(G)\setminus X$. A part may be empty. Two parts have no edge between them if no edge of $G$ joins a vertex of one to a vertex of the other. Since the graph is undirected, checking the three unordered pairs of distinct parts covers the requirement for every $i\ne j$.

Formalization targets

Lemma 2.9: balanced separators and three parts

The goal is the equivalence stated on page 328, also restated as Lemma 6.2 on page 363:

$$X\text{ is a balanced }S\text{-separator} \quad\Longleftrightarrow\quad \begin{gathered} V(G)\setminus X=M_1\mathbin{\dot\cup}M_2\mathbin{\dot\cup}M_3,\\ \text{no edge joins distinct }M_i,\\ |M_i\cap S|\le |S|/2\quad(i=1,2,3). \end{gathered}$$

The equivalence is the target, including both directions. It applies even when $S$ or $V(G)\setminus X$ is empty. It does not include a bound on $|X|$.

Lemma 6.3: three bounded sums

The main supporting result on page 363 says that nonnegative integers $a_1,\ldots,a_p$ with total $q$ and $a_i\le q/2$ can be divided into three classes, each with sum at most $q/2$. The milestone list also records the paper's merge inequality and its assertion that a component cannot cross between parts having no edge between them. These are the specific claims used in the published discussion of Lemma 2.9.

Significance

Lemma 2.9 lets a componentwise balance condition be represented by three sets whose coverage, disjointness, edge separation, and cardinalities can be inspected directly. It gives an exact equivalence, so the three-part formulation loses no balanced separators and introduces none that fail the original definition. That is the mathematical content needed when a later argument represents a separator by a bounded number of regions rather than by a list of all its components. The result is already proved in the 2016 paper; the open work in this mission is a machine-checked formalization of that known result and its cited supporting claims.

Formalizing the equivalence also establishes reusable interfaces for vertex deletion and component membership in a finite simple graph. A future development can state a separator condition using IsBalancedSSep, or use the three-part conclusion without redefining what a component of $G\setminus X$ means. The independent integer-partition lemma has uses whenever indivisible nonnegative weights, each no larger than half the total, must be grouped into three bounded classes. Nothing in that statement depends on graphs.

Difficulty

There may be arbitrarily many components of $G\setminus X$, although the conclusion permits only three parts. Simply assigning all components to one part can violate the half bound, while splitting a component between different parts may create forbidden edges. A component's weight is the number of its vertices in $S$, and those weights can be uneven or zero. The theorem has to accommodate all such patterns without changing the threshold $|S|/2$. In the converse direction, the absence of edges between the three parts must control entire walks, not only their first edge; ordinary connectivity in $G$ would allow a walk through $X$ and would describe the wrong components.

Formalization scope

The Lean development uses SimpleGraph V with V : Type, [Fintype V], and [DecidableEq V]. Vertex sets are Finset V. The shared walk-based AvoidReach G X u v requires every vertex on a walk to lie outside $X$, including both endpoints; avoidComp G X u collects the vertices reachable in this way. It is used only for $u\notin X$ when quantifying over components. This shared definition matches the paper's $G\setminus X$. The graph itself need not have decidable adjacency, since the statements concern propositions rather than computations.

Half bounds are written as $2c\le |S|$ or $2c\le q$ in natural-number arithmetic. This is equivalent to the paper's rational half bound and avoids any interpretation of natural-number division. The three parts may be empty, so $X=V(G)$ is a genuine boundary case. The set $S$ may meet $X$; the right-hand denominator remains $|S|$. The graph may have no vertices. There is no treewidth parameter or size condition on $X$: adding one would change Lemma 2.9 and can make its reverse implication false. Nor may components be computed using connectivity in the original graph, where paths through deleted vertices could merge them.

The required infrastructure is finite graph walks, finite sets, cardinalities, sums over finite index types, and the three original claims in the milestone list. The graph-component definitions and the integer grouping theorem are reusable beyond this mission. Contributions that prove any milestone or the full equivalence under exactly these conventions are in scope.

Selected references

• H. L. Bodlaender, P. G. Drange, M. S. Dregi, F. V. Fomin, D. Lokshtanov and M. Pilipczuk, A c^k n 5-approximation algorithm for treewidth, SIAM Journal on Computing 45(2):317–378, 2016. DOI: 10.1137/130947374.

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

Multivariate multipoint evaluation asks for the values $f(\alpha_0), \dots, f(\alpha_{N-1})$ of one polynomial $f \in \mathbb F_q[X_0, \dots, X_{m-1}]$ at $N$ points of $\mathbb F_q^m$. Kedlaya and Umans showed that this problem is equivalent to modular composition, the computation of $f(g(X)) \bmod h(X)$ for univariate polynomials, and that fast algorithms for it yield the fastest known algorithms for factoring univariate polynomials over finite fields (Kedlaya–Umans, Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X). Modular composition is the bottleneck of the factoring algorithms of von zur Gathen and Shoup (1992) and Kaltofen and Shoup (1998), so a near-linear multipoint evaluation algorithm translates directly into a faster factoring algorithm.

The paper gives two such algorithms. Section 4 works over any ring $\mathbb Z/r\mathbb Z$ and is not algebraic: it lifts the problem to the integers and reduces modulo many small primes. Section 6, the subject of this mission, gives an algebraic algorithm, using only ring operations, for fields of small characteristic. Its correctness rests on one identity, Lemma 6.1, which lets the evaluation of the $m$-variate $f$ at a point be read off from the evaluation of a single univariate polynomial $f^*$ at a related point of an extension ring.

Setting

Let $p$ be a prime and $\mathbb F_q$ a finite field of characteristic $p$. Fix integers $m \ge 0$ and $d \ge 1$. Let $h = p^c$ be a power of $p$ with $h > m^2 d$ (the paper takes the least such power), and let $P(W) \in \mathbb F_p[W]$ be a polynomial of degree $c$ that is irreducible over $\mathbb F_p$. Then:

• $K = \mathbb F_p[W]/(P(W))$ is a field with $h$ elements. Let $\eta$ be a primitive element of $K$, a generator of its multiplicative group, so $\eta$ has multiplicative order $h-1$.
• $R = \mathbb F_q[W]/(P(W))$, with $P$ viewed over $\mathbb F_q$. $P$ need not remain irreducible over $\mathbb F_q$, so $R$ is a ring containing $\mathbb F_q$ and $K$ but in general not a field.
• $\sigma : R \to R$, $x \mapsto x^h$, is a power of the Frobenius endomorphism; $\sigma^i$ is $x \mapsto x^{h^i}$. On $\mathbb F_q$ it is an automorphism, with inverse $\sigma^{-i}$.
• $E(Z) = Z^{h-1} - \eta \in R[Z]$ and $S = R[Z]/(E(Z))$. Every element of $S$ has a canonical representative, its remainder modulo the monic $E$, of degree less than $h-1$.

Three maps connect the problem to $S$:

• the lift $\varphi : \mathbb F_q^m \to S$ sends $\alpha = (\alpha_0, \dots, \alpha_{m-1})$ to the class of the polynomial $g_\alpha(Z) \in R[Z]$ of degree at most $m-1$ with $g_\alpha(\eta^i) = \sigma^{-i}(\alpha_i)$ for $i = 0, \dots, m-1$ (Eq. (6.1));
• the projection $\pi : S \to R$ sends an element with canonical representative $g(Z)$ to $g(1)$;
• the Kronecker substitution sends $f \in \mathbb F_q[X_0, \dots, X_{m-1}]$ to the univariate

$$f^*(Y) = f\big(Y, Y^h, Y^{h^2}, \dots, Y^{h^{m-1}}\big) \in S[Y].$$

In the Lean development these are K, R, h, ι (the inclusion $K \subseteq R$), sigma i ($=\sigma^i$), E, S, sigmaInv i ($=\sigma^{-i}$ on $\mathbb F_q$), gAlpha, phi, pi, gIter ($g_\alpha^{(i)}$) and fStar, in the namespace KedlayaUmans.FrobeniusLift.

Formalization targets

Goal: Lemma 6.1 (p. 19)

For every $f \in \mathbb F_q[X_0, \dots, X_{m-1}]$ with degree at most $d-1$ in each variable and every $\alpha \in \mathbb F_q^m \subseteq R^m$,

$$\pi\big(f^*(\varphi(\alpha))\big) = f(\alpha).$$

Milestones, in the order the proof uses them

1. Properties of $\eta$ (p. 18): $\eta$ has order $h-1$ in $R$, and $\eta^i - \eta^j$ is a unit of $R$ for $i \ne j$ in $\{0, \dots, m-1\}$.
2. Eq. (6.1) (p. 19): $\sigma^i(\sigma^{-i}(a)) = a$ for $a \in \mathbb F_q$; $\deg g_\alpha \le m-1$; $g_\alpha(\eta^i) = \sigma^{-i}(\alpha_i)$.
3. The Frobenius congruence (p. 19): $\eta$ is fixed by $\sigma$, and $(g(Z))^{h^i} \equiv \sigma^i(g)(\eta^i Z) \pmod{E(Z)}$ for every $g \in R[Z]$.
4. Eq. (6.2) (p. 19): with $g_\alpha^{(i)} = g_\alpha^{h^i} \bmod E$, $\deg g_\alpha^{(i)} = \deg g_\alpha$ and $g_\alpha^{(i)}(1) = \alpha_i$ for $i < m$.
5. No reduction (pp. 19–20): the canonical representative of $f^*(\varphi(\alpha))$ is $f(g_\alpha^{(0)}, \dots, g_\alpha^{(m-1)}) \bmod E$, and this remainder equals $f(g_\alpha^{(0)}, \dots, g_\alpha^{(m-1)})$ itself.

Significance

The result. Lemma 6.1 is the correctness half of Theorem 6.2: to evaluate $f$ at $N$ points one computes the $N$ lifts $\varphi(\alpha_k)$, evaluates the one univariate polynomial $f^*$ at all of them by fast univariate multipoint evaluation, and projects back with $\pi$. Since univariate multipoint evaluation runs in nearly linear time, the identity turns a multivariate problem into a univariate one at the cost of the degree growth $\deg f^* \le dm\,h^m$. Corollary 6.3 turns this into an operation count of $(dm+N)^{1+\delta}$ for every $\delta>0$, provided $m \le d^{o(1)}$ and the characteristic satisfies $p \le d^{o(1)}$.

Formalizing it. The lemma is proved in the paper; no machine-checked version is known to exist. This mission states it for the objects exactly as constructed in Section 6 (an explicit interpolant for $\varphi$, the canonical-representative projection for $\pi$) and splits its proof into the five steps above. The definitions of the rings $R$ and $S$, the Frobenius powers on a ring that is not a field, and the Kronecker substitution into a quotient ring are reusable for formalizing other uses of the Frobenius-lift technique, such as the Parvaresh–Vardy codes and their Guruswami–Rudra instantiation, which the paper names as the inspiration for this algorithm (§1.5, p. 6).

Difficulty

The obvious attempt is to treat $\pi$ as evaluation at $Z = 1$ and push it through $f^*$. This fails: $E(1) = 1 - \eta$ is a unit, not zero, so evaluation at $1$ does not factor through $S = R[Z]/(E)$, and $\pi$ is not a ring homomorphism. The identity holds only because the polynomial $f(g_\alpha^{(0)}, \dots, g_\alpha^{(m-1)})$ is already reduced modulo $E$, which requires both the degree bound $h - 1 \ge m^2 d$ and the fact that raising to the power $h^i$ does not raise the degree of $g_\alpha$ modulo $E$. The second fact depends on $\eta$ being fixed by $\sigma$ and on $\eta^{(h^i-1)/(h-1)} = \eta^i$. The equality $\deg g_\alpha^{(i)} = \deg g_\alpha$ further needs that $\sigma^i$ does not kill the leading coefficient in $R$, a ring with possible zero divisors. Finally, interpolation must happen in $R$, not a field, which is possible only because the nodes $\eta^i$ lie in the subfield $K$.

Formalization scope

• $\mathbb F_q$ is a type F with [Field F] [Fintype F] [CharP F p], $p$ a prime ([Fact p.Prime]). $P$ is a polynomial over ZMod p with [Fact (Irreducible P)]; $c$ is P.natDegree and $h$ is p ^ P.natDegree. $R$ is AdjoinRoot of $P$ mapped to F; $R$ is never assumed to be a field and $P$ is never assumed irreducible over F.
• The paper's $h$ is the least power of $p$ above $m^2 d$; the statements assume only m ^ 2 * d < h, which contains the paper's case. $d \ge 1$ is a hypothesis.
• "Primitive element" is IsPrimitiveRoot η (h - 1), equivalent to generating $K^\times$ since $|K| = h$.
• "Individual degrees $d-1$" means at most $d-1$: ∀ i, f.degreeOf i ≤ d - 1.
• Variables and points are indexed by Fin m, starting at $0$; $f^*$ substitutes $Y^{h^i}$ for $X_i$.
• $g_\alpha$ is the explicit Lagrange interpolant: Mathlib's Lagrange.basis over the field $K$ at the nodes $\eta^0, \dots, \eta^{m-1}$, mapped into $R[Z]$, with coefficients $\sigma^{-i}(\alpha_i)$. $\pi$ is the remainder modulo $E$ (AdjoinRoot.modByMonicHom) evaluated at $1$.
• Only correctness is formalized. The operation counts of Theorem 6.2 and Corollary 6.3, and the cost of finding $P$ and $\eta$, are out of scope.

A formalization that takes $\varphi(\alpha)$ to be any element satisfying (6.2), or defines $\pi$ as a ring homomorphism, would make the goal trivial or false; both are ruled out because $\varphi$ and $\pi$ are explicit definitions with no hypotheses attached, and (6.1) and (6.2) are milestones to be proved.

Infrastructure a full proof needs: the Frobenius on polynomial rings in characteristic $p$ ($g^{p} = \sigma(g)(Z^{p})$, cf. Mathlib's expand and map_frobenius_expand), Lagrange interpolation transported along a ring homomorphism from a field, degree bounds for MvPolynomial.eval₂, and reducedness of $R$ (from separability of $P$ over the perfect field $\mathbb F_p$). Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• K. S. Kedlaya, C. Umans, Fast polynomial factorization and modular composition, Dagstuhl Seminar Proceedings 08381, version of Aug. 31, 2008. http://drops.dagstuhl.de/opus/volltexte/2008/1777
• K. S. Kedlaya, C. Umans, Fast polynomial factorization and modular composition, SIAM J. Comput. 40(6), 2011. https://doi.org/10.1137/08073408X
• F. Parvaresh, A. Vardy, Correcting errors beyond the Guruswami–Sudan radius in polynomial time, FOCS 2005, pp. 285–294. https://doi.org/10.1109/SFCS.2005.29
• V. Guruswami, A. Rudra, Explicit capacity-achieving list-decodable codes, STOC 2006, pp. 1–10. https://doi.org/10.1145/1132516.1132518