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.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
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?
Firms that buy from unreliable suppliers face two broad remedies: spread orders across several suppliers (dual sourcing), or invest in making a supplier more reliable (process improvement). Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), compare the two in a single newsvendor model in which suppliers deliver less than ordered because of random capacity losses. This mission covers the first half of that comparison: the pure dual-sourcing strategy, in which the firm improves nobody and only chooses how much to order from each of two suppliers.
A single-supplier random-capacity model was studied by Ciarallo, Akella and Morton (Management Science 40(3), 1994); in that model, as the paper notes, the firm never orders more than demand to hedge against capacity shortfall. Dada, Petruzzi and Schwarz (M&SOM 9(1), 2007) studied several unreliable suppliers but gave only necessary conditions for optimal orders. The paper states necessary and sufficient conditions for two suppliers (its Theorem 1) and, for deterministic demand, a closed-form optimal order in each of six demand regions (Theorem 2). Its proofs are in an online appendix.
A product sells at unit revenue , is salvaged at , and unmet demand costs per unit, with . Two suppliers have unit cost , committed-cost fraction and design capacity . Supplier suffers a random capacity loss whose continuous distribution function depends on a reliability index : a larger index makes the loss stochastically smaller, for . The losses are independent of each other and of demand , which has distribution function .
For an order vector , supplier delivers and is paid . The realized profit is
and the second-stage expected profit is . With and this is the paper's Eq. (3). The optimal value is , and an optimal procurement vector is a attaining it.
Let demand be deterministic, , let , let , let each be strictly increasing on a support with , and let . With , , and , an optimal vector is
In – the firm orders more in total than demand: the quantity hedge.
Theorem 2 is the paper's explicit description of how a buyer splits orders between two unreliable suppliers: single sourcing when capacity is ample, dual sourcing at total order equal to demand, then deliberate over-ordering, and finally ordering full capacity. The quantity hedge is the paper's main qualitative finding for dual sourcing, since, as the paper notes, over-ordering of this kind does not occur with one random-capacity supplier. Corollary 1 says how this hedge responds to reliability, which is the comparison with process improvement that the rest of the paper builds on; Lemma 2(b) is the value of reliability used there.
None of these results has a machine-checked proof, and the paper's proofs are in an online appendix not used here. A formalization would also settle the printed statement, which contains a slip (below) that a formal proof must avoid.
is submodular but not jointly concave in , so the usual route (concavity plus first-order conditions) is not available, and the paper invokes unimodality instead. Under deterministic demand is not differentiable on the line , where the and optima sit, so Theorem 1 cannot simply be specialized to Theorem 2: optimality there needs one-sided arguments. In every region the claim is global optimality over all , including orders above the design capacities, and the feasible set is unbounded.
Suppliers are indexed by Fin 2 (index 0 is supplier 1). The capacity losses are a family of probability measures on without atoms and with , and is their distribution function. is the Bochner integral of against for a demand law . Every theorem assumes is a probability measure on with finite mean. Deterministic demand is . Theorem 1 and Eq. (6) add Lebesgue (the paper's density). "Optimal" means a global maximizer over , and "increasing" is weak, as the paper declares. Added standing hypotheses: , , and , which bound above so that is a genuine supremum. is the generalized inverse .
Corrections to the printed Theorem 2, each disclosed in its item:
Theorem 1's "" is read as . Lemma 2(a) is not formalized: optimal orders are not unique and no reading of " is increasing" was found that is both faithful and safely true.
Stating Theorem 2 as " satisfies the first-order conditions", or optimality only within a region's face, would trivialize it; the statement requires for every . Proofs need integrals of piecewise-linear functions of independent variables, differentiation under the integral sign, and facts about generalized inverses of continuous distribution functions. Lemma 1 and the generalized-inverse facts are reusable beyond this mission; proofs of any milestone are welcome.
In a linearly parameterized bandit a decision maker repeatedly chooses an arm from a set and observes a noisy reward whose mean is linear in an unknown vector . The model covers problems in which many arms share a few underlying features: products described by a handful of characteristics, prices, or routes whose costs depend on a few parameters. Because the arms are correlated through , a good policy can learn about every arm from the rewards of any arm, and its regret can be made to depend on the dimension instead of on the number of arms, which may be infinite.
Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, published in Mathematics of Operations Research, 2010) prove an lower bound on the regret when the arms form the unit sphere, give a matching phase-based policy for strongly convex arm sets, and propose the Uncertainty Ellipsoid (UE) policy for arbitrary compact arm sets. The UE policy is close to the algorithms of Auer (2002) and Dani, Hayes and Kakade (2008), with two differences: it does not need to know the horizon , and it allows and the noise to be unbounded. This mission formalizes its regret bound for general compact arm sets, Theorem 4.1 of the paper.
Fix and a compact set of arms , with the Euclidean norm . Playing arm in period yields
where the noises are independent of each other and of , identically distributed in for each arm, and have mean zero. A policy chooses the arm of period as a function of the history . The regret given and the Bayes risk are
Assumption 1 (p. 13) fixes constants such that, for every : (a) for every arm and every ; (b) every arm has , and contains linearly independent arms with .
The UE policy keeps the ordinary least squares estimate , where , and, with and , the uncertainty radius
It plays in the first periods and then, in each period , an arm maximizing over , with ties broken arbitrarily.
There are constants depending only on such that for every , every compact arm set satisfying Assumption 1, every run of the UE policy, all and all ,
The constants are not fixed: any positive values that work suffice.
The proof in Appendix B proceeds through large deviation inequalities for adaptive least squares (Theorem B.1 for finitely many arms; Lemmas B.3, B.4, B.5 leading to Theorem B.2 for infinitely many), the radius bound (Lemma B.6), the instantaneous regret bound (Lemma B.7), the regret decomposition
(Lemma B.8), and the deterministic Lemmas B.9–B.11, which bound by the value of an optimization problem and that value by .
Theorem 4.1 shows that one policy achieves regret within a factor of the lower bound for every compact arm set, finite or infinite, with sub-Gaussian unbounded noise and without knowledge of . The dependence on the problem is only through and the three constants of Assumption 1; the number of arms does not appear. The large deviation inequalities of Appendix B.1 are also the input of the paper's Theorem 4.2 for finitely many arms.
The result is proved on paper; no machine-checked proof of it is known. A formal development would produce reusable components that are currently absent from Mathlib: a Chernoff-type bound for least squares estimates built from adaptively chosen regressors, the self-normalized inequality of De la Peña, Klass and Lai in the form of Lemma B.3, the determinant recursion behind Lemma B.9, and the law of a bandit history driven by a policy and an arm-dependent noise kernel.
The arms depend on past noise, so with is not a sum of independent terms with fixed weights, and the classical Chernoff bound does not apply. For finitely many arms a union bound over the possible pull counts suffices (Theorem B.1), but its bound grows like and is useless for infinite arm sets. Theorem B.2 instead needs a self-normalized martingale inequality and a covering argument over directions to compare with in the Loewner order. A second difficulty is that the sum of the radii played is not bounded term by term: each term can be as large as , and only the multiplicative recursion of Lemma B.9 shows that large terms are rare.
is EuclideanSpace ℝ (Fin r), so norms are Euclidean. The constants are written ubar, lam0. Policies are deterministic, history-dependent and measurable (measurability is implicit in the paper). The noise is a Markov kernel giving the law of for each arm; the history given is built period by period with fresh independent noise, which is the law of the paper's history. Assumption 1(a) is a bound on a lower Lebesgue integral, so it also asserts finiteness; is . The standing assumptions of Sec. 1.1 (compact , , independent mean-zero noise identically distributed in ) are hypotheses. equals for an infinite arm set. A UE run is any measurable policy that plays first and then a maximizer of after every history that starts with ; on those histories is a genuine inverse.
Deviations from the page, all disclosed in the items: Lemma B.4 is printed for but its proof needs , and at the printed claim fails; it is stated for . Lemmas B.4 and B.5 are printed without "" and are stated for each fixed , the form in which the paper uses them. Lemmas B.9 and B.10 ("with probability one") are stated for every arm sequence that starts with and stays in the ball of radius , which is stronger. Theorem B.1 carries the hypothesis that is finite.
The regret is minus the expected total reward, whose integrand is bounded, so it is never a junk value; the risk bound asserts integrability of the regret in and assumes . The constants are chosen before , the arm set and the instance, so a formalization in which they depend on or on does not prove the goal.
Welcome contributions include proofs of any milestone, in particular the deterministic Lemmas B.9–B.11, and reusable lemmas on matrix determinants, self-normalized bounds and bandit history measures. The source is arXiv:0812.3465v2; its printed page numbers equal the PDF page numbers.
A set of vertices of a graph is a metric generator when every vertex is determined by its vector of distances to the elements of . The minimum size of such a set is the metric dimension, studied in graph theory since the 1970s and surveyed by Chartrand, Eroh, Johnson and Oellermann (Discrete Appl. Math. 2000). Metric generators also appear in combinatorial search, where identifying a vertex from distance queries is the same as weighing false coins.
Sebő and Tannier (Math. Oper. Res. 2004) ask a converse question. Suppose an isometric copy of is already placed inside a second graph . When does that placement extend to an isometric embedding of the whole graph into ? With the question contains clique detection and is NP-hard (p. 385), so the interest lies in hypotheses on that make it tractable. The paper's answer, Theorem 4, is the tool behind its main application: deciding whether a graph has a connected minimum -join (§3.2), a question raised by Frank (1996).
All graphs are finite, simple, undirected and connected. For a graph , is the number of edges of a shortest path between and .
In Lean these are IsMetricGenerator, IsStrongMetricGenerator, IsIsometry, IsIsometryOn, Extends, Represents, candSet, cand and cStar in the namespace MetricGenerators.IsometryExt.
Let be a strong metric generator of with a forest, and an isometry. Then
and if exists, is a representation with for every representation , so it is the unique inclusionwise maximal one.
A further theorem states the criterion behind Corollary 1 (p. 389): an extension exists iff every is nonempty.
Theorem 4 turns a global question (does an isometric embedding with prescribed values on exist?) into a local one about adjacencies among candidate sets, and the procedure settles it in at most rounds. In §3.2 of the paper the theorem is applied to a tree with its set of leaves (all but one leaf forms a strong metric generator, Theorem 3), and this yields the characterization and polynomial-time recognition of graphs with a connected minimum -join. Without the forest hypothesis the characterization fails: Figure 2 of the paper gives a representation, with a triangle in , for which no extension exists.
The result is proved in the paper. To our knowledge none of it has a machine-checked proof: Mathlib has graph distances (SimpleGraph.dist), acyclicity and induced subgraphs, but no metric generators, no isometry-extension results and no metric dimension. A formal proof would provide that vocabulary and a verified decision criterion. It would also be the first step towards formalizing the -join application of the same paper.
The necessity half and the maximality of are bookkeeping. The difficulty is sufficiency: from a representation one must build an actual isometry. The obvious idea is to pick any for every , but this fails: two independently chosen candidates for adjacent vertices need not be adjacent, and condition (ii) only guarantees some adjacent partner. The choices must be coordinated along . Even with coordinated choices, the distance between images must be bounded above along every shortest path of , including paths that leave one component of , pass through , and return. Figure 2 shows that without the forest hypothesis no such choice need exist. Lemma 1 supplies the matching lower bound, and its proof needs the strong generator property, not just the metric-generator property.
Fintypes; graphs are SimpleGraphs, and both and are assumed Connected in every statement. SimpleGraph.dist is -valued and equals on unreachable pairs, so connectivity is load-bearing.Finset of vertices of ; is a function on the subtype of , so it has no values outside .H.induce (↑T)ᶜ, and "forest" is IsAcyclic. is allowed.Sets; the recursion follows the page's union form, and is the stage .Represents. Without it the empty family would represent every and the right-hand side of the goal would be trivially true. "Unique inclusionwise maximal" is stated as "a representation containing every representation".sInf.Reusable infrastructure: metric generators and strong metric generators of graphs, isometries between graph metrics, and lemmas relating SimpleGraph.dist to shortest paths through a vertex. Contributions are welcome on any milestone and on general SimpleGraph.dist lemmas they need.
Monotone variational inequalities (v.i.) cover convex minimization, convex–concave saddle-point problems, Nash equilibria of convex games and complementarity problems. Matrix games and other large saddle-point problems are typical cases. At large scale, first-order methods that use only values of the operator and simple auxiliary minimizations are the practical tool. The paper's introduction (pp. 229–231) contrasts this with the black-box lower bound of order evaluations for nonsmooth Lipschitz minimization, and with Nesterov's smoothing method (2005), which reaches for structured saddle-point objectives. The paper states that its complexity estimate is new, to the author's knowledge, even in the Euclidean case, where the scheme is Korpelevich's extragradient method of 1976.
A. Nemirovski, Prox-Method with Rate of Convergence O(1/t) for Variational Inequalities with Lipschitz Continuous Monotone Operators and Smooth Convex-Concave Saddle Point Problems, SIAM J. Optim. 15(1):229–251, 2004 (doi:10.1137/S1052623403425629), introduced what is now called the mirror-prox method. It showed that two prox steps per iteration give an ergodic error of order when the operator is Lipschitz continuous, and that the bound holds in an arbitrary norm, adapted to the geometry of the feasible set by a distance-generating function. The method and its analysis underlie later work on smooth saddle-point problems, including Nesterov's dual extrapolation and Juditsky–Nemirovski–Tauvel's stochastic mirror-prox (2011).
Let be a finite-dimensional real vector space with an arbitrary norm , not necessarily Euclidean. Dual vectors act on by , and the conjugate norm is . Let be nonempty, convex and compact.
The operator maps to dual vectors and satisfies (2.1): it is -Lipschitz, , and monotone, , for all . A solution of the v.i. is a point with for all . The accuracy of a candidate is
The distance-generating function is continuously differentiable on and strongly convex with modulus in the form (2.2): . The prox-mapping is
and the constant measures how far extends from the starting point in the geometry of .
The basic implementation fixes the stepsize (3.2). At step it computes and checks the test (3.4),
for . If the test passes, and . Otherwise and . The output after steps is the average of the points .
For every run of the basic implementation, (3.4) holds at every step, so two inner iterations always suffice, and for every
Lemma 2.1 (2.4), Lemma 3.1 (3.7.b) and Remark 2.3 are also stated as companion theorems.
The theorem gives an bound for monotone Lipschitz v.i. and for smooth convex–concave saddle points at a cost of two operator evaluations and two prox problems per step. With a distance-generating function adapted to , the paper derives rates that are, in its words, nearly dimension-independent under favorable circumstances, for matrix games, eigenvalue minimization and the Lovász capacity number (§5). In the Euclidean case the method is Korpelevich's extragradient method, so the theorem also gives an ergodic rate for that method.
The result is proved in the paper; no machine-checked proof of it is known. The platform has a formalized statement of mirror prox for minimization of a smooth convex function (Bubeck's Theorem 4.4), which uses a mirror map on an open set and a function-value gap. It does not cover operators, the v.i. accuracy measure or a prox-mapping over a compact set. This mission produces the general v.i. version, with an arbitrary norm and a distance-generating function defined only on .
The algebra of each step is short. The work is in three places. First, the first-order optimality conditions of the constrained prox problems, (2.6) and (3.8), must be derived when is only a derivative within , and may have empty interior. Second, (3.7.d) needs the function-value form of strong convexity, , which must be derived from the monotonicity form (2.2) along segments of . Third, the telescoping of (2.15) uses the identity for , and the passage from the weighted sum to the average uses monotonicity of .
The natural first idea is to prove that the inner map is a contraction, observation (3.1), and iterate it to a fixed point. That gives only a geometric number of inner steps, not two. The two-step bound comes from Lemma 3.1, which decouples the two prox steps and compares them through strong convexity.
Dual vectors are continuous linear functionals E →L[ℝ] ℝ on a finite-dimensional normed space E, and is the operator norm. This is equivalent to the paper's Euclidean space with a second norm. is assumed convex, compact and nonempty in every item. has a derivative within that is continuous on , and (2.2) is assumed in the monotonicity form. The prox-mapping is the relation " minimizes over ". and are suprema over the image of , which are maxima under these assumptions. The paper's indices are kept: z 0 is , and step goes from z t to w (t+1) and z (t+1).
Disclosed choices: and are hypotheses, because (3.2) and (3.9) divide by them. The termination test (2.8) is not modelled, so runs never stop; this only adds runs. The basic implementation's inner loop is cut at , which is what the goal's first claim justifies. The bound on is stated for every , which is equivalent to the bound on the maximum. Items that use only monotonicity of , or no property of , do not assume the rest of (2.1).
The goal quantifies over every run, and a sorry-free sanity file exhibits a run on , so the run relation is not empty. The average is over the , not the . The suprema are taken over compact nonempty with continuous , so they are not junk values. The saddle-point form (3.10), the bound (2.14) and Theorems 4.1–4.2 are not posed.
Useful contributions: optimality conditions for minimizers of functions differentiable within a convex set; the function-value form of strong convexity derived from (2.2); and the Legendre-transform identity. All three are reusable for other mirror-descent and prox-method analyses.
A retailer that carries several substitutable products, such as brands of the same item, loses part of a customer's demand when the preferred product is out of stock, but not all of it: some customers buy another product instead. How much of each product to stock then depends on the stocking levels of the others. When all products are managed by one company, the stocking problem is a joint optimization; when each product is managed by a separate firm, it is a game, and each firm ignores the effect of its stock-outs on its competitors.
A common view in the inventory literature is that competition drives inventories up for every product. Mahajan and van Ryzin and Lippman and McCardle demonstrated it in special cases (Lippman & McCardle, Operations Research 1997; Mahajan & van Ryzin, Columbia working paper 1999, published in Operations Research 2001). Netessine and Rudi (SSRN 303779, 2002, later published in Operations Research, 2003) study the general model with products, an arbitrary continuous joint demand distribution, and arbitrary substitution fractions. They show that the common view fails in general: some products may be stocked more under centralized management (Proposition 6(i)), but at least one product is always stocked no less under competition (Proposition 6(ii)). This mission formalizes Proposition 6(ii) and the centralized first-order analysis on which it rests.
There are products, indexed , sold in a single period. Product is stocked at units at unit cost , sold at unit price , and salvaged at unit value , with . Write (the underage cost) and (the overage cost).
The first-choice demand vector is random, with a known continuous joint law on the positive orthant. A fraction of the unmet demand for product switches to product , with and ; a customer whose second choice is also out of stock is lost. The effective demand for product is
Under centralized management a single company maximizes the expected profit
over all ; a maximizer is written . Under competition firm chooses to maximize
given the other firms' quantities; a Nash equilibrium is a vector at which no firm gains by changing its own quantity. In the Lean development these objects are Model, Ds, centralProfit, IsCentralOptimal, firmProfit, IsBestResponse and IsNash in the namespace DemandSubstitution.Comparison.
For every optimal centralized stocking vector and every Nash equilibrium ,
The statement quantifies over all optima and all equilibria; it asserts neither existence nor uniqueness of either.
Proposition 6(ii) bounds how far competition can depart from the centralized solution in the downward direction: it can never make every product understocked. Together with Proposition 6(i), it shows that neither "competition overstocks everything" nor its opposite holds in general, and it is the step from which the symmetric case, Proposition 6(iii) (every product is stocked at least as much under competition), follows. The centralized condition (7) and the derivative (8) are of independent use: they give the first-order conditions of the multi-product newsvendor with stock-out substitution for an arbitrary number of products and an arbitrary continuous demand law, obtained without Leibniz-rule integration over polyhedral regions.
The results are proved in the paper; none of them has a machine-checked proof. A formal proof requires differentiating an expectation of piecewise-linear functions of the demand under the integral sign, and handling the measure-zero boundaries where those functions have kinks. That machinery is reusable for other multi-product newsvendor models.
The centralized profit is not concave in general for three or more products (the paper's own example, pp. 3–5), so the optimum cannot be characterized as the unique solution of first-order conditions: the argument must work with an arbitrary maximizer and use only the necessary condition at an interior coordinate. The derivative (8) must be justified as a two-sided derivative of an integral whose integrand is not differentiable on hyperplanes in demand space; the paper's difference quotient argument leaves the boundary terms implicit. Finally, the obvious comparison of the two first-order conditions yields only an inequality between probabilities; turning it into an inequality between stocking levels requires the distribution function of to be strictly increasing, and an optimal may be zero, where (7) does not hold.
Products are Fin n (0-based). The model data and the standing assumptions , , , are fields of a structure Model n. The demand law is a probability measure on that is absolutely continuous with respect to Lebesgue measure, is concentrated on the open positive orthant, and has integrable coordinates (IsDemandLaw). Expectations are Bochner integrals and probabilities are μ.real of sets with the strict and weak inequalities exactly as printed. Derivatives are two-sided HasDerivAt in one coordinate, the others held fixed through Function.update.
Three hypotheses are pinned relative to the page and disclosed in the statements:
NeZero n in the goal: for "at least one " is false.HasPositiveDensity μ in the goal: a Lebesgue density strictly positive on the open positive orthant. The paper's last step uses strict monotonicity of the distribution function of without stating it.The centralized optimum is a maximizer of over nonnegative vectors and the Nash equilibrium is the no-profitable-deviation property over nonnegative quantities. Defining either by its first-order condition ((7) or (10)) would turn the propositions into definitions and is ruled out. Stating the goal for one chosen optimum or equilibrium is ruled out as well: it holds for every pair.
Contributions welcome: differentiation of expectations of piecewise-linear functions under absolutely continuous laws; null-set lemmas for ; Fermat's rule at a coordinate-wise interior maximizer; the Nash condition (10) of the competitive game, which milestone 5 needs and which is also posed in the companion mission on equilibrium existence.
Barabási and Albert (Science 1999) proposed preferential attachment as a mechanism behind the heavy-tailed degree distributions observed in the web graph and other networks: vertices arrive one at a time and attach to existing vertices with probability proportional to their degree. Empirical work on such networks reported that typical distances are very small compared with their size. The original description left the model underdetermined (the joint law of the edges of a new vertex was not specified), so its distances could not be analysed as stated.
Bollobás and Riordan (Combinatorica 2004) fixed a precise version of the model, the LCD model, and determined its diameter: for edges per vertex it is asymptotically . For the graph is a forest (with loops), and a result of Pittel states essentially that its diameter is of order . Together with the degree-sequence analysis of Bollobás, Riordan, Spencer and Tusnády (Random Struct. Alg. 2001), the paper is one of the first rigorous results on a scale-free random graph model.
The process . Vertices are . Vertex sends a single edge to a vertex , chosen given the past with
where is the degree of in the graph built so far (a loop counts twice). Loops () are allowed.
The graph . Run and identify the vertices into a single vertex , for . The resulting random graph on is . The paper's graph has loops and multiple edges; its diameter is the largest graph distance between two vertices of the underlying simple graph.
Almost every. For fixed , a.e. has a property if its probability tends to as . All logarithms are natural.
The endpoint model (for the upper bound). Let be independent with density on (), their sorted values, , , . Given , the random graph joins each vertex to and , independent with for . The events (Lemma 7) say that the follow the profile and that the spacings are neither too small nor too large in specified ranges.
For fixed and , a.e. is connected and
The theorem shows that the diameter of this scale-free graph is smaller by a factor than that of a classical random graph with the same constant average degree, and identifies versus as the dividing line. It made the "small world" claims about the Barabási–Albert model precise for one exact version of it, and the LCD representation and the endpoint model introduced here were used in later work on preferential attachment.
The result is proved in the paper; nothing here is open. The work of the mission is formalizing the known proof. As far as is known, no machine-checked development of preferential-attachment graphs exists in Mathlib or elsewhere. A complete development would supply a reusable probability space for the attachment process, a Chernoff–Janson inequality for heterogeneous Bernoulli sums, a negative-correlation lemma for the process, and order-statistic estimates for i.i.d. samples, each of independent use.
The lower bound is a first-moment count of short paths, but the edges of are not independent: an earlier edge into a vertex raises the chance of later ones. Lemmas 2–4 show that small subgraphs still appear with probability comparable to an independent model with edge probabilities ; Lemma 3 requires a description of the process in which the needed independence is visible.
The upper bound is the hard half. A naive breadth-first expansion from a vertex fails: the weight of the next neighbourhood has the right mean but a very skewed distribution, and vertices near the end of the ordering have few early neighbours. The paper replaces the process by a conditionally independent model given the sorted endpoints , controls the globally (Lemma 7), handles late vertices separately (Lemmas 8–10), and runs a weighted expansion with a growing blow-up factor (Lemmas 11–12). Each step needs uniformity in : every must depend on only.
Vertices are stored as Fin N (0-based) and statements read 1-based labels through the accessors tgt and lab. A sequence is a dependent function (t : Fin N) → Fin (t+1), its probability is the product of the exact conditional factors , and probabilities are finite weighted sums. , and are Mathlib simple graphs: loops and multiple edges are dropped, which does not change connectivity or distances. The model is the paper's: not uniform attachment, not independent choices per vertex, and with the self-loop term.
in the goal is SimpleGraph.diam, which is on a disconnected graph; the goal therefore keeps connectivity explicit, as the page does. Every other diameter bound uses "every two vertices are joined by a walk of length ", and lower bounds use its negation, so a disconnected graph never satisfies an upper bound by default. Hidden constants follow the paper's quantifier order: the constants of Lemmas 2 and 4 come before every index; each of §§7–8 is a function chosen before (a bound chosen after would make these statements nearly empty); "for sufficiently large" is before or . Theorem 5 assumes the bound of Lemma 4 for its constant . Every statement about assumes . Lemma 7 is stated as "the probability of the complement tends to " under the product law of ; the coupling is stated as the equivalent stochastic-domination inequality for every property preserved under adding edges.
Not formalized: Lemma 9 (a conditional bound given the history of a breadth-first exploration), the LCD representation of (§2), and Theorem 13 (), which the paper states without proof.
Contributions welcome: proofs of any milestone, the identity with , the LCD representation, and general lemmas about the attachment process and Bernoulli tails.
Obstacle problems, contact problems and control-constrained optimal control problems lead, after discretization, to complementarity systems of the form "find and with and ". The primal-dual active set strategy solves such systems by guessing which constraints are active, solving one linear system, and updating the guess. It is widely used because each iteration is a single linear solve and, in practice, it terminates after few iterations.
Hintermüller, Ito and Kunisch (SIAM J. Optim. 13(3), 2002; authors' version hal-01660511v1) showed that the strategy is a semismooth Newton method applied to a reformulation of the complementarity system with a max-function. This gives local superlinear convergence. For global convergence, from arbitrary initial data, the paper gives three sufficient conditions on the matrix : the M-matrix case (Theorem 3.2), the condition of Theorem 3.3 treated in this mission, and small perturbations of M-matrices (Theorem 3.4). Theorem 3.3 is the one that goes beyond sign patterns: it covers P-matrices whose blocks satisfy a norm bound and a cone condition, with the sum of the components of serving as a merit function.
Fix , a matrix , vectors and a parameter . Vectors are ordered componentwise. The problem is
with the maximum taken componentwise. In the paper's notation the matrix is and the index sets are calligraphic: (active) and (inactive).
A P-matrix is a square matrix all of whose principal minors are positive. For an index set with complement , is the principal submatrix of on , and is the submatrix with rows in and columns in . For a P-matrix every is invertible.
The primal-dual active set algorithm starts from an arbitrary pair . Given it sets
and determines from
For a rectangular matrix , is the matrix of the positive parts of its entries, and is the matrix norm subordinate to the one-norms, i.e. the maximal absolute column sum. Thus .
If is a P-matrix and for every partition of into disjoint sets and
then for every solution of (3.1) and every run of the algorithm, .
The proof in the paper passes through the following claims, in order: the sign facts and for ; the update formula on the inactive set derived from the Newton system (3.3); inequality (3.6); inequality (3.7),
and the fact that a repeated active set yields a solution of (3.1).
Existence of a run from every initial pair when is a P-matrix; Remark 3.3 (an M-matrix satisfies the conditions of Theorem 3.3); and the stronger conclusion of the proof, that every run reaches after finitely many steps.
Theorem 3.3 gives global convergence of the primal-dual active set strategy for a class of matrices that is not restricted to M-matrices, and identifies as a merit function under its two conditions. The paper points out that the result applies to discretizations of control-constrained optimal control problems, where the system matrix is generally not an M-matrix, and Remark 3.3 shows that the M-matrix case falls under it.
The result is proved on paper; none of it has been machine-checked. A formal development would produce a checked global convergence theorem for a semismooth Newton method, together with reusable statements about principal blocks of P-matrices and the subordinate one-norm of a positive part. The step from "the merit function does not increase" to convergence is the part of the paper's argument that a formal proof has to make fully precise (see below).
The obvious route is the paper's: show that decreases strictly until the active set repeats, conclude that no active set can recur, and use finiteness of the set of possible active sets. The inequalities (3.6) and (3.7) give only a non-strict decrease. The paper's assertion ", unless " does not follow from them as written: the right-hand side of (3.7) vanishes when on , and the cone condition permits with . A complete proof has to exclude cycling among active sets at equal merit value by a further argument. That is the central difficulty of this mission, and the reason the strict part of (3.7) is not stated as a milestone.
Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ; index sets are Finset (Fin n) and blocks are submatrices along the subtype inclusion. The P-matrix predicate is the published definition RobinsonSR.Schur.IsPMatrix (every nonempty principal minor is positive). The algorithm is encoded as a relation between consecutive iterates, and a run is an infinite sequence related step by step with arbitrary initial data; the stopping option of the algorithm is not modelled. The solution of (3.1) enters as a hypothesis: for a P-matrix it exists and is unique, so no assumption beyond the paper is made. Convergence is convergence of in . The parameter is the paper's standing assumption.
Conventions committed to:
The goal does not assume a decrease of the merit function or finite termination; a formalization that adds either as a hypothesis would be trivial and is ruled out. The run-existence companion shows that the hypothesis "let be a run" can be met, so the goal is not vacuous.
A complete development needs: invertibility of principal blocks of a P-matrix, the block form of one step, the elementary estimate of by for , and an argument that excludes cycling. Proofs of any milestone, of the companion statements, or of the goal through an argument other than the paper's are welcome.
Manufacturers of computer hardware, software and automobiles routinely pay channel rebates to their retailers: a payment for each unit the retailer sells to end customers, either for every unit (a linear rebate) or only for units beyond a target (a target rebate). In the same industries manufacturers also accept returns, crediting the retailer for unsold stock. Both instruments are meant to make the retailer act in the interest of the whole supply chain. When the retailer's sales effort drives demand and cannot be written into a contract, the question is which of these instruments, alone or combined, can make the retailer choose the effort and the stock that maximize total chain profit.
T. A. Taylor, Supply Chain Coordination Under Channel Rebates with Sales Effort Effects, Management Science 48(8) (2002) (DOI 10.1287/mnsc.48.8.992.168), answers this in a newsvendor model with multiplicative effort. Its Theorem 2 shows that a target rebate combined with returns can coordinate. This mission formalizes the complementary negative result, the paper's Proposition 2: no single instrument suffices. It is related to the impossibility shown by Cachon and Lariviere for revenue sharing with retailer effort (Management Science 51(1), 2005), but concerns different instruments.
A retailer orders a quantity and exerts a sales effort before demand is observed. Demand is , where is a random variable with a density on that vanishes on and is strictly positive on (Assumption A4), with finite mean. Write
Effort costs , where and is strictly increasing and strictly convex on (Assumption A5; the paper declares all such properties strict). The retail price , the manufacturer's unit cost , the wholesale price and the salvage value satisfy and (Assumption A1); may be negative.
The integrated channel earns
and denotes a maximizer of over , . Under a contract with wholesale price , rebate per unit sold beyond the target , and return credit per unsold unit, the retailer earns
Returns alone is with ; a target rebate alone is , with no returns, (the retailer salvages leftovers herself); a linear rebate alone is the case of the latter. Channel coordination means that the retailer's optimal decisions under the contract are the integrated channel's .
For every , every and every ,
The three clauses are returns alone, a linear rebate alone, and a target rebate alone. The statement asserts that is not among the retailer's maximizers at all, which is stronger than saying that the retailer's optimum is not exactly .
Proposition 2 is the converse half of the paper's main message. Together with Theorem 2 it says that the combination of a target rebate with returns is the minimal coordinating scheme among those considered: each ingredient alone fails, under general demand and general effort cost, not only in a parametric example. The proposition also frames the paper's remark that a linear rebate combined with returns coordinates only at and , which leaves the manufacturer no profit.
The result is proved in the paper; nothing in this mission is open mathematics. No part of it has been machine-checked before. The formal development adds a precise account of what the paper's argument needs: the existence and interiority of the integrated optimum, the differentiability of the effort cost, and a full characterization of the retailer's optimal order for a general positive density, which the paper states but proves only for the quantity-only case.
The obvious route compares first-order conditions, but neither problem is globally smooth. The retailer's profit in has an upward kink at , so it is concave only piecewise and its maximizer is decided by a comparison of two local maxima, not by a first-order condition. Consequently the retailer's value as a function of effort, , switches branch at and is neither concave nor differentiable there. Showing that is not a retailer optimum therefore requires the global order characterization (Lemma 2) in place of a local condition, a separate argument for the knife-edge effort , and differentiability of expectations such as in the effort level under only a finite-mean assumption. The paper's own proof cites Lemma 1 where Lemma 2 with is needed.
The density form of A4 is literal: a measurable , zero on negatives, positive on , integrating to one, with integrable. The law of is Lebesgue measure with density ; the law of is its image under . The expectations and are the published CachonCoord.Newsvendor.expSales and expLeftover of that image law; the rebate term is the integral of . Critical fractiles and the threshold are stated by their defining equations, never as inverse functions. "Optimal" means a maximizer over (and ).
Two hypotheses are pinned relative to the page and disclosed in each statement. The effort cost carries a derivative with differentiable at every : the paper writes in every first-order condition without stating it, and without it a kink of at could let both the channel and the retailer stop at . The integrated optimum is a hypothesis, as the paper assumes its existence in words, and it is required to have , as the paper's optimum is interior. Without the channel would sell nothing, and a degenerate statement would follow.
A trivializing reading is ruled out: the goal does not say that the retailer's first-order conditions fail at , nor that her optimum is not unique; it says that is not a retailer maximizer.
Needed infrastructure: differentiation under the integral of and in , strict monotonicity of and on , and the piecewise-concavity analysis of the newsvendor with a target rebate. These pieces are reusable for the sibling missions of this paper and for other effort-dependent newsvendor models. Proofs of the milestones and of supporting lemmas on these expectations are welcome.
The eigenvalues of a large random matrix with independent entries follow deterministic limiting laws. For non-Hermitian matrices with i.i.d. entries of mean zero and variance one, the circular law asserts that the eigenvalues of become uniformly distributed on the unit disk. These laws are used across statistics (covariance and signal-plus-noise models), numerical analysis (spectra of perturbed matrices), mathematical physics and the theory of neural networks; what makes them usable is universality: the limit depends only on the mean and variance of the entries, not on their distribution.
Timeline of the circular law and its universality:
This mission formalizes the main universality theorem of that paper (Theorem 1.5) together with the lemmas its proof rests on.
Let be an complex matrix with eigenvalues , counted with algebraic multiplicity. Its empirical spectral distribution (ESD) is the probability measure
on . The Hilbert–Schmidt norm is .
A complex random variable has zero mean and unit variance if and . Given such and , let and have entries that are i.i.d. copies of , resp. . Let be deterministic matrices with
and set , .
Measures on carry the vague topology: test functions are continuous compactly supported . The random measures converge to zero in probability if, for every test function and ,
and almost surely if, with probability one, the difference of integrals tends to zero for every test function. The additional hypothesis
concerns only the deterministic shift.
The statement involves no limiting law: it compares two ensembles, so it holds whether or not itself converges.
The proof combines three results, each a milestone:
Supporting milestones: the linear-algebra Lemmas A.1 (interlacing), A.2 (Weyl's second-moment inequality) and A.4 (negative second moment); the probabilistic dominated convergence Lemma 3.1; Girko's identity (Lemma 3.3); the least singular value bound (Lemma 4.1); the lower tail bound for distances to subspaces (Proposition 5.1); and the high- and low-dimensional row contributions (Lemmas 4.2 and 4.3).
The result. Theorem 1.5 with and complex Gaussian transfers Mehta's computation for the Ginibre ensemble to every zero-mean unit-variance entry distribution: this is the circular law under the optimal moment assumption (Theorem 1.10 of the paper). With nonzero it gives universality for perturbed and non-centred matrices, including results with entries of nonzero mean. The replacement principle (Theorem 2.1) is a general tool: it reduces vague convergence of non-Hermitian ESDs to convergence of log-determinants and applies to ensembles without independent entries.
Formalizing it. The theorem is proved in the paper; no part of it, and no ESD of a non-Hermitian matrix, has been formalized. The mission produces a machine-checked statement of universality in the vague topology and a library of reusable pieces: ESDs of complex matrices, convergence of random measures in probability and almost surely, interlacing and Weyl-type inequalities for singular values, and Girko's identity. Lemmas 4.1 and 5.1 rest on results the paper cites (Tao–Vu's least singular value bound, Talagrand's concentration inequality); formalizing those is part of the work.
The ESD of a non-Hermitian matrix is not stable under small perturbations: eigenvalues of a nearly singular matrix can move a long way, so the moment method and the Stieltjes transform method that settle the Hermitian case do not apply. The log-determinant is a stable proxy only if the small singular values of are controlled, and with only a second moment on the entries the entries can be unbounded, which defeats standard concentration arguments. The obvious approach, comparing and by swapping entries one at a time, needs smooth bounded statistics of the matrix, and the log-determinant is neither: it is unbounded near singular matrices.
Matrices are Matrix (Fin n) (Fin n) ℂ; eigenvalues are the roots of the characteristic polynomial as a multiset, so the ESD counts algebraic multiplicity; for the ESD is the zero measure, harmless because every statement is asymptotic. The Hilbert–Schmidt norm is written as an explicit sum, not Mathlib's default (sup) matrix norm. Singular values are Mathlib's zero-indexed LinearMap.singularValues, shifted so that is the largest.
Conventions committed to:
A trivializing formalization is excluded: the goal mentions only ESDs, i.i.d. entries, (1.3) and (1.4) — no log-determinant or singular value hypothesis — and its in-probability half holds without (1.4). Lemmas 6.3 and 6.4 and the internal Lemmas 3.2, 3.4, 5.3, 6.1, 6.6, 6.7 and Theorems 5.2, B.1 are not posed. Contributions are welcome on any milestone, and particularly on the deterministic Lemmas A.1, A.2, A.4 and 3.3, which are reusable well beyond this mission.
The Lasso fits a linear model to data by penalizing the norm of the coefficient vector. Xu, Caramanis and Mannor (arXiv:0811.1790) showed that -regularized regression is exactly a robust regression problem: it minimizes the worst-case residual when every feature column may be disturbed within a norm ball. That reading explains Lasso through what it protects against, not through a prior or a sparsity heuristic.
The paper's Section V turns the same identity into a statistical statement. For a fixed coefficient vector , the robust loss on the training data equals a worst-case expected loss: the largest expected squared prediction error over a class of probability distributions built around the samples. One of these distributions is a kernel density estimator of the data, and from this the authors derive the consistency of Lasso using robustness alone. This mission formalizes that bridge, Corollary 3 of the paper, together with the steps of its proof in Appendix D.
The same authors later generalized the underlying equivalence (Proposition 1 here) to weighted, possibly overlapping uncertainty sets in A distributional interpretation of robust optimization (Math. Oper. Res. 2012).
There are samples and features. The data are a response vector and an observation matrix ; its -th row is the feature vector of sample . A coefficient vector is , and is a fixed budget (the paper writes because its later consistency argument lets it depend on ). Norms are and .
A pair , with and with columns , is admissible if and for every column . Each admissible pair defines one box per sample,
a rectangle around the observed pair in the joint response–feature space. The box-constrained class is the set of Borel probability measures on such that
The empirical distribution of the samples belongs to it, and so does any distribution that spreads the mass of each sample over its box. Finally is the union of these classes over all admissible .
The equation holds for every data set: there is no assumption on how was generated (Remark 1 of the paper).
The remaining step of the proof applies Proposition 1 of the paper: for Borel sets , . Its general weighted form is already posed on the platform as DistInterpRO.Equivalence.theorem_2_1 (inf form, weights summing to one; take and ), and the one-set case (Lemma 2) as DistInterpRO.Equivalence.corollary_2_1. They are credited here and not posed again.
The result. Corollary 3 gives Lasso a distributional reading: minimizing is, up to the additive constant , minimizing the worst-case root mean squared error over all distributions that stay, sample by sample, inside boxes of controlled size around the data. Because a box kernel density estimator lies in , the paper's Theorem 7 derives the consistency of Lasso from this identity when suitably. Without the corollary that argument has no starting point.
Formalizing it. The result is proved in the paper but has no machine-checked proof. A formal development yields three reusable pieces: the robust-regression identity with a perturbed response, the decomposition of a worst case over a product of boxes into per-sample worst cases, and the finite-dimensional instance of Proposition 1 with uniform weights. Together they are the deterministic half of a formal consistency proof for Lasso.
The left-hand side of (8) is a worst case over perturbations of the data; the right-hand side is a worst case over probability measures. Bounding the right-hand side above requires controlling for every in the class, and the constraint on is not that each box receives mass : the boxes may overlap, and a measure may concentrate mass on intersections. The natural argument of moving each sample's mass to the worst point of its box therefore does not apply to a general member of the class. A second, smaller difficulty is the order of the suprema: is a union over , and the square root must be exchanged with a supremum over measures.
Fin (m+1) → ℝ with its product (= Borel) σ-algebra, response first: , . This matches the boxes; the paper's ordering is notation only. is a Matrix (Fin n) (Fin m) ℝ, indices are Fin n, Fin m.IsLUB), with no claim that it is attained. The integral is the Lebesgue integral of the nonnegative integrand with values in , never a Bochner integral. The "max" of the first display is an attained maximum (IsGreatest). The equalities of suprema in the second and third displays are stated as "the same real number is the least upper bound of each set". The inner supremum over a nonempty compact box is encoded as the greatest value of the loss on it.sSup with a junk value and no Bochner integral that could silently vanish appear in any statement. The class keeps the constraint for every , including , which forces each measure onto ; dropping it would make the supremum infinite.DistInterpRO.Equivalence.theorem_2_1 is reusable well beyond this mission. Proofs of either milestone, of the uniform-weight Proposition 1 for boxes, and of the goal are all welcome.Robust regression guards a linear model against errors in the data matrix. The observations are fitted by , but the features (the columns of ) are only known up to a disturbance from an uncertainty set . The robust estimator minimizes the worst-case residual,
Xu, Caramanis and Mannor (arXiv:0811.1790v1; IEEE Trans. Inf. Theory 56(7), 2010) showed that when each column is perturbed independently within a Euclidean ball of radius , this problem is exactly the weighted -regularized problem , an un-squared Lasso (their Theorem 1, the subject of the first mission of this series). Robustness then explains regularization: the penalty is the price of the worst disturbance.
Section III of the paper asks which regularizers arise when the disturbances of different features are coupled, that is, when a single budget limits all columns jointly. The answer it gives is that every norm-based regularizer arises this way: a norm budget on the vector of column-disturbance sizes produces the dual norm as the penalty. This links robust optimization (Ben-Tal, El Ghaoui, Nemirovski 2009) and regularized estimation, and it recovers the robust least-squares formulation of El Ghaoui and Lebret (1997) as the Euclidean special case.
Fix , , and an arbitrary norm on . The data are the columns of and the response ; for , . A disturbance is with ; the perturbed matrix has columns . For an uncertainty set the robust objective is
Three families of uncertainty sets appear.
A fourth, polytope set, for , , is the subject of Corollary 2. Write .
For an absolute norm and , for every the worst case over the norm-budget set is attained and
and the robust problem and have the same minimizers.
For and every : , attained, with the same minimizers.
For every , in the extended reals,
If some has , then for every the worst case over the polytope set equals (both sides when the constraints are infeasible), the infimum is attained when feasible, and robust minimizers are exactly the -parts of optimal solutions of that linear program.
The paper's general result, Theorem 4 (p. 6), expresses the coupled robust problem through a Lagrangian function under the assumption that has nonempty relative interior. The mission does not pose it: that assumption is not Slater's condition, and the statement fails without one (an explicit counterexample with is recorded in the series plan). The mission poses the decomposition (13), on which Theorem 4 rests, and the two corollaries, which are true as stated under the readings below.
The result. Corollary 1 says that any norm penalty is the worst-case cost of column disturbances whose sizes are jointly bounded in the dual norm. Taking gives the penalty (budget per column), gives (a shared budget), and both Euclidean gives the Frobenius-ball model of robust least squares. Corollary 2 shows that polytope budgets keep the problem a linear program apart from the loss, which allows modeling, for instance, corruption of an unknown subset of features. Eq. (13) is the common reduction behind these: the coupled worst case is the uncoupled one maximized over the admissible budget vectors.
Formalizing it. None of these statements has a machine-checked proof. The mission makes precise two points the paper leaves implicit: which "symmetric" norms the corollary is true for, and in what sense "max" holds when the budget set is empty or unbounded. The finished development is a self-contained library of worst-case residual identities for arbitrary norms on finite-dimensional or general normed spaces. Related platform items, credited and not reused: SPOBounds.StronglyConvex.dual_norm_ball_max (maximum of a linear functional over a norm ball, with the continuous-dual norm), and RobustLS.Unstructured.worst_case_residual_closed_form (El Ghaoui–Lebret, which perturbs in a Frobenius ball, a different set).
The upper bound of every identity is a triangle inequality. The content is in the matching lower bound: a disturbance must be exhibited that aligns all perturbed columns with the residual direction, and in (13) each column disturbance must have norm exactly , including columns with , which is where enters. The paper's first line of the proof of (13) rewrites as ; that set identity is false unless is downward closed, so the obvious route through it does not work for (13) as stated. For Corollary 1 the remaining step is the identity , which needs the absolute property and fails for norms that are only permutation invariant. For Corollary 2 the remaining step is linear programming duality, which Mathlib does not yet provide in this form.
is an arbitrary real normed space with Nontrivial E (the paper's implicit ); finite dimension is not imposed, a harmless generalization. Columns are a family a : Fin m → E, disturbances δ : Fin m → E, coefficients Fin m → ℝ, and . Explicit readings:
EReal; it is never defined by its closed form. "Max" is stated as IsGreatest of the set of residual values (attained) in Theorem 3 and Corollary 1, where the maximum exists, and as an EReal supremum in (13) and Corollary 2, where it need not.Seminorm on Fin m → ℝ with (the type already carries the sup norm, so the notation is not used for it). The dual norm is a real sSup of , a nonempty set that is bounded above because is a norm on .A trivializing formalization is ruled out: the robust objective is the EReal supremum (or the residual-value set) over the uncertainty set, so no identity holds by unfolding, and no real sSup junk value enters a robust objective. Welcome contributions: the explicit worst-case disturbance in an arbitrary normed space, the absolute-norm duality lemma, and a finite-dimensional LP strong duality theorem, each reusable beyond this mission.
Two-stage stochastic linear programs model decisions taken before uncertainty is revealed (a first-stage plan ) followed by a corrective recourse action once it is. The classical model needs the full probability distribution of the uncertain data. In practice usually only estimates of a few moments are available, and the computed plan can be sensitive to the distribution that is assumed. The minimax (distributionally robust) approach replaces the single distribution by a class of distributions sharing given moments and optimizes against the worst member of the class. Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) combine this with risk aversion, through a piecewise-linear disutility of the second-stage cost, and show which instances become semidefinite programs.
Besides the optimal value, the worst-case distribution itself is of practical interest: the paper proposes it as a natural distribution for stress-testing a first-stage solution (§4). This mission concerns the case where the right-hand side of the second stage is random, and formalizes the paper's construction of a worst-case distribution that is a genuine member of the moment class.
A first-stage decision is feasible if . Given a recourse matrix , a technology matrix , a constant cost vector and a realized right-hand side , the second-stage cost is the optimal value of the dual of the recourse linear program,
Risk aversion enters through the disutility with . The right-hand side is random; its distribution is only known to lie in the moment class
and the worst-case expected disutility is .
The standing assumptions are: complete recourse, ; a nonempty dual polyhedron ; ; and (Assumption 5) the extreme points of the dual polyhedron are known. Under these, the paper introduces the semidefinite program (16): over symmetric blocks indexed by pairs ,
From a point of (16) the paper builds the mixed distribution , which with probability draws a normal vector with mean and covariance .
For every there is with
where the common value is the attained maximum of (16), and the expected disutility is integrable under every member of .
The result. Theorem 3.3 shows that, once the dual extreme points are known, the worst case over the moment class is attained, and by an explicit finite mixture of normal distributions read off an optimal solution of a semidefinite program. This contrasts with the random-objective case of the same paper (Theorem 2.2), where the bound is in general only approached by a sequence of distributions. The extremal distribution gives a concrete stress-test scenario for a candidate first-stage plan, and the identity certifies the value of the inner worst-case problem without appeal to strong duality for the moment problem.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. A formal proof needs a measure-theoretic treatment of conditional moments on the cells of a piecewise-linear maximum, the existence of optima of a bounded semidefinite program, and moment computations for multivariate normal mixtures. These pieces are reusable well beyond this paper, for instance in other moment-based distributionally robust models.
The obvious route goes through moment-problem duality: dualize , reformulate the semi-infinite constraint as linear matrix inequalities, and dualize again. That route only gives the inequality chain up to a duality gap and says nothing about attainment over . The proof here avoids strong duality, but it must show two separate things: every distribution in maps to a feasible point of (16) without loss of value (this needs a measurable choice of the maximizing pair and the conditional moments on each cell), and the optimal point of (16) maps back to a distribution in whose value is at least the optimum. The second step fails on blocks with zero weight , where no normal component can be formed; those blocks have to be removed from an optimal solution first.
The Lean development works on as Fin r → ℝ, with measures in place of the paper's densities. The moment class reuses the published definitions MomentDRO.Conf.HasSecondMoments, meanVec and secondMomentAbout P 0 (uncentred second moment). , and are real sSups; every theorem that uses them states the relevant maximum or bound explicitly, so no statement depends on the junk value of an empty or unbounded supremum. Bordered matrices are Matrix.fromBlocks over Fin r ⊕ Fin 1 and is Matrix.PosSemidef. The normal components are Mathlib's multivariateGaussian, transported from EuclideanSpace ℝ (Fin r); the mixture weights are ENNReal.ofReal .
Readings of the page:
The goal asserts that a maximizer over exists, not only an equation between suprema: an equation such as alone could hold through a junk value and is ruled out as the target. No strong-duality hypothesis is assumed, since the proof does not need one. Contributions welcome: the measurable argmax selection, compactness of the feasible set of (16), and second-moment computations for Gaussian mixtures.
Facility networks fail: plants close after floods, distribution centres lose power, suppliers go bankrupt. The reliable uncapacitated facility location problem (RUFL) of Cui, Ouyang and Shen (UCTC-FR-2010-02, February 2010; published as Operations Research 58(4), 2010, doi:10.1287/opre.1090.0801) chooses which facilities to open and, for every customer, an ordered list of backup facilities, so as to minimize fixed cost plus expected transportation and penalty cost when facilities fail independently with site-dependent probabilities. It extends the uniform-probability model of Snyder and Daskin (Transportation Science, 2005).
RUFL is solved by Lagrangian relaxation in the sense of Fisher (Management Science, 1981): dualizing the constraints that link assignments to open facilities splits the problem into one relaxed subproblem (RSP) per customer. Every evaluation of the Lagrangian dual solves all subproblems, and (RSP) is itself a hard combinatorial problem, because the probability that a backup facility is used depends on which facilities sit above it. The paper therefore replaces (RSP) by a fixed-probability reformulation (RRSP), an assignment problem, and Proposition 4 asserts that its optimal value is a valid lower bound. A Lagrangian bound computed from (RRSP) is a valid bound on RUFL only if this holds.
Fix one customer and drop the index from the variables. The data are: the demand rate ; regular facilities with unit costs and failure probabilities ; an emergency facility with (the penalty per unit of unserved demand) and ; multipliers ; and levels with .
A level assignment is a binary array (: facility serves at level ) such that the customer has distinct regular facilities at levels , the emergency facility at a level , and nothing after it. In the paper's constraints:
The level- facility serves exactly when all facilities at the levels above it have failed. The transitional probabilities are and , with imposed through linear constraints. The relaxed subproblem is
Order the regular facilities by reliability, , and set and . The reformulation freezes the probabilities at these values:
over the same level assignments.
The proof works through a split formulation: chooses whose distance is paid at each level, a second level assignment chooses whose failure probability is used, and the cost is . Imposing gives back (RSP).
With , , , and any reliability ordering: for every (RSP)-feasible there is an (RRSP)-feasible with
The result. Proposition 4 makes (RRSP) usable as a lower-bounding oracle. (RRSP) is an assignment problem with rows and levels, so it can be solved in strongly polynomial time by the Hungarian method (Kuhn, 1955). The exact subproblem algorithm of §3.3.1 needs branch and bound over subsets. With the bound, every subgradient iteration of the paper's Lagrangian scheme still yields a valid lower bound on RUFL, which is what the gap-closing branch and bound relies on.
Formalizing it. The proposition has a printed proof, but the proof is incomplete (see below), and to our knowledge no machine-checked version exists. A formal proof certifies the bound, settles which hypotheses it needs, and gives a reusable model of multi-level backup assignment with transitional probabilities.
The obvious argument says that is the largest probability any facility can have of serving at level , so freezing the probabilities at can only lower the cost. That is false as stated: transport costs and the penalty may be negative, and a larger serving probability then means a higher cost. What is needed is a comparison of the whole cost profile, not level by level.
The paper's route is the split formulation. Lemma 1 shows that the probability facilities of some optimal split solution can be taken in increasing order of . The proof then ends with "without loss of generality, we can fix and … which leads to the (RRSP) formulation". This step has a gap. Lemma 1 only says that is ordered. Turning its probabilities into , also needs to use the facilities with the globally smallest failure probabilities, and the paper never shows this. A complete proof has to replace 's facilities by the most reliable ones and show that the cost does not increase. That replacement raises every cumulative service probability , so the comparison is a rearrangement argument over the ordered distances. Lemma 1 alone does not close the proposition.
The sign of the multipliers matters. With of mixed sign the proposition is false, for instance with , , , , , , . There while . Lemma 1, by contrast, holds for multipliers of either sign.
Facilities are Fin (J+1) with Fin.last J the emergency facility, levels are Fin (R+1), and every variable is a real array, with constrained to . The customer index is dropped. The ordering is a bijection of Fin J with monotone, and the goal quantifies over every such . "Lower bound" is stated as for-all/exists, so no infimum of a possibly empty set is taken; both feasible sets are finite and contain the emergency-only assignment.
Conventions fixed in Lean, each recorded in the docstrings:
The statements are not trivial. A sanity-check file exhibits a two-facility instance satisfying every hypothesis, together with feasible points of all three formulations.
A complete development needs finite sums and products over Fin, the explicit form of along a level assignment (a product of failure probabilities), and a rearrangement inequality for ordered sequences. All three are reusable for the other missions of this series and for reliability models in general. Contributions are welcome on the milestones, on a corrected proof of the final step, and on lemmas such as "the transitional probabilities of a level assignment are products of the 's".
Many problems in system identification, collaborative filtering, low-dimensional embedding and model reduction ask for the matrix of least rank in an affine space. Affine rank minimization — given a linear map and , find a matrix of minimum rank with — is NP-hard in general. Recht, Fazel and Parrilo (arXiv:0706.4138; SIAM Review 52(3), 2010, doi:10.1137/070697835) showed that the convex relaxation which minimizes the nuclear norm (the sum of the singular values) instead of the rank recovers the minimum-rank solution exactly whenever satisfies a restricted isometry property on low-rank matrices. That deterministic theorem is the subject of the companion mission in this series.
A deterministic condition is only useful if maps satisfying it exist and are common. This mission formalizes the paper's second main result: random linear maps from a broad class — including Gaussian, symmetric Bernoulli and sparse random matrices — satisfy the restricted isometry property with overwhelming probability once the number of measurements is of order . This parallels the role of random matrices in compressed sensing (Candès–Tao 2005; Baraniuk, Davenport, DeVore and Wakin 2008), where the vector restricted isometry property is established for random measurement matrices by a concentration and covering argument.
Write for the trace inner product on and for the Frobenius norm. A linear map is given by measurement matrices through ; is the Euclidean norm in , and is the operator norm.
The -restricted isometry constant (Definition 3.1) is the smallest such that
A random linear map is nearly isometrically distributed (Definition 4.1) if for every , ; for every and ,
and for some and all , .
For subspaces of a Euclidean space, the projection distance is , the operator norm of the difference of the orthogonal projections (4.10). For subspaces , , the subspace consists of the matrices whose column space lies in and whose row space lies in .
Fix . There are depending only on such that for all with , all , and every nearly isometric random map ,
The theorem supplies the hypothesis of the paper's recovery theorem for random measurements: with and rank , it shows that random linear measurements suffice for nuclear norm minimization to recover every matrix of rank at most exactly. Since a rank- matrix has degrees of freedom, this is within a logarithmic factor of the information-theoretic count. The result made the nuclear norm heuristic a guaranteed method and seeded the theory of low-rank matrix recovery, including matrix completion.
The result is proved in the paper, though Lemma 4.5 rests on Szarek's covering estimates for the Grassmannian, cited without proof. To the best of the curators' search of the platform, none of these statements is machine-checked: there is no formal treatment of the matrix restricted isometry property, of nets on Grassmannians in the projection metric, or of nearly isometric random maps. A formalization would supply the probabilistic half of a fully verified low-rank recovery guarantee, together with reusable pieces — the projection distance, the stability of near isometry under subspace perturbation, and a covering bound for Grassmannians.
The set of matrices of rank at most is not a subspace, so concentration for one matrix and a union bound over a single net in do not suffice: a net of the unit ball of all matrices has size exponential in , which would require of order . The set must instead be covered by finitely many -dimensional subspaces, which requires a quantitative covering of the Grassmannians and in the projection distance — the content of Lemma 4.5, whose source in the literature (Szarek) does not give the constant explicitly. A second subtlety is that the event " is a near-isometry on all of a subspace" involves an uncountable family of matrices, and the bound for the supremum of over a unit sphere has to be controlled from the finitely many points of a net.
All statements live in the namespace MinRankRecovery.RandomRIP. Matrices are Matrix (Fin m) (Fin n) ℝ; the Frobenius norm and the trace inner product come from the published module HighDimStat_MatrixRank_Core. A linear map is represented by its measurement matrices Xs : Fin p → Matrix (Fin m) (Fin n) ℝ, which loses no generality. A random map is Xs : Ω → Fin p → Matrix … on a probability space (Ω, μ), with measurable entries.
Conventions committed to:
EuclideanSpace ℝ (Fin m × Fin n), which carries the Frobenius inner product. Lemma 4.4 is stated on EuclideanSpace ℝ ι for any finite index type.Real.log is the natural logarithm.Two printed statements are corrected. Theorem 4.2 assumes : at , and a two-point random scalar map is nearly isometric while violating the conclusion. Lemma 4.5 is posed for , since for large the right side drops below .
The constants of the goal are quantified before the dimensions, the distribution and ; a formalization in which they may depend on or on the distribution, or in which the near-isometry hypothesis is unsatisfiable, would be trivial and is ruled out by these choices.
A complete development needs: orthogonal projections and operator norms on finite-dimensional inner product spaces (Mathlib), volumetric -nets of spheres in subspaces, covering bounds for real Grassmannians in the projection metric, and the measure-theoretic union bound. The Grassmannian covering bound and the stability lemma are reusable beyond this mission. Contributions of any milestone, including Lemma 4.5 on its own, are welcome.
Stochastic programs of the form are rarely solvable exactly, because the expectation is an integral over a large or continuous scenario space. The standard remedy is sample average approximation (SAA), also called the Monte Carlo or sample path method: draw an i.i.d. sample from and minimize the sample average instead. Two-stage linear programs with recourse are the main case in practice. There each is the value of a second-stage linear program, hence piecewise linear and convex, and the scenario distribution is often discrete with an astronomically large but finite support.
Shapiro and Homem-de-Mello (SIAM J. Optim. 11(1), 2000) observed that in this discrete, piecewise linear regime SAA does far better than the usual statistical rate suggests: the SAA problem often returns an exactly optimal solution of the true problem. In their median example, a sample of solves a problem with scenarios exactly with probability about . This mission formalizes the version of that phenomenon that allows the true problem to have many optimal solutions.
Timeline. In 2000, Shapiro and Homem-de-Mello proved almost-sure exactness of SAA under a sharp-minimum condition (Theorem 2.1) and for finite piecewise linear problems with possibly non-unique optima (Theorem 2.3). They then showed that both events fail with exponentially small probability (Theorems 3.1 and 3.2). In 2002, Kleywegt, Shapiro and Homem-de-Mello extended exponential rates to SAA for discrete stochastic optimization. In 2002, Shapiro, Homem-de-Mello and Kim related the exponential constant for convex piecewise linear programs to a conditioning measure of the problem.
Let be the feasible set, a finite set of scenarios with a probability measure , and . The true problem (1.1) and the SAA problem (1.2) are
where is one i.i.d. sequence with law , defined on an auxiliary probability space . Write for the set of optimal solutions of the true problem and for that of the SAA problem. depends on the sample path, and either set may be empty.
The standing assumptions of Theorem 2.3 are:
A subset of a convex set is a face of if is convex and every open segment of that meets lies in . The event of interest is
Under assumptions 1–4 there is with
The constant is not specified; the goal asserts only that the failure probability decays exponentially.
Under the same assumptions, is compact, convex and polyhedral, and with probability one is a nonempty face of for all large enough.
The milestones are the three parts of Lemma 2.4 (p. 6) and the two steps of the proof of Theorem 3.2 (pp. 12–13).
The result explains the observed behaviour of SAA on two-stage linear programs with discrete distributions. For a fixed problem, the sample size needed to recover an optimal face of the true problem with a prescribed probability grows only logarithmically in the inverse failure probability. When the true optimum is not unique, the theorem still gives a structural guarantee: every SAA optimal solution is optimal for the true problem, and every vertex of is a vertex of . Theorem 2.3 is the almost-sure consequence, by Borel–Cantelli.
The results are proved in the paper; none of them has a machine-checked proof that we know of. Formalizing them requires a library of polyhedral convex analysis that Mathlib lacks: the cell decomposition of a piecewise linear function, faces of polyhedra, and finiteness of the set of extreme points. It also requires one-dimensional exponential tail bounds for empirical means of finite-valued variables. The mission makes precise one point the paper leaves implicit. The paper first reduces to the unconstrained case by an exact penalty, and the strict gap recalled on p. 12 holds for the penalized function. For the original the lemma is stated with instead of the printed .
The probabilistic part is routine. Once Lemma 2.4 (c) is available, the event lies in a finite union of events, each a deviation of one real sample mean from its expectation, and each of those decays exponentially. The difficulty is the deterministic Lemma 2.4 (c). Its points must be independent of the sample. The argument that all , and hence every , are affine wherever is affine needs every scenario to have positive mass. Passing from local information near to global optimality of uses convexity on a polyhedral neighbourhood of built from finitely many cells. The natural first idea, uniform convergence of to on a compact set, gives only that approaches , not that , and certainly not that is a face.
EuclideanSpace ℝ (Fin m), and is a Fintype with measurable singletons.ω : ℕ → S → Ω of measurable, independent maps with law ; are its first terms. At the sample average is the junk value .Convex ℝ F ∧ IsExtreme ℝ A F;Set.extremePoints.i.val < ℓ and ℓ ≤ j.val in Fin q.The empty set is a face of every set, and so is itself. therefore carries nonemptiness explicitly, and "face" is not weakened to . Lemma 2.4 (c) also carries the gap : without it, repeating an extreme point among the would make (2.13) unsatisfiable and the lemma empty.
The subdifferential is the published ShorNonsmooth.Subdiff.subdifferential with domain . Contributions are welcome in three areas: polyhedral convex analysis (cells of a piecewise linear convex function, faces and extreme points of polytopes, exact penalties); Hoeffding or Cramér bounds for i.i.d. bounded means; and proofs of the milestones in any order. The polyhedral lemmas are reusable well beyond this mission.
An insurance company whose surplus falls below zero is ruined. The probability of ruin is the classical measure of solvency risk in actuarial mathematics. A company can lower it in two ways: it can invest part of its surplus in a risky asset, and it can pass part of each claim to a reinsurer in exchange for part of the premium. Which mix of investment and reinsurance minimises the probability of ruin is a stochastic control problem. It is studied in risk theory and in applied probability, and it is a model case for control problems with jumps.
Hipp and Plum (2000) solved the problem with investment alone. They wrote down the Hamilton–Jacobi–Bellman (HJB) equation and showed that it has a smooth solution. H. Schmidli (2002) added proportional reinsurance. He proved a verification theorem (his Theorem 1) and an existence theorem (his Theorem 2) for the combined problem. This mission formalizes the existence theorem and the analytic statements it rests on.
Claims arrive as a Poisson process with rate . The claim sizes are independent with distribution function , where and is continuous. The insurer collects premiums at rate . A risky asset follows a geometric Brownian motion with drift and volatility . Under proportional reinsurance with retention level , the insurer pays the fraction of each claim and pays the reinsurer a premium at rate . The function is decreasing and continuous, , , and there is with for and for . In particular, full reinsurance costs more than the premium income.
Write for an unnormalised survival probability, with for . The HJB equation (1) of the problem is
where is the amount invested. Eliminating and substituting turns (1) into the integral equation (5):
Condition (6) at is . In Lean, ReinsPremium, ClaimLaw, tail, den (), SolvesEq5On, H and SolvesHJB (equation (1)) live in the shared module SchmidliRuin.Verif.Setting; HasBoundedDensity, Cond6, SolvesEq3At and SolvesHJBAtZero live in SchmidliRuin.Exist.Setting.
If has a bounded density, then
Lean states this as two conjuncts: existence, and equality on of any two strictly decreasing solutions.
The existence theorem completes the dynamic-programming solution of the problem. By the verification theorem, divided by is the maximal survival probability . The maximisers of the HJB equation define the optimal feedback strategy: the investment and the retention level . Without Theorem 2 the verification theorem would be a statement about a function that might not exist. Equation (5) is also the basis of the paper's numerical scheme (§5), which iterates (5) to compute and the optimal strategies.
Theorem 2 has a published proof. As far as is known, none of the results above has a machine-checked proof, and nothing on Prove2Me states them. The work is to formalize the published argument. This takes the local existence result of Hipp and Plum, which the paper cites rather than reproves, and a continuation argument for a nonlinear Volterra-type equation whose kernel is an infimum over a control parameter. Milestones 6 and 7 are the purely analytic content of the verification theorem that the uniqueness part of Theorem 2 uses. The paper derives milestone 7 stochastically, and an analytic proof is equally welcome.
The denominator vanishes at : , because . The integral in (5) is therefore improper at the origin. A Picard iteration started from a constant does not work, because it does not control . One needs the exact square-root rate , and Lemma 4 obtains it only through Lemma 3 (no reinsurance near ) and the Hipp–Plum analysis of the reinsurance-free equation. Lemma 4's proof in the paper is a two-line citation, so a solver must formalize that local existence result.
The second difficulty is continuation. A solution can be continued as long as condition (6) holds, and Lemma 5 has to exclude that (6) degenerates at a finite endpoint. There the infimum over interacts with the vanishing of . The paper's argument uses a Gronwall estimate and the shape of around , and the minimiser in need not be unique or continuous.
Model data. are real parameters, all strictly positive. The claim law is a probability measure on , with cdf ν, and continuous. "Bounded density" means has a measurable density with values in . is .
Premium. is a real function, used on . The condition is the lower bound near , which is equivalent. A real-valued excludes the case that the paper allows when .
Conventions.
tail, never by Lean's .IsLUB … 0). Lean's sSup would return on an unbounded family, for example when , and that would make " solves (1)" true by accident.Trivialising readings ruled out.
Infrastructure needed.
ContractingWith).The continuation and closure lemmas (milestones 3–5) are reusable for other HJB equations of risk theory with a jump term. Contributions that state and prove intermediate claims of the paper's proofs are welcome as sub-results.
Reinforcement-learning methods for Markov decision processes split into critic-only methods, which learn an approximate value function and act greedily with respect to it, and actor-only methods, which adjust a parameterized policy along a simulated estimate of the gradient of its performance. Critic-only methods with function approximation can fail to converge; actor-only gradient estimates have high variance. Actor–critic methods combine the two: a critic learns, by temporal-difference (TD) learning, just enough about the value function to give the actor a low-variance gradient direction.
Konda and Tsitsiklis (SIAM J. Control Optim. 42 (2003)) gave the first convergence proof for actor–critic algorithms whose critic uses linear function approximation. Their key observation, found independently by Sutton, McAllester, Singh and Mansour (NIPS 1999), is that the critic need not approximate the value function: it suffices to compute its projection onto a low-dimensional subspace spanned by features determined by the policy parameterization. Earlier convergence results (Konda and Borkar, 1999) covered lookup-table representations only. Actor–critic algorithms, in many later variants, are now a standard tool of reinforcement learning, and this paper is the reference for their asymptotic analysis in the average-cost setting.
A finite cost MDP consists of finite sets (states) and (actions), transition probabilities and a one-stage cost . A randomized stationary policy with parameter chooses action in state with probability . Under the policy , the states form a Markov chain with transition matrix , and the pairs a chain with matrix . When these chains are irreducible and aperiodic, denotes the stationary law of , , and the average cost is
The score is , and .
The critic approximates Q-values by with features whose span contains the components of . Along one simulated trajectory , where is drawn from , the algorithm updates an average-cost estimate , the critic parameter and an eligibility trace at step size (equation (3.1)), and the actor parameter by
at a slower step size . The TD(1) critic resets its trace when the state is entered; the TD() critic discounts it by .
Under Assumptions 2.1 (positive, smooth policies; irreducible aperiodic chains; uniform reachability of ), 3.1–3.2 (bounded smooth features spanning the scores, uniformly nondegenerate) and 3.3 (two-time-scale step sizes and the scaling ),
The statement leaves the initial parameters and the initial state–action law arbitrary.
In attack order: the gradient formula for every Poisson solution, with bounded Hessian (Theorem 4.6); boundedness of the regenerative quantities (Lemma 5.1) and of the trace moments (Lemma 5.2); uniform positive definiteness of the critic's mean matrix for TD(1) and TD() (Lemmas 5.3, 5.6); critic tracking, (Theorem 5.7); the bias of the actor direction, (Lemma 6.1); the descent inequality (6.1); and the convergence of the noise terms (Lemma 6.2).
The theorem says that a policy-gradient method whose gradient is estimated by a linearly parameterized TD critic, rather than by Monte Carlo returns, still converges to a stationary point of the average cost (exactly for TD(1), approximately for TD()). It justifies the compatible features principle (the critic's features must span the score functions), the two-time-scale step-size design, and the trade-off in between variance and bias of the actor direction. The intermediate results are of independent use: Theorem 4.6 is the average-cost policy-gradient theorem for arbitrary Poisson solutions, and Theorem 5.7 is a tracking result for linear stochastic approximation driven by a Markov chain whose kernel changes slowly.
The result is proved in the paper, but the proofs of Theorem 4.6, of parts of the verification of the stochastic-approximation hypotheses and of Theorem 6.3 are given as outlines, with details deferred to a separate appendix and to Theorem A.7, recalled from another paper. No machine-checked proof of the theorem, or of the convergence of any actor–critic method, is known. The mission asks for a formal proof of the finite-case theorem and its milestones, which fills in the outlined steps. The finite-case gradient formula of §2 (Theorem 2.2, recalled from Marbach and Tsitsiklis) is posed, unproved, elsewhere on the platform in a reward-MDP form; it is a special case of milestone Theorem 4.6.
The obvious argument treats the actor as a stochastic gradient method with a noisy gradient estimate. It fails at the first step: the critic's estimate is biased at every finite time, and the bias does not vanish unless the critic converges, while the critic's target moves with the actor. The noise is Markovian, generated by a chain whose transition kernel depends on the current parameter, not a martingale difference sequence. Making the two time scales interact correctly requires a Poisson-equation decomposition of the Markov noise that is uniform in , together with moment bounds for the eligibility trace, which for TD(1) is an unbounded sum over a regeneration cycle. Uniformity in is essential, because the actor iterates are not assumed to stay in a bounded set.
State and action sets are finite types; parameters live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), so is the Euclidean norm and Mathlib's gradient is . The transition probability is stored as p x u y. is a stationary probability vector of , unique under Assumption 2.1(c). The law of the simulated path is built on by the Ionescu-Tulcea construction (Kernel.trajMeasure), with the next action drawn under the actor parameter that the recursion computes from the history; nothing about the critic or the actor's behaviour is assumed.
Readings and corrections, each also recorded in the affected items:
The is taken in , so a sequence with cannot satisfy the conclusion through a junk value, and differentiability of is part of the conclusion, so the statement cannot hold because Lean's gradient returns at non-differentiable points. Series (tsum) and matrix inverses in the milestone objects converge, respectively are invertible, under the assumptions. The hypotheses are satisfiable: , , and the features (which satisfy Assumption 4.9 at every state) meet the parts that could be in doubt.
A complete development needs finite Markov-chain theory uniform in a parameter (existence, uniqueness and smooth dependence of stationary laws; geometric ergodicity; Poisson equations; regeneration), differentiation of , almost-sure convergence of linear stochastic approximation with Markov noise, and martingale convergence. The Markov-chain and stochastic-approximation parts are reusable well beyond this mission. Contributions of proofs of any milestone, of auxiliary lemmas on parameterized finite Markov chains, and of the general two-time-scale tracking theorem (the paper's Theorem A.7) are welcome.
Measurements of Ethernet and Web traffic in the 1990s showed burstiness at every time scale, long-range dependence, and file sizes and transmission times with tails like , (Leland, Taqqu, Willinger and Wilson, 1994; Crovella and Bestavros, 1997). The standard explanation models each user as an ON/OFF source that alternates between transmitting at unit rate and staying silent, with heavy-tailed period lengths. Many such sources are superposed and time is rescaled. Taqqu, Willinger and Sherman (1997) showed that the limit is fractional Brownian motion when the number of sources is sent to infinity first. That limit is the basis of Gaussian queueing models of network buffers.
Mikosch, Resnick, Rootzén and Stegeman (2002) asked what happens when the number of sources and the time scale grow together. The answer depends on how fast grows. Under fast growth the limit is fractional Brownian motion; this is Theorem 4 of the paper and a separate mission. Under slow growth the limit is an α-stable Lévy motion: it has independent increments and infinite variance, and its sample paths jump. This mission formalizes the slow growth result, Theorem 2. The two answers lead to different buffer and dimensioning models, so the dichotomy matters for traffic engineering.
Period laws. ON-periods have law and OFF-periods have law ; both are laws of non-negative random variables. Their means are and , and . Their right tails satisfy (2.1)–(2.2):
where and are slowly varying: for every . The ON-periods therefore have the heavier tail.
One source. Let be iid and iid . Let be Bernoulli with . Let and have the integrated-tail laws . All of these variables are independent. Put . The delay is , and the renewal epochs are . The source is ON at time when
This construction makes stationary.
Superposition. iid sources feed a server. is the number of active sources, and is the cumulative input; its mean is .
Growth. is the quantile function (2.9). is integer valued, non-decreasing and tends to infinity. Slow Growth Condition 1 is .
Stable laws. is the law with characteristic function for . The α-stable Lévy motion has independent stationary increments, and .
With , and , under Condition 1
Every constant is stated as printed. The normalisation is the paper's and the limit is the totally skewed () Lévy motion.
Theorem 2 identifies the limit regime where the Gaussian heavy-traffic picture fails for ON/OFF traffic. When few sources are observed over long horizons, the aggregate input has infinite-variance, independent-increment fluctuations of size . Read together with Theorem 4, the result says the growth rate of relative to decides between the two classical models of network input. The proof turns the ON/OFF superposition into row-wise iid random sums and uses a heavy-tailed large-deviation estimate for random walks (Cline and Hsing). That technique carries over to other renewal-reward processes with regularly varying rewards.
The result is proved in the paper. No machine-checked version exists, either of the theorem or of the probabilistic substrate it rests on. Formalization would produce:
Correction. Lemma 12 as printed omits the normalisation on its left-hand side. Its proof and its use in Theorem 2 both have it, and without it the claim fails because the left-hand side grows. The mission states Lemma 12 with the normalisation. Lemma 11's upper summation limits are read as integer parts, as elsewhere in §5.
The natural first idea is to treat as a sum of iid terms and apply the stable central limit theorem for triangular arrays. This fails as stated: each source's contribution is itself a random sum , and its count depends strongly on the . Moreover, grows too slowly for a law-of-large-numbers smoothing across sources. The count must be replaced by its mean simultaneously for all sources, with an error probability , uniformly as . This requires the two-sided large-deviation estimate of Lemma 4. Its lower tail rests on the Cline–Hsing asymptotics for heavy-tailed random walks; its upper tail rests on a Cramér bound. Then Petrov's conditions must be checked at the exact scale . That needs Potter bounds for the slowly varying factors and a non-uniform Berry–Esseen estimate for the truncated sums. None of these tools is in Mathlib.
All declarations are in the namespace NetTraffic.OnOffStable, in one definitions file.
Conventions.
X n and Y n are the paper's and .Set.ncard (junk on a null event). is a tsum of indicators, and is an interval integral.EuclideanSpace ℝ (Fin k) whose characteristic function is that of , and the laws of the normalised input vectors converge weakly to it. The characteristic function pins the limit down. Its existence is part of the claim, because Mathlib has no stable laws.Ruled out. None of the following is acceptable: an encoding in which , or collapses to a junk value; a model hypothesis that no family satisfies (the period laws must be genuine probability laws with finite means, which holds because ); a limit "law" not pinned by its characteristic function; or convergence of one-dimensional laws only.
Needed infrastructure.
The regular-variation and stable-law layers are reusable well beyond this mission. Formalizations of any milestone, of those general tools, or of alternative proofs of the one-dimensional limit are welcome.
A retailer that carries several substitutable products, such as brands of the same item or sizes of the same garment, must choose stock levels before demand is known. When a product runs out, some of its customers buy another product instead. Inventory models with this demand substitution go back to McGillivray and Silver (1978, INFOR 16(1)) and Parlar and Goyal (1984). When the products are run by different firms, each firm's stock affects the demand its competitors see, and stocking becomes a game. Parlar (1988) proved existence and uniqueness of the equilibrium for two products; Lippman and McCardle (1997) treated a symmetric version of the game with an arbitrary number of firms.
Netessine and Rudi (SSRN 303779, working paper 2002; journal version in Operations Research 51(2), 2003) treat products with a general joint demand distribution and general prices and costs, under both centralized and competitive management. This mission formalizes their analysis of the competitive game (§2.2): the first-order characterization of its Nash equilibria (Proposition 3) and the existence, uniqueness and global stability of the equilibrium (Proposition 4).
There are products, indexed , sold in a single period. Product is stocked at units at unit cost , sold at unit price , and leftovers are salvaged at , with . Write (underage cost) and (overage cost).
The first-choice demand is a random vector with a known continuous joint distribution with positive support. A fraction of the customers who want product and find it out of stock buy product instead, with and for every ; a customer whose second choice is also out of stock is lost. The effective demand for product is
which depends on the other products' stocks but not on .
In the competitive model, firm chooses and earns the expected profit
A best response of firm to is a stock maximizing , and a Nash equilibrium is a stock vector from which no firm gains by deviating.
A Nash equilibrium exists, the equilibria are exactly the nonnegative solutions of the first-order conditions
and if either for all or for all , the equilibrium is unique and globally stable: every sequence of simultaneous best responses started at any nonnegative stock vector converges to .
Proposition 4 makes the competitive equilibrium a well-defined object: a single stock vector, characterized by (10), which can be compared with the centralized optimum (the paper's Proposition 6) and which best-response adjustment reaches from any starting point. Without uniqueness, comparative statements about "the" competitive stocking level would be about an arbitrary selection.
The paper's argument has two gaps that this mission makes explicit. The proof asserts that best responses are single-valued because each profit is concave, and differentiates the best response using a density of ; the bound on the Jacobian is then stated in derivative form. The formal statements replace the derivative bounds by difference (Lipschitz) bounds, which need no differentiability, and state the positivity of the density on which single-valuedness rests. The paper also proves existence by citation to Lippman and McCardle; here existence is part of the goal. No machine-checked proof of these results is known.
The obvious route differentiates the best response implicitly, as the paper does. That requires to have a continuous, positive density at the equilibrium quantile, which is not a consequence of a continuous joint law: is a piecewise-linear function of , and its distribution function may have kinks. A second point is that concavity of alone does not make the best response unique: a demand law whose support has a gap gives a flat stretch and an interval of maximizers. Global stability must hold for every sequence of best responses, not for the iterates of one selected best-response function. Finally, the probabilities in (10) use strict inequalities, and their identification with uses that has no atoms, which needs a measure-theoretic argument about under an absolutely continuous law.
Products are indexed by Fin n (0-based). The model data and the standing assumptions , , and are fields of a structure Model n. a i j is the share of 's unmet demand going to , so uses a j i. The demand law is a probability measure on that is absolutely continuous with respect to Lebesgue measure, gives every coordinate a positive value almost surely, and has integrable coordinates; this is the reading of "a known continuous multivariate demand distribution with positive support". Expectations are Bochner integrals and probabilities are μ.real of events, with the strict and weak inequalities as printed.
The stocks range over , with no upper bound. A best response maximizes over ; a Nash equilibrium is defined by the absence of a profitable deviation, not by (10). Defining equilibria by (10) would make Proposition 3 and half of Proposition 4 true by definition, and is ruled out.
One hypothesis is added beyond the page and disclosed in every statement that uses it: has a Lebesgue density that is strictly positive on the open positive orthant. It is used for single-valued best responses, the slope and contraction bounds, and the goal; the derivative, concavity and Proposition 3 do not use it. In the goal, the second branch of the uniqueness condition, for all , coincides with the standing assumption of §2, so uniqueness always applies within the model; the disjunction is kept as printed. The paper's proof attaches the one-norm bound to the first branch, which is a column-sum condition on ; both branches are true, with the one-norm used for row sums and the infinity-norm for column sums.
A complete development needs: differentiation under the integral sign for piecewise-linear integrands, the absence of atoms of under an absolutely continuous law, quantiles of strictly increasing continuous distribution functions, and the Banach fixed-point theorem on the closed nonnegative orthant (Mathlib's ContractingWith). The first two are reusable for every newsvendor model with substitution. Proofs of the milestones in any order are welcome.
Measurements of Ethernet and Internet traffic in the 1990s showed that cumulative traffic is self-similar and long-range dependent: correlations of the input rate decay so slowly that they are not summable, and fluctuations at large time scales do not average out the way Poisson-type models predict. A widely accepted explanation is that the lengths of individual transmissions (file sizes, session durations) are heavy tailed, with infinite variance. Queueing and capacity-planning calculations then depend on which stochastic process approximates the cumulative input over long horizons.
Two candidate approximations had been proposed: fractional Brownian motion, a Gaussian self-similar process with dependent increments (Taqqu, Willinger and Sherman, 1997; Leland, Taqqu, Willinger and Wilson, 1994), and α-stable Lévy motion, a heavy-tailed process with independent increments. Mikosch, Resnick, Rootzén and Stegeman (Ann. Appl. Probab. 12 (2002) 23–68) showed that both arise from the same model, and that the answer depends on how fast the connection rate grows relative to the time scale. This mission formalizes their Gaussian answer for the infinite source Poisson model: Theorem 3.
Connections start at the points of a homogeneous Poisson process on with rate , labelled so that ; equivalently, , and () are iid exponential with parameter . Connection transmits at unit rate for a length ; the are iid with law on and independent of . The tail is regularly varying:
with slowly varying ( for every ). The mean is finite and the variance infinite. The number of active connections and the cumulative input are
The model is indexed by a time scale , with a connection rate that is non-decreasing in . With the quantile function , the fast growth Condition 2 is
equivalently : many transmissions longer than the observation window start in it. With the normalised input is
Standard fractional Brownian motion with Hurst index is a mean-zero Gaussian process on with a.s. continuous paths and .
Under (2.8), non-decreasing and Condition 2,
On the constant. The paper takes from its display (6.6), . With that value the theorem is false. Two terms are lost in the variance bookkeeping of the proof: (6.4) omits the factor in the variances of the second and third regional sums, each of which contributes , and (6.2) discards by an argument valid only under slow growth; under Condition 2 its variance is . The sum equals , which is also what and Karamata's theorem give. Since , only this value makes the limit standard. All other constants are those of the paper.
The milestones follow the proof: Lemma 1 (Condition 2 ⇔ ⇔ ), Lemma 2 (fast part), the covariance identity (2.14), the moment asymptotics (4.9) and (4.14), the central limit theorem (6.3) for the first regional sum, the one-dimensional limit (6.5) with the corrected variance, stationarity of the increments of , and the fourth-moment bounds (6.8) and that give tightness.
The theorem identifies the fast-growth regime of the infinite source Poisson model (the M/G/∞ input model) with fractional Brownian motion, so that Gaussian long-range-dependent models of network traffic are limits of a mechanistic model, not postulates; together with Theorem 1 it shows that the choice between Gaussian and stable approximations is decided by a single growth condition, or . Queueing analyses of fluid queues fed by fractional Brownian motion inherit their justification from limits of this kind.
The result is proved in the paper, apart from the constant discussed above; it is not formalized anywhere. A formalization adds a machine-checked statement with the correct normalisation and a reusable development of regularly varying tails, Poisson marked point processes on , fractional Brownian motion, and Skorokhod's topology on .
The obvious argument is a central limit theorem for , but is not a sum of independent terms of bounded variance: transmissions that straddle the window are long and heavy tailed, and their contribution is of the same order as the bulk. The proof splits the points into four regions according to where a transmission starts and ends, and each region needs its own moment asymptotics through Karamata's theorem; the bookkeeping is exactly where the printed constant goes wrong. The functional statement then needs tightness in : a fourth-moment bound on increments that is uniform in and in the position of the increment, which requires Potter-type bounds on for small . Convergence of finite-dimensional distributions alone does not give the theorem.
atTop on . Each model has its own probability space; the theorems hold for every family of models with the stated rate and length law. Time in runs over .Optimal control problems with pointwise bounds on the control, such as
reduce, after eliminating the state, to a quadratic program in with a pointwise upper bound. The primal-dual active set strategy solves such problems by guessing the set where the bound is active, solving one linear system on that guess, and updating the guess from the new primal and dual values. It is used routinely in PDE-constrained optimization because each iteration costs one linear solve and, in practice, very few iterations are needed.
Hintermüller, Ito and Kunisch (SIAM J. Optim. 13 (2002) 865–888; authors' version hal-01660511) showed that this strategy is a semismooth Newton method for a nonsmooth reformulation of the optimality system, built on the notion of slant differentiability of Chen, Nashed and Qi (SIAM J. Numer. Anal. 38 (2000) 1200–1216). In finite dimension this gives local superlinear convergence (missions I–IV of this series). This mission concerns the paper's function-space result, Theorem 4.1: in , under a norm gap on the operator, the method still converges locally superlinearly. Ulbrich (SIAM J. Optim. 13 (2003) 805–841) developed a related semismooth Newton theory for superposition operators in function spaces, which also requires a norm gap.
Let be a finite measure space (the paper takes a bounded domain with Lebesgue measure) and the real Lebesgue spaces, with inner product on . The paper writes for an operator and calligraphic , for active and inactive sets.
Slant differentiability (Definition 1). For Banach spaces , , a map is slantly differentiable in an open set if there is , a slanting function, with
For , the candidate slanting function of the pointwise max is if , if , if (4.1).
The problem. Given and a self-adjoint with
minimize subject to . The solution and its multiplier are the unique solution of
for any fixed . The norm gap hypothesis is
The algorithm. From , set , , and solve
A sequence obeying this rule for every is a run. Superlinear convergence of means and, for every , eventually .
The page reads: "Assume that (H1), (H2) hold and that ψ and f are in L^q(Ω). Then the primal-dual active set strategy or, equivalently, the semismooth Newton method converge superlinearly if ‖y⁰ − y*‖ is sufficiently small and λ⁰ = β(y⁰ − ψ)." The formalized goal is the statement the proof establishes: with , there is such that every run with
converges superlinearly to in . The initialization differs from the printed one; see Formalization scope.
Two companion items accompany the goal: existence of a run from every , and Proposition 4.1(i), the paper's counterexamples showing that fails to be a slanting function from to .
Theorem 4.1 is the infinite-dimensional justification of a method used throughout control-constrained optimal control: it shows that the method converges locally superlinearly for the continuous problem itself, not only for each discretization. Example 1 of the paper shows that distributed control of the Poisson equation, and boundary control with Sobolev embeddings, satisfy (H2). Proposition 4.1 isolates the structural reason: the pointwise max is a Newton-differentiable map only between spaces with a norm gap.
None of these results is known to be machine-checked. A complete development would provide slant differentiability in Banach spaces, the Chen–Nashed–Qi local convergence theorem, the norm-gap differentiability of between Lebesgue spaces, and invertibility of block operators on of a measurable partition. Each of these is reusable for other semismooth Newton analyses in function space.
The obvious argument fails at the max. In finite dimension, is slantly differentiable with because a small perturbation does not change the sign of any nonzero component. In , a perturbation of small norm can flip the sign of on a set of positive measure, and on that set the error is as large as . Proposition 4.1(i) shows that this error is not in for any . Superlinear convergence in therefore needs the argument of the max to be controlled in a stronger norm than the error is measured in, which is what (H2) and provide. A second difficulty is that the two-variable algorithm is not literally a Newton method for a map of alone; it must be identified with the reduced algorithm, and that identification depends on the initialization.
Lp ℝ p μ on an arbitrary finite measure space; is an extended real with 2 < q. The paper's bounded Lipschitz domain is replaced by a finite measure space: the proofs use only , and Mathlib has no notion of Lipschitz boundary.run_exists shows that the runs the goal quantifies over exist.PDASNewton.FunSpace.Setting): slanting functions, superlinear convergence, , property (A) for , system (4.2), one step and runs of the algorithm. These duplicate the finite-dimensional definitions of the other missions of the series in a separate namespace.Proofs of any milestone are welcome, as are reusable lemmas on Lebesgue spaces (Hölder on sets of small measure, multiplication operators, Lax–Milgram on of a measurable subset).
Policy gradient methods search a parameterized family of stochastic policies , , by following the gradient of the policy's performance. They are the standard tool when the state space is too large for tabular dynamic programming and when a compact policy class (a neural network, a linear softmax) is easier to represent than a value function. Every such method rests on one identity: a formula for the gradient of the value with respect to that involves only quantities of the current policy, so that it can be estimated from the policy's own trajectories.
Chapter 4 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), states this identity in two settings, the -epoch undiscounted setting and the -discounted setting, both in the thesis's normalized convention, in which values lie in . The thesis then uses the formula to analyse how many samples a gradient estimate needs (§4.2.3), and in §5.4.2 rewrites it in terms of advantages to explain why gradient methods can stall far from optimal: the gradient weights advantages by the current policy's state distribution, not by the distribution of an optimal policy.
Timeline:
A finite MDP has a finite state set , a finite nonempty action set , a transition kernel and a deterministic reward .
-epoch case. Epochs are , . A non-stationary policy chooses at epoch in state with probability . Starting from , is the probability of being in at epoch . The normalized -value is
the state-action value is with , and the future state-time distribution on is .
Discounted case. For a stationary policy and , the normalized value, state-action value, advantage and discounted future state distribution are
A parameterized policy is a family (resp. ) of policies indexed by , each entry differentiable in ; is the gradient in .
The statement asserts that is differentiable at the given parameter and that its derivative is the right-hand side. It is the thesis's version of the Sutton–McAllester–Singh–Mansour theorem, and the result the rest of the thesis's discussion of gradient methods builds on.
The result. The gradient formula contains no derivative of the state distribution: the effect of on which states are visited cancels, and the gradient is an expectation over states drawn from the current policy, weighted by a sum over actions. This is what makes Monte Carlo and actor-critic estimators possible, and it is the reason the thesis's sample-size analysis of §4.2.3 has no dependence on the size of the state space. The advantage form makes the limitation equally explicit: a small gradient certifies small advantages only under , while the performance difference lemma (Lemma 5.2.1) shows that closeness to optimal is governed by advantages under . That gap motivates the conservative policy iteration of Chapter 7.
Formalizing it. The theorems are proved in the thesis and in the cited literature; none of them is machine-checked in this normalized convention. The platform has a proved finite-horizon policy gradient theorem for a scalar parameter, a stationary policy and unnormalized values (policy_gradient_discounted_finite, policy_gradient_finite_horizon), and a posed direct-parameterization gradient for Agarwal et al.'s unnormalized discounted value (PolicyGradTheory.ProjGA.direct_gradient). This mission adds the multi-parameter statements, the non-stationary -epoch version with its state-time distribution, and the infinite-horizon discounted version, where differentiability of an infinite series must be established rather than computed from a finite recursion.
In the -epoch case the value is a finite polynomial in the policy entries, and the work is bookkeeping: unrolling the backward recursion for against the forward recursion for so that the terms involving telescope. In the discounted case the obvious route, differentiating the recursion term by term and recursing forever, presupposes that is differentiable, which the thesis's proof takes for granted. The value is an infinite series in , so that differentiability is a genuine part of the claim, and the resulting formula must be matched with and , which are themselves defined as infinite series.
Fintype), nonempty; transition kernel IsTransitionKernel P; rewards in as a standing hypothesis of every statement; ; . The thesis's later chapters allow infinite state spaces; this mission is finite.ApproxOptRL.Shared.Model (value, qValue, advantage, futureStateDist; is futureStateDist at the point mass on ). The -epoch layer is defined in this mission (TEpoch): 0-based epochs, tValue by backward recursion, tQValue, stateDist, stateTimeDist.EuclideanSpace ℝ (Fin k). Every statement assumes that (resp. for ) is a probability distribution for every , and that each entry is differentiable at the parameter ("the derivatives exist", p. 48). Differentiability of the value is not assumed.HasFDerivAt: the value map has the right-hand side as its Fréchet derivative at . A statement with fderiv of the value alone, or with a policy that does not depend on , would reduce to and is ruled out.Most practical reinforcement-learning methods do not compute value functions exactly. They alternate between estimating a value function from data, usually with a parametric approximator, and acting greedily with respect to that estimate. Approximate value iteration and approximate policy iteration are the two classical schemes of this kind, and their error analysis decides how accuracy in the estimation step translates into quality of the policies produced. Chapter 3 of S. M. Kakade's thesis On the Sample Complexity of Reinforcement Learning (University College London, 2003) collects the basic guarantees, developed from Bertsekas (Dynamic Programming: Deterministic and Stochastic Models, 1987) for greedy policies, Singh and Yee (1994), and Bertsekas and Tsitsiklis, Neuro-Dynamic Programming (Athena Scientific, 1996). The bounds are stated in terms of the worst-case (max-norm) error of the evaluation step, and the thesis uses them to argue that max-norm error is the obstacle to state-space-independent sample complexity results for these methods, which motivates the later chapters of the thesis.
A finite discounted Markov decision process consists of a finite set of states , a finite nonempty set of actions , a transition kernel (for every a probability distribution over ), a deterministic reward , and a discount factor . A policy is a probability distribution over actions for every state; a deterministic policy is a map , identified with the policy that plays with probability one.
Values are normalized: the value of at is
and the state-action value is . With rewards in , every value lies in . An optimal policy has for every policy and state ; write and . The max norm is on state vectors and on state-action arrays.
The backup operator is . A deterministic policy is greedy with respect to if for every .
The policies need not converge; the statement bounds where they end up.
The results give the standard performance guarantee for greedy approximate dynamic programming: an evaluation error of in max norm costs at most in max-norm suboptimality, uniformly over the asymptotic set of policies, with a geometric rate of approach. Example 3.1.2 of the thesis shows that the factor of Theorem 3.1.1 is attained, so the greedy step itself cannot be improved; the two factors of the horizon in the limit bound are the reason the thesis turns to other error measures in later chapters.
All the statements are classical and proved in the literature (Bertsekas–Tsitsiklis 1996, Chapter 6, in the unnormalized model and with a factor to spare in the limit bounds); Lemma 3.2.3 and Theorem 3.2.2 are stated in the thesis without proof. To our knowledge none has a machine-checked proof. The mission produces formal proofs in the normalized model shared with the formalization of Kakade–Langford (2002) on this platform, so later chapters of the series (conservative policy iteration, policy search) can compare against them.
Approximate policy iteration is not monotone: with evaluation errors, can be worse than at some states, so the argument of exact policy iteration, which uses everywhere, does not apply. The difficulty of Lemma 3.2.3 is to control the distance to optimality without improvement at each step, combining the greedy step with the lack of monotonicity of the new policy's value; the thesis calls the proof of Theorem 3.2.2 "somewhat technical" and omits it. A second, mechanical difficulty is that the normalized value is defined as an infinite series, so its Bellman equation , the optimality equation and the bound have to be derived from that definition before any of the recursions can be run.
ApproxOptRL.Shared.Model: value P r γ π is (defined as times a tsum), qValue is . and are finite types, nonempty; satisfies IsTransitionKernel; every statement assumes and .IsOptimalPolicy P r γ πstar (a stationary stochastic policy dominating every stationary stochastic policy at every state). Such a policy exists for every finite MDP (p. 26 of the thesis), and for finite MDPs it is optimal among all policies.S → A, and are evaluated through the indicator policy detPolicy. "Greedy" is the relation ∀ s a, Q s a ≤ Q s (f s): every tie-breaking rule is covered.ℕ, with the greedy and accuracy conditions as hypotheses at every index; the value-iteration condition is written for indices and .S → ℝ and S → A → ℝ.value for indicator policies, , monotonicity and contraction of policy-evaluation and backup operators in the normalized model, and the bound . Contributions of these lemmas are welcome.Asset prices observed at high frequency show two kinds of discontinuity: jumps in the price itself and abrupt changes in its volatility. Whether the two occur at the same times matters for modelling. Many stochastic volatility models used in option pricing let the price and the volatility jump together (for example the affine jump-diffusion models of Duffie, Pan and Singleton, Econometrica 2000), while others make them jump independently or not at all, and the choice affects pricing, hedging and risk management. Jean Jacod and Viktor Todorov (Do price and volatility jump together?, Ann. Appl. Probab. 20 (2010)) built statistical tests of this question that use only discretely observed prices. The tests rest on a law of large numbers, Theorem 3.1 of the paper, and this mission formalizes it.
The price is an Itô semimartingale on a filtered probability space :
where is a Brownian motion, is a Poisson random measure on with compensator , and is the jump size produced by an atom of . The volatility is , and is the jump of at time .
Two assumptions are imposed. (H-), : the drift is locally bounded, is càdlàg with and , and with locally bounded and ; smaller means fewer small jumps, and means finitely many jumps on bounded intervals. (K-), : for a function , where is itself an Itô semimartingale with controlled jumps and is Hölder of order in the sense for .
For a test function , the unobservable target is the jump functional
which compares, at each price jump, the volatility just before and just after it. The data are the values on a grid of mesh , with increments . With a truncation level and a window size , the local volatility estimator is
and the observable statistic is
The tuning (3.3) is and with and . Finally, is the family of open sets with finite complement that contain every value with .
Let be Borel, continuous at each point of for some , and assume one of (a) for ; (b) ; (c) for . Then is a.s. well defined and
They follow the proof of §8, in which the coefficients are bounded by a constant (the localized bound (8.3)):
Theorem 3.1 makes a consistent estimator of . Choosing nonnegative with makes exactly when and jump together on , and the tests of §4 of the paper (Theorems 4.1–4.5), together with the central limit theorems 3.2 and 3.3, are built on this. The same truncated local volatility estimators appear throughout high-frequency econometrics, so their consistency (Lemma 8.1) is reusable on its own.
The result is proved in the paper. No machine-checked proof of it, or of any of its steps, is known to exist. A formal development would also produce a reusable layer for Itô semimartingales with Poisson jumps: the representation (2.1), compensated jump integrals, and convergence in probability in the Skorokhod space. None of these is currently available in Mathlib.
The obvious argument treats each increment and replaces the estimators by . This fails in two places. First, has about summands, so errors of each summand that vanish in probability need not sum to something small. The infinitely many small jumps must be controlled in mean, through the moment bounds of §8.2 and the growth condition of case (c), and the cutoff must separate jumps from Brownian increments. Second, the estimators look at windows of increments that may contain a jump of or of . Consistency holds only away from the big jumps, and the jump times are random, so conditioning has to be done with respect to the enlarged filtrations that know the big jumps in advance. Finally, the limit is in the Skorokhod topology: the jumps of occur at grid times close to, but not equal to, those of , so uniform convergence fails.
Time is and processes are functions ℝ≥0 → Ω → ℝ. The Poisson random measure is given by its atoms , with at most one atom at each time. The Brownian integrals use the published EthierKurtz.HasBrownianItoIntegral. The compensated jump integral is characterized by the Lévy–Itô limit of compensated truncated sums. Càdlàg paths and Skorokhod convergence are the published KurtzProtter91.Integrals definitions. Convergence in probability for the Skorokhod topology is the subsequence criterion: every subsequence has a further subsequence converging almost surely. The identity (2.1) and the path properties hold almost surely, for each .
The conventions are the following.
The conclusion of Theorem 3.1 includes the a.s. summability of . A formalization in which the infinite sum takes a default value, the expectations are junk values of non-integrable variables, or the hypotheses cannot be met is ruled out: with and no jumps satisfies every hypothesis with and .
A complete development needs stochastic integration against Brownian motion and compensated Poisson measures, Burkholder-type moment bounds, and the Skorokhod topology on . These are reusable well beyond this mission. Contributions to any of them, and proofs of individual milestones, are welcome.
Belief propagation (BP) is the message-passing algorithm used throughout artificial intelligence, coding theory and statistical physics to approximate marginals of graphical models. On graphs with cycles it is a heuristic: it may fail to converge, and when it converges its output need not be the true marginal. Rigorous guarantees had mostly been confined to the high-temperature regime, as a consequence of a uniform decay of correlations (spatial mixing) under which any boundary condition is forgotten; see the works cited as [3, 23, 26] in §1 of the paper.
Dembo and Montanari (arXiv:0804.4726v3, Ann. Appl. Probab. 20 (2010)) proved that for the ferromagnetic Ising model with a positive external field, BP converges exponentially fast on every graph of bounded degree, at every temperature, and that on locally tree-like graphs its fixed point computes local marginals accurately. The low-temperature regime, where the Gibbs measure on the limiting infinite tree is not unique, is the point: the field breaks the symmetry, and monotonicity replaces spatial mixing.
Let be a finite graph in which every vertex has at most neighbours, an inverse temperature and a magnetic field. The Ising model on is the distribution on spin configurations
More generally one allows a field at each vertex, and (a vertex pinned to ).
A message is a distribution on attached to the directed edge . The BP iteration is
with the neighbours of and a normalization. An initial condition is positive if on every directed edge. Distances between distributions are in total variation, .
For , is the ball of radius , its vertices at distance exactly , and a neighbour in of each . Given a BP fixed point , the BP estimate of the marginal on is
The proofs run through Ising models on rooted trees : is the tree of the first generations, the -th generation, and , the Ising models on with free and plus boundary conditions (the latter pins to ). A random tree is conditionally independent with average offspring bounded by if, given the first generations, the offspring numbers of generation are independent with conditional means at most (Definition 2.5).
For , and , there are and depending only on such that every finite graph of maximal degree has a BP fixed point with
for every positive initial condition and every . The constants are uniform over graphs; this uniformity is the content of the theorem.
With and : if is a tree, then .
The tree estimates of §3–§4, in the order the proofs use them: Griffiths' inequality (Theorem 3.1); the GHS inequality (Theorem 3.2); the reweighting bound in total variation (Lemma 3.3); marginals on subtrees (Lemma 4.1); the bound on root magnetizations (Lemma 4.3); its extension to marginals near the root (Theorem 4.2); a Simon-type factorization of tree correlations (Lemma 4.4); and Corollary 4.5: exponential decay of correlations (4.13), Theorem 4.2 with rate , and the root-magnetization bound .
The theorem gives an unconditional convergence guarantee for BP on a nontrivial class of models with cycles, valid deep in the low-temperature phase, with a rate independent of the number of vertices. Theorem 2.7 adds that the fixed point is accurate on locally tree-like graphs such as random regular graphs and sparse Erdős–Rényi graphs, so BP is a polynomial-time algorithm for local marginals there. The tree estimates of §4, in particular the insensitivity of the root to plus versus free boundary conditions on conditionally independent trees, are also the engine of the free-entropy theorem of the same paper (mission 1 of this series).
The results are proved in the paper; none of them, nor Griffiths' or the GHS inequality, has a machine-checked proof known to this mission. Formalizing them produces a reusable library for ferromagnetic Ising models on finite graphs and trees (correlation inequalities, pinned boundary conditions, marginals on subtrees) and a formal account of BP as an operator on message families.
The obvious argument is a contraction: show that one BP step shrinks the distance between message families, uniformly over the graph. At low temperature this fails: the BP map is not a contraction, the infinite-tree Ising model has several Gibbs measures, and without a field BP has several fixed points. Uniform decay of correlations, the tool behind high-temperature results, is false in this regime. What has to be controlled instead is a single, weaker quantity: how much the root of a tree of depth feels a plus boundary condition compared with a free one, with a bound that is uniform over all trees of bounded average offspring and over all depths. The difficulty is concentrated in that estimate (Lemma 4.3), and in upgrading its rate to an exponential one (Corollary 4.5), which is where the positive field enters quantitatively.
Spins are Booleans (true ); the edge sum counts each unordered edge once; a field is a pinned vertex, never a large real number. Graphs are finite (Fintype V) with all degrees at most . Messages are functions on ordered vertex pairs whose values on directed edges are distributions on ; the BP iterates are computed from the update, not posited. Total variation is . Trees are encoded by offspring functions on finite words (Ulam–Harris), random trees by probability measures on offspring functions with the product -algebra; conditional independence uses Mathlib's iCondIndepFun, with integrable offspring numbers. Fields on trees are nonrandom functions of the vertex. Expectations that may be infinite, such as , are lower Lebesgue integrals in , and every expectation of a tree functional comes with a measurability conclusion, so that no integral can take a junk value. Constants are quantified before the graph, the tree law and the field, and, where the paper names their dependence (Theorem 4.2's and ), as functions of exactly those parameters.
Two readings are fixed explicitly. Theorem 2.7 is stated for every positive BP fixed point, which by Theorem 2.6 is the paper's fixed point. Corollary 4.5's clause (4.13) carries the hypotheses of Theorem 4.2 ( on ). A fixed point that is not a family of distributions, a "zero message" family, or a bound that holds only because an integral defaults to does not satisfy these statements.
The computation tree of §5, through which the paper derives Theorems 2.6–2.7 from Corollary 4.5, is a proof device and is not part of any statement; building it is welcome as supporting work. Proofs of the classical inequalities (Griffiths, GHS) are independently reusable.