Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Multi-agent scheduling studies a machine shared by parties with their own jobs and their own objectives. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model: agents and each own a set of jobs, and the schedule must serve both. The paper frames this within multiagent systems, where agents negotiate the use of a common resource over time, and its schedules are meant to support that negotiation: either the best schedule for one agent given what the other accepts, or the whole set of nondominated (Pareto-optimal) schedules. The paper classifies the complexity of the constrained problems for the classical regular objectives.
One of its polynomial cases concerns the number of late jobs on both sides: agent accepts schedules in which at most of its jobs are late, and agent minimizes the number of its own late jobs. For a single agent, minimizing the number of late jobs is solved by Moore's algorithm (Moore 1968), and a dynamic program of the Lawler–Moore type over jobs in due-date order solves related weighted versions (Lawler & Moore 1969). §7 of the 2004 paper adapts that dynamic program to two agents by tracking the number of late jobs of each agent separately.
There are jobs , all available at time . Job has a processing time , a due date , and an owner, agent or agent . A schedule is a sequence of all jobs processed on one machine from time without idle time or preemption; the completion time of is the sum of the processing times of and the jobs before it. Job is late if and early otherwise. denotes the number of late jobs of agent .
Given an integer , the problem asks for a schedule with (a feasible schedule) minimizing . An instance may have no feasible schedule at all.
The jobs are numbered in earliest-due-date (EDD) order, . A partial schedule of is described by its set of early jobs: the jobs of run first, in EDD order, each completing by its due date, and the other jobs of count as late. The table is the minimum completion time of the last early job over partial schedules of with at most late -jobs and at most late -jobs, and if there is none. It is computed by , at a negative index, and
when belongs to (with in place of when belongs to ), where if and otherwise.
For a feasible instance with jobs in EDD order, for some , and
is the optimal value of : some feasible schedule has exactly late -jobs, and every feasible schedule has at least .
A feasible instance has an optimal schedule whose early jobs come first, in EDD order, and whose late jobs come last.
For : if is finite, it is the minimum, attained, of over partial schedules of with at most late -jobs and at most late -jobs; if , there is no such partial schedule.
The theorem places among the polynomially solvable two-agent problems (Table 1 of the paper lists it as ), in contrast with , which the same paper shows binary NP-hard. Through the binary-search argument of §3.1, solving the constrained problem for every also yields the nondominated pairs of the corresponding Pareto problem.
The result is proved in the paper; to the knowledge of this mission it has no machine-checked proof. The mission produces a checked correctness proof of the table, including the boundary convention, which the printed text leaves incomplete (see below). Further welcome work: the complexity bound in an explicit cost model, and the weighted variant.
The table is defined over partial schedules, in which the jobs outside the early set are only counted as late, while the problem is posed over complete sequences, in which lateness is measured: a job declared late may finish on time once it is appended. The correctness of must bridge the two objects in both directions, and the bridge is the structural Lemma 7.1, which the printed proofs use without detail. Lemma 7.2 is an optimal-substructure claim: it requires that the early set of minimizing total processing time is also the right one to extend by , which holds only because of the EDD numbering. Finally, the printed boundary gives only ; the natural reading for makes Theorem 7.3 false, so the boundary must be read from the definition of , not from the display.
Fin n, 0-based, numbered in EDD order, with an owner label ag : Fin n → Agent; this follows the paper's single numbered list in §7 rather than separate index sets per agent. EDD order is the hypothesis Monotone d, ties allowed. Data are natural numbers.MooreLateJobs.Shared.completionTime (sequences without idle time) and late jobs the published MooreLateJobs.NumLate.lateSet (late iff ), reused as references with the data cast to .WithTop ℕ, with ⊤ for ; no large sentinel number is used. The boundary is for all , the value forced by the "at most" definition of ; a negative index gives ; early means , as in the recursion (the proof of Lemma 7.2 prints a strict "").Nat.find of the existence clause, which the goal asserts.Balanced truncation reduces a large control system to a small one by discarding the states that are both hard to reach and hard to observe. For linear systems "hard to reach" is measured exactly by the controllability Gramian : the minimal input energy needed to steer the system from to is . For bilinear systems, in which the input also multiplies the state, no such exact formula is known, and several papers have tried to describe the nonlinear controllability energy functional through state-dependent Gramians.
Gray and Mesko ([25] in the paper, 1998) and Condon and Ivanov ([11], 2005) stated that, for with sufficiently small, the gradient of is given by a state-dependent Gramian of the linearization, , and derived from this comparison inequalities between and the algebraic Gramian. Benner and Damm (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X) observed that this formula needs an integrability condition that is not automatic, and gave an explicit two-dimensional system for which it fails (Example 3.3, pp. 697–698). This mission formalizes that counterexample.
A bilinear control system with state and input is
with real matrices and ; write for the -th column of . The system is locally controllable if the pair is controllable, that is, the Kalman matrix has rank .
Linearizing the system at a state and the input gives a linear system whose input matrix has columns . Its controllability Gramian is the solution of the Lyapunov equation
When is stable, (3.9) has exactly one solution for every , and it is symmetric. The claim under test is
A vector field on an open set is integrable (a gradient field) if for some real function .
Example 3.3 is the single-input system (, ) with
and a real parameter . In Lean these are exA, exN ν and exb (with exB the matrix ), equation (3.9) is IsLinGramian, and controllability is IsControllable.
For every , with solving (3.9) for every : the pair is controllable, and for every there is no with
The goal refutes every potential , not only , so it does not depend on how is defined; it is exactly the statement that the field is not integrable on any punctured neighbourhood of the origin, which is how (3.8) is claimed.
The result. The example shows that the state-dependent Gramian of the linearization does not, in general, describe the controllability energy of a bilinear system through (3.8), even for a locally controllable system and arbitrarily close to the origin. As a consequence, the inequalities and derived in [25, 11] from (3.8) lose their justification, and the comparison of with the algebraic Gramian requires the different argument the paper develops in its later sections. The example is a minimal one: two states, one input, one coupling parameter.
Formalizing it. The counterexample is proved in the paper by a hand computation through Kronecker products, and that computation contains a sign slip (see below); a machine-checked version settles the claim independently of it. The result is proved in the paper and, to our knowledge, has not been formalized anywhere. The general derivative formula (milestone 2) is reusable for any parametric Lyapunov equation.
The obvious route is to compute the Jacobian of at one point and observe that it is not symmetric. Two steps of this route need care. First, is defined only implicitly, through (3.9) at every point, so its differentiability in , and that of its inverse, must be derived from the invertibility of the Lyapunov operator and of near the point. Second, passing from "the Jacobian of is not symmetric" to " is not a gradient" requires the symmetry of second derivatives of a function that is only assumed differentiable with gradient on a punctured ball; the regularity of is inherited from that of , not assumed. The goal is also not a statement about a single point: it must hold for every radius , so the asymmetry must be exhibited at points arbitrarily close to the origin, where it is of order .
Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the paper's indices are Fin m. In the goal the plane is EuclideanSpace ℝ (Fin 2) and the potential is required to satisfy HasGradientAt at each point of the punctured ball , with no further regularity.Matrix.inv, which returns at singular matrices; is invertible near the origin, and milestones 2–4 assume invertibility (or ) where they use it.Contributions welcome: proofs of the four milestones, in particular the smooth dependence of the solution of a Lyapunov equation on its right-hand side (milestone 2), which is general and reusable.
A finite-sum optimization problem asks for one vector that performs well across many component objectives. In empirical risk minimization, each component can represent the loss from one data point. A full gradient uses every component, whereas a stochastic gradient uses one component and can be much cheaper per step. The latter carries sampling noise, so a method must control that noise while moving toward the optimum. Allen-Zhu's Katyusha paper gives a direct accelerated stochastic method for this setting. Its strongly convex result, Theorem 2.1, bounds the expected objective error of a specified algorithm after a specified number of epochs.
The problem is relevant when the number of terms is large enough that a full gradient at every iteration is costly, but individual component gradients and proximal steps remain practical. Katyusha combines a periodically refreshed full gradient with individual component gradients. The paper's result concerns the actual returned snapshot of Algorithm 1, Option I, whose weighted averaging rule matters to the claim. Formalizing a generic noisy gradient method would leave the paper's central algorithmic guarantee unstated.
Let be differentiable functions, with . Their finite-sum objective is . A real-valued regularizer gives the composite objective
Each is convex and smooth: its gradient is Lipschitz in the Euclidean norm. The regularizer is strongly convex, with , in the paper's convention that the quadratic term has coefficient . The comparison point minimizes the full objective .
Algorithm 1 starts from and keeps three vectors: a snapshot , a proximal sequence , and another proximal sequence . In each epoch it computes . At a current point , it samples uniformly from and forms the gradient estimator
The algorithm then makes two proximal updates using and . Its next snapshot is a weighted average of the new values, with weights for . The iterates and persist between epochs. In the theorem's run the epoch length is , and , , and . The output after epochs is .
For every starting point and minimizer of , the target is the paper's two-case expected bound:
The expectation is over every independent uniform index sampled by the run. The two regimes meet at the threshold where the algorithm's minimum defining changes branch. The milestone list follows Lemmas 2.3–2.7 and the displayed one-epoch inequalities of Section 2.2. It includes the variance bound, the proximal estimates, and the two regime-specific epoch estimates that feed the final theorem.
The theorem gives an accelerated linear reduction of the expected composite-objective error under the paper's strong convexity assumptions. It identifies how the rate depends on component count , smoothness , strong convexity , and epoch count . The author also translates the result into an iteration-complexity statement and uses it as a basis for later reductions and generalizations in the paper. The objective-error theorem is the stable mathematical claim formalized here; the complexity paraphrase is outside this mission's Lean goal.
Allen-Zhu proved Theorem 2.1 in the paper. The Lean declarations in this proposal are targets with proof placeholders, not machine-checked proofs of Katyusha's convergence. Completing them would produce a checked account of the exact algorithm, its finite probability space, and the conditional inequalities for an epoch. The finite-sum and proximal-point definitions reused here are already published in the SAGA formalization; Katyusha's weighted snapshot and coupling statements require their own development.
The estimator is unbiased, but that fact alone does not give the claimed acceleration. Its variance depends on the snapshot and current point, and a direct descent estimate retains a variance penalty. The bound in Lemma 2.4 expresses that penalty through a smooth convex gap which can have either sign before it is combined with other terms. The two proximal sequences and the snapshot therefore have to be accounted for together. Across an epoch, the iterates are averaged with nonuniform weights, while and themselves are carried into the next epoch. Replacing the snapshot with the final value or with a uniform average changes the algorithm and the theorem.
The two rate cases also reflect different parameter values. When , is determined by a square root; above that threshold it is fixed at . A proof of only one branch would omit part of the source result. Treating the sampled indices as a single arbitrary path would ask for a false pathwise guarantee, whereas stating the result for a favorable path would lose the expectation bound.
Vectors are EuclideanSpace ℝ (Fin d) and component indices are Fin n, translating the paper's one-based to a zero-based finite type. The goal fixes as Algorithm 1 does; the conditional one-epoch statements admit any positive . The number of epochs can be zero, in which case the output is the initial snapshot. The objective is real-valued. Thus may be nondifferentiable but does not include extended-valued indicator functions. The component gradient fields are required to be the actual gradients of their functions, and the comparison point minimizes , not merely .
A proximal map is an explicit argument constrained, for every , to minimize the proximal objective of the given . The run computes the paper's two proximal updates with that map. The expectation is the finite uniform average over all sequences, equivalent to independent uniform samples. It never quantifies over a convenient sequence. These links prevent a vacuous or unrelated encoding of the method.
The paper writes both rates using . Its Section 2.2 bounds yield the concrete coefficient in the square-root regime and in the regime; these are the expressions in the Lean goal. For Case 1 the rate is represented by division by , a positive denominator. For Case 2 it is . The statement retains both conclusions at their stated boundary. The one-step lemmas average only a fresh sampled index with the current state fixed, and the epoch statements average the current epoch's indices.
The development needs finite sums and finite expectations, Euclidean smooth and strong convexity facts, proximal minimizer inequalities, and algebra of the weighted snapshot. The finite-sum objective, averaged gradient, proximal-point predicate, and finite index expectation are shared definitions; the Katyusha run, progress value, potential, and epoch inequalities are specific to this algorithm. Contributions proving the milestone statements, establishing existence and uniqueness of the proximal map under these assumptions, or improving reusable proximal and finite-expectation lemmas are within scope.
Many objective functions in engineering design, Chebyshev approximation and game-theoretic planning are extremal-valued: they are the pointwise maximum or minimum of a family of smooth functions, . Such a function is typically not differentiable at points where two or more members of the family are active, so gradient methods do not apply directly. In 1976 R. Mifflin introduced the class of semismooth functions to identify which nondifferentiable functions can be minimized by bundle-type and line-search methods whose convergence relies only on generalized gradients (Mifflin, IIASA RR-76-21; journal version SIAM J. Control Optim. 15 (1977), doi:10.1137/0315061). For that class to be useful it must contain the functions that actually occur in practice. §3 of the report shows that it contains min–max objectives, which is the content of this mission.
Background: F. H. Clarke defined the generalized gradient of a locally Lipschitz function and computed it for max functions (Clarke, Trans. AMS 205 (1975), Theorem 2.1). A. Feuer's Columbia dissertation (1974) proved the formulas of Theorem 1 below under stronger assumptions and a result close to semismoothness, from which Mifflin's proof of Theorem 2 is adapted (report, Remark, p. 8). Mifflin's notion of semismoothness was later extended to vector-valued maps by Qi and Sun (1993), where it became the standard hypothesis for superlinear convergence of nonsmooth Newton methods.
Let carry the Euclidean inner product and norm , and let . is Lipschitz on a set if for all . Clarke's generalized directional derivative is
and the generalized gradient is . When exists it is the directional derivative ; is quasidifferentiable at if exists and equals for all .
is semismooth at (Definition 1) if it is Lipschitz on a ball about and, for each and all sequences , with , and , the real sequence has exactly one accumulation point. is semiconvex at with respect to (Definition 2) if it is Lipschitz on a ball about , quasidifferentiable at , and , imply .
In §3, is open, is a topological space, is sequentially compact, , and satisfies either (d) on or (d′) on . The active set is , and is the generalized gradient of at . Hypotheses (a)–(c) ask that be continuous on , Lipschitz in uniformly in , and that be upper semicontinuous on ; (e) and (e′) ask that exist and equal , respectively .
If (a) holds, has the max form (d) or the min form (d′), is differentiable on for each , and is continuous and bounded on , then
in the max form, and in the min form.
Theorem 2 places every min–max objective with continuously differentiable data inside the class on which Mifflin's descent algorithms, and the bundle methods that followed them, are proved to converge. Theorem 1 is the generalized-gradient form of Danskin's theorem, the standard tool for computing subgradients of max functions. Theorem 3 shows that semiconvexity, unlike pseudoconvexity, survives pointwise maximization, which is what the sufficient optimality results of §5 of the report need.
All of these results are proved in the report and in the literature since 1977; none is open. As far as is known, none of them has a machine-checked proof. Mathlib has Fréchet derivatives and convex analysis but no Clarke generalized gradient calculus, no semismoothness and no Danskin-type theorem. A formalization produces those pieces as reusable infrastructure, and checks the report's statements under exactly stated hypotheses. One printed claim already needs a correction (see Formalization scope).
Lipschitz continuity of and the inequality follow from Theorem 1 and the upper semicontinuity of . The difficulty is the matching lower bound: semismoothness asks that the slopes along an arbitrary sequence , with arbitrary , not accumulate strictly below . A generalized gradient of at is only a convex combination of gradients of the active functions at , and the active set can change discontinuously along the sequence. Upper semicontinuity of alone does not prevent this; the function (p. 6) is Lipschitz and has an upper semicontinuous but is not semismooth at . The argument has to use the continuity of jointly in and the compactness of . Theorem 1 itself needs a mean value theorem for Lipschitz functions and a compactness argument over the active set, neither of which is in Mathlib in this form.
is EuclideanSpace ℝ (Fin n). is the published ClarkeGradients.Shared.genDirDeriv, a real limsup; every statement assumes the Lipschitz hypothesis of the page at the points where or is used, so that this limsup is the true value. is the support-set definition of the page, not Clarke's convex hull of gradient limits; the two coincide by Proposition 1(c), which is not assumed. is a relation (HasDirDeriv), so "" means "exists and is nonnegative". "Exactly one accumulation point" is a unique cluster point, not convergence. "" is read as "positive and tending to ", as the report reads it in the proof of Lemma 2. "max" and "min" are attained extrema (IsGreatest, IsLeast), never suprema with default values.
is a given function constrained by (d) or (d′), not a supremum; this rules out the trivializing formalization in which is defined as ⨆ u ∈ U, f x u and takes the default value for an empty or unbounded family. (d) and (d′) force . The page's "for each either (d) and (e) or (d′) and (e′)" is read as one form on all of , as the proof of Theorem 2 treats it, and Theorem 1 is stated as two items. Hypothesis (c) is the sequential accumulation-point form in which Proposition 1(d) glosses upper semicontinuity.
The goal does not assume (b), (c), (e), (e′) or convexity of ; the report derives the first four from smoothness. The report claims (b) on all of , which fails for non-convex open (a bounded gradient gives a uniform Lipschitz constant only on convex sets). The corresponding milestone states (b) on balls contained in , which is all the proof needs.
The development needs Clarke's calculus for Lipschitz functions on (Propositions 1 and 2, a Lebourg mean value theorem), a Danskin-type theorem, and the regularity of functions. These are reusable well beyond this mission; a companion mission of the series covers Propositions 1(c), 2 and the chain rule. Contributions are welcome on any milestone, including alternative proofs of Theorem 1.
Nonlinear model predictive control (NMPC) computes a feedback law by solving, at every sampling time, an optimal control problem that starts from the currently measured state. The control actually applied is the first control of that problem's solution. When the dynamics are fast relative to the time an optimizer needs, solving each problem to convergence is impossible, and the delay between measuring the state and applying the control degrades or destabilises the closed loop.
Diehl, Bock and Schlöder (SIAM J. Control Optim. 43(5), 2005) analysed the real-time iteration: a scheme that performs a single Newton-type iteration per sampling time and then moves on to the next problem. The scheme is the basis of widely used NMPC software (for example the ACADO toolkit and acados) and of much of the later theory on suboptimal and "anytime" MPC. The paper's Theorem 4.1 is the first contraction result for it; Theorem 5.1 bounds the price paid in closed-loop cost for not solving each problem to optimality.
A discrete-time system , , has states and controls . For and a state , the shrinking-horizon problem is
Its primal-dual vector is and its Lagrangian is
The projection drops the block .
A Newton-type method solves by steps , where is the KKT matrix with its Hessian blocks (and the terminal block) replaced by approximations, for instance those of the constrained Gauss–Newton method. The real-time iteration starts from a guess and, for , computes for , applies , lets the system evolve to , and sets .
The analysis uses a neighbourhood and its projections , norms on with and , two constants (the Hessian approximation error) and (a Lipschitz-type constant of ), the rates , and the ball .
Assume is twice continuously differentiable on , is continuous with bounded inverse on , the conditions (4.1a)–(4.1c) hold with , and . Then for
for
and the Newton-type iterates of started at converge to a stationary point with
No constant is chosen by the formalization: all of them are the paper's.
The proof has three parts (contraction, well-definedness, distance to the stationary points). The milestones are its steps: the gradient transition identity between consecutive problems; the block identity ; the one-step contraction; the recursion ; the lifting of a nearby point of to ; the contraction (4.7) of the Newton-type method on a fixed problem; and the convergence of those iterates to .
If moreover on , then , and for the loss is . The intermediate estimate (5.4), , is a separate item.
Theorem 4.1 says that a scheme which never solves any problem to convergence still produces iterates that contract at the rate of the underlying Newton-type method and approach the exact solutions of the problems along the closed loop, geometrically. It justifies the "one iteration per sample" design of real-time NMPC under explicit, checkable conditions on the Hessian approximation, and its constants are those of the classical affine-invariant Newton-type convergence theory, so it extends to Gauss–Newton and other approximations. Theorem 5.1 turns the contraction into a closed-loop performance guarantee: the suboptimality is quadratic in the first step, quartic for exact Newton.
The results are proved in the paper; none is formalized. A formal proof would supply the details the paper leaves implicit (that the segments used by the integral mean value theorem stay in the domains, that the ball around lies in ), would give a reusable Lean model of discrete-time optimal control problems with their KKT structure and shrinking-horizon projections, and would make the classical local contraction argument for Newton-type methods available for general norms.
Each single estimate is a variant of the textbook local convergence proof for Newton-type methods. The difficulty is that the real-time iteration changes the problem at every step: the next step is computed for a different, smaller problem at a different initial state, so the textbook argument does not apply as is. The proof needs two structural facts that tie consecutive problems together, the gradient transition along the undisturbed closed loop and the block identity of the Hessian errors, together with the compatibility of the norms with the projections. A second obstacle is well-definedness: the iterates must be shown to stay in regions where the hypotheses hold, which requires tracking the projections of through all shrinking spaces.
is a Euclidean space whose coordinates are indexed by (multiplier, state or control block, stage, component) for the stages ; is a restriction and its transpose the extension by zero. The gradient and Hessian are Mathlib's gradient and fderiv; the inverse is ContinuousLinearMap.inverse. The approximations of the stage Hessian blocks depend on (the paper's misprinted read as ), the terminal block may be approximated as in §2.2, and symmetry of the approximations is not required. The norms are a structure carrying the norm axioms and the two compatibility conditions. The real-time iterates follow the undisturbed closed loop. The hypotheses (4.1a)–(4.1c) are imposed at the points of where the paper's functions are defined, that is, for with ; no convexity of is assumed. Theorem 5.1 is stated with Euclidean norms on every , because its last step bounds by ; is the objective at the primal part of , not an infimum.
Mathlib's inverse is at a non-invertible operator and its derivative is at non-differentiable points; either junk value would make every step vanish and every bound trivial. The statements therefore require invertibility and twice continuous differentiability at the points of , keep the membership (4.2) as a conclusion, and pin as the limit of the Newton-type scheme started at , so it cannot be chosen after the fact. Degenerate norms are excluded by the norm axioms.
Some milestones add a hypothesis that Theorem 4.1 supplies internally: a segment , the ball around the starting point contained in , or for the abstract δ-recursion. Contributions welcome: proofs of the milestones, a sorry-free instance of the hypotheses for a linear-quadratic problem, and general lemmas on the integral mean value theorem for gradients in arbitrary norms.
Progressive hedging separates a stochastic optimization problem by scenario, solves those smaller problems, and coordinates their first-stage decisions through weighted aggregation and price updates. It is useful when the full extensive formulation is too large to solve directly. For stochastic mixed-integer programs, its iterates can provide feasible decisions, but a feasible cost alone does not reveal how far that cost is from the global optimum. A lower bound gives the missing comparison: the difference between a feasible cost and a valid lower bound is an optimality gap. Branch-and-bound methods also use lower bounds to discard regions whose best possible cost cannot improve the current solution. These are the reasons the authors seek a bound available during a progressive-hedging run, rather than only after convergence. Gade et al., author manuscript, §§1–3.
The paper establishes lower bounds for two-stage stochastic mixed-integer programs, extends them to scenario bundles, and studies their behavior computationally. The mission concerns the mathematical statement that the price vector produced at each completed iteration is eligible for a decomposed lower bound. The paper was published in Mathematical Programming in 2016; the theorem and page labels here follow the authors' SAND2013-9195J manuscript. Gade et al., author manuscript.
Let be a finite set of scenarios and let be their probabilities, with . A first-stage decision is made before the scenario is known. Its first coordinates are nonnegative integers; the others are unrestricted reals. It incurs cost and must satisfy . After scenario is observed, a second-stage decision incurs cost . Its first coordinates are nonnegative integers, and it must satisfy . The recourse matrix is common to all scenarios. The scenario feasible set contains pairs satisfying these restrictions for one . Gade et al., §2, pp. 3–5.
In the extensive scenario formulation, each scenario has a copy of the first-stage vector, and a common vector enforces implementability through . Its optimum is . Algorithm 1 starts with zero prices , solves unpenalized scenario problems, and at iteration computes and . Later scenario solves add both and to their objectives. Here is the algorithm's scalar parameter. Gade et al., Algorithm 1, p. 6.
For any scenario prices , define the decomposed dual value by
Proposition 1 states that prices with satisfy . The price invariant in §3.1 states that the update maintains this weighted zero sum. The mission's goal combines these source claims at every completed iteration of Algorithm 1:
The formal goal is the lower-bound inequality; the zero-sum statement and Proposition 1 are its two milestones. Gade et al., Proposition 1, p. 6, and §3.1, p. 7.
For a partition of the scenarios, a bundle has probability . A bundle subproblem uses one first-stage vector for its scenarios and second-stage weights . Proposition 3 gives the corresponding inequality when . The proposal also records the bundle price invariant and the resulting inequality at each completed bundled iteration as companion statements. Gade et al., §3.3, pp. 9–10.
The scenario bound turns each price vector into an independent set of optimization problems whose weighted values certify a lower bound on the original mixed-integer optimum. The bound does not require the scenario first-stage decisions to agree at that iteration. The bundle result gives the same kind of certificate when several scenarios are solved together. These are the paper's known results, not new open mathematical conjectures. Gade et al., §§3.1 and 3.3.
Formalizing them requires a reusable interface for finite-support stochastic mixed-integer models, their scenario feasible sets, implementability equations, price systems, and finite prefixes of both algorithms. It also separates the general price-feasibility inequality from the algorithmic invariant. The mission currently proposes statements with open Lean proofs; it does not claim a machine-checked proof of these paper results.
An iteration of progressive hedging solves scenario problems with a quadratic proximal term, while the lower-bound calculation uses scenario problems without that term. Their objective values cannot simply be identified. The relevant connection is the price vector: to apply Proposition 1 at an arbitrary iteration, its weighted zero-sum condition must follow from the actual aggregation and price-update rules. The bundle version adds normalization by , so every bundle must have positive mass and the bundle weights must cover the full scenario distribution. Gade et al., §§3.1 and 3.3.
Lean represents vectors as Fin n → ℝ, linear constraints componentwise, and the extensive formulation with the weighted implementability equation printed in (15). The dimensions satisfy and , as required by the paper's spaces . The finite scenario weights are positive and sum to one. The first integer coordinates are nonnegative; every remaining real coordinate is free. The paper's assumptions that the SMIP has an attained finite optimum and each is nonempty are explicit in the goal and Propositions 1 and 3. The scenario and bundle subproblem values, and , live in the extended reals: an unbounded-below subproblem retains rather than acquiring an arbitrary real infimum. Gade et al., §§2–3.
An algorithm run is a finite prefix through its last aggregation and price update, with exact minimizers recorded as conditions on its sequences; a stopping test truncates the prefix. The proximal term is the Euclidean sum of squared coordinate differences. No positivity condition on is added to the lower-bound statements, since the page does not require one for these claims. Bundles form a partition, but equal bundle sizes are not required for the inequalities. Algorithm 2's printed w^ν(i) at initialization and Σ_i P_β x^ν(β) at aggregation are read with bundle indices. A bundle recourse vector is represented as a function on all scenarios, with only its coordinates inside the bundle constrained or used.
The exact equations of the scenario model and runs prevent a trivial encoding that assumes dual feasibility or the desired bound as part of a run. Contributions to the model, the price invariants, the extended-real weak-duality arguments, and the bundle extension are all within scope. The paper's convexified limit result (Proposition 2), its cited Theorem 1, and multi-stage Algorithm 3 are outside this mission.
Reflected backward stochastic differential equations describe processes that must remain above a prescribed obstacle. El Karoui, Kapoudjian, Pardoux, Peng and Quenez connect that probabilistic construction to a parabolic partial differential equation with an obstacle in their 1997 paper. A representation by a stochastic process is useful only if the associated differential equation identifies a definite function. The comparison result in Theorem 8.6 supplies that identification: within a specified growth class, two viscosity solutions cannot disagree. This mission isolates that deterministic uniqueness statement. The companion existence and stochastic representation result is Theorem 8.5 of the same paper.
Fix a terminal time and a spatial dimension . At time and point , the drift is a vector and the diffusion coefficient is a matrix. Both are continuous and Lipschitz in uniformly over . A continuous terminal payoff has at most polynomial growth. The continuous generator depends on a scalar value and a vector ; it has polynomial growth at and is Lipschitz in . The continuous obstacle has a polynomial upper bound and satisfies .
Write . The associated second order spatial operator is . The obstacle problem asks for a function whose terminal value is and whose interior value obeys
A parabolic superjet or subjet at an interior point is a triple of a time slope, spatial slope and symmetric second order matrix that bounds the function locally above or below by the associated quadratic expansion, up to . These jets let a continuous function satisfy the differential inequality without having ordinary derivatives. A viscosity subsolution uses superjets and a terminal upper bound; a viscosity supersolution uses subjets and a terminal lower bound. A viscosity solution satisfies both definitions.
The goal is the paper's Theorem 8.6. Under the coefficient assumptions above and condition (27), every pair of continuous viscosity solutions with polynomial growth agrees on the entire closed time strip:
Condition (27) gives a continuous modulus for the change in between bounded spatial points, with argument and . The quantifiers include every radius , every bounded scalar argument, and every gradient vector . The milestone is Lemma 8.7, which controls the location and separation of the maximizers of the paper's doubled-variable function .
The theorem shows that the obstacle PDE has at most one solution in the natural class allowed by polynomially growing coefficients and payoffs. Together with Theorem 8.5, which identifies the reflected backward SDE value as a viscosity solution, and the growth estimate at the end of Section 8, it yields the paper's probabilistic representation of the unique solution. Theorem 8.6 alone asserts uniqueness, so it makes no existence claim.
The formal development provides reusable interfaces for parabolic jets, viscosity inequalities, the obstacle operator and uniform polynomial growth on a finite time strip. Those interfaces can serve other comparison theorems and other parabolic obstacle problems. The mathematical result is proved in the 1997 article; this mission asks for a Lean proof of its deterministic uniqueness statement. The proposal declares the theorem with a proof placeholder and includes the comparison lemma as an intermediate target.
The first obstruction is that the candidate solutions need only be continuous. Subtracting their PDE expressions directly would assume derivatives they may not possess. The paper instead uses viscosity jets, and its comparison argument invokes the theorem of sums from Crandall, Ishii and Lions' viscosity-solutions guide. The generator's spatial modulus must control a gradient argument that grows as the two spatial points approach each other. Lemma 8.7 provides the necessary separation limit for the maximizers. The argument also treats a polynomial growth class on all of , so a comparison confined to one fixed bounded ball would not establish the stated result.
Lean uses nonnegative real time and functions on represented by Fin d → ℝ. The terminal time and dimension are positive. Bounds with existential constants use the finite-dimensional sup norm, which is equivalent to the Euclidean norm in the paper. The displayed quadratic form, and are written by coordinate sums, so their signs, factor , and matrix order are exact. The obstacle is bounded only above in the data assumptions, exactly as condition (22) states. Condition (27) is imposed only on uniqueness, not folded into the definition of viscosity solution.
Jets are taken at through a one-sided little- bound in the relative neighborhood of the interior strip. The terminal equality comes from the two terminal inequalities; the viscosity tests impose no separate condition at . The printed text calls “symmetric nonnegative matrices,” but the proof of Theorem 8.6 uses arbitrary symmetric matrices produced by the theorem of sums. The formal definition therefore uses all symmetric matrices and records this correction for review.
The mission permits every continuous solution of polynomial growth. It does not restrict candidates to smooth, bounded or stochastic-representation functions. The companion reflected SDE construction, penalization limit and existence theorem are outside this mission's goal; the general stochastic interface Peng1990.SMP.Stochastic is listed as series context but is not imported by the deterministic statements. Useful contributions include the comparison proof, the lemma on doubled-variable maximizers, and reusable lemmas about jet transformations and the matrix trace inequality.
Benders decomposition solves an optimization problem in two groups of variables by fixing one group, solving the remaining subproblem, and turning what the subproblem's solution proves into a constraint, the Benders cut, on the fixed variables. In the classical method of Benders (1962) the subproblem is a linear program and the cut comes from its LP dual. Many problems that decompose naturally have subproblems that are not linear programs: scheduling, satisfiability, 0-1 and constraint programs. Hooker and Ottosson (Math. Program. 96, 2003) replaced the LP dual by the inference dual, the problem of inferring the strongest bound on the objective from the constraints, and obtained a Benders scheme in which any sound inference method produces cuts. This logic-based Benders decomposition has since become a standard technique for planning and scheduling problems that combine an assignment master problem with combinatorial subproblems.
The correctness of the generic scheme rests on two short theorems of the paper. Theorem 1 says that if every cut is valid, then each of the algorithm's three ways of stopping reports the right answer. Theorem 2 says that the algorithm stops when the fixed variables range over a finite set. This mission formalizes both theorems, together with the facts used in the proof of Theorem 1.
An optimization problem (1) has a domain , a feasible set and a real-valued objective ; its value is . Optimal values lie in : an infeasible minimization has value , an unbounded one , and the reverse holds for maximization. For propositions about , implies with respect to , written , if holds at every where holds. The inference dual (2) of (1) is
In Benders decomposition the variables are pairs with , , and problem (6) is over . Fixing at a trial value gives the subproblem (7), over , with inference dual (8): s.t. . A bounding function defines the cut . The cut satisfies
(B1) if every feasible of (6) satisfies , and
(B2) if , the value obtained in the subproblem dual.
The cuts generated so far form the master problem (9): s.t. for every cut , .
The generic Benders algorithm (Figure 1 of the paper) starts with and some . While the subproblem dual at has a feasible , it formulates with and adds its cut. If the master is then infeasible, it stops and reports (6) infeasible. Otherwise it takes an optimal solution of the master and repeats. When the loop exits, the optimal value of (6) is reported as .
In Lean, LogicBenders.Generic.Setting defines all of these objects: optVal, subVal, IsDualFeasible, ValidCut, masterLHS, IsMasterOptimal and MasterInfeasible, and a Run with the predicates IsRun, StopsAtWhile and StopsAtMaster.
Assume (B1) for every cut the run has added. Then three statements hold.
If (B1) and (B2) hold, is finite, and the subproblem dual is solved to optimality, then no run of the algorithm continues forever.
Lemma 3 (p. 20) gives a criterion for a 0-1 inequality to imply the branching clause (29). The §4 statement (p. 7) characterizes when a feasible linear system implies .
Theorem 1 is what allows any sound inference method to supply Benders cuts. Correctness needs only (B1), so the method that derives the cuts (resolution, constraint propagation, a branch-and-bound proof, LP duality) never has to be re-verified at the level of the decomposition. The paper's specializations to satisfiability, 0-1 programming and machine scheduling, and much of the later literature on logic-based Benders, rely on this theorem when they check validity of their cuts and nothing more. Theorem 2 is the matching termination guarantee, and the example on p. 10 shows that the finiteness of cannot be dropped.
Both theorems are proved in the paper, and to the extent known no machine-checked version exists. A formalization makes the paper's implicit conventions precise: values in , what "the subproblem dual is infeasible" means when is always a feasible bound, and exactly which cuts the master contains at each iteration. It also exposes two gaps in the printed proofs. Theorem 1's first clause uses the attainment of the subproblem optimum without stating it. Theorem 2's printed proof claims the subproblem value increases at every iteration, which is false, although the theorem itself is true. The definitions form a small reusable layer for later formalizations of specific logic-based Benders schemes.
The mathematics is elementary, and the difficulty lies in stating it faithfully. Several readings of the statements are wrong. A "run" whose are not master optima for exactly the cuts generated so far makes Theorem 1 false. Optimal values taken as real infima turn the infeasible case into junk. Defining "dual infeasible" over the extended reals makes clause 3 vacuous. For Theorem 2, the obvious argument is the printed one, that (or ) increases strictly. It fails: with three values of and cuts equal to away from their own , the subproblem value can decrease between iterations while stays fixed. The printed argument therefore cannot be transcribed, and the theorem needs a proof the page does not give.
X stands for , Y for and D for . The feasible set is S : Set (X × Y) and the objective is f : X → Y → ℝ. Optimal values are EReal infima and suprema, with for infeasible and for unbounded problems.EReal, so is always feasible. "The subproblem dual is infeasible" is therefore stated as "no real is feasible". A master optimum means and is at most that maximum at every ; the value means the master is unbounded.ybar k, has bound zbar k, and adds cut k. The structure IsRun encodes Figure 1 exactly: zbar 0 = ⊥, every iteration finds a dual-feasible beta k > zbar k with cut k (ybar k) = beta k, and the next is a master optimum for exactly the cuts 0, …, k. An unconstrained "run", or a dual infeasibility that satisfies vacuously, would trivialize the goal, and both are ruled out by these definitions.Retailers decide which product variants to stock, and most assortment-planning tools model consumer choice with the multinomial logit (MNL) model: a consumer who does not find an acceptable variant simply leaves without buying. Cachon, Terwiesch and Xu (Retail Assortment Planning in the Presence of Consumer Search, working paper of December 2002; published in MSOM 7(4), 2005, doi:10.1287/msom.1050.0088) point out that consumers also search: a consumer who likes what the store offers may still walk out to look elsewhere, and that is more likely when the assortment is narrow.
In practice a retailer does not know consumer preferences; it estimates them from sales data and re-plans. This mission formalizes §5.1 of the paper, which asks what happens when a retailer runs this estimate-and-replan loop with the traditional no-search MNL model while consumers actually search. The loop can settle at a heuristic equilibrium in the sense of Cachon and Kok (2002), and the question is how that equilibrium compares with the truly optimal assortment.
There are product variants, labelled from most to least popular, with preferences , and a no-purchase option ("variant 0") with preference . An assortment of depth is the set . Variant has margin , with whenever (monotone margins, p. 6), and carrying it at demand incurs an operational cost , where is concave and increasing on (demand is normalised to one consumer).
True demand: the independent assortment model. With a constant (Theorem 1 of the paper: ) and , the probability that a consumer searches is , and variant has demand
The no-purchase demand is , and the true profit is .
Estimates. Observing for , the retailer fits the MNL model, normalised by : for , and for variants not carried it reuses the estimates from an initial depth test with the full assortment. The no-search model fed with preferences predicts the shares and the profit .
Heuristic equilibrium. A depth is a heuristic equilibrium when maximises over : the assortment is optimal for the estimated preferences, and the estimates are those observed under the assortment. An optimal depth maximises the true profit over .
If is a heuristic equilibrium and is an optimal depth such that every deeper depth is strictly worse ( for ), then
Theorem 8 says that a retailer who ignores consumer search and plans iteratively from its own sales data can only err on the side of a too-narrow assortment, never a too-deep one. The bias is structural: Theorem 7 shows that the estimates get every product variant's relative preference right but misjudge the no-purchase option in a direction fixed by the depth. The result thus separates the part of the MNL model that survives consumer search (IIA among products) from the part that does not (IIA with respect to the no-purchase option).
The results are proved in the paper, by short arguments, but some steps are only asserted: the non-negativity of variant profits at the equilibrium is attributed to "the previous section", and the overlapping assortment model is dismissed with "the similar process". No machine-checked proof of these results is known. A formalization makes explicit the hypotheses the paper leaves implicit (, and a strict-deeper condition on in place of the presumed uniqueness of the optimum), and delivers a reusable formal model of MNL estimation under search.
Each step is elementary, and the difficulty lies in keeping two profit functions apart and carrying the right inequalities between them. The tempting shortcut, "the estimates are correct, so the no-search optimum is the true optimum", fails: the estimates are correct only up to the no-purchase preference , which depends on , and that single number shifts every predicted share. The proof of Theorem 7 must reduce the comparison of and to the monotonicity of the function . The step from no-purchase demand to profit needs every predicted variant profit to be non-negative, which requires the monotone labelling of preferences and margins together with concavity of and ; the paper asserts it without proof.
Fin n, 0-based: the paper's variant is index . Depths are natural numbers, and depth is the published RetailVariety.Structure.popularSet n x; the MNL share is the published RetailVariety.Structure.share.Fin n; its preference and estimate are separate reals.Trivializing formalizations are ruled out: the estimates are not the true preferences (in particular , which would force ); is not an arbitrary maximiser but one with all deeper depths strictly worse; , where nothing is observed, is excluded rather than given junk estimates; and nothing is claimed for the overlapping model.
Contributions welcome: proofs of the milestones, in particular Theorem 7 and the positivity step, and a formal treatment of the overlapping model with its additional hypotheses.
A retailer choosing which variants of a product to stock (colours, sizes, models) faces a trade-off that operations management has studied since van Ryzin and Mahajan (1999): a deeper assortment attracts more purchases, but each added variant takes demand away from the variants already on the shelf. This loss is called cannibalization. In the standard model of consumer choice, the multinomial logit (MNL), cannibalization holds exactly: every variant's purchase probability falls when a variant is added.
The MNL assumes that a consumer who walks into a store buys either from that store or nothing. Real consumers can also leave to search elsewhere, and a deeper assortment makes them less likely to leave. Cachon, Terwiesch and Xu (working paper, 2002; published in Manufacturing & Service Operations Management, 2005, doi:10.1287/msom.1050.0088) add search to the MNL and ask whether cannibalization survives. Two forces now act on a variant's demand when the assortment expands: the share of buyers who choose it falls, and the share of consumers who stay in the store rises. This mission formalizes their answer for the first of their two search models, the independent assortment model, in which the outside option does not depend on what the retailer stocks.
There are possible variants ; the retailer stocks an assortment . A faux variant represents not buying.
Gumbel shocks. Fix a scale and let be Euler's constant. The zero-mean Gumbel law with scale has distribution function and density
Utilities. Variant has expected net utility (utility minus price), and the no-purchase option has (its price is ). A consumer's realised utilities are and , with independent and Gumbel. The preference of variant is , and .
No search. The consumer buys the variant of with the highest utility, or nothing if is higher. The probability that she buys is .
Search. A consumer may instead search at a cost and receive , where is another independent Gumbel shock that she has not yet observed. Having seen , the best utility in the store, she searches when the expected gain minus the expected loss is at least :
The independent-assortment demand is the probability that variant has the highest utility in , beats the no-purchase option, and the consumer does not search. Write (the search threshold), and .
For all and with ,
The goal leaves the utilities , , , the search cost , the scale and the number of variants arbitrary.
Theorem 1 says that under independent-assortment search the demand for every stocked variant is its MNL demand scaled by one common factor, the probability that the best option in the store clears the threshold . The threshold itself does not depend on the assortment. Theorem 2 then shows that the MNL's cannibalization effect dominates the retention effect of a deeper assortment, so each variant's demand still falls strictly when variants are added. The paper's later results on the shape of the profit function and on the structure of optimal assortments under search build on this closed form.
The paper's proofs are short but rely on steps it states without proof: the MNL formula is cited from Anderson, de Palma and Thisse (1992), the search rule is obtained "after rearranging terms", and the closed form follows from a change of variables. No machine-checked version of these steps is known. The mission produces a checked derivation of a logit-type closed form from an explicit random-utility model with an outside option and an endogenous stopping decision, at the paper's scale and with its centring constant .
Theorem 2 is not monotonicity of a single fraction. Adding a variant enlarges the denominator of and simultaneously raises the factor , so the sign of the change is a competition between the two, and a bound on either factor alone does not settle it. The comparison becomes one-dimensional only after Theorem 1 is available, and Theorem 1 itself requires computing a probability of an event defined by finitely many strict inequalities among independent Gumbel variables together with the consumer's search decision. That calculation is an iterated integral over the product law, with the decision rule, the mean of the Gumbel law and the change of variables each needing their own justification.
Fin n, 0-based (the paper's variant is index ). The no-purchase option is the extra index none of Option (Fin n). Assortments are Finset (Fin n), and is S ⊂ Splus.IsZeroMeanGumbel μ G says the probability measure G on ℝ has distribution function above; and is Real.eulerMascheroniConstant. Such a law exists for every (checked sorry-free locally).Option (Fin n) → ℝ with the product measure Measure.pi (fun _ => G). The search shock does not appear in it: the consumer decides before observing , so only its law enters, as integration against G in the search rule.noSearchProb) and (searchProb) are the real values of the probabilities of the choice events, with strict inequalities. The search event uses the paper's decision rule (the displayed integral), not the threshold ; the equivalence is a milestone. The closed form is the published RetailVariety.Structure.share.Ruled out. Demand defined by the closed form (3), which would make Theorem 1 true by definition and Theorem 2 a calculus fact; Theorem 2 with and ; a standard Gumbel law (scale , mean ) in place of the paper's zero-mean scale- law; and a model without the no-purchase option.
Infrastructure. A complete development needs the distribution theory of the Gumbel law (density, mean), choice probabilities of products of i.i.d. continuous variables as iterated integrals, and calculus for . The Gumbel and MNL lemmas are reusable for any logit-based choice model, including the other missions of this series. Contributions of proofs of any milestone, or of general MNL infrastructure that the milestones can import, are welcome.
A retailer deciding which variants of a product to stock trades off two effects. A deeper assortment captures consumers whose favourite variant would otherwise be missing, but it splits demand among more variants, each of which then carries its operational costs (shelf space, handling, inventory) at a smaller, less efficient scale. Van Ryzin and Mahajan (Management Science 1999) showed that under multinomial-logit (MNL) demand the optimal assortment consists of the most popular variants, which reduces the search over assortments to candidates.
Cachon, Terwiesch and Xu (working paper, 2002; published in MSOM 2005) add consumer search: a consumer who finds nothing good enough in the store may leave to look elsewhere, and a deeper assortment makes that less likely. In their independent-assortment model the search threshold does not depend on the store's assortment, but the fraction of consumers who stay does. This mission formalizes their Theorem 5: even with this extra dependence, the profit change from adding a variant is quasi-convex in that variant's preference.
There are variants. Variant has a preference and the no-purchase option has preference (in the paper , with the net utility and the Gumbel scale). For an assortment the MNL purchase probability without search is
A consumer searches when her best alternative in the store, including no purchase, falls below a threshold . With Euler's constant and , this happens with probability , and by the paper's Theorem 1 the independent-assortment demand is
Each variant sold earns a margin , and stocking a variant with demand costs , where the cost function is concave and increasing on (economies of scale). Variant 's profit is . Write .
Fix and a variant , and treat 's preference as a variable. Let be variant 's profit in ; its demand carries the factor , not . The cannibalization loss and the profit change are
Quasi-convexity of says that a variant is worth adding, if at all, at an extreme of its popularity. The paper uses it to conclude that, as without search, the optimal assortment under independent-assortment search lies among the popular assortments, the sets of the most preferred variants. This reduces assortment optimization to candidates. The paper also shows that the conclusion fails in its overlapping-assortment model, so the independent-assortment case marks where this structural result survives the addition of search.
The result is proved in the paper; none of it has a machine-checked proof. The paper's proof contains gaps that a formalization must close: several sign and monotonicity facts are asserted without proof ("It can be shown", "by a similar argument as in Theorem 4"), display (8) is printed without a factor , and the step from (10) to (11) rests on an inequality asserted without the full expression. A complete formal proof of Theorem 5 therefore also fixes the argument.
The no-search analogue (Theorem 4) is easy: the numerator of is increasing, so changes sign at most once. Here the search factor depends on , and the derivative splits as with , , nondecreasing and nonincreasing, but neither nor is monotone. So the argument used for Theorem 4 no longer applies, and when and the derivative cannot be written as a positive factor times a monotone one. The proof needs a separate second-order argument at critical points in that case. Showing only that has at most one zero is also not enough: it must change sign from negative to positive.
Fin n (0-based); the no-purchase option is a separate real v0 > 0, not an element of Fin n. All preferences are positive. The MNL probability is the published RetailVariety.Structure.share, referenced, not redefined.deriv c. The value is unconstrained; .Function.update v j x on insert j S, with . Quasi-convexity is Mathlib's QuasiconvexOn ℝ (Set.Ici 0).A retailer that sells a product in many variants (colours, sizes, flavours) has to decide which variants to stock. This is the assortment planning problem. Each variant added to the shelf brings new demand. It also cannibalizes demand from the variants already stocked, and it lowers their cost efficiency, because operational costs (shelf space, handling, holding) usually show economies of scale. Cachon, Terwiesch and Xu, in Retail Assortment Planning in the Presence of Consumer Search (Wharton working paper, December 2002), study this trade-off under the multinomial logit (MNL) model of consumer choice. They compare a model without consumer search with two models in which consumers may leave to search elsewhere.
There are nonempty assortments of variants, so full enumeration is impractical. The retailer wants to know whether attention can be restricted to the popular assortments , the assortments made of the most preferred variants.
Timeline. Van Ryzin and Mahajan (Management Science 45(11), 1999, doi:10.1287/mnsc.45.11.1496) showed that, without search and with a cost derived from the newsvendor model, the profit change from adding a variant is quasi-convex in that variant's preference. As a consequence, the optimal assortment is a popular one. Cachon, Terwiesch and Xu (working paper 2002; Manufacturing & Service Operations Management 7(4), 2005, doi:10.1287/msom.1050.0088) extended the quasi-convexity to any concave increasing cost (Theorem 4 of the working paper), and then to search with independent assortments (Theorem 5). This mission formalizes Theorem 4.
Let be the possible variants. Variant has a preference ; in the paper , where is the variant's expected net utility and is the Gumbel scale. The no-purchase option has preference . With assortment , the MNL demand of variant is
Variant has margin (price minus purchase cost). Stocking it incurs an operational cost , where the cost function is concave and increasing on (the consumer population is normalised to , so demands lie in ). The profit of variant is , and the retailer's profit is .
Fix and a variant , and let . Treat 's preference as a variable. Write for variant 's demand with assortment , and for its profit. The loss on the variants already stocked is
and the net profit change from adding is . Adding is profitable exactly when . Write .
that is, every sublevel set is an interval. The goal holds for every concave increasing and every choice of margins, and assumes no differentiability.
The result. A quasi-convex function on an interval attains its maximum at an endpoint. So if adding a less preferred variant to is profitable, adding a more preferred variant (with ) is at least as profitable. With monotone margins, this exchange argument shows that an optimal assortment with variants consists of the most popular variants. The search for the optimal assortment then reduces from candidates to . The paper uses this structure again for the search model with independent assortments (Theorem 5) and in its analysis of a heuristic equilibrium (Theorem 8).
Formalizing it. The theorem is proved in the paper, and is not known to have been formalized anywhere. The mission produces a machine-checked proof for an arbitrary concave increasing cost, with per-variant margins. The paper's proof differentiates and writes a single common margin. A formal proof settles that neither assumption is needed. Van Ryzin and Mahajan's newsvendor-specific Lemma 1 is posed separately on Prove2Me (RetailVariety.Structure.lemma_1). It concerns a different function, a ratio on , and is not a special case of the statement here.
Adding changes every demand at once: 's own demand rises while all of 's demands fall, each through the shared denominator . The obvious approach is to show that is convex, and it fails: is in general not convex in , for example, when is linear and every margin equals some , is a positive multiple of the concave demand plus a constant. The paper's own argument goes through the derivative (6). It needs a derivative of , and its last step ("at most one with ") is literally false when the numerator of (6) vanishes on an interval, for instance when is linear with slope equal to a common margin, so that is constant. A rigorous proof must handle a non-differentiable concave , the endpoint where 's demand is , and a numerator that may be constant on stretches.
Fin n, 0-based (the paper's variant is index ). The no-purchase option is not a variant: is a separate real, with and for all .RetailVariety.Structure.share (from RetailVariety.Structure.Model), with assortments as Finset (Fin n). is share applied to the preference vector with 's entry replaced by the variable, on insert j S, and is assumed.ConcaveOn ℝ (Set.Icc 0 1) c, MonotoneOn c (Set.Icc 0 1)). Nothing is assumed about , so .m : Fin n → ℝ are arbitrary reals. The monotone-margin assumption of §3 is not needed and not imposed.QuasiconvexOn ℝ (Set.Ici 0). The domain is the closed half-line, including .deriv c. The goal does not.The following formalizations would trivialize the problem and are ruled out: a specific cost (newsvendor, power, linear); convexity instead of quasi-convexity; only on ; or a common margin imposed without need.
Contributions welcome: proofs of the milestones, a proof of the goal that avoids derivatives, and general lemmas on quasi-convex functions of one variable and on the algebra of MNL shares, which the companion missions of this series (I and III–V) can reuse.
Twin-width was introduced by Bonnet, Kim, Thomassé and Watrigant (J. ACM 69(1), Article 3, 2021) as a graph parameter under which first-order model checking is fixed-parameter tractable when a contraction sequence is given. Its interest lies in the classes it covers at once: planar and, more generally, -minor-free graphs, bounded-degree grids, unit ball graphs of bounded clique number, and the classes of bounded rank-width or clique-width. These are the classical dense-graph width measures, for which FO (indeed MSO) model checking was already known to be tractable through Courcelle–Makowsky–Rotics.
This mission formalizes the link to the dense width measures, stated in the paper through boolean-width (Bui-Xuan, Telle and Vatshelle, Theor. Comput. Sci. 412(39), 2011). It is known that (Vatshelle's PhD thesis, Chapter 4), so a bound on twin-width in terms of boolean-width shows that bounded twin-width captures bounded rank-width, clique-width, module-width and boolean-width simultaneously.
Let be a finite simple graph on a vertex set .
Two vertex sets are homogeneous if either all pairs are edges or none is. For a partition of , a part has red degree equal to the number of other parts that are not homogeneous to ; is a -partition if every part has red degree at most . The graph has twin-width at most , written , if there are partitions of with the partition into singletons, having at most one part, each obtained from by merging two parts, and every a -partition. This is the paper's partition form (p. 3:32) of its definition through trigraphs and red edges (pp. 3:11–3:12).
A decomposition tree of is a rooted binary tree , every internal node having exactly two children, whose leaves are in one-to-one correspondence with . Each edge of lies above exactly one rooted subtree and induces a cut of : is the set of leaf labels of that subtree and . For disjoint write
the number of different neighbourhoods in of subsets of , the empty subset included. The boolean-width of the cut is , the boolean-width of is its maximum over the edges of , and is the minimum over all decomposition trees. In Lean, nbhdCount G A B is , and BoolWidthLE G N states that some decomposition tree has on every edge, so is BoolWidthLE G (2^k).
Every graph with boolean-width has twin-width at most . With , the integer neighbourhood count,
The theorem places the classes of bounded boolean-width, and therefore of bounded clique-width and rank-width, inside the classes of bounded twin-width, with a single-exponential bound. Combined with the paper's model-checking algorithm, it recovers tractability of FO model checking on these classes once a contraction sequence is computed, and it situates twin-width as a common generalization of the dense width measures and of sparse classes such as -minor-free graphs.
No machine-checked version of twin-width or boolean-width is known to exist; neither notion is in Mathlib. The mission produces Lean definitions of twin-width in partition form, of decomposition trees and of the neighbourhood count behind boolean-width, together with the four combinatorial steps the paper's proof states explicitly. The definitions are shared, in identical form, with the other missions of this series on the same paper.
The first three milestones are elementary: a counting bound on contraction sequences, a walk down a binary tree, and a pigeonhole argument. The fourth is a direct count of non-homogeneous parts.
The difficulty is the iteration. After the first contraction the leaves of the updated tree are contracted vertices, so "the same neighbourhood in " must be read as homogeneity to all of for a set of vertices, and the boolean-width bound of the cuts must be re-established for sets rather than single vertices. The paper asserts the invariant that the contractions never create a red component of more than vertices without proving it. A complete proof of the goal therefore has to supply an invariant, carried through all contractions, that keeps every part's red degree below . The naive repetition of the first step does not by itself control red edges between previously contracted parts.
Twin-width is the predicate TwinWidthLE G d, never a numerical infimum, so a junk value of an empty or unbounded infimum cannot make the goal trivial. A contraction sequence must merge exactly two parts at each step and start from singletons; it cannot jump to one part. Homogeneity counts all pairs between two parts, in both of its alternatives. Boolean-width is bounded on every edge of the decomposition tree, not only at the root, and the count runs over neighbourhoods of all subsets of , not only of single vertices. The bound depends only on , not on the graph.
Boolean-width is kept as the integer count ; since means that the least admissible count is , the Lean goal for this is exactly the printed theorem. Subtractions are in and exact where used. Graphs live on a Fintype vertex type with decidable equality and decidable adjacency. A graph on the empty vertex set has no decomposition tree; the goal is silent about it, and it has twin-width . No hypothesis is added to any statement relative to the page except in milestone 2, which the page has implicitly () and without which the conclusion is impossible.
The definitions needed are the setting module TwinWidthI.BoolWidth.Setting: merge steps, homogeneity, -partitions, twin-width, decomposition trees (DTree), the count and BoolWidthLE. Proofs of the milestones, a proof of the goal, and lemmas towards the iteration invariant are welcome.
Treewidth measures how closely a graph resembles a tree. Many problems that are NP-hard on general graphs can be solved in time linear in the number of vertices once a tree decomposition of bounded width is available, so computing such decompositions quickly is a basic task in algorithmic graph theory. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) gave an algorithm that, for a graph on vertices and an integer , either reports that the treewidth of exceeds or returns a tree decomposition of width at most , in time .
The paper's headline is that algorithm, a statement about pseudo-code and running times. This mission does not formalize it. It formalizes one of the paper's combinatorial lemmas, Lemma 6.5 (p. 369), which the algorithm's data structure uses to answer its balanced-separator query: it turns the search for a small balanced separator into two maximization problems that a dynamic program can solve.
Timeline. Robertson and Seymour (Graph Minors II, J. Algorithms 7, 1986) proved that graphs of treewidth have balanced separators of size (Lemma 2.1 of the paper). Robertson and Seymour (Graph Minors XIII, 1995) used it in an approximation algorithm, Reed (1992) improved the dependence on to , and Bodlaender et al. (2016) reached linear time with a single-exponential dependence on .
All graphs are finite and simple. For , is the graph obtained by deleting ; its components are the vertex sets of its connected components.
A separation of is a partition of (parts may be empty) such that no edge of joins to . Its order is . It is -balanced if .
For and sets of terminals , a terminal separation of the induced subgraph of order (Definition 6.4) is a partition of with
It is left-pushed if is maximum, and right-pushed if is maximum, among all terminal separations of of order with the same terminals.
The treewidth is the least width of a tree decomposition of (Definition 1.1), where the width is the largest bag size minus one.
Let and let be a separation of with . Then there are a partition of and integers with such that, for with terminals ,
In the order of the proof, the milestones are: Lemma 2.1 (balanced -separators of size , cited from Graph Minors II); the packing step of the proof sketch of Lemma 2.2 (components holding at most of each split into two sides holding at most each); the folklore -balanced separation of order ; the restriction of that separation to , which gives part (i); four lower bounds on , ; the dichotomy that two opposite "quadrants" have at least vertices each; the comparison of pushed separations with the restricted one; and the gluing step of part (ii).
Lemma 6.5 is what makes the paper's balanced-separator query computable: given a bag that splits a component in a balanced way, a left-pushed and a right-pushed terminal separation are each the solution of a maximization problem, and the lemma guarantees that gluing them gives a separator of order whose sides are bounded away from . The constant feeds into the approximation ratio of the whole algorithm.
The proof is complete in the paper and elementary given Lemma 2.1. No part of it is formalized in Lean's Mathlib or, as far as a search of the Prove2Me catalog shows, on the platform. Lemma 2.1 itself, Robertson and Seymour's balanced-separator theorem for bounded treewidth, is not in Mathlib; a machine-checked proof of it would be reusable wherever treewidth separators are used (divide-and-conquer on tree decompositions, Lipton–Tarjan style arguments, grid-minor theorems).
Everything after Lemma 2.1 is counting with partitions, but the bookkeeping is the obstacle: the two separations and cut into nine pieces, the induced subgraphs overlap on , and pushedness is a maximum over a family of partitions of a subset, not of .
Lemma 2.1 is the hard milestone. It is a statement about tree decompositions, and any proof has to relate subtrees of the decomposition tree to components of for a bag , infrastructure that does not yet exist in Mathlib.
V : Type with decidable equality; vertex sets are Finset V, is Finset.univ, is Fintype.card V. Universe 0 matches the published definition of treewidth.RobertsonSeymour1986.GM5.TreewidthLE G k: a decomposition tree on a finite type whose bags have at most vertices. Definition 1.1 roots the tree; rooting does not change the width.avoidComp G X u: the vertices reachable from by a walk of none of whose vertices, endpoints included, lies in .Part (i) is part of the goal: without it, left- and right-pushed separations of the chosen orders might not exist and part (ii) would hold vacuously. Choosing does not trivialize the goal, because the size bound and the budget must hold simultaneously.
Welcome contributions: a proof of Lemma 2.1 from tree decompositions (reusable on its own), the packing lemma, and the counting milestones of the proof of Lemma 6.5.
Graph coloring asks whether vertices can be assigned colors so that adjacent vertices receive different colors. Restricting the graphs by forbidden induced paths can expose structure that is absent from general graphs. Bonomo, Chudnovsky, Maceli, Schaudt, Stein and Zhong study list three-coloring when the graph has no induced path on seven vertices, building on earlier work on coloring graphs with shorter forbidden induced paths. Their paper proves an algorithmic result, but its treatment also uses a purely graph-theoretic statement: a connected -free graph has a small connected set that reaches every vertex within two steps, unless the graph contains a four-vertex clique. This mission isolates that statement as Corollary 5 of the paper.
The structural input to the corollary is a theorem of Camby and Schaudt about connected dominating sets in -free graphs, quoted as Theorem 4 in the coloring paper. That result applies to every allowed path length , rather than only to the seven-vertex case. It is a milestone here in the precise form printed in the source article. The Camby–Schaudt paper develops connected domination as a characterization of graphs without long induced paths.
A simple graph has a vertex set and an undirected edge relation with no loops. The graphs in this mission are finite. The path has vertices and consecutive vertices adjacent. A graph is -free when it has no induced subgraph isomorphic to : the graph may contain a path with vertices as a non-induced subgraph if extra edges join vertices of that path. This distinction matters throughout the source paper.
For a vertex set , its open neighborhood consists of vertices outside with a neighbor in . Write . The set is dominating when , so each vertex lies in or has an edge to . It is 2-dominating when , meaning each vertex is at graph distance at most two from some vertex of . A dominating or 2-dominating set is connected when the subgraph induced by is connected. In this mission, connectedness includes nonemptiness, as in the paper's use of such sets.
A clique of size four is a set of four pairwise adjacent vertices. The notation below asserts the existence of such a set. Since all edges between those four vertices are present, it is also an induced complete subgraph. The notation means there is a graph isomorphism from the induced graph on to that path.
For a finite, connected, -free graph , the goal is
The four-vertex clique is a genuine alternative in the claim; the mission does not assume its absence. The result is the first, structural sentence of Corollary 5. Its following sentence gives a running time for finding the set or clique and is outside this mission.
For every , the cited theorem asserts that each finite connected -free graph has a connected dominating set for which
The other milestones are statements identified in the proof of Corollary 5: a connected -free graph is complete, domination inside a dominating set yields 2-domination in the original graph, and the three non-leaf vertices work when the induced dominating graph is a . These are listed in the paper's order of use, with the quoted theorem also available as a separate target.
Corollary 5 gives a bounded set of vertices from which the rest of a connected -free graph can be reached in two steps, except when a is present. Its bound is the concrete number three, independent of graph size. In the coloring paper this supplies a small structural seed for later restrictions on vertex palettes. A formal statement of the corollary makes that finite structural claim available independently of any coloring algorithm.
Theorem 4 has broader reuse: it links forbidden induced paths to connected dominating sets for general . The remaining milestones isolate the graph facts needed to connect this general result to the seven-vertex corollary. The article and the cited theorem provide mathematical proofs; these Lean declarations are open theorem statements, with machine-checked proofs still to be supplied. This mission therefore asks for formal proofs of known graph-theoretic results, not for a new resolution of an open mathematical problem.
The difficult step is finding a connected dominating set whose induced graph has the much stronger path restriction in Theorem 4. Ordinary domination by itself does not impose that restriction, and replacing induced-path exclusion with exclusion of all paths would change the class of graphs. The later cases require careful handling of connectedness and the passage from domination within to distance-two domination in . These issues are mathematical as well as formal: an empty set or a merely preconnected induced graph would erase the intended content.
Lean represents as SimpleGraph V with a finite vertex type. Vertex sets are Finset V; is Mathlib's pathGraph t; -freeness is the absence of an induced copy using IsIndContained. The definitions of , , domination and 2-domination are shared within P7ThreeColor.Seed. A connected induced graph uses Connected, which requires at least one vertex. Four-clique existence is ¬ G.CliqueFree 4. The only added standing convention is finiteness, implicit in the source's graph algorithm and finite cardinalities. No extra colorability or clique-free hypothesis is attached to the goal.
The running-time claim in the second sentence of Corollary 5 and the paper's headline Theorem 1 are not formalized because this mission has no machine model. A statement that merely postulates a small set as a hypothesis, or substitutes ordinary domination for 2-domination, would miss the result. Contributions are welcome for proofs of the goal and milestones, reusable facts about induced paths and connected domination, and auxiliary Mathlib lemmas needed to cross between graph isomorphisms, induced subgraphs and finite sets.
Treewidth measures how closely a graph resembles a tree. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) study an algorithm for producing tree decompositions. Its headline result is algorithmic; this mission formalizes one combinatorial lemma used in its analysis.
In §4.3.2, p. 349, the authors isolate a purely combinatorial fact, Lemma 4.3, which bounds the number of nodes of a rooted tree in terms of a measure placed on its nodes. They use it for the partial tree decomposition built by FindPartialTD, with a measure of the form . This mission formalizes Lemma 4.3 and the steps of its proof. The lemma is self-contained and does not mention graphs or treewidth.
A rooted tree consists of a finite vertex set , a root , and a parent map defined on such that every vertex reaches by iterating . If , then is a child of and is the parent of . A vertex without children is a leaf. The descendants of are the vertices with for some (including itself), and the subtree rooted at is the tree they span; is its number of vertices, and .
A measure is any function . Lemma 4.3 considers measures with three properties, for a constant :
Throughout, .
Under properties (i)–(iii),
Each step is stated for an arbitrary vertex of , with the subtree in the role of the paper's tree.
The result. Lemma 4.3 converts two local conditions, superadditivity of the measure over the children of each node and geometric decay by a factor along each parent–child edge, into a global linear bound on the size of the tree. Superadditivity alone does not bound the size: a long path with constant measure satisfies (i) and (ii). Decay alone does not either: a star with many leaves satisfies (iii). The counting principle can also be used when a recursive construction splits a resource among child nodes while reducing that resource along every edge.
Formalizing it. The lemma is proved in the paper. The mission produces formal statements of the lemma and the main bounds in its proof, over a published, reusable encoding of finite rooted trees by parent maps. A complete development would also establish structural facts about descendants and children that can be reused for other results about finite rooted trees.
The summed bound for the children's subtrees contains the term . When , superadditivity alone does not give the target's final : a path with constant measure is a counterexample if geometric decay is omitted. Formalization also has to account for the fact that the reusable tree representation is a parent map on a finite type, rather than an inductively constructed tree.
The rooted tree is the published definition HarelTarjan.Compressed.RootedTree: a finite vertex type V with a root and a total parent map in which every vertex reaches the root, with the convention . is Fintype.card V, and is the published subtree size size T v (the number of descendants of , including ). The local definition file adds IsChild T v c ( and ) and children T v; the condition removes the pseudo-edge , so the root is never its own child.
Conventions: is real valued, as on the page; property (ii) is a sum over a possibly empty set of children; the constant of property (iii) is a parameter with the two hypotheses and , because the conclusion is stated with that same . The fraction is real division, and the hypothesis keeps it away from Lean's convention . The bound keeps the page's "".
A trivializing formalization is ruled out explicitly: the parent–child relation is directed by the root, so property (iii) constrains each edge in one direction only. A symmetric reading (" for all adjacent ") would be unsatisfiable for and make every statement vacuous; the hypotheses here are satisfied, for example, by the two-vertex tree with and .
A complete development needs the decomposition of size T v as and an induction principle for parent-map trees. Both are reusable for statements about rooted trees given by parent maps, and contributions of them as separate lemmas are welcome. The paper's subsequent application is outside this mission's scope.
Classical mean field theory describes exchangeable diffusions, each interacting with the empirical average of all the others. As the particles become independent copies of a McKean–Vlasov process (propagation of chaos). Many systems of interest are not exchangeable. Particles sit at the vertices of a network and interact only with their neighbours, as in models of opinion dynamics, epidemics on contact networks, synchronisation of oscillators and systemic risk in financial networks. When the network is dense and its adjacency structure converges, the natural limit object is a graphon, a symmetric measurable function that encodes the limiting edge density between "positions" (Lovász, Large Networks and Graph Limits, 2012).
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) develop a law of large numbers for such systems. This mission formalizes their second main result, Theorem 3.1. Under cut-metric convergence of the interaction kernels, the empirical measure of the -particle system converges in probability to the averaged law of a continuum graphon particle system. Related work includes Bhamidi, Budhiraja and Wu (Stochastic Process. Appl., 2019) on weakly interacting particles on inhomogeneous random graphs, Coppini, Dietert and Giacomin (Stoch. Dyn., 2020) on Erdős–Rényi graphs, and Bet, Coppini and Nardi (arXiv:2006.07670) on oscillators on dense random graphs.
Write with Lebesgue measure and fix a horizon . Let with the uniform norm . On one probability space take independent initial states with laws and independent -dimensional Brownian motions , for all . The graphon particle system (2.1) for a graphon and Lipschitz coefficients is the continuum of nonlinear diffusions
where is the law of . Write for the path law of and for the averaged law.
The -particle system (3.1) places particle at label , starts it at , drives it by , and weights its interaction with particle by :
The weights come from a step graphon , constant on the squares of the -grid. Either , or are independent Bernoulli variables for , independent of the noise (Condition 3.1). The kernels converge in the cut norm . Two further norms appear: the operator norm , and the Wasserstein-2 distance on .
Assume the initial laws are measurable in with a uniform -moment and are Lipschitz (Condition 2.1). Assume is -continuous on each interval of a finite cover of (Condition 2.2(a)), and that Condition 3.1 holds with in the cut metric. Then
If, in addition, is continuous at for a.e. at each interior point of the cover (Condition 2.2(b)), then
In order: Remark 2.1, where cut-norm convergence implies operator-norm convergence; Theorem 2.1(a), continuity of in ; the weak-LLN bound (6.4); the discretization bound (6.11); Lemma 6.1,
Lemma 6.2, a law of large numbers for the continuum particles ; the approximation of by continuous graphons; the continuity (6.12) of in the graphon, in a corrected qualitative form; the empirical coupling bound for ; and (6.14).
Theorem 3.1 shows that the averaged graphon law is the correct macroscopic description of a dense heterogeneous particle system. This holds for deterministic weights and for Erdős–Rényi-type random weights, and the graphon may be discontinuous. It is the foundation for graphon mean field games and for control of large networked systems, where replaces the intractable -particle law. Under the regularity Condition 2.2(b) the convergence holds in , particle by particle, along the natural coupling.
The result is proved in the paper (§6.1–§6.2). Nothing in it is formalized. A formal proof would produce reusable infrastructure: graphons, the cut and operator norms, Lusin approximation of graphons, Wasserstein distances between empirical measures, and laws of large numbers for random probability measures on path space. It also needs pathwise stability estimates for SDE systems built on Itô integrals, which goes well beyond what Mathlib has today.
The particles are neither exchangeable nor identically distributed. The classical propagation-of-chaos argument compares each particle with an i.i.d. copy of one McKean–Vlasov process, and it does not apply here. Each must be compared with its own limit , and the error has two sources: the random or discretized weights , and the replacement of by . Cut-metric convergence controls only through integrals against bounded test functions. The interaction term, however, integrates the unbounded function against varying laws . When is merely measurable, the map need not be continuous, and the error of replacing by the average over the labels need not vanish. The direct estimate therefore fails for (3.3) without Condition 2.2(b), and this is the case the goal must cover.
The setting file GraphonMF.DenseLLN.Setting fixes these conventions:
Fin d → ℝ with the sup norm. All statements are invariant under this choice: constants are existential and the other conclusions are limits.Peng1990.SMP.IsItoProcess. The filtrations are the uncompleted natural filtrations and .WassersteinDRO.Duality.wassersteinDistance with values in .Two encodings would trivialize the targets, and both are ruled out. A pointwise or almost-sure reading of (3.3), or convergence of for a single test function, is not the claim. Choosing the constants of Lemma 6.1 and (6.11) after the sequence would make them nearly empty, so they are chosen before it. A sorry-free check confirms that the solution predicates are satisfiable: with the constant paths solve both systems.
Solvers will need several pieces of library work: the inequality , BDG-type moment bounds for the Itô integrals of Peng's library, Gronwall estimates, Lusin's theorem on , and the metrization of weak convergence on (Lévy–Prokhorov). Contributions to any of these are welcome independently of the goal. The paper's proofs are in its §5 (Theorem 2.1) and §6.1–§6.2 (Lemmas 6.1, 6.2 and Theorem 3.1).
Classical mean-field theory describes diffusions that interact symmetrically, each feeling the empirical average of all the others, and shows that as every particle behaves like an independent copy of a single McKean–Vlasov process. Many systems of interest are not symmetric: neurons, agents in a financial network, or oscillators interact through a graph, and particles in different parts of the graph feel different neighbourhoods. A graphon is the limit object of dense graph sequences (Lovász, Large Networks and Graph Limits, AMS 2012), and it is the natural way to describe the interaction structure of such systems in the limit.
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) study a continuum of diffusions indexed by labels whose interaction is weighted by a graphon, and prove laws of large numbers and rates of convergence for -particle systems on graphs sampled from the graphon. This mission targets their uniform rate of convergence for weights sampled from a Lipschitz graphon (Theorem 3.2).
Write with Lebesgue measure. Fix a horizon and let with .
On one probability space, are i.i.d. -dimensional Brownian motions and are independent initial states with laws , independent of the Brownian motions. Given a graphon and coefficients , the graphon particle system (2.1) is
with . The particles are independent but not identically distributed, and their laws are coupled through the -integral.
The -particle system (3.1) uses the same randomness at the labels :
so particle and the continuum particle at share their initial state and Brownian motion.
The hypotheses are:
Under Conditions 2.1, 2.3 and 3.2 there is such that
The result. Theorem 3.2 gives a quantitative propagation of chaos for heterogeneous interactions: with weights sampled from a blockwise Lipschitz graphon, every particle of the finite system, not just an average particle, is within in root-mean-square path distance of the continuum particle with the same label. The rate matches the classical mean-field rate (e.g. Sznitman 1991), so heterogeneity of the interaction costs nothing in the exponent. The same estimate covers the deterministic weighted graph and the random graph sampled from (in the annealed sense), and it is the dense counterpart of Theorem 4.2 for percolated graphs.
Formalizing it. The result is proved in the paper (§6.3); it has no machine-checked proof. A formal development would produce a reusable account of graphon particle systems and their finite- approximations: graphon-weighted McKean–Vlasov drifts, couplings through shared noise, and the decomposition of the interaction error into a Lipschitz feedback term, a law-of-large-numbers term and a Riemann-sum discretization term.
The obvious approach is to compare with directly and close a Gronwall inequality. The difficulty is that the comparison involves the empirical, graph-weighted average of the other particles, which is neither the graphon average nor an average of independent terms. Three different errors must be controlled simultaneously and uniformly in : the feedback of all particles' errors into particle , the fluctuation of a sum of independent but non-identically distributed terms whose weights may themselves be random, and the error of replacing an integral over labels by a sum over the grid . The last needs regularity of the law in the label , which is itself a theorem about the graphon system (Theorem 2.1(b)) and fails at block boundaries of , where only the small number of boundary cells saves the rate. Averaging over , as in the law of large numbers of Theorem 3.1, is not enough: the goal bounds the maximum.
Fin d → ℝ with the sup norm; matrices are measured entrywise. All statements are norm-invariant because every constant is existential. Particle is Lean's i : Fin n with label ; time is ℝ≥0; is Mathlib's unitInterval.Peng1990.SMP.Stochastic definitions; an SDE with random initial value is stated as an Itô process for . Each continuum particle uses the natural filtration of ; the -particle system uses the natural filtration of the weights, initial states and Brownian motions at the labels.WassersteinDRO.Duality.wassersteinDistance 2, valued in ; expectations of nonnegative quantities are lower Lebesgue integrals.Policy gradient methods optimize a parameterized policy for a Markov decision process by local search on its expected cost. The objective is nonconvex, so local search can in principle stall at a poor stationary point. Bhandari and Russo, Global Optimality Guarantees for Policy Gradient Methods show that for a broad family of control problems this does not happen, and, in quantitative form, that the objective is gradient dominated: its suboptimality is bounded by a multiple of the size of its gradient. The multiple involves a single problem-dependent quantity, the effective concentrability coefficient , which measures how well the initial state distribution covers the states that matter for optimal behaviour. Theorem 2 and the convergence rates of Theorem 5 of the paper are only informative when is finite, so sufficient conditions for a finite are what make those results usable. This mission formalizes the paper's three such conditions (Theorem 4).
Distribution-mismatch coefficients of this kind go back to Kakade and Langford (2002), and appear in the analyses of approximate dynamic programming by Scherrer and Geist (2014) and of policy gradient methods in finite MDPs by Agarwal et al. (2021).
A discounted Markov decision process consists of a measurable state space , nonempty feasible action sets , a bounded measurable per-period cost , a transition kernel , a discount factor and an initial probability distribution on . A feasible measurable stationary policy () picks an action in every state. Its cost-to-go is the expected discounted cost from , its discounted state-occupancy measure is
and its average cost is . The Bellman operator acts on bounded measurable functions by
An optimal policy minimizes at every state; . A policy class is indexed by a convex set , and .
The effective concentrability coefficient (Definition 3) is the smallest scalar such that
with , and if no scalar works. It converts a -weighted Bellman error into a -weighted optimality gap.
If for every measurable set , then satisfies (13); equivalently
(a) If is finite and for all , then . (c) If is a contraction with modulus in a norm with , then .
The element-wise inequalities , (5); the performance difference identity (29); the sup-norm bound (26); the occupancy-weighted inequality from the proof of part (b); and the contraction step from the proof of part (c).
Theorem 4 is what turns the paper's gradient-dominance theorem into a usable statement: with part (b), the constant in Theorem 2 is bounded by the worst-case likelihood ratio between the optimal policy's state distribution and the initial distribution, a quantity that can be checked without knowing the policy class. Part (a) shows that in finite problems any fully supported initial distribution suffices, and part (c) gives a route through weighted norms, used in the paper for optimal stopping (Lemma 13).
The results are proved in the paper. None of them is machine-checked. The mission produces a general-state-space formalization of the discounted cost MDP (kernels, occupancy measures, Bellman operators, measurable selection) together with the performance difference identity on measurable state spaces; existing formal developments of policy gradient theory on the platform are for finite MDPs only. The occupancy-measure and Bellman-operator layer is shared with the other missions of this series.
The argument for part (b) is short on paper, but each step is a measure-theoretic statement about infinite-horizon objects. The performance difference identity (29) exchanges an infinite discounted sum with integration against the chain's laws and needs the occupancy measure to be built from the -step kernels of the controlled chain. The change of measure from to needs the Bellman error to be nonnegative and integrable; its measurability is not automatic, because is a pointwise minimum over uncountably many actions, and is supplied by the measurable selection assumption. Part (c) needs the fixed-point property of the optimal cost-to-go, which again rests on measurable selection.
All statements use one Lean layer: MDP S A with measurable spaces S, A (a generalization of the paper's Borel subsets of Euclidean spaces), the cost and kernel given on all of , measurable stationary policies MPolicy S A, and costToGo, occupancy, loss, bellmanPi, bellmanOpt. The paper prints the Bellman operators (3)–(4) without the discount factor; every later use includes it, and so does the formalization. The optimal policy is a binder πstar with IsOptimal M πstar. Assumptions 1 and 2 of the paper are standing hypotheses of every main statement.
The coefficient is never formed as a number: "" is the predicate IsConcBound M Θ πθ πstar X, which says that satisfies (13); because the right-hand side of (13) is nondecreasing in the scalar, the two are equivalent. Part (b) quantifies over every with setwise, which is equivalent to ; a real-valued essential supremum is avoided because it reads exactly when the paper's bound is infinite. Part (a) assumes for every state, since otherwise is on paper and in Lean. Part (c) requires the norm comparison (21) on all bounded measurable functions, as its proof uses it on and , and encodes "a norm" by subadditivity, the one property used.
A formalization in which (13) or the occupancy-weighted inequality is assumed, or in which is a junk value of an empty infimum, would make the goal trivial; neither is used.
Contributions are welcome on every milestone, in particular on the performance difference identity and the measurability of the cost-to-go and of , which are reusable for any discounted MDP on a measurable state space.
Policy gradient methods optimize a parameterized policy by gradient descent on its expected total cost. They are a staple of reinforcement learning and of simulation-based optimization in operations research, but the objective is nonconvex in the policy parameters, and the standard theory guarantees convergence only to a stationary point. J. Bhandari and D. Russo (arXiv:1906.01786v3, Operations Research, 2024, DOI 10.1287/opre.2021.0014) identify structural conditions under which every stationary point is globally optimal.
Their first result (Theorem 1) requires the policy class to be closed under policy improvement. That excludes many classes used in practice, where it is known only that some member of the class is optimal: base-stock policies in finite-horizon inventory control are the standard example (Bertsekas, Dynamic Programming and Optimal Control, 1995). For stationary policy classes, containing an optimal policy is not enough: the paper's Example 1 has a policy class that contains the optimal policy, and policy gradient still gets stuck in a bad local minimum. Theorem 3 shows that for finite-horizon problems with a non-stationary policy class (separate parameters for each period), containing an optimal policy suffices, together with a single-period regularity condition imposed only at the optimal cost-to-go. This mission formalizes Theorem 3.
A Markov decision process consists of a state space , nonempty feasible action sets , a bounded measurable cost , a transition kernel , a discount factor and an initial distribution . A policy is a measurable map with ; is the set of all of them. The cost-to-go is , the loss is , and the discounted state-occupancy measure is . An optimal policy has pointwise for all ; . With the Bellman operator , the weighted policy-iteration objective is
A parameterized policy class is for a convex , and . A point is stationary for if is differentiable at and for all .
The finite-horizon structure (Condition 3) embeds a time-inhomogeneous problem in this discounted formulation: the states split into stages ; from a state in , , every feasible action leads to ; and is a costless absorbing state. The parameter is a concatenation , the parameter set is a product , and on the action depends only on . The stage objectives are .
Condition 4 asks that for every , the problem has no suboptimal stationary points. Assumption 3 asks that for every . Condition 0 asks that the policy-iteration objective be continuously differentiable in the parameters.
Under Conditions 0, 3 and 4 and Assumption 3, if is an optimal policy for some , then every stationary point of on satisfies
Theorem 3 covers finite-horizon dynamic programs in which a structured class of time-varying policies is known to contain an optimal policy, but is not closed under policy improvement: the paper's Example 8, multi-period inventory control with base-stock policies, is the motivating case. Policy gradient on such a class has no suboptimal stationary points, so any method that finds a stationary point finds a globally optimal policy, optimal among all policies and not only within the class. Condition 4 involves only the Bellman objective of the optimal cost-to-go , which often has regularity (for instance convexity) that the cost-to-go of an arbitrary policy lacks.
The result is proved in the paper. To our knowledge no part of it, nor the policy gradient theorem for deterministic policies on general state spaces, has a machine-checked proof. Formalizing it requires a measure-theoretic treatment of occupancy measures, the stage-wise decomposition of the weighted policy-iteration objective, and the backward induction of App. D.2.
The obvious approach reasons stage by stage directly on , but couples the stages: changing changes the distribution of states visited after stage . The paper's argument instead passes through the policy gradient theorem, which turns stationarity of into stationarity of single-period problems weighted by the occupancy measure of the current policy. These single-period problems involve , while Condition 4 speaks about ; relating them requires a backward induction over stages in which almost-sure equality on stage is transported to stage through the balance equation. This step needs the occupancy measures of all policies in the class, including policies other than , to be equivalent to , which is where Assumption 3 enters. The naive variant with a stationary policy class fails (Example 1).
The state and action spaces are arbitrary measurable spaces (the paper takes Borel subsets of Euclidean spaces; no argument uses that structure). Cost and kernel are given on all state-action pairs; the cost is bounded. Policies are deterministic, stationary and measurable; parameters live in EuclideanSpace ℝ (Fin d), so gradients and norms are Euclidean. is never defined as an infimum: an optimal policy is a hypothesis, with . Stages and sub-vectors are numbered from by a measurable stage index and a block index on coordinates; the product structure of is encoded as closure under exchanging one block.
Hypotheses beyond the printed sentence of Theorem 3, all disclosed in the item statements: Assumption 3 (announced on p. 17 as required, used in the proof); Condition 0 (needed for Lemma 6, which the proof invokes), in a joint form that the proof of Lemma 6 uses and that implies the printed partial-map form; the standing Assumptions 1 and 2 of §2; and, inside Condition 4, differentiability of on , the premise of Definition 1. The Bellman operators carry the factor omitted in the printed (3)–(4). The stage-wise balance equation is stated for ; the printed range fails at the absorbing state.
A formalization in which the goal assumes the stage-wise characterization (31), the balance equation, or on any stage is not Theorem 3; neither is one where "contains an optimal policy" means optimal only within . Stationarity includes differentiability, so a junk zero gradient never makes a point stationary.
Needed infrastructure: occupancy measures as series of iterated kernels and their balance equation, the cost-to-go as a bounded measurable function, the performance difference identity, the policy gradient theorem, and the decomposition of integrals over the stage partition. The occupancy-measure and policy gradient results are reusable for every mission of this series; contributions of these general lemmas are welcome.
Taxi fleets, ride-hailing services and dial-a-ride systems assign incoming customer requests to vehicles under time constraints. Bertsimas, Jaillet and Martin (Online Vehicle Routing: The Edge of Optimization in Large-Scale Applications, Operations Research 67(1), 2019) model the online taxi routing problem, a special case of the online dial-a-ride problem with time windows in which a vehicle serves one customer at a time. They show that mixed-integer optimization over a sparsified graph can dispatch thousands of New York City taxis in real time. The offline problem, in which all requests are known in advance, is the building block of their online algorithms, and its structure determines which offline methods are fast.
The structural fact this mission formalizes is the paper's Theorem 1. When every customer has a fixed pick-up time, the mixed-integer formulation of the offline problem is integral: its linear relaxation has only binary extreme points. So the problem is a linear program in disguise, which the paper uses for its maxflow heuristic.
The source is the authors' accepted manuscript (March 2018, 46 pages); every page and display number below refers to that manuscript, not to the typeset article.
Let be a finite set of customers and a finite set of taxis. Customer has a pick-up time window , and taxi becomes available at time . For customers , the number is the travel time from serving to picking up , and is the profit earned when is served right after . The numbers and are the travel time and profit when is the first customer of taxi .
The graph has the customers and taxis as nodes. Between customers there is an arc exactly when
Taxi nodes have outgoing arcs only. Throughout the paper is assumed acyclic (§2.1, p. 7).
The mixed-integer formulation (5)–(14) (pp. 11–12) has binary variables (customer is picked up right after ), ( is the first customer of taxi ) and ( is served), and continuous pick-up times . It maximizes subject to the flow constraints
the binary constraints (9)–(11), and the time constraints
Constraints (13) and (14) are strengthened Big-M constraints: with , (13) reads .
The LP relaxation replaces (9)–(11) by . A formulation is integral when every extreme point of its LP relaxation has .
If for every customer (and is acyclic, the standing assumption), then
Three further statements from the same pages are included as plain theorems. The first is the paragraph after Theorem 1: a solution with fixed times is feasible for the formulation with windows. The other two are the conditions (3) and (4) of §2.1, which exclude 2-cycles and all cycles of .
Theorem 1 turns a mixed-integer program into a linear program when the time windows shrink to points. The fixed-time problem can then be solved by the simplex method or by a max-flow algorithm. By the paragraph after the theorem, any choice of times inside the windows then gives a feasible solution of the original problem. This is the maxflow heuristic, and the paper reports it to be near-optimal when windows are small. The theorem also locates the source of the integrality gap: the time constraints (12)–(14), not the flow structure.
The result is proved on the page, briefly. No machine-checked version exists. Formalizing it means making the page's "equivalent to a formulation in which variable is removed" precise. The extreme points of the relaxation in -space must correspond to those of a flow polytope in -space. The integrality of that flow polytope must then be proved, which the page settles by appeal to max-flow.
The reduction to the flow system is elementary linear arithmetic. The substance is milestone 3. The system (6)–(8) is not literally in the standard form of a network-flow problem: it mixes an equation defining with inequalities, has unit upper bounds, and allows arbitrary arc sets, including cycles and loops . Neither the integrality theorem for standard-form network flows nor total unimodularity can be applied without first exhibiting a network and checking that the polytope corresponds to its flow polytope. Mathlib has the definition of total unimodularity but not the Hoffman–Kruskal theorem.
The page's phrase "the formulations are equivalent" also hides a step: the goal speaks of extreme points in -space, while the flow system lives in -space, and the two notions of extreme point have to be related explicitly.
Set.extremePoints ℝ.Two trivializing readings are ruled out. "Integral" is the extreme-point property of the relaxation, not the existence of an integral optimum for a given objective, and not the integrality of the mixed-integer feasible set, which holds by definition. Integrality is never demanded of the continuous times .
A complete development needs an integrality theorem for flow polytopes with integer bounds, which Mathlib does not have. Such a result is reusable well beyond this mission. Contributions of general network-flow integrality lemmas are welcome.
Policy gradient methods optimize a parameterized control policy by gradient descent on its long-run cost. They underlie much of modern reinforcement learning, from REINFORCE and actor-critic methods to trust-region and proximal policy optimization, and they are used in operations problems such as inventory control and optimal stopping. Their objective is almost never convex in the policy parameters, even in textbook problems, so the classical guarantees of first-order optimization do not explain why they reach good policies.
Bhandari and Russo (arXiv:1906.01786v3, Operations Research, 2024, doi:10.1287/opre.2021.0014) identify structural conditions under which this non-convex landscape is benign. Their Theorem 1 shows that, for a policy class closed under policy improvement, every stationary point is globally optimal. This mission formalizes their Theorem 2, the quantitative version: approximate stationarity implies approximate optimality, a gradient dominance (Polyak–Łojasiewicz-type) inequality that yields convergence rates.
Timeline. Polyak (1963) introduced the inequality for unconstrained problems. Kakade and Langford (2002) proved the performance difference lemma for finite Markov decision processes. Fazel, Ge, Kakade and Mesbahi (2018) established gradient dominance of policy gradient for linear-quadratic control, and Agarwal, Kakade, Lee and Mahajan (2021) for tabular policies with direct and softmax parameterizations. Bhandari and Russo (preprint 2019, journal 2024) give a single condition-based argument covering general state spaces and several of these examples.
A Markov decision process has a measurable state space , feasible action sets , a bounded expected cost , a transition kernel , a discount factor and an initial distribution . A stationary policy maps states to feasible actions; is the set of measurable such policies. Its cost-to-go is , its discounted state-occupancy measure is , and its loss is . An optimal policy has for every .
The Bellman operator is and is its optimality version. The weighted policy iteration objective is
A policy class is with convex, and the policy gradient objective is . For , the map is the single-period problem that one step of policy iteration within the class would solve.
A function is -gradient dominated over (, ) if for all
The hypotheses are Condition 0 (differentiability of in the policy and occupancy arguments), Condition 1 (closure: for every some minimizes over all of ) and Condition 2.B (each single-period objective is -gradient dominated over ). The effective concentrability coefficient is the smallest with for all , .
If Conditions 0, 1 and 2.B hold and , then
It is stated for every satisfying the concentrability inequality, which is the page's statement at .
The remark of §3 that differentiable -strongly convex functions are -gradient dominated and convex ones -gradient dominated, and Corollary 1: under Conditions 0 and 1, convexity (strong convexity) of every single-period objective makes gradient dominated of degree one (two).
Gradient dominance of degree two gives linear convergence of projected gradient methods, and degree one gives sublinear rates, so Theorem 2 converts structural knowledge about one-step policy improvement into iteration complexity for the multi-period problem. The constant makes explicit the dependence on the initial distribution: an exploratory with small is what the guarantee needs. The paper instantiates the conditions for tabular MDPs, linear-quadratic control, optimal stopping with threshold policies, and finite-horizon inventory control.
The result is proved in the paper. As far as is known, none of it is machine-checked: Mathlib has convexity, strong convexity, gradients and Markov kernels but no discounted dynamic programming on general spaces, no occupancy measures and no policy gradient theorem. The formal development would supply the general-space performance difference identity and the policy gradient theorem, reusable for every other result of the paper and for related work on policy optimization.
The policy gradient objective is not convex, so the usual derivation of a Polyak–Łojasiewicz inequality from convexity is unavailable. Gradient dominance of the single-period objective does not transfer to by comparing the two functions: they differ by how a change of policy moves the state distribution, these terms do not vanish, and the minimum of over is not the minimum of . The mismatch between , and is unavoidable, which is why a concentrability factor appears in the constants. On a general state space each identity also needs the right measurability and integrability (the measurable-selection assumption is what makes measurable), and Condition 0 must be strong enough to justify a total-derivative expansion.
All declarations live in PGLandscape.GradDom. and are arbitrary measurable spaces; the cost is bounded and measurable and, like the kernel, given on all of . Policies are measurable maps; the cost-to-go is a series of integrals against -step kernels; is a measure of total mass one. The parameter space is EuclideanSpace ℝ (Fin d), so is the Euclidean gradient and the norm. is for an optimal given as a hypothesis; no real infimum over policies is used.
Committed conventions and disclosed additions:
A formalization that assumes gradient dominance of , the closure bound, or a finite state space would not be this theorem; the goal assumes only Conditions 0, 1, 2.B and concentrability.
Contributions welcome: Markov-chain lemmas for iterKernel (summability, measurability, the fixed-point equation ), the general-space performance difference identity, and proofs of any milestone.
Policy gradient methods search for a policy by changing a finite vector of parameters. The method can reach a stationary point of its objective without finding an optimal policy: a small change in the available parameters might not represent the policy improvement that the underlying control problem calls for. Bhandari and Russo identify a condition on the policy class that limits this obstruction. Their exact-closure result rules out suboptimal stationary points; their approximate-closure result measures the residual cost when the class can represent policy improvements only approximately. This mission formalizes the latter statement, Theorem 5 of Bhandari and Russo, Global Optimality Guarantees for Policy Gradient Methods, using the arXiv v3 text and numbering.
The result concerns the optimization landscape rather than a particular gradient algorithm or convergence rate. It applies to structured policy classes in discounted control problems, including settings with general state spaces. The paper also discusses state aggregation as a source of small approximation error in Lemma 15; that example motivates the error condition, while the target here is the general guarantee of Theorem 5. The error is measured in the states visited by each current policy, so the condition describes what the restricted class can do where improvement affects that policy's performance.
A Markov decision process has a measurable state space , a measurable action space , and a nonempty feasible action set at each state . Choosing incurs a bounded cost and changes the state according to a probability kernel . A discount factor reduces future costs, and an initial probability measure specifies where evaluation begins. A stationary policy is a measurable choice .
The cost-to-go is the expected sum of discounted costs when starting at and following . The discounted occupancy measure is the normalized, discounted distribution of visited states when the initial state has law . The policy's objective is . The factor puts on the scale of a per-period cost. An optimal policy minimizes cost-to-go at every state. Section 2, pp. 5–8 supplies these objects and Assumptions 1 and 2: absolute continuity of with respect to , and measurable selection of a Bellman-minimizing action for bounded measurable value functions.
A parameter belongs to a convex set and determines a feasible policy . The policy gradient objective is . A stationary point is a feasible parameter with for every . The Bellman optimality operator selects the smallest one-step cost plus discounted future value among feasible actions. The weighted policy improvement objective evaluates the one-step Bellman update from a candidate policy , averaged under the current policy's occupancy measure. Section 5.1, pp. 12–14 introduces its smoothness and stationary-point conditions.
The target is Theorem 5, p. 26. Condition 5 says the restricted class has inherent Bellman error : for each current policy in the class, a class member gets within of the best one-step weighted Bellman objective over all feasible policies. Condition 2.A says stationary points of that weighted one-step objective are global minima over . Condition 0 supplies differentiability. For a nonnegative coefficient satisfying the effective concentrability inequality (13), the goal is continuous differentiability of and, at every stationary point,
The paper defines as the least coefficient satisfying (13). The Lean statement quantifies over an admissible ; its conclusion therefore includes the bound at when that coefficient is finite. The milestone list follows the paper's supporting statements: occupancy domination after (2), Bellman inequalities (5), the performance difference identity (29), the policy gradient formula in Lemma 6, the stationary policy-improvement identity in Lemma 7, and the Bellman-error bound displayed in the proof of Theorem 5.
The bound turns a property of the policy class into a quantitative guarantee about every stationary parameter. If and a finite concentrability bound applies, the stated cost gap is zero. For positive error, it separates the approximation error from the factor that reflects evaluation under the exploratory start distribution and the effective planning horizon. Thus a small gradient alone is not the claim; the structural conditions on the one-step objective and the policy class determine what stationarity means for long-run cost. Theorem 5 and its discussion, §8 make this interpretation explicit.
The paper proves Theorem 5. The declarations in this mission currently compile as open theorem statements; they are not machine-checked proofs. A complete development would formalize the links among discounted kernels, occupancy integrals, Bellman operators, and gradients on the parameter space. The general measurable-state MDP definitions would be reusable for other discounted control results, while the stationary-point and approximate-closure predicates provide a vocabulary for further policy-gradient theorems.
A stationary point of need not be a minimum of the one-step Bellman objective by definition. Condition 0 and Lemma 6 connect their gradients, and Condition 2.A then links stationary points to minima of the restricted one-step objective. Approximate closure only compares that restricted minimum with the unrestricted one up to . The final result also requires moving an error measured under to one under and relating Bellman residual to the optimality gap. Each comparison has a distinct measure or operator, and losing a discount factor changes the constant in the theorem.
The Lean model uses arbitrary measurable spaces for and and measurable stationary policies, extending the paper's Borel-subset setting. The cost and kernel are defined on all and are uniformly bounded there; feasibility still restricts every policy and Bellman minimization to . These extensions let Condition 0 evaluate nearby parameter values even when their policies need not be feasible. The representation uses Mathlib kernels, measures, Bochner integrals, and Euclidean parameter vectors. It fixes , a probability initial distribution, nonempty feasible action sets, an optimal policy, and the paper's Assumptions 1 and 2. The goal carries a nonnegative concentrability coefficient and Conditions 0, 2.A, and 5; it does not assume exact closure or the Bellman-error conclusion it is meant to establish.
Two corrections to the printed assumptions are explicit. The Bellman operators contain , consistently with equations (6) and (7), although displays (3) and (4) omit it. Condition 0 asks for joint continuous differentiability near the current parameter pair, the form used by the proof of Lemma 6; the printed condition lists two partial maps. The theorem's is constrained to be nonnegative to represent the paper's effective concentrability coefficient. Definitions use pointwise optimality rather than a real-valued infimum over policies, and Bellman minimization uses the nonempty feasible-action subtype. These choices prevent default values of ill-bounded infima or non-integrable functions from turning the target into an empty claim. The needed contributions are proofs of the six milestones and the final bound, plus supporting measurable-kernel and gradient facts.
Classical Markov decision theory minimizes expected cost. A decision maker who dislikes variability, such as an insurer, a portfolio manager or an operator of a service system, may instead evaluate a random cost by its certainty equivalent for an increasing utility (disutility) function . Bäuerle and Rieder (More Risk-Sensitive Markov Decision Processes, Math. Oper. Res. 39(1), 2014; authors' manuscript at KIT 1000039663) develop dynamic programming for this criterion with general . Classical risk-sensitive MDPs, studied since Howard and Matheson (1972), use the exponential utility, and for it the average cost problem differs considerably from the risk-neutral one (Cavazos-Cadena and Fernández-Gaucherand 2000; Di Masi and Stettner 1999). Their §5 asks what happens in the long run. The average cost per stage is evaluated through a power utility . Does risk sensitivity change which stationary policy is optimal?
This mission formalizes their answer, Theorem 5.2, and the results its proof uses (manuscript p. 17).
A controlled Markov process in discrete time has a standard Borel state space and action space . A measurable set lists the admissible state–action pairs, and every is nonempty. A transition law gives the distribution of the next state, and a measurable cost satisfies on .
A history-dependent policy chooses the action measurably from the past. The set of all such policies is . Each and initial state determine a probability measure on trajectories, with and . The accumulated cost is .
A stationary policy uses a measurable decision rule with at every stage. Under it, is the Markov chain with kernel .
Fix and . The risk-sensitive average cost (5.1) and its optimal value are
The risk-neutral average cost is , the case .
A Markov chain is Harris recurrent if, for some nonzero -finite measure , every set with is visited infinitely often almost surely from every starting point. It is positive Harris recurrent if it also has an invariant probability measure (Meyn and Tweedie 2009, §§9–10). The MDP is called positive Harris recurrent if the state chain of every stationary policy is.
Let and let the MDP be positive Harris recurrent. If satisfies for all and , then
The optimal policy does not depend on .
The result. Theorem 5.2 reduces a risk-sensitive long-run problem to a classical one. Under positive Harris recurrence, any stationary policy that is optimal for the expected average cost, for instance one obtained from the average-cost optimality equation, is also optimal for every convex power criterion , simultaneously. Theorem 5.1 explains why: along a positive Harris recurrent chain the empirical average cost converges almost surely to a constant, so in the limit the power utility sees no randomness at all. The contrast is with exponential utility, where the risk-sensitive average cost generally differs from the risk-neutral one and leads to a multiplicative Poisson equation. Positive homogeneity of the utility is what removes the risk effect.
Formalizing it. The results are proved in the paper. As far as is known they have no machine-checked proof, and the platform has no strong law of large numbers for Harris chains on general state spaces. The mission produces a Borel MDP with history-dependent policies and Ionescu-Tulcea path measures, a reusable definition of (positive) Harris recurrence for an arbitrary Markov kernel, and a formal comparison of risk-neutral and risk-sensitive average costs. Each milestone is a self-contained target.
Milestones 1 and 3 are elementary once the expectations are handled correctly: holds only almost surely, and Jensen's inequality has to be applied with real powers. The central difficulty is Theorem 5.1. It needs the ergodic theorem for positive Harris recurrent chains, almost surely from every initial state (Meyn and Tweedie, Theorem 17.0.1). It also needs an identification of the state process under with the canonical chain of . The natural first idea, to quote a convergence theorem in total variation, fails: positive Harris recurrence allows periodic chains, for which need not converge. Pathwise averages converge, marginal laws need not, and the argument has to work with the former.
Kernel.trajMeasure on . Stationary policies act through .Real.rpow. For all terms of the sequences lie in , so real limits superior are meaningful. The term (Lean's ) is irrelevant.Contributions are welcome at every level. Reusable pieces, such as the identification of the state process with the chain of , the strong law for positive Harris chains, or bounded-convergence lemmas for path measures, are valuable beyond this mission.
Sequential decisions often have costs whose timing matters. A controller may choose an action now, observe a random next state, and choose again. Ordinary expected-cost minimization averages the sum of the costs. A risk-sensitive criterion first applies an increasing function to the total cost and then takes its expectation. The curvature of changes how uncertain costs affect the ranking of policies: convex utility penalizes variability in a cost-minimization problem, while concave utility has the opposite tendency. Bäuerle and Rieder study this criterion for controlled Markov processes with general continuous increasing utility, rather than fixing an exponential function. Their finite-horizon discounted result is Theorem 3.6, pp. 10–12 of the authors' manuscript.
Discounting gives early and late costs different weights. For linear , the remaining expected cost can be described using only the current physical state. For general , the effect of a future cost also depends on what has already been paid and on the discount weight currently attached to the next cost. The mission targets the paper's finite-horizon treatment of these two additional quantities. The infinite-horizon problem is a separate part of the paper.
The state space and action space are Borel spaces. At state , the nonempty set contains the actions that may be chosen. If action is selected, the next state has distribution and the stage cost is . The cost is measurable and bounded between positive constants and . The discount factor satisfies , and is continuous and strictly increasing. The paper imposes its compactness and continuity conditions (CC) on , , , and ; these are stated in the model item and correspond to §2, pp. 3–4.
A history policy chooses measurably from the states and actions observed through time . Starting from , it induces a law for the state-action trajectory. The first stages incur the discounted cost , with . The paper minimizes over every admissible history policy. The inverse utility appearing in the paper's original certainty-equivalent criterion can be omitted when selecting a minimizer because is strictly increasing §2, p. 3; §3.3, p. 10.
The extended state is . Its coordinates record the current physical state, accumulated cost, and current discount weight. Define and . A measurable extended-state decision rule chooses an action in . The paper's operator integrates a continuation value at ; takes the infimum of the same integral over equations (3.8)–(3.9), pp. 10–11.
The first target identifies the cost iteration of any sequence of extended-state rules :
The second target is the paper's value iteration for the infimum over all history policies, together with membership of every in its regularity class :
The goal is Theorem 3.6(c): minimizers of exist, and their stage-dependent history rules attain the original objective for every . At stage , the rule uses at the current state, the observed sum , and . “Optimal” compares against all admissible history policies, including those that use more of the history than these three quantities.
Theorem 3.6 gives a finite sequence of minimum-operator evaluations for a problem whose utility of total cost is not additively separable in the physical state alone. Its policy statement also identifies which observable quantities an optimal controller needs to retain. Together, these results relate the original history-dependent problem to an extended-state Markov decision problem §3.3, pp. 10–12.
The paper proves these statements. This mission asks for machine-checked definitions and proofs of the finite-horizon discounted theorem, including the comparison with all admissible history policies. The model layer and the finite-dimensional expectation construction can support later formalizations of other risk-sensitive objectives. The mission itself has no completed proof at the drafting stage.
The extra discount coordinate is essential: after one action, the next cost enters utility with weight , not . Keeping only accumulated cost would describe a different process. The other demanding point is the policy comparison. An iteration over extended-state decision rules has to establish the value of an infimum over arbitrary measurable history policies. Regularity and measurable selection must also be maintained at each step under (CC). The proof of Theorem 3.6 invokes the corresponding total-cost argument from Theorem 3.1, pp. 5–6; the formal development must supply the precise discounted version.
Lean represents and as Borel subsets of Polish spaces, with standard Borel measurable structures. The controlled process is a separate reusable definition containing , , and history policies; the risk-sensitive model adds , , and . The admissible graph is Borel and every section is nonempty. A history is a chronological finite list of earlier state-action pairs and a current state. Each rule is defined on all lists, but only admissible lists of the matching length are visited. The transition kernel is total as a Lean object, and its values outside are irrelevant.
Policy values use nested kernel integrals representing the finite-dimensional marginals of the path law. They are defined from the cost and utility, so the Bellman recursion remains a theorem. The optimized value is an infimum over the subtype of measurable, admissible infinite history policies. The real infimum is meaningful here because this policy class is nonempty under (CC) and finite-horizon costs keep utility bounded on the relevant interval. The extended state uses real coordinates restricted to and ; its transition stays in that domain. “Increasing” in means componentwise nondecreasing in . A minimizer is an admissible measurable rule satisfying on the entire extended domain.
The source's proof sentence that preserves is recorded with explicit integrability of each one-step continuation. For an arbitrary real-valued member of on an unbounded state space, the source's conditions alone do not ensure a finite real expectation. This domain condition prevents Lean's zero value for a nonintegrable real integral from turning the assertion into a different one. It does not narrow the finite-horizon values appearing in the goal. Contributions toward finite-dimensional expectation identities, kernel integrability, the regularity of , and measurable minimizer selection are within scope.