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?
In a road or communication network where each unit of traffic picks its own route, the outcome is a Nash flow (Wardrop equilibrium): no traffic can lower its own latency by switching paths. It is well known since Pigou (1920) that such selfish routing can be inefficient: the total latency of a Nash flow may exceed that of the best centrally planned flow. The ratio between the two, maximized over a family of instances, is the price of anarchy. Network designers, transportation economists and computer scientists use it to decide when central coordination (tolls, routing protocols) is worth its cost.
Timeline:
A network is a finite directed multigraph ; parallel edges are allowed. There are commodities; commodity has a source , a sink , a rate , and at least one simple – path. A flow assigns a nonnegative amount to each simple – path ; it is feasible if for every . The edge flow is .
Each edge carries a latency function , nonnegative, differentiable and nondecreasing. The latency of a path is and the cost of a flow is . A feasible flow of least cost is optimal. A flow is a Nash flow (Definition 2.1) if moving any amount of commodity from a used path to another path yields a flow with . The ratio between the cost of a Nash flow and of an optimal flow is .
A latency function is standard if is convex on ; its marginal cost is . A class of latency functions is standard if it contains a nonzero function and all its members are standard. The anarchy value of a standard is
and . It is the worst ratio in a Pigou-type network: two parallel links, one with a constant latency and one with . Finally, is the network with one source, one sink and two edges from source to sink.
For a standard class that contains the constant functions , , with the set of all instances with latencies in and the single-commodity instances on ,
It is stated as two parts: every ratio of a feasible Nash flow to a feasible flow of positive cost, in any network with any number of commodities, is at most ; and every value below is exceeded by such a ratio on .
The milestones follow the paper's proof: the edge form of the cost (§2.1), the shortest-path characterization of Nash flows (Proposition 2.2), the cost of a Nash flow (Proposition 2.3), monotonicity and continuity of marginal costs (§2.3), existence of (§3.1), Lemmas 3.5–3.7, the upper bound (Theorem 3.8) and the two-link lower bound (Lemma 4.1).
Lemma 4.4 and Theorem 4.5 replace "contains the constants" by diversity (for each some has ) and show that networks of parallel links are worst possible among single-commodity instances. Proposition 5.1 computes the price of anarchy of polynomials of degree at most with nonnegative coefficients:
The theorem reduces a combinatorial question (the worst instance over all networks and all commodity structures) to a one-dimensional calculus problem: computing for the steepest functions of the class. It yields exact prices of anarchy for polynomial latencies (Proposition 5.1), for M/M/1 delay functions and others, and it shows that the inefficiency of selfish routing is never caused by the interaction of commodities or by network structure: Pigou's two-link example already captures it. The bound has become a standard reference point for later work on smoothness arguments, tolls and Stackelberg routing.
The result is proved; it has not been formalized. This mission produces a machine-checked model of nonatomic multicommodity routing on directed multigraphs (simple paths, path flows, Nash flows in the paper's own definition, marginal costs), the general upper bound for an arbitrary standard class, and the matching lower bound in two-link and parallel-link networks. Alternative arguments, such as the variational-inequality proof of Correa, Schulz and Stier-Moses, are equally welcome as proofs of the same statements.
The obvious approach, following Roughgarden–Tardos for affine latencies, scales the Nash flow down by a constant factor and shows the result is optimal for reduced rates. For nonlinear latencies no single factor works. The paper's proof scales each edge by its own factor , which produces a pseudoflow that obeys no conservation constraints, and the augmentation from it to an optimal flow must then be priced edge by edge. Formally, the scaling factors are solutions of that need not be unique, marginal costs are one-sided derivatives at , and the anarchy value may be infinite, so every comparison has to be valid in the extended reals.
All declarations live in PoAIndep.Topology. A network is a pair of finite types with endpoint maps src tgt : E → V; parallel edges are free. Simple paths are nonempty edge lists with a repetition-free vertex sequence, so commodities with are excluded. A flow stores one finitely supported path flow per commodity. Latency functions are maps whose properties (nonnegative, differentiable, nondecreasing; for standard ones, convex) are required on only, and is the derivative within . The standing assumptions of §2.1 (, , latency properties) are fields of the Instance structure; standardness of the latencies enters through the class .
The anarchy values live in ; is the supremum over all admissible pairs , which equals the page's value because the expression does not depend on the choice of . Instead of , which presupposes existence and uniqueness of the Nash cost (Proposition 2.4, cited by the paper), statements bound for every feasible Nash flow and every feasible with . The networks and are instances of the general model, so holds literally.
The Nash condition is Definition 2.1, not the shortest-path characterization, and the cost is the path sum, not the edge sum; both alternatives would make milestones trivial. The goal is not satisfied by the two-link lower bound alone: its upper part quantifies over every network and every number of commodities.
Reusable beyond this mission: the routing model, Nash flows, marginal costs and the anarchy value, which also underlie the companion paper on the bound and later work on tolls and Stackelberg strategies. Proofs of any milestone, and supporting lemmas about convex functions with one-sided derivatives, are welcome.
A Markov decision process (MDP) is evaluated by solving a linear fixed-point equation built from its transition probabilities. In practice those probabilities are rarely known exactly: they are estimated from data, elicited from experts, or obtained by aggregating the states of a larger model, and each estimate comes with an error band. Givan, Leach and Dean (Bounded-parameter Markov decision processes, Artificial Intelligence, 2000) replace each transition probability by a closed interval and ask what can still be said about the value of a policy. Their answer for a fixed policy is an interval value: at each state, the smallest and the largest expected discounted reward the policy can obtain over all exact MDPs consistent with the intervals.
The same model reappears under other names. Robust MDPs with rectangular uncertainty sets (Nilim and El Ghaoui, Operations Research, 2005; Iyengar, Mathematics of Operations Research, 2005) take the pessimistic end of the interval, and optimistic model-based reinforcement learning (for example UCRL-type algorithms) takes the optimistic end over a confidence set. Interval transition models are also used to bound the error of state aggregation. In all of these, the basic computational question is how to evaluate a fixed policy against a whole family of MDPs at once.
Fix a finite set of states and a finite nonempty set of actions. An exact MDP has transition probabilities , each row a probability distribution, a reward per state, and a discount rate . A policy is a map . Its value function is the expected discounted cumulative reward of the Markov chain with transition matrix :
On the space of value functions , with the sup norm , the value-iteration operator is , and is the same with the action in place of . An operator on is a contraction mapping if for all and some .
A bounded-parameter MDP (BMDP) gives intervals with , a reward and a discount rate . An exact MDP belongs to if it has the same and and every transition probability lies in its interval. The interval value of a policy (Definition 3) is
Interval policy evaluation acts on an interval value function by
with lower and upper bound maps .
For the optional part, interval value iteration adds a maximization over actions: and take, at each state, the largest of the candidate intervals for the lexicographic orders (upper end first) and (lower end first). For a value function , and are the actions maximizing and , and , .
For every BMDP, every policy , and every interval value function with ,
The limit is the interval value of Definition 3, an extremum over infinitely many MDPs; nothing about the starting point is assumed beyond its being an interval value function.
The result. The interval value is defined as a minimum and a maximum over a continuum of MDPs, and there is no a priori reason it should be computable by a dynamic program. The goal says it is: one operator, whose per-state step is a small linear program over a box intersected with a simplex, iterated from any start, converges to both ends of the interval simultaneously. The pessimistic end is the robust value of the policy under rectangular uncertainty, so the goal is also a policy-evaluation theorem for interval-rectangular robust MDPs; the optimistic end is the value used by optimism-based exploration. Theorem 11 is the bridge between the "game" definition (nature picks the MDP) and the fixed-point characterization; Theorem 13 is the corresponding first step for the optimal interval values of the companion mission.
Formalizing it. The results are proved in the paper (2000), with Theorem 11 relying on the existence of a single member MDP that is -minimizing at every state simultaneously (the paper's Theorem 7). No machine-checked version of the BMDP model or of these results is known. Nearby statements formalized elsewhere concern other models: robust MDPs with costs and general row sets, and optimistic Bellman equations over compact confidence sets. This mission produces the BMDP model and its interval operators, the contraction and fixed-point theorems, and the convergence theorem, all stated against the member-MDP definition of .
The contraction estimates (Theorems 10 and 13) follow the familiar pattern for Bellman operators, with the extra point that the minimum or maximum over the infinite family must be attained. The real difficulty is Theorem 11. The obvious argument compares with state by state; but is a minimum taken separately at each state, possibly by a different MDP at each state, and need not a priori be the value function of any single member MDP. Without a member MDP that is minimizing at all states at once, the inequality does not follow. Establishing that simultaneous minimizer is the central step.
All statements live in the namespace BoundedParamMDP.IntervalEval. The exact MDP, the BMDP, its member MDPs, , , and Definition 3's , are the shared definitions BoundedParamMDP.Optimal.MDP and BoundedParamMDP.Optimal.BMDP used by the companion mission, so its theorems apply to the same objects. Conventions:
Q → A.F p α q , rows nonnegative and summing to , a state reward R, and the discount rate as a field. Rewards are tight (the paper's footnote 3): members share the BMDP's R and γ.Member B; all quantities are bounded, so these are the genuine values (and attained, by the paper's Lemma 1).(V↓, V↑) of functions Q → ℝ. The operators are defined on all pairs; the goal assumes as the paper's interval notion, though the conclusion does not need it.Q → ℝ (the sup norm (4)); convergence of pairs is in the product topology. A contraction mapping is "there exists ", as on p. 6; the modulus is not fixed to .A trivializing formalization is excluded: the limit in the goal is Definition 3's infimum and supremum over member MDPs, not the fixed point of , so the goal is not Banach's theorem alone; and the member type is nonempty for every BMDP, so the infima and suprema are not the junk value .
The proof of Theorem 11 uses the paper's Lemma 1 (attainment in the order-maximizing family), Theorem 3 ( is the unique fixed point of ), Theorem 6 (comparison principle) and Theorem 7 (existence of -minimizing and -maximizing MDPs). These are milestones of the companion mission Bounded-parameter Markov Decision Processes 1 and are not restated here. The Banach fixed-point theorem is Mathlib's ContractingWith. Contributions welcome: proofs of the milestones, a reusable lemma on the attained minimum of a linear function over a box intersected with the simplex, and the order-maximizing construction itself.
Boosting combines many weak classifiers into a strong one by refitting, again and again, to reweighted data. AdaBoost (Freund and Schapire, 1997) and its confidence-rated variant Real AdaBoost (Schapire and Singer, 1999) were introduced through the theory of online learning. Friedman, Hastie and Tibshirani (2000) recast them as stagewise fitting of an additive model by minimizing the exponential criterion , where is the class label. In that view Real AdaBoost minimizes exactly over the new term at each stage.
The same paper proposes Gentle AdaBoost (Algorithm 4, §4.4), which replaces the exact minimization by a single Newton step. Its increments are bounded, and the authors report that it often matches or beats Real AdaBoost and LogitBoost, especially when numerical stability is an issue. The paper's stagewise view of boosting led on to gradient boosting (Friedman, 2001). This mission formalizes the paper's justification of the algorithm: its population version takes Newton steps on .
A feature ranges over a measurable space . The label takes values in , and has a joint probability law on . Conditional expectations given , written , are integrals against the conditional law of given , and .
The algorithm maintains a current additive fit , starting from . For a new term , the conditional exponential criterion is
a function of the real number for each fixed .
The weight attached to an observation is . The weighted conditional expectation (p. 347) is
and are the weighted class probabilities.
Gentle AdaBoost (Algorithm 4) repeats three steps: fit by weighted least squares of on with weights , update , and update with renormalization. In the population version the weighted least-squares fit is the weighted conditional mean, so one step is
For comparison with LogitBoost the paper uses the symmetric logistic and the 0/1 response .
For every , with and : is the first derivative of at , is the second derivative, , and
This is the paper's Result 4, "the Gentle AdaBoost algorithm (population version) uses Newton steps for minimizing ", in the precise form its Derivation gives.
The result. Result 4 places Gentle AdaBoost alongside LogitBoost (Result 3) as a Newton method. Real AdaBoost (Result 2) and Gentle AdaBoost minimize the same criterion, but one solves the stagewise problem exactly and the other takes one Newton step. Displays (37) and (38) then put Gentle AdaBoost and LogitBoost in the same coordinates and . The two updates are close when . LogitBoost's update can be unbounded as approaches or , while Gentle AdaBoost's always stays in . This is the paper's explanation for the stability of Gentle AdaBoost.
Formalizing it. The result is proved on the page by direct calculation. No machine-checked version is known to exist. The mission produces a formal account of the population algorithm on an arbitrary joint law, through Mathlib's disintegration of a measure on , and of the Newton-step identity. It also gives a reusable treatment of the paper's weighted conditional expectation in the conditional-kernel language. The same objects appear in the other missions of this series (Real AdaBoost, LogitBoost).
The calculus on the page is short. The work is in the setting. "Differentiate the criterion with respect to " has to mean differentiating an integral against the conditional law of given with respect to a parameter, with the derivative established, not read off a formula. A plain derivative equation proves nothing at a point where the function is not differentiable. The second derivative needs the first derivative as a function of , not only its value at . The Newton step divides by , so its positivity must be established before the identity has content. Finally, (37) requires recovering from the conditional law being a probability measure, and the second equality in (37) holds only for the symmetric logistic.
Labels are Bool (true for , false for ); is sgn b and is ystar b. The joint law is ν : Measure (X × Bool) with [IsProbabilityMeasure ν], and is the Bochner integral against ν.condKernel x, a probability measure on the two-point type. Every statement holds for every . No almost-everywhere qualifier, integrability or measurability hypothesis is needed, and none is added. The kernel is unique only almost everywhere, and the statements hold for the chosen version. They use only the fact that it is a Markov kernel. The definitions file fixes the conditional criterion condCritAt, the weighted conditional expectation wCondExp with weight , the weighted class probabilities wProb, the population step gentleStep, and the symmetric logistic symLogistic. All of these are written exactly as on the page.
Derivatives are HasDerivAt statements. The second derivative is the derivative at of an explicit first-derivative function, which is itself shown to be the derivative at every point. is a conclusion of the goal, never a hypothesis. Several formalizations would trivialize the claims and are ruled out. The criterion is the integral against the conditional law, not a closed form in a free parameter . No bare deriv equation and no division by an unproved nonzero quantity is used. The logistic is the symmetric , not , which differs by a factor in and makes (37) false. The sample version of Algorithm 4 (trees, terminal-node averages) is not formalized.
Welcome contributions: proofs of the milestones, general lemmas on differentiating integrals over finite label spaces with respect to a parameter, and lemmas connecting condKernel on Bool with the closed forms in .
Scheduling jobs on unrelated parallel machines to minimize the total weighted completion time, the problem written in the three-field notation, is one of the basic NP-hard models of machine scheduling. Each job may take a different time on each machine, as when heterogeneous processors, plants or crews serve the same pool of tasks, and the objective rewards finishing important jobs early. For a single machine the problem is solved exactly by Smith's ratio rule (Smith, 1956). With several unrelated machines the problem is strongly NP-hard and the question is how close to the optimum a polynomial-time algorithm can come.
Timeline of the guarantees for :
There are jobs and machines . Job has a weight and a processing time on machine . A schedule assigns each job to one machine and orders the jobs on every machine; the completion time of a job is the time at which it finishes when each machine works without idle time.
For a fixed assignment, Smith's ratio rule orders each machine optimally. Fix for each machine the total order iff , ties broken by index. Under an assignment the completion time of is
and the problem is to minimize over all assignments.
With indicating that runs on , the problem is the integer quadratic program (IQP) with objective
where is symmetric with entry at for and zero across machines and on the diagonal. Relaxing to with gives (QP). Raising the diagonal gives the convex program (CQP), with objective . Adding the lower bound gives (CQP′):
Randomized rounding of a fractional sends job to machine with probability , the choices being pairwise independent across jobs, and then orders every machine by .
For every instance with , :
The first part makes a lower bound on the optimum. The second is Lemma 2.8. Together they are Corollary 2.9 and the value guarantee of the -approximation.
In attack order:
The result gives a -approximation for from a relaxation with only variables, without time indexing, so its size does not depend on the processing times. The same convexification, adapted to time slots, yields the factor 2 with release dates (§3 of the paper). The equality of Theorem 2.1 makes the analysis exact: the loss of rounding is exactly the gap between and the convex objective. The relaxation also bounds the power of preemption (§4), and for identical machines it connects scheduling to Max--Cut (§6).
All these results are proved in the paper; none is known to be formalized. A formal development adds:
Two steps resist the obvious approach.
Positive semidefiniteness. alone is indefinite: two jobs with unit data give the block . Positive semidefiniteness of holds only because the jobs on each machine are ordered by Smith's ratio. A generic matrix argument that ignores this ordering fails, and the "only if" half of Lemma 2.4 needs a specific family of instances.
Exact expectations under pairwise independence. Theorem 2.1 is an equality that uses only the one- and two-job marginals. A proof that silently assumes full independence of the choices proves a different statement. A proof that drops the product condition on pairs is false: with correlated choices the expected value differs from .
Jobs and machines are Fin n and Fin m; vectors in are functions on Fin m × Fin n and is a Matrix over that type. The order is cross-multiplied (, or equality and ), which equals the page's ratio definition because .
Standing assumptions of p. 2 are hypotheses of every theorem: and . Hypotheses added relative to the page:
Optimum. The scheduling optimum is the minimum of over assignments, by Smith's rule (p. 7, cited by the paper, not reproved). "Within a factor of the optimum" is stated as a bound against the value of every assignment, so no optimum is presupposed.
Rounding. Randomized rounding is any nonnegative weight of total mass 1 on assignments, with and for . The product weight satisfies this.
Not formalized. Polynomial running time, solvability of (CQP′) within additive error (ellipsoid method), and derandomization by conditional probabilities. Theorem 2.10 is formalized as the existence of an outcome in the support of the rounding with the guarantee.
Trivializing formalization ruled out. A bound for an arbitrary number says nothing about schedules. The goal therefore also states that every schedule is feasible for (CQP′) at its own value, so is a genuine lower bound on the optimum.
Contributions welcome. A complete development needs:
The rounding calculus and the PSD lemma are reusable for §§3–4 of the same paper. Alternative proofs of Lemma 2.4 are welcome.
Minimizing a submodular set function is one of the central tractable problems of combinatorial optimization. Minimum cuts in graphs and hypergraphs, matroid intersection and partition, the rank of a matroid union, and many problems in facility location, image segmentation and machine learning are special cases or subroutines of it. The question is algorithmic: given only a value oracle for , find a set with using a number of operations bounded by a polynomial in alone, independent of the size of the values of (strongly polynomial).
Timeline.
Schrijver's algorithm is the one usually taught. Its proof uses only the greedy vectors of , a reachability digraph and a lexicographic potential.
Let and let be a real function on all subsets of that is submodular:
normalized so that . For and write . The base polytope is .
For a total order on let . The greedy vector of is . A lower ideal of is a set closed under taking -smaller elements. The interval is . For , the order is obtained from by moving to the position just before . The vector is the incidence vector of .
The algorithm keeps a point with and ; initially for an arbitrary order. It forms the digraph , where , and the sets and .
For every submodular with :
Part (iii) is the opening claim of §5 (p. 352), and part (i) is display (16) (p. 351). Part (ii) states that the description of §4 can always be carried out, and it keeps (iii) from holding vacuously.
In order: the diminishing-returns inequality (9); on lower ideals and (§2); the comparison (8) of with ; the subroutine (12); the Case 1 certificate (16); existence of a Case 2 iteration (§4, p. 352); the location (22) of new arcs; monotonicity (20) of distances; and the lexicographic decrease (21) of while stays fixed.
The result. The theorem gives a submodular minimizer after a number of iterations bounded by a polynomial in . Each iteration makes polynomially many oracle calls and arithmetic operations, so the algorithm is strongly polynomial. The same exchange-and-potential scheme underlies later improvements (Fleischer–Iwata's push-relabel variant, Iwata–Orlin, Orlin's bound). Section 6 of the paper, the companion mission, transfers the result to submodular functions on ring families.
Formalizing it. The result is proved and has been in textbooks for twenty years. It has no machine-checked proof that we know of, in Lean or elsewhere, and Mathlib has no submodular minimization. A complete development yields a verified correctness and termination proof for a nontrivial combinatorial algorithm on the base polytope. It also yields reusable facts about greedy vectors and lower ideals, and a worked example of a lexicographic-potential termination argument.
Correctness (16) is short once on lower ideals is available. The difficulty is termination. A single iteration can increase at and decrease it at , and it adds new orders and so new arcs. Neither nor need improve monotonically, and the obvious potentials fail. The argument needs the precise structure of the new arcs (22): every new arc lies inside the interval of , and that gives both the monotonicity of distances (20) and the strict lexicographic decrease (21). The choice rule for and ("largest") is what makes (21) hold. An arbitrary choice can cycle. Well-definedness also takes work: it combines (12) with a Carathéodory reduction over the hyperplane .
Fin n and subsets are Finset (Fin n). Values are real; the paper allows any ordered field. "Largest" in the choice of and is the order of Fin n.IsMoved). A state is a list of (order, weight) pairs.NonmonotoneSubmod.Shared.Submodular) and are the paper's standing assumptions of §2 and §4. Milestones that do not need omit it.Step that admits every choice the paper leaves open: any subroutine output , any maximizing index, and any Carathéodory reduction. The reduced decomposition may only use orders (), each at most once, and only when .Step relation that is never satisfiable would make the bound vacuous. Part (ii) of the goal rules this out, and the goal does not mention , , or the matrix of §3.Most stochastic programs cannot be solved as stated, because the objective is an expectation over a distribution that is high-dimensional, continuous or known only through a simulator. The standard remedy is the sample average approximation (SAA), also called the Monte Carlo or sample-path method: draw an i.i.d. sample, replace the expectation by the sample mean, and solve the resulting deterministic problem. The method is the workhorse of two-stage stochastic programming, and its statistical behaviour decides how large a sample a practitioner must draw.
For smooth problems with a unique optimum, the classical theory says the SAA solution converges at rate and is asymptotically normal. Shapiro and Homem-de-Mello (SIAM J. Optim. 11 (2000)) observed that two-stage linear programs with finitely many scenarios behave quite differently: their optimal solutions are typically sharp, the objective grows linearly away from the minimizer, and then the SAA problem does not just approach the true solution but returns it exactly once the sample is large enough. This mission formalizes that first observation, Theorem 2.1 of the paper. Its sequels in the same series show that the probability of failure decays exponentially in (mission 2) and extend the picture to multiple optimal solutions in the finite polyhedral case (mission 3).
Let be a probability measure on a sample space , let be a set of feasible decisions, and let be a cost function. The true problem (1.1) is
Let be an i.i.d. sequence of random elements of with law , defined on some probability space . The approximating problem (1.2) uses the first of them:
For a function on write ; the optimal set of the true problem is . The directional derivative of at in direction is ; for the cost of a single scenario it is written . The tangent cone to a convex set at is the closure of .
Assumption (A). The true problem has a unique optimal solution , i.e. , and there is with
An optimal solution with this linear growth is a sharp minimum.
A statement holds w.p.1 for large enough if for -almost every sample path there is , depending on the path, such that it holds for every .
Suppose (i) is convex for every ; (ii) is well defined and finite valued; (iii) is closed and convex; (iv) Assumption (A) holds. Then w.p.1 for large enough
that is, the approximating problem has a unique optimal solution and .
The result. Theorem 2.1 says that for convex stochastic programs with a sharp optimum, SAA is not an estimator with sampling error in the usual sense: almost every sample path eventually produces the true solution itself. This is the qualitative statement behind the paper's main quantitative result (Theorem 3.1, mission 2 of this series), that the probability of not obtaining the exact solution decays like . Together they explain why, in two-stage linear programs with finitely many scenarios, modest sample sizes often recover the optimal first-stage decision exactly, a phenomenon the paper documents numerically. The proposition on directional derivatives (Proposition 2.2) is of independent use: it is the almost-sure uniform convergence of first-order information of a sample average, which recurs in the asymptotic analysis of SAA estimators.
Formalizing it. The theorem is proved in the paper; nothing here is open. Machine-checked SAA theory is thin: the existing platform material treats uniform convergence of the objective on compact sets, not directional derivatives or exactness at sharp minima. A complete development supplies, on top of Mathlib, the strong law of large numbers applied to directional derivatives of convex integrands, the passage from pointwise to uniform convergence for convex functions, and the characterization of sharp minima by directional derivatives on the tangent cone. Each of these is reusable well beyond this paper.
The obvious argument fails at the step from convergence to exactness. Strong consistency of SAA ( w.p.1) says nothing about equalling ; for a smooth objective it never does. Exactness has to come from a first-order condition at that holds with a margin, and that margin must be transferred to uniformly over all tangent directions at once, not one direction at a time, since there are uncountably many directions and each carries its own null set. The second difficulty is that and are typically nonsmooth (piecewise linear in the motivating examples), so the first-order objects are one-sided directional derivatives, and differentiation under the integral sign, in its usual smooth form, does not apply to them.
EuclideanSpace ℝ (Fin m). The sample is one infinite i.i.d. sequence on a separate probability space : each is measurable with law , and the family is mutually independent. uses the first terms (0-based in Lean). "W.p.1 for large enough" is ∀ᵐ s ∂Q, ∀ᶠ N in atTop, …; a fresh sample for each is not used.limUnder along ), used only for convex finite functions, where the limits exist. Optimal sets are defined directly as argmin sets, without infima.posTangentConeAt, the cone of limits of with ; for convex it is the closure of . Mathlib's tangentConeAt ℝ, which allows negative scalings and is symmetric, is not the paper's cone and is not used.Metric.hausdorffEDist. Subdifferentials use the published definition ShorNonsmooth.Subdiff.subdifferential.Contributions welcome: proofs of any milestone; in particular the convex-analysis lemmas (milestones 1, 2 and 4) need no probability, and (2.5)–(2.6) need only Mathlib's strong law.
The scheduling problem asks for a nonpreemptive schedule of jobs on unrelated parallel machines, each job with a machine-dependent processing time and a release date, so that the total completion time is minimal. It is NP-hard, and the question that remains is how well it can be approximated in polynomial time. Positive results include the 2-approximation of Skutella (J. ACM 2001), based on a convex quadratic relaxation. This mission covers the negative side, from §7 of the same paper: the problem has no polynomial-time approximation scheme unless P = NP.
The standard route to such a statement is an L-reduction (Papadimitriou and Yannakakis 1991) from a problem already known to be MaxSNP-hard. MaxSNP-hard problems have no approximation scheme unless P = NP, by the PCP theorem (Arora et al. 1998).
Timeline.
An instance of 3-OCCURRENCE MAX3SAT has variables and clauses. Each clause is a set of one to three literals (a variable or its negation ), and each variable occurs at most three times in total. A truth assignment gives each variable the value true or false and satisfies a clause when one of the clause's literals is true. denotes the number of satisfied clauses, and .
The scheduling instance has jobs and machines.
A schedule gives every job a machine and a start time , with no two jobs on one machine overlapping. Its value is the total completion time . The truth assignment sets true exactly when the v-job of runs on the true machine. is the minimum of over feasible schedules.
has an optimal schedule , and
for every feasible schedule . These are the two conditions of an L-reduction, with constants and .
The result. The two inequalities are what an L-reduction requires. Combined with the MaxSNP-hardness of 3-OCCURRENCE MAX3SAT, they show that is MaxSNP-hard (Theorem 7.2, due to Hoogeveen, Schuurman and Woeginger), and therefore has no polynomial-time approximation scheme unless P = NP. Together with the constant-factor algorithms of the earlier sections of the paper, this places the problem in APX but outside PTAS. The identity of Lemma 7.1 b) is exact, so the reduction transfers solutions in both directions with no loss beyond the affine shift .
Formalizing it. The result is proved, on paper, by both the 1998 and the 2001 reductions. As far as the platform's corpus shows, neither is machine-checked. This mission produces a checked version of the combinatorial core of Skutella's reduction: the exact relation between optimal schedules of and optimal truth assignments of , and the two L-reduction constants. A Lean model of 3-OCCURRENCE MAX3SAT and of nonpreemptive schedules with release dates and machine eligibility is a by-product.
The obvious argument is the paper's intuition: given a truth assignment, a c-job can start at time without conflicting with a v-job exactly when its clause is satisfied. That is not enough for Lemma 7.1 a), which concerns every feasible schedule. In an arbitrary schedule a v-job may be delayed so that c-jobs of unsatisfied clauses run before it on its machine, and v-jobs and c-jobs may start at arbitrary real times. To compare such a schedule with a normalized one, its total completion time has to be bounded from below by . The bound depends on the occurrence limit of three, which caps how many c-jobs can share a machine with a given v-job; without that limit Lemma 7.1 a) is false. Lemma 7.1 b) also needs the existence of an optimal schedule, which the paper takes for granted.
Variables and clauses are Fin n and Fin m; here and count variables and clauses, not jobs and machines as in the rest of the paper. A literal is a pair (x, b) with b = true for and b = false for , and a clause is a Finset of literals. Jobs are Fin n ⊕ Fin m and machines Fin n × Bool. Infinite processing times are encoded by an eligibility relation. Start times are real numbers, and is a real number; and are natural numbers cast to the reals, so no natural-number subtraction occurs. is never a primitive: statements assert, or assume, a feasible schedule that is no worse than every feasible schedule.
Two conventions are fixed that the page leaves implicit:
Zero-length jobs need a precise non-overlap rule. Two distinct jobs on one machine must satisfy or . Under this rule a c-job at time conflicts with a v-job running over , but several c-jobs may share a start time. Reading jobs as half-open intervals would let a zero-length c-job sit inside a v-job, so every clause would count as satisfied: that formalization is ruled out.
Not formalized: MaxSNP, MaxSNP-hardness and Theorem 7.2's statement itself; the definition of an L-reduction as a pair of polynomial-time maps; the polynomial running time of and ; the weighted variant for in the last paragraph of §7, which the paper does not prove. Contributions are welcome on the counting facts, on a normal form for schedules of (v-jobs at time , c-jobs at time or ), and on the existence of optimal schedules.
A dispatcher assigns each arriving job to one of servers. Sending it to a uniformly random server is simple but produces long queues near capacity; sending it to the globally shortest queue requires full state information. The power of choices sits between the two: each job samples servers at random and joins the shortest of them. Mitzenmacher's analysis of this supermarket model (IEEE TPDS 12(10), 2001) together with the balls-into-bins result of Azar, Broder, Karlin and Upfal (SIAM J. Comput. 29(1), 1999), established that a second random choice changes the behaviour of the system qualitatively. The idea underlies load balancers, hashing schemes and distributed schedulers.
This mission formalizes the paper's quantitative statement of that improvement in heavy traffic, the regime where the arrival rate per server approaches the service rate .
Customers arrive as a Poisson stream of rate with , service times are exponential with mean , and each customer joins the shortest of queues sampled uniformly with replacement. As the fraction of queues with at least customers follows a deterministic limiting system with fixed point . Corollary 2 of the paper shows that, for , the expected time a customer spends in that limiting system converges to
With a single choice the system is independent M/M/1 queues, and the expected time is
This mission takes these two formulas as its definitions; the limiting system itself and the convergence to are the subject of the companion mission (part I). The auxiliary function of Lemma 3 is
Throughout, is an integer and logarithms are natural.
The goal is a statement about the shape of the growth, not a constant: it pins the leading behaviour .
Theorem 4 makes "exponential improvement" precise. With one choice the expected time grows like as the load approaches capacity; with choices it grows like . It also quantifies the diminishing return of extra choices: going from to only divides the leading term by , while going from one choice to two changes its order. These constants are the benchmark against which later heavy-traffic analyses of join-the-shortest-of- policies are compared.
The result is proved in the paper (the limit clause; see Difficulty for the other clause). No machine-checked version is known to exist. The formalization yields a self-contained Lean development of the lacunary series near and of the base- product identity, both of which are classical analytic facts with uses outside queueing (lacunary power series, digit expansions).
The obvious approach compares with an integral, but the terms are not monotone images of a smooth function of a continuous index in a way that controls the error uniformly as : the number of terms close to grows like and each of them contributes nearly , so the error terms are of the same order as the quantity being measured. The difficulty is to obtain matching upper and lower bounds with constants tending to , uniformly as . Passing from Lemma 3 to Theorem 4 additionally requires controlling the change of variable inside the logarithm.
Theorem 4 as printed also contains a first clause, for all . It is false as printed near : while . The paper does not prove it, and this mission does not pose it.
lam), a natural number with the hypothesis on every statement. , and are real-valued definitions in one definition file.tsums; they converge for . Outside that range Lean's conventions (a divergent series sums to , , for ) produce meaningless values, so every statement either restricts to or or is a limit along .𝓝[<] 1; the limit uses Real.log.HasProd (unconditional convergence of finite subproducts), which for factors is the same as convergence of the partial products.Boosting combines many weak classifiers into a strong one by refitting, round after round, to a reweighted version of the training data. Freund and Schapire's AdaBoost was introduced as a procedure, with guarantees on the training error, and for several years it was not clear what statistical model it fitted. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) answered this by showing that boosting is stagewise additive modelling: each round adds one term to an additive function so as to improve a population criterion.
Section 4.3 of that paper takes the step from interpretation to design. If boosting is stagewise fitting of an additive logistic model, one can choose the criterion directly: the Bernoulli log-likelihood. The resulting procedure, LogitBoost (Algorithm 3), fits at each round a weighted least-squares regression to a working response, exactly as iteratively reweighted least squares fits a logistic regression. Result 3 states that this is no accident: in the population, LogitBoost's update is a Newton step on the expected log-likelihood. The same Newton reading reappears in gradient boosting with logistic loss, where each terminal node of a tree takes one Newton step (Friedman 2001).
Timeline:
Let be a measurable space of features and let be a probability measure on , the joint law of a feature and a 0/1 response . Write for the conditional expectation given , an integral against the regular conditional distribution of given .
A current fit is a function . The symmetric logistic model (30) represents by
For an update , the expected log-likelihood (31) is
whose integrand is the Bernoulli log-likelihood of under the model.
For a positive weight , the weighted conditional expectation is . LogitBoost (Algorithm 3), population version, computes the working response and weight
fits (the population weighted least-squares regression of on ), and updates .
Fix and let . Then has first derivative and second derivative at ,
, and the population LogitBoost update equals the Newton update:
The result. Result 3 explains what LogitBoost computes: a stagewise Newton–Raphson ascent of the expected Bernoulli log-likelihood, one coordinate at a time. It makes the working response and the weights of Algorithm 3 the score and curvature of the likelihood, and reduces each round to a weighted least-squares problem (36) that any regression method can solve.
Formalizing it. The result is proved on the page by a short calculation, and no machine-checked version exists. The mission produces a formal account of the population algorithm on an arbitrary joint law, with conditional expectations taken through a regular conditional distribution, the derivatives stated with differentiability, and the Newton step identified exactly, including the constants , and that the symmetric parametrization forces.
The algebra is short; the formal content is in keeping every object honest. The derivatives are of a conditional expectation in a parameter, so differentiation must pass through the integral against the conditional law. The second derivative needs the first derivative as a function of , not only its value at . The Newton step divides by , which must be shown nonzero from rather than assumed. A tempting shortcut, replacing the conditional expectation of the log-likelihood by its closed form in a free probability parameter, removes the joint law from the statement and is ruled out.
Bool, with and . The joint law is a probability measure ν on X × Bool; is the integral against Mathlib's ν.condKernel x. Every statement is for every , conditional on as in the Derivation; because the label space is finite, no integrability or measurability hypotheses are needed.HasDerivAt, never with deriv, which returns at non-differentiable points; is a conclusion, so the division in the Newton step cannot silently return .Contributions welcome: differentiation of finite conditional expectations in a parameter, and derivative facts for the symmetric logistic, both reusable across the other missions of this series.
The Learning with Errors (LWE) problem, introduced by Regev in On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324), asks to recover a secret vector from noisy inner products . The noise is drawn from a periodic normal distribution on the circle : a centred normal variable reduced modulo . LWE has since become the main hardness assumption of lattice-based cryptography, including the post-quantum standards built on it.
Regev's reductions repeatedly need to compare and for nearby parameters, for instance when the noise parameter is known only up to a small relative error. Claim 2.2 of the paper (p. 34:16) quantifies this: the two periodic normal distributions are close in statistical distance, linearly in the relative change . This mission formalizes Claim 2.2 and the steps of its proof. The source is the published J. ACM article; the paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series.
Identify with the segment with addition modulo . For the normal density with mean and standard deviation is
(Eq. (5) in dimension one), and the periodic normal density (Eq. (7)) is its periodization
the density of a -distributed variable reduced modulo .
The statistical distance of two densities (p. 34:14) is
the integral taken over for densities on the line and over for densities on . The paper uses this normalization without a factor , so that ranges in on probability densities. In Lean these objects are RegevLWE.PeriodicGauss.nu, Psi, statDist and statDistT.
For any ,
The hypotheses and the constant are exactly as printed.
and the final evaluation
Claim 2.2 is a stability statement for the LWE error distribution. It lets an algorithm that works for one noise parameter be applied to a nearby one at a controlled cost in statistical distance, which is how Regev's reductions tolerate an approximately known parameter. It also states a quantitative fact about wrapped normal distributions, which appear outside cryptography, for example in directional statistics.
The result is proved in the paper; no machine-checked proof is known to this mission. Formalizing it produces a reusable one-dimensional toolkit: the distance between two centred normal densities, the second moment of a Gaussian in Regev's normalization, and the contraction of distance under periodization. Each of these is a building block for formalizing the rest of the paper's analysis of Gaussian noise.
The arithmetic is elementary; the work is in the analysis. The statement on involves infinite series inside an integral, and the passage from the line to the circle requires exchanging a sum over with an integral and controlling the series almost everywhere. A direct attack on termwise on does not by itself produce a bound in terms of ; the comparison has to be made on the line first. On the line, the scaling to is a change of variables in a Lebesgue integral, and the evaluation of requires Gaussian moment identities in the paper's normalization rather than Mathlib's.
Set.Ico 0 1 with Lebesgue measure; is a real tsum over , which converges absolutely for .∫⁻ ENNReal.ofReal |φ₁ - φ₂| valued in , with no factor , as on p. 34:14. Bounds are compared through ENNReal.ofReal. A Bochner integral would be on a non-integrable difference and would make any upper bound trivially true; the extended-valued integral rules this out.A standard way to coordinate a supply chain is to align incentives: contracts are written so that the retailer's profit is a fixed fraction of the whole chain's profit. With buy-back terms and wholesale price , for instance, the retailer's profit is , where is the chain's newsvendor profit. A perfectly rational retailer maximising picks the same order as a central planner maximising , so the chain is coordinated (Cachon, Supply Chain Coordination with Contracts, 2003). Laboratory subjects working under such contracts nevertheless fail to reach the coordinated outcome (Katok and Wu, Contracting in Supply Chains: A Laboratory Investigation, Management Science 2009).
Su, Bounded Rationality in Newsvendor Models, MSOM 10(4), 2008 gives a model-based explanation. A boundedly rational decision maker chooses better options more often, but not always the best. The choice probabilities depend on the actual size of the payoffs, not only on their ranking, so scaling the payoff by changes behaviour. This mission formalizes the paper's §7 result: a larger stake in the same payoff raises the expected payoff. The source is the published MSOM 2008 article.
A decision maker chooses from a decision domain to maximise a utility . Under the multinomial logit model with bounded-rationality parameter , the choice is random with density (eq. (2))
and off . Large means near-uniform choice; recovers the perfectly rational choice. In Lean this is logitDensity S u β, and the expectation of is logitExp S u β g .
Proposition 5 takes an arbitrary payoff on . Two decision makers have the same but different stakes in : their utilities are and . The resulting behavioral decisions and have densities and .
In the newsvendor instance, demand has density on , a unit costs and sells for , and the expected profit is (eq. (3))
is the smallest interval containing the support of . A retailer who receives the share of the chain's profit has utility .
If and is not almost everywhere constant on , then
The goal leaves , , and the sign of the free. Its only standing requirement is that the two logit laws and their expected payoffs exist.
For the newsvendor profit, , and shares , . Here the existence of the logit laws and the non-constancy of are proved, not assumed.
The result. Proposition 5 says that proportional incentive alignment does not coordinate a boundedly rational chain. A retailer with share makes noisier decisions than a sole owner with the same , so the chain's expected profit is strictly lower. Two consequences follow in §7. Two-part tariffs, which make the retailer the sole residual claimant (), restore coordination. Arrangements that give the retailer an effective stake in each decision may supercoordinate: the decentralised chain can earn more than a centralised but boundedly rational one. The statement applies to any logit decision problem, not only to the newsvendor.
Formalizing it. The paper's proof is short but informal. Formalization makes three things explicit. First, the existence conditions for the logit laws: when is unbounded, need not be integrable. Second, the non-constancy hypothesis that strictness needs. Third, the correction of the printed strict inequalities in (56)–(57). Corollary 2 additionally needs the newsvendor-specific facts that the logit law exists without a finite-mean assumption and that is never constant on . To our knowledge none of these results has a machine-checked proof.
The natural first attempt is to differentiate and identify the derivative as . On an unbounded domain this needs differentiation under the integral sign with uniform domination in , and a finite variance at every intermediate . Neither is among the hypotheses, which give integrability only at and . The paper instead compares the two densities directly through a single crossing. Turning that into a strict inequality between expectations needs a measure-theoretic argument that a nonnegative integrand with zero integral vanishes almost everywhere, together with the non-constancy hypothesis. For Corollary 2 the main work is analytic: proving that decays at least linearly without assuming , and that it is strictly decreasing near the right end of .
All quantities are real (ℝ). Integrals are Lebesgue/Bochner integrals, and "the density of " is logitDensity S (fun x => λᵢ * π x) β. The following conventions are committed.
Not formalized: the §7 discussion of two-part tariffs, sales rebates and supercoordination, which the paper argues rather than states.
Needed infrastructure: positivity of integrals of positive functions, set integrals over sub-level sets, and the newsvendor profit's derivative . The single-crossing lemma and the stochastic-dominance lemma apply to any one-parameter Gibbs family and are reusable beyond this mission. Proofs of the milestones, of the goal, and of Corollary 2 are all welcome.
A seller choosing inventory before demand is known faces two kinds of uncertainty: uncertainty about demand and uncertainty about how consistently the decision maker selects a profitable quantity. The classical newsvendor model treats the seller as choosing a quantity that maximizes expected profit. In the bounded-rationality model of Su (2008), the chosen quantity is random, and quantities with higher expected profit receive greater probability. This makes it possible to ask whether a systematic change in the demand density creates a systematic change in the seller's average order, even when the classically optimal order is fixed.
The question matters for interpreting inventory decisions. An order above the classical optimum might reflect the shape of demand rather than a changed selling price, purchase cost, or demand forecast. Su's Proposition 4 isolates this effect by placing the classical optimum at the midpoint of the possible demand range. The resulting shift is called rare-event bias: the average behavioral order moves toward the end of the demand range where realizations are less likely. The target and its source are the published Manufacturing & Service Operations Management article, not a numerical approximation or a later restatement. Su (2008), §6, p. 577.
Let demand be nonnegative and have a density supported on , with . Its distribution function is , and its survival function is . The midpoint and half-width of the demand range are and . The seller pays per unit ordered and sells each fulfilled unit at price , where . For order quantity , expected fulfilled demand is , and expected profit is
The optimal order maximizes over real order quantities. The mission studies the case . The paper gives the usual critical-fractile characterization ; the first supporting target below makes its midpoint consequence explicit rather than assuming it as a substitute for optimality. Su (2008), §4, p. 572, and Appendix, p. 586.
Under logit choice, the seller selects a random behavioral order from the decision domain . Its density is
and outside that interval. The parameter measures the amount of choice noise. The quantity compared with is the genuine mean . The profit, decision domain, and sign in the exponential follow equations (2)–(4) of the paper. Su (2008), pp. 571–572.
The supporting targets from the appendix identify the critical fractile at the midpoint, compare profits at reflected quantities, and express the behavioral mean through reflected choice densities:
for , followed by
These are the source's appendix displays (43)–(53). The profit comparison is strictly positive when is strictly decreasing. The goal, Proposition 4, contains both directions:
The proposition states a directional bias, rather than a formula for its size. The increasing-density direction is part of the printed proposition even though the appendix explicitly works through only the decreasing-density case. Su (2008), Proposition 4, p. 577; proof, pp. 586–587.
Holding the optimal order at removes a shift in the rational optimum from the comparison. A decreasing density then gives more demand mass toward , yet the average behavioral order lies above ; an increasing density reverses the conclusion. Thus the mean of the choice distribution cannot generally be inferred from the modal or classically optimal order alone. This is a qualitative property of the continuous logit newsvendor, not a claim about every possible bounded-rationality model. Su (2008), §6, p. 577.
The result is proved in the published paper. The formalization work here is to supply machine-checked proofs of the stated Lean targets, together with reusable definitions of density-based expected sales, newsvendor profit, and a continuous logit choice law. These declarations are proposed open targets; a successful local build checks that their statements are well formed, but it does not constitute proofs. The reflection identity for a general continuous utility can also serve other one-dimensional logit-choice comparisons on symmetric bounded domains.
The classical first-order condition determines , but it does not determine the mean of the logit distribution. Even when the optimal order is exactly , the profit function may have different values at and , and the exponential normalization changes how those values affect the mean. A direct appeal to the monotonicity of alone therefore does not establish the conclusion. The appendix records the reflected profit and mean identities that a complete proof must justify for the density-based model. In Lean, these claims also require careful treatment of integration and the distribution function at interval boundaries. Su (2008), Appendix, pp. 586–587.
The Lean development represents as a real-valued integrable density, nonnegative everywhere, zero on negative demand, and of total integral one. For this mission it is also zero outside . The decision domain is exactly ; under either strict monotonicity assumption its closure agrees with the smallest interval containing the demand support. The logit density uses , and its expectation is an ordinary real integral. Because profit is continuous and is compact with , the normalizer is finite and positive. A zero-valued Lean integral on non-integrable input must not make any target true accidentally.
The standing readings are and . The source says “decreasing” and “increasing” while its displayed proof uses a strict density inequality; the goal therefore requires strict monotonicity. A constant density can have and , showing why a strict conclusion cannot follow from weak monotonicity alone. At , the two reflected densities are equal, so the proof's phrase “for every ” for a strict comparison is read as . The paper's prose also swaps the inequality labels for overordering and underordering; the formal inequalities follow the conclusion of its proof. These corrections are disclosed in the item descriptions and audit notes. Su (2008), §6, p. 577; Appendix, p. 587.
The midpoint is required to be a maximizer of the defined profit function over all real orders. It is not supplied as an unrelated parameter or characterized by the critical-fractile equality by fiat. The central reusable components are the density, its cumulative distribution function, expected fulfilled demand, and the logit density and expectation. Contributions that establish their continuity, integrability, and reflection properties directly advance the goal.
A retailer deciding how many variants of a product to carry (colours, sizes, flavours) trades off two effects. More variants capture more customers whose favourite would otherwise be missing, but they split demand into smaller and more variable streams, and stocking many small streams costs more inventory per unit sold. van Ryzin and Mahajan (Management Science 45(11), 1999) model this trade-off with multinomial logit (MNL) choice and newsvendor inventory costs. Their §4 asks how the trade-off depends on the category itself: is a fashion category, where customer preferences are spread evenly over many variants, intrinsically less profitable than a basic category, where a few variants dominate? They make "evenness" precise with the theory of majorization (Marshall and Olkin, Inequalities: Theory of Majorization and Its Applications, Academic Press, 1979) and prove that, with everything else equal, the more fashionable category earns no more optimal profit. This mission formalizes that comparison, Theorem 3 of the paper.
A category has variants with preferences (sorted by popularity, as in §3.1) and a no-purchase option with preference . If the store offers an assortment , a customer picks variant with the MNL probability
The prefix set holds the most popular variants, with .
Every variant sells at price and costs , with . The store sees customers on average. Two demand models give two optimal-profit functions of the assortment (equations (7) and (8) of the paper). In the independent population model, demand for variant is normal with mean and standard deviation , where and . Its optimal expected profit is
with the standard normal distribution function. In the trend-following population model, all customers make one common random choice, and the optimal profit is
For write for its entries in decreasing order. Then is majorized by , written , if
A category is more fashionable than if : its preferences are more evenly spread.
Let and be two categories with variants each, both sorted, sharing and with . Let maximize and maximize over all subsets of . Then
for and for .
In the order the proof uses them:
The theorem isolates a structural cost of fashion. Holding volume, margin and outside-option attractiveness fixed, fragmentation of preferences alone lowers the best achievable profit, even when the retailer chooses variety and stock levels optimally. The paper uses it to argue that fashion categories must command higher prices or volumes to be carried, and §4.2 asks at what prices two categories break even. The comparison also links the paper's MNL assortment model to Schur-convexity, which is the right tool for any question about how evenness of preferences affects an optimized objective.
The result is proved on paper; no machine-checked version exists. Formalizing it adds:
The obvious argument fails: one cannot apply Karamata's inequality directly to the optimal profits. The optimal assortments and have different sizes, so the MNL denominators differ, and is not a sum of one fixed convex function over the coordinates of . Moreover, majorization compares whole vectors of length , while the optimal profit of depends only on its top coordinates, and the profit of is maximized over a discrete family of prefix sets. Bridging the vector inequality and the discrete optimization is the content of the proof. Lemma 2 itself is classical but nontrivial, and Mathlib has no version of it.
Fin n, 0-based: variant of the paper is index , and A n i is the indices below .v0 > 0, shared by both categories.Antitone), the §3.1 convention under which is the set of the most popular variants.Real.rpow, with ), and is max x 0.Statements that do not count:
Each of these changes the theorem.
Needed infrastructure: Karamata's inequality (Lemma 2), which is reusable well beyond this paper; basic facts about MNL shares; and the quasi-convexity of ratio functions from Lemma 1. Proofs of any milestone are welcome, as are alternative proofs of the goal, for example through Schur-convexity.
Semidefinite programs optimize a linear objective while requiring an affine matrix to be positive semidefinite. They include familiar linear and quadratic optimization models and arise in engineering and combinatorial optimization. Vandenberghe and Boyd's survey develops their duality theory and describes interior point methods that work with primal and dual matrices simultaneously. The question in this mission is quantitative: if a method lowers a particular potential by a fixed amount at each step, how quickly does its primal-dual objective gap shrink? Vandenberghe and Boyd, pp. 49, 76–77.
The paper uses the potential to combine two kinds of progress. One term records the size of the duality gap; another records how far the current matrices are from a central pair. Decreasing the gap alone does not ensure the matrices remain well positioned for the next step, so the potential accounts for both quantities. Theorem 5.1 turns a per-step decrease in this scalar into an explicit bound on the gap after steps. The theorem concerns any sequence meeting that decrease condition; it does not prescribe a particular search direction or step-selection algorithm. Vandenberghe and Boyd, pp. 76–77.
Fix a vector and symmetric real matrices . For , define the affine matrix
The primal problem minimizes subject to . A dual-feasible matrix satisfies and for every . Here means positive semidefinite; means positive definite. The pair is strictly feasible if both and , with the dual equations still satisfied. Section 4 also assumes that are linearly independent. Vandenberghe and Boyd, pp. 49, 63, 70.
For a feasible pair, the duality gap is the difference between the primal objective and the dual objective . Equation (32) identifies it as
For a strictly feasible pair, define the deviation from centrality and the potential by
The logarithm is natural. The matrix size determines the factor; it is distinct from the number of decision variables. These are the explicit formulas on p. 76, where the paper also expresses through a central pair. Vandenberghe and Boyd, pp. 64, 75–76.
The first milestones establish the gap identity, the expanded determinant formula for , and nonnegativity of with its stated equality condition. The final milestone bounds the gap by the potential:
For the goal, let , , be strictly feasible pairs and suppose a fixed gives the decrease stated in equation (56) at every step :
The goal theorem, Theorem 5.1, says that for and
one has the boundary-correct gap estimate
The paper prints a strict inequality in the last display. Its stated non-strict threshold permits equality, as explained under Formalization scope. Vandenberghe and Boyd, p. 77, (56) and Theorem 5.1.
The theorem converts a local numerical guarantee into a global bound on an optimization certificate. Because the gap is the difference between primal and dual objectives, shrinking it gives a quantitative measure of progress toward optimality for every strictly feasible iterate. The expression records the dependence on matrix size, desired relative gap, starting deviation, and guaranteed potential decrease. It leaves the mechanism that achieves the decrease open, so different potential reduction methods can use the same conclusion. Vandenberghe and Boyd, pp. 64, 76–77.
The target here is a machine-checked statement and proof of this known 1996 result, together with its four supporting facts. The draft declarations compile as statements; their proofs remain open. A complete development would make the determinant, trace, positive-definiteness, and sequence reasoning reusable for other matrix optimization arguments. It would also record the boundary correction precisely rather than carrying forward a strict sign that fails at equality.
The substantive matrix claim is . The product need not be symmetric, even though both factors are positive definite, so directly applying a result about symmetric matrix eigenvalues to the product is not automatic. The nonnegativity and its equality case must respect the positivity and determinant conventions used by the explicit formula. The later exponential bound and iteration statement depend on those facts and on keeping each logarithm in its positive domain. Vandenberghe and Boyd, p. 76.
Lean uses Fin m for the variable matrices, indexed from zero, with as a separate argument; Fin n indexes matrix rows and columns. Matrix.IsHermitian represents real symmetry. Matrix.PosSemidef and Matrix.PosDef represent the paper's matrix inequalities and , including symmetry. The matrix size satisfies . Traces, determinants, natural logarithms, and are the corresponding Mathlib operations. All statements involving or require strict feasibility, so the real logarithm's default value on nonpositive inputs cannot decide a theorem. The paper's linearly independent are an explicit hypothesis on the Section 4 and 5 statements. Vandenberghe and Boyd, pp. 49, 70, 76–77.
The definition of uses the explicit second formula on p. 76. The central pair in the preceding formula is not represented; its existence is introduced on p. 75 without a proof there. The p. 76 prose describes for feasible pairs, but its finite real logarithmic formula and the potential reduction iterates use strictly feasible pairs. The milestone states that domain explicitly. In Theorem 5.1 strict feasibility is assumed for the iterates and equation (56) for the steps only, so the statement covers a method that stops after steps. The fixed is positive, and and are explicit.
The paper's strict conclusion is false at its own inclusive threshold. Take , , , , , and . Then , each decrease is exactly one, and at the gap equals times its initial value. The goal therefore uses , the strongest statement valid at the printed threshold. This correction is recorded in the theorem's description and moderation notes. Vandenberghe and Boyd, p. 77, Theorem 5.1.
A complete proof needs Mathlib's matrix order, determinant and trace identities, logarithm and exponential facts, and an arithmetic-geometric mean statement for positive eigenvalues. Matrix lemmas and the deviation inequality are welcome contributions alongside the final sequence bound. The definitions preserve the paper's full potential and feasible domain; replacing by zero or dropping the factor would change the target.
In a periodic-review inventory system, an order placed today arrives only after a lead time of periods. When unmet demand is lost rather than backlogged, the optimal ordering problem is a dynamic program whose state records the stock on hand and every order still in the pipeline. The problem goes back to Karlin and Scarf (1958) and Morton (1969, 1971). It is computationally difficult because the state dimension grows with the lead time, and few structural facts about how the optimal cost depends on the system's parameters are known.
Zipkin (2008), Old and New Methods for Lost-Sales Inventory Systems, states one such fact in its abstract: the optimal cost is increasing in the lead time. Section 5 of the paper makes this precise for the discounted cost by comparing the system with lead time to the one with lead time , and derives from the comparison a lower bound, (6), on the cost of the longer system in terms of the solution of the shorter one. The paper uses that bound to start the computation of system from the solution of system , and reports it in the "Bound" rows of its numerical tables. The paper also remarks that the argument applies to any system with control lag.
The state of the system with lead time is : is the stock on hand after this period's arrival, and is the order that arrives periods from now. With an order and a demand , the next state is
and demand in excess of is lost. Demands are independent with a common law on with finite mean.
The costs are a unit procurement cost , a unit holding cost , a unit lost-sales penalty and a discount factor . After the paper's standard transformation, the holding cost becomes and the cost charged to the current order is
where and is the stock on hand periods later. The one-period cost of system is . Writing for the first components of the next state, the costs satisfy the recursion .
The optimal cost is the limit of the finite-horizon costs of recursion (2),
as the horizon grows. It satisfies the optimality equation (3), .
For , every state of system , and the state of system obtained by dropping the most recent order,
and
The first inequality is the formal content of "the system cost is nondecreasing in " in the discounted case: the systems live on state spaces of different dimension, and system pays one extra period cost before system starts to accumulate costs. The second is the bound the paper uses numerically.
A further statement, not a milestone, records that for , the discounted analogue of the paper's remark (p. 1256) that the optimal lost-sales cost is bounded when mean demand is finite.
The result. Monotonicity in the lead time is a basic comparative-statics fact about lost-sales systems that is not obvious from the dynamic program, because the two systems have state spaces of different dimension. Inequality (6) turns it into a computational tool: the solution of system yields a lower bound for system , which can be used to warm-start value iteration for the larger system and to certify the quality of heuristics.
The formalization. The results are proved in the paper, informally and in a few lines; none of them has a machine-checked proof. A formal development requires making the paper's coupling argument (system placing, one period ahead, the order system places now) precise as an inequality between value functions on spaces of different dimension. The optimality equation for a dynamic program with a continuous state space and an unbounded action set is a reusable result for other inventory models with the same structure.
The paper's argument constructs a non-Markovian policy for system from an optimal policy of system . Turned into a statement about value functions, the policy-based argument needs a theory of history-dependent policies and their costs that the definitions here deliberately avoid: the optimal cost is defined through the operator of (2), not as an infimum over policies. Either that theory is built, or the comparison has to be expressed directly between value functions on two state spaces of different dimension, where the extra order of system has no counterpart in system .
The optimality equation (3) is not automatic either. Showing that the limit of value iteration is a fixed point requires interchanging an infimum over the noncompact set with an increasing limit; for a general monotone operator with a noncompact action set the interchange fails, so the lost-sales structure has to be used.
The Lean development lives in the namespace LostSalesOldNew.LeadTime. Its conventions:
Fin L → ℝ; is Fin.snoc x z; is Fin.init x (dropping the most recent order, not the oldest); shift x d is and next x z d is the full transition. The goal is stated with lead times and , so no natural-number subtraction occurs.D on ℝ with D (Iio 0) = 0 and finite mean (Integrable id D); the demands of several periods have the product law Measure.pi. The paper's i.i.d. assumption is encoded this way.ENNReal.ofReal; this is exact on nonnegative states because there under the sign conditions. The paper's is an infimum over in the operator, and its attainment is a separate clause of the milestone, stated under or (with and unbounded demand the minimum is not attained); negative orders are excluded. The first goal inequality is kept in additive form, since subtraction in truncates.A trivializing reading is ruled out: the goal is not stated as (6) alone, which would drop the monotonicity claim, and the separate finiteness statement shows that the inequalities compare finite numbers rather than holding because one side is .
The average-cost version of §5 is not formalized (it presupposes an average-cost optimal policy), nor is uniqueness in (3) beyond minimality. Related platform formulations of the lost-sales system, such as CappedBaseStock_Model (Xin's capped base-stock analysis), use another state convention, an empty initial pipeline and the average-cost criterion, so they are not referenced. Contributions welcome: the recursion for (a Fubini computation over product measures), the optimality equation, the finiteness bound, and the goal.
The trust-region subproblem asks for the minimum of a quadratic function over a Euclidean ball,
with a real symmetric matrix that may be indefinite. It is solved at every iteration of a trust-region method for nonlinear optimization (Moré and Sorensen 1983; Conn, Gould and Toint 2000), so a method for it is used many thousands of times in a single run. Classical methods based on factorizations of do not scale to large sparse problems.
Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998)) apply to their DCA, a general algorithm for d.c. programs (minimizing a difference of two convex functions). For a suitable splitting of the objective, one DCA iteration is a matrix–vector product followed by a scaling onto the ball. This mission formalizes the convergence theorem for that iteration (Theorem 4.1 of the paper), together with the general DCA convergence results it is derived from (Theorem 3.7 and the Appendix).
Timeline (as recorded in the paper's introduction):
Let with inner product and norm . For a function , , and is the set of proper, lower semicontinuous, convex functions. For the conjugate is , and the subdifferential at is . The function is -convex () if is convex.
A d.c. program is with , under the convention and the standing inclusions , . Its dual objective is . The simplified DCA builds two sequences from :
For let (), its indicator, and . Fix with positive semidefinite and split as in (16):
The resulting DCA starts at any and, with , sets if and otherwise; equivalently . A Kuhn–Tucker point of is an with some such that , and .
For every run of the DCA,
decreases to a limit , , and every limit point of is a Kuhn–Tucker point.
In attack order:
The equality case of Theorem 3.7(i) and Theorem 3.7(ii) (the dual descent) are included as further draft theorems.
Theorem 4.1 makes the DCA a descent method for whose accumulation points satisfy the first-order conditions. That property is what the paper's restarting procedure (§4.2) builds on: at a Kuhn–Tucker point that is not a global minimizer, one eigenvector computation gives a better feasible point, and the DCA reaches a global solution after at most restarts, where is the number of distinct negative eigenvalues of . Theorem 3.7 is the convergence theorem for the DCA on general d.c. programs, used throughout the later DCA literature.
All of these results are proved in the paper. As far as is known, none of them has a machine-checked proof: Mathlib has convex conjugates and subdifferentials in pieces, but no d.c. duality, no DCA and no analysis of the trust-region subproblem. This mission produces that development: a statement layer for d.c. programming with extended values, a formal proof of the general descent and criticality theorem, and its specialization to .
Every inequality of the analysis runs over . The differences and need the paper's convention , and the finiteness of each value along a run has to be derived from the standing inclusions. The hard step is the passage to limit points in Theorem 3.7(iv). Lower semicontinuity of , and gives only one-sided inequalities at a limit point, while the theorem asserts equalities of values there. The naive argument of passing to the limit in and fails, because and need not have the same limit unless . For the specialization needs boundedness of the iterates, finiteness of , and the subdifferential of the indicator of the ball. None of these is a hypothesis of Theorem 4.1, so each must be proved from the run.
is EuclideanSpace ℝ (Fin n). Extended values are EReal, and every d.c. difference is dcSub g h x, equal to when and to otherwise, because Mathlib's EReal has . , subgradients and the conjugate come from published platform definitions (IsProperClosedConvex, IsSubgradient, CondatPD.FinDim.conj). The modulus of strong convexity is never defined as a supremum. Statements take explicit constants with " is -convex", which is what the paper requires of them. Hypotheses "" become . The matrix is a self-adjoint continuous linear operator. " is the smallest eigenvalue of " is encoded by quantifying over every with . A limit point is a cluster point. The objective is outside , and the run starts from an arbitrary , as on the page. Statements involving are for . Theorem 3.7(iv)'s limit identity is stated along a common convergent subsequence, as in its proof.
Ruled out: the goal is stated for the explicit iteration a)/b) of p. 490, never for an abstract run assumed to satisfy Theorem 3.7, and it carries no hypothesis of boundedness, finite or convergence. A run predicate that no sequence satisfies would make everything vacuous, and a sanity file exhibits concrete runs.
Needed infrastructure: the Fenchel–Young equality and its equality case for functions in EReal, subdifferential inversion , strong-convexity versions of the subgradient inequality, and the normal cone of a Euclidean ball. These are reusable well beyond this mission and are welcome as separate contributions.
The newsvendor problem is the basic model of a one-period inventory decision: a seller orders units at unit cost before a random demand is observed, and sells units at unit price . A perfectly rational newsvendor orders the critical fractile , where is the distribution function of . Laboratory experiments (Schweitzer and Cachon 2000; Bolton and Katok 2008) found that human subjects systematically deviate from : their orders are noisy and, on average, pulled toward mean demand.
Su (2008) explains these patterns with a model of bounded rationality taken from the logit choice literature (Luce 1959; McFadden 1981). The decision maker does not pick the best order; instead each order is chosen with probability density proportional to the exponential of its expected profit, scaled by a noise parameter . The resulting random order, the behavioral solution , is the object of the paper. For uniform demand it is a truncated normal and its moments are explicit (§4.1). For a general demand distribution there is no closed form, and §4.3 of the paper characterizes the moments of through a single function instead. This mission formalizes that characterization, Proposition 2.
Demand has a density : , for , and . For an order quantity , the expected sales are and the expected profit is (eq. (3))
The decision domain is the smallest interval containing the support of : the boundedly rational newsvendor may order any quantity between the smallest and the largest possible demand. The behavioral solution is the random order with density (eqs. (4), (11))
and for .
A family of densities forms an -dimensional exponential family if they have the form (eq. (10)); the are the natural parameters, the the sufficient statistics and the log-partition function. Su observes that the choice densities are of this form with , natural parameters and , statistics and , and
In the Lean development these objects are IsDemandDensity f, expMin f, nvProfit f p c (), decisionDomain f (), logitDensity S (nvProfit f p c) β (), logitExp S u β g (the expectation ) and logPartition f η₁ η₂ (), all in the namespace BoundedNV.ExpFam.
With and , both partial derivatives of exist at , and
Proposition 2 turns the computation of the expected order and the expected profit of a boundedly rational newsvendor, which are integrals against the density (11), into the differentiation of one function of two variables. The paper uses this in two ways (p. 575): moments of can be approximated numerically from finite differences of , and can be estimated from aggregate laboratory data by the method of moments, choosing so that at matches the observed average order.
The result is classical in structure: (13) is the standard identity for exponential families (see, e.g., Lehmann and Casella 1998). What the formalization adds is the verification that the identity applies to this particular family under the paper's hypotheses, including demand distributions with unbounded support, where the decision domain is a half-line and the integrals are improper. To our knowledge, no part of the paper has been formalized before.
The identity (13) rests on differentiating under the integral sign in (12). The textbook justification requires the natural parameter to lie in the interior of the natural parameter space, together with a dominating function for the derivative of the integrand. Neither is on the page: the paper states the Fact for exponential families in general. For bounded the domination is immediate; for unbounded it is not, and the natural first idea, to bound by the mean of , fails because the paper assumes no finite mean. The required control comes instead from the growth of , which is sublinear in , against the linear decay with . This must be established uniformly for parameters in a neighborhood of .
All quantities are real. Integrals are Lebesgue (Bochner) integrals over or over , and partial derivatives are derivatives of the one-variable sections and . The conventions committed to are:
Junk values ruled out. In Lean, , , the integral of a non-integrable function is , and deriv of a non-differentiable function is . If the statements used these silently, every identity could hold because every term vanishes. The milestones therefore assert integrability and positivity of the normalizer and that integrates to . Every derivative is stated with HasDerivAt, which asserts differentiability.
The Fact (13) is not formalized for abstract exponential families, whose hypotheses the page does not state; it is specialized to this family. The method-of-moments remarks after Proposition 2 and the empirical §5 are not part of the mission.
The infrastructure needed is differentiation of parametric integrals over unbounded domains (Mathlib's hasDerivAt_integral_of_dominated_loc_of_deriv_le) and elementary facts about : continuity, for , and sublinear growth. The last of these is reusable for any newsvendor model with general demand. Contributions of proofs for each milestone, and of a lemma establishing the uniform domination near , are welcome.
The source is the published article in Manufacturing & Service Operations Management (2008); page numbers are the journal's.
A d.c. program minimizes a difference of two convex functions,
with and proper, lower semicontinuous and convex. Every twice continuously differentiable function is d.c. on compact convex sets, so the class covers most smooth nonconvex optimization, and it includes the trust-region subproblem that motivates the paper of Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998) 476–505). Global minimization of a d.c. function is NP-hard in general, so practical algorithms, in particular the DCA of the same authors, compute local minimizers and critical points. The theory of local optimality is therefore what those algorithms can actually certify.
D.c. programs come with a dual program built from conjugate functions, , which has the same optimal value. Toland (J. Math. Anal. Appl. 66 (1978)) showed that global solutions correspond under this duality. For local solutions the correspondence is subtler, and §3.2 of the paper gives conditions under which a local minimizer of the primal produces one of the dual. Toland's earlier version required to be differentiable on the whole space; Corollary 3.5 of the paper needs only a condition at the single point .
Let with inner product and norm ; the dual space is identified with . Functions take values in . is the set of proper lower semicontinuous convex functions. For :
Differences are taken under the convention . Throughout, satisfy the standing inclusions
A point is a local minimizer of if is finite and there is a neighbourhood of with for all (display (4) of the paper); under the convention this is the same as requiring it for . It is a critical point if . The set collects the points satisfying the classical necessary condition. "Local minimizer of " is the same definition applied to the dual pair .
Let have an open neighbourhood with for all , and let . If
then is a local minimizer of .
then on , and is a local minimizer.
Corollary 3.5 lets a local solution of the primal d.c. program be read off as a local solution of the dual one. This matters when the dual program is easier to handle locally, and it is the local counterpart of the global duality of Theorem 3.1. Theorem 3.2(ii), which the authors present as new, is a sufficient condition for primal local optimality stated through the dual objective. Corollaries 3.3 and 3.4 are the sufficient conditions on which the convergence analysis of the DCA rests: they explain when the critical points that the DCA reaches are in fact local minimizers, for instance when is polyhedral.
These results have been proved on paper since 1997–1998 and are not open. To our knowledge none of them has a machine-checked proof. Formalizing them produces the local optimality theory of d.c. programming on top of an extended-real convex analysis layer (conjugates, subdifferentials, the convention ), which the sibling missions of this series (global optimality, the DCA for the trust-region subproblem) can reuse.
Theorem 3.2 and Corollaries 3.3–3.4 are short arguments built on the Fenchel–Young inequality and its equality case. The obstacle in the goal is that the dual application of Theorem 3.2(ii) needs its hypothesis on a whole neighbourhood of , while (12) is a condition at the single point . Bridging this requires the upper semicontinuity of the subdifferential of at an interior point of its domain. That rests on two facts: is continuous and locally bounded there, and the subdifferential is locally bounded with closed graph. Neither is in Mathlib for extended-real functions. The dual application also needs to satisfy the standing assumptions, which needs biconjugation for , again in the extended-real setting. A first attempt that works only with finite-valued convex functions does not apply: is typically outside a bounded set.
EuclideanSpace ℝ (Fin n) and values are EReal. , and the conjugate are the published definitions ThreeOpSplitting.ConvexRates.IsProperClosedConvex, InertialFB.IFB.IsSubgradient and CondatPD.FinDim.conj (an EReal supremum over all of ). The subgradient predicate requires the base point to lie in the domain, as the paper does.dcSub, which returns whenever . Mathlib's EReal subtraction is not used for it, because Mathlib sets , and that would make every point outside a global minimizer with value .IsLocalMin is not used), and the goal's conclusion includes the finiteness of .DCStanding and are a hypothesis of every item.EReal-valued functions;In a strategic game, players may repeatedly change their own choices when a change raises their payoff. This gives a simple model of decentralized adjustment: each move uses the current profile and one player's immediate incentive. The central question is whether such adjustment can continue forever. Monderer and Shapley introduced the finite improvement property (FIP) to state that every sequence of strict unilateral improvements ends. Their 1996 paper, pp. 128–130, relates that dynamic property to a real-valued function on the game's strategy profiles.
An ordinal potential records each player's strict preference between two of their strategies when the other players' strategies are fixed. Such a function is useful because it assigns one common direction to the players' individual choices. The paper gives a two-player game that has the FIP but no ordinal potential, then introduces a weaker, generalized ordinal potential and proves that it captures exactly the finite games with the FIP (Monderer and Shapley, pp. 129–130). This mission isolates that characterization from the paper's other results about exact potentials and congestion games.
Let be a finite set of players. Player has a strategy set , and a strategy profile selects one strategy for each player. The payoff function gives player 's payoff at a profile. Write for the profile obtained by replacing player 's strategy in by . A finite game has finite for every player. These are the paper's conventions at the start of §2 (p. 127).
A path is a sequence of profiles in which each step changes exactly one player's strategy to a different strategy. It is an improvement path when the moving player strictly increases their payoff at every step. The game has the FIP if no infinite improvement path exists. Thus the property concerns paths of any length and every allowed choice of deviator, rather than the behavior of one selected update rule (p. 128).
An ordinal potential satisfies
for every player , opponents' profile , and . A generalized ordinal potential replaces this equivalence by the forward implication only. The two notions are distinct, as the game on p. 129 shows (equations (2.1) and (2.3), pp. 127, 129).
For every finite game ,
This is Lemma 2.5, p. 129. It specifies a precise characterization rather than choosing a particular potential or a particular update schedule.
The milestone list follows the paper's statements: Lemma 2.3 says a finite ordinal potential game has the FIP; the proof of Lemma 2.5 says the finite-improvement reachability relation is transitive under the FIP; and it concludes that the whole strategy-profile set can be represented by a real function increasing along that relation (pp. 128–130). Corollary 2.6 and the explicit game record the boundary between ordinal and generalized ordinal potentials: under its distinct-payoff condition a finite game with the FIP has an ordinal potential, while shows that condition cannot simply be omitted (pp. 129–130). Lemma 2.1 and Corollary 2.2 concern equilibria: an ordinal potential game has the same pure equilibria as the game in which every player receives the potential, so a maximizer of the potential is an equilibrium, and every finite ordinal potential game has a pure-strategy equilibrium (p. 128).
The goal connects a property of all possible strict improvement paths to the existence of a single real-valued certificate on profiles. In a finite game, such a certificate describes a common direction for unilateral payoff gains, regardless of which improving player moves next. The distinction between ordinary and generalized ordinal potentials matters: an ordinary potential must also preserve indifference, whereas the FIP alone does not require that (Monderer and Shapley, p. 129).
The characterization is proved in the paper; the remaining work in this mission is a Lean proof of its faithful finite-game statement. The local platform index used for this proposal has no published theorem expressing this characterization. The definitions of improvement paths and improvement reachability can also support other formal results about game dynamics. The game serves as a concrete check on the strict distinction between the two potential notions.
The payoff vector itself does not give an immediate numerical order on whole profiles: each step compares one player's payoff, and the next step may involve another player. Finiteness rules out an endlessly increasing sequence only after a suitable profile-level ordering has been established. The converse direction therefore requires more than observing that each individual move helps its deviator. The paper's also rules out replacing the generalized potential in the goal with an ordinary ordinal one (p. 129).
Players form a finite Lean type ι with decidable equality; each player's strategies form a type Y i. A theorem about a finite game additionally assumes every Y i is finite. These types may be empty: in that case there is no strategy profile, and the corresponding FIP and potential statements retain their ordinary quantified meaning. No nonemptiness assumption is inserted into Lemma 2.5. Corollary 2.2 alone assumes every strategy set nonempty, which the page takes for granted: without it there is no profile and no equilibrium. An equilibrium point is a pure Nash equilibrium in the sense of the published definition AGT.IsPureNash (no player gains strictly by a unilateral deviation), and "P admits a maximal value in Y" in Lemma 2.1 is read as "P attains its maximum on Y". The finite player assumption follows the standing convention on p. 127; the finite strategy assumption is added only where the source says “finite game.”
The expression is Function.update y i x. IsStep requires one coordinate to change to a different value. HasFIP forbids an infinite natural-number-indexed path of strict payoff improvements, so it cannot be satisfied merely because each separately described finite path has finite length. A finite path stores its deviator at each step; the genuine-step condition determines that deviator uniquely. The same path bundle contains the paper's path sum and closed-path predicates for consistency across this paper's missions, although only finite improvement paths are used here. The relation ImprovesTo u x y means that a finite strict improvement path leads from to a distinct .
The necessary development comprises the two potential predicates, path and FIP definitions, the finite improvement relation, the transitivity and representation milestones, and the goal characterization. Contributions that prove these statements or simplify their proof dependencies are within scope. A definition that checks only finite paths, allows null steps, or confuses the one-way condition (2.3) with the two-way condition (2.1) would change the result.
In sequential prediction, several forecasters can issue different answers for the same instance. A master algorithm must combine their advice before the true label is known. Littlestone and Warmuth's Weighted Majority framework gives worst-case guarantees for this setting: the instances and labels need not come from a probability distribution. The paper first studies binary predictions and then allows real predictions and labels in the unit interval. The continuous version matters when the distance between a prediction and a label carries information that a binary mistake count discards. The formal target here is the paper's total absolute-loss guarantee for that continuous master, WMC (Littlestone and Warmuth 1994, §5).
The result is part of the paper's generalized analysis, which also covers a binary master WMG and a randomized master WMR. These algorithms share a range of allowed weight updates, but their predictions and losses differ. This mission isolates WMC's deterministic, continuous-label theorem and the numbered lemmas on which its statement rests. The finite-sequence convention is explicit in the paper's notations and assumptions (Littlestone and Warmuth 1994, p. 220).
Fix a finite nonempty pool of forecasters and a finite sequence of trials. At trial , expert predicts , and after the master predicts, a label is revealed. Expert has weight before that trial. Every initial weight is positive, and weights remain nonnegative. The total weight and weighted mean prediction are
WMC predicts . Its loss on the trial is the absolute error , and its total absolute loss is . Write and for total weight before the first and after the final update (Littlestone and Warmuth 1994, pp. 232–233).
WMC updates on every trial. For , it multiplies each weight by a factor in the interval
The factor may depend on both trial and expert. The paper permits any choice in this interval, so WMC denotes a class of runs rather than one fixed recurrence. Its convention is used when and an expert has zero error (Littlestone and Warmuth 1994, p. 233, eq. (5.1)).
For every run with positive final total weight, the target is the paper's explicit inequality
The bound uses the run's actual initial and final weights, so it applies whether the upper or lower permitted update factor was selected, or a factor between them. The finite-valued statement assumes ; the paper regards the bound as vacuous when the denominator of the logarithm is zero (Littlestone and Warmuth 1994, p. 236, Theorem 5.2).
Lemma 5.1 states for and , ensuring the update interval is nonempty. Lemma 5.2 states the logarithmic potential estimate under only the update's upper inequality, including the special case in which and a master's unit loss forces the final total weight to zero. Lemma 5.3 turns those same conditions into the displayed total-loss bound. Each is a separate milestone with the paper's statement and page provenance (Littlestone and Warmuth 1994, pp. 233–236).
The theorem controls the master's accumulated real-valued prediction error by an observable change in the total pool weight. It requires no distributional assumption on the trial sequence and no single choice of update factor. That breadth lets the same estimate be used for different update rules within the allowed range, while the explicit constant records the dependence on the algorithm's parameter. The paper also uses Lemma 5.3 in its analysis of WMR's expected loss (Littlestone and Warmuth 1994, pp. 236, 240).
The paper proves these results; this mission asks for machine-checked proofs of their exact Lean statements. Its definition of a permitted continuous run and its upper-update potential conditions can also support subsequent formalizations of WMG and WMR. Lemma 5.1, the potential estimate, and the final loss bound remain distinct proof targets so that a solver can use or improve the underlying analytic infrastructure without changing the goal.
A binary mistake indicator cannot express the magnitude of an error between two unit-interval values. The generalized update contains a real exponent, absolute values, and a range of legal factors. An argument that handles only a selected endpoint of that range would leave permitted WMC runs uncovered. A further boundary occurs at : an allowed update can reduce a positive weight to zero, and real logarithms in Lean have a defined value at zero although the paper's logarithmic bound is infinite there. The formal statements therefore distinguish the zero-final-weight clause from the finite-logarithm clause.
The pool is Fin n with and the trials are Fin t; an empty sequence of trials is allowed. Lean's trial index starts at zero, so w 0 represents and w t represents the weights after all trials. The inputs are the prediction array and label array. Instances are not stored separately because the theorem refers to them only through expert predictions. Values, factors, totals, and losses are real numbers. The run predicate requires positive initial weights, nonnegative weights, predictions and labels in , , and a permitted factor for every expert on every trial.
The theorem quantifies over every permitted run. A sorry-free local example exhibits a one-trial run with positive final weight, ruling out a globally empty run predicate. For positive final weight, the update conditions ensure earlier total weights are positive, so every weighted mean used in the loss has its intended denominator. The finite logarithmic conclusions assume positive final weight because Real.log 0 would otherwise introduce an unrelated total-function value. The definition layer supplies total weight, weighted mean, loss, base conditions, the upper-update conditions, and WMC runs; the proof development needs finite-sum and real logarithm inequalities from Mathlib. Contributions that establish the three numbered lemmas or the goal under this interface are in scope.
Bounds on the upper tail of a sum of independent random variables are used throughout probability, statistics, queueing and risk theory: they control ruin probabilities, the error of empirical averages, and the size of the largest deviations of random walks. The classical exponential inequalities (Bernstein, Hoeffding, Bennett) require the summands to be bounded or to have finite exponential moments of a fixed order. The polynomial bounds of Fuk and Nagaev only require finite power moments, at the price of a power-law rate.
Between these two regimes lie summands whose right tails decay like for a function growing faster than a logarithm — Weibull-type and other subexponential or superexponential tails. For such summands the natural size parameter is not a power moment but a generalized moment . Section 2 of S. V. Nagaev's survey Large deviations of sums of independent random variables (Ann. Probab. 7, 1979, doi:10.1214/aop/1176994938) develops bounds on in terms of these quantities. Theorem 2.5 of that section, attributed to S. K. Sakoyan and Nagaev, treats the case where has a positive nondecreasing derivative — the case of the paper — and gives a bound in product form whose exponential order is .
Let be a probability space and independent real random variables with distribution functions . Write
Let be differentiable with a derivative that is positive and nondecreasing; in particular is convex and increasing, and as .
For each summand define the generalized moment
and, for a real , the negative-part factor
The factor is always finite, since its integrand lies in ; may be infinite, and the theorem is meaningful only when every is finite. In Lean these objects are S n X, bg P X g j and bj P X g g' j s in the namespace NagaevLD.GenMoment.
For every ,
The statement holds for every , every distribution of the summands with finite , and every admissible ; no constant is hidden.
The proof of the paper passes through the following displays, all on pp. 767–768, with where indicated:
The bound separates the tail of into a product of one-summand quantities. For fixed and one has , so for large (the paper's (2.49)); compared with the elementary lower bound (2.50), this shows the exponential order is the right one when the right tails of the summands are of order . The only case where the right side does not depend on is , the classical Chernoff regime, of which the theorem is a generalization.
The result is a published theorem with a complete half-page proof; it is not open. As far as a search of the Prove2Me catalogue shows, no part of it has been machine-checked: the catalogue contains single-variable Chernoff bounds (Mathlib's measure_ge_le_exp_mul_mgf) but no bound in terms of generalized moments. The mission produces a formal proof of the theorem and, along the way, reusable statements about tilted truncated moments of independent sums.
Each step of the argument is short; the work is in carrying it through real-valued measure theory. The exponential Chebyshev step requires the moment generating function of a sum of independent variables to factor, which needs the integrability of every — a fact that here must be derived from the finiteness of and the bound on , not assumed. The supremum in (2.46) has to be identified as a maximum attained at , which rests on the convexity of on obtained from a monotone derivative. Finally the split of at must match the definition of exactly: a mismatch at the single point breaks the theorem.
The summands are X : Fin n → Ω → ℝ on a probability space, each measurable and jointly independent (iIndepFun); index in Lean is the paper's . Integrals over a set of are written as expectations restricted to the corresponding event, so no distribution functions appear. Probabilities are P.real, and is P.real {ω | x ≤ S n X ω}.
Committed conventions and disclosed additions:
sSup: (2.46) is stated for every upper bound of on , and (2.47) as IsGreatest.A complete development needs the factorization of exponential moments of independent sums (available in Mathlib as iIndepFun.mgf_sum), Markov's inequality, splitting a Bochner integral over an event and its complement, and the tangent-line inequality for a function with monotone derivative. Proofs of the milestones, alternative arguments, and lemmas on truncated exponential moments are all welcome.
Congestion games model situations in which agents choose sets of shared resources and the payoff of each resource depends only on how many agents use it: drivers choosing routes through road segments, jobs choosing machines, flows choosing links in a network. Rosenthal (A class of games possessing pure-strategy Nash equilibria, Int. J. Game Theory 2, 1973) showed that every such game has a pure-strategy Nash equilibrium, by exhibiting a single real function on strategy profiles whose changes track every player's unilateral payoff changes.
Monderer and Shapley (Potential Games, Games Econ. Behav. 14, 1996) isolated that property and called games having it potential games. Their Section 3 shows that the property characterizes congestion games: Rosenthal's argument gives Theorem 3.1 (every congestion game is a potential game), and Theorem 3.2 gives the converse up to a renaming of strategies. Potential games have since become a standard tool in algorithmic game theory (convergence of best-response dynamics, price of stability bounds, learning in games), and Theorem 3.2 is the reason that results proved for congestion games apply to all finite potential games.
A game in strategic form has a finite set of players , for each player a strategy set , the profile set , and payoff functions . For a profile and , is with player 's strategy replaced by . The game is finite if every is finite.
A function is a potential for (condition (2.2) with unit weights) if
and is a potential game if it has a potential (IsPotential, IsPotentialGame).
A congestion model has players , a finite set of facilities , for every player a set of strategies, each a nonempty subset of , and for every facility a vector , where is the payoff to each user of when exactly players use it. The associated congestion game has strategy sets and payoffs
Two games with the same players are isomorphic (IsIsomorphic) if there are bijections with for every player and profile .
Formally: for every finite set of players, finite strategy sets and payoffs admitting a potential, there are and a congestion model on the facilities , all of whose strategies are nonempty facility sets, whose congestion game is isomorphic to .
The milestones follow Appendix B of the paper.
Theorems 3.1 and 3.2 together say that, up to renaming strategies, the finite potential games and the congestion games are the same class. Consequently any statement about finite congestion games that is invariant under isomorphism (existence of pure equilibria, convergence of improvement dynamics, the structure of equilibrium sets) holds for all finite potential games, and conversely any potential game can be realized as a resource-sharing model. The representation is also the starting point of the later literature on the number of facilities needed to represent potential games, which the paper itself begins with a remark at the end of Appendix B.
Theorem 3.1 is already machine-checked on the platform, as Rosenthal's potential identity PriceOfStability.Harmonic.rosenthal_potential_change (Proved); it is included in this mission as a reference item. Theorem 3.2 is proved in the paper but has no machine-checked proof that we know of. The mission adds a formal statement of the theorem, of isomorphism of games, of congestion games as games in strategic form, and of the explicit construction of Appendix B; and, once proved, a verified converse to Rosenthal's theorem.
The theorem is an explicit construction, and its difficulty is bookkeeping rather than a single hard idea. The facility set is a product of Boolean cubes, one per player; each player's strategy is the set of facilities with a 1 in a given coordinate; and the facility payoffs are defined only at load and load , by two auxiliary vectors whose definitions involve a choice of representative. Showing that the resulting congestion game reproduces every payoff requires identifying, for every profile, exactly which facilities are used by one player and which by all players, and showing that the "load 1" facilities pick up precisely the part of that player cannot influence. The paper leaves the two key set identities as "it can be verified"; they are the milestones.
The construction as printed does not cover one player: with the vectors and are the same vector, defined twice. The theorem is still true for one player, and the formal goal does not exclude it, so a complete proof must treat that case separately.
ι with decidable equality; strategy sets are types Y i, finite in the goal ([∀ i, Fintype (Y i)]). is Function.update y i x. No nonemptiness of the strategy sets and no lower bound on the number of players is assumed.CongestionPoA.AsymSum.CongestionGame ι M (reference item): strategies i is the finite family and latency j k is the paper's , an arbitrary real number. No sign change is made; the published names "latency" and "cost" are only names. Values of latency at and above never enter (3.1).congestionPayoff G, whose strategy set for player is the subtype of G.strategies i. Because the isomorphism maps onto that subtype, the strategies of a player are distinct facility sets.Fin m for an existentially quantified , and nonemptiness of every strategy, which is part of the definition of a congestion model on p. 133 but not of the published structure, is a separate conjunct. Dropping it, or replacing "congestion game" by an arbitrary game whose payoffs equal , would make the goal a different, weaker statement; the formal goal does neither.FacilityConstruction) indexes the coordinates of player by itself instead of ; is passed as a full profile whose -th coordinate is ignored; and select a representative by choice, the chosen -th coordinate playing the role of the arbitrary in (B.4).Contributions welcome: proofs of the milestones, a proof of the goal (by the paper's construction, with the one-player case handled separately, or by any other construction), and general lemmas about transporting potentials along isomorphisms.
Monotone comparative statics asks when the optimal choice of a decision maker moves in a predictable direction as a parameter of the problem changes: when a firm facing a higher price produces more, when a monopolist facing lower costs sets a lower price, when a player in a game best-responds with a higher strategy to higher strategies of the others. The classical sufficient conditions, due to Topkis (Topkis 1978), are supermodularity of the objective in the choice variable and increasing differences in the choice and the parameter. Both are cardinal conditions: they can be destroyed by a strictly increasing change of the units in which the objective is measured, although such a change does not alter any optimal choice.
Milgrom and Shannon (Econometrica 1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed that the ordinal conditions are necessary and sufficient for the set of maximizers to be monotone in the parameter and the constraint set (their Theorem 4). This mission concerns the relation between the ordinal notion and the cardinal one: in which sense is a quasisupermodular function "a supermodular function up to a change of units"? Section 3 of the paper answers it with Theorem 8. An earlier notion in the same direction, supermodularizable functions, was studied by Li Calzi (1991).
Let be a lattice: a partially ordered set in which every two elements have a least upper bound (join) and a greatest lower bound (meet). Examples are and products of finite chains, ordered componentwise.
A function is supermodular on a set if
It is quasisupermodular (p. 162) if for all
A function is strictly increasing if implies . A function is supermodularizable if is supermodular on for some strictly increasing .
For the set is closed under and ; it is the sublattice generated by and and has at most four points.
Quasisupermodularity depends only on the order of the values of , so it is preserved by strictly increasing transformations; supermodularity is not. Every supermodular function is quasisupermodular, and so is every supermodularizable function.
is quasisupermodular if and only if there is such that (i) is strictly increasing for every , and (ii) for every ,
The Lemma is the "only if" direction of Theorem 8 on a single sublattice; Example 1 shows why the transformation in Theorem 8 must be allowed to depend on .
Theorem 8 characterizes an ordinal property by a family of cardinal ones: quasisupermodularity is exactly local supermodularizability, on every two-generated sublattice. It explains why quasisupermodularity, and not supermodularity, is the natural hypothesis of ordinal comparative statics, and Example 1 marks the boundary: a single global transformation is not enough, so supermodularizable functions form a strictly smaller class. The paper states an analogous characterization of the single crossing property (Theorem 9, p. 166) without proof.
On the formalization side, none of these results is machine-checked anywhere known to this mission. The platform already holds Topkis's lattice-theoretic definitions and theorems (supermodularity, increasing differences, monotonicity of the argmax under the cardinal conditions); this mission adds the ordinal notion and its characterization on top of the published definition of supermodularity. A formal proof of the Lemma also requires constructing a strictly increasing map of all of that moves one prescribed value, which is reusable for other "ordinal versus cardinal" results.
The "if" direction and the invariance and supermodularizability remarks are short unfoldings of the definitions. The work is in the Lemma. On a four-point lattice the values of at need not satisfy , and the obvious attempt, applying one transformation fixed in advance (such as an exponential), fails: the needed transformation depends on the four values. A strictly increasing of the whole real line must be chosen to separate the values while preserving their order, and the degenerate configurations in which some of the four values coincide, or in which and are comparable so that the lattice has fewer than four points, have to be handled separately. A second subtlety is that quasisupermodularity is used for both orders of the pair .
Lattice class; joins and meets are ⊔ and ⊓. Functions are real valued.QuasiSupermodularOn g S, relativized to a set ; the paper's notion on is QuasiSupermodularOn f Set.univ. It quantifies over all ordered pairs of .Supermodularity.Monotonicity.SupermodularOn (Topkis series), also relativized to a set; supermodularity "on the sublattice" is SupermodularOn _ {x₁, x₂, x₁ ⊔ x₂, x₁ ⊓ x₂}.StrictMono. With merely monotone transformations the statements trivialize: a constant transformation is supermodular on every set, which would make the "if" direction of Theorem 8 false and the second half of Example 1 false. The formal statements rule this out.g : ℝ → X → X → ℝ; it may depend on but not on . Transformations are defined on all of , as printed, not only on the values of .Fin 2 × Fin 4 with the product order.Contributions welcome: proofs of the milestones and the goal; a general lemma producing strictly increasing maps with prescribed values on finitely many points.
The speed at which a finite reversible Markov chain approaches its stationary distribution is controlled by its eigenvalues. For a chain with eigenvalues , the distance to stationarity after steps is governed by , where (Diaconis and Stroock 1991, Proposition 3). Upper bounds on the second eigenvalue are the familiar half of this picture, and they are what Cheeger-type and Poincaré inequalities provide. The other half is the smallest eigenvalue : a chain whose smallest eigenvalue is close to oscillates almost periodically and mixes slowly whatever is. A chain is aperiodic exactly when , but that qualitative fact gives no rate.
Diaconis and Stroock's paper gives geometric bounds for both ends of the spectrum, expressed through systems of paths in the graph of the chain. Their bound on uses closed paths with an odd number of edges, the combinatorial witnesses of aperiodicity. The paper has been a standard reference for path (canonical-path, multicommodity-flow) methods in the analysis of Markov chain Monte Carlo since its publication.
Timeline:
Let be a finite set and the transition matrix of an irreducible Markov chain on , reversible with respect to a probability distribution :
The operator is self-adjoint on , with inner product , so its eigenvalues are real. Write and let be the smallest eigenvalue of .
The graph of the chain has vertex set , an edge from to when , and a self-loop at when . An odd closed path at is a sequence of edges from back to , with an odd number of edges, in which no directed edge is traversed twice. Its length is
A system of odd paths chooses one such path for every point, and its load is
the maximum over directed edges of the weighted length of the paths through (display (1.7) of the paper).
For the random walk on a graph , when , with the degree, and . There is the maximum degree, the largest number of edges of a path in , and .
For an irreducible, aperiodic, reversible chain and every system of odd closed paths,
Proposition 2 turns aperiodicity into a number. With Proposition 1, which bounds through paths between pairs of points, it bounds the absolute spectral gap entirely in terms of path geometry, and so bounds the variation distance to stationarity through Proposition 3. Corollary 2 is the form most often applied: for a random walk on a non-bipartite graph, a choice of short odd cycles that do not crowd any single edge certifies that the walk does not oscillate.
Proposition 2 and its corollary are proved in the paper. As far as a search of the platform shows, no machine-checked proof exists. The platform already has the vocabulary (stochastic matrices, stationarity, reversibility, eigenvalues and the inner product, from the published Levin–Peres–Wilmer layer) and the qualitative fact that is not an eigenvalue of an irreducible aperiodic chain. This mission adds the quantitative bound, the identity (1.8), and the path inequality, all reusable for other path-based eigenvalue estimates.
Each step is elementary, but the bookkeeping is where a proof can go wrong. The Cauchy–Schwarz step is applied along each path separately, and the resulting double sum over points and over the edges of their paths must be exchanged into a sum over edges. That exchange is exact only if each path traverses each directed edge at most once. A path that crosses an edge twice contributes twice, while counts it once. Self-loops are edges here, and the sum over directed edges in the last step must match the sum over ordered pairs , including , in the identity (1.8). The alternating signs work only because the number of edges is odd; an even closed path cancels instead of doubling it.
The bound is also only as good as the chosen paths: short odd cycles that spread their load over many edges give a small , and the choice of is part of every application.
The chain is a real matrix P : Matrix V V ℝ on a Fintype V, with the published predicates IsStochastic, Irreducible, Aperiodic, IsStationary (which includes that is a probability vector) and DetailedBalance. is edgeMeasure, the inner product innerPi, eigenvalues IsEigenvalue (a real eigenvalue with a nonzero real eigenfunction). is the infimum of the real eigenvalues of , a minimum for a stochastic matrix on a nonempty set.
Paths are vertex lists. A path traverses the directed edges between consecutive vertices, each with . The paper defines "by analogy with (1.4)", whose paths may not repeat an edge. For the directed edges of §1C this rule is read as "no directed edge twice". Under the unordered reading a vertex of degree one would have no odd closed path, contradicting the page's remark that such paths always exist for irreducible aperiodic chains. is a real supremum over the finite set of directed edges with , and it is only when there is no edge. A system of odd paths on a nonempty set excludes that case, so the bound is never reduced to by . The system is a universally quantified hypothesis of every statement, never an existential one. No milestone assumes the inequality of milestone 3 or the identity (1.8) as a hypothesis. No assumption is made.
Milestones 3 and 4 do not assume aperiodicity: the existence of an odd path system implies it. The identity (1.8) assumes only stochasticity and stationarity. Corollary 2 assumes only that the graph is connected and not 2-colorable; the chain properties follow from these. In Corollary 2, counts paths through a directed edge, which is at most the count through the unordered edge, so the stated bound implies the one with the unordered count. Only the first half of Remark 1.3 is stated; its second half needs Proposition 1's quantity, which belongs to another mission of the series.
Contributions welcome: proofs of the milestones in order, a general Cauchy–Schwarz-along-paths lemma shared with the Poincaré inequality, and the existence of odd path systems for irreducible aperiodic chains.
How fast a finite Markov chain forgets its starting point is the central quantitative question in the analysis of Monte Carlo algorithms, card shuffling and random walks on groups. The classical tool is the spectral gap , which controls convergence in but loses a factor when converted into a bound for a chain started at a point. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996) 695–750) brought the logarithmic Sobolev constant , introduced by Gross for Gaussian measures (Amer. J. Math. 97 (1975)), into the study of finite chains, and showed that it gives sharper mixing bounds in many examples.
The entropy route to ergodicity is the cleanest consequence of a log-Sobolev inequality: the relative entropy of the chain's law with respect to stationarity decays exponentially at rate , and at rate for reversible chains. The paper notes that the reversible case is contained in Bakry's Saint-Flour lectures (Lecture Notes in Math. 1581, 1994) and Stroock's notes on Gibbs states (Lecture Notes in Math. 1563, 1993), and that Miclo (preprint, 1995) treated the nonreversible case.
Let be a finite set and a Markov kernel: and . Let be an invariant probability, , with for every . Functions act on the right, , and is the inner product of , with norms . The chain is reversible if for all .
The continuous-time heat semigroup is
acting on functions by and on probability measures by . The row is the law at time of the chain started at .
The Dirichlet form is ; it is bilinear but not symmetric unless the chain is reversible. With
the log-Sobolev constant is
The relative entropy of a probability is , and the total variation distance is .
For every probability measure on ,
and, if is reversible,
For an irreducible chain, every and ,
with replaced by for reversible chains.
Theorem 3.6 turns a single functional inequality into a convergence statement valid for every initial law, with no spectral assumption and no reversibility in the first half. Through Pinsker's inequality it gives (3.3), whose prefactor replaces the factor of the spectral bound . When is exponentially small in the size of the problem, as for random walks on large groups or product spaces, is polynomial where is exponential, and the time needed to make the bound small drops accordingly. This is the mechanism behind the sharp mixing bounds the paper derives from .
The results are proved in the paper and are classical; they are not, to our knowledge, formalized. The platform has measure-theoretic statements of Pinsker's inequality and the published finite Markov chain vocabulary of Levin–Peres–Wilmer (stochastic matrices, stationarity, total variation, the heat kernel), but nothing about log-Sobolev constants of finite chains, the entropy derivative along a Markov semigroup, or entropy decay. A formal development provides the entropy layer of the finite-chain theory: the adjoint semigroup, the dissipation identity, the comparison of with , and Pinsker's inequality in the encoding used by the mixing-time library.
The statement is about measures, while the natural quantities to differentiate are densities with respect to , and for a nonreversible chain the density of evolves under the adjoint semigroup, not under . The Dirichlet form is not symmetric, so the order of its arguments matters at every step, and the improvement from to holds only under reversibility.
The obvious first idea, differentiating term by term, meets wherever the density vanishes. The initial law may be a point mass, and for a reducible chain the density can stay zero at positive times. The argument must therefore handle the boundary and the degenerate laws separately from the smooth interior. The constant is defined as an infimum over all functions, with no claim that it is attained or positive.
The state space is a Fintype with decidable equality, is a real matrix with the published predicate MarkovMixing.IsStochastic, satisfies MarkovMixing.IsStationary K π and for all , and reversibility is MarkovMixing.DetailedBalance K π. is the published MarkovMixing.heatKernel K t (the Poisson series), the adjoint kernel is MarkovMixing.timeReversal K π, and total variation is MarkovMixing.tvDist. Time is real, and the decay statements are for .
The local definitions are , the norms , , as a real infimum over the ratios with , , and as the row vector . Lean's Real.log 0 = 0 implements . The goal does not assume irreducibility: it is true for every stochastic with a positive invariant probability, and a reducible chain has . The companion (3.3) keeps irreducibility, the standing assumption of Section 3. In Lemmas 2.5 and 2.7 the paper's is strengthened to , because is at a zero of on the page and in Lean.
Several encodings would make the goal trivially true and are ruled out. is not assumed positive. is a probability, since for the entropy is a positive constant in . is invariant and positive, so is meaningful. The eigenvalue-based MarkovMixing.spectralGap is not used. Applying to as a function, , is not the same as for a nonreversible chain.
A complete development needs: termwise differentiation of the heat-kernel series and the semigroup property ; the adjoint identity for ; elementary convexity inequalities for and ; the symmetric form of for reversible chains; Pinsker's inequality on a finite set; and a scalar Grönwall lemma. The heat-kernel calculus and Pinsker's inequality in the MarkovMixing.tvDist encoding are reusable by the other missions of this series and by any mixing-time development. Proofs of individual milestones are welcome independently of the goal.