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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
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?
Sample covariance matrices are the basic object of multivariate statistics: principal component analysis, factor models and signal detection all start from the eigenvalues of built from observations of variables. When is comparable to , the largest eigenvalue of is no longer a consistent estimate of the largest population eigenvalue, and the question of when a "spike" in the population covariance is visible in becomes a question about the law of at large .
Timeline.
This mission formalizes the critical and subcritical side of that transition, Theorem 1.1(a) of the 2005 paper.
Let with independent real normal variables of mean and variance : a standard complex Gaussian. Let , , , be i.i.d. standard complex Gaussians. Fix an unitary matrix and positive reals , the population eigenvalues, and put . The samples are , mean-zero complex Gaussian vectors with covariance . The sample covariance matrix is and is its largest eigenvalue. Write .
The limit laws are built from the Airy function , integrated along a contour from to , and the Airy kernel
For , (with the pole above the contour) and . The Fredholm determinant of a kernel on is its Fredholm series
and
is the GUE Tracy–Widom distribution and .
Fix integers . Let with , and suppose , and stay in a compact subset of . Then for every real ,
The goal leaves arbitrary and allows to vary inside along the sequence. A companion item states Corollary 1.1(a): in probability.
Theorem 1.1(a) shows that is the exact threshold. Spikes strictly below it do not change the Tracy–Widom limit of . spikes exactly at it produce a new family of limit laws on the same scale. Together with part (b), where separates and fluctuates on the scale , it gives the first complete description of the transition. It is the reference point for spiked-model results on detection limits in PCA, for the real case (Bloemendal–Virág, Mo) and for finite-rank perturbations of Wigner matrices (Péché, Féral–Péché).
The paper's proof is complete and has been in the literature since 2005. No part of it is machine-checked. The mission produces:
The obvious approach is to compute the law of from the eigenvalue density, which is explicit (61). It fails because the density is an -fold integral whose integrand is a signed determinant, so no direct limit exists. The paper converts it into a Fredholm determinant of a double contour integral kernel. Two steps then carry the difficulty.
First, the steepest-descent analysis. With spikes at , the poles of the integrand sit exactly at the double critical point of the phase function. The contour cannot pass through the critical point and must enclose these poles, so it has to be routed at distance of order to the left of . All estimates must be uniform in and in the remaining spikes.
Second, the passage from kernel convergence to convergence of Fredholm determinants. It needs bounds strong enough to control every term of the Fredholm series, which is what the exponential tails in Proposition 3.1 provide. The functions grow polynomially, so even the finiteness of (Lemma 3.3) needs an argument.
Lean encoding:
Trivializing formalizations ruled out:
Infrastructure needed and reusable:
The Fredholm-determinant layer and the Airy function are reusable in any Tracy–Widom result. Andréief's identity and Hankel's formula are reusable well beyond random matrices.
Contributions welcome: proofs of any milestone, and lemmas that bound Fredholm series by Hadamard's inequality.
Firms that buy from unreliable suppliers have two broad ways to protect themselves against supply disruptions: dual sourcing, which splits the order between two suppliers so that a shortfall at one is cushioned by the other, and process improvement, which invests in a supplier's operations so that it fails less often. 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-period model in which the uncertainty is in the supplier's capacity, not in a proportional yield.
Real supply bases are rarely symmetric. Suppliers differ in cost, reliability and capacity because of their history or location, and the paper (p. 501) cites evidence that global sourcing has widened those differences. This mission formalizes the paper's analytical answer to one question this raises: as two otherwise identical suppliers drift apart in unit cost, which strategy gains? The paper's answer (Theorem 7, p. 502) is that the advantage of single sourcing with improvement over dual sourcing grows with the cost gap.
A firm sells one product over one season with unit revenue , salvage value and penalty per unit of unmet demand; demand has a known law with finite mean. Supplier has unit cost , committed-cost fraction and design capacity . Its realized capacity loss has a continuous distribution indexed by a reliability index ; a larger index means a stochastically smaller loss: implies for all . Losses are independent of each other and of demand.
An order delivers and costs . The realized profit is
the second-stage expected profit is , and .
In Lean these objects are MitigateSupplyRisk.Heterogeneity.Model (with Pi2, Pi2star, PiDS, Pi1single, PiSSI, Pi1) and SymData (with costModel Δ and etaModel Δ).
For suppliers identical except in unit cost,
The statement fixes no parameter values and no particular distribution; it asserts only the direction of the effect.
Theorem 7 turns a strategy comparison into a comparative-statics statement: once SSI is preferred at some cost gap, it stays preferred at every larger gap, so the preference switches at most once along a cost-heterogeneity path. Theorem 6 shows separately that both strategies benefit from heterogeneity, which is immediate for a single-sourcing strategy but not for dual sourcing, where one supplier improves and the other deteriorates. Lemma 5 is the structural fact the paper uses for the combined strategy: improvement efforts at the two suppliers are substitutes.
The results are proved in the paper's online appendix, which this formalization does not use. To our knowledge none of them has a machine-checked proof. A formal development would supply reusable pieces: an expected-profit model for random capacity with integrable profits, envelope and convexity arguments for suprema of affine families, and monotone comparative statics for single- and dual-supplier newsvendor problems.
and are both nondecreasing in (Theorem 6), so the goal compares the growth rates of two optimal values. Neither has a closed form. Both are suprema of families affine in , so they are convex but may have kinks, and an optimal improvement level need not exist when the index set is unbounded. The comparison concerns orders at different cost levels and under different strategies, so it needs a link between the dual-sourcing order from the cheaper supplier and the single-sourcing order and its response to improvement. Evaluating each side at a fixed optimizer does not give it, because the two optimizers move with . For Lemma 5, submodularity of in for each fixed does not pass to the supremum over by itself.
Fin 2. Each is the cdf of a measure ν i a on ℝ. Expectations are Bochner integrals against the product of the two loss laws and the demand law. The integrand is bounded by a constant times , so the integrals are genuine.Model.Standing and SymData.Standing):
MonotoneOn.Contributions are welcome at every level: integrability and boundedness lemmas for , convexity of the optimal values in , the symmetry argument behind Theorem 6(b), and monotone comparative statics of single-supplier orders in the reliability index.
A -join of a graph is a set of edges such that exactly the vertices of a prescribed even set have odd degree in . Minimum -joins are a classical object of combinatorial optimization: they contain shortest paths (), Chinese postman tours and perfect matchings as special cases, and their duality with -cuts connects them to integral multiflows. Whether the minimum size of a -join equals the maximum number of disjoint -cuts has been studied extensively; equality always holds in bipartite graphs (Seymour 1981).
Sebő and Tannier (Math. Oper. Res. 2004) study the number of connected components of a minimum -join, motivated by the observation that a minimum -join with few components yields a large integral packing of -cuts. Deciding whether some minimum -join has at most components is NP-complete in general (their Theorem 5). This mission formalizes the opposite end, : Theorem 6 characterizes exactly when a minimum -join can be chosen connected, in terms of the shortest-path metric of restricted to . The result first appeared in the authors' IPCO paper Connected joins in graphs (2001); the 2004 article derives it from its theory of isometric embeddings.
All graphs are finite, simple, undirected and connected. For vertices of , is the number of edges of a shortest – path. For , is the restriction of to pairs of vertices of .
For an edge set , is the number of edges of at ; is a -join if is odd exactly when . A minimum -join has the fewest edges among all -joins; a minimal one has no proper subset that is a -join. is the set of endpoints of edges of ; is connected (a tree) when the graph is connected (a tree), and is the distance in .
An isometry from to is a map with for all . A metric on a finite set is a tree metric if there is a tree (unit edge lengths) and an isometry from to ; the pair is a realization. A realization is inclusionwise minimal if no proper subtree of contains . A tree is an -join if its vertices of odd degree are exactly those of .
For connected and nonempty of even cardinality,
The conditions are required of every minimal realization; all of them are isomorphic.
Theorem 6 turns the existence of a connected minimum -join, a question about all -joins of , into conditions on the finite metric alone plus one isometric embedding of a tree into . Tree metrics can be recognized and their minimal realization constructed efficiently (Buneman 1974), and the embedding problem is the one solved in §2 of the paper, since contains all leaves of . The authors deduce that connected minimum -joins can be found in polynomial time, which contrasts with the NP-completeness of the same question for components. A consequence stated in the paper: if the minimal realization of is not a -join, then no minimum -join is connected.
The result is proved in the paper. No machine-checked version of Theorem 6, of Lemma 2, or of the uniqueness of minimal tree realizations is known to exist; Mathlib has graph distances, trees and walks, but neither -joins nor tree metrics. The mission produces these definitions and a formal proof of the characterization; the complexity consequence is out of scope.
The central difficulty is in the necessity direction. A connected minimum -join is itself a minimal realization of (Lemma 2), so satisfies the conditions; but the conditions concern the minimal realization, and transferring them from to an arbitrary minimal realization requires that minimal realizations are unique up to a label-preserving isomorphism. That uniqueness (milestone 3) is the step where the obvious approach stops: it is a statement about all trees realizing a metric, not about the graph .
SimpleGraph V with [Fintype V] [DecidableEq V]; G.Connected is a hypothesis of every statement about (SimpleGraph.dist is on unreachable pairs). Distances are natural numbers (SimpleGraph.dist).Finset (Sym2 V). Connectivity, the tree property and refer to the graph with edge set induced on , not on all of .Fin N together with a map Fin N; this avoids quantifying over a universe. A tree metric must satisfy .Reusable beyond this mission: the -join vocabulary, the path decomposition of minimal -joins, and tree metrics with the uniqueness of minimal realizations. Contributions to any milestone are welcome, as are alternative proofs of milestone 3.
Many objective functions in engineering and statistics are nonsmooth and nonconvex: the spectral abscissa of a parametrized matrix, the largest eigenvalue of a symmetric matrix function, the norm of a closed-loop system, or a maximum of finitely many smooth functions. Such functions are typically differentiable almost everywhere, yet their minimizers usually sit exactly where the gradient fails to exist. Gradient descent then zig-zags or stalls, and bundle methods, which are designed for convex functions, lose their guarantees.
Burke, Lewis and Overton (SIAM J. Optim. 15 (2005) 751–779) proposed the gradient sampling (GS) algorithm: at each iterate, sample gradients at random nearby points, take the element of least norm in their convex hull, and search along its negative. The method needs nothing beyond gradients at points of differentiability, and it has since become a standard tool for nonsmooth, nonconvex minimization (Burke, Curtis, Lewis, Overton, Simões, 2020). This mission formalizes the paper's convergence theory.
Timeline. Goldstein (1977) introduced the -subdifferential of a Lipschitz function and a conceptual descent method built on it. Clarke's generalized gradient (Clarke 1983) supplied the stationarity notion. Burke, Lewis and Overton (2005) made Goldstein's idea implementable by random sampling and proved almost-sure convergence to Clarke -stationary points for a fixed sampling radius. Kiwiel (2007) revisited the analysis and proved convergence for a modified version of the algorithm.
Let be locally Lipschitz, and let be an open dense set on which is continuously differentiable. Write for the closed Euclidean unit ball, and fix such that the level set is compact.
The Clarke subdifferential is the convex hull of all limits with and differentiable at each . For define
and the Clarke -subdifferential . A point is Clarke -stationary if , and Clarke stationary if .
The GS algorithm. Fix , , , , , and a sample size . At iteration :
With and the radius stays fixed, : this is fixed-radius mode.
In fixed-radius mode, with probability , either the algorithm stops at some iteration with , or it runs forever and there is a subsequence with
The theorem asserts nothing about along ; the authors list as an open question.
The milestones follow the paper's argument: the minimax characterization of the search direction (Lemma 2.1), the line-search descent estimate and the descent property of the iterates (§2), the almost-sure absence of a Step 1 stop, upper semicontinuity of and the uniform covering of Lemma 3.2(iv)–(v), Lebourg's mean value theorem (Theorem 3.3), the representation , the estimate of Lemma 3.1, the inclusion , and the closed graph of .
Well-posedness of the algorithm (every sample realization admits a run), Corollary 3.5(1) (the case: ), Corollary 3.6 (Clarke -stationary points with cluster at Clarke stationary points, and with a unique stationary point in the sets converge to it in the Hausdorff sense), Corollary 3.7 (with a unique stationary point in , small forces the run near it), and Theorem 3.8 (the variable-radius mode with ).
Theorem 3.4 is the first convergence guarantee for a practical method on general locally Lipschitz, nonconvex functions that uses only gradients at points of differentiability. It holds for a fixed sampling radius, the setting where most of the work is, and Corollaries 3.6–3.7 and Theorem 3.8 transfer it to radii decreasing to zero, which is how the method is used in practice. Later gradient sampling variants and their analyses start from these results.
The results are proved on paper; no machine-checked proof of them is known. A formalization would make the probabilistic structure precise, which the paper leaves informal (see Formalization scope), and would certify the hypotheses under which the theorem holds. Already the statements record two such corrections.
The natural argument, " decreases and is compact, so the steps tend to zero, hence ", fails: can go to zero while stays bounded away from zero. The difficulty is to show that, on the event , the random samples land infinitely often in a configuration whose sampled hull nearly realizes at a fixed nearby point, uniformly over a compact set of iterates, and that the failed trial step at such an iteration contradicts the Armijo rule. The iterates depend on all past samples, so independence across iterations cannot be used directly.
EuclideanSpace ℝ (Fin n), is Mathlib's gradient, the Clarke subdifferential is the published ClarkeGradients.Shared.generalizedGradient, and is Metric.infDist 0 C. Local Lipschitz continuity is Mathlib's LocallyLipschitz; continuous differentiability on is ContDiffOn ℝ 1 f D.IsGSRun on the iterates, radii, tolerances, step lengths, least-norm vectors, directions and a stopping index , imposing Steps 0–4 up to . "" is the least admissible , and the Armijo and (2) inequalities are strict.IsRandomGSRun) lives on a probability space with a filtration : the samples are uniform on , independent within an iteration, and independent of , while are -measurable. The Step 4 choice may use the past and extra randomness but never future samples. "With probability 1" is ∀ᵐ. The paper's event , the realizations that hit every positive-measure subset of infinitely often, is not used, because no sequence has that property.In a linearly parameterized bandit, the expected rewards of many arms are driven by a small number of unknown parameters. Each arm is a vector , and its expected reward is the inner product with an unknown parameter vector . Problems of this kind arise in marketing and revenue management, where each product is described by features (price, popularity, …) and the expected revenues of thousands of products are, to a good approximation, linear in a few unknown feature weights. Pulling one arm then reveals information about all of them, and a good policy has to exploit this correlation.
Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, 2010) studied this model with unbounded, sub-Gaussian noise and a prior on . They proved an lower bound, a matching policy for smooth arm sets, and the Uncertainty Ellipsoid (UE) policy for arbitrary arm sets. This mission formalizes their Theorem 4.2: when the set of arms is finite, the regret of UE grows like , within a constant factor of the Lai–Robbins lower bound for the classical multi-armed bandit (Lai and Robbins, 1985).
Timeline.
Let and let be a finite, nonempty set of arms. Fix , the value of the unknown parameter. Playing arm in period yields the reward . The noise is drawn afresh in each period from a law that depends only on the arm played, independently of the past. A policy chooses the arm of period as a function of the history . The regret given is
and for a prior of the Bayes risk is . The gap of arm is , and is the number of periods among the first in which is played.
Assumption 1.
The UE policy first plays . It then forms the least squares estimate with , and plays an arm maximizing . The uncertainty radius is
with and . Ties are broken arbitrarily.
There are constants depending only on such that for all and ,
If moreover each has a point mass at and a density bounded by on , there are depending only on with
The constants are left unspecified, as in the paper. Their existence, uniformly in and in the arm set, is the content.
The result. For a fixed finite arm set, Theorem 4.2 shows that a single anytime policy, which does not know , has regret for every parameter and Bayes risk . It does this with unbounded noise and correlated arms. The dependence on the problem enters only through the gaps and the number of arms. The companion result for general compact arm sets (Theorem 4.1) gives only . The finite case shows that the same policy adapts to the easier problem.
Formalizing it. The theorem is proved on paper. As far as is known, it has no machine-checked proof. The platform's finite-armed bandit library (Lattimore–Szepesvári) has the regret decomposition and UCB pull-count bounds for independent arms, e.g. BanditAlgorithm.bandit_regret_decomposition. Those statements live in a different model and do not apply to correlated linear rewards with a least squares estimator. This mission adds:
The arms are chosen adaptively, so the design matrix is random and depends on the noise. Applied with the realized , the classical Chernoff bound for a fixed weighted sum of independent noises is not valid. The obvious union bound over arms does not apply either: the event concerns the random matrix , not one arm. In the pull-count bound, the radius of arm must be controlled through the number of times was played, although mixes all arms, and the Gram matrix of the other arms may be singular.
EuclideanSpace ℝ (Fin r), so is Euclidean. The source is arXiv:0812.3465v2; its printed page numbers equal the PDF's.Set, and is its ncard. Theorem B.2 and Lemma B.6, which the paper states for any compact arm set, are stated for compact nonempty arm sets, as printed.The eigenvalues of a large non-Hermitian random matrix are hard to study directly. For Hermitian matrices, the empirical spectral distribution (ESD) is controlled by the resolvent and the Stieltjes transform, both stable under small perturbations. For non-Hermitian matrices no such tool exists: eigenvalues can move a long way under tiny perturbations, and the moment method fails because moments do not determine a measure on . The route that works, going back to Girko (1984) and used by Bai (1997), Götze–Tikhomirov (2007), Pan–Zhou (2007) and Tao–Vu (2008), passes through logarithmic determinants. The identity links the ESD to a scalar quantity. That scalar is computable from the singular values of , which are eigenvalues of a Hermitian matrix.
Tao and Vu, with an appendix by Krishnapur (Ann. Probab. 38 (2010) 2023–2065), turn this link into an exact criterion. Theorem 1.15 of that paper states that the ESD of a normalized i.i.d. random matrix converges to a measure if and only if the normalized log-determinants converge to the logarithmic potential of for almost every . The same holds for a regularized version built from the singular values. This mission formalizes Theorem 1.15 and the main steps of its proof (§8 and Appendix A of the published article).
Let be a complex random variable with and , and let be independent copies of on a probability space . For each , . Let be deterministic complex matrices with
and put .
For with eigenvalues , counted with algebraic multiplicity, the ESD is . Its singular values are . A sequence of random measures converges in probability to a deterministic if, for every continuous compactly supported , tends to in probability. It converges almost surely if, with probability one, for all such at once. The logarithmic potential of a measure is .
Hypothesis (1.4) states that, for almost every , the ESDs of the deterministic matrices converge to a limit.
In Lean everything lives in the namespace UnivESD.LogDet. The ESD is esd, the one-based singular value is sv, logPotential is the logarithmic potential, and ConvInProb/ConvAS/ESDConvInProb/ESDConvAS are the modes of convergence. IIDArray is the entry model, HSBound is (1.3), shiftA M xs z n ω is , and Cond14 is (1.4).
Let be a probability measure on with . The following are equivalent:
in probability.
Under (1.4) the same equivalence holds with almost sure convergence throughout.
Theorem 1.15 reduces convergence of a non-Hermitian ESD to a family of scalar limit statements. Each of these can be attacked through Hermitian tools, because the regularized log-determinant in (iii) is a smooth functional of the singular values. Corollary 1.16 of the paper derives from it a practical criterion: the ESD converges to once the singular value distributions of converge for a.e. to laws with . With the universality principle (Theorem 1.5, the companion mission) and Mehta's computation for complex Gaussian matrices, this yields the circular law for i.i.d. matrices with finite variance.
The theorem is proved in the source. To our knowledge neither it nor any of its milestones has a machine-checked proof. Mathlib has the ingredients for the objects (characteristic polynomials and their roots, LinearMap.singularValues, the strong law of large numbers) but not the results. A formal proof would give the platform its first verified bridge between eigenvalue and singular value asymptotics. Lemma A.3 alone, Weyl's multiplicative majorization, is a standard linear-algebra fact absent from Mathlib.
Two things make the obvious argument fail. First, is unbounded at . Vague convergence of controls only for continuous compactly supported , while has a singularity at and grows at infinity. Passing between (i) and (ii) therefore requires uniform control of the eigenvalues (and singular values) near after the shift: the contribution of the smallest ones must vanish. Second, eigenvalues are not stable under perturbation, so this control cannot be read off the eigenvalues. It has to come from the singular values, through a lower-tail bound on that is exponentially small in a power of , and through a deterministic inequality transferring bounds from singular values to eigenvalues. The smallest singular values ( below ) need a separate polynomial lower bound (the paper's Lemma 4.1, posed in the companion mission). The tail bound in its printed form is false at that end of the range.
Conventions committed to in Lean:
Integrable (‖w‖²) μ. The logarithmic potential is a Bochner integral, which is when not integrable; by (8.1) this happens only for a null set of , which "for a.e. " ignores.Real.log 0 = 0. In (ii), a singular matrix would contribute instead of ; for this model the determinant is almost surely nonzero eventually. Every milestone with or carries positivity of those quantities in its conclusion.sv A i is Mathlib's singularValues (i-1)). Eigenvalue enumerations are Fin n-indexed, and the paper's is index .Disclosed corrections to the printed text:
A trivializing formalization is ruled out by construction. The goal mentions only and . The proof's comparison ensemble is not a hypothesis. No statement takes a log-potential or a log-determinant as an input that could be fixed to make it hold.
The companion mission (Theorem 1.5, universality) poses Theorem 2.1 (the replacement principle), Lemma 1.7 (tightness) and Lemma 4.1 (least singular value), which the proof here also uses. They are not restated here. Once that mission is published they belong here as references. Contributions are welcome on the linear-algebra layer (Lemma A.3, multiplicative Weyl majorization), the Fubini argument of (8.1), and the singular-value tail bound (8.3). These are reusable well beyond this paper.
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.
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.
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 .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.
In a linearly parameterized bandit, a decision maker repeatedly chooses an arm from a set and observes a noisy reward whose mean is the inner product with an unknown parameter vector . The model covers pricing, assortment and recommendation problems in which arms are described by feature vectors and the number of arms is large or infinite, so that learning arm by arm is hopeless and information must be shared through the common parameter.
Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, published in Mathematics of Operations Research, 2010) give matching lower and upper bounds of order for this problem when the arm set is the unit sphere. This mission is the lower bound, Theorem 2.1. It says that the dimension enters the regret linearly and that no policy can do better than , which makes the phased exploration policy of the paper's Section 3 optimal up to a constant.
Timeline. For , Mersereau, Rusmevichientong and Tsitsiklis (2009) showed regret and Bayes risk . Dani, Hayes and Kakade (2008) proved an minimax lower bound for a compact arm set built from products of circles. Rusmevichientong and Tsitsiklis (2010) proved the lower bound for the sphere itself, both for the regret and for the Bayes risk under a Gaussian prior, with the explicit constant .
Fix a dimension . The arms are the unit sphere , with the Euclidean norm . The unknown parameter is drawn from the prior : each coordinate is an independent normal with mean and variance , so . Playing arm in period yields the reward
where the noise variables are independent standard normals, independent of .
A history lists the arms played and rewards observed up to period . A policy chooses the arm of period from the history. Since , the regret of given and the Bayes risk of over periods are
The milestones use the least mean squares estimator and orthonormal vectors that are orthogonal to and are functions of .
For every policy and every ,
The constant is absolute; the parameter may depend on .
The result. Theorem 2.1 shows that the regret and Bayes risk of linearly parameterized bandits grow at least linearly in the dimension, even when the arm set is as regular as a sphere and the noise is Gaussian. Together with the paper's Theorem 3.1 it pins the optimal order at on the sphere, and it shows that the Bayes risk achievable in dimension one does not survive in dimension two or more. Since the sphere is one compact arm set, the theorem also shows that the paper's upper bounds of order for general compact arm sets (Section 4) cannot be improved beyond logarithmic factors in that generality (Table 1, p. 8).
Formalizing it. The theorem is proved in the paper; to our knowledge it has not been machine-checked. The platform has a minimax lower bound for the unit ball with a fixed-norm parameter (Lattimore and Szepesvári, Theorem 24.2), which is a different statement: a frequentist bound over a finite family of parameters, not a Bayes risk under a continuous Gaussian prior. Formalizing Theorem 2.1 requires Gaussian posterior computations with an adaptively chosen design, a piece of Bayesian linear regression that is reusable well beyond bandits.
The obvious argument fixes the parameter's norm and treats the problem as a Gaussian estimation problem in each direction orthogonal to the current estimate. That fails because is random under the prior: the risk per direction trades off exploration, weighted by , against estimation error, weighted by , and neither weight is bounded. The proof has to localise to an interval with positive probability uniformly in , which is the content of Lemma 2.4 and the reason the lemma needs .
The second obstacle is that the design is adaptive: the arms depend on past rewards, so the posterior of given must be identified as Gaussian with covariance even though the regressors are random and history-dependent. Lemma 2.3 rests on this identification and on a matrix inequality for diagonal entries of an inverse.
The source is arXiv:0812.3465v2; its printed page numbers equal the PDF's. All declarations live in the namespace LinParamBandits.LowerBound.
EuclideanSpace ℝ (Fin r), so norms are Euclidean and inner is . Every theorem carries , the paper's standing assumption.stdGaussian); the noise is an i.i.d. standard normal sequence (Measure.infinitePi), independent of .arm ψ z η t is the paper's .A complete development needs: measurability of the trajectory map, the Gaussian posterior for a sequentially chosen design, the inequality for positive definite , a chi-square lower-tail bound, and Gaussian tail values. The posterior computation and the chi-square bound are reusable; contributions of either, or of a proof of any single milestone, are welcome.
Facilities fail: plants close, warehouses flood, suppliers strike. Reliable facility location models choose facility sites knowing that each opened site may be unavailable, and they assign every customer a primary facility and an ordered list of backups. Snyder and Daskin (Transportation Science, 2005) introduced the level-assignment formulation with a common failure probability. Cui, Ouyang and Shen (Operations Research 58(4), 2010; working paper UCTC-FR-2010-02, February 2010) let every site have its own failure probability , with failures independent. With site-dependent probabilities, even for fixed open sites, the best backup list for one customer is no longer simply the nearest sites in order of distance (their Example 1, p. 11).
The paper solves the model by Lagrangian relaxation. Relaxing the constraints that link assignments to open sites splits the problem into one relaxed subproblem (RSP) per customer , solved at every subgradient iteration. The authors show that (RSP) is the minimization of a set function over sets of at most sites, and their Proposition 3 asserts that is supermodular, which makes the branch-and-bound algorithm of Goldengorin et al. for supermodular minimization applicable. This mission formalizes Proposition 3 and the steps of its proof (Appendix A.3).
Fix a customer with demand rate and unserved-demand penalty . There are regular sites with unit costs , failure probabilities and Lagrange multipliers . An emergency facility with index never fails () and costs per unit: being served by it means not being served. The customer is assigned at levels with . A level- facility serves the customer exactly when the facilities at levels have all failed.
The variables are (site is the level- facility), (the probability that serves at level , given the earlier levels) and , which the linearization constraints force to equal . The constraints of (RSP) say that every level is filled by one regular site or comes after the emergency facility, that each regular site is used at most once, that the emergency facility appears exactly once, and that
For a set , is the minimum of
over the feasible points that use no regular site outside . The customer's subproblem is .
For every customer , every and all regular sites outside with ,
The paper states " is supermodular" without restriction. That statement is false: for sets larger than the inequality can fail (an instance with , is recorded in the goal's statement). The cardinality bound covers all the sets the subproblem ranges over, and the paper's proof uses it implicitly.
Supermodularity of is what the paper's exact algorithm for (RSP) rests on: the branch-and-bound method of Goldengorin et al. prunes by comparing marginal costs, and its correctness requires them to be monotone. Each Lagrangian iteration solves such subproblems, so this property sits inside the paper's whole solution method. The closed form (milestone 1) is also a self-contained statement about the optimal backup order with site-dependent failure probabilities: once the set of sites is fixed, nearest-first is optimal, and sites beyond the penalty distance are never used.
Formally, nothing in this mission is machine-checked yet. The paper's argument has gaps that a formalization has to repair: the missing cardinality hypothesis; a "strict" sign claim (milestone 3) that is only weak when some or ; counts printed as infima; and an intermediate inequality in Case 2 that does not hold as printed, although the case's conclusion does. A checked proof settles which version of Proposition 3 is true.
The algebra of the cases is routine once the closed form is available. The hard step is the closed form itself: is defined as the minimum of a mixed-integer program, and the paper justifies the closed form only by "a similar argument as in the proof of Proposition 2", an exchange argument. One has to show that every feasible point is a nearest-first chain truncated at the emergency facility, that and are then determined by , that reordering a chain by distance never increases the cost, and that adding a site within the penalty distance never hurts. With at most regular levels, the exchange must respect the level budget. This is exactly where the cardinality hypothesis enters.
A tempting shortcut is to define by its closed form. That makes milestone 1 true by definition and detaches the goal from the optimization problem; the definition here is the program (5).
Lean conventions: one customer at a time, with the index dropped in the definition. Regular sites are Fin J; all sites are Fin (J+1), with Fin.last J the emergency facility, whose cost and probability are built into the extended data. Levels are Fin (R+1). Variables are real-valued, with as a constraint. is the infimum of the set of feasible objective values. This set is nonempty and bounded below, and in fact finite, so the infimum is the minimum. Data hypotheses: , , ; costs, penalties and multipliers carry no sign assumption. The list is any duplicate-free list of sorted by distance. Ties are allowed.
Printed typos corrected in the definitions: the level constraint (4b) counts the emergency facility in its first sum; (5b) includes the linearization constraints (4h); (5c) covers regular site ; (5a) has for the undefined .
Excluding the configurations with from the goal is deliberate. Weakening the goal further, for example to or to sets on which is modular, would trivialize it.
Contributions welcome: a proof of the closed form (an exchange argument on level chains, reusable for the other propositions of the paper), then the marginal-cost algebra and the two cases.
A large control system is often built from many subsystems , each of which is input-to-state stable (ISS) with respect to the states of the others. Whether the interconnection is again ISS is decided by a small gain condition on the matrix of interconnection gains. For two subsystems this goes back to Jiang, Teel and Praly (1994) and to the Lyapunov version of Jiang, Mareels and Wang (1996). For subsystems, Dashkovskiy, Rüffer and Wirth formulated the condition as a property of a monotone operator on (2007). Rüffer's thesis (2007) and the paper on which this mission is based (arXiv:0901.1842, SIAM J. Control Optim. 2010) turned it into a Lyapunov construction.
The construction needs a geometric object: a path in the positive orthant, unbounded in every coordinate, along which the gain operator strictly decreases every component. For a linear gain matrix this is a Perron vector. For nonlinear gains, its existence is the first of the paper's two main results (Theorem 5.2). This mission formalizes that theorem and the lemmas of §8 that prove it. The companion mission formalizes the second main result, the Lyapunov function built from such a path.
Write . Vectors in are compared componentwise: means for all , and means for all . A function is of class if it is continuous, strictly increasing and , and of class if it is moreover unbounded.
A gain matrix is with and . A monotone aggregation function (MAF) is a continuous with for , whenever , and as . Typical examples are sums and maxima. Given MAFs , the gain operator is
The paper assumes from p. 8 on that , restricted to the coordinates of the nonzero entries of row , still has the strict monotonicity (Remark 2.6). The small gain condition (SGC) is : for every , at least one component of is strictly smaller than the corresponding component of . The set
collects the points that every component of strictly decreases.
An -path (Definition 5.1) is a continuous with every component such that (i) each is locally Lipschitz on ; (ii) on every compact the derivatives of all , where they exist, lie in for constants depending on only; and (iii) for all .
Let be a gain matrix and a compatible vector of MAFs. Assume one of: (i) is linear with spectral radius less than one; (ii) is irreducible and ; (iii) and ; (iv) the entries of are bounded and . Then
In cases (i)–(iii) the entries are in , and in case (iv) they are in .
The milestones follow §8 in the order the proof uses them.
An -path turns a small gain condition into a Lyapunov function. If each is an ISS Lyapunov function of , then is one for the network (Theorem 5.3). So Theorem 5.2 is the step that makes the small gain condition a certificate of network stability, and the corollaries of §5–§7 (sums, maxima, neural networks) all pass through it.
The results are published and proved on paper. None is machine-checked: no proof assistant library contains MAFs, gain operators, the sets and , or -paths. The paper cites three ingredients without proof: Lemma 8.6, Proposition 8.9 and the scaling step of Theorem 8.11. It also gives Theorem 8.14 only as a sketch. Formalizing them closes those gaps in one place.
For bounded gains the problem is easy: far out, every point of a large ray lies in , and the only work is the descent to the origin. With entries, is unbounded and no ray need stay in . Following the image of a single point fails, because forward iterates go to , not to infinity. The paper instead uses backward orbits inside . That this set is nonempty and unbounded is a fixed-point argument of Knaster–Kuratowski–Mazurkiewicz type (Propositions 8.9 and 8.10), not a monotonicity argument. A second obstacle is strictness. A backward orbit is only -increasing, while Definition 5.1 needs strictly increasing components with derivative bounds. This is where the diagonal scalings of Lemmas 8.6–8.7 enter.
is ℝ≥0 and is Fin n → ℝ≥0, with subsystems indexed from . The strict order is a named predicate (SLt), never Lean's < on functions, which means " and ". The small gain condition is ∀ s ≠ 0, ¬ s ≤ T s. The inverses are carried as explicit two-sided inverses, and derivatives are ordinary real derivatives at points where they exist. Compatibility (Remark 2.6) and are hypotheses of every statement about . Irreducibility is the matrix-power form of p. 12, which Mathlib's Matrix.isIrreducible_iff_exists_pow_pos connects to Matrix.IsIrreducible. The spectral-radius hypothesis says that every complex eigenvalue has modulus . The 1-norm defines .
Hypotheses made explicit or corrected:
A path with , or with Lean's < on functions, is not an -path. Such a reading would make the goal follow from the origin alone, and it is ruled out.
Needed infrastructure: comparison-function calculus (inverses and compositions of functions), piecewise linear interpolation in with Lipschitz inverse bounds, and a KKM-type argument on the simplex. The first two are reusable well beyond this mission. Contributions of any milestone, proofs of the cited ingredients (Lemma 8.6, Proposition 8.9, Proposition 8.10, the scaling step of Theorem 8.11) and a full proof of Theorem 8.14 are welcome.
A manufacturer that sells through a retailer can accept returns: it pays a return credit for every unit the retailer has not sold at the end of the season. Returns policies are common in publishing, software and computer hardware, and since Pasternack (Marketing Science, 1985) they have been studied as a way to make the retailer order more. Retailers also raise demand through sales effort: merchandising, shelf space, point-of-sale advertising. A recurring view in the marketing and operations literature is that returns weaken this incentive. Padmanabhan and Png (1995, p. 70) write that "by reducing the risk of losses due to excess inventory, a returns policy lessens some of the retailer's incentive to invest in such efforts", and Kandel (1996, p. 348) makes the same argument for consignment.
T. A. Taylor, Supply Chain Coordination Under Channel Rebates with Sales Effort Effects (Management Science 48(8), 2002), studies a newsvendor retailer who chooses an order quantity and a sales effort level before demand is observed. Its Proposition 4 shows that in this model the conventional view is reversed: a larger return credit makes the retailer exert strictly more effort. This mission formalizes that proposition and the solution of the retailer's problem it rests on.
Prices satisfy and (Assumption A1): is the retail price, the wholesale price, the manufacturing cost and the salvage value, which may be negative. A demand factor has a density with for every (Assumption A4), distribution function and partial mean .
The retailer chooses an effort level , and demand is . Effort costs , where is strictly convex and strictly increasing with (Assumption A5; the paper declares every convexity and monotonicity statement strict). Write .
Under a returns-only contract with , the retailer orders , exerts effort , and earns the expected profit
This is the integrated channel's profit with in place of and in place of . An optimal pair is a maximizer of over , . The paper's is the effort of such a pair, and is the critical fractile .
If , is an optimal pair under the credit , is an optimal pair under , and , then
The paper writes this as . Its proof shows strict monotonicity, and that is the statement here.
For a fixed , the unique maximizer of over is , and
An optimal pair with satisfies
and conversely every solving this first-order condition gives the optimal pair .
The result. Proposition 4 separates two effects of a return credit. For a fixed order quantity, a larger credit lowers the marginal value of effort: it pays the retailer for unsold units, and effort only matters through sold units. This is the fixed-quantity comparison on which the conventional view rests; Cachon's survey states it for buy-backs as Eq. (19) (on Prove2Me as CachonCoord.EffortNewsvendor.sec_6_4_1_effort_coordination, clause 1). Once the order quantity is chosen together with the effort, the larger credit raises the order, and the effort follows. For the multiplicative demand model the net effect is unambiguous for every demand density and every convex effort cost. A manufacturer that wants more retailer effort can therefore use the return credit as a lever, and a model that ignores the quantity response gets the sign wrong.
Formalizing it. The result is proved in the paper, in a four-line appendix argument that relies on the §4.2 solution of the retailer's problem; neither is machine-checked anywhere. The mission produces a checked newsvendor-with-effort solution (the scaling and the profit ), which the other missions of this series and any multiplicative-effort supply-chain model can reuse, and a checked statement of the comparative statics in the return credit.
The obvious argument differentiates the retailer's first-order condition in with the order held fixed, and it gives the wrong sign; the order quantity must be re-optimized. The correct comparison runs through the reduced problem in the effort alone, and it needs the §4.2 solution in full: the scaling of the optimal order with the effort, which turns and into newsvendor expectations of at ; the value of the optimal order as a function of ; and the first-order characterization of the optimal effort. The comparison across credits then involves two objects: the function , and the retailer's reduced profits under the two credits at a common effort level. The statement compares maximizers of two different optimization problems, not roots of an equation, so a formal proof must connect optimality of the pair to the first-order condition, which uses the strict convexity of and the positivity of the density.
Everything lives in the namespace ChannelRebate.ReturnsEffort. The definitions file holds:
Demand: a measurable density , zero on , positive on , integrating to , with finite mean;EffortCost: A5 with strict convexity and strict monotonicity on and ;returnsProfit;The expectations are the published CachonCoord.Newsvendor.expSales and expLeftover applied to the law of (the image of the law of under ).
The formalization makes the following commitments, each recorded on its item:
The goal is about optimal pairs of the joint problem. Defining as the root of the first-order condition, or fixing the order quantity and varying , would give a different and, in the second case, false statement; neither is the target.
Contributions are welcome:
The two facts the paper's proof uses — that is strictly increasing on , and that the retailer's reduced profit at a fixed effort increases with the credit — may be posted as supporting theorems.
Manufacturers of computer hardware, software and automobiles routinely pay their retailers channel rebates: a payment per unit the retailer sells to end customers. A target rebate pays only for units sold beyond a target level. These industries also commonly offer returns: a credit for each unsold unit. Both instruments are used to change the retailer's behaviour, and the retailer controls two things that matter to the manufacturer: how much stock she orders, and how much sales effort she exerts to raise demand. Effort cannot be observed or written into a contract, but sales can.
T. A. Taylor's paper (Management Science 48(8), 2002) asks whether a contract built on sales and returns can make an independent retailer choose the effort level and the order quantity that maximize the profit of the whole supply chain, while splitting that profit in any desired proportion. Its Proposition 2 shows that returns alone, linear rebates alone, or target rebates alone cannot do this. Its Theorem 2, the goal of this mission, shows that a target rebate combined with returns can, when demand is uniform and effort cost is quadratic.
A manufacturer with unit production cost sells to a retailer at wholesale price ; the retailer sells at the fixed retail price , and unsold units have salvage value . The standing assumption is and ( may be negative). Before demand is seen, the retailer chooses an order quantity and an effort level . Demand is , where is uniform on , with distribution function and . Effort costs , .
The integrated channel, which owns both firms, earns
Its optimum uses the critical fractile , defined by , the effort and the order . Its optimal profit is , where .
A target rebate and returns contract pays the retailer for every unit sold beyond the target , and credits her for every unsold unit. Her profit is
The manufacturer earns . The other quantities the statements use are:
Contract terms of Theorem 2. Put and
and are the fixed points on of and , with and evaluated at , . and are the retailer's profits at effort and at effort .
For every there is such that for every the following holds. Pairs with
exist. Every such pair gives , and . The pair is the retailer's unique optimum under , and
The result. Theorem 2 shows that two contractible instruments can align two decisions, one of them not contractible. The rebate pushes effort and quantity up when sales are high, and the return credit raises both when demand is low. Together they reproduce the integrated channel's optimum , and the free parameter allocates the profit between the firms in any proportion. Proposition 2 of the same paper rules out each instrument alone. This makes Theorem 2 the basis for the paper's recommendation that rebates and returns be used together. The uniform instance is the only one in which the paper proves this; for normal demand it gives only numerical evidence.
Formalizing it. The theorem is proved in the paper; it has not been formalized. The printed proof treats the wholesale price as fixed while it varies: and contain , so , and move with . A machine-checked proof therefore has to repair the argument, not only transcribe it. A numerical check (p = 10, c = 4, s = 1, a = 1; for example κ = 1.2, ε = 0.012 gives w* ≈ 4.889, T* ≈ 1.095) found the statement itself consistent.
The retailer's problem is not concave. For fixed effort, has a kink at , and the optimal order jumps from to at . After the order is optimized out, the profit in effort, , has an upward kink at and can be convex and then concave beyond it. Checking the first-order condition at is therefore not enough. Coordination is a statement about the global maximum of a kinked, non-concave function, and comparing the two local candidates is what the threshold and the profits , do. The contract is then pinned down by two equations in whose coefficients themselves depend on through and .
Everything is stated for , taken as Lebesgue measure on , and for , as in all of Lemmas 3–6 and Theorem 2. Lemma 2 and the §4.1–4.2 solutions, which the paper states for general demand, are specialised to this instance. The uniform law has bounded support, so the paper's Assumption A4 (positive density on ) is not imposed; the paper allows that relaxation on p. 995.
The expectations use the published expSales and expLeftover (Cachon's newsvendor definitions) of the image law of under . and are integrals of the uniform density, not hard-coded closed forms. Every inverse (, , ), the threshold , the function and its root , the fixed points , and the profits , are stated by their defining equations, never by a choice function. "Optimal" means a maximizer over , . Channel coordination means that the retailer's set of maximizers is exactly . The manufacturer's profit , which the paper does not display, is written from the contract's cash flows: units bought back at are salvaged at .
A trivializing formalization is ruled out: coordination is global optimality of , not a first-order condition at . may depend on but not on . and are tied to their fixed-point equations and are not free variables.
A complete development needs:
The uniform newsvendor identities and the kinked-maximization lemmas are reusable beyond this mission. Contributions to any milestone, and alternative proofs of the existence part of Theorem 2, are welcome.
An insurance company that collects premiums and pays random claims is ruined when its surplus becomes negative. The probability of ultimate ruin is the classical solvency criterion of risk theory, going back to Lundberg and Cramér. Real insurers have two levers on this probability: they can invest part of the surplus in a risky asset, and they can cede part of every claim to a reinsurer, at a price. The question of how to use both levers dynamically, as a function of the current surplus, so as to make the probability of ruin as small as possible, is a stochastic control problem for a jump-diffusion.
H. Schmidli, On minimizing the ruin probability by investment and reinsurance, Ann. Appl. Probab. 12 (2002), solves this problem for the Cramér–Lundberg model with proportional reinsurance and investment in a Black–Scholes asset. The main results are a verification theorem (Theorem 1, the subject of this mission) and an existence theorem for the associated integral equation (Theorem 2, the companion mission).
Timeline. Hipp and Plum (2000) treated investment in the Cramér–Lundberg model through the Hamilton–Jacobi–Bellman equation, assuming a bounded solution. Schmidli (2001) treated optimal proportional reinsurance alone. The 2002 paper combines investment and reinsurance, and proves the verification theorem without assuming the solution to be bounded.
Claims arrive at the jumps of a Poisson process with rate ; the claim sizes are i.i.d. with continuous distribution function , , independent of . The insurer receives premiums at rate . A risky asset , with and a standard Brownian motion independent of the claims, is available.
A strategy is a pair of processes , predictable for the smallest right-continuous filtration generated by the claims and : is the amount invested in the risky asset (locally bounded), and is the retention level, meaning the insurer pays of a claim occurring at time , at a reinsurance premium rate . The surplus starting from solves
where is the aggregate claims process. The ruin time is , the survival probability is , and the value function is .
The premium function is decreasing and continuous on , , , and there is with for and for (full reinsurance is too expensive).
The Hamilton–Jacobi–Bellman equation for is, with the convention for ,
For strictly concave the maximum over is attained at (equation (2)); denotes a measurable maximiser in .
Let be strictly increasing and nonnegative on , continuous there, twice continuously differentiable on , zero on , and a solution of (1) at every . Then is bounded, ,
and every surplus process from following , has survival probability .
The proof of Theorem 1 runs through: Lemma 3 (for small surplus the optimal retention is ); the identity along the feedback strategy; the inequality for every strategy; Lemma 1 (almost surely, either ruin occurs or ); the existence of a strategy with ; the comparison with equality for the feedback strategy; and the absence of ruin by creeping, .
The second sentence of Theorem 1 (that satisfies the hypotheses whenever is a decreasing solution of the integral equation (5)) and its last sentence (at most one such solution of (1) with ) are separate items.
Theorem 1 reduces a control problem over all predictable strategies to an analytic question: find one increasing smooth solution of (1). Combined with Theorem 2 (existence of a solution of (5)), it shows that the optimal survival probability is and that the optimal strategy is a Markov feedback rule in the current surplus. It also yields that this solution is bounded, which Hipp and Plum (2000) had to assume, and closes the gap they left open on ruin by creeping (Remark (iii), p. 897). Numerical procedures for the optimal strategy (§5 of the paper) rest on this identification.
The theorem is proved in the paper; nothing in it is formalized. The mission produces a machine-checked verification theorem for a controlled jump-diffusion with an Itô integral against Brownian motion, a Poisson claim stream and a predictable control, together with a formal model of the Cramér–Lundberg process with investment and reinsurance that later results in risk theory can reuse.
The standard verification argument applies Itô's formula to and uses (1) to show that is a supermartingale, and a martingale under the feedback strategy. Here is not at (), is discontinuous at after the extension by , and is not assumed bounded, so the stochastic integral is only a local martingale and the passage needs both Lemma 1 and a separate argument that the feedback process does not creep through . Lemma 1 itself is only sketched in the paper ("We will just describe the argument"). The optimality part needs a surplus process following the feedback rule; its existence is not proved in the paper.
The model is formalized on a measurable space with a probability measure: i.i.d. exponential interarrival times (realising the Poisson process), i.i.d. claim sizes with law , and a real Brownian motion (IsBrownianReal), the three families mutually independent. Independence of from the claims is not printed in the paper but is used by (1) and its proof; it is a disclosed standing assumption. The filtration is , not completed. The Itô integral is the published relation EthierKurtz.HasBrownianItoIntegral, and its paths are required to be continuous, so that the pathwise ruin event is well defined. The surplus equation holds for every and every sample point.
Conventions: the premium is real valued (so , which the paper allows to fail when ); the supremum in (1) is stated as a least upper bound equal to , so an unbounded family never counts as a solution; is on and (1) is required for ; is a supremum over all admissible triples (strategy and surplus process); the controls of the feedback rule at non-positive pre-jump surplus are left free, and optimality is stated for . Expectations of are lower Lebesgue integrals of nonnegative functions, so no default value of a non-integrable expectation satisfies an inequality. The optimality clause is stated for every process following the feedback rule; it would be vacuous if no such process existed, and its existence is not part of the target.
Infrastructure needed: Itô's formula for a semimartingale with Brownian and compound-Poisson parts, the compensator of the compound Poisson random measure, localisation, and optional stopping. The model definitions, the HJB predicate and the comparison lemmas are reusable for other ruin-minimisation and dividend problems. Contributions to any milestone, and to general stochastic-calculus lemmas they need, are welcome.
Manufacturers in computer hardware, software and automobiles routinely pay channel rebates to their retailers: a payment per unit the retailer sells to end consumers, as opposed to per unit the retailer buys. A target rebate pays only for units sold beyond a target level, a linear rebate pays for every unit sold. 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, asks whether such payments can make an independent retailer act in the interest of the whole supply chain.
The question belongs to the supply-chain contracting literature built on the newsvendor model. A wholesale price above cost makes the retailer under-order relative to the integrated channel (double marginalization, Spengler 1950). Returns contracts (Pasternack 1985) and revenue sharing (Pasternack 1999; Cachon and Lariviere 2000, as cited by Taylor) are known remedies. Cachon's survey, Supply Chain Coordination with Contracts (Handbooks in OR & MS 11, 2003), discusses sales-rebate contracts through a first-order condition. Taylor's Theorem 1 is the global statement for the target rebate, with an explicit contract and an arbitrary profit split, and without any lump-sum side payment.
This mission covers §3 of the paper, the model without sales effort. Missions II–IV of the series cover §4, where the retailer's effort also affects demand.
A manufacturer sells to a retailer who places one order of size before observing demand . Demand has a density with for and for every (Assumption A4), and a finite mean. Write
The retail price , the production cost and the salvage value are fixed with and ; may be negative. A contract specifies a wholesale price , a rebate and a target (Assumption A1: , , , ). No other transfer is allowed (Assumption A3).
and the manufacturer earns .
The contract coordinates the channel when is the retailer's unique optimal order. Finally .
Fix . For every sufficiently small there is exactly one triple with , , and
and this triple has , , , coordinates the channel, and gives the retailer and the manufacturer .
Theorem 1 shows that a single sales-based instrument, a target rebate, achieves what a wholesale price alone cannot: the retailer orders the channel-optimal quantity, and the channel profit is split in any proportion . The parameter can be set to the retailer's opportunity cost, so a manufacturer with all the bargaining power extracts the rest of the channel profit without a side payment. Proposition 1 explains why the target is needed: a linear rebate that coordinates the channel leaves the manufacturer with a loss. The quantity-only analysis is also the base case of §4, where the paper shows that a target rebate combined with returns coordinates effort and quantity as well.
The results are proved in the paper (Appendix, p. 1005). No machine-checked proof of any of them is known to exist. The mission produces a Lean statement of the model and of each result, and invites formal proofs of the newsvendor solution, the shape of the kinked profit, the threshold lemma and the coordination theorem.
The retailer's profit is not concave: its derivative jumps up at the target. The usual newsvendor argument, a stationary point of a concave function is a global maximum, therefore fails. A first-order condition at shows only that is a local candidate on . The retailer may still prefer the smaller candidate on , and coordination fails exactly when she does. Theorem 1(b) requires comparing the two branches globally, through the threshold of Lemma 1, and then showing that the contract's target lies strictly below .
The contract itself is defined implicitly. solves an equation involving the critical fractile , and solves (1). Existence and uniqueness of both, and the placement of relative to , are part of the claim.
All definitions are in ChannelRebate.Quantity.Setting. Demand is a structure Demand carrying the density with the properties listed under Setting; its law is Lebesgue measure with density . and are expSales and expLeftover of the published definition CachonCoord_Newsvendor_Contracts, applied to this law. is the local rebateUnits. and are interval integrals from .
Conventions:
Demand; no continuity of is assumed.A formalization that reads coordination as the first-order condition at , or that defines or by a choice function, would make Theorem 1 vacuous or weaker, and is ruled out by the statements above.
A complete development needs the newsvendor calculus for a density (derivatives of and in , strict monotonicity of on ), the intermediate value theorem for the two implicit equations, and the global comparison of the two concave branches. The newsvendor calculus is reusable for missions II–IV of this series and for other newsvendor contracts. Proofs of the milestones in any order are welcome.
Two-stage stochastic programs are solved with an approximation of the true distribution of the random data: an empirical measure, a scenario tree, or a discretization. Whether the computed decisions mean anything depends on how the optimal value and the solution set react when the underlying probability measure is replaced by a nearby one, and on which distance between measures "nearby" refers to. Rachev and Römisch (preprint, edoc.hu-berlin.de; published in Math. Oper. Res. 27 (2002) 792–818, doi:10.1287/moor.27.4.792.304) organize this question in two steps. First, a minimal information distance , built from the integrands of the problem itself, controls optimal values and solution sets (their Theorems 2.2 and 2.3). Second, for a given class of models, is bounded by a canonical probability metric that depends only on the analytical properties of the integrands.
For linear two-stage programs the integrands are locally Lipschitz in the random parameter and the canonical metric is a Fortet–Mourier metric. When the second stage has integer variables, the recourse function is discontinuous, and metrics of Fortet–Mourier type no longer control the problem. This mission formalizes the paper's answer for that case (§3.2): mixed-integer two-stage programs are Hölder stable with respect to a polyhedral discrepancy built from Lipschitz functions restricted to polyhedra. The structure of mixed-integer value functions that makes this possible goes back to Blair and Jeroslow (1977), Bank et al. (1982) and Schultz (1996), all cited in the paper.
Let , let be closed and a polyhedron, i.e. an intersection of finitely many closed half-spaces. The second stage has costs , and - and -matrices , . Its value function is
and is the set of right-hand sides for which the constraint set is nonempty. The right-hand side and the technology matrix depend affinely on . For a Borel probability measure on the program is
Three conditions make (9) well defined: (B1) and have rational entries; (B2) for all (relatively complete recourse); (B3) there is with and (dual feasibility).
and denote the optimal value and solution set of (9) under ; for an open bounded , and are the same objects with replaced by . is a complete local minimizing (CLM) set if it is nonempty and contained in . The minimal information distance is . The moment classes are , and the polyhedral metric is
Finally, is the growth function at , , and .
Under (B1)–(B3), with for some , , and an open bounded neighbourhood of , there are , and such that for all with
and is a CLM set. The constants and the number of faces are existential; only the exponent is fixed.
For bounded and every the same conclusions hold with the Lipschitz rate , where over polyhedra with at most faces.
Theorem 3.6 says that, for mixed-integer recourse, closeness of the distributions in is enough for closeness of optimal values and of localized solution sets, with an explicit Hölder exponent that degrades with the second-stage dimension and improves with the number of moments. Two consequences follow. Scenario reduction and discretization methods for mixed-integer models can be judged by a polyhedral discrepancy; and, through the entropy estimates of §4 of the paper, empirical approximations converge at rates governed by uniform laws for polyhedra. Corollary 3.7 shows that for bounded supports the rate becomes Lipschitz in the polyhedral discrepancy.
The results are proved in the paper, partly by reference: Lemma 3.5 is quoted from Bank et al., Schultz, and Blair–Jeroslow, and the partition argument behind (12) refers to Schultz (1996). None of it has a machine-checked proof. Formalizing the mission produces the first formal treatment of mixed-integer value functions with rational data, a formal version of the minimal-information-distance stability theorems in the objective-only case, and the polyhedral metric itself.
The obvious route to a stability estimate, a Lipschitz bound on followed by a Fortet–Mourier or Wasserstein bound, fails at the first step: jumps across the boundaries of the pieces , so is only piecewise Lipschitz, with pieces that move with . Any metric that controls must therefore see the indicator functions of these pieces, which is why polyhedra enter. The second obstacle is that there are countably many unbounded pieces: a single polyhedral bound covers only a bounded region of , and the tail outside it must be paid for with moments, which is the origin of the exponent. Lemma 3.5 itself, in particular the uniform Lipschitz constant and the local finiteness of the partition, rests on rationality of and ; without (B1) the value function need not be lower semicontinuous.
, , are Euclidean spaces (the paper never fixes its norm, and every constant in the statements is existential). Measures are Borel probability measures on with . The integral of the extended-real integrand is the published DupacovaWets.Consistency.expect ( when ). , optimal values and are extended-real infima, on empty sets; the paper's "min" is read as an infimum. Distances and take values in , and every estimate between optimal values states explicitly that both are finite, so that no convention for can make a bound vacuous. is a linear map and its operator norm. Integer vectors are tuples of natural numbers; , are real matrices with rational entries.
Disclosed reading: a "polyhedron with at most faces" is an intersection of closed half-spaces. Because is existential in Theorem 3.6 and Corollary 3.7, the theorems are equivalent under this reading and under a facet count. The clause "piecewise polyhedral" of Lemma 3.5 is not defined in the paper and is not formalized. The page states ""; the argument proves and uses , and that direction is the one formalized. Theorems 2.2 and 2.3 are stated in their objective-only () form for a general normal integrand.
The integrals in are Bochner integrals over , which are meaningful because measures in with integrate . A formalization that took the supremum over all of instead of , quantified over all of , or let a non-integrable function contribute would not state the paper's theorem, and these readings are excluded.
Needed infrastructure: the structure theory of mixed-integer value functions with rational data (the partition of Lemma 3.5 and the attainment of the minimum in (10)), lower semicontinuity of integral functionals of normal integrands via Fatou's lemma, Berge's upper semicontinuity of parametric argmin maps, and approximation of polyhedral pieces by polyhedra. The value-function results and the general stability theorems are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3.5, are welcome.