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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
A disjunctive normal form (DNF) is a disjunction of terms, each term a conjunction of Boolean literals. An unambiguous DNF has pairwise disjoint terms: no Boolean assignment satisfies two different terms. This restriction makes several tasks easy. In particular, the cited open-problem entry records polynomial-time algorithms for weighted satisfiability on unambiguous DNFs and for unweighted falsifiability. The unresolved boundary is weighted falsifiability: can one find a high-weight assignment outside the union of the terms, without enumerating all assignments?
This question is relevant to the complexity of negating compact representations of Boolean functions. Amarilli's entry observes that, since unambiguous DNFs are d-DNNFs, a polynomial-time negation procedure for d-DNNFs would yield a polynomial-time solution to weighted falsifiability on unambiguous DNFs by applying weighted satisfiability to the negated representation. Conversely, if weighted falsifiability for unambiguous DNFs—or even for d-DNNFs—is NP-hard, then, unless , d-DNNFs cannot be negated in polynomial time. These are implications stated by the source, not results established by this mission.
The question appears on Albertine Amarilli's open-problem list. The entry cites a Theoretical Computer Science Stack Exchange question by Mikaël Monet and credits him with helping prepare the entry. It records two partial tractability results: weighted satisfiability with binary weights, and weighted falsifiability when the variable weights are unary. The entry gives no date for when the problem was posed or last seen open, so this description does not assign one. The linked discussion is useful context, not a novelty or resolution certificate.
Let be exactly the variables occurring in the DNF. The formal input declares this finite universe by its size ; validity requires every declared variable to occur in at least one literal. An input DNF is a finite list of terms, and each term is a finite list of signed variable indices. An assignment is a function . A positive literal is true when ; a negative literal is true when . A term is true when all its literals are true, and the DNF is true when at least one term is true. Thus the empty DNF is false and an empty term is true.
The input also contains one positive integer weight for each variable and a positive threshold . The weight of an assignment is
The DNF is valid for this problem when every literal index is below and every pair of distinct terms is mutually unsatisfiable. The decision question is whether there exists an assignment that falsifies the DNF and has weight at least .
For valid unambiguous DNF inputs with positive binary-encoded weights and threshold, the decision problem asking whether a satisfying assignment has weight at least has a deterministic polynomial-time algorithm. This is the weighted-satisfiability baseline recorded in the source entry. It is a separate result from the goal below.
For the same valid DNF model, when each variable weight is encoded in unary, weighted falsifiability has a deterministic polynomial-time algorithm. The threshold remains binary-encoded in this formalization. The source entry records this unary-weight restriction as tractable.
For arbitrary positive binary-encoded variable weights and a positive binary-encoded threshold, determine whether one fixed deterministic Turing machine and one polynomial time bound decide weighted falsifiability for every valid input. The machine must be correct on all valid instances; its running-time bound is uniform and measured in the length of the explicit input code. No witness output is required.
The two partial results are reference points, not assumptions from which the goal is claimed to follow. The goal is the open binary-weight case; it must not be replaced by the satisfiability problem or by the unary-weight restriction.
Input, semantics, validity, and serialization definitions
├── binary-weight weighted satisfiability (source baseline)
├── unary-weight weighted falsifiability (source baseline)
└── binary-weight weighted falsifiability (open goal)
Each branch shares the same finite DNF model and correctness predicates. The arrows indicate required definitions and scope, not a claim that either partial theorem implies the open goal.
A positive result would give a uniform algorithm for finding whether a disjoint union of Boolean subcubes omits any sufficiently heavy point, even when weights are represented compactly in binary. A negative complexity result would identify a sharp obstruction to efficient complement-related operations on these representations. The exact-weight version (asking for weight exactly ) is a different problem and is outside this mission's scope; the goal here is specifically weight at least .
Formalizing the question fixes the universe of variables, signed-literal semantics, unambiguity condition, threshold direction, input encoding, and computational model. It also makes the unary and satisfiability baselines comparable to the binary-weight goal without treating a finite search or a candidate implementation as a complexity proof. No solution is supplied or presumed here.
The direct search over all assignments is exponential in . Counting satisfying assignments is enough to settle ordinary falsifiability, but a weighted threshold partitions assignments by exponentially many possible total weights when the weights are binary. The unary dynamic program therefore does not by itself give a polynomial bound in the binary input length. Conversely, solving weighted satisfiability on the DNF does not answer whether a heavy assignment lies outside it. The task is to settle that gap without silently replacing binary magnitude by unary size.
The Lean model uses Input, an explicit variable count, a list of signed-index terms, a weight list, and a threshold. validInput requires exactly one positive weight per variable, positive weights and threshold, in-range literal indices, that every declared variable occurs in the formula, and pairwise unsatisfiable distinct terms. The finite assignment type is Fin n → Bool; unused variables remain part of the input. The decision predicate is existential and exact.
The binary code includes the variable count, every list count and delimiter, all signed indices, all weights, and the threshold. Natural-number payloads use canonical binary digits with an explicit unary length prefix. The unary-weight code changes only the variable-weight payloads to unary; formula data and threshold remain binary. The complexity statements use Mathlib's bundled deterministic Turing.TM2ComputableInPolyTime model, with a single machine and polynomial bound in the chosen code length. This formalization does not claim refinement to JSON, CPython, or any runtime implementation. Human review should check the encoding/decoder round-trip and the source correspondence before launch.
The reusable definitions are the finite DNF semantics, weighted assignment score, validity predicate, binary/unary encoders, and exact decision predicates. Formalizing the two cited partial results is part of the mission's milestone path; neither is evidence that the binary-weight goal is solved.
Many queues observed at well-chosen instants are Markov chains on the nonnegative integers. For the single-server queue with Poisson arrivals and general service times (M/G/1), D. G. Kendall showed in 1951 that the number of customers left behind at successive departure epochs is such a chain, the imbedded Markov chain (Kendall 1951; Kendall 1953). Whether the queue settles into a steady state, keeps returning to empty without settling, or grows without bound is then a question about this chain: is it ergodic, null recurrent, or transient?
F. G. Foster's 1953 paper (doi:10.1214/aoms/1177728976) answers this question by first proving general criteria for an irreducible chain on , stated as solvability conditions for linear inequalities in the transition matrix, and then applying them to the M/G/1 and GI/M/1 chains. Theorem 2 of the paper is the drift condition now known as Foster's criterion, the starting point of the Lyapunov-function method for the stability of queues and stochastic networks (Meyn and Tweedie 2009). This mission is the M/G/1 half of the paper.
Timeline:
A Markov chain on the states is given by a transition matrix : and for every row . Write for the probability that the chain started in first reaches (for , first returns to ) at step . The chain is irreducible if every state can be reached from every other, and aperiodic if for every state the return times have greatest common divisor . A state is recurrent if and transient if ; a recurrent state is ergodic (positive recurrent, "recurrent-nonnull") if in addition its mean recurrence time is finite. The mean first-passage time from to is .
The M/G/1 matrix is built from a sequence of positive numbers summing to one ( is the probability of arrivals during one service):
that is, and, for , when and otherwise. The traffic intensity is
the mean number of arrivals per service.
The goal leaves arbitrary apart from positivity and normalization; in particular is allowed and falls in the transient case.
The result. The classification is the stability theorem for the M/G/1 queue: for the departure-epoch queue length has a stationary distribution, which is what the Pollaczek–Khinchine formula describes; for the queue empties infinitely often but has no steady state; for it grows without bound. The general criteria behind it (Theorems 2, 4, 5) apply to any chain on the nonnegative integers and are reused in the companion GI/M/1 mission and throughout queueing and Markov-chain stability theory.
Formalizing it. All results here are proved on paper (Kendall and Foster, 1951–1953, with Theorems 3 and 7 classical lemmas from Feller). None of them is known to have a machine-checked proof against a Lean development of countable-state Markov chains. The mission produces such proofs on the published discrete-chain vocabulary (transition matrices, first-passage probabilities, return probabilities, positive recurrence), together with the general Foster criteria as reusable theorems. Theorem 2 is already posed as an open platform theorem and is reused here.
The queue-specific part of the argument is short once the general criteria are available; the weight of the mission is in those criteria. They relate qualitative properties of an infinite chain (ergodicity, recurrence, transience) to solvability of infinite systems of linear inequalities, and this needs limit behaviour of the -step probabilities and of hitting probabilities of state , none of which follows from finite-state arguments. Two further points resist the naive approach. The converse directions (ergodic , recurrent ) need exact identities for mean first-passage times, not just bounds, and these must be handled in because the means may be infinite. And the boundary case (null recurrence) separates the two equivalences: an argument that only compares the mean drift with , such as a law of large numbers for the increments, cannot tell recurrence from transience there.
QueueingFundamentals.Foundations.TransitionMatrix (entries P.p i j, rows summing to as a HasSum), with its firstPassage, returnProb, Irreducible, Aperiodic and PositiveRecurrent. "Ergodic" is P.PositiveRecurrent; aperiodicity is the paper's standing assumption and is not folded into it a second time.i ≠ 0.mg1Matrix k : ℕ → ℕ → ℝ; the goal and the §3 display quantify over every TransitionMatrix P with P.p = mg1Matrix k. Such a P exists for every admissible k (checked in a sorry-free local file for ).Summable or HasSum); Theorem 3's equation (6) is written as in together with finiteness of the , .Ruled out: as a real tsum (which is for a divergent series and would call a heavy-tailed chain ergodic); defining "ergodic" or "recurrent" through the existence of Lyapunov or drift functions (which would make the criteria tautological); a goal over a matrix that need not exist.
Contributions welcome: proofs of the general criteria (Theorems 2–5) on the published chain vocabulary, the limit theorem for irreducible aperiodic chains, first-step analysis for hitting times, and Theorem 7 as a lemma on probability generating functions; all of these are reusable beyond this mission.
Temporal-difference (TD) learning estimates the value function of a Markov chain — the expected discounted sum of future rewards from each state — from a single stream of observed transitions, without knowing the transition probabilities. With a linear function approximator the value of state is represented as for a feature vector and a parameter . Classical TD() updates by stochastic approximation, and its behaviour depends on a step-size schedule that must be tuned.
Bradtke and Barto (Machine Learning 22, 1996) replaced the stochastic-approximation update by a least-squares solve: LS TD (Eq. (11)) recomputes at every step as the instrumental-variable least-squares solution of the empirical consistency condition. The method, later generalized as LSTD() by Boyan (Machine Learning 49, 2002), is the basis of least-squares policy iteration and of the "LSTD" methods in standard reinforcement-learning texts (Sutton and Barto, Reinforcement Learning, 2nd ed., 2018, §9.8). Its appeal is that it has no step size; the question this mission formalizes is whether it nonetheless converges, with probability one, to the true parameter.
Timeline. Sutton (1988) introduced TD(). Watkins and Dayan (1992) and Tsitsiklis (1994) proved probability-one convergence of tabular TD(0) and Q-learning. Bradtke and Barto (1996) proved probability-one convergence of LS TD on absorbing chains (Theorem 1) and on ergodic chains (Theorem 2). Tsitsiklis and Van Roy (IEEE TAC 42, 1997) proved convergence of linear TD() with general features on ergodic chains.
A finite Markov chain on a finite nonempty set is a matrix with and . A transition earns reward ; the expected reward out of is . For a discount factor the value function is
The chain is ergodic (Kemeny and Snell) if every state can be reached from every state: for all there is with . An invariant distribution is a probability vector with ; write .
Each state has a feature vector ; is the matrix with rows . The true parameter is a vector with for all .
The algorithm (Figure 3) starts at an arbitrary state , lets the chain move , and after transitions computes
the sums running over the transitions observed so far.
If is ergodic, (1) is linearly independent, (2) each has dimension , and (3) , then is finite and, from any initial law,
The goal leaves the chain, the rewards, the features and the initial law arbitrary.
The result. Theorem 2 shows that an LS TD learner running on one long trajectory recovers the exact value function whenever the features can represent every function on the states, with no step-size schedule. It is the step-size-free counterpart of the tabular TD(0) convergence theorems and the starting point for the later analysis of LSTD with fewer features than states, where the limit is the TD fixed point rather than . Lemma 5 is the general identification of that fixed point as the almost-sure limit of LSTD.
Formalizing it. The result is proved in the paper; it has not been machine-checked. A formalization adds three things the paper delegates: the strong law of large numbers for occupation times of a finite irreducible Markov chain, which the paper cites to Kemeny and Snell and which is not in Mathlib; the per-state transition frequencies used in the first sentence of the proof of Lemma 5; and the linear algebra of the limit. The first is reusable well beyond reinforcement learning.
The algebra is short once the empirical averages in (11) are known to converge. The difficulty is probabilistic: the averages are over a dependent sequence, so the ordinary strong law of large numbers does not apply. Two facts are needed: that the fraction of time in each state converges to almost surely for any starting law, including periodic chains, where itself does not converge; and that, among the visits to , the fraction followed by a move to converges to , which needs the strong Markov property at successive visit times. Neither follows from convergence of the chain's distribution, and neither holds for a chain started at a fixed state without an argument that every state is reached.
X with Fintype, DecidableEq, Nonempty, a row-stochastic matrix P : Matrix X X ℝ (structure Chain), rewards R : X → X → ℝ, features φ : X → Fin m → ℝ. Condition (2) is m = Fintype.card X; condition (1) is LinearIndependent ℝ φ.tsum is on a divergent series, so "θ* is finite" is stated as convergence of the series together with existence of with . is existential, never defined as Lemma 5's limit.Needed infrastructure: the strong law for occupation times of a finite irreducible chain under an arbitrary initial law (milestone 1), the strong Markov property at visit times, positivity of the invariant distribution of an irreducible chain, and the invertibility of for . Contributions to any of these, as standalone lemmas, are welcome.
A supplier who sells to a retailer at a per-unit wholesale price above her own production cost induces the retailer to order less than an integrated firm would. This effect, double marginalization, goes back to Spengler (1950) and is the standard benchmark against which supply chain contracts are judged: a contract coordinates the channel if it makes the decentralized decisions coincide with the integrated optimum. Revenue-sharing contracts, as used in the video-rental industry, coordinate the channel; the plain wholesale-price contract does not. Whether a supplier should bother with the administrative cost of revenue sharing depends on how much the wholesale-price contract actually loses and how much of the remaining profit the supplier keeps.
Cachon and Lariviere answer that question for a retailer whose revenue depends only on the quantity ordered, in Section 4.1.1 of their working paper Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations (June 2000; the 2005 Management Science version renumbers and revises the material). They show that the answer is governed by the curvature of the marginal revenue curve, and they compute it exactly for a one-parameter family. The source is the June 2000 working paper, whose results are unnumbered; every item cites its section, page and display.
A supplier produces at unit cost and sells to a single retailer. The retailer's expected revenue from units is , where , is strictly concave and differentiable on with derivative (the marginal revenue), is differentiable on with derivative , the product is viable (), and a finite quantity is optimal ( for some ). The supply chain profit is ; the integrated quantity maximizes over .
Under a wholesale-price contract with price , the retailer orders to maximize . Each order is induced by exactly one price, , so the supplier can be thought of as choosing . Her profit, the retailer's profit, and their sum are then
Following the paper, is assumed decreasing, which makes unimodal. The supplier's optimal quantity to induce maximizes over , and is her optimal wholesale price. The efficiency of the contract and the supplier's profit share are
In the α-family, for and , so : marginal revenue is convex for , linear for and concave for .
For and , the quantities and are the unique maximizers of and on , the profit share is , and
a quantity that does not depend on , is strictly increasing in , tends to as and to as .
The general milestones turn the paper's area argument (the triangle under the tangent to marginal revenue at ) into three comparisons: convex marginal revenue makes the wholesale-price contract worse for the chain and leaves the supplier at most two thirds of a smaller pie, concave marginal revenue the opposite. The α-family makes the trade-off exact: efficiency never falls below , while the supplier's share moves much faster than efficiency, which is the paper's argument for why revenue sharing is most attractive when marginal revenue is convex.
These results are proved on paper but, to our knowledge, not machine-checked anywhere; Mathlib has no supply chain contract theory. The formalization provides a reusable single-retailer wholesale-price model, a checked version of the convex/concave tangent comparisons, and a corrected statement of the α-family's monotonicity (see the scope section).
The general comparisons are short on paper but rest on a picture: they need the first-order condition at an interior maximizer, the tangent-line inequality for a convex or concave derivative, and the fundamental theorem of calculus for a function whose derivative is known only on a half-line and one-sided at . Strictness needs a strictly positive integrand on a nondegenerate interval.
The α-family is where the analysis is not routine. The closed forms involve real powers with exponents and , which must be combined carefully. The limit as is classical, but the monotonicity of on all of is not a one-line derivative sign check: the derivative mixes with rational terms, and its sign has to be established uniformly near and near .
Quantities and prices are real numbers. "Optimal" always means a maximizer over all admissible quantities (IsMaxOn on , or on in the α-family, as the page restricts), never a root of a first-order condition. The derivative of the general model is linked to by a one-sided derivative hypothesis on ; is required only on , since for it blows up at . In the α-family the marginal revenue is deriv of , not a separate function, and is assumed (implicit on the page: and ). Efficiency and profit share are real divisions; their denominators are positive at the optimal quantities.
Deviations from the page, all disclosed in the items:
A trivializing formalization is ruled out: the efficiency in the goal is the ratio of profits computed from at the maximizers, not a definition equal to , and the maximizers are characterized as unique argmaxes rather than assumed.
Welcome contributions: proofs of the general tangent comparisons, which are reusable for any concave revenue model; the real-analysis lemmas on ; and the α-family closed forms.
Impulse control models an agent who acts on a random system through discrete interventions, each with a fixed cost: inventory replenishment, cash management, exchange-rate interventions by a central bank. With two agents whose objectives conflict, the problem becomes a nonzero-sum stochastic differential game with impulse controls. Before the work of Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; preprint arXiv:1605.00039), such games had no general verification theorem and few explicit equilibria; the paper supplies both. Its main application, formalized in this mission, is a game between two central banks with different targets for an exchange rate, a two-player version of the exchange-rate control models of Bertola, Runggaldier and Yasuda and of Cadenillas and Zapatero (references [10], [12] of the paper). The paper proves that this game has an explicit one-parameter family of Nash equilibria of threshold type, with closed-form payoffs.
The state is a real process. Without interventions it is , where is a standard real Brownian motion and . Player 1 may shift it up by impulses , player 2 down by impulses :
Player 1 earns the running payoff , player 2 earns , with . An impulse costs its author and pays the opponent . Payoffs are discounted at rate . The standing assumptions are , , and .
A strategy of player is a pair : an open continuation region and a continuous impulse map . Player intervenes when the state leaves , applying the impulse ; player 1 has priority when both want to act. This rule defines the controlled process and the interventions inductively. Player 's payoff is
A pair is -admissible, , when these random variables are integrable, has all moments, and neither player's interventions accumulate in finite time. A Nash equilibrium is an admissible pair from which no player gains by deviating to any strategy that keeps the pair admissible.
The explicit objects are , and
From the zero of and a free parameter , the formulas (4.20)–(4.21) give thresholds , targets , coefficients , the functions and the piecewise candidates of (4.6). These are linear outside and equal inside.
For every and every initial state , the threshold strategies
form an -admissible Nash equilibrium, and
Milestones 1–3 are deterministic real analysis; milestone 4 and the goal are probabilistic.
The result gives explicit equilibria, with explicit thresholds and payoffs, for a nonzero-sum stochastic game with impulse controls. Such games rarely have closed-form solutions. The equilibria form a continuum indexed by : equilibrium payoffs are not unique, and every equilibrium in the family is a translate of a fixed interval policy. The explicit formulas also support the comparative statics of Section 4.4, where the continuation region widens as the fixed cost grows.
Proposition 4.7 is proved in the paper by applying its verification theorem (Theorem 3.3) to . The admissibility estimate (4.26) is written out only for initial states ; the general case is said to be similar. As far as is known, none of these results has a machine-checked proof. A formal proof would check every regularity, pasting and admissibility condition. It would also yield a reusable pathwise construction of impulse-controlled Brownian motion.
The deterministic milestones need careful algebra with nested logarithms and square roots. Proving Lemma 4.6 requires the global shape of , which needs the sign pattern of from Proposition 4.2, not only local conditions at the thresholds.
The goal is harder. The Nash inequality must hold against every admissible deviation: any open continuation region and any continuous impulse map, not only threshold strategies. Comparing payoffs therefore needs a verification argument, namely Itô's formula for a function that is only piecewise and across the thresholds, applied along a process with an unbounded number of jumps, plus a localisation that uses the moment condition (2.8). Admissibility needs a renewal-type bound on the discounted number of interventions, built from i.i.d. exit times of Brownian motion from an interval.
The Lean development lives in the namespace ImpulseGames.LinearGame.
Model with the proposition Model.Standing. The added hypothesis appears in every statement that uses : with , which the standing assumptions allow, has no zero in and the family (4.20) does not exist.IsBrownianReal W P on a probability space, with time in . Definition 2.2 is formalized pathwise: exit times in with , the tie rule favouring player 1, and for the tail of each impulse control. No SDE or stochastic integral appears in any statement; the uncontrolled dynamics are .Two slips of the page are corrected. First, the paper's impulse maps are not -valued on all of ; they are replaced by and , which agree with them wherever each player acts. Second, in Lemma 4.6 the maximiser (4.23) is not unique when , in the opponent's intervention region (all impulses tie there). The statement asserts maximality everywhere and uniqueness outside that region.
A complete development needs: elementary real analysis for milestones 1–3; a pathwise theory of piecewise-defined processes; an Itô formula for Brownian motion with , piecewise- functions; and exit-time estimates for Brownian motion. The last two are reusable well beyond this mission. Proofs of the deterministic milestones are welcome independently of the stochastic part.
Sequential decisions often change the distribution of future states. A planner choosing an action today must account for both its immediate reward and the later rewards made possible by the resulting state. The mathematical question is whether an optimal rule can be chosen once and reused at every stage, even when a competing plan may randomize and use the entire observed history. In Discounted Dynamic Programming, Blackwell studies this question on general Borel state and action spaces, beyond the finite models in which a direct comparison of actions is available.
The paper distinguishes several strengths of optimality. For each distribution of the initial state, an approximately optimal stationary plan exists, but a single plan that is approximately optimal at every initial state need not exist in a general Borel problem. Essential countability of the actions restores uniform approximate stationary optimality; essential finiteness yields exact stationary optimality. These are different mathematical claims, and the mission keeps their different quantifiers visible. Blackwell 1965, pp. 227, 229, 232–234.
A state is an element of a nonempty standard Borel space , and an action is an element of a nonempty standard Borel space . The transition kernel gives a probability distribution for the next state after action in state . The reward may depend on that next state ; it is bounded and Borel measurable. Future rewards are discounted by with . These are the objects of Blackwell’s Sections 2–3. Blackwell 1965, pp. 227–228.
A plan assigns a probability distribution of actions to each possible history before a decision. At stage , that history contains completed state-action pairs and the current state. Thus plans may randomize and depend on earlier states and actions. A Markov plan instead uses a Borel function at each stage; a stationary plan uses the same function at every stage and is denoted . Starting from state , the plan has discounted expected return
Here and are the state and action at stage . The comparison class for an optimal plan is all such plans, including randomized and history-dependent ones. Blackwell 1965, pp. 228–229.
Two actions are equivalent at state when they have the same reward for every next state and the same transition measure . An action set is essentially countable by a Markov plan if, for every , one of the actions is equivalent to at . It is essentially finite by that plan if has a countable Borel partition such that, for , one of is equivalent to every action at . A finite action set is a special case. Blackwell 1965, pp. 233–234.
For a probability distribution on and , -optimality asks for a stationary with
Theorem 6(b) asserts that such an always exists. Under essential countability, Theorem 7(a) obtains a stronger, uniform -optimality statement: for every there is a stationary with for all . Its other targets identify the optimal return with the fixed point of the operator and with the unique bounded solution of the optimality equation . Blackwell 1965, pp. 232–234.
The mission’s goal is Theorem 7(b). Under essential finiteness, it asks for a stationary with exact optimality:
The milestone list also includes the paper’s operator identity, approximate selection result, contraction criterion, generated-plan comparison, and upper-bound criterion. Each has its own source index and statement. Blackwell 1965, pp. 231–234.
The exact result says that, under a condition weaker than a globally finite action set, repeated use of one measurable state-based rule matches or exceeds the return of every adaptive randomized plan. It is a structural result about what information and randomization can add to discounted control. The preceding approximate results specify what can still be guaranteed when that condition is relaxed; Blackwell’s examples show that the distinctions cannot simply be ignored. Blackwell 1965, pp. 229–230, 234.
Blackwell proved these statements in 1965. The formalization work here is to give machine-checked proofs for the Borel-space model and its full comparison class, together with reusable definitions of history-dependent kernels, returns, stationary rules, and Bellman operators. The draft theorem statements compile as Lean declarations, but their proofs remain open. The milestone results are intended to make both the final theorem and its supporting measure-theoretic objects independently usable.
On an uncountable Borel action space, the pointwise supremum of available action values does not automatically come with a Borel action selector. Choosing a maximizing action separately at each state may fail to define a measurable rule, and a supremum need not be attained. Also, a Markov or stationary comparison cannot by itself certify optimality against plans that depend on full histories. These issues are real in the paper’s examples: general Borel problems may lack an -optimal plan, and a given plan need not be uniformly approximated by a Markov plan. Blackwell 1965, pp. 229–230.
The Lean model uses nonempty StandardBorelSpace types for and . “Baire function” is read as Borel measurable on these metrizable spaces. The problem stores a Markov transition kernel, a bounded measurable real reward on , and ; is included. A plan contains a probability kernel on each finite history, and the return is the actual absolutely convergent series of expected one-stage rewards. The first decision is indexed by in Lean, corresponding to the paper’s index . The finite history law is assembled through kernel composition products, and a stationary rule is represented by deterministic kernels. The integrals and series therefore express the paper’s expected return, including the cases where the reward depends on the next state.
For the operator results, means bounded and measurable real functions. The suprema defining and the optimal return are real suprema over nonempty families bounded by the reward and discount; they are used only in that setting. The abstract operator in Theorem 5 maps into itself. The action equivalence predicate uses the paper’s explicit equality of reward functions and transition laws; the later “i.e.” phrasing on p. 234 is weaker when interpreted as equality of operators alone. A partition piece may be empty, and Lean’s piece corresponds to the paper’s , with rules .
An optimality claim here always compares with every randomized history-dependent plan. Restricting that quantifier to Markov or stationary plans would trivialize the target. A complete development needs measure-theoretic facts about history laws and their bounded integrals, the discounted series, measurable partitions and selections, and the sup-norm contraction of bounded Borel functions. The history-law and bounded-function infrastructure can be reused outside this mission. Contributions to those foundations and to the numbered milestone theorems are welcome.
In network design games, selfish users build a shared network and split the cost of every edge among the users of that edge. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008), DOI 10.1137/070680096) studied the fair connection game, in which the cost of an edge is shared equally (the Shapley value) among its users. In this game the worst equilibrium can cost times the optimum, so the relevant measure is the price of stability: the ratio between the cheapest pure Nash equilibrium and the optimal centralized design. Their Theorem 2.1 bounds it by the harmonic number in every directed graph, and that bound is tight for directed graphs.
For undirected graphs the paper notes that is not tight and calls the correct bound "an interesting open problem". Its Section 4 settles the smallest case: two players with a common terminal. The general theorem gives there; Claim 4.1 improves this to , and a three-node example shows that is the right value.
Timeline. Rosenthal (1973) showed that congestion games have pure Nash equilibria through a potential function. Anshelevich et al. (FOCS 2004; journal version 2008) introduced the price of stability for the fair connection game, proved the bound and the two-player undirected bound treated here. Subsequent work studied the undirected multi-player case, which remains without a matching upper and lower bound in general.
Let be a finite undirected simple graph, with a cost on every edge . There are two players, a common terminal and personal terminals . A strategy of player is a set of edges that connects with : in the graph , and lie in the same connected component. A profile is a pair of strategies.
Under fair cost sharing each edge is paid for equally by the players using it. With the number of players whose strategy contains , player pays
A pure Nash equilibrium is a profile in which no player can lower its payment by switching to another strategy while the other player's strategy stays fixed. The total cost of a profile is the cost of the network it builds,
For a set of edges write . For a profile , the quantities , and split the total cost into the private and the shared parts.
The game is an instance of a congestion game, with per-user latency on edge ; the mission builds on the published congestion-game layer CongestionPoA.AsymSum.Model.
If the game has a profile, then some pure Nash equilibrium satisfies
Moreover, in the three-node example (nodes , edges of cost , edge of cost , with ) the cheapest pure Nash equilibrium costs exactly and the optimum costs exactly , so the ratio approaches .
The result shows that the price of stability of fair cost sharing depends on the network: the bound, tight for directed graphs, is not tight for undirected ones even with two players. It is the first undirected bound below and the starting point for the later study of undirected fair network design, where the question for many players is still open.
The theorem is proved in the paper; this mission formalizes it. A search of the Prove2Me library found no formalization of the price of stability of fair connection games. Beyond the theorem itself, the mission produces a reusable undirected layer over the congestion-game library: connectivity strategies stated with Mathlib's graph reachability, fair cost sharing as a congestion game, and the total-cost functional. A checked proof of the potential inequality (4.1) is the two-player case of the potential argument behind Theorem 2.1.
The obvious argument starts from an optimal solution, follows improving moves to an equilibrium and compares potentials. For two players this only yields the factor : the potential counts shared edges with weight , so a potential inequality alone cannot rule out an equilibrium in which both players share expensive edges. The improvement to needs a second inequality, (4.2), obtained from a specific deviation of each player in the equilibrium, and that deviation is valid only because of the undirected structure: the private parts of the two optimal paths together connect with , and the deviating player can then follow the other player's equilibrium route to . Making this connectivity claim precise for edge sets rather than drawn paths is where the formal work lies. It holds when the optimal strategies are inclusion-minimal, which is why the deviation milestones carry that hypothesis.
Fintype with decidable equality; edges are unordered pairs Sym2 V; the graph is a SimpleGraph V. Edge costs are a real function c with 0 ≤ c e for every e.i : Fin 2 (the paper's players 1 and 2 are 0 and 1) is a Finset of edges contained in G.edgeSet such that t i and s are Reachable in SimpleGraph.fromEdgeSet. Strategies are not restricted to paths.CongestionGame from CongestionPoA.AsymSum.Model with latency ; profiles, player costs and pure Nash equilibria are that library's IsProfile, cost and IsPureNash.Contributions welcome: a proof of the potential inequality (finite improvement paths in the two-player fair game), the graph-theoretic lemma that the symmetric difference of two simple paths with a common endpoint connects their other endpoints, and a computation of the three-node example.
Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.
Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the -stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.
Let (states) and (controls) be sets, and for each let be a nonempty control constraint set. Write and let be the set of all functions , ordered pointwise. A mapping is given, subject to the Monotonicity Assumption: implies for all , .
A selector is a function with for all . A policy is a sequence of selectors. Define
and let be the -fold composition of . A terminal function with for all is fixed. The -stage cost of and the -stage optimal cost are
A policy is uniformly -stage optimal if each tail is -stage optimal, and -stage -optimal if where and where .
The three conditions on used in the chapter are F.1 (continuity of along nonincreasing sequences with ), F.2 (there is with for all ), and F.3 (a quantitative selection property with a constant ).
Under F.1, if for all and ; or under F.2, if for all and :
and under F.2, for every there is with .
The identity says that an infimum over an infinite-dimensional policy space equals nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in . Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.
These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.
The obvious argument interchanges the infimum over policies with the composition of operators: . The inequality follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside (F.1) or bounding how errors at later stages propagate through (F.2, F.3). Both steps break at infinite values. With there may be no -optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is , which is why F.3 and the definition of -optimality have two cases.
The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. is m.T^[N], and is a recursion that applies first. All values lie in EReal. The book's convention never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns when the positive part diverges). Every theorem assumes and . Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants and .
is defined as an infimum over policies of the composed operators, never through , so the goal is not true by definition. A formalization in which already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.
Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.
Iterative methods for optimization and equation solving on a smooth constraint set (orthogonal matrices, fixed-rank matrices, spheres, Stiefel and Grassmann manifolds) compute an update vector in the tangent space at the current iterate and then have to return to . The Riemannian exponential map does this along geodesics, but computing it means solving an ordinary differential equation. The notion of retraction, introduced by Adler, Dedieu, Margulies, Martens and Shub (IMA J. Numer. Anal., 2002) and developed in the book of Absil, Mahony and Sepulchre (Princeton, 2008), captures what such a return map needs for Newton's method to keep its local quadratic convergence and for gradient methods to converge: smoothness, , and first-order agreement with the exponential.
Absil and Malick (SIAM J. Optim., 2012; HAL hal-00651608v2) give a general recipe for building retractions on submanifolds of a Euclidean space: move tangentially from to , then come back to along a prescribed family of admissible directions. This mission formalizes that recipe, Theorem 4.2 of the paper ("retractors give retractions"), together with the two lemmas its proof rests on.
Let be a Euclidean space of dimension (in the paper's examples, with the Frobenius inner product). A set is a submanifold of dimension if around every it is a coordinate slice: there are an open neighbourhood of and a diffeomorphism of onto an open subset of with . Throughout, .
The tangent space is the linear subspace of of tangent directions of at , the normal space is its orthogonal complement, and the tangent bundle is .
A map from to is a retraction around (Definition 2.1) if, on a neighbourhood of in , it is of class , satisfies , and has derivative at . It is a retraction on if this holds around every point.
A retractor (Definition 4.1) is a map , defined on a neighbourhood of the zero section of , with values in the Grassmann manifold of -dimensional linear subspaces, such that for every . Given , set and let
The theorem asserts both that the point-to-set map is single-valued near the zero section and that it is a retraction there.
Near there is one and only one smallest with ; ; and is a retraction around , hence on .
On a neighbourhood of the zero section, for a unique linear depending on .
If and for all , then for all .
Theorem 4.2 reduces the construction of a retraction to the choice of a smooth field of subspaces transverse to the tangent space at . The orthographic retraction () and the projective retraction () are both instances, as are the gnomonic, orthographic and stereographic projections on the sphere. Theorem 4.9 then certifies, by a check at only, that a retraction agrees with the exponential to second order, which matters for the superlinear convergence of Riemannian trust-region and Newton methods. Lemma 4.7 goes beyond an earlier result on tangential parameterizations (reference [28, Th. 3.4] of the paper) by giving regularity jointly in , not only in (Remark 4.4 of the paper).
The results are proved in the paper. None of them is machine-checked: Mathlib has the implicit function theorem and smooth manifolds, but no embedded submanifolds of a Euclidean space with their tangent and normal bundles, no retractions, and no smooth Grassmannian-valued maps. The work here is to formalize the known proof and to build this layer, which every later mission of this series (projective, spectral, fixed-rank and Stiefel retractions) also needs.
The statement is an implicit-function argument, but the obvious one does not apply directly. The unknown lives in the normal space , which moves with , and ranges over the tangent bundle, a submanifold of rather than an open set of a vector space. The equation has to be read in charts of the bundle, which costs one derivative; the uniqueness given by the implicit function theorem holds only locally in , and turning it into "the smallest ", or "the nearest point of ", requires excluding far-away intersection points. For a general retractor, the subspace also moves, and has to be written as a graph over the normal space with a dependence before a second implicit-function argument applies.
is a finite-dimensional real inner product space E, is Module.finrank ℝ E, and are natural numbers with and (the latter inside the submanifold definition). The coordinate slice uses an open partial homeomorphism E → EuclideanSpace ℝ (Fin n), in both directions, with 0-based coordinates. is the span of Mathlib's tangent cone (chart-free), its orthogonal complement. Retractions and retractors are total maps on constrained only on with open; "of class on a subset of " is ContDiffOn on that set. A Grassmannian-valued map is when its orthogonal projector is, and the dimension of is part of the definition. The set-valued uses the published nearest-point predicate RandomGradFree.Nonsmooth.IsMetricProjection. In Lemma 4.8, is extended by on so that it is an operator on . Theorem 4.9 assumes , the standing assumption of the definition of second-order retractions (display (2.3)), and reads the page's "" as for all .
The goal is not satisfied by exhibiting some retraction: it requires the nearest-point set to equal a singleton (so it is nonempty) and that very to be a retraction. Theorem 4.9 requires the curve to be twice differentiable, so a junk second derivative of does not satisfy it.
A complete development needs: finite-rank facts for tangent spaces of slices (), smoothness of , charts of and of the Whitney sum , ContDiffOn on submanifolds, and local orthonormal frames of a smooth field of subspaces. All of these are reusable beyond this mission. Contributions to any of them, and proofs of the two lemmas, are welcome.
Many large convex programs have the form "minimize a strictly convex function subject to linear equations ". Examples are entropy maximization under moment constraints, the estimation of a matrix with prescribed row and column sums (the matrix-scaling or RAS problem of transportation and input–output analysis), and least-norm solutions of linear systems. When is large and sparse, methods that touch one equation at a time are attractive: each step needs only one row of .
L. M. Bregman's 1967 paper (doi:10.1016/0041-5553(67)90040-7) introduced such a method. §1 defines a "relaxation" for finding a common point of closed convex sets , in which each step replaces the current point by its -projection onto one set: the minimizer of a distance-like function over that set. §2 chooses from the objective itself, with the gradient of ; this function is now called the Bregman divergence. Theorem 3 of the paper, the target of this mission, shows that with this choice the relaxation does more than find a feasible point: started at a suitable point, its limit minimizes over the feasible set. The resulting row-action methods underlie later work on entropy optimization and matrix balancing (Censor and Zenios, Parallel Optimization, 1997) and the Bregman-projection techniques of modern optimization.
Work in the Euclidean space with inner product . Let be a convex set with closure and interior . Let be strictly convex and continuously differentiable over , with gradient at , and continuous over . Let be an matrix with nonzero rows and . The problem (2.1)–(2.3) is
with feasible set , assumed nonempty. A point of minimizing over is a solution.
The function (1.4) is
and also denotes the hyperplane . The paper assumes that satisfies its conditions I–VI of §1 with respect to these hyperplanes; among them, condition II provides, for every , a -projection minimizing over . It also assumes condition (2): if and , then .
A relaxation sequence with control starts at and sets . The control is any sequence of row indices. Finally,
is the set of points of at which the gradient lies in the row space of .
Assume that the -projection of every point of onto every lies in . For every control and every relaxation sequence with that converges to a point ,
Convergence of the sequence is a hypothesis; the theorem says what the limit is, whichever control produced it.
An additional item states Note 2: the point and the multiplier in (2.7)–(2.8) are unique.
Theorem 3 converts a feasibility algorithm into an optimization algorithm for equality-constrained convex programs. Each step solves a one-dimensional problem (the multiplier of a single equation), so the method scales to systems with very many equations, and with the controls of Theorems 1–2 of the same paper it gives a complete algorithm. Specializations include iterative proportional fitting for entropy objectives and Kaczmarz-type projections for .
The theorem and its proof are classical and have been reproved many times, but no machine-checked proof is known to exist. A formalization produces a verified bridge between three standard pieces of convex analysis: first-order optimality on an affine set, the supporting-hyperplane inequality for a differentiable convex function extended to the closure of its domain, and the passage of a Lagrange condition to a limit. Each is reusable in other row-action and mirror-descent developments.
The obvious argument says: the limit is feasible, and the gradient at every iterate lies in the row space of , so the limit satisfies the Karush–Kuhn–Tucker conditions. Two steps of this argument fail as stated. First, the gradient is only known on , the limit may lie on the boundary of (or outside , in ), and need not extend continuously there, so the multipliers need not converge and no Lagrange condition holds at the limit. Lemma 3 must therefore reach optimality without a gradient at . Second, the Lagrange condition (2.7) at an iterate requires the projection to be an interior minimizer, which is why the theorem carries the hypothesis that preserves ; on the boundary of a minimizer over need not satisfy (2.7).
The space is EuclideanSpace ℝ (Fin p), rows are vectors a i, and is the real inner product. The gradient is explicit data tied to by HasGradientWithinAt f (g x) S x for and continuous on ; is not assumed open, and Mathlib's gradient is not used. The relevant explicit choices are:
lam.The goal does not conclude that the relaxation converges; a statement asserting convergence is a different, unproved theorem. Equally, it must not be weakened to a fixed control, to an open , or to a limit assumed to lie in : any of these would trivialize the passage to the limit that the theorem is about.
A complete development needs the first-order condition for a local minimum on an affine hyperplane, the gradient inequality for , , and an induction along the relaxation sequence. Proofs of the milestones and of Note 2 are welcome independently.
A reproducing kernel Hilbert space is a Hilbert space of functions on a set in which every point evaluation is continuous; the function that represents evaluation at is its reproducing kernel. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404, DOI 10.1090/S0002-9947-1950-0051437-7) gave the general theory of these spaces, which today underlies kernel methods in statistics and machine learning, Gaussian-process regression, and the Bergman and Szegő kernels of complex analysis.
Part I of the paper studies how kernels behave under the basic operations on classes of functions: sums, inclusions, products, restrictions, and limits. §9 treats limits. Its case A concerns a decreasing sequence of classes with increasing norms, defined on an increasing sequence of sets. The application in the paper's Part II is the computation of kernels of a domain by approximation from simpler domains: when a domain is exhausted by an increasing sequence of subdomains, the kernels of the subdomains converge to the kernel of the whole domain. This mission formalizes §9, Theorem I and the steps of its proof.
Let be an arbitrary set and subsets with union . For each let be a complex Hilbert space of functions on , with norm , in which point evaluations are continuous; , for , is its reproducing kernel, characterized by and
with the scalar product linear in . For and , denotes the restriction of to . The standing assumptions of §9 A (p. 362) are:
together with the existence of every kernel . For two kernels on a set , means that is a positive matrix: for all finite families , . is the restriction of to .
The limit class is the set of functions on such that (1°) every restriction belongs to and (2°) .
Under the standing assumptions there is such that, whenever ,
and is the reproducing kernel of with the norm
The result. Theorem I turns a monotone family of function spaces into a single space and identifies its kernel as the pointwise limit of the kernels. It reduces the computation of a kernel on a large set to kernels on an exhausting sequence of subsets, the method Aronszajn uses in Part II for Bergman-type kernels of plane domains. With for all (explicitly allowed on p. 362) it gives the limit of a decreasing sequence of kernels on one set as the kernel of the intersection class with the limit norm. The milestones (4)–(6) are quantitative: (5) bounds the distance between restricted kernel sections by the decrease of the diagonal values, which yields strong convergence of in every .
Formalizing it. The theorem is classical and proved in the paper; to our knowledge no machine-checked proof exists. Mathlib has the RKHS class, the operator-valued kernel, the positive semidefiniteness of kernels and the Moore–Aronszajn construction RKHS.OfKernel, but nothing about restrictions of an RKHS to a subset, the order between kernels, or limits of sequences of reproducing kernel spaces. This mission produces those statements on Mathlib's RKHS vocabulary over , with kernels on varying domains.
The kernels live on different sets , so convergence is not convergence of a sequence of functions on one set: a pair enters the sequence only from the first containing both. The identification of the limit class needs three separate facts: that with the limit norm is a Hilbert space (the limit of norms must be shown to come from a scalar product, and completeness requires passing to the limit in two indices), that , and that reproduces. The natural first idea, to embed all in one space and take an intersection, fails: the are spaces of functions on different sets, and their norms differ, so there is no common ambient Hilbert space; the comparison goes only through restriction and the inequalities (3). Eq. (4) itself uses §7, Theorem II (a contractively included Hilbert subclass has a dominated kernel) and the restriction theorem of §5, neither of which is in Mathlib.
H n with [InnerProductSpace ℂ (H n)] [CompleteSpace (H n)] [RKHS ℂ (H n) (E n) ℂ], a space of functions on the subtype E n; the set is a type X with no topology, measure or nonemptiness assumption.kernelFn H x y is Mathlib's RKHS.kernel H x y 1. Mathlib's inner product is conjugate-linear in the first slot, so Aronszajn's is ⟪g, f⟫_ℂ.IsDecreasingRKSequence; every statement takes it as a hypothesis. Restriction is pointwise agreement on . Indexing starts at .KernelLE K₁ K := (Matrix.of K - Matrix.of K₁).PosSemidef, with Mathlib's positive semidefiniteness over an arbitrary index type (finitely supported vectors).ComplexOrder, which also asserts that these values are real.Tendsto).RKHS.OfKernel K₀ and then asserts that its kernel is would be a tautology (RKHS.kernel_ofKernel); the goal instead characterizes the space by its functions and norm, as the paper does.Needed infrastructure, reusable beyond this mission: restriction of an RKHS to a subset (§5), the dominated-kernel theorem for contractive inclusions (§7, Theorem II), and the passage from a convergent sequence of norms to a convergent sequence of scalar products. Proofs of any milestone, and of these general facts as separate lemmas, are welcome.
Mathlib/Analysis/InnerProductSpace/Reproducing.lean (the RKHS class, RKHS.kernel, RKHS.OfKernel). https://github.com/leanprover-community/mathlib4Reproducing kernel Hilbert spaces are the function spaces of kernel methods in statistics and machine learning (Gaussian-process regression, support vector machines, kernel mean embeddings), of the Bergman and Szegő spaces of complex analysis, and of the theory of positive-definite functions. In all of these, bounded operators on the space (covariance operators, integral operators, projections onto subspaces, multiplication operators) are handled through functions of two points rather than through abstract operators. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) gives, in its §11, the dictionary between bounded operators on a space with a reproducing kernel and their kernels, and characterizes the kernels of bounded symmetric operators with prescribed bounds. Aronszajn credits the ideas of the section to E. H. Moore.
Let be an arbitrary set and let be a class of complex-valued functions on that forms a complex Hilbert space with scalar product , linear in and conjugate-linear in . A reproducing kernel of is a function such that, for every , the function belongs to and
Such a kernel exists exactly when every point evaluation is continuous.
For a bounded linear operator on , with adjoint defined by , the kernel of is
the value at of the element of . By the reproducing property, for every and , so is determined by .
A function is a positive matrix if for every finite family of points and complex numbers . For two arbitrary functions on , one writes if is a positive matrix. A bounded operator is symmetric if , and positive if for every . A symmetric has lower bound and upper bound if
A kernel is hermitian symmetric if .
For an arbitrary hermitian symmetric function and real numbers :
The function is not assumed to have ; that membership is part of what the condition yields.
Theorem I identifies, by finite quadratic-form inequalities alone, which functions of two points are kernels of bounded symmetric operators and with which spectral bounds. It reduces statements about operators (boundedness, positivity, operator inequalities ) to statements about finitely many evaluations of kernels, the form in which they are checked in practice, for instance when a covariance or integral operator is shown to be bounded and positive from its kernel. The milestones make the correspondence a usable calculus: adjoints become conjugate transposes, composition becomes a scalar product in the middle variable, and limits of operators become limits of kernels.
All of these results are proved in the paper. None is formalized: Mathlib has reproducing kernel Hilbert spaces (RKHS), adjoints, positive operators and positive semidefinite matrices over arbitrary index types, but no kernel of an operator and none of the statements above. The mission produces machine-checked proofs of the §11 dictionary and of Theorem I.
The necessity half of Theorem I and milestones (3), (6), (4) follow from the reproducing property. The sufficiency half is where the work is: is an arbitrary function, and the hypothesis is only about finite families of points. One has to produce an operator on all of . The obvious attempt, defining on the dense span of the functions by the kernel and extending by continuity, needs the bound on that span, which does not follow directly from the two one-sided inequalities on the diagonal forms. The positivity of and does not by itself give the membership , which the definition of the kernel of an operator requires. In milestone (7), positivity of an operator is a statement about all of , while positivity of the kernel only sees finite combinations of kernel functions; the passage between them uses density of these combinations.
RKHS ℂ H X ℂ: a complex Hilbert space H whose elements are functions X → ℂ on an arbitrary type X (no topology, no measure, not assumed nonempty), with continuous evaluations. The scalar kernel is the series' shared definition AronszajnRK.Sum.kernelFn H x y := RKHS.kernel H x y 1; the function is the element RKHS.kerFun H y 1.L : H →L[ℂ] H is opKernel L x y := (adjoint L) (kerFun H y 1) x. Mathlib's ⟪u, v⟫_ℂ is conjugate-linear in u, so the paper's is ⟪g, f⟫_ℂ, and every formula with a scalar product or a bar has been rewritten in that order. On a one-point with , and , the kernel is .Matrix.PosSemidef of Matrix.of Λ over the index type X (finitely supported test vectors, ComplexOrder on ℂ); no finiteness of X is assumed.IsSelfAdjoint L. "Positive" in (7) is ∀ f, 0 ≤ ⟪f, L f⟫_ℂ in ComplexOrder (real and nonnegative), without assuming self-adjointness, as in the paper. The bounds in Theorem I are bounds of the quadratic form, m‖f‖² ≤ Re⟪f, L f⟫ ≤ M‖f‖², not of the operator norm. The paper does not assume and neither does the statement: for both sides hold exactly when and .H, and that the kernel of L₁ ∘L L₂ is their scalar product.⟪v, Lₙ u⟫ → ⟪v, L u⟫ for all u, v; uniform convergence is ‖Lₙ − L‖ → 0 in operator norm.HilbertBasis with arbitrary index types, and the double limit is taken along growing finite sets of indices in both variables. For systems indexed by this contains the paper's over ; the general form also covers finite-dimensional spaces. The second sentence of Theorem III (kernels in correspond to operators of finite norm) needs the direct product and is not stated.RKHS, RKHS.kerFun_inner, RKHS.kerFun_dense, RKHS.posSemidef_kernel, ContinuousLinearMap.adjoint, ContinuousLinearMap.IsPositive and isPositive_iff_complex, HilbertBasis, Matrix.PosSemidef. Contributions welcome: a general lemma that a function with is the kernel of an operator , and the inclusion theorem , both reusable beyond this mission.In a network design game each player must connect its terminals in a graph whose edges carry fixed costs, and the cost of an edge is split among the players that use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008)) studied the fair (Shapley) split, in which the users of an edge pay equal shares. That game is a congestion game in the sense of Rosenthal (Int. J. Game Theory 2 (1973)), so it has an exact potential and pure Nash equilibria always exist.
Section 6 of the same paper turns to weighted players: player has a weight (a traffic volume, a bandwidth demand, a share of ownership) and pays for each edge it uses a share proportional to its weight. The equal-split potential is then lost, and the paper notes that weighted games with three or more players need not have a pure Nash equilibrium at all (Chen and Roughgarden, Network design with weighted players, SPAA 2006). Theorem 6.3 identifies a natural class in which equilibria survive: all players share one source and one sink. For that class it shows more than existence. The simplest decentralized procedure, letting players in turn switch to a cheapest route, always stops, and where it stops is an equilibrium.
A finite directed multigraph has a finite set of arcs; each arc has a tail and a head vertex, and parallel arcs between the same two vertices are allowed. Fix a source and a sink . A simple – path is a sequence of arcs (), each starting where the previous one ends, beginning at , ending at , and visiting no vertex twice; it is identified with its arc set . Write for the finite set of these paths.
The weighted single-commodity game has a finite set of players; player has a weight , arc has a fixed cost , and every player's strategy set is . In a profile let
be the total weight on arc . Player pays
A profile is a (pure) Nash equilibrium if no player can lower its payment by switching alone to another path.
A best-response move of player replaces by a path that minimises 's payment given the other players' paths, provided this strictly lowers 's payment. Best-response dynamics is any sequence of profiles in which each profile arises from the previous one by a best-response move of some player.
For every such game with and :
The goal asserts only termination and existence; it fixes no bound on the length of a run.
For a profile define the marginal cost of a path, , and the tuple of all values , , sorted increasingly. With strictly positive arc costs:
The theorem gives a guarantee about dynamics, not only about existence: in single-commodity weighted network design, any order in which players take turns playing best responses reaches a stable outcome in finitely many steps. This places the single-commodity case on the positive side of the boundary drawn by the nonexistence examples for general weighted games. The tuple of sorted path costs is a potential that is not a single number, a device that applies to other games without an exact potential.
The result is proved in the paper; it has no machine-checked proof that this mission is aware of. A formal development contributes a reusable layer for weighted cost-sharing games (payments, best responses, Nash equilibria on arbitrary strategy families), a treatment of simple directed paths in multigraphs as strategy sets, and a lexicographic termination argument over sorted lists of extended reals. The goal is stated for nonnegative costs, as in the paper's model, while the printed proof uses positive costs; closing that gap is part of the work.
The obvious route, finding a real-valued function that every improving move decreases, is unavailable: the paper notes that Rosenthal's potential is not a potential once weights are added, and that improving moves can increase it. Termination must instead come from an ordinal quantity, a whole sorted list compared lexicographically, and the move of one player changes the marginal costs of every path that shares an arc with the old or the new route, in both directions.
The argument also depends on the shape of the strategy sets. Two distinct simple – paths are never nested as arc sets; with walks that repeat vertices, or with arbitrary strategy families, the comparison between a path's marginal cost before and after a deviation can fail. Arcs of cost zero create a further gap: is on an unused free arc, and the strict inequalities of the proof degenerate, so the nonnegative-cost goal needs more than the printed argument.
Finset of arcs; the strategy family of every player is the finite set of arc sets of simple – paths (a list of consecutive arcs with distinct visited vertices). There are no paths when .IsStandard); the milestones (6.1) and the lexicographic decrease assume .ℝ≥0∞): an unused arc of positive cost contributes . Computing it in the reals, where , would make unused paths free and the milestones false.Contributions welcome: lemmas on simple paths in multigraphs (non-nestedness), the multiset-to-sorted-list lexicographic comparison, and the treatment of zero-cost arcs.
We establish the polynomial simulation needed for WordRAM-based NP proofs. It reuses the same machines and Cook–Levin definitions, with uniform programs, logarithmic word widths, and standard bit input/output.
The targets cover function outputs and verifier verdicts, including loading and serialization costs.
This adapts Cook–Reckhow’s Theorem 2(a), pp. 361–363, to Hagerup’s bounded-word operations, including multiplication; no particular simulation exponent is prescribed.
Mean field games (MFG), introduced by Lasry and Lions and by Huang, Caines and Malhamé, describe Nash equilibria of very large populations of identical rational agents. The equilibrium is a coupled system: a backward Hamilton–Jacobi–Bellman equation for the value function of a representative agent and a forward Fokker–Planck equation for the density of the population. In the planning problem, proposed by P.-L. Lions, both the initial density and the final density are prescribed, and one asks for a cost structure under which the population moves from one to the other. This is a mean field analogue of optimal transport.
Achdou, Camilli and Capuzzo-Dolcetta (hal-00465404, SIAM J. Control Optim. 2012) propose finite-difference schemes for the planning problem. Mission I of this series treats the existence of a solution of the discrete planning scheme. Since the two boundary conditions on make the discrete system hard to solve directly, the paper also introduces a penalized scheme, in which the initial condition is replaced by a penalty ; for each this is a standard discrete MFG system with a unique solution. This mission formalizes the paper's §3.2: the penalized solutions converge, as , to a solution of the planning scheme.
Fix integers , , a horizon and a viscosity ; put and . The grid consists of the points , (periodic indices). A grid function is a real function on ; time levels are .
The planning scheme (18) asks for families with, for ,
, and . The penalized scheme (20)–(23) has the same two equations, for , , and in place of .
Under the hypotheses of Theorem 1, for every sequence , every choice of penalized solutions , and every limit in ,
If is strictly convex, the whole sequence converges to the unique solution of (43)–(46) with .
In 3–5 the constant depends on , and the data, never on .
Proposition 4 justifies the penalized scheme as a way to compute solutions of the discrete planning problem. The penalized system has a standard initial–terminal structure that Newton's method (the paper's §4) handles well. The planning system does not, because it prescribes two conditions on and none on . The estimates of Propositions 2–3 and Corollary 1 also give a rate: the initial mismatch of the penalized density is .
The results are proved in the paper. None of them has been machine-checked: the platform holds no formalization of mean field games, of their finite-difference schemes, or of the Lasry–Lions monotonicity argument. A complete development would yield a reusable library of the monotone finite-difference operators on the discrete torus, a formal Lasry–Lions uniqueness argument for discrete MFG systems, and a template for compactness-plus-uniqueness convergence proofs in finite dimension.
Compactness of the densities is free, since is compact. Passing to the limit in the scheme needs only continuity of , and . The substance lies in the two uniform estimates.
All objects live in the namespace MFGPlanning.Penalized.
ZMod Nh × ZMod Nh (periodicity is built in), time levels are Fin (NT + 1), and the four momentum components are Fin 4 indices 0, …, 3.EReal, so unbounded suprema are .Three trivializing formalizations are ruled out. The constants in Propositions 2–3 and Corollary 1 are quantified before and before the solution. The goal quantifies over every sequence and assumes no convergence of and no limit solution. Its part 2 does not assume convergence of .
The existence of a solution of the planning scheme (Theorem 1) is posed in mission I and not restated here. A solver of Proposition 2 will need it once mission I's goal is proved. The existence and uniqueness of solutions of (20)–(23) are quoted by the paper from Achdou–Capuzzo-Dolcetta (2010) and are not items. Welcome contributions include discrete summation-by-parts lemmas on the torus, the discrete comparison principle for monotone schemes, and the Poincaré-type inequality on zero-mean grid functions.
Single-machine sequencing is the base case of deterministic scheduling theory. Many multi-machine and shop problems are analysed by reduction to it, and many bounds and approximation algorithms for harder models use it as a subroutine. A central objective class is the bottleneck or minmax objective. Each job carries a nondecreasing cost of its completion time, and the schedule is judged by its worst job. Maximum lateness, maximum tardiness and maximum weighted tardiness are all special cases.
Before 1973 the minmax problem was solved without precedence constraints. Jackson (1955) showed that ordering by due date minimizes maximum lateness. Moore (1968, Management Science 15(1)) gave a procedure for general nondecreasing deferral costs, and Lawler and Moore (1969) gave a related method. In Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5), 1973, Lawler showed that arbitrary precedence constraints can be added at no loss of efficiency. Jobs are chosen from last to first, by a single comparison of costs at a known time. The resulting procedure is the standard algorithm for the problem written in the classification of Graham, Lawler, Lenstra and Rinnooy Kan (1979). It is one of the first polynomial-time results for precedence-constrained scheduling that every survey of the field cites.
A finite, nonempty set of jobs is processed on a single machine, one job at a time and without interruption. Each job has a processing time and a cost function that is monotone nondecreasing. The value is the cost incurred when is completed at time .
The precedence constraints are an arbitrary relation on jobs: means that job is required to precede job . A sequence lists every job of once. It observes the precedence constraints if never holds for positions . The machine starts at time with no idle time, so the completion time of is . The maximum incurred cost of is
and a feasible is minmax optimal if for every feasible .
For a set of jobs, is the set of jobs of that are not required to precede any other job of , and . Lawler's rule builds a sequence from the last position to the first. With the jobs not yet placed, it chooses with , places in the latest open position and removes it from . Ties are broken arbitrarily. In Lean the objects are IsFeasible, lastEligible (), IsMinmaxOptimal and IsLawlerSequence, in namespace LawlerPrec.MinMax. They are built on the published MooreLateJobs.Shared.completionTime and MooreLateJobs.MaxDeferral.maxCost.
Every sequence that Lawler's rule can produce, under any tie-breaking, observes the precedence constraints and satisfies
This is the statement of §3 (p. 545), "An efficient algorithm for finding a minmax optimal sequence follows immediately from the theorem above". It contains no constants.
The result shows that is solvable in polynomial time for every family of nondecreasing costs. The ordering of an optimal sequence depends on the costs only through their values at the partial sums along the way. The deadline problem is a corollary (§5): sequencing from last to first by latest deadline among the currently available jobs avoids tardiness whenever any sequence does. The last-to-first scheme is reused in later backward rules for objectives. A formal statement of the rule, its feasibility and its optimality makes these extensions available for formal reuse.
The result is classical and its proof is short. No machine-checked proof of it is known to be in Mathlib. The work this mission asks for is a formal proof of the known exchange argument and of the induction that turns the Theorem into the algorithm's correctness. The induction needs the reduced problem's sets and times to be the correct ones at each stage, which the definitions fix.
The exchange argument of §2 is elementary. The difficulty lies in stating the algorithm faithfully and carrying the induction. At each stage the eligible set and the time must be recomputed on the remaining jobs, with constraints into already placed jobs ignored. The induction must also show that the rule's sequence is feasible, which is a conclusion and not an assumption.
A first attempt often proves only the Theorem, that some optimal sequence has last. That statement says nothing about a sequence built entirely by the rule, because an optimal sequence of with last need not restrict to an optimal sequence of . Optimality of the rule's whole sequence is the target, and milestone 5 isolates the corresponding step of the page.
ι with decidable equality, and the job set is J : Finset ι.a : ι → ℝ, costs are c : ι → ℝ → ℝ, and the precedence constraints are prec : ι → ι → Prop.J. Positions are 0-based, and completion times are prefix sums (MooreLateJobs.Shared.completionAt).prec is arbitrary: it is not assumed transitive, irreflexive or acyclic. A cycle among distinct jobs leaves no feasible sequence. A self-loop constrains nothing, both in feasibility and in (the "others" of the page exclude the job itself).The standing assumptions of §1 appear as hypotheses wherever they are used: monotone nondecreasing for , and nonempty where the maximum is taken. Two hypotheses are added relative to the page and disclosed in each statement. Processing times are non-negative (), since they are durations and the exchange argument fails without them. The Theorem also assumes the existence of a feasible sequence, which its conclusion presupposes.
The rule is the property IsLawlerSequence of a finished sequence. At each position , the job there lies in of the jobs in positions and minimizes the cost at their total processing time. Every tie-break is covered. The rule is not a deterministic function, and it is not an arbitrary choice function. Feasibility of the rule's output is part of the goal's conclusion, so the goal cannot be obtained by assuming it. A statement that compares the rule only with some sequence, or that asserts only that an optimal sequence exists, is weaker and is ruled out by the goal's form. Milestone 6 shows the goal's hypotheses are satisfiable whenever a feasible sequence exists.
The operation count of §4, the first-to-last rule of §5 and the deadline corollaries of §5 are not part of this mission. A development needs only finite lists and finsets from Mathlib. Lemmas about moving an element to the end of a duplicate-free list, and about prefix sums under that move, are reusable for other exchange arguments in single-machine scheduling.
Empirical risk minimization (ERM) chooses, from a class of loss functions, the one with the smallest average loss on a sample . Its standard guarantees bound the excess population risk by a term of order , whatever the variance of the losses. When good functions in have small variance, a better trade-off is available in principle: minimize the empirical risk plus a standard-deviation penalty . Maurer and Pontil (COLT 2009) showed that this sample variance penalization enjoys faster rates, but the penalized objective is non-convex even for convex losses, so it cannot be minimized efficiently in general.
Duchi and Namkoong (arXiv:1610.02581v3, 2017; NIPS 2017) replace the variance penalty by a distributionally robust objective: the worst-case average loss over all reweightings of the sample within a -divergence ball of radius . This objective is convex whenever the loss is convex, and it equals the empirical risk plus the standard-deviation penalty up to an error of order . Theorem 3 of the paper turns this into a guarantee for the minimizer of the robust objective, using covering numbers of the class. This mission formalizes Theorem 3 and the lemmas its proof rests on.
Let be a measurable space, a probability measure on it, and () an i.i.d. sample from with empirical distribution . Let be a nonempty class of measurable functions , and set . Write , for the variance of , and
For , the ball is the set of weight vectors with , and : the distributions on the sample with for . The robust risk of is
and a robust minimizer is any .
Complexity is measured by empirical covering numbers. For , is the least number of points such that every lies within sup-distance of some . For let , and
Let , , and . With probability at least , every robust minimizer satisfies
Under the same hypotheses and with the same probability, simultaneously for all ,
Inequality (15) says the robust risk is a uniform upper confidence bound on the population risk, with an slack instead of the slack of the empirical risk. Inequality (16) says the robust minimizer competes with the best variance-penalized population risk in the class. When some has small risk and small variance, the excess risk of is of order up to the covering term, a rate ERM does not achieve in general (§3.3 of the paper gives an example). For a parametric class with polynomial in , choosing gives Corollaries 3.1 and 3.2 of the paper.
The results are proved in the paper; none of them has a machine-checked proof that we know of. The mission's output is a formal proof of Theorem 3 and its ingredients: a deterministic analysis of the -constrained linear program (Theorem 1 (10)), a covering-number empirical Bernstein inequality (Lemma C.1, from Maurer and Pontil), concentration of the sample standard deviation (Lemma A.1), and the scalar Bernstein inequality in the form used. Each of these is reusable outside distributionally robust optimization.
The deterministic part, (10), is a short analysis of a quadratically constrained linear program. The main obstacle is Lemma C.1. A union bound over a cover of fails directly: the cover depends on the sample, and a population-level cover of need not be finite. The standard route goes through a ghost sample of size (hence covering at points), a symmetrization that must preserve the sample variance rather than only the mean, and a concentration bound for the sample variance itself. Lemma A.1 needs concentration of , a non-linear and non-smooth function of the sample, at the sub-Gaussian rate . Finally, the oracle inequality (16) holds for an infimum over the whole class, while the concentration step for the comparison function is only proved for one fixed at a time.
The sample is the coordinate process of the product measure on (Measure.pi). Each probability statement bounds the probability of the bad event, the set of samples where the inequality fails for some (or some minimizer). This set need not be measurable, and its measure is then the outer measure, as is standard in empirical-process theory. Probability bounds are computed in , and the covering number is valued in , so an infinite covering number makes the bound trivial rather than collapsing to zero. Covering numbers are internal (centres in ) and use closed sup-norm balls, as on p. 9; this is Mathlib's Metric.coveringNumber. The empirical variance is normalized by . The ball is encoded as weight vectors on the sample points; with tied sample values this gives the same supremum as the paper's distributions on the sample. Statement (16) is formalized for every minimizer of the robust risk, and the event is empty if no minimizer exists. The infimum ranges over the nonempty class , on which every term is at least . Population moments are those of bounded measurable functions, hence finite.
Deviations from the printed text:
A trivializing formalization is ruled out: the bound is not taken over all functions, a probability bound is not formed from the real part of an infinite covering number, and the minimizer is not a hypothesis that can fail to exist for the given sample.
Needed infrastructure: product-measure concentration (Bernstein, and a bounded-difference or convex-Lipschitz inequality for ), symmetrization with a ghost sample, and finite union bounds over a cover. Contributions are welcome on any milestone, in particular a general covering-number empirical Bernstein inequality, which is reusable on its own.
In a network design game each of players must connect its own terminals in a shared graph, and the cost of every edge that is bought is split among the players who use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 2008) studied the fair (Shapley) split, in which the users of an edge each pay . That game is a congestion game in the sense of Rosenthal (Networks 1973), so it has an exact potential function and pure Nash equilibria always exist.
When players carry different amounts of traffic, the natural rule is to split an edge's cost in proportion to weight: a player of weight on an edge whose users have total weight pays . The paper notes that this rule is analogous to weighted generalizations of the Shapley value (Monderer and Samet, Variations of the Shapley Value, Handbook of Game Theory III, 2002). The weighted model leaves Rosenthal's framework: the share depends on which players use an edge, not only on how many, and Chen and Roughgarden (SPAA 2006) showed that weighted games with three or more players need not have a pure Nash equilibrium at all. Section 6 of the paper identifies structural conditions under which equilibria do exist. This mission covers the first of them.
Timeline. Rosenthal (1973): every congestion game has a pure Nash equilibrium, via an exact potential. Monderer and Shapley (GEB 1996): potential and weighted potential games, and the equivalence of exact potential games with congestion games. Anshelevich et al. (FOCS 2004, journal 2008): Theorem 6.1, existence when every resource is shared by at most two players, and Theorem 6.3, existence when all players share a source and a sink. Chen and Roughgarden (2006): weighted network design games with three or more players may have no pure equilibrium.
A weighted cost-sharing game consists of a finite set of players, a finite ground set of edges (resources), and for each player :
together with a fixed edge cost for every . A profile picks for every player. For an edge , is the total weight of the players with , and player 's payment is
A profile is a pure Nash equilibrium when no player has a with , where is the profile in which plays and everyone else keeps their strategy.
The strategy space of player is the set of edges that occur in at least one strategy of . The hypothesis of Theorem 6.1 is that every edge lies in the strategy spaces of at most two players: no edge can ever be shared by three players, whatever they choose.
The network design game is the instance in which is the edge set of a graph and is the set of edge sets of paths connecting player 's source to its sink .
The paper's proof uses an explicit function with when is unused, when alone uses , and when and both use it, where . It is part of the definitions of this mission.
If every edge lies in the strategy spaces of at most two players, there is a weighted potential: a real function on profiles with
and, if every is nonempty, a pure Nash equilibrium exists. The goal asserts the existence of such a rather than fixing the paper's formula, so it remains valid for any other weighted potential.
An extra item states Corollary 6.2: every two-player weighted game with nonempty strategy sets has a pure Nash equilibrium.
The result. Theorem 6.1 is one of the two existence results the paper proves for weighted cost sharing, a game that in general has no pure equilibrium. It shows that the obstruction found by Chen and Roughgarden needs resources shared by three or more players: whenever sharing is limited to pairs, the game is a weighted potential game, so improving moves cannot cycle and equilibria exist. Corollary 6.2 makes the two-player case unconditional, and the paper notes that the same potential gives a (weak) bound on the price of stability.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. The mission produces a reusable Lean model of weight-proportional cost sharing (shared in form with the companion mission on single-source single-sink weighted games), an explicit weighted potential, and the general step from a weighted potential to a pure equilibrium, which applies to any finite game with positive weights.
The obvious approach, reusing Rosenthal's potential from the unweighted game, fails: the paper observes that in a weighted game improving moves can increase it. A player's share of an edge depends on the weights of the specific co-users, so no function of the edge loads alone can track all players' costs. The identity must therefore hold for every unilateral move, including moves that leave some edges and join others at the same time, and for every pair of possible co-users of an edge. The statement fails without the at-most-two hypothesis, so any argument has to use it in an essential way. The existence step needs the identity on all profiles reachable by feasible deviations, not only along a single path of moves.
Lean namespace PriceOfStability.WeightedPotential. Players form a Fintype ι and edges a Fintype E; a game is a structure with strategies : ι → Finset (Finset E), weight : ι → ℝ and edgeCost : E → ℝ. Standing assumptions wᵢ ≥ 1 and c_e ≥ 0 are the predicate IsStandard. Profiles are functions ι → Finset E with the feasibility predicate IsProfile; every deviation is to a feasible strategy, via Function.update. Nash equilibria are pure and in cost form. The strategy-space hypothesis is a bound on the number of players whose strategy space (the union of their strategies) contains each edge — not a bound on the users in one profile, which would be a different statement. Φ_e is computed from the current users of e; its value with three or more users is a placeholder that never arises under the hypothesis. Strategies are arbitrary subsets of the ground set, as the paper's remark after the proof allows, so the network game is a special case.
The goal is not satisfiable trivially: the function Φ must satisfy the weighted identity for every feasible unilateral deviation from every profile, and an exact (unweighted) potential is not what is asserted. Nonempty strategy sets are added explicitly for the existence part, since without a profile there is no equilibrium.
Needed infrastructure: finite sums over filtered Finsets, the improvement-path argument over the finite set of profiles. The improvement-path lemma (milestone 3) is reusable for any weighted potential game. Contributions of proofs for any milestone are welcome.
Many optimization algorithms are discretizations of a continuous-time descent: the gradient flow for smooth objectives, and its nonsmooth analogue, the subgradient dynamical system, for objectives with kinks or constraints. A basic question about such a flow is whether a bounded trajectory actually converges, rather than merely accumulating on a continuum of critical points, and how fast. For real-analytic this was settled by Łojasiewicz through his gradient inequality, which forces bounded gradient trajectories to have finite length. Without some such structure the answer is negative: there are smooth functions whose bounded gradient trajectories spiral forever around a circle of critical points.
Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the Łojasiewicz inequality to nonsmooth subanalytic functions, possibly taking the value , by replacing with the least norm of a limiting subgradient. Section 4 of the paper turns this inequality into convergence results for subgradient trajectories of convex and lower- functions. This mission formalizes that section. The same "Łojasiewicz argument" later became the Kurdyka–Łojasiewicz framework behind convergence proofs for proximal, alternating and splitting algorithms (Attouch–Bolte 2009; Bolte–Sabach–Teboulle 2014).
Timeline. Łojasiewicz (1963, 1984) proved the gradient inequality for real-analytic functions and finite length of bounded analytic gradient trajectories. Kurdyka (Ann. Inst. Fourier 1998) extended it to functions definable in an o-minimal structure. Kurdyka, Mostowski and Parusiński (2000) proved Thom's gradient conjecture for analytic functions. Bolte, Daniilidis and Lewis (2007) gave the nonsmooth subanalytic version and the trajectory results formalized here.
Let with domain . The Fréchet subdifferential is the set of with . The limiting subdifferential is the set of limits of with and . The nonsmooth slope is , equal to when , and is the set of critical points.
The standing assumptions of Section 4 are:
A trajectory of the subgradient system is an absolutely continuous curve , , with for almost every and for every . It is maximal if it admits no extension to a longer interval. The Łojasiewicz inequality holds around with exponent if is bounded near , with and . A Łojasiewicz exponent at is any such .
Under –, every bounded maximal trajectory is defined on and converges to a critical point . For every Łojasiewicz exponent at there are and such that for
and for , for all large . The constants are existential, so the goal survives any later sharpening of them.
Theorem 4.5 says that for convex or lower- subanalytic objectives, including constrained problems through indicator functions of subanalytic sets, the subgradient flow never oscillates indefinitely: bounded trajectories converge to one critical point. Theorem 4.7 adds rates that depend only on the Łojasiewicz exponent at the limit: exponential at , polynomial above it, finite time below it. These are continuous-time templates for the convergence analyses of proximal and splitting methods under the Kurdyka–Łojasiewicz property.
On the formalization side, the results are proved on paper but, to our knowledge, not formalized in any proof assistant. A development would provide reusable infrastructure: a Lean notion of a trajectory of a differential inclusion on , a chain rule for along absolutely continuous curves, and a comparison lemma for the differential inequality . The analysis of Section 4 uses subanalyticity only through inequality (20), so Theorems 4.5 and 4.7 can be attacked with (20) as an imported milestone, independently of the subanalytic geometry.
Compactness gives cluster points of a bounded trajectory, and the decrease of gives convergence of . Neither gives convergence of . The usual first idea, that forces convergence, fails, since square-integrable speed allows infinite length. The difficulty is to control rather than . That needs a lower bound on the slope in terms of the function gap near the cluster point, which is exactly what (20) supplies, plus a trapping argument showing the tail of the trajectory stays in the ball where (20) holds. In the nonsmooth setting the chain rule itself is nontrivial: is differentiable almost everywhere with derivative for every , which relies on for convex and lower- functions. Global existence on (Corollary 4.1(iii)) must also be established before any asymptotic statement makes sense.
Space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "bounded from below" by a real number excludes . The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff, and convexity is the published MoreauProx.Characterization.EConvex (convex epigraph). The slope is valued in . The Łojasiewicz inequality is encoded as for near and every , which is the bounded ratio under the paper's conventions. Times are real numbers and . Curves are functions whose values outside are irrelevant. "Absolutely continuous on " means absolutely continuous on every compact . Velocities appear only "for almost every ". Lengths are lower Lebesgue integrals in , never Bochner integrals (which would vanish for a non-integrable speed).
Two trivializations are ruled out. Maximality is a hypothesis and is a conclusion: assuming would narrow the theorem, and dropping maximality would make it false. Rates are claimed for every Łojasiewicz exponent at the limit, not for one chosen exponent. Corollary 4.1(iii) is stated as "defined on with ", because the printed would fail for any trajectory with nonzero limit.
Needed infrastructure: absolutely continuous curves and their a.e. derivatives (Mathlib's AbsolutelyContinuousOnInterval), chain rules for convex and lower- functions, existence and uniqueness for monotone differential inclusions (Brézis), and an ODE comparison principle. Contributions to any of these are reusable well beyond this mission.
Scheduling in a multiclass queueing network asks which waiting job a server should work on next when jobs of several types share stations and revisit them along fixed routes. Such networks model semiconductor wafer fabs, job shops and communication switches. Optimal policies are rarely computable: the state space is countably infinite, and even deciding properties of optimal policies is hard (Papadimitriou and Tsitsiklis 1999). A practical substitute is the achievable region approach: describe, by constraints that every policy must satisfy, a set containing all performance vectors any policy can achieve, then optimize a linear cost over that set to get a lower bound on the optimal cost.
Bertsimas, Paschalidis and Tsitsiklis (MIT Sloan working paper 1992; Ann. Appl. Probab. 1994) gave a general method for producing such constraints for open networks, by computing the steady-state drift of quadratic potential functions. This mission formalizes their first-order bounds (Section 4).
Timeline:
A network has single-server stations and job classes. Class is served at station , and is the set of classes served at station . Class- jobs arrive from outside as a Poisson stream of rate , service times are exponential with rate , and after service a class- job becomes a class- job with probability or leaves with probability . The traffic equations
have a unique solution (the network is open), and at every station.
The state counts the jobs of each class. A Markovian policy decides from the current state which classes are in service, at most one per station and only classes with jobs present; idling is allowed. Write for the event that station serves class , and for the event that station is idle. Under such a policy is a continuous-time Markov chain. Assumption A requires that it has a unique invariant distribution and that for all . Let , which equals with the mean response time of class (Little's law), and define
For a set of classes, f-parameters are reals for such that is nonnegative and the same for all ; that common value is , and when (restriction (17)). The sums over include the exit .
For every policy satisfying Assumption A, every and every f-parameters satisfying (17),
where
The formal goal is the product form .
Theorem 4.1 gives, for each choice of and , a linear inequality on mean response times valid for all admissible policies. Minimizing a linear holding cost subject to these inequalities is a linear program whose value bounds the optimal scheduling cost from below; the paper reports numerical values of such bounds in its Section 9. Theorems 4.2–4.4 show that a polynomial-size polyhedron in the variables implies all of these inequalities at once, so the parametric search over is unnecessary.
The results are proved in the paper. As far as is known, none of them has a machine-checked proof. Formalizing them requires a Lean treatment of invariant distributions of controlled countable-state Markov chains with unbounded test functions, which is currently absent from Mathlib, and then the algebra of the drift identities. The definitions here (network data, Markovian sequencing policies, the generator, Assumption A) are the substrate that the paper's later results on routing, closed networks and higher-order bounds would reuse.
Every statement except Theorem 4.4 rests on taking expectations of the generator applied to unbounded functions (, ) under the invariant distribution. The invariance condition is stated only for indicators of single states; extending to quadratic needs an interchange of summations justified by the second-moment condition of Assumption A. The utilization identity additionally needs uniqueness of the traffic solution to identify with . Theorem 4.1 then needs the sign bookkeeping that turns an identity into an inequality: the terms dropped are nonnegative only because on , and at most one class per station is in service.
Classes are Fin R, stations Fin N, states Fin R → ℕ, all rates and probabilities real. A policy is a Bool-valued function of the state with the two admissibility constraints; work conservation is not assumed. Invariance is global balance of the generator on the countable state space; expectations are tsums. The uniformized chain and the epochs of the paper are not built: the paper notes that its expectations at are expectations under the invariant distribution of .
Conventions fixed in Lean:
A quotient-form statement of (18) would be trivially true when , and defining as would make the utilization identity hold by definition; both are excluded.
Welcome contributions: a general lemma extending global balance to test functions of polynomial growth under moment conditions; proofs of the drift identities; the deterministic Theorem 4.4.
The Łojasiewicz inequality states that near a critical point of a real-analytic function there are and with . Łojasiewicz used it in the 1960s to prove that every bounded trajectory of the gradient flow has finite length and converges to a single critical point, a conclusion that fails for general functions. The inequality has since become the standard tool for convergence analysis of descent methods on nonconvex problems.
Optimization problems are, however, rarely smooth: constraints enter through indicator functions, and objectives contain norms, maxima and penalties. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the inequality to nonsmooth subanalytic functions, replacing by a slope built from the limiting subdifferential. Their Section 3.1 treats functions continuous on a closed domain; Section 3.2, the subject of this mission, treats lower semicontinuous convex functions, which may jump to and whose domain need not be closed. The Kurdyka–Łojasiewicz framework built on this paper (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014) underlies the convergence theory of proximal and splitting algorithms used throughout operations research.
Work in with the Euclidean norm, and let with domain .
A set is semianalytic if near every point it is a finite union of finite intersections of sets with real-analytic. It is subanalytic if near every point it is the projection of a bounded semianalytic subset of . A function is subanalytic when its graph is. Semialgebraic functions (norms, polynomials, indicators of polyhedra) are subanalytic.
The Fréchet subdifferential is the set of with , for , and is empty otherwise. The limiting subdifferential is the set of limits of with . The nonsmooth slope is , equal to when , and is the set of critical points. For lower semicontinuous convex , is the subdifferential of convex analysis and is the set of minimizers. Write for the minimum value and for the distance from to . The epigraphical sum is the Moreau envelope of .
Ratios follow the paper's conventions and .
Let be lower semicontinuous, convex and subanalytic with . For every bounded set there is such that
The exponent may depend on ; neither nor the bound is fixed.
Theorem 3.3 gives, for convex subanalytic functions, a Łojasiewicz inequality that is uniform on bounded sets rather than local at one critical point, and it needs neither continuity of on its domain nor a closed domain. Remark 3.4 of the paper exhibits a convex function covered by Theorem 3.3 but not by the continuous-case Theorem 3.1. Through inequality (20) of Section 4, it yields finite length and convergence rates for the subgradient flow of such functions. The intermediate inequality (15) is a Hölderian error bound, , of the kind that drives linear and sublinear rate analyses of first-order methods.
The result is proved in the paper; no machine-checked version of it, or of the nonsmooth Łojasiewicz inequality in any form, is known. Formalizing it would add to the library: subanalytic sets and functions, the limiting subdifferential of convex functions and its agreement with the classical one, the Moreau envelope with its critical points and infimum, and the passage from a growth condition to a Łojasiewicz inequality. Remarks 3.5 and 3.6 isolate parts that need no subanalytic geometry at all.
The convex-analysis steps (inequality (16), properties of the Moreau envelope) are classical. The obstacle is subanalytic geometry. The natural first idea, applying the Łojasiewicz factorization lemma directly to and , fails: is neither continuous nor finite, and its domain need not be subanalytic even when is convex and subanalytic (Example 2.5 of the paper). The milestones route through the Moreau envelope, which is continuous and finite, but subanalyticity is not preserved by infima over unbounded sets, so the subanalyticity of the envelope (Proposition 2.9) needs a localization argument. The subanalyticity of and of rests on the stability theory of subanalytic sets (Gabrielov's complement theorem, the projection theorem for globally subanalytic sets), none of which exists in Mathlib.
The space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "lower semicontinuous, convex, somewhere finite and never " is the published definition MoreauProx.Characterization.GammaZero, whose convexity is convexity of the epigraph. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the convex subdifferential subgrad appears only in Eq. (5), which proves the agreement and is never assumed. Semianalytic and subanalytic sets are defined from scratch for any finite-dimensional real normed space, so that one definition serves and its products; global subanalyticity is not defined. is written in EReal and converted to a real number only where it is finite. The bounded ratio (14) is encoded as " for every and every ", with real powers (Real.rpow, ). Inequalities (15) and (17) are imposed only where , since Lean sends to under toReal.
Trivializing encodings are ruled out: the goal is stated with the limiting subdifferential rather than an assumed convex subdifferential, the slope is never computed in ℝ≥0∞ where would make the ratio vacuous, and remains existential in with the quantifier order "for every there is ", so that is excluded at critical points in by .
A complete development needs a working theory of subanalytic sets (stability under finite unions, complements, closure, projections of bounded sets, the factorization lemma), the Moreau envelope of a convex function on and its property, and the convex-analytic description of the limiting subdifferential. The subanalytic-geometry layer and the Moreau-envelope facts are reusable well beyond this mission; contributions to either, or proofs of the convex-only milestones (Eq. (5), (16), Remarks 3.5–3.6), are welcome independently.
In the mid-1990s, neural networks trained by gradient descent were observed to generalize well even when the number of weights far exceeded the number of training examples. The classical theory could not explain this: VC-dimension bounds for networks grow with the number of parameters, so for large networks they are vacuous. Bartlett's paper (IEEE Trans. Inform. Theory 44 (1998)) showed that, for classification with a margin, what controls generalization is the size of the weights, not the size of the network. Its two main technical results are a margin bound in terms of the fat-shattering dimension (Theorem 2, the subject of mission I of this series) and a bound on the fat-shattering dimension of networks with bounded weights (Theorem 17, the subject of this mission). The same idea of weight-norm capacity control underlies much of the later theory of margins, boosting and kernel methods.
Timeline. Kearns and Schapire (1994) introduced the fat-shattering dimension. Alon, Ben-David, Cesa-Bianchi and Haussler (1997) bounded ℓ∞ covering numbers by it. Bartlett, Kulkarni and Posner (1997) gave the matching lower bound on ℓ1 covering numbers used here as Lemma 19. Maurey's approximation lemma (reported by Pisier, 1981) was used by Jones (1992) and Barron (1993) for approximation by networks, and by Lee, Bartlett and Williamson (1996) for covering numbers of convex hulls. Bartlett (1998) combined these into Theorem 17.
Let be a set and a class of functions . For , a sequence is -shattered by if there is such that for every some satisfies for all . The fat-shattering dimension is
A cover of a class at scale for a pseudometric on functions is a set of functions such that every has some with ; is the least size of a cover. For a sample the pseudometrics , , are the maximum, the mean, and the root mean square of over , and the uniform covering numbers are .
The hidden units form a nonempty class of functions . For the two-layer network class with ℓ1-bounded output weights is
In Lean these are BartlettNN.Margin.fat, BartlettNN.Margin.coverNum and BartlettNN.Margin.Ninf (shared with mission I), and BartlettNN.FatNet.N1, BartlettNN.FatNet.N2 and BartlettNN.FatNet.combos F A.
There is a universal constant such that for every , , , and with ,
The constant is left unspecified, as in the paper, so that the goal survives any improvement of the numerical constants.
Theorem 17 bounds the capacity of a network class without reference to the number of hidden units . With Theorem 2 (mission I) it gives misclassification bounds for networks with small weights that hold for networks of any size, and by iteration it yields the bounds for deep sigmoid networks of Theorem 28 (mission III). Its method — upper-bound ℓ2 covering numbers through Maurey's lemma and compare with a lower bound in terms of fat-shattering — is a template for bounding the fat-shattering dimension of convex hulls in general.
The results are proved in the paper (Lemmas 19 and 21 by citation). None of them is formalized: the platform has no fat-shattering dimension, no uniform sample covering numbers of function classes, and only a finite-dimensional, diameter-based form of Maurey's lemma (HighDimProb.Appetizer.approx_caratheodory), which is not Lemma 21. This mission produces machine-checked statements of all five ingredients and of the theorem.
The obvious route would bound through a VC-type count of the network's parameters, which fails because is unbounded. The paper's route needs a lower bound on covering numbers by the fat-shattering dimension (Lemma 19, a combinatorial packing argument not proved in the paper), an upper bound by the fat-shattering dimension at a finer scale (Lemma 20, which goes through the Alon et al. scale-sensitive Sauer lemma and a quantization argument), and a probabilistic approximation argument in the empirical space (Lemmas 21 and 22). The final step solves a transcendental inequality (6) for , with care at the boundary where the logarithm is small.
X → ℝ; fat is valued in ℕ∞, so an unbounded shattering is , not a junk . Labels are Bool read through pm (true ↦ 1); sequences are indexed by Fin m (0-based).Metric.coveringNumber (closed balls, metric types) is not used.Contributions welcome: proofs of the five milestones and of the goal, and reusable infrastructure on fat-shattering and covering numbers of function classes.
The conditional logit model is the workhorse of discrete choice analysis in econometrics, transportation planning, marketing and revenue management. An individual facing a finite set of alternatives picks alternative with probability proportional to , where is a vector of observed attributes and an unknown parameter vector. Daniel McFadden's 1974 chapter, Conditional Logit Analysis of Qualitative Choice Behavior, derived this model from a theory of random utility maximization and set out how to estimate by maximum likelihood. McFadden received the 2000 Nobel Memorial Prize in Economic Sciences for his development of theory and methods for analyzing discrete choice.
Every confidence interval and hypothesis test computed from a fitted logit model rests on the large-sample theory in §III of that chapter: the maximum likelihood estimator exists with probability tending to one, converges to the true parameter, and is approximately normal with covariance given by the inverse information matrix. This mission formalizes that theory, Lemmas 5 and 6 of the paper, as proved in its Appendix.
Observations are indexed serially, , as in the paper's Appendix ("Let m be a serial index of trials and repetitions"). Observation offers alternatives, and alternative carries a vector of independent variables. For a parameter the selection probabilities are
The data are generated at a true parameter : the chosen alternatives are independent random variables with . The log-likelihood of the first observations is . The moment matrix of observation is
Axiom 7 asks that and uniformly, and that converge to a positive definite matrix . Axiom 6, for a given sample, asks that no nonzero satisfy for all observed and all . A maximum likelihood estimator is a measurable choice of a maximizer of , wherever one exists.
The result. Lemma 6 is what licenses reading as approximately , so that the diagonal of the inverse information matrix estimates the sampling variances and is asymptotically . Lemma 5 complements it: in finite samples the likelihood can fail to have a maximum (the observations are then "explained" by a direction of Axiom 6), and the lemma shows this failure is asymptotically negligible. The data are not identically distributed (each observation has its own alternatives), so the result is not an instance of the textbook i.i.d. maximum likelihood theorem.
Formalizing it. The results are proved in the paper, in outline. A machine-checked version adds: a complete proof of the existence part (Lemma 5), whose published argument is a sketch by induction over an infinite index set; a precise treatment of the estimator where no maximizer exists; the correction of two misprints in the published proof (the normalization in (58), which must be , and a constant in (51)); and a multivariate Lindeberg–Feller central limit theorem for bounded, independent, non-identically distributed vectors, which the proof invokes and which is reusable well beyond this paper. No machine-checked proof of these results is known.
The obvious route, "the log-likelihood is concave, so its maximizer converges", needs a maximizer to exist, and in a finite sample it may not; the estimator is defined only on an event whose probability must first be shown to tend to one. Consistency then needs a uniform law of large numbers for the gradient on a sphere around , controlled by the third-derivative bound (43). Asymptotic normality needs a central limit theorem for independent but not identically distributed score vectors, with covariances that converge only on average; the i.i.d. central limit theorem does not apply. Finally the random Hessian at an intermediate point must be shown to converge in probability, which ties the consistency result into the normality argument.
EuclideanSpace ℝ (Fin K); is the inner product, and all norms are Euclidean (footnote 11's sum-of-absolute-values norm is equivalent and gives the same qualitative axiom); derivative bounds use operator norms.TendstoInMeasure. Asymptotic normality is TendstoInDistribution to a random vector whose law is stdGaussian. is the positive semidefinite square root CFC.sqrt.The conditional logit model assigns probabilities to choices among alternatives whose observable attributes differ from trial to trial. A fitted parameter vector is usually obtained by maximizing a log-likelihood. For a finite data set, however, maximization need not produce a finite vector: some directions in parameter space can keep improving the likelihood while their length grows without bound. McFadden identifies a condition that rules out these directions and then gives a quadratic program that can test the condition. This mission formalizes that test, Lemma 4 of the published 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior.
The chapter develops a statistical model from observable choice data and addresses the existence of a maximum likelihood estimate in Lemma 3. Lemma 4 turns its existence condition into a finite optimization problem. The diagnostic matters because an optimization routine returning increasingly large parameter estimates is not, by itself, evidence that a finite maximizer exists. The result specifies a mathematical test tied to the observed choice counts and the attributes of the alternatives.
There are trials. Trial offers alternatives, indexed by and . Alternative has an attribute vector , and counts how many times it was selected in that trial. Each trial has at least two alternatives and observations. The vector is the unknown parameter of the underlying conditional logit model. Equation (16) assigns alternative a probability proportional to , with the probabilities normalized over the alternatives in the same trial McFadden, pp. 113–114, equation (16).
For the test, define the weighted difference
It is indexed by every trial and every ordered pair of alternatives, including and alternatives whose observed count is zero. Such terms simply produce zero vectors. Keeping them in the index set makes the formal statement agree with the chapter's quantifiers and its quadratic program.
Axiom 5, called full rank in the chapter, says that the rows obtained by subtracting each trial's probability weighted mean attribute vector from its alternative attributes have rank . Equivalently, the vectors span ; the probability weights in that mean are strictly positive and sum to one. Axiom 6 says that no nonzero direction satisfies for every ordered index triple. These are conditions on the same observed experiment, but they serve different roles: full rank concerns the attribute geometry, while Axiom 6 also uses the choice counts McFadden, p. 116, Axioms 5–6.
Let be the set of feasible vectors
The mission's goal is the equivalence in Lemma 4:
The right side means that the program attains a value of zero. An infimum of zero without an attained feasible point would be a weaker statement and would not express the lemma. The three milestones follow the three assertions in the printed proof: a zero minimum implies Axiom 6; an interior origin in the cone generated by the gives positive coefficients and a zero minimum; and a noninterior origin gives a separating direction that violates Axiom 6 McFadden, p. 117, Lemma 4 and equation (22).
Lemma 3 of the chapter states that Axiom 6 characterizes the existence of a vector maximizing the conditional-logit log-likelihood under the preceding axioms. Lemma 4 gives a finite quadratic-programming criterion for that same condition. It therefore allows the model's existence question to be checked from data before treating a numerical optimizer's output as an estimate McFadden, pp. 116–117, Lemmas 3–4.
The paper proves these results. The work here is to produce machine-checkable statements for the finite-dimensional data, the two axioms, the feasible set, and the equivalence, followed by proofs in the solver stage. The cone and separation milestones can support later formalizations of existence conditions in other finite exponential-family models, provided their hypotheses and signs are checked anew. This mission does not claim a general theorem for all such models.
The tempting diagnostic is to ask whether a numerical solve returns a small objective value. That does not settle the mathematical question: the objective's infimum could approach zero without the feasible set containing a zero vector. The paper's conclusion is about a minimum, so attainment must remain visible in the formal statement. There is also a distinction between positive coefficients in a cone representation and the printed constraints in equation (22). Both conditions must appear in their proper places.
The full-rank condition alone does not ensure that the vectors span the attribute space if a trial has no observed choices. The section describes repetitions of each trial, and the formal data require . This convention is needed for the strict-inequality claim in the first paragraph of Lemma 4's proof. The geometry also has to account for every ordered pair, even when its vector is zero; dropping these indices would alter the program stated in the chapter.
Lean represents a nonempty set of trials by Fin N, alternatives in trial by Fin (J n), counts by natural numbers, and attributes by EuclideanSpace ℝ (Fin K). The count is the sum of observed choice counts. The model requires and for each trial. There is no extra assumption that : the zero-dimensional case is included and the equivalence has its ordinary degenerate meaning there.
Axiom 5 is encoded through the equivalent span of within-trial attribute differences. This removes the parameter dependent logit probabilities from a theorem that only uses rank. Axiom 6 retains exactly the nonpositive sign and every from the page. The feasible set uses coefficients at least one, while the auxiliary generated cone uses nonnegative coefficients. The quadratic objective is the square of the Euclidean norm. IsLeast on its image over the feasible set expresses an attained minimum, so the statement cannot be satisfied by a vacuous or unattained infimum.
The definition bundle and the three proof-step theorems are the mission's direct scope. A complete development needs finite-dimensional inner-product geometry, finite sums, a cone interior argument, and separation. The definitions of weighted differences and the feasible set are reusable for studying nearby existence tests. Contributions that prove the stated milestones or supply faithful finite-dimensional geometry for them are welcome; substitutions that weaken the coefficient constraint or the attainment claim do not establish Lemma 4.
Neural-network classifiers can be made to change their output by perturbations of the input that are imperceptible to a person. A certified defense is a classifier together with a proof that its prediction at a point does not change for any perturbation in a stated set, typically an ball . Randomized smoothing turns an arbitrary base classifier into one with such a certificate by classifying Gaussian-noised copies of the input and returning the most likely class. Cohen, Rosenfeld and Kolter (arXiv:1902.02918v2, ICML 2019) gave the certified radius (their Theorem 1) and showed, in their Theorem 2, that this radius cannot be enlarged when only the two class-probability bounds are known about the base classifier. This mission formalizes Theorem 2. Theorem 1 is the subject of the companion mission of this series.
Earlier certificates for the same smoothed classifier, by Lecuyer et al. (2019) via differential privacy and Li et al. (2018) via Rényi divergence, gave smaller radii. Theorem 2 shows that no further analysis that uses only the class-probability bounds can improve on Theorem 1.
Inputs live in with the Euclidean norm ; classes form a set . A base classifier is a map with Borel decision regions. For a noise level , write for the isotropic Gaussian law of with . The class probability of at is , and the smoothed classifier is
Let be the standard Gaussian CDF and its inverse on . A classifier is consistent with the observed class probabilities (6) for a top class and numbers if
The certified radius is . In Lean these are gaussNoise x σ, classProb f σ x c, IsConsistent f σ x cA pA pB and radius σ pA pB in the namespace Cohen2019.Tight, with Phi and PhiInvReal from the series' shared module Cohen2019.Robust; the half-spaces and of the paper's Appendix A are setA and setB.
Quotations write the paper's underlined lower bound as p̲A and its overlined upper bound as p̄B. The PDF has no printed page numbers; every page cited is the PDF page of arXiv:1902.02918v2.
Assume , , and that some finite set of classes other than satisfies . Then for every with there is a base classifier consistent with (6) and a class with
so that under any tie-breaking. The classifier may depend on .
The class-capacity hypothesis is a correction. As printed, with only , the theorem fails for two classes: with , , and , one has , yet every consistent gives probability at least , and Theorem 1 then certifies radius .
The milestones are the steps the paper itself states, in its order: the Claims and for ; the disjointness of and (corrected to "null" when ); equations (13) and (14) for ,
the equivalence ; and the existence of the worst-case classifier satisfying (6) with equalities.
Theorem 2 makes the guarantee of Theorem 1 exact: when only (6) is known about , the set of perturbations under which the Gaussian-smoothed prediction is provably constant is exactly the open ball of radius . It settles that improvements to Gaussian-smoothing certificates must use more information about the base classifier than the two bounds, as later work on higher-order and Lipschitz-based certificates does.
The paper's proof is complete in its main lines and has two gaps that this mission records and repairs: the printed statement omits a condition on the number of classes, and the claim fails at . To our knowledge neither Theorem 1 nor Theorem 2 has a machine-checked proof. Mathlib at the pinned revision has the multivariate standard Gaussian but no normal quantile function and no Gaussian half-space lemma; this mission adds statements for both kinds of fact.
Each step is elementary on paper but rests on facts about Gaussians that Mathlib does not package: the image of the standard Gaussian on under a linear functional is the one-dimensional Gaussian with variance , and is a continuous strictly increasing bijection with . The construction of has a further step the paper leaves informal: the region between and , of mass , must be shared among "other classes" with none exceeding , which is where the capacity hypothesis enters. Measurability of the constructed decision regions must be carried along.
is EuclideanSpace ℝ (Fin d). is the pushforward of Mathlib's stdGaussian under , with a binder. is cdf (gaussianReal 0 1); is the generalized inverse , which is the true inverse on and the junk value at the endpoints, so every statement that evaluates it assumes ; at or the paper's radius is infinite and Theorem 2 is vacuous. Class probabilities are real numbers. The base classifier in the conclusion is deterministic with Borel decision regions, which is the stronger existence statement. The conclusion is the strict inequality between class probabilities, not merely the failure of to be a strict unique argmax.
A formalization in which the junk endpoint value of makes negative, or in which the classifier's decision regions are non-measurable so that its class probabilities are default values, would make the goal trivial; the hypotheses above exclude both.
Reusable beyond this mission: the Gaussian half-space probabilities and the normal quantile on . Contributions of general Mathlib-style lemmas (the law of for , properties of ) are welcome.