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?
Robust linear optimization replaces an uncertain constraint by the requirement that hold for every in an uncertainty set (Ben-Tal and Nemirovski 1999). The method leaves open where should come from. Risk theory answers a related question from the other side: a decision maker's attitude to an uncertain reward is described by a risk measure , and the constraint is imposed as .
Bertsimas and Brown (2009) connect the two. When is coherent and is supported on finitely many observed data points , the risk constraint is exactly a robust constraint whose uncertainty set is built from the data and the family of probability vectors generating . For the class of distortion risk measures, the uncertainty set has an explicit polyhedral form, the -permutohull of the data, and the robust constraint has a reformulation of polynomial size. This mission formalizes that chain of results, Sections 2–4.3 of the paper.
The sample space is finite, , and a random variable is a vector , read as a reward; means for every . The probability simplex is , and .
A risk measure is a function with and . It is coherent if it is moreover convex and positively homogeneous. A set generates if for all . The conditional value-at-risk under a probability vector is for .
Two random variables are comonotone if for all ; is comonotonic if it is additive on comonotone pairs, and law invariant if it takes equal values on random variables with the same distribution. A distortion risk measure is a coherent, comonotonic, law-invariant risk measure. From Section 4.2 on, carries the uniform distribution .
The restricted simplex is . For put
where are the increasing order statistics of . The data are , the uncertain vector takes the value at , and the -permutohull of is
Under the uniform distribution, for every distortion risk measure there is with , and for this , all data and every ,
The vector depends on only; the data are quantified after it.
A companion item states Corollary 4.3: , and the class equality it yields: the uncertainty sets of all distortion risk measures are exactly the polytopes , , .
The goal theorem identifies the uncertainty set implied by any distortion risk measure: it is a permutohull of the data, a polytope with up to vertices that is nevertheless representable with extra variables and linear constraints. Combined with Theorem 4.2, the uncertainty sets of distortion measures are exactly the mixtures of the sets of -point averages of the data (Corollary 4.3), with as the generators. The later sections of the paper build on this: centrally symmetric permutohulls (Section 4.4) and the construction of a distortion risk measure from a given polyhedral uncertainty set (Section 4.5) are the subjects of the two companion missions.
The results are proved in the paper; no machine-checked version is known. The formalization adds checked statements of the finite-space representation theory of coherent and distortion risk measures, which the paper obtains partly by citing general results, and records the corrections the printed statements need.
The two equalities of the goal have unequal weight. The second is a statement about one polytope with up to vertices and a linear system of size ; it is finite-dimensional linear programming. The first requires the complete characterization of distortion risk measures on a finite uniform space, and that is where the obvious approach fails. The known representation of law-invariant comonotonic coherent measures as mixtures of CVaR (Kusuoka 2001) is proved for atomless spaces and does not transfer to a discrete . The uniform distribution is essential, not a convenience: Remark 4.2 of the paper gives a two-point space with probabilities and a monotone, normalized, submodular set function depending only on probability whose induced distortion is not concave, so the conclusion of Theorem 4.2 fails there.
Fin N with ; random variables are Fin N → ℝ; indices are 0-based throughout, so qhat j is the paper's and is Antitone q. Order statistics are X ∘ Tuple.sort X.stdSimplex ℝ (Fin N). Generation (1) is an IsLUB over an arbitrary set of probability vectors, not a maximum over a finite family (that version is false).A linear decision made with uncertain coefficients can be protected by requiring the constraint to hold for every coefficient vector in an uncertainty set. Choosing that set determines how conservative the decision is. Bertsimas and Brown connect this choice to a risk measure: a functional that assigns a cost to the random reward left by a decision. Their construction turns certain risk constraints into robust linear constraints over a convex hull of weighted samples. This mission isolates the structural question asked in §4.4 of their paper: which such risk measures always produce uncertainty sets that are centrally symmetric about the sample mean? The answer matters because this symmetric family is the class used in the paper's subsequent approximation of general polyhedral uncertainty sets. Bertsimas and Brown (2009), §§4.3–4.5.
There are observations, indexed by , with equal reference probabilities. A probability weight vector has nonnegative entries summing to one. The restricted simplex contains those vectors whose entries are nonincreasing: . For a reward vector , write for its increasing order statistics. The associated distortion risk measure is . A larger reward therefore reduces risk. Under the uniform distribution, the paper's Theorem 4.2 identifies these functionals, for , with its distortion risk measures. Bertsimas and Brown (2009), Theorem 4.2.
Take arbitrary sample vectors . For a permutation of their indices, form the weighted vector . The -permutohull is the convex hull of all these vectors. Its center of interest is the sample mean . A set is centrally symmetric through when implies for every . The quantifier “for any data” ranges over every dimension and every choice of sample vectors. It is stronger than symmetry for one selected data set. Bertsimas and Brown (2009), Definitions 4.7–4.8.
The first target is Proposition 4.1's characterization of weights giving universal symmetry. If is the vector with every entry , then
This condition defines the symmetric restricted simplex inside . Bertsimas and Brown (2009), Proposition 4.1 and Definition 4.9.
The main target is Theorem 4.4. Put . For , define a generator by
A functional represented by a whose permutohull is symmetric for every data set is exactly a convex mixture of the generator functionals:
The milestones also state the two set inclusions behind the equality of with the convex hull of these generators, including the coordinate reversal identity. Bertsimas and Brown (2009), Theorem 4.4 and its proof.
The result gives a finite list of risk functionals from which every member of the universally symmetric distortion subclass can be formed. The number of generators is , rather than an unspecified family. It also connects a geometric property of a robust uncertainty set to a checkable condition on its weights. The paper uses this symmetric subclass to formulate the inner approximation problem in §4.5, where a symmetric permutohull is fitted inside another polytope. Bertsimas and Brown (2009), §§4.4–4.5.
The mathematical result is proved in the 2009 paper. This formalization task is to obtain Lean proofs of the classification and its source-stated intermediate claims. The definition layer is a reusable interface for finite distortion risk measures, permutohulls, and symmetry under coordinate permutations. Formal proofs here would provide a checked foundation for later robust optimization statements using the same finite sample model. The proposed goal and milestones are open Lean statements; compiling them verifies their syntax and types, not their proofs.
Symmetry of one pictured polygon does not determine its weight vector. The hypothesis demands symmetry for every possible collection of sample vectors, so the converse in Proposition 4.1 must recover a relation among weights from a universal geometric property. Another difficulty is that the explicit generators change shape at the midpoint, and the odd and even cases have different middle ranges. The paper writes the calculation for odd and says the even case is analogous; the theorem itself makes no parity restriction. A proof therefore has to cover the even boundary, including the generator whose band is empty. Bertsimas and Brown (2009), Proposition 4.1 and proof of Theorem 4.4.
The Lean sample space is Fin N, with . Its indices start at zero; the prose and source formulas above start at one. The source's is N / 2 + 1 in natural numbers. Probability vectors use Mathlib's standard simplex together with antitone coordinate order. Permutohulls use convexHull of the finite permutation family, and order statistics use Tuple.sort. The reference distribution is uniform, as in the paper's Assumption 4.1. Real vector spaces of dimension zero are allowed because the claim quantifies over every dimension; the nonempty sample condition excludes division by zero.
The goal takes an arbitrary functional and requires an actual representation by a restricted-simplex weight. This is the paper's Theorem 4.2 parametrization of distortion risk measures, stated directly because that theorem is being drafted in a separate mission of the same series. Universal symmetry is derived from the data quantifier; it is not assumed as a condition on . The generator mixture is likewise the conclusion, with its coefficients nonnegative and summing to one. Central symmetry includes membership of the center in the set.
Useful contributions include proofs of the source's permutation characterization, validity and symmetry of generator mixtures, and their converse spanning property. The definitions of finite probability weights and weighted permutation hulls can support further finite sample robust optimization results. The paper's inconsistent accent on the generator risk measure in Theorem 4.4 is read as the functional of the displayed generator vector; its intermediate sum on p. 1492 does not alter the stated normalized mixture.
A firm holds a fixed stock of a perishable or seasonal product: airline seats, hotel rooms, fashion goods, tickets. It must sell the stock over a finite season, and whatever is left at the end is worth nothing. The firm can change its price at any time, and demand responds to the price at random. Should it adjust its price continually as sales occur and time runs out, or is one well-chosen price nearly as good?
Gallego and van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons (Management Science 40(8), 1994, doi:10.1287/mnsc.40.8.999), set up this question as a continuous-time stochastic control problem and answered it. The source for this mission is the published 1994 article. Its answer is quantitative: the expected revenue of a single fixed price is within a factor of the best possible dynamic policy. The paper is one of the founding results of dynamic pricing in revenue management. The deterministic (fluid) upper bound it introduced became the standard benchmark of the field, and later work on re-solving heuristics, network revenue management and learning-while-pricing builds on it.
Demand. The firm chooses a demand intensity from an interval of allowable rates, and the market charges the inverse-demand price . On nonzero rates, is strictly decreasing and nonnegative; rate corresponds to the null price , at which nothing sells. The revenue rate is . It has , and it is continuous, concave and bounded on . denotes its least maximizer, and , . Such data form a regular demand function (§2.1).
The stochastic problem. At time the firm holds items and has a horizon . A non-anticipating pricing policy chooses the intensity at each elapsed time as a function of the sales history so far. Sales follow a Poisson process with this controlled intensity, and at most items can be sold. A sale at time earns the current price . The expected revenue is , where counts the sales, and the optimal expected revenue is .
The deterministic problem. Replacing random sales by their rates gives
It is solved by the constant rate (Proposition 2).
Fixed-price heuristics. is the expected revenue of charging for the whole horizon. is the expected revenue of the best constant price.
For , and , is finite and positive, and
The result. Theorem 2 says that uncertainty can only cost revenue. The deterministic value is a computable upper bound for every policy, so any heuristic can be judged against it. Theorem 3 turns this into a guarantee: with 400 items and scarce stock, a single price earns at least 97.5% of the optimum. The loss vanishes as the expected sales volume grows. This is the justification for the stable, rarely changed prices seen in practice, and the template for the asymptotic-optimality analyses that followed: fluid bounds, re-solving, bid prices.
Formalizing it. The results are proved on paper, and none is formalized. The platform has a discrete-time Bernoulli analogue of Theorem 2 (Talluri–van Ryzin, RevenueManagement.deterministic_upper_bound) and Bitran–Caldentey's periodic-review version as open items. Neither is this continuous-time model. A formalization would add a controlled Poisson sales process with a policy-dependent intensity, the compensator identities (13)–(14) for it, and a Lagrangian-duality argument over measurable rate paths. These are reusable for every continuous-time revenue-management model on the platform. Gallego's moment bound (18) is already proved there.
The deterministic side (Proposition 2, the duality gap) is convex analysis on one concave function. The fixed-price bounds reduce to a Poisson computation and (18). The obstacle is Theorem 2's stochastic step. The revenue is collected at random jump times chosen by an adaptive policy, and comparing it with a deterministic integral requires the compensator identity for an arbitrary non-anticipating intensity. The paper cites Brémaud's martingale theory for this, which Mathlib does not have. A first idea is to apply Jensen's inequality to directly. It fails because the stock constraint holds only pathwise, through , and not in expectation for a rate path. Restricting to Markovian policies does not remove the need for the identity.
RevenueManagement.*).PricingRM.DetHeuristic.*).Multiechelon inventory theory studies supply systems in which stock is held at several levels: here, a depot that orders from an outside supplier and a retail outlet that is replenished from the depot and faces random customer demand. The question is how much to order and ship in each period so as to minimize expected holding, shortage and ordering costs over an infinite horizon. Clark and Scarf (Management Science, 1960) showed that the finite-horizon problem of a serial system decomposes into single-location problems linked by an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) extended the decomposition to the infinite horizon under discounted and average costs, and then asked what it costs to compute an optimal policy.
In the reduced single-location problem the only nonlinear part of the one-period cost is the expected induced penalty . Any algorithm for the reduced problem (Veinott–Wagner type policy computations, for instance) evaluates many times. In general each evaluation is a numerical integral. Section 4 of the paper shows that when demand is normal, has a closed form in the univariate and bivariate standard normal distribution functions. This mission formalizes that closed form, eq. (13) on p. 830.
Time is discrete. One-period demand is with , independent across periods. For , is the total demand over periods. It is normal with mean and standard deviation , density and cdf . The shipment lead time from depot to outlet is and the order lead time from the supplier is . The cost factors are a system-wide holding cost , a retailer holding cost and a retailer shortage penalty . Write . Costs are average costs, so the discount factor is throughout.
The retailer's one-period cost (p. 822) is
The critical number is a global minimizer of (property (b), p. 824). The induced penalty cost is for and for . Its expectation over the order lead time is
Let and be the standard normal cdf and density, , and the cdf of a bivariate normal pair with standard normal marginals and correlation . The paper defines (p. 830)
with .
For every real ,
This is an exact identity for every admissible parameter value. It holds with no constants left free.
The milestones follow the paper's outline of the derivation on pp. 829–831:
Two side remarks of p. 830 are also included: , and the simplified form of .
The result. Under normal demand, (13) replaces the numerical integral (12) with a few evaluations of , and the bivariate normal cdf, all available in standard numerical libraries. Together with the decomposition results of Sections 1–3 of the paper, it makes the policy computation for the two-echelon system with normal demand no harder than a single-location computation with an explicit cost function. The same functions reappear in the paper's Section 5 for several retail outlets, after a reinterpretation of .
Formalizing it. The paper proves (13) only in outline: it calls the derivation "an elementary integration problem, but … sufficiently involved to warrant an outline" and leaves "tedious algebra" and "more algebra" to the reader. A machine-checked proof turns that outline into a complete argument, including the analytic steps the outline passes over: differentiation under the integral sign, the limits at , and the identification of an integral of normal densities with a bivariate normal probability. To our knowledge no formal proof of (13) exists, and no bivariate normal distribution function is on the platform yet.
The obvious approach is to substitute (11) into (12) and integrate. The result is a double integral of normal densities over a region bounded by a line, and it does not reduce to univariate functions. The paper's route is to differentiate first, identify the derivative (14) as a probability for the correlated pair , and then recover by integrating from . That route needs three things: justification for differentiating under the integral in (12), whose integrand has a kink at ; control of the limits at ; and the conditional-normal identities, which involve conditioning on a null event and so must be handled through densities. The verification of is a long computation with , and , in which every constant matters.
Everything lives in the namespace FZEchelon.NormalDemand. The model data form the structure Data (fields ). The law of is the platform's normal demand law InventoryControl.newsboyDemand with mean and standard deviation . Expectations are Bochner integrals, and improper integrals are set integrals over Set.Ioi/Set.Iic. is cdf (gaussianReal 0 1). The bivariate cdf is the iterated integral of the explicit bivariate density over a lower-left quadrant (meaningful for ; here ). Derivatives are HasDerivAt and limits are Tendsto … atTop (𝓝 0).
Standing hypotheses of every theorem: ; (p. 821); ; and minimizes . Two of these are added to the page and disclosed. is needed because every divides by some . is needed because , and the paper treats zero order lead time separately (p. 819). Demand is exactly normal, as in §4, which acknowledges that this violates and ignores the objection. No nonnegativity, truncation or approximation enters. The goal fixes , the average-cost case the section restricts to. The discounted analogue is not part of this mission.
A trivializing formalization is ruled out: every Bochner integral in the statements has an integrable integrand, since integrands grow at most linearly and the normal law has all moments. No division by a zero standard deviation can occur under the hypotheses. A sorry-free check in the workspace shows that all hypotheses hold together, with a minimizer of proved to exist.
Needed infrastructure: properties of gaussianReal (moments, convolution of independent normals), differentiation of parametric integrals, and a bivariate normal distribution function with its partial derivatives. A reusable treatment of the bivariate normal cdf, linking the density form used here to Mathlib's multivariateGaussian, would be a contribution of independent value. Proofs of individual milestones are welcome in any order.
A learning algorithm that picks a function from a class by minimizing an empirical average is only as good as the gap between the empirical average and the true mean , uniformly over the functions it might choose. The classical way to control this gap uses a global complexity of the whole class, such as its Rademacher average, and yields rates of order . These rates are too slow in many problems of statistics and learning theory, where the functions that matter (those close to the best one) have small variance. Bartlett, Bousquet and Mendelson (arXiv:math/0508275, Annals of Statistics 33 (2005) 1497–1537) showed that the gap can instead be controlled by a local complexity, the Rademacher average of the small-variance part of the class. The resulting bounds give fast rates, often of order , and the paper is the standard reference for this method in empirical process theory and statistical learning.
The method builds on Koltchinskii and Panchenko (2000), Massart (2000) and Lugosi and Wegkamp (2004), and its concentration step uses Bousquet's form of Talagrand's inequality (2002). It is the basis of the fast-rate analyses in Koltchinskii's 2006 Annals of Statistics paper on local Rademacher complexities and oracle inequalities, and in later work on variance-regularized risk minimization.
Let be a probability space and independent random variables with law . For a function write
Let be independent signs, . For a class of functions, the empirical Rademacher average is
the expectation over the signs with the sample fixed, and the Rademacher average is its expectation over the sample.
The star-hull of around is . A functional assigns a number to each function; it plays the role of a variance proxy (for instance or ).
A function is sub-root if it is nondecreasing and is nonincreasing on . A nontrivial sub-root function has a unique positive fixed point , the solution of (Lemma 3.2 of the paper).
Let be a class of functions with values in , , and a functional with , and for , . Let be sub-root with fixed point and assume, for every ,
Then for every and , with probability at least ,
and, with probability at least ,
The theorem replaces the global complexity that a direct application of Talagrand's inequality would give by the fixed point , which is never larger and is often much smaller. For a class with a Bernstein-type variance condition (, as for excess losses of empirical risk minimizers), is of order for VC-type classes and of order of the eigenvalue tail for kernel classes, which yields the fast rates of the paper's Sections 4–6. The second part, formalized here, gives better constants than the first by working with the star-hull of the class, and it is the version the paper's later results (Theorem 4.1 and its corollaries) are built on.
On the formal side, nothing of local Rademacher theory is in Mathlib or, beyond the definitions reused here, on the platform. The concentration inequality used in the proof (Theorem 2.1, from Bousquet's form of Talagrand's inequality) is posed but unproved on the platform. A complete formalization would make the fixed-point machinery available to every fast-rate result built on it. The paper's printed constants for this statement are wrong (see below), so a machine-checked version also settles which constants the argument supports.
The obvious approach applies a concentration inequality directly to and bounds the complexity term by a single Rademacher average; this loses the variance information and gives only rates. The localized argument needs a level that is simultaneously above the fixed point and large enough that the deviation of the rescaled class is at most . Converting a bound on the rescaled class back into a bound on requires the multiplicative structure of . The probabilistic core is Talagrand's concentration inequality for suprema of empirical processes with Bousquet's constants, whose proof (entropy method) is the main piece of missing infrastructure. Measurability of the suprema involved is a separate technical obstacle.
X → ℝ on a measurable space with a probability measure P; the sample is s : Fin n → X under the product measure, with n ≥ 1. is empMean s f, is empRademacher (the average over all sign vectors of a real supremum, without absolute value), is expRademacher, and IsSubRoot is Definition 3.1; these are reused published definitions.empRademacher; elementary sub-root calculus. The sub-root lemmas and the containment step are reusable by any later mission on local Rademacher complexities.Dynamic programming often replaces a search over whole plans with an equation for a value function. That replacement is useful only when solving the equation recovers the value actually available through policies. In his 1967 paper, Eric Denardo isolated conditions on an abstract return function that make this identification possible, without committing to a particular transition law or a finite state space. The framework covers discounted decision models and other examples discussed in the paper, while allowing different decisions at different states. Denardo, 1967.
The mission concerns the paper's first regime: a one-step contraction together with monotonicity. It focuses on the question raised just after equation (4): does the solution of the functional equation equal the supremum of the return functions generated by policies? The paper proves that it does under these assumptions. Its later -stage regime is a separate mission. Denardo, 1967, pp. 167–169.
Let be a set of states. At each there is a decision set . A policy selects a decision at every state, so the policy space is the full Cartesian product . Let be the bounded real functions on , with the uniform metric . A return function assigns a real return to a state, an available decision, and a continuation value . Denardo, 1967, p. 166.
For a policy , its policy operator acts by . Under the contraction assumption, some satisfies and for all eligible . Each then has a unique fixed point , called that policy's return function. The optimal return function is defined pointwise by . These are the paper's definitions, rather than a presumed equality between and a Bellman fixed point. Denardo, 1967, pp. 166–167.
The maximization operator instead chooses the best decision at each state for a supplied continuation value: . Denardo assumes that and remain bounded, so both operators act on . The monotonicity assumption says that pointwise implies for every policy. These are separate conditions: contraction controls distance between value functions, while monotonicity controls their order. Denardo, 1967, pp. 166–168.
The central target is Theorem 3. Under contraction and monotonicity, the unique bounded solution of equation (4) is the optimal return:
The milestones follow the paper's route to that assertion. Theorem 1 bounds a policy's return by its fixed-point residual, . Theorem 2 says that itself has modulus at most . The text accompanying equation (4) establishes that has exactly one fixed point. Corollary 1 then gives, for each , a policy with residual at most at that fixed point and return within of it, together with an exact equality criterion for zero residual. Denardo, 1967, pp. 167–168.
Theorem 3 justifies reading the functional equation as an optimization equation: its solution is the pointwise supremum of returns realized by the paper's policy model. Corollary 1 supplies policy returns arbitrarily close to that solution in the uniform metric. With the compactness and continuity assumptions of Corollary 2, the paper also obtains a policy that attains it, though that optional result is outside this mission's milestone list. Denardo, 1967, pp. 167–168.
The mathematical result was proved in the cited paper. This mission asks for machine-checked proofs of its abstract statements in Lean, including the residual estimate, the maximization operator's contraction, fixed-point existence, and the identification with optimal policy return. The definitions are reusable for decision models whose returns fit Denardo's assumptions; they do not prescribe a probability kernel or a finite action set.
The fixed-point theorem alone identifies a unique solution of ; it does not identify that solution with , because is defined through the separate fixed points of all . The distinction matters: the paper observes that contraction without monotonicity can leave different from , and gives as a nonmonotone example. The formal goal therefore retains both definitions and requires monotonicity. Denardo, 1967, pp. 167–168.
There is also a choice issue in Corollary 1. A near-maximizing decision is available separately at every state, while its conclusion asks for one policy choosing all those decisions at once. The full Cartesian policy space is essential to the statement. On an infinite state set, the value functions must remain bounded even after applying or a policy operator; contraction of differences by itself does not provide that range condition. Denardo, 1967, pp. 166–168.
Lean represents by bounded real functions lp (fun _ : Ω => ℝ) ⊤; its metric is . The state type may be infinite or empty, and decision sets depend on the state. Policies are precisely dependent functions . The operators and are maps into supplied with equations fixing their values from . This expresses the bounded-range assumptions on pages 166–167. Pointwise order is explicit because the bounded-function type has no order instance. Denardo, 1967, pp. 166–168.
Every supremum in the mission is a genuine real least upper bound. IsMaxOperator requires it for the decision returns at each state; IsOptimalReturn requires it for the policy returns. These predicates avoid assigning a default value to an empty or unbounded supremum. Where states exist, IsMaxOperator also entails a nonempty decision set. The family is supplied with ; contraction ensures each such return exists uniquely. Equation (4) and the main goal explicitly assert existence of the fixed point of , so the goal cannot hold merely because there is no solution to identify. Defining from the fixed point of , or defining from the policy supremum, would erase the paper's substantive claim and is excluded.
The definition layer needs bounded functions, uniform distance, real least upper bounds, and dependent policies. The theorem layer needs fixed-point and order reasoning on these objects. Contributions toward those general operator facts and the paper's four milestone statements are within scope.
Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They are among the most widely used methods in reinforcement learning, from REINFORCE (Williams 1992) and the policy gradient theorem to natural policy gradient and trust-region methods. The objective is not concave in the policy, even when the policy is a raw table of action probabilities, so standard optimization theory guarantees at best convergence to a stationary point, and it was long unclear whether or how fast these methods find an optimal policy.
Agarwal, Kakade, Lee and Mahajan (JMLR 2021) give a systematic answer for the tabular and function-approximation settings. This mission formalizes their warm-up result, Theorem 4.1: projected gradient ascent over the simplex of stochastic policies reaches an -optimal policy after a number of iterations polynomial in the sizes of the MDP, the effective horizon , , and a distribution mismatch coefficient. The gradient domination idea it rests on goes back to the analysis of conservative policy iteration by Kakade and Langford (2002) and to Scherrer and Geist (2014).
A finite discounted MDP consists of finite sets of states and of actions, a transition kernel , rewards and a discount factor . A policy assigns to each state a probability distribution over actions. Its value from a start state is
and for a start distribution , . The action value is and the advantage is . The discounted state visitation distribution is . An optimal policy maximizes at every state simultaneously; .
In the direct parameterization the parameter is the table itself, , a point of the product simplex . The algorithm optimizes for a chosen start distribution by projected gradient ascent
where is the Euclidean projection and . Performance is measured under a possibly different distribution , and the distribution mismatch coefficient (componentwise ratio) measures how well covers the states an optimal policy visits from .
With step size , from any initial policy, for every and ,
The theorem shows that, for the simplest constrained parameterization, a first-order method finds a globally optimal policy at a polynomial rate in spite of non-concavity. The guarantee holds for every performance distribution at once, and it isolates the role of exploration in a single quantity, the mismatch coefficient; Section 4.3 of the paper shows that without a well-covering gradient methods can need exponentially many steps. Lemma 4.1 and the smoothness bound are reused across the rest of the paper, and the performance difference lemma underlies essentially all of its analyses.
All results here are proved in the paper, with Theorem E.1 and Theorem E.2 cited from Beck (2017) and Ghadimi–Lan (2016). None of them has a machine-checked proof on the platform. A formal development provides a verified link between the policy gradient expression of the direct parameterization and a standard nonconvex projected-gradient rate, and a reusable formal library of discounted visitation distributions, the performance difference identity, and projected gradient methods on Euclidean spaces.
The obvious argument, "projected gradient ascent converges to a stationary point, and stationary points are optimal", fails on both counts as stated. Stationary points of need not be optimal when does not cover the relevant states; the quantitative replacement is gradient domination, which only controls suboptimality through the mismatch coefficient. The convergence rate itself requires smoothness of the value as a function of the policy table, which is a bound on second derivatives of a matrix inverse with the dependence and the factor made explicit. Finally, the near-stationarity delivered by the gradient-mapping rate is at the next iterate, not the current one, which is why the conclusion is over . On the Lean side, the value is an infinite series in the policy entries, so its differentiability and the exact gradient formula have to be established for a function defined on the whole parameter space.
Policies are parameter vectors in EuclideanSpace ℝ (S × A), so norms are and Mathlib's gradient is ; the objective is defined on the whole space and is only ever evaluated, with its gradient, at policies. The MDP layer (transition kernels, policies, , , occupation distributions, optimal policies) is the published FoundationsML.ReinforcementLearning library; is the unnormalized discounted sum. The projection is any map satisfying the nearest-point property. The optimal policy is a hypothesis IsOptimalPolicy (optimal from every state), not a supremum over all functions.
Conventions committed to:
A formalization that defines the update through formula (7), that assumes gradient domination or smoothness as hypotheses of the goal, or that takes the gradient off the simplex where the value series may diverge, would trivialize the goal; the goal mentions none of these, and (7) is a milestone theorem.
A complete development needs: summability and differentiability of the value series near the simplex; the performance difference lemma; the Euclidean projection inequality on a closed convex set; the descent lemma for functions smooth on a convex set; and the gradient-mapping argument. The projection and gradient-mapping results are independent of reinforcement learning and reusable. Contributions to any milestone are welcome, as are proofs of Theorem E.2 (Ghadimi–Lan) as a stepping stone to Proposition B.1.
A seller who does not know how demand responds to price has to learn the demand curve from its own sales while it is selling. The most natural policy is certainty equivalent pricing (also called myopic pricing or passive learning): after every period, estimate the unknown demand parameters from all data collected so far, and charge the price that would be optimal if the estimates were the truth. It is simple, uses all data, and is what a price manager would do without further thought.
den Boer and Zwart (Management Science 60(3):770–783, 2014) show that this policy can fail. In the linear-demand, Gaussian-noise model, the prices it produces fail to converge to the optimal price with positive probability: the policy is not strongly consistent. The result motivates the paper's main contribution, controlled variance pricing, which adds just enough price dispersion to keep learning (treated in the companion mission of this series).
The phenomenon has a history in adaptive control:
A monopolist sells one product in periods at prices from an interval with . The demand in period is
where are independent random variables. The parameters are unknown to the seller and satisfy , , , . The expected revenue at price is , maximized at the optimal price
Certainty equivalent pricing charges two different initial prices in . After periods it computes the least squares estimates , the solution of the normal equations , and charges
with when the estimated slope is nonnegative.
The goal states only the failure of convergence, for every admissible parameter and every pair of different initial prices; it does not fix where the prices go.
This is what the paper's argument establishes; since it implies the goal.
The milestones are the displayed steps of the appendix proof, in attack order: the determinant of the coefficient matrix of the linear system (12); the bound for ; positivity of the probability of an explicit event on the noise for large ; the case (the first fitted line pushes to ); the representation of the least squares error; recursive and closed forms of and ; and the deterministic induction that every noise path in keeps the price at forever.
The result is the standard counterexample to certainty equivalence in dynamic pricing. It shows that estimation and optimization cannot be separated naively: a policy that always exploits its current estimate can lock itself into a price at which the data no longer move the estimate enough to correct it. Every later policy in this literature that forces exploration (controlled variance pricing, semi-myopic policies, constrained iterated least squares) is designed against this failure, and its necessity is argued by pointing to results of this kind.
The result is proved in the paper; nothing here is open. To our knowledge it has no machine-checked proof. Formalizing it adds:
The obvious heuristic, "with positive probability the first two observations are so noisy that the fitted slope is wrong", is not enough: one bad estimate is corrected by later data unless the policy stops generating informative data. The proof has to control the whole infinite future. It does so by showing that on a single event, defined through the first two noise values and a uniform bound on all later running means, the price stays at forever, which requires the closed form of the least squares estimate along a price path that is constant from period 3 on. That event involves infinitely many noise variables, so its probability is positive only through a maximal inequality, and independence between and the later noise. A second subtlety is the choice of constants: the size of the band enters the conditions on , so the order in which and the set of admissible are chosen matters (the printed proof picks them in a circular order; a non-circular choice exists).
CVPricing.CertEquiv.Model bundles with the standing assumptions of §2 as fields, including (the paper's neighbourhood assumption specialized to linear demand). The noise is the referenced published definition RobustBooking.Shared.GaussianNoise (measurable, mutually independent, each ); its Lean index is period , so the paper's is ε (i - 1).cePrice is a deterministic recursion on a noise path, so the random price process is obtained by evaluating it at . Periods are 1-based. The least squares estimate is the referenced KeskinZeevi.SufficientConditions.lsEstimateOf, the solution of the normal equations (4), unique whenever . The certainty equivalent rule is the projection of onto when , and when ; the latter is the convention the paper's proof adopts for wrong-signed estimates.Regularized least squares is the standard tool of high-dimensional linear regression. The square-root LASSO of Belloni, Chernozhukov and Wang (Biometrika, 2011) minimizes . Unlike the LASSO, its optimal regularization parameter does not depend on the unknown noise level. Regularization is usually justified through sparsity or bias–variance arguments. Blanchet, Kang and Murthy (arXiv:1610.05627, J. Appl. Probab. 56(3), 2019) give a different justification. The square-root LASSO, and every -penalized square-root least-squares estimator, is exactly a distributionally robust estimator. It minimizes the worst-case expected square loss over all data distributions within a given optimal-transport distance of the empirical distribution.
The rest of the paper builds on this representation: the radius of the transport ball is the regularization parameter, which the paper's Robust Wasserstein Profile function selects by a statistical criterion (mission 3 of this series). The duality theorem underneath, Proposition 1, is due to Blanchet and Murthy (Math. Oper. Res., 2019). Closely related representations for logistic regression appear in Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NeurIPS 2015), where they are approximate. The cost function introduced in this paper makes them exact.
The training data are pairs with predictors and responses . No distributional assumption is made; the data are fixed vectors. The empirical distribution is . For the square loss is and the mean square error is .
A cost function assigns to two points of a value , the cost of moving a unit of mass from to . The optimal transport cost between probability measures and is
The worst-case expected loss at radius is , and the distributionally robust regression problem (8) minimizes it over .
Two costs are used. With :
The exponent is the dual of , , and .
For the cost , every and every ,
and consequently
The second identity is the printed theorem; the first is what its proof establishes for each . The goal states both.
The result. Theorem 1 identifies -penalized square-root least squares with a min–max problem over data distributions. For , the minimizers are those of the square-root LASSO with . The regularization parameter therefore acquires a meaning: it is the square root of the transport budget an adversary may spend perturbing the predictors. This is the basis of the paper's choice of by the Robust Wasserstein Profile function (§4), and of the interpretation of regularized estimators as robust to covariate perturbations. Proposition 2 shows that letting the adversary also move the responses changes the penalty to , which is why the label-preserving cost is needed for an exact match.
Formalizing it. All results are proved on paper; none is formalized. A complete development gives a machine-checked strong-duality theorem for optimal-transport balls with possibly infinite costs (Proposition 1), two explicit worst-case computations, and corrected boundary cases of the closed forms (28) and the outline display, which print for all although the value can be finite at equality. The corrections do not affect the theorems.
The obvious argument fails in two places. The first is the duality step: the supremum ranges over all Borel probability measures on within transport cost , an infinite-dimensional set that is not compact in any convenient topology, with a loss that is unbounded above. Exchanging the supremum with the Lagrange multiplier of the budget constraint is Proposition 1, a theorem in its own right (Blanchet–Murthy), and its attainment claim needs .
The second is the cost , which is off , so the standard Wasserstein duality theorems, which assume a finite metric cost, do not apply. The degenerate cases , , , where the objective in does not blow up at both ends, must be covered separately.
(Fin d → ℝ) × ℝ with the product σ-algebra and topology. Proposition 2's cost uses the stacked vector in Fin (d+1) → ℝ (response last, built with Fin.snoc), and is the stacked vector of .PiLp, with exponents in ℝ≥0∞, so (the square-root LASSO case) is included. The exponents are linked by p.HolderConjugate q, and throughout. Theorem 1 does not print a range for ; the range is taken from Proposition 2, which the paper calls essentially the same result.ℝ≥0∞-valued, and is an infimum over probability couplings with both marginals fixed. Expectations of the nonnegative losses are lower Lebesgue integrals, and the worst case is a supremum in ℝ≥0∞ over all probability measures in the ball. No integrability side condition removes measures from the ball. Identities with a real right-hand side are stated after embedding it with ENNReal.ofReal.WassersteinDRO.Regularization.empiricalDistribution, applied to , with .A formalization in which the transport infimum did not fix both marginals, allowed sub-probability couplings, or used a Bochner integral would make the worst case trivially or . The conventions above rule this out: at the ball is and both sides of the goal equal .
The work needs Kantorovich-type duality for lower semicontinuous costs on (absent from Mathlib), Hölder's inequality with its equality case for PiLp, and elementary one-variable optimization. The duality theorem and the transport-cost definition are reusable beyond this mission: mission 2 of this series (classification) uses Proposition 1 with the cost , . Contributions that prove Proposition 1, or its weak-duality half, are particularly welcome.
Robust optimization protects a decision against every realization of uncertain data in a prescribed uncertainty set. The standard approach replaces the uncertain constraints by a deterministic robust counterpart and solves that counterpart directly (Ben-Tal, El Ghaoui, Nemirovski, Robust Optimization, 2009). The counterpart is often a harder problem than the original: a robust linear program with ellipsoidal uncertainty becomes a second-order cone program, and a robust quadratic program can become a semidefinite program. A practitioner who has an efficient, specialised solver for the nominal problem may therefore have no efficient solver for its robust version.
Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) ask whether the robust problem can be solved by repeatedly calling a solver of the nominal problem, with the number of calls independent of the dimension. Their first answer, the dual-subgradient meta-algorithm of §3.1, does so whenever the constraints are concave in the noise and the uncertainty set is convex. It is a primal–dual scheme: an online-learning algorithm picks the noise, and the nominal solver answers. This mission formalizes that result, Theorem 3.
Let be a convex domain, a convex uncertainty set, and constraint functions. The robust feasibility problem (3) is
(An objective is handled by binary search on its value, so feasibility is the core question.) A point is an -approximate solution if for all and all .
An -approximate oracle (Figure 1) takes a noise vector and either returns some with for all , or answers "infeasible", which it may do only if no has for all .
The standing assumptions of §3.1 are: each is convex on ; each is concave on for ; for all ; and for , . Write for the Euclidean projection onto .
Algorithm 1 sets and , starts from , and for updates
stopping with "infeasible" as soon as the oracle says so, and otherwise returning . In Lean these are alg1T, alg1Eta, alg1U, alg1X, alg1Output and alg1Calls in the namespace OracleRO.DualSubgrad.
For every -approximate oracle,
and the number of oracle calls is at most .
The result. Theorem 3 turns any approximate solver of the nominal problem into an approximate solver of its robust counterpart, at a cost of solver calls, a number that depends on the geometry of and the sensitivity of the constraints to the noise but not on , or . It is the prototype of the paper's oracle-based reductions: the same primal–dual template, with a different online learner, gives the dual-perturbation algorithm of §3.2–3.3 for non-convex uncertainty sets, and the applications of §4 (robust linear programs, quadratic programs, semidefinite programs) instantiate it.
Formalizing it. The theorem is proved in the paper; none of it is machine-checked. A formal development adds a checked statement of the reduction with an explicit call count in place of the paper's , and a reusable regret bound for projected online gradient ascent on concave rewards (Lemma 1), which the paper quotes from Zinkevich without proof and which many other online-learning results rest on.
The obvious argument for the dual side fails at one point: in round the primal point is computed from , so the reward that the dual player faces depends on its own current move. A regret bound that assumed rewards fixed in advance, or drawn independently of the learner's play, would not apply. Lemma 1 must be used in its adversarial form, valid for every sequence of reward functions, including adaptively chosen ones. A second point is that the projection step requires the variational characterization of a nearest point in a convex set, which a mere "map into " does not provide.
Points are elements of EuclideanSpace ℝ (Fin k), so every norm is the norm. The projection is a predicate IsProjOnto U P (each is a nearest point of to ), not a construction; the oracle is a function (Fin m → E d) → Option (E n) with none for "infeasible", constrained by the predicate IsApproxOracle on inputs in . The goal is quantified over every oracle meeting that specification. The gradient is a given map gradU with HasGradientAt at points of ; no differentiability in is assumed. Rounds are indexed by natural numbers with index for the initialization; the starting primal point , used by the first update and left undefined by the algorithm, is an input. Hypotheses and are added so that and are meaningful. Maxima over are stated as "for every ".
Explicit instantiations and corrections:
Trivializing formalizations are ruled out: an oracle specification under which "infeasible" is never returned, or an output that is not the average of the oracle's answers, would not be Theorem 3. The "infeasible" conclusion is about the robust problem, not the nominal one.
A complete development needs the variational inequality for nearest points in a convex set, the gradient (supergradient) inequality for a concave function differentiable at a point of a convex set, Zinkevich's telescoping argument, and Jensen's inequality for finite averages. The first two and Lemma 1 are reusable beyond this mission. Proofs of the milestones, in any order, are welcome.
Data-dependent risk bounds in statistical learning replace combinatorial quantities such as the VC dimension with averages of how well a function class can fit random noise on the observed sample. Bartlett and Mendelson's article (JMLR 3, 2002) established these averages, the Rademacher and Gaussian complexities, as a general tool: a risk bound (their Theorem 8) holds with a complexity penalty, and the complexity of a complicated class can be bounded through structural results that relate it to the complexities of simpler classes.
This mission formalizes two of those structural results, both stated for Gaussian complexities. The first (Theorem 14) controls a Lipschitz function of several real-valued classes at once, the vector-valued analogue of the classical contraction principle. The second (Theorem 16) controls an arbitrary fixed boolean combination of classes of classifiers, such as intersections, unions or majority votes of a fixed number of base classifiers, by the sum of the complexities of the components. Such combinations arise whenever a classifier is assembled from simpler ones, for instance in decision lists, small decision trees over a base class, or voting schemes.
Let be a set, a probability measure on it, and a sample size. For a class of functions and a sample , the empirical Gaussian complexity is
with independent standard Gaussian variables, and the Gaussian complexity is for i.i.d. with law (Definition 2, p. 464). In Lean these are empiricalGaussian n F x and gaussianComplexity μ n F.
Three constructions of classes appear.
SubsetDirectSum F Fi).compClass φ F).boolComb g F).A centred Gaussian process indexed by a finite set is a family of real random variables whose finite-dimensional laws are jointly Gaussian with mean zero; .
For a fixed boolean function with and classes of -valued functions,
Theorem 16 turns any bound on the Gaussian complexity of base classes into a bound for a fixed boolean combination of them, at the cost of a factor on the sum of their complexities, whatever and are. Together with the comparison between Gaussian and Rademacher complexities (Lemma 4 of the paper) and the risk bound of Theorem 8, it yields generalization bounds for classifiers built as combinations of base classifiers. Theorem 14 is the general tool: it handles any Lipschitz loss of a vector-valued predictor, such as multiclass margins, through the complexities of its coordinate classes.
All three results are proved in the paper (Lemma 13 is classical and cited from Pisier). None of them is formalized on Prove2Me; the finite-dimensional Sudakov–Fernique inequality, with constant , is (HighDimProb.RandomProcesses.sudakov_fernique_finite_dim). This mission produces machine-checked versions of the vector contraction for Gaussian averages and of the boolean-combination bound, and records the corrections the printed statements need.
The obvious approach to Theorem 14 compares two Gaussian processes indexed by the class, but Definition 2 takes the supremum of an absolute value scaled by , while Gaussian comparison inequalities bound the expected supremum of the process itself. The printed proof equates the two; done carefully, the comparison with the printed constant of Lemma 13 gives only . Reaching the printed requires a comparison with constant and an argument that handles the absolute value. A second difficulty is that the classes may be infinite and unbounded, so expected suprema must be handled as extended-valued quantities, and the reduction to finite classes ("without loss of generality") must be justified. For Theorem 16 the extension of must be checked to be Lipschitz across the boundaries of the tents in the Euclidean, not the sup, norm.
The source is the published JMLR article (vol. 3, 2002, pp. 463–482), not the COLT 2001 version, whose numbering differs.
ENNReal supremum against and . An unbounded class has complexity ; a real-valued supremum or Bochner integral would silently return there and make the upper bounds false, so that encoding is ruled out. No finiteness or boundedness of any class is assumed.EuclideanSpace ℝ (Fin m), so "Lipschitz" refers to the Euclidean distance as printed. Using Fin m → ℝ (the sup distance) would change the theorem.A complete development needs Gaussian comparison for finite index sets (available on the platform), the reduction from infinite to finite classes for extended-valued suprema, and elementary Euclidean geometry of the cube. The first two are reusable for every Gaussian-average argument in learning theory. Proofs of any milestone, and of the constant- variant of Lemma 13 transported between probability spaces, are welcome.
The multi-secretary problem is the basic model of selecting under a budget from a stream of offers. Hiring a fixed number of candidates, accepting a fixed number of requests for a perishable resource, and admitting customers into a capacity-limited service all have this structure. Each item must be accepted or rejected on arrival, and the comparison point is the offline decision maker, who sees the whole sequence and keeps the best items. The gap between the two expected values is the regret.
A common class of heuristics in revenue management and online resource allocation does not react to the realised history. These policies fix in advance, period by period, a probability of accepting each type of item, and then follow it until the budget runs out; static bid-price and randomised-acceptance rules are of this kind (Talluri and van Ryzin 2004). Arlotto and Gurvich (arXiv:1710.07719v2, Theorem 1) show that when abilities take finitely many values, an adaptive policy has regret bounded uniformly in the horizon and the budget . Their Theorem 3 shows that the restriction to non-adaptive policies costs order over a wide range of budgets. Read together, these two results separate adaptive from non-adaptive control by an unbounded factor. This mission formalizes the non-adaptive half.
There are candidates with abilities , independent and identically distributed on values , with masses and . Write and . The budget is , with .
The offline value is
A non-adaptive policy is a matrix . At time , if budget remains and , the candidate is selected with probability , independently of everything else. The selection coins are then independent Bernoulli variables with . The policy selects until coins have come up. Its value is the expected total ability selected, and
The deterministic relaxation replaces the random counts by their means. Its value is
with solution . The index policy takes its probabilities from : .
For every , and there is such that, for all masses with and all with ,
The constant does not depend on the masses beyond , nor on or .
Theorem 3 is the lower half of the separation in Theorem 1 of the paper. The Budget-Ratio policy and the dynamic-programming policy have regret , uniformly in , while every non-adaptive policy has regret when lies strictly between and . The order of fluid and static randomised policies is therefore a property of the whole class, not of a poor choice inside it. Lemma 4 shows that the budget range cannot be removed: with a small budget a non-adaptive policy is as good as any.
The result is proved in the source but has not been machine-checked. A complete development would formalize, inside one finite probabilistic model: the binomial overshoot bound, a uniform anti-concentration estimate for Bernoulli sums, the structure of optimal non-adaptive policies, and the comparison with the offline sort. The source's proof of Theorem 3 also relies on a lemma that fails as printed (see Formalization scope), so a formal proof would close a real gap in the published argument.
The upper bound of order (Lemma 3) follows from a variance computation. The lower bound must hold for every non-adaptive policy, including time-varying ones, and the obvious argument does not cover them. That argument compares a policy with the index policy and shows the index policy loses . A policy can, however, differ from the index policy by order in its expected selection counts and still have regret of the same order. The step "small regret forces ", which the source uses, is exactly the step that fails.
What has to be shown is that the selection count of an optimal policy fluctuates by order , uniformly in the policy. A policy that runs out of budget early then misses top-value candidates late in the horizon, and one that keeps budget wastes slots. Both effects must be bounded below by a multiple of that is uniform over all masses with the same . Lemma 5 needs a normal approximation with an explicit, -independent error. Lemma 7 needs the existence of an optimal policy, which is a maximisation over a continuum of matrices.
The source is the arXiv preprint arXiv:1710.07719v2 (1 June 2018). Its printed page numbers equal the PDF page numbers.
a f : Fin m → ℝ. Lean index is the paper's index , so a 0 is the largest value and f (Fin.rev 0) is the mass of the smallest. The standing assumptions of Sec. 2 are IsValues a (strictly decreasing, positive) and IsMasses f (positive, summing to one).Contributions of any kind are welcome. Reusable pieces include binomial overshoot bounds, anti-concentration for sums of independent Bernoulli variables (for example via a Wasserstein normal approximation, which Mathlib lacks), and compactness arguments for optimal randomised policies.
The multi-secretary problem is the simplest model of capacity allocation under uncertainty: a decision maker sees candidates one at a time and may hire at most of them, with every decision final. The same structure underlies single-resource revenue management (accepting or rejecting booking requests against a fixed inventory; see Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004), online knapsack and packing problems, and dynamic assortment of limited stock.
The performance of an online policy is measured against the offline benchmark, the value of the best candidates chosen with full hindsight. The gap between the two is the regret.
This mission formalizes that upper bound.
Abilities take values in a finite set of distinct positive reals, with probabilities , . Write for the mass strictly above , and
The abilities are independent with this distribution. Budget pairs range over the triangle .
For every there is a constant such that for every instance with and all , and
No constant is fixed. Only the shape is asserted: a bound uniform in , , the support size and the distribution, given .
The result. Bounded regret means that the loss from not knowing the future is a fixed number of candidates' worth of value, however long the horizon and however large the budget. The bound holds uniformly over all distributions with the same . It is attained by an explicit, adaptive, non-randomized rule that compares one ratio with fixed thresholds. The companion result of the same paper shows that every non-adaptive policy suffers regret of order in the interior regime. Together they quantify the value of adapting to the remaining budget. Lemma 1 of the paper shows the dependence on cannot be removed.
Formalizing it. The result is proved in the paper, but no part of it is machine-checked; there is no multi-secretary or bounded-regret development on the platform. The mission produces several pieces of machinery: a reusable finite model of sequential selection with online policies and the offline benchmark; an explicit online policy with its stopping-time analysis; and a binomial overshoot bound usable elsewhere. The constant is not made explicit in the paper. A formal proof would give one, and sharper constants are welcome.
The offline decomposition and the sufficient condition are bookkeeping with counts and one concentration bound. The hard step is Theorem 2: showing that the budget ratio stays within of its attracting threshold until a bounded expected number of periods before the end. Near the horizon a single selection moves the ratio by about , so the band becomes easy to leave. Equivalently, the target that the deviation process must exceed shrinks to zero. A standard martingale or drift argument with a fixed band therefore does not give a bound uniform in . The paper combines the mean-reverting drift of the deviation process with an exponential tail bound (its Proposition 4) and a Lyapunov argument. A second subtlety is uniformity: every constant must depend on (and ) only, never on , the , or .
The source is arXiv:1710.07719v2; its printed page numbers equal the PDF page numbers.
Representation.
Fin m, with index 0 the largest value ; Lean index is the paper's .Quantifiers. The constant in the goal is chosen after and before , the instance, and . A statement with chosen after the instance, or after , is trivial (regret ) and is excluded.
Corrections to the printed text, disclosed in the items.
Infrastructure. The model definitions (instance, offline value, online policies, counts, thresholds, action index) and the binomial overshoot lemma are reusable for other finite-support online selection and revenue-management results. All of the following are welcome:
Assortment optimization asks which set of products a firm should offer when customers choose among the offered products according to a discrete choice model; it underlies shelf-space planning in retail and fare-class control in airline revenue management (Talluri and van Ryzin, 2004). Under the nested logit model products are grouped into nests, and a customer first picks a nest and then a product inside it. Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) map out how hard this problem is across variants of the model.
When every nest dissimilarity parameter is at most one and a customer who chose a nest always buys there, offering the top-revenue products of each nest is optimal (Theorem 4 of the paper, the subject of an earlier mission of this series). Once a customer may leave a nest without buying — a partially-captured nest — that structure breaks and the problem becomes NP-hard (Theorem 8). This mission targets the paper's response: a small, explicitly constructed family of candidate assortments per nest from which a linear program recovers a solution within a factor of two of optimal.
There are nests and, in each nest, products . Product of nest has a revenue and a preference weight , with . Nest has a dissimilarity parameter and a within-nest no-purchase weight ; is the weight of choosing no nest. For an assortment ,
and the expected revenue of is . The optimal expected revenue is the optimal value of the linear program
and problem (4) is the same program with the second family of constraints imposed only for a chosen collection of candidate assortments in each nest.
Throughout, for every nest and the are arbitrary. For a capacity , the knapsack value is the largest over assortments with (display (9)). Its continuous relaxation (11) allows fractional under the same capacity. The greedy solution of (11) fills the capacity with the products of weight at most in revenue order, each fully while it fits and the next one fractionally, and
Problem (10) replaces the per-assortment constraints of (3) by .
Let be an optimal solution of (4) with candidate collections . Then
Two further statements accompany the goal: the factor-two revenue guarantee obtained from Theorem 10 and Theorem 1 of the paper, and the fact that every is one of the at most assortments , the first products by revenue among the lightest.
Theorem 10 turns an NP-hard assortment problem into a linear program with variables and constraints whose solution is within a factor of two of optimal. The construction is explicit: the candidates are defined by a greedy rule, not by an optimization oracle. The same template, a restricted linear program whose doubled optimum is feasible for the full one, is reused in §6 of the paper for the most general instances, and Lemma 9's knapsack reformulation is the link to the classical approximation theory of knapsack problems (Williamson and Shmoys, 2011).
The theorem is proved in the paper. No machine-checked proof of it, of Lemma 9, or of greedy optimality for the continuous knapsack with an eligibility bound exists on the platform. Formalizing it yields a checked factor-two guarantee and a reusable fractional-knapsack development.
The obvious argument would compare the restricted program (4) with (3) constraint by constraint. That fails: (3) has one constraint per subset of products, and most subsets are not candidates. The comparison has to pass through the knapsack reformulation (10), which requires showing that a maximum over all subsets equals a maximum over a one-dimensional capacity parameter, using and in an essential way. The second obstacle is that the greedy assortment keeps only the fully taken products, so its value can fall short of the continuous knapsack value, and no single candidate assortment need attain the knapsack bound. With dissimilarity parameters above one the monotonicity behind the reformulation is lost, and §6 of the paper needs a different factor.
Products are Fin n (indices ), nests a finite type, and every quantity is real. Powers are Real.rpow; , which gives . An optimal solution of a linear program is a feasible pair whose is minimal among feasible pairs. The constraint "" of (10) is stated in constraint form, for every , so no real supremum is taken. is defined for only; its placeholder value for is never used. Ties in revenue (and, for , in weight) are broken by index. The candidate collection is taken over real ; adds nothing, since every capacity of at least already gives .
Standing assumptions and added hypotheses: for every nest (the section's assumption) on the goal and on every model milestone; the pins , , and the revenue ordering, shared by the series; on Lemma 9, on and on (28)/(29), the paper's nonempty ; and on the factor-two revenue guarantee, where Theorem 1 of the paper fails without it.
The greedy assortments are defined explicitly. Quantifying over arbitrary optimal solutions of (11) instead would change the candidate collection and is not the paper's theorem. The goal states feasibility for the full program (3) and does not mention knapsack values, the greedy solution or the case split. A formalization that weakens the conclusion to feasibility for (10), or that drops the singletons from the candidate collection, is not a solution.
Needed infrastructure: fractional knapsack optimality of the greedy rule with an eligibility bound, monotonicity of and for , and finite maximization over subsets. The fractional-knapsack lemmas are reusable beyond this mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.
A retailer choosing which products to display, or an airline choosing which fare classes to open, solves an assortment optimization problem: pick the set of offered products that maximizes expected revenue when customers choose among what is offered according to a discrete choice model. Under the multinomial logit model the answer has a simple form: an optimal assortment consists of the few highest-revenue products (Talluri and van Ryzin, 2004). The multinomial logit model, however, forces every pair of products to compete in the same way. The nested logit model relaxes this by grouping products into nests (brands, store sections, departure times) and letting a customer first choose a nest and then a product inside it.
Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) study how much of the multinomial logit structure survives under the nested logit model. Their first answer is the theorem this mission targets: when the nest dissimilarity parameters are at most one and no customer who chose a nest leaves it without buying, offering the top products of each nest is still optimal. The other missions of this series treat the cases where this fails: dissimilarity parameters above one (the problem becomes NP-hard) and nests with their own no-purchase option.
There are nests and, in each nest, products . Product of nest has a revenue and a preference weight ; products are ordered so that . Nest carries a dissimilarity parameter and a within-nest no-purchase weight , and is the weight of choosing no nest at all.
An assortment is a tuple of subsets . Write
A customer picks nest with probability and then, inside the nest, product with probability . The expected revenue is
and problem (2) asks for over all assortments. The nested-by-revenue assortment collects the highest-revenue products of nest , with and .
This mission works under the standing assumptions of §3 of the paper: competitive products, , and fully-captured nests, , for every nest .
If and for all , there exists an optimal solution of problem (2) such that
A companion item (not a milestone) states the algorithmic consequence at the end of §3: solving the linear program (4) over the candidates and choosing in each nest a maximizer of problem (5) gives an optimal solution of (2).
Theorem 4 reduces problem (2), a search over assortments, to nested-by-revenue combinations, and the paper then finds the best one with a linear program with variables and constraints. It marks the exact boundary of the classical multinomial logit structure inside the nested logit model: the paper's §4 shows that a single nest with already breaks it, and that the general problem is NP-hard. The structural statement is also the base case for the approximation guarantees of §§5–6, which compare against nested-by-revenue assortments.
The theorem is proved in the paper; to our knowledge it has no machine-checked proof. A formal proof would supply a verified reduction from a combinatorial revenue maximization over the nested logit model to a polynomial-size search, with every boundary case (empty nests, , ties in revenues) handled explicitly.
The obvious argument copies the multinomial logit proof: take an optimal assortment and swap a low-revenue product for a missing higher-revenue one. Under the nested logit model this exchange changes the nest's attraction non-linearly, so the revenue of the modified assortment is not an affine function of the change, and a simple swap can lower the expected revenue. The argument must instead control how adding or removing one product moves the nest weight relative to the nest revenue, and this is exactly where enters, through two scalar inequalities in the ratio of nest weights. With these inequalities fail and so does the theorem.
A second subtlety is ties: several optimal assortments may exist, and only some of them are nested by revenue. The statement asserts existence, not that every optimum has this form.
All statements live in the namespace NestedLogitVariants.Competitive and share one definition file. Nests form a finite type ι with decidable equality; products are Fin n, indexed , so is nbr n j with , and gives . Powers are Real.rpow, and , which gives . Optimality of an assortment means its revenue is at least that of every assortment.
Standing assumptions carried as hypotheses: , , revenues ordered within each nest, and §3's and . Three pins are disclosed: (the paper allows zero-weight padding products, under which Proposition 2 fails), , and (the paper's ; its convention fails at ). The section's "without loss of generality " is a hypothesis of Proposition 2, Lemma 3, the threshold, the exchange step and the LP item; the goal itself only assumes , and the case is milestone 1. The two scalar inequalities are stated as inequalities, not as monotonicity claims.
The goal is not trivialized by any hypothesis: it assumes none of the milestones, and stating "some nested-by-revenue assortment exists" (always true) or "every optimal assortment is nested by revenue" (false under ties) would be a different theorem.
Needed infrastructure is light: finite sums, real powers, and concavity of for . The scalar lemmas are reusable for other nested logit results. Proofs of any milestone are welcome independently.
Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision is fixed before an uncertain right-hand side is revealed, and a second-stage decision is chosen after it, as a function of . The objective protects against the worst in an uncertainty set . Computing an optimal fully adaptable solution is intractable in general (Feige, Jain, Mahdian and Mirrokni, IPCO 2007), so practitioners restrict the second stage to affine policies , introduced in robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004). An optimal affine policy is computed by a single convex program, but its cost may exceed the adaptive optimum.
Bertsimas and Goyal (Math. Program. Ser. A, 2012) quantify this loss. Earlier, Bertsimas, Iancu and Parrilo (Math. Oper. Res. 2010) proved affine policies optimal for a class of one-dimensional multistage problems. The present paper shows that affine policies are optimal when is a simplex (Theorem 1), that they can lose a factor in general (Theorem 3), and — the subject of this mission — that when the first-stage constraint matrix is nonnegative they never lose more than (Theorem 4). Nonnegative first-stage matrices occur in network design, facility location, capacity planning and other covering problems.
Let , , , , and let be convex, compact and full-dimensional. The problem is
where the minimum is over first-stage vectors and arbitrary maps . The problem is assumed feasible. The value is the same minimum restricted to affine second stages , which must still satisfy on .
For each coordinate put and fix a maximizer with (display (38)). The scaled sum of over an index set is .
Algorithm (Fig. 1 of the paper) starts with and . While some has scaled sum over larger than , it picks a maximizer of that scaled sum, adds to the running vector on the coordinates of , and moves to every coordinate whose running value has reached . It returns the number of iterations , the vectors , their sum , and the partition .
In the -uncertain variant (60)–(63), only right-hand sides are uncertain and the remaining are fixed at ; all data are nonnegative. Its values are and .
If entrywise, then a feasible affine solution exists and
Theorem 4 is an upper bound on the price of restricting to affine policies, and Theorem 3 of the same paper shows it is tight up to a constant factor: for every there are instances with where the gap is . Together they settle the order of the approximation ratio of affine policies for covering-type two-stage problems. Theorem 5 refines the bound to when only of the right-hand sides are uncertain, which is the regime of many applications. The construction is also the template for the paper's Theorem 6, a -approximation for general obtained from a single dominating simplex.
The results are proved in the paper. To the knowledge of this mission, none of them has a machine-checked proof. Formalizing them produces a reusable model of two-stage adaptive linear programs with affine policies, a verified analysis of a greedy covering procedure (Algorithm ), and an explicit-constant version of an statement.
The obvious attempt scales the fully adaptable solution at the extreme points linearly in : . This is feasible at cost factor only when the scaled sums stay below on (condition (39)); in general they can reach , and the linear rule then costs a factor . The difficulty is to handle the coordinates where has large scaled mass. Algorithm isolates them, and the delicate point is the iteration count: each round must add scaled mass above , while the total scaled mass that can be absorbed before every coordinate leaves is at most . A formal proof must also track the algorithm's state through its recursion, because the argmax choices are not unique and the statements must hold for every run.
Vectors are Fin m → ℝ with the componentwise order, indices are 0-based, and matrices are Matrix (Fin m) (Fin n) ℝ. Nonnegativity of a matrix is stated entrywise. and are infima of the set of worst-case cost bounds achieved by feasible solutions; the goal and Theorem 5 assert the existence of a feasible affine solution, which rules out the trivializing reading in which is the infimum of an empty set (Lean's junk value ) and the inequality holds for free. The goal does not mention , or Algorithm ; these appear only in milestones.
and are given with their defining properties ( is the greatest value of on , and with ). Algorithm is encoded as a recursion on a choice sequence , with step 2(d) read as . A complete run requires the loop test and the argmax property at each iteration and the failure of the loop test at the end. The milestones on the constructed policy are stated for every feasible and every cost bound , so that no attainment of the optimum is assumed.
Standing assumptions of (1) carried by the goal: ; convex, compact, with nonempty interior; feasibility. Milestones drop the ones they do not use. Theorem 5 carries compactness and full-dimensionality of , which §5.1 does not repeat but its proof uses through Theorem 4. Lemma 11 assumes that is finite, since the paper's inequality is between extended reals.
A complete development needs: finite-dimensional linear programming facts (existence of optimal solutions is not needed), compactness arguments for the argmax in Algorithm , and manipulation of finite sums over Finset. The model of (1) and the analysis of Algorithm are reusable by the companion mission on Theorem 6. Contributions of proofs of any milestone, and of supporting lemmas about the recursion of Algorithm , are welcome.
An -graph is a -regular graph on vertices in which every eigenvalue of the adjacency matrix other than the top eigenvalue has absolute value at most . Graphs of this kind with small compared with are expanders. They are used in derandomization, error-correcting codes, sorting networks and many other constructions in theoretical computer science. A Ramanujan graph achieves , which is asymptotically optimal.
The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (LPS, 1988) exist only for special vertex counts, such as for a prime or the size of a quaternion group modulo . N. Alon, in Explicit expanders of every degree and size (arXiv:2003.11673, 2020; Combinatorica 41, 2021), asks for explicit -graphs with for every degree and every number of vertices . His Proposition 1.1 builds such graphs out of LPS graphs, and one ingredient is purely arithmetic. If the available vertex counts of an LPS family are dense enough, so that for every large one is within a factor of , then a few vertices can be added or removed while keeping the spectral bound.
This mission formalizes that ingredient, Lemma 2.2 of the paper (p. 7). It concerns the vertex counts of the LPS graphs for two fixed primes and all exponents . With fixed, the construction needs no large primes, which is why Proposition 1.1 is strongly explicit for every fixed degree.
Fix natural numbers . For natural numbers define the LPS vertex count
When are distinct primes congruent to modulo and , this is the number of vertices of the LPS Cayley graph (§2.3, p. 6). Lemma 2.2 itself only requires to be distinct primes. Both fractions are integers, because is a product of three consecutive integers.
The proof uses the real number , and the fractional part , written in the paper.
For distinct primes there is a function with such that for all sufficiently large there are integers with
Equivalently, the ratio between consecutive elements of tends to . The statement fixes no rate for , matching the paper's .
The result. Lemma 2.2 is the step of Proposition 1.1 that turns a family of Ramanujan graphs with sparse vertex counts into a family whose vertex counts approximate every large up to a factor . The deviation from can then be absorbed by the general packing argument of §2.1 of the paper. Without it, the construction would have to search for large primes depending on , and the result would be explicit but not strongly explicit.
The formalization. The lemma is proved in the paper, in one paragraph. To our knowledge no machine-checked proof exists, and the platform has no statement of it. The only related platform item is the irrationality of , the case , of milestone 1. Formalizing the lemma requires a quantitative inhomogeneous step that the paper leaves implicit ("implying the desired result"). Its last sentence also contains a misprint that the formalization corrects (see below). The Diophantine milestones 1–3 are reusable for any argument about the multiplicative density of , for instance the ratio of consecutive elements of .
Each milestone is short. The difficulty is in making the paper's last sentence ("implying the desired result") into a proof. Taking or large separately does not work: changing or by one multiplies by or , a fixed factor larger than , so the values obtained by varying one exponent leave gaps of a constant ratio. The bound must hold for every large , not just along a subsequence, and the exponents must stay positive throughout. Milestone 2 is the classical fact that the multiples of an irrational number are dense modulo . It needs a pigeonhole argument, not just the irrationality.
Real.log, and the fractional part is Int.fract.IsLittleO along atTop) and, eventually in , with . This is equivalent to the form "for every , every large has with ". The paper's proof yields the second form, with the factor for arbitrary .Int.fract and a pigeonhole or Dirichlet-approximation argument for milestone 2, and real exponentiation and asymptotics for the goal. Contributions of alternative proofs of milestone 2, for instance via Mathlib's Dirichlet approximation theorem, are welcome.The conditional logit model is the workhorse of discrete choice analysis in transportation, marketing, labour and industrial organization. McFadden's 1974 chapter derived it from a theory of population choice behaviour and showed how to estimate it by maximum likelihood; this line of work was recognized by his 2000 Nobel Prize in Economic Sciences, awarded for theory and methods of discrete choice analysis. Every applied logit estimation rests on a basic question: does the maximum likelihood estimate exist for the sample at hand? In small samples it may not. When one alternative is always chosen whenever it is available, the likelihood keeps increasing as a parameter tends to infinity, and numerical optimizers report diverging coefficients. This failure is known in the binary case as complete or quasi-complete separation. McFadden's Lemma 3 gives the exact condition, for the multinomial conditional logit model with general alternative sets, under which a maximizer exists.
Timeline. Berkson (1951, 1955) popularized binomial logit; multinomial versions were developed by Gurland (1960), Bloch (1967), Rassam (1971), McFadden (1968) and Theil (1969, 1970). McFadden (1974) stated the existence criterion for the conditional logit likelihood (Lemma 3) together with a quadratic-programming test for it (Lemma 4). Albert and Anderson (1984) later classified separation patterns for binary and multinomial logistic regression, and Haberman (1974) treated existence for log-linear models.
A choice experiment has trials. Trial offers an alternative set of alternatives, indexed , each described by an attribute vector (the values of specified functions of the individual's and the alternative's characteristics). Trial is repeated times, and alternative is chosen times, so .
For a parameter , with the inner product, the selection probabilities are
and the log-likelihood of the sample is
Write for the probability-weighted mean attribute vector of trial .
Axiom 5 (Full Rank). The matrix with rows has rank .
Axiom 6. There is no nonzero with for all and . Equivalently, no nonzero direction makes every observed choice weakly best in its alternative set.
Under Axiom 5,
Lemma 3 tells the practitioner when the conditional logit maximum likelihood estimate exists, before any numerical optimization is attempted. It is a linear-inequality condition on the data alone, so it can be checked by linear or quadratic programming (Lemma 4 of the same paper). The existence of the estimator is also the first step of McFadden's asymptotic theory: Lemma 5 shows that Axiom 6 holds with probability tending to one, and Lemma 6, consistency and asymptotic normality, concerns the estimator whose existence Lemma 3 characterizes. The concavity and Hessian formulas (19)–(20) are the basis of the Newton–Raphson computation of the estimator and of its asymptotic covariance matrix.
The result has been proved since 1974 and is classical. To our knowledge it has no machine-checked proof; Mathlib has no statement about the existence of logit or softmax-regression maximum likelihood estimates. Formalizing it produces a verified existence criterion for the multinomial logit likelihood, verified gradient and Hessian formulas for log-sum-exp likelihoods with repeated observations, and a verified link between full column rank and strict concavity.
The likelihood is concave, and concave functions on need not attain their supremum. Concavity alone therefore gives nothing, and existence must come from a growth condition. The obvious approach, "the likelihood is bounded above by , hence attains its maximum", fails: is bounded but can approach its supremum only at infinity, which is exactly the separation case. Sufficiency needs a quantitative rate at which decreases, uniform over all directions; a direction-by-direction argument does not suffice. Necessity requires strict concavity, which is where Axiom 5 and the requirement that every trial be observed enter. A trial with can supply the rank of Axiom 5 while contributing nothing to , so with such a trial necessity fails. The calculus part, (19)–(20), involves differentiating sums of log-sum-exp terms over dependent index types and identifying the result with a weighted covariance operator.
EuclideanSpace ℝ (Fin K), so is the Euclidean norm and is the inner product ⟪z, θ⟫. Trials are Fin N, alternatives of trial are Fin (J n), and the counts are natural numbers.Data K bundles , , , and the standing assumptions and for every trial; these make the trial and alternative index sets nonempty.Data plus Axiom 5".Equilibrium distributions of Markov models of networks are rarely computed by solving the full equilibrium equations directly. In the classical product-form results (migration processes, Jackson and Kelly networks, loss networks, clustering processes) the equilibrium distribution satisfies a stronger, local family of equations, and that is what makes it computable. The strongest such family is detailed balance, which characterizes reversibility. Many models that are not reversible still satisfy an intermediate family, partial balance: the probability flux balances not pair by pair but across a chosen set of transitions. F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) uses partial balance throughout: quasi-reversibility in Chapter 3 is a form of it, and the models that display it tend to be insensitive, meaning their equilibrium distribution does not change when exponential holding times are replaced by general ones with the same mean.
Section 9.4 of the book collects what partial balance means in a single statement. Theorem 9.5 summarizes Exercises 1.6.2–1.6.4 and 1.7.7–1.7.8 and gives five operational characterizations of partial balance. Corollaries 9.6–9.8 translate them into the language of spatial processes, and Theorem 9.9 turns partial balance of a coarse description into a product-form equilibrium for a finer one. This last step is the mechanism behind insensitivity.
A Markov process on a state space has transition rates for , with . It is irreducible: every state can be reached from every other through transitions of positive rate. An equilibrium distribution is a collection of positive numbers summing to one that satisfies the equilibrium equations
For an irreducible process on a finite state space it exists and is unique.
Given a set , satisfies partial balance with respect to if
Truncating the process to deletes every transition out of , and the result is required to be irreducible within . The time-reversed process of a process with equilibrium distribution has rates .
A spatial process has sites, the vertices of a graph . Site carries an attribute from a finite set , and the state space is . Write for the state with the attribute of site changed to . The process must satisfy three conditions: only one site changes at a time; the rate depends on the other sites only through the neighbours of ; and any can be reached from without changing the other sites. The conditional distribution of site given the rest is . A Markov field is a positive distribution whose conditional distributions depend only on the neighbours of .
For an irreducible process on a finite with equilibrium distribution , a nonempty within which the truncated process is irreducible, and a constant , , the following are equivalent:
When is nonempty, these are also equivalent to:
Theorem 9.5 makes partial balance testable by operations on the process itself: truncation, speeding up or slowing down transitions, and time reversal. The book points to close relationships between statement (iv) and the product form of Section 2.3, and between statement (ii) and part (iii) of Theorem 3.12. Corollary 9.6 (iv) explains why the reversed migration process has such a simple form. Corollary 9.7 strengthens Theorem 9.3 by replacing reversibility with partial balance at each site. Theorem 9.9 is the step from partial balance to insensitivity: it is what the book uses to show that a spatial process keeps its equilibrium distribution when the lifetimes of attributes are mixtures of gamma distributions.
All of these results were proved in 1979. None has a machine-checked proof. The platform has the reversible special case of statement (ii) (KellyStochasticNetworks.truncated_reversible) and the rate-level objects for time reversal and truncation, which this mission reuses. Formalizing Theorem 9.5 also produces a reusable account of embedded exit and entry chains of a finite Markov process.
Most of the equivalences (i)–(v) are short manipulations of the equilibrium equations, but each direction from a property of an altered process back to partial balance needs uniqueness of equilibrium distributions for irreducible finite processes, and (v) ⇒ (i) also needs their existence. Mathlib has neither in the form needed here. Statement (vi) is a different kind of claim. The equilibrium distribution of the exit chain is proportional to the exit flux , and that of the entry chain to the entry flux. Proving this requires the hitting distributions and the Green's function of the jump chain killed on leaving a set, and the convergence of the series that define them. Corollary 9.8 (v) inherits that work. Theorem 9.9 requires uniqueness for the reduced frozen processes and careful bookkeeping of the fibres .
State spaces are finite types, and every sum is an unconditional sum over a finite type. Because the state space is finite, the book's extra condition for (vi), a finite flux out of , holds automatically. Rates are real functions with built into the hypotheses; the reduced rates of (9.31) also have zero self-rates. "The equilibrium distribution of a process is " means: is positive, sums to one, satisfies the equilibrium equations, and every distribution with these properties equals . The book's " or " is read as , , so that altered rates remain rates. Truncation to is the published truncatedRates, a process on the subtype , and the reversed rates are the published reversedRates. The exit and entry chains are defined from the jump chain through series of restricted matrix powers. Spatial processes live on with given by Function.update. In Theorem 9.9 the graph is complete, as the book assumes from p. 202 on.
The equilibrium distribution of the truncated process must be the unique positive normalized solution of the truncated equilibrium equations. It must not be defined as the conditional distribution, which would make (ii) a tautology. For the same reason (iii) and (iv) are stated through the equilibrium equations of the altered rates, not by assumption.
Theorem 9.10 (p. 207) is not a target. Its hypothesis, that a nominal lifetime "can have any distribution with unit mean", is not defined on the page, and the point-process and lifetime description it needs lies outside this rate-level development.
Contributions are welcome at every level: uniqueness and existence of equilibrium distributions for irreducible finite rate matrices (reusable across the series), convergence of the killed Green's function, and proofs of the corollaries from the goal.
Many convex optimization models combine a smooth loss, a nonsmooth penalty whose proximity operator is easy to compute, and a second penalty applied after a linear map. Imaging models, for example, often place a data-fitting term on the image and a regularizer on its transformed coefficients. The resulting objective has the form . Condat's primal–dual method evaluates the smooth gradient and two proximity operators separately, without requiring a proximity operator for the composite . Condat, 2013 establishes weak convergence with relaxation and summably weighted computational errors. This mission targets its main positive-smoothness theorem, Theorem 3.1, in the final author's version.
The theorem matters when a computed gradient or proximal point is inexact, as is common when a proximal subproblem is itself solved numerically. Its conditions account for these errors directly rather than treating the displayed algorithm as exact. It also gives one parameter regime for two orders of updating the primal and dual variables. These two algorithms share an objective and a solution inclusion, but have distinct recursions.
Let and be real Hilbert spaces and let be bounded linear, with adjoint . The smooth term is convex and differentiable. Its gradient is -Lipschitz when for all . The nonsmooth terms and are proper, lower semicontinuous, convex functions with values in . Such functions form the class . An infinite value may encode a constraint.
For a convex function , its proximity operator minimizes over , where . The Fenchel conjugate is . A subgradient obeys for every . The sought primal–dual solution satisfies
Algorithms 3.1 and 3.2 maintain sequences and . Algorithm 3.1 updates the primal proximity step before the dual one; Algorithm 3.2 reverses that order. Each uses positive step sizes , positive relaxation weights , and errors , and in the gradient and the two proximal evaluations. Their full recursions are part of the Lean setting, so a run is determined by its initial pair. The paper specifies the problem in §2 and both algorithms in §3.
The goal is Theorem 3.1 on p. 5. Suppose , the primal–dual solution set is nonempty, and . Set
For , the theorem assumes
Under these conditions, both sequences of each algorithm converge weakly to the components of a primal–dual solution. The solution may depend on the initial pair and on the run. The milestone list includes Lemmas 4.1 and 4.3–4.5, the strict positivity claim for the block operator , estimate (29), and the error-free optimality inclusions (22) and (44), ordered as preliminary results followed by the two algorithm-specific claims. These targets match the results stated in §4 of the source version.
The result supplies a convergence guarantee for a composite objective under an explicit coupling condition on , , and . It permits relaxation weights that vary with and errors that are summable only after weighting by those same relaxation values. The dual conclusion is substantive: convergence of the primal sequence alone would not give convergence of the dual certificate produced by the algorithm. The weak topology is appropriate in general Hilbert spaces; norm convergence would assert more than the paper proves.
The theorem is proved in the 2013 paper. The present formalization task is to give its statement and the selected operator lemmas machine-checked proofs in Lean. Related platform definitions for proximal maps, monotone operators, nonexpansive maps, subgradients and weak convergence already exist; the paper-specific convergence theorem and its selected milestones are new targets in this proposal. The resulting definitions and abstract Lemmas 4.1, 4.3–4.5 can be reused in later operator-splitting developments.
The displayed recursions involve three errors, two proximal evaluations, a linear map and its adjoint, and two different update orders. A direct estimate on does not by itself control the coupled dual variable, while a bound on only the combined objective value would not establish weak convergence of either iterate. The relaxation condition permits weights without a fixed positive lower bound, so a convergence argument cannot replace the stated divergent series by a simpler constant-step assumption. The abstract lemmas must also retain the endpoints and present in the source.
Lean uses complete real inner-product spaces for and , a continuous linear map for , and EReal for , and their conjugates. The conjugate supremum is taken in EReal. The paper's class and proximity maps use published definitions; the latter are parameters constrained to be the actual proximal minimizers. Positive step sizes and proper closed convex data ensure such maps exist and are unique. The subgradient predicate explicitly requires a finite value at the base point; this follows from the source's properness assumptions when a subgradient exists.
Both algorithms are represented by recursion predicates on every natural-number index, with all error terms present. The goal quantifies over every run and chooses its weak limit afterwards. Divergence to means finite partial sums tend to atTop; a finite weighted error sum means the corresponding nonnegative real sequence is summable. These choices prevent a default value of an infinite sum from satisfying the hypotheses. The nonempty solution set is an explicit standing assumption from p. 4 and implies the earlier nonempty-primal-minimizer assumption. A condition that made all runs impossible, or one that discarded either the primal or dual conclusion, would not represent Theorem 3.1.
The block operator is represented through its quadratic form ; is recorded for Algorithm 3.2. The complete development will need the abstract iteration lemmas, proximal optimality conditions, block-metric estimates, and the links from each algorithm's inclusion to the solution set. Contributions proving those results, or building reusable Hilbert-space operator infrastructure needed by them, are in scope. The several-composite-functions extension in Theorem 5.1 is reserved for separate work.
The conditional logit model assigns to an alternative in a finite choice set the probability , where is a "representative utility" built from observed attributes of the alternative and the decision maker. It is the workhorse of discrete choice econometrics, transportation demand forecasting, marketing and revenue management, where it underlies multinomial logit assortment and pricing models. Its appeal for applied work is computational; its appeal for economics is that it can be read as the aggregate behaviour of a population of utility maximizers. This mission formalizes the result that makes that reading exact: Lemmas 1 and 2 of D. McFadden, Conditional logit analysis of qualitative choice behavior (1974), which show that, under a mild regularity condition, logit choice probabilities arise from random utility maximization exactly when the idiosyncratic taste shocks follow the extreme value (Gumbel) distribution.
Timeline:
An individual faces alternatives with representative utilities . The utility of alternative is , where the taste shocks are independent and identically distributed with a common law on and distribution function . The individual chooses the alternative of highest utility, so the selection probability of is (Equation (2) of the paper)
computed under the product law of the shocks. The logit formula (Equation (12)) is . The extreme value law (Equation (13)) is .
A law is translation complete if for every function of bounded total variation on with , the condition for every real forces outside a Lebesgue-null set. Laws whose characteristic function never vanishes, the extreme value law among them, are translation complete (footnote 5 of the paper).
In Lean the law is μ : Measure ℝ with [IsProbabilityMeasure μ], is ProbabilityTheory.cdf μ, the selection probability is selProb μ V i for V : Fin J → ℝ, and the logit formula is logitProb V i.
Fix a universe of alternatives with a representative utility map onto the real line. For a translation complete law normalized by ,
The normalization only fixes the location of the shocks: without it the conclusion is the one-parameter family of Lemma 2 below.
The result separates two readings of the logit formula. Lemma 1 shows that it is consistent with utility maximization; Lemma 2 shows that, within the class of i.i.d. additive random utility models with translation complete shocks, the extreme value law is the only one consistent with it. Consequences drawn from the random utility reading, such as the log-sum formula for expected maximum utility used in welfare analysis, therefore apply to logit models without further distributional assumptions inside that class. The same reading supports the interpretation of multinomial logit demand in assortment optimization and revenue management.
Both lemmas are proved in the paper and in later textbooks; neither is open. As far as a search of the Prove2Me catalog shows, neither has a machine-checked proof. The mission provides Lean statements of the random utility model with i.i.d. shocks, of translation completeness and of the extreme value law that later discrete choice formalizations can reuse.
Lemma 1 is a computation with the extreme value density; its formal cost lies in passing from the product-measure probability (2) to the iterated integral (3) and evaluating an improper integral. Lemma 2 is harder. The natural first idea is to differentiate the logit identity in the utilities and solve a differential equation for ; this requires a density, which Lemma 2 does not assume. Without a density, the only handle on is the logit identity itself, an equality of integrals against that holds for every utility vector; turning such integral identities into pointwise information about is where the hypothesis of translation completeness enters, and it yields statements only outside a Lebesgue-null set, so one-sided continuity of distribution functions is needed to recover identities at every point. A second subtlety is that the paper's (14) is written with while the event (2) is strict, so with a general law the integrals involve left limits of .
Alternatives are indexed by Fin J; the model is indexed by the utility vector, so the individual attributes and alternative attributes enter only through . The shocks have joint law Measure.pi (fun _ => μ), which is what "independently identically distributed" means; a general joint law is not allowed. The event in (2) uses strict inequalities, and the selection probability is defined for every law, with no density. Translation completeness quantifies over BoundedVariationOn h Set.univ with limits at both ends; such are bounded and measurable, so the integrals are genuine, and "measure zero" is Lebesgue measure.
Lemma 2's hypothesis is stated on every finite subset of the paper's alternative universe, with a surjective utility map. Distinct alternatives may have the same utility. The printed proof uses equal-utility alternatives, which surjectivity alone need not supply; proving the stated theorem requires an additional continuity argument. A trivializing formalization is ruled out: the selection probability is a genuine product-measure probability, and the hypotheses of the goal are met by the extreme value law, which is translation complete with .
A complete development needs: Fubini for Measure.pi over Fin J split at one coordinate; the Gumbel density and the improper integral ; the facts that bounded-variation functions are bounded and measurable and that distribution functions are right-continuous with left limits. The integral representation (milestone 1) and the Gumbel computations are reusable in any random utility formalization. Proofs of the milestones, of the footnote-5 fact that the extreme value law is translation complete, and alternative proofs of Lemma 2 are welcome.
A robust Markov decision process (robust MDP) evaluates a policy against the worst transition kernel and reward in an uncertainty set around a nominal model . It is the standard model for planning when the dynamics are estimated from data (Iyengar 2005; Nilim and El Ghaoui 2005; Wiesemann, Kuhn and Rustem 2013). Its Bellman update contains an inner optimization over the uncertainty set at every state, which makes robust planning costly when the sets are not -rectangular.
Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) show that, for -rectangular ball uncertainty sets, this inner optimization can be replaced by an explicit penalty that depends both on the policy and on the value function. The resulting twice regularized (R²) MDPs have Bellman operators with no inner optimization over models. The first mission of this series formalizes the robust–regularized equivalence (Theorem 4.1 of the paper). This mission formalizes Section 5: the R² Bellman operators are monotone and contracting under a bound on the transition radius, and the greedy policy of the R² optimal value is optimal.
Let and be finite nonempty sets of states and actions, a discount factor, a transition kernel and a reward. A policy assigns to each state a probability distribution on . For write and
All norms below are -norms, ; is the sup norm.
Fix nonnegative radii for each state. The R² regularizer is , and the R² Bellman operators are
A policy is greedy for when .
Assumption 5.1 (bounded radius). For each there is with
and . The R² value function of a policy and the R² optimal value are the fixed points of and .
Under Assumption 5.1, and every have unique fixed points; a greedy policy for exists, and every such policy satisfies
every optimal policy is greedy; and when for all the greedy policy is unique, hence the unique optimal R² policy.
Theorem 5.1 is the R² counterpart of the fundamental theorem of discounted dynamic programming: optimal R² values are achieved by stationary policies obtained by a single greedy step. Together with the contraction of Proposition 5.1 (iii) it justifies the R² modified policy iteration algorithm of the paper, whose greedy step is a projection onto the simplex rather than a robust max–min problem. Combined with the first mission of the series, which identifies the robust value of an -rectangular ball-constrained MDP with the optimum of an R²-regularized program, it gives a route to robust planning at the cost of regularized planning.
The results are proved in the paper (App. C), partly by reference to Geist, Scherrer and Pietquin (2019) for the optimality operator. No machine-checked proof of any of them exists; this mission produces the first. Prop. 2.1 is a general fact of convex analysis (Danskin-type smoothness of a conjugate on the simplex) that is reusable for any regularized MDP or entropy-regularized game.
The R² evaluation operator is not affine: the value regularizer is concave in and decreases as grows. Monotonicity therefore does not follow from the positivity of as in the standard case; it requires the second bound of Assumption 5.1, which compares the variation of with the minimal nonnegative bilinear form of . Likewise the contraction modulus is not but , because the regularizer is -Lipschitz between the and sup norms. The optimality step of the classical proof uses linearity of when comparing values of policies; here only monotonicity and contraction are available. Uniqueness of the greedy policy rests on strict concavity on the simplex, which holds only when the regularization weight is positive.
States and actions are finite nonempty types; transitions are arrays P₀ : S → A → S → ℝ with the published predicate IsTransitionKernel; value functions are S → ℝ with the pointwise order. The -norm is an explicit l2norm (Mathlib's norm on S → ℝ is the sup norm, used only for ). is the real supremum over the simplex (attained), and the inner minimum of Assumption 5.1 is the real infimum over nonnegative -unit vectors; the witnesses are explicit. Greedy policies are a predicate, never a function, and the R² value functions are not defined by choice: the goal asserts their existence and uniqueness and speaks about the fixed points.
Disclosed deviations from the page. Assumption 5.1 is a hypothesis of Theorem 5.1 (its proof assumes it). The uniqueness clause of Theorem 5.1 additionally assumes for all : with one state, two actions, zero reward and zero radii every policy is greedy and optimal. Proposition 2.1 assumes continuous on the simplex, without which the maximum need not be attained, and strong convexity is Mathlib's StrongConvexOn for some modulus (norm-independent in finite dimension). Proposition 5.1 (ii) is false as printed and is not drafted: with one state, one action, , , , , , , one has , and , give . Remark 5.1, Algorithm 1 and the variant of App. C.1 are out of scope. The inner minimum of Assumption 5.1 is whenever some , forcing ; this is the assumption as printed.
A formalization in which is the sup norm, the inner minimum ranges over all unit vectors (making the assumption unsatisfiable), or the value functions are postulated rather than shown to exist would be trivial or wrong; the drafted statements avoid all three. Contributions welcome: Prop. 2.1 as a general convex-analysis lemma, Banach fixed-point plumbing for S → ℝ with the sup norm, and the strict concavity of on the simplex.
Many systems consist of a finite number of sites whose states influence one another only locally: fruit trees in an orchard that are diseased or healthy, power sources that are working or broken, individuals holding one of several views. Chapter 9 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) asks which joint distributions such systems have in equilibrium. Earlier chapters of the book produce product-form distributions in which the components are independent; spatial models instead give a limited dependence, and §9.1 makes that notion precise through Markov fields.
The central characterization, that a positive random field is Markov with respect to a graph exactly when it factorizes over the cliques of that graph, is the theorem of Hammersley and Clifford (1971, unpublished manuscript), with published proofs by Besag (1974), Grimmett (1973) and Preston (1973). It underlies Gibbs random fields in statistical mechanics, spatial statistics, image analysis and graphical models. Kelly's §§9.2–9.3 then use it to identify the equilibrium distributions of interacting-particle Markov processes ("spatial processes"), connecting it to reversibility and partial balance.
There are sites, the vertices of a finite graph ; is the set of neighbours of site and the set of sites other than . Site carries an attribute from a finite set , and a state is in . For a set of sites , is the vector of attributes of the sites in . The operator changes the attribute of site to .
A random field is a function on with for every state and . The conditional probability that site has attribute given all other sites is
is a Markov field if for every and (9.2): the attribute of a site depends on the rest of the system only through its neighbours. A simplex is a single site or a set of sites any two of which are neighbours; is the set of simplices of .
A spatial process is a Markov process on with rates such that (i) only one component changes at a time, (ii) depends on only through and , and (iii) can be reached from by transitions that do not alter . The general spatial process of §9.3 has rates
for positive functions , .
A random field is a Markov field if and only if
for some constant and functions .
and it satisfies the partial balance equations (9.18) site by site.
Theorem 9.2 turns a statement about conditional laws, which is how local interaction is usually specified, into an explicit parametrization of the joint law by clique potentials. On a lattice with binary attributes it reduces a Markov field to one parameter per site and one per pair of adjacent sites, giving the form (9.9). Theorem 9.3 shows that local, reversible dynamics produce Markov-field equilibria, and Theorem 9.4 gives a family of non-reversible processes, containing the closed migration process of Chapter 2, whose equilibria are still explicit; its partial balance equations are the bridge to §9.4.
All four results are classical and proved in the book. They are not, to our knowledge, machine-checked in this discrete form. The platform has an open statement of Hammersley–Clifford in a different setting, HighDimStat.GraphicalModels.thm11_8_hammersley_clifford (Wainwright, High-Dimensional Statistics, Theorem 11.8): a random vector in with a strictly positive Lebesgue density and the global (separation) Markov property. Neither statement implies the other as formalized, so this mission poses Kelly's finite, local version separately. A formal proof here also gives reusable infrastructure: conditional probabilities of a distribution on a finite product space, and factorizations over the cliques of a graph.
The "if" direction is routine. The "only if" direction is where the content lies: the functions must be produced from alone, and a product over the cliques of must reproduce at every state, not only at the states whose nonzero attributes sit on a single clique. The natural first idea, one factor per site read off from the conditional laws, fails as soon as two sites interact. The Markov property must also be brought from its explicit form (9.2), which involves a marginal over the non-neighbours, into a usable statement about itself. Strict positivity is essential: without it the "only if" direction is false (Exercise 9.2.2). For Theorem 9.3, condition (iii) cannot be dropped: Exercise 9.2.2 gives a reversible process satisfying (i) and (ii) whose equilibrium is not a Markov field, so any argument that uses only the local form of the rates fails.
V with decidable equality; attributes at site j form a finite type N j, which may differ between sites. States are dependent functions (j : V) → N j, and is Function.update n j m. The graph is a Mathlib SimpleGraph V, so is G.neighborSet j.KellyStochasticNetworks.DetailedBalance), and "equilibrium distribution" in 9.4 is a positive distribution summing to one satisfying the equilibrium equations (KellyStochasticNetworks.FullBalance), together with its uniqueness under irreducibility. The Markov process itself is not constructed. The state space is always finite, so all sums are finite.Chapter 4 of F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) applies the product-form theory of Chapter 3 to concrete systems. Two of its results have numbered statements, and they answer two practical questions.
The first comes from the design of store-and-forward communication networks (telegraph and packet-switched data networks). Messages queue at channels; the designer chooses each channel's capacity subject to a budget, and wants to minimize the delay messages suffer. Because the equilibrium law at every channel is geometric under several different modelling assumptions (§4.1, pp. 95–96), the mean delay has a closed form, and the budget allocation problem becomes a small convex program with an explicit solution. This square-root capacity assignment goes back to L. Kleinrock's work on communication nets (Communication Nets, McGraw-Hill, 1964) and remains the textbook example of optimal design for a network of queues.
The second comes from compartmental models in biology, birth–illness–death processes and manpower planning (§4.5, pp. 113–115). Individuals enter a system as a Poisson stream and move through it independently. Equilibrium results follow from Chapter 3; Theorem 4.2 describes the transient behaviour exactly, starting from an empty system.
Capacity allocation (§4.1). A network has channels. Channel receives traffic at average rate and is given capacity . In equilibrium the number of messages at channel has the geometric law (4.1),
which requires . Its mean is . Capacity on channel costs per unit and the total budget is , giving the cost constraint (4.2)
The mean number of customers in the network is
and the feasible set is the set of with for every that satisfy (4.2). In Lean these are meanNumberInNetwork a φ and FeasibleCapacities a f F. The proof works with the Lagrangian lagrangian a f F y φ .
Compartmental model (§4.5). Individuals arrive in a Poisson stream of rate at a system of compartments that is empty at time . Let be the probability that an individual is in compartment a time after its arrival; and , since individuals may leave. Let be the number of individuals in compartment at time , and
In Lean the model is the predicate IsCompartmentModel P ν t p M T Loc, the counts are compartmentCount M Loc j, and is alpha p j t.
If , , and , then
is feasible and minimizes over the feasible set, and every other feasible has .
The proof's generating-function identity, for ,
and the theorem itself: are independent and is Poisson with mean .
Theorem 4.1 is a closed-form design rule. Every channel first receives the capacity needed to carry its traffic; the remaining budget is shared in proportion to , not to the traffic . Sizing capacity in proportion to the load, which is the obvious rule, is therefore not optimal. The same calculation applies to any network whose stations have the geometric law (4.1), for example a manufacturing job shop (p. 97). The mean number in the network and the mean time a customer spends in it are minimized together.
Theorem 4.2 is the exact transient law of a network of infinite-server queues started empty. It holds however complicated the motion of an individual is, provided individuals move independently, and letting it recovers the equilibrium Poisson law of §4.5.
Both results are classical and proved in the book. Neither is formalized on Prove2Me. The platform has the geometric equilibrium law of the M/M/1 queue (KellyStochasticNetworks.mm1_equilibrium) but not its mean, and no result on Poisson thinning or marking by independent random locations. The formal work for Theorem 4.1 is a strict-convexity and Lagrangian-sufficiency argument in . For Theorem 4.2 it is a Poisson marking theorem in measure-theoretic probability. Both pieces are reusable.
For Theorem 4.1, the book's proof sets the partial derivatives of the Lagrangian to zero. A stationary point is not a global minimizer in general, so the formal proof must show that is (strictly) convex on the open region , and it must use Lagrangian sufficiency, not first-order conditions alone. The region is open and the objective is unbounded near its boundary. Feasibility of needs , which the book leaves implicit.
For Theorem 4.2, the steps of the proof that read "conditional on " have to be carried out with measure-theoretic independence. One step averages a product over independent uniform instants. Another sums the Poisson mixture into an exponential. The last turns a factorized generating function into mutual independence of counts with Poisson marginals. Mathlib has the Poisson distribution (ProbabilityTheory.poissonMeasure) but no marking or thinning theorem, and no uniqueness theorem for multivariate probability generating functions.
Channels and compartments are indexed by Fin J; all rates, costs and capacities are real numbers.
Theorem 4.1. The statement carries the book's implicit hypotheses explicitly: , , , . Stability is part of the feasible set. The conclusion is global optimality over the feasible set (IsMinOn) together with feasibility of , plus strict optimality against every other feasible point. Uniqueness is a slight strengthening of the book's "the optimal allocation is", and it holds by strict convexity. A statement that satisfies (4.2), or that it is a stationary point of the Lagrangian, is not the theorem: those are one-line computations or the proof method, and the goal is stated as global optimality to rule them out.
Theorem 4.2. The model is pinned down as in the proof on p. 115:
"Individuals move independently" is formalized as this conditional independence. The are measurable sub-probabilities, not assumed to sum to one. The conclusion is mutual independence of the counts (iIndepFun) together with the Poisson probability mass function of each. Infinite time horizons and the point-process description of the system are out of scope.
Useful contributions: a reusable Lagrangian-sufficiency lemma for separable convex objectives under one linear constraint; a Poisson marking (colouring) theorem for finitely many colours; the multivariate generating-function uniqueness lemma for -valued random vectors.
Many optimization problems in statistics, signal processing and control are posed over sets of matrices with a constraint that makes them curved: matrices of fixed rank, matrices with orthonormal columns, symmetric matrices with a prescribed spectrum. Algorithms on such sets ("optimization on manifolds") compute a step in the tangent space at the current point, as in a vector space, and then need a rule that brings the point back to the set. A retraction is such a rule; the notion was introduced by Adler, Dedieu, Margulies, Martens and Shub for Newton's method on Riemannian manifolds (IMA J. Numer. Anal. 2002) and is the basic building block of the algorithms in Absil, Mahony and Sepulchre's monograph (Princeton, 2008). Any retraction preserves the local convergence of Newton's method, so the choice among retractions is about cost and convenience.
The most natural candidate is to project back onto the manifold: take the nearest point. Absil and Malick (SIAM J. Optim. 2012; preprint HAL hal-00651608) show in §3.1 that this projective retraction is always a valid retraction of maximal smoothness, and then compute it for fixed-rank, spectral and Stiefel manifolds. The underlying fact, that the nearest-point map onto a submanifold is locally single-valued and , is classical (the paper cites Lewis and Malick, Math. Oper. Res. 2008); the paper gives a short proof through the inverse function theorem on the normal bundle. This mission formalizes §3.1: that lemma and the resulting retraction.
Let be a Euclidean space, a finite-dimensional real inner product space, of dimension (in the paper's examples, with the Frobenius inner product). A set is a submanifold of class and dimension around if and there are an open neighbourhood of and a diffeomorphism from onto an open subset of with
The tangent space is the linear subspace of spanned by the tangent cone of at , and the normal space is . The tangent bundle and normal bundle are and , subsets of . denotes the orthogonal projector onto .
The projection of onto is the set of nearest points,
which may be empty (if is not closed) or contain several points (if is not convex).
A map from to is a retraction around (Definition 2.1) if on some neighbourhood of in it is of class , satisfies , and for .
The formal retraction predicate includes and a local submanifold chart at ; this ensures that its base point lies on .
For a submanifold () around , the map
is single-valued near in , and this single value is a retraction around .
The projective retraction is the reference retraction on an embedded submanifold: it exists for every submanifold, it has the maximal smoothness allowed by the tangent bundle, and it is the one practitioners compute first (truncated SVD for fixed-rank matrices, polar factor for the Stiefel manifold). Section 4 of the paper shows that it is moreover second order and generalizes it to projections along arbitrary smooth fields of transverse subspaces; Lemma 3.1 is the model of that argument. Lemma 3.1 on its own is a basic tool well beyond retractions: local single-valuedness and smoothness of the nearest-point map underlies the local convergence analysis of alternating projections on manifolds and the theory of prox-regular sets.
All statements here are proved results. No machine-checked proof of them is known to exist: Mathlib has the inverse function theorem, tangent cones and orthogonal projections onto subspaces, but no embedded submanifolds of a Euclidean space with their normal bundle and no nearest-point map onto non-convex sets. The mission produces these statements in Lean and invites proofs of them.
The obvious argument writes the nearest point as a critical point of on and applies the implicit function theorem. Two things break. First, existence: is not assumed closed, so a nearest point exists only because is locally closed near and points of far from are farther from than is. Second, uniqueness: critical points are not unique in general, and the implicit function theorem only describes critical points near a given one. Uniqueness needs a quantitative argument that every nearest point of lies in the region where on the normal bundle is injective. Finally, the normal bundle is itself only a manifold, whose tangent space at must be identified before the inverse function theorem applies; this is milestone (3.3).
The ambient space is any type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]; is Module.finrank ℝ E, and are natural numbers with stated as a hypothesis (so that in ℕ is honest). The paper's standing assumption " is a submanifold of class () and dimension " enters only as the local hypothesis IsSubmanifoldAt k d M xbar, exactly as Lemma 3.1 and Proposition 3.2 state it ("around "). The chart is an OpenPartialHomeomorph onto EuclideanSpace ℝ (Fin n), in both directions, with 0-based coordinates. No closedness of is assumed, because the paper does not assume it.
The projection is the platform predicate IsMetricProjection M x z ( and for all ); single-valuedness is stated as equality of the set of such with a singleton, which asserts existence and uniqueness. A formalization that only states "some selection is ", or uses (satisfied by the empty set), would drop the main claim and is ruled out. The tangent space is the span of Mathlib's tangentConeAt; "class on a neighbourhood in " is ContDiffOn on with open; is a HasFDerivAt statement on the normed space ; is Submodule.starProjection.
A complete development needs: the tangent space of a slice submanifold equals the image of the chart's derivative, the normal bundle as a manifold, an inverse function theorem on it, and compactness of for small . These are reusable for the other missions of this series (fixed-rank, spectral and Stiefel manifolds, and the retractor construction of Section 4), and contributions of such general lemmas as intermediate theorems are welcome.