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.
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?
Classical Markov decision theory minimizes expected cost. A decision maker who dislikes variability, such as an insurer, a portfolio manager or an operator of a service system, may instead evaluate a random cost by its certainty equivalent for an increasing utility (disutility) function . Bäuerle and Rieder (More Risk-Sensitive Markov Decision Processes, Math. Oper. Res. 39(1), 2014; authors' manuscript at KIT 1000039663) develop dynamic programming for this criterion with general . Classical risk-sensitive MDPs, studied since Howard and Matheson (1972), use the exponential utility, and for it the average cost problem differs considerably from the risk-neutral one (Cavazos-Cadena and Fernández-Gaucherand 2000; Di Masi and Stettner 1999). Their §5 asks what happens in the long run. The average cost per stage is evaluated through a power utility . Does risk sensitivity change which stationary policy is optimal?
This mission formalizes their answer, Theorem 5.2, and the results its proof uses (manuscript p. 17).
A controlled Markov process in discrete time has a standard Borel state space and action space . A measurable set lists the admissible state–action pairs, and every is nonempty. A transition law gives the distribution of the next state, and a measurable cost satisfies on .
A history-dependent policy chooses the action measurably from the past. The set of all such policies is . Each and initial state determine a probability measure on trajectories, with and . The accumulated cost is .
A stationary policy uses a measurable decision rule with at every stage. Under it, is the Markov chain with kernel .
Fix and . The risk-sensitive average cost (5.1) and its optimal value are
The risk-neutral average cost is , the case .
A Markov chain is Harris recurrent if, for some nonzero -finite measure , every set with is visited infinitely often almost surely from every starting point. It is positive Harris recurrent if it also has an invariant probability measure (Meyn and Tweedie 2009, §§9–10). The MDP is called positive Harris recurrent if the state chain of every stationary policy is.
Let and let the MDP be positive Harris recurrent. If satisfies for all and , then
The optimal policy does not depend on .
The result. Theorem 5.2 reduces a risk-sensitive long-run problem to a classical one. Under positive Harris recurrence, any stationary policy that is optimal for the expected average cost, for instance one obtained from the average-cost optimality equation, is also optimal for every convex power criterion , simultaneously. Theorem 5.1 explains why: along a positive Harris recurrent chain the empirical average cost converges almost surely to a constant, so in the limit the power utility sees no randomness at all. The contrast is with exponential utility, where the risk-sensitive average cost generally differs from the risk-neutral one and leads to a multiplicative Poisson equation. Positive homogeneity of the utility is what removes the risk effect.
Formalizing it. The results are proved in the paper. As far as is known they have no machine-checked proof, and the platform has no strong law of large numbers for Harris chains on general state spaces. The mission produces a Borel MDP with history-dependent policies and Ionescu-Tulcea path measures, a reusable definition of (positive) Harris recurrence for an arbitrary Markov kernel, and a formal comparison of risk-neutral and risk-sensitive average costs. Each milestone is a self-contained target.
Milestones 1 and 3 are elementary once the expectations are handled correctly: holds only almost surely, and Jensen's inequality has to be applied with real powers. The central difficulty is Theorem 5.1. It needs the ergodic theorem for positive Harris recurrent chains, almost surely from every initial state (Meyn and Tweedie, Theorem 17.0.1). It also needs an identification of the state process under with the canonical chain of . The natural first idea, to quote a convergence theorem in total variation, fails: positive Harris recurrence allows periodic chains, for which need not converge. Pathwise averages converge, marginal laws need not, and the argument has to work with the former.
Kernel.trajMeasure on . Stationary policies act through .Real.rpow. For all terms of the sequences lie in , so real limits superior are meaningful. The term (Lean's ) is irrelevant.Contributions are welcome at every level. Reusable pieces, such as the identification of the state process with the chain of , the strong law for positive Harris chains, or bounded-convergence lemmas for path measures, are valuable beyond this mission.
Sequential decisions often have costs whose timing matters. A controller may choose an action now, observe a random next state, and choose again. Ordinary expected-cost minimization averages the sum of the costs. A risk-sensitive criterion first applies an increasing function to the total cost and then takes its expectation. The curvature of changes how uncertain costs affect the ranking of policies: convex utility penalizes variability in a cost-minimization problem, while concave utility has the opposite tendency. Bäuerle and Rieder study this criterion for controlled Markov processes with general continuous increasing utility, rather than fixing an exponential function. Their finite-horizon discounted result is Theorem 3.6, pp. 10–12 of the authors' manuscript.
Discounting gives early and late costs different weights. For linear , the remaining expected cost can be described using only the current physical state. For general , the effect of a future cost also depends on what has already been paid and on the discount weight currently attached to the next cost. The mission targets the paper's finite-horizon treatment of these two additional quantities. The infinite-horizon problem is a separate part of the paper.
The state space and action space are Borel spaces. At state , the nonempty set contains the actions that may be chosen. If action is selected, the next state has distribution and the stage cost is . The cost is measurable and bounded between positive constants and . The discount factor satisfies , and is continuous and strictly increasing. The paper imposes its compactness and continuity conditions (CC) on , , , and ; these are stated in the model item and correspond to §2, pp. 3–4.
A history policy chooses measurably from the states and actions observed through time . Starting from , it induces a law for the state-action trajectory. The first stages incur the discounted cost , with . The paper minimizes over every admissible history policy. The inverse utility appearing in the paper's original certainty-equivalent criterion can be omitted when selecting a minimizer because is strictly increasing §2, p. 3; §3.3, p. 10.
The extended state is . Its coordinates record the current physical state, accumulated cost, and current discount weight. Define and . A measurable extended-state decision rule chooses an action in . The paper's operator integrates a continuation value at ; takes the infimum of the same integral over equations (3.8)–(3.9), pp. 10–11.
The first target identifies the cost iteration of any sequence of extended-state rules :
The second target is the paper's value iteration for the infimum over all history policies, together with membership of every in its regularity class :
The goal is Theorem 3.6(c): minimizers of exist, and their stage-dependent history rules attain the original objective for every . At stage , the rule uses at the current state, the observed sum , and . “Optimal” compares against all admissible history policies, including those that use more of the history than these three quantities.
Theorem 3.6 gives a finite sequence of minimum-operator evaluations for a problem whose utility of total cost is not additively separable in the physical state alone. Its policy statement also identifies which observable quantities an optimal controller needs to retain. Together, these results relate the original history-dependent problem to an extended-state Markov decision problem §3.3, pp. 10–12.
The paper proves these statements. This mission asks for machine-checked definitions and proofs of the finite-horizon discounted theorem, including the comparison with all admissible history policies. The model layer and the finite-dimensional expectation construction can support later formalizations of other risk-sensitive objectives. The mission itself has no completed proof at the drafting stage.
The extra discount coordinate is essential: after one action, the next cost enters utility with weight , not . Keeping only accumulated cost would describe a different process. The other demanding point is the policy comparison. An iteration over extended-state decision rules has to establish the value of an infimum over arbitrary measurable history policies. Regularity and measurable selection must also be maintained at each step under (CC). The proof of Theorem 3.6 invokes the corresponding total-cost argument from Theorem 3.1, pp. 5–6; the formal development must supply the precise discounted version.
Lean represents and as Borel subsets of Polish spaces, with standard Borel measurable structures. The controlled process is a separate reusable definition containing , , and history policies; the risk-sensitive model adds , , and . The admissible graph is Borel and every section is nonempty. A history is a chronological finite list of earlier state-action pairs and a current state. Each rule is defined on all lists, but only admissible lists of the matching length are visited. The transition kernel is total as a Lean object, and its values outside are irrelevant.
Policy values use nested kernel integrals representing the finite-dimensional marginals of the path law. They are defined from the cost and utility, so the Bellman recursion remains a theorem. The optimized value is an infimum over the subtype of measurable, admissible infinite history policies. The real infimum is meaningful here because this policy class is nonempty under (CC) and finite-horizon costs keep utility bounded on the relevant interval. The extended state uses real coordinates restricted to and ; its transition stays in that domain. “Increasing” in means componentwise nondecreasing in . A minimizer is an admissible measurable rule satisfying on the entire extended domain.
The source's proof sentence that preserves is recorded with explicit integrability of each one-step continuation. For an arbitrary real-valued member of on an unbounded state space, the source's conditions alone do not ensure a finite real expectation. This domain condition prevents Lean's zero value for a nonintegrable real integral from turning the assertion into a different one. It does not narrow the finite-horizon values appearing in the goal. Contributions toward finite-dimensional expectation identities, kernel integrability, the regularity of , and measurable minimizer selection are within scope.
When a controller acts on a system whose state is hidden, measurements may help it choose later actions, but the value of those measurements depends on the transition law, the observation mechanism, and the available controls. Åström's 1965 paper gave a finite-state formulation of this problem and compared the best expected loss under incomplete measurements with two limiting cases: exact state observations and no useful observations. The comparison, stated in (5.12), quantifies the value of the information available to the controller without requiring a particular numerical example. Åström, 1965.
The bounds are useful when an exact partially observed policy is difficult to calculate. The complete-information problem provides an optimistic benchmark, because a controller that sees the hidden state can condition its decision on more information. The open-loop problem provides a conservative benchmark, because it commits to a control schedule without responding to later measurements. Both auxiliary problems have simpler backward equations than the partially observed problem, as Åström notes in §V of the paper. Åström, 1965, pp. 190–193.
The hidden state belongs to a finite nonempty set , and the measured output belongs to a finite nonempty set . There are decision stages. At stage , a control is chosen from a nonempty compact set . Given state and control , the next state is with probability . At state , the observed output is with probability ; observations are conditionally independent given the state path. The stage loss is , with no fixed sign, terminal loss, or discount. The transition probabilities and loss are continuous in the control. Åström, 1965, §II.
An admissible control law may use the whole output history when choosing . Write for its expected total loss, computed from the joint law of the state and output paths, and write for the infimum of over every such admissible law. The distribution of is . After the first output , the belief is the conditional distribution of . More generally, is the conditional distribution of given outputs through time , when that history has positive probability.
Three backward values describe the information regimes. The partial-observation value obeys the Bayesian recursion (3.28). The complete-information value is the linear extension of the statewise recursion (5.4). The open-loop value obeys (5.7), in which the belief moves by prediction through without using an output. Each recursion has terminal value zero at . Åström, 1965, pp. 184, 190–191.
Theorem 2 identifies the partial-observation value with the original control problem: a selector attaining the minimum in (3.28) exists, and every such selector yields an admissible feedback law attaining . Theorem 4 gives the complete-information lower bound , and Theorem 5 gives the open-loop upper bound for every probability belief and every stage . Both inequalities apply to a general observation matrix. Åström, 1965, Theorems 2, 4 and 5.
The goal is the paper's expected-cost comparison (5.12), with its middle term explicitly identified as the minimum of the original problem:
Here the expectation is over the first measured output under and . An output with probability zero contributes zero. The left and right members represent, respectively, the costs with perfect state information and with no useful measurements. Åström, 1965, (5.12), p. 193.
For any model satisfying the stated finite-state assumptions, the two easier dynamic programs bracket the best achievable expected loss with partial information. The differences between these values are the paper's measures of the value of perfect state information and the value of incomplete state information, described immediately after (5.12). Because the loss may have either sign, these are order comparisons of minimal costs rather than bounds that depend on a nonnegativity convention. Åström, 1965, (5.13)–(5.14).
The mathematical result was established in the paper. This mission asks for machine-checked proofs of its finite-path model, the three value recursions, the identification of P.1's minimum, and the information bounds. The value functions are linked by shared definitions, so later finite-state partially observed control developments can reuse the pathwise cost and Bayes update instead of rebuilding them for each theorem.
The tempting comparison between the three Bellman equations cannot simply replace the posterior belief by its average: the controller may choose different actions after different observations, and the continuation value is generally nonlinear in the belief. The exact-information case must also be read at beliefs concentrated at a single state. Its value formula is linear in an arbitrary input belief by definition, but the partial-observation value need not equal that linear function away from those state vertices. A second issue is connecting a feedback solution of (3.28) to the original expected loss over all output-history laws; using a belief-defined objective at the outset would assume the identification that Theorem 2 establishes.
The Lean model uses finite state, output, and horizon types, a nonempty compact control set in , stochastic transition and observation rows, and continuous dependence on controls where the paper requires it. All probabilities and expectations are finite sums and products. A Fin N index of zero represents paper time one. The model starts from the law of , since §II introduces the law of but specifies neither a control at time zero nor the transition to . The transition controlled at time is therefore written with the paper's transition index . These conventions make the first-output expectation and (3.22) use the same timing.
The norm of is its norm, the sum of absolute coordinates. At an impossible output, Lean's totalized posterior is zero; the associated continuation term has weight zero. Conditional-probability claims apply only to positive-probability histories. Each minimum over controls is represented by a real infimum over . The compact control set is nonempty and the continuous costs are bounded on it, so this has the intended finite attained meaning on probability beliefs. The terminal values , and are zero.
The original objective is a separate pathwise expected cost, minimized over all admissible output-history laws. The target includes its equality with ; stating only an inequality between three unrelated Bellman solutions would omit the subject of (5.12). Reusable contributions include finite-path probability identities, the Bayes recursion, attainment for continuous control minima, and the three value comparisons. No special observation matrix is assumed in Theorems 4, 5, or the goal.
In a congestion game, several users choose facilities and each facility becomes more costly as more users choose it. Such games model settings in which each participant chooses a route or collection of resources for personal use while the resulting load is shared. A pure Nash equilibrium is a stable choice of routes: no single participant can lower their own cost by switching. Stability alone gives no assurance that the resulting allocation serves the group well. The price of anarchy compares the social cost of an equilibrium with the best social cost attainable by coordinated choices.
Christodoulou and Koutsoupias studied finite congestion games with linear latency functions and several notions of social cost. For the maximum cost borne by any player, their STOC 2005 paper gives both an upper bound valid for all such games and a family of instances showing that its square-root dependence on the number of players has the right order. This mission formalizes those two claims together. The maximum criterion matters when a single heavily delayed user is significant even if the total cost of the population is moderate.
Let be the number of players and let be a finite set of facilities. Player has a finite collection of available pure strategies, each a subset of . A profile chooses one strategy for every player. For a facility , its load is the number of players whose chosen strategy contains . The latency of at load is . Player pays the sum of the latencies on the facilities they chose:
A profile is a pure Nash equilibrium if no player can decrease this cost by replacing their own strategy while the others keep theirs. The paper calls latencies linear when with ; these are affine functions in standard terminology. The paper displays many calculations for the special case and states the general nonnegative affine convention in its model section. The maximum social cost is ; the total cost is . The paper's average social cost is .
For a game with at least one pure Nash equilibrium and a positive optimal maximum cost, the maximum-cost pure price of anarchy is the largest equilibrium value of divided by the smallest feasible value. The Lean targets use inequalities against every feasible comparison profile rather than dividing by an optimum. This form continues to say something when an optimum has cost zero, and finite strategy sets ensure an optimum exists whenever the profile space is nonempty.
For every , every finite game with nonnegative affine latencies, every pure Nash equilibrium , and every feasible profile , Theorem 5's proof yields
This states a numerical version of the paper's theorem without an unspecified constant. Taking to minimize gives the corresponding price-of-anarchy bound. The bound is about asymmetric games: players may have different strategy sets, and no symmetry assumption is present.
For every integer , let . Theorem 6 provides an identity-latency congestion game with players and facilities, a pure Nash profile , and an optimal profile for which
Every feasible profile in the instance has maximum cost at least . Thus the ratio is , and . The proof's explicit instance has positive comparison cost, so the lower bound cannot be satisfied by a zero-cost game. The source also says such behavior occurs in network congestion games and sketches a network realization in Figure 2; this mission's formal lower target is the finite congestion-game construction.
Together these results identify the order of growth of the worst pure equilibrium maximum cost relative to an optimum: it can grow with the population, yet for linear latencies it grows no faster than a constant times . The upper statement applies to any feasible comparison profile, so it can also be used when a convenient benchmark is known without solving the entire optimization problem. The lower family prevents replacing the square-root dependence by a bound independent of for this class of games.
The results are proved in the 2005 paper; the mission is to give them machine-checked Lean proofs in a common finite-game representation. The development also supplies reusable definitions of congestion games, loads, pure cost equilibria, and maximum social cost, together with the total-cost estimate of Theorem 1 and the intermediate bounds appearing in Theorem 5. The current draft contains statements with sorry placeholders, not completed proofs.
A bound on total player cost does not directly control the cost of the most expensive player sharply enough. An individual player can use several facilities whose loads interact, and bounding each load separately loses the dependence required for the square-root result. Affine coefficients add another issue: the proof printed for identity latencies writes a cardinality where the general statement needs a coefficient-weighted quantity. The lower example has an indexing discrepancy in the printed alternative strategies, so the intended Nash profile must be checked against the costs on every permitted deviation.
Players are represented by Fin N; facilities by an arbitrary finite type in upper bounds and by a type with elements in the lower family. A profile is a function from players to finite facility sets, with feasibility stated separately. Latencies are real-valued on natural-number loads. The IsLinear predicate requires explicit nonnegative affine coefficients. Pure Nash uses a cost inequality; it is the negative-payoff version of a standard finite game's payoff equilibrium. MAX requires at least one player, and all upper-bound targets therefore require . The lower family begins at , where is positive.
The source's number is written as in Lean to keep natural-number subtraction inside its valid range. The two expressions agree for . In the source's one-based indexing, the proposed alternative strategy uses a ceiling index. The printed denominator makes some alternative facilities carry users and breaks the Nash assertion; denominator agrees with Figure 2's short-route users per layer and gives the stated costs. This correction is recorded with the lower theorem. No normalization of coefficients or artificially restricted strategy class is assumed. Contributions to the finite-game definitions, Theorem 1, the player-cost bounds, and the explicit lower instance are all in scope.
Approximate message passing (AMP) is an iterative method for large systems with random matrices. At each step, every coordinate receives a weighted combination of nonlinear messages from all other coordinates, together with a correction for dependence created by earlier steps. For symmetric random matrices, the correction makes a simple description of the high-dimensional iterates possible: a finite collection of covariance matrices predicts their limiting distributions. Bayati, Lelarge and Montanari prove this state evolution statement for polynomial AMP on a broad class of independent sub-Gaussian matrix entries, rather than only Gaussian entries (paper, §§1.2–1.3). It gives a precise distributional account of an algorithm whose coordinates are coupled at every iteration.
The paper has three distinct headline results. Its Theorem 3 compares AMP moments under two matrix laws with equal entry variances, and its Theorem 2 concerns projected cross-polytopes. This mission targets Theorem 4, which identifies the limit of empirical averages of AMP iterates with a Gaussian expectation. The companion missions address the other results; the statements here use their own copy of the paper's AMP model because draft definitions cannot yet be imported across proposals (paper, pp. 5, 8–9).
For each size , let be a random symmetric matrix with zero diagonal. Its entries above the diagonal are independent, centered, and sub-Gaussian at scale . Each coordinate carries a polynomial map at iteration and an initial vector . Their coefficients have degree at most and a uniform bound . The AMP orbit is
The second sum is the Onsager memory term; it is absent at . Here is the Jacobian, so its product with the preceding -vector is another -vector. The initial vectors obey an exponential bound on their squared Euclidean norms. These assumptions form the paper's -regularity condition (Definitions 2–4, pp. 6–7).
A converging sequence has a fixed finite set of classes . Coordinate belongs to for one class , whose proportion approaches . A symmetric nonnegative matrix specifies entry variances: if and , then . Independent labels have class-dependent laws , each a finite mixture of Gaussian laws that may be degenerate. The polynomial maps have the common form for (Definition 5, pp. 8–9).
The empirical second moments of converge in probability to a prescribed positive semidefinite matrix . For , state evolution defines
where is independent of . The index in the first formula and in the second are essential (equations (1.9)–(1.11), p. 9).
For a nonnegative multi-index and a coordinate sequence eventually in class , Proposition 4 identifies the Gaussian limit of each moment. Proposition 5 says the variance of the class-average monomial tends to zero:
The diagonal two-time identity (4.4) is another milestone: has four blocks, each equal to . These are the paper's stated intermediate targets (pp. 15, 30, 32).
For , class , and every locally Lipschitz function with for some , prove convergence in probability:
The target covers polynomial-growth test functions, including functions beyond monomials. The expectation on the right is under the product law of the Gaussian state and the independent class label (Theorem 4, p. 9).
The theorem assigns a computable asymptotic distribution to each class of AMP coordinates at every fixed positive iteration time. It can be used to evaluate empirical observables without tracking the full coupled -dimensional random trajectory. The class weights and variance profile permit heterogeneous coordinates, while the sub-Gaussian assumption covers more matrix laws than a Gaussian-only statement (paper, Introduction and Theorem 4).
The paper proves this result. The mission's Lean statements are compilation-checked targets, with proofs still to be formalized. A completed development would establish the measure-theoretic meaning of the covariance recursion and its Gaussian expectations, as well as the moment and concentration claims needed for the empirical limit. The polynomial representation, random-matrix regularity predicate, and Gaussian transport are reusable for other AMP results from the same paper.
The matrix is reused at every AMP iteration, so a new coordinate is correlated with earlier coordinates and with the matrix entries that produced them. A direct independent-summand argument for its Gaussian limit is unavailable. The memory term is tuned to this dependence, and any formal proof must account for its exact Jacobian and squared-entry form. Passing from individual moments to empirical averages also requires control of correlations between different coordinates. The target allows locally Lipschitz functions with polynomial growth, so convergence for a fixed monomial alone does not finish the job (paper, §4.7).
Vectors in are functions Fin q → ℝ; squared Euclidean norms are explicit sums of coordinate squares. Polynomials use bounded real coefficient arrays as in (4.10), with an explicit Jacobian. Fin N uses zero-based indices. The orbit stores the current and preceding iterates and omits the memory term at . A single probability space carries all sizes; matrix entries, labels, coefficients, and initial vectors have explicit measurability and independence conditions.
The paper's displayed sub-Gaussian formula conflicts with its stated scale, so the model uses the scale required by its moment estimates and imposes the moment-generating bound for all real arguments. Its initial exponential bound is read almost surely at every size, which ensures the expectations used by the paper are well-defined. Label-dependent polynomial coefficients are measurable. The full label vector is independent of the matrix and initial vectors; this makes explicit the independence needed for Theorem 4's Gaussian-label product law. Independence of the induced polynomial coefficients alone would not imply it when ignores part of a label. The initial covariance limit is entrywise convergence in probability; finite-dimensional equivalence makes this the same matrix convergence. Class averages divide by the class cardinality, even though that expression has Lean's default value at an empty class for a small . Positive limiting class fractions make those finite exceptions irrelevant.
Gaussian laws live on Mathlib's Euclidean space and are transported to coordinate vectors. Theorems explicitly assert positive semidefiniteness or integrability where a non-PSD covariance, non-integrable expectation, or non-square-integrable variance could otherwise give a default value. The source's in (1.12) is read as , its summation index, and its final covariance as . The Gaussian covariance is computed by the recursion above; it is not defined from the proposed limit. Contributions establishing moment bounds, covariance positivity, Gaussian integrability, the three milestones, or the full Theorem 4 are within scope.
Policy gradient methods optimize a parameterized policy for a Markov decision process by running gradient descent on its expected cost. They underlie most large-scale reinforcement learning, from robotics to game playing, and are also natural in operations research, where structured policy classes (linear feedback, base-stock levels, thresholds) are standard. The objective, however, is almost never convex in the parameters, and classical theory only promises convergence to stationary points. Whether such methods find optimal policies therefore depends on the landscape: whether stationary points can be suboptimal.
J. Bhandari and D. Russo (arXiv:1906.01786v3, published in Operations Research, 2024, DOI 10.1287/opre.2021.0014) identify structural conditions under which the answer is no, connecting policy gradient to classical policy iteration. Fazel et al. (2018) established a landscape result for linear-quadratic control; Kakade and Langford (2002) developed a performance-difference identity for conservative policy iteration on finite MDPs. Bhandari and Russo's Theorem 1 gives a general sufficient condition on a general state space; Agarwal et al. (2021) developed the tabular case in detail.
A Markov decision process is a tuple : a measurable state space , nonempty feasible action sets , a bounded measurable cost , a transition kernel , a discount factor and an initial probability distribution . A policy is a measurable map ; it is feasible, , if for every .
For a policy , the cost-to-go is the expected discounted sum of costs started from . The discounted average cost is , and the discounted state-occupancy measure is . The Bellman operators are
An optimal policy satisfies pointwise for every . Two standing assumptions hold throughout: Assumption 1, (the initial distribution is exploratory), and Assumption 2, measurable selection of a minimizing action in .
A parameterized policy class is with convex, and is the policy gradient objective. A point is stationary if for all . The weighted policy-iteration objective is
the cost of following for one period and then incurring , averaged over .
The three conditions of the main theorem are:
Under Conditions 0, 1 and 2.A, is continuously differentiable, and for every
The right side compares with the optimum over all feasible policies, not only the class.
Theorem 1 converts a question about a nonconvex, multi-period objective into checks on single-period problems. Any algorithm that provably reaches stationary points (projected gradient descent, for instance) then reaches globally optimal policies whenever the policy class is closed under improvement and the one-step problems are benign. The paper verifies the conditions for LQ control, finite MDPs with softmax policies, optimal stopping with threshold policies and inventory control with base-stock policies; the quantitative refinements (gradient dominance, approximate closure, finite horizons) are the subject of the later missions of this series.
The result is proved in the paper; nothing in it has been machine-checked. A formalization would produce a measure-theoretic library for discounted MDPs on general spaces (cost-to-go via kernels, occupancy measures, Bellman operators, the performance difference identity) that is reusable well beyond this paper, and would pin down the exact differentiability hypothesis the argument needs.
The obvious route, differentiating directly, requires differentiating an infinite discounted sum of -step kernels in the parameter, and on a general state space that derivative is not available without regularity of the transition law. The performance difference identity demands an exchange of an infinite series with integrals against composed kernels, and measurability of every object involved, including , which is measurable only through the selection assumption. The stationary-implies-optimal direction must pass from an inequality weighted by to one weighted by , and then to , where Assumption 1 enters.
and are arbitrary measurable spaces; the paper takes Borel subsets of Euclidean spaces, a structure no argument uses. The cost is bounded and, with the kernel , defined on all of : Condition 0 differentiates at parameters near , where need not be feasible. Policies are deterministic, stationary and measurable; randomized policies are covered by taking actions to be probability vectors. is the Euclidean space, gradients are Euclidean, and is convex (not assumed closed).
Conventions committed to in Lean:
The goal does not assume that contains , the equation of Lemma 7 or the conclusion of Lemma 8; a formalization that takes any of these as a hypothesis trivializes the theorem.
A complete development needs the composition of kernels, interchange of series and integrals for bounded functions, the fixed-point identity , the performance difference identity, the first-order optimality condition on a convex set, and the chain rule for a jointly function along the diagonal. The MDP layer, the identity (29) and the element-wise inequalities are reused by the other missions of the series. Proofs of the milestones, and proofs of the identity (29) in isolation, are welcome.
Large interacting diffusion systems often have different interaction strengths between different pairs of agents. A graphon gives a continuum description of such weighted networks: each agent carries a label in , and a kernel assigns the strength of interaction between two labels. The question in this mission is whether the law of the resulting continuum stochastic system changes continuously when its graphon changes. This matters when a large finite network is represented by an approximate graphon, since an approximation of the network should lead to an approximation of the dynamics. Bayraktar, Chakraborty and Wu establish this stability as Theorem 2.1(c) of Graphon mean field systems.
The paper also studies dense and less dense finite-particle systems. Their convergence results use a limiting graphon particle system even when the limiting kernel is only measurable, with no continuity in the labels. Theorem 2.1(c) is the continuity result that makes approximation by simpler graphons useful in those later sections Bayraktar–Chakraborty–Wu, §§3–4.
Let , fix a time horizon , and let be the space of continuous paths with the uniform norm . A graphon is measurable and symmetric. Its cut norm is the largest absolute integral of over a measurable rectangle . For two graphons, their cut distance is the cut norm of their difference.
For each label , an initial state and a -dimensional Brownian motion live on one probability space. Initial states are mutually independent, Brownian motions are mutually independent, and the two families are independent of each other. The initial state has law . The process evolves with a drift obtained by averaging first against the time- law of and then over . Its diffusion coefficient averages the matrix-valued in the same way and drives . This is the graphon particle system (2.1) Bayraktar–Chakraborty–Wu, p. 3591.
Condition 2.1 requires measurable initial laws, a uniform moment for some , and a common global Lipschitz bound for and . The path-law family belongs to when it is measurable as a family of probability measures on and has uniformly bounded second moments. The distance between path laws uses the supremum norm through time ; is the supremum of these distances over labels Bayraktar–Chakraborty–Wu, pp. 3591–3592.
For graphons converging to in cut metric, let and be the laws of the associated solutions, with the same initial laws and coefficients. The target is
The conclusion is an integrated law convergence statement. It does not assert that the laws converge uniformly in or that paths converge almost surely. This is precisely Theorem 2.1(c) Bayraktar–Chakraborty–Wu, p. 3593.
The mission also states the paper's cut-to-operator convergence (Remark 2.1), existence of frozen-flow solutions (5.2), the squared estimate established in the proof of (5.3), well-posedness and moments for the nonlinear system (Proposition 2.1), and the quantitative stability display on p. 3604. These are the source's claims used to reach the target, with their provenance attached to each milestone Bayraktar–Chakraborty–Wu, §§2 and 5.
Stability shows that the continuum model is robust to graphon approximation in a metric natural for dense networks. Together with Proposition 2.1, it gives a well-defined solution-law family whose dependence on the network kernel can be controlled. The paper uses this framework in its later laws of large numbers for finite interacting systems Bayraktar–Chakraborty–Wu, §§3–4.
The theorem is proved in the paper; this mission asks for a machine-checked proof of the faithful statements. A complete development would also supply reusable Lean interfaces for graphons, cut and operator norms, measurable families of path laws, and stochastic systems whose coefficients depend on those families. The Itô-process and general Wasserstein definitions already available as published modules are reused. The remaining graphon-specific definitions and the estimates in §5 are open proof targets.
A direct stability argument for stochastic differential equations would compare the two coefficients point by point. Cut convergence does not provide pointwise convergence of to , nor a uniform bound on their difference that tends to zero. The drift and diffusion also contain laws generated by the processes being compared, so a change in the graphon feeds back into the law family. The central challenge is to control these coupled differences using only a weak kernel metric while retaining the measurable structure needed to integrate over labels Bayraktar–Chakraborty–Wu, §5.2.
The result also depends on a well-posedness theory for a continuum of stochastic equations. The laws need to vary measurably with even though the paper does not assume the sample paths themselves vary measurably with Bayraktar–Chakraborty–Wu, Remark 2.3(b).
Lean uses unitInterval for , nonnegative real time, and continuous maps from to Fin d → ℝ for . The norm on is the sup norm; the paper's Euclidean norm is equivalent in finite dimension, so existential Lipschitz and stability constants may change while the qualitative claim remains the same. The diffusion coefficient is a matrix, measured through its entries. Wasserstein quantities and nonnegative expectations are valued in , avoiding defaults for infinite moments. The path-law family uses the measurable space of measures, with the Borel space on paths. A zero-time or zero-dimensional state space is admitted where the formulas still have their stated meaning; and are explicit.
For each graphon, a solution is a continuous-path process driven by the same given initial variables and Brownian motions, adapted to the natural filtration of those variables for each label. Its path map is almost everywhere measurable, its law family belongs to , and the nested interaction integrals are required to be integrable. These clauses prevent a zero measure from arising through a nonmeasurable pushforward and prevent a nonintegrable Bochner integral from silently evaluating to zero. The graphons are explicitly measurable, symmetric, and -valued, so the real cut and operator norms are used only on bounded kernels. The theorem also asserts measurability of each Wasserstein integrand, reflecting the paper's treatment of the displayed integral.
The paper's proofs are in §§5–7; this mission concerns §5. Contributions to any stated milestone and to the reusable measure and Itô lemmas needed for them are welcome. A formalization that assumes the stability limit, that treats arbitrary unbounded kernels as graphons, or that uses an empty solution class would not establish this target.
An online decision maker repeatedly chooses an action, observes an outcome, and receives a reward. In a Bayesian model, an unknown parameter controls the outcomes, and the decision maker begins with a prior distribution for that parameter. Thompson sampling acts by drawing a parameter from its current posterior distribution and choosing an action that would be best if that draw were correct. This makes it applicable when an agent can simulate a plausible model and optimize an action for that model. Russo, Van Roy, Kazerouni, Osband, and Wen explain this rule for general online decision problems in Section 4 of their tutorial.
The tutorial's Section 8.1.2 asks how to analyze the rule's expected regret. An upper confidence bound method chooses an action using an optimistic score and can analyze regret through the score's optimism and its uncertainty width. Thompson sampling does not choose its actions by maximizing such a score. Yet the tutorial shows that any score computed from the observed past can be used to split Thompson sampling's expected regret into the same two types of terms. The result is stated on pp. 72–73, equation (8.4) and the display that follows.
Let be a finite, nonempty set of actions, a finite set of outcomes, and a measurable parameter space. A prior probability measure is placed on the unknown parameter . If action is selected, the outcome is sampled from a probability kernel on . A known function turns an outcome into a reward. The mean reward of action under parameter is
For each , choose an action maximizing . This choice uses a fixed tie-break and is measurable. The same selector is used throughout the mission. A length- history records the first action–outcome pairs. A policy assigns an action distribution to every such history. The prior, the policy, and the outcome kernel together determine the law of all histories: first draw from , then choose each action from using the past history, and finally generate its outcome using .
After history , the posterior law of is obtained by reweighting the prior by the likelihood of the observed outcomes. Thompson sampling draws a parameter from this posterior and plays the selected optimum for that parameter. Thus the law of its next action, given , is the posterior law of given . The policy remains defined even for a history with zero likelihood; choices there do not affect expectations.
For a period , let be any real score that uses the action and the observed history . The score is fixed before the period's outcome or the unknown parameter can be inspected. The period regret is , with expectation taken over the prior, the policy's randomization, and the outcome process.
The first target makes posterior sampling precise. For every feasible history and action , the probability that Thompson sampling next plays , together with observing , equals the joint probability that the selected optimum is and the history is . Consequently, for every history-determined ,
This is equation (8.4) on p. 72. It asserts equality of unconditional expectations while preserving the fact that may depend on the past. It does not assert that and have the same joint law with .
The goal is the full chain of equalities displayed on p. 73:
The theorem holds for every score determined by the past history. In particular, need not be a confidence bound for the identity to hold. Being a useful upper confidence bound matters when one later estimates the two terms.
The equality permits analyses built around optimistic scores to be transferred to Thompson sampling. It separates expected regret into a term measuring whether the score falls below the true optimal mean and another measuring the gap between the score and the true mean at the sampled action. The tutorial cites Russo and Van Roy for the surrounding regret bounds; the identity here is the precise bridge used in that discussion.
The result is already proved in the tutorial. This mission seeks a machine-checked proof of its finite-action, finite-outcome form, including the posterior-sampling law, the policy-dependent history distribution, and the conditioning behind equation (8.4). The goal and milestones are open Lean statements, not completed machine-checked proofs. Their definitions can be reused in later finite Bayesian decision models with a general measurable parameter.
The central issue is that and are not interchangeable inside an expression that depends on . The sampled action and the selected optimum have the same distribution after conditioning on the observed past, but generally have different dependence on the true parameter. For example, replacing by would make the claimed equality false. A formal proof therefore has to respect the boundary between history-derived scores and parameter-dependent quantities, and it must use the same history law to interpret every expectation. Histories of zero probability also require a consistent posterior convention.
The Lean model uses finite action and outcome types and a general measurable parameter type. This is a disclosed specialization of the tutorial, which also allows infinite actions and more general outcome spaces. The kernel is nonnegative, sums to one over outcomes, and is measurable in . The prior is a probability measure. The reward function is real valued and bounded because its domain is finite. The optimal-action selector has measurable fibers and maximizes the mean reward for every parameter. These conditions make the integrands measurable and bounded, avoiding default values of nonintegrable Lean integrals.
Histories are functions from a finite period index to action–outcome pairs. Policies are normalized, nonnegative behavioural action probabilities. The likelihood of a history multiplies both its policy action factors and its kernel outcome factors. The posterior uses only outcome likelihood factors, which give the Bayes update on every positive-evidence history. The Thompson-sampling predicate enforces the posterior action probabilities on those histories and permits any normalized policy on impossible ones. Lean period denotes the tutorial's period .
The shared tie-break is essential: Thompson sampling and use the same selected maximizer. The score has type , so it cannot inspect or the current outcome. No definition is allowed to supply regret or the decomposition as a predetermined constant; the expectation is built from the prior, policy and outcome kernel. The development needs reusable definitions for the Bayesian model, finite histories, behavioural policies, likelihoods, posterior masses, and the two regret terms. Contributions proving probability matching, equation (8.4), and the final identity are welcome.
Policy gradient methods for Markov decision processes are frequently run on a regularized objective rather than on the cost of interest: a convex penalty on the action distribution is added to every single-period cost. Regularization smooths the problem, makes optimal policies strictly stochastic, and keeps iterates away from the boundary of the probability simplex, where gradients of common parameterizations vanish. Entropy and relative-entropy penalties are standard in this role; a unified treatment of regularized MDPs is given by Geist, Scherrer and Pietquin (2019), and Agarwal, Kakade, Lee and Mahajan (2021) analyse policy gradient with a log-barrier penalty added to the softmax objective.
Regularization changes the problem being solved. Anyone who uses it needs a quantitative answer to one question: how suboptimal, for the original costs, is a policy that is exactly optimal for the regularized costs? Bhandari and Russo (arXiv:1906.01786v3), whose main results establish that policy gradient objectives have no suboptimal stationary points under a closure condition, answer this question for a relative-entropy regularizer in finite MDPs (their Lemma 10). Bounds of this type for the negative-entropy regularizer are in Geist et al.; as Bhandari and Russo note (p. 20), those bounds do not apply to the unbounded log-barrier regularizer used here.
The state space is finite. There are deterministic actions , and an action is a probability vector . A policy chooses at each state; is the set of all such policies. Transitions are linear in the action,
where each is a probability vector. Each state has a nonnegative cost vector . For , the regularized cost is
where is the uniform distribution. The divergence is unless every , so takes values in .
Given a discount factor and an initial distribution , the discounted average cost of a policy is
is the unregularized cost. The discounted occupancy of is . and denote the optimal cost-to-go and state-action cost-to-go of the unregularized problem. The constant of the result is
If with , then
The result. Lemma 10 says that the price of regularization is of order as , with an explicit constant depending only on the cost scale and the effective horizon . Together with the paper's landscape results (Example 4 shows the regularized policy-iteration objective is strongly convex and the policy class is closed under policy improvement, so the regularized objective is gradient dominated), it turns convergence of first-order methods on the regularized problem into near-optimality for the original problem, and it gives a principled rule for choosing as a function of the target accuracy. The bound holds for the log-barrier (relative entropy from the uniform distribution) regularizer, which is unbounded on the simplex, a case the negative-entropy analyses do not cover.
Formalizing it. The result and its proof are published (arXiv:1906.01786v3; Operations Research, 2024). No machine-checked proof of Lemma 10 or of its steps is known. The mission produces Lean statements of the lemma and of the four steps of its proof, built on a published finite-MDP layer, and invites proofs. Step 2 relies on the duality-gap bound for log-barrier problems from interior-point theory, which the paper cites from Boyd and Vandenberghe; a formal proof of that bound (in the simplex case) is reusable for any log-barrier analysis.
The first idea, comparing with an unregularized optimal policy , fails: is typically deterministic, so and , giving no information. The comparison policy has to be built by hand: it must be strictly stochastic, nearly optimal for the unregularized problem, and have bounded divergence from the uniform distribution at every state. Each of these three properties is a separate argument: a duality-gap bound for a barrier problem on the simplex, a propagation of a one-step Bellman inequality to the whole horizon, and a quantitative lower bound on the smallest action probability of the barrier minimizer.
A second pitfall is the printed form of the lemma, whose right-hand side is ; since gives , that inequality is trivially true. The proof establishes, and the text on p. 20 announces, the bound against , which is the goal here.
States and deterministic actions are finite types S and I (nonempty, as on the page, so that is defined); . Policies, transition kernels, the occupation distributions, the cost-to-go and come from the published FoundationsML.ReinforcementLearning layer (IsPolicy, IsTransitionKernel, OccupationDist, PolicyValue, QFunction), with the cost vector passed in the reward slot: PolicyValue is a plain discounted sum, so this is the cost-to-go. Optimality is the cost-minimizing notion, defined locally.
, and take values in , with off the open simplex; real-valued junk such as never stands in for , and is never coerced to (that would make boundary policies look optimal). At the convention gives , and Lean's makes the goal's bound , the limit of the page's bound. is written as " for every policy ". The minimizer is a hypothesis (any minimizer); the barrier-greedy policy of (36) appears only in the milestones, never in the goal. A statement of the goal with the printed right-hand side , or one that assumes (35) or the divergence bound, would be a trivializing formalization and is ruled out.
Welcome contributions: proofs of the four milestones and the goal; a general Lean lemma that the discounted cost of a stationary policy in a finite MDP equals the occupancy-weighted single-period cost (milestone 1), which is reusable across policy gradient formalizations; and the log-barrier duality-gap bound on the simplex.
Mean field games describe the limit of symmetric stochastic differential games with players as . A basic question of the theory is which mean field equilibria are limits of Nash equilibria of the -player games. For closed-loop equilibria, in which each player's control may depend on the states of all players, this question was open in general until D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745, Ann. Appl. Probab. 2020). That paper shows that limits of closed-loop -Nash equilibria are weak mean field equilibria, a class that can be strictly larger than the classical (strong) one.
Section 7.3 of the paper gives an explicit game in which the difference is visible. It has exactly three strong equilibria (Lacker, Probab. Theory Related Fields 165, 2016, Proposition 3.6, cited as [43] in the paper) and infinitely many weak ones. The weak equilibria form a family indexed by a switching time , and for they are not mixtures of strong equilibria (Remark 7.1). Proposition 7.2, the subject of this mission, treats : the natural symmetric feedback is an -player approximate Nash equilibrium, and its population mean selects the equal mixture of the two strong equilibria rather than the third one, . The selection mechanism is regularization by noise: the mean of the population solves an ill-posed ODE, and the small noise of the -player system picks out a particular random solution (Trevisan, Electron. Commun. Probab. 18, 2013, cited as [57] in the paper).
Fix a horizon . In the mean-sign game each of players controls a real state
with controls and independent standard Brownian motions . The mean process is , the mean of the empirical measure . Player maximizes the expected terminal reward
that is, , , with , and initial law .
A Markovian control of player is a Borel function of time and the current states of all players. A profile is a Markovian -Nash equilibrium if no player can raise their payoff by more than by switching to another Markovian control while the others keep theirs (Definition 2.1).
With for , , , the sign feedback (7.13) with is
the same for every player. Finally on (7.11).
For the profile :
The goal also asserts that the -player system under has a solution, so that the equilibrium property cannot hold vacuously.
Proposition 7.2 is a concrete instance of the paper's main theme. Theorem 2.7 says that limits of closed-loop equilibria are weak equilibria; this example exhibits explicit, symmetric, Markovian approximate equilibria whose limit is a genuinely random equilibrium (the sign of the mean is a fair coin), selected by noise among infinitely many candidates, and it identifies the limiting law of the population mean exactly. The paper states that the analogous claim for , where the limit would be a weak equilibrium that is not a mixture of strong ones, is not resolved; a formal treatment of the case makes the structure of that question precise.
Nothing of this proposition is machine-checked. Formalizing it requires weak solutions of SDEs with discontinuous drift, Nash equilibria over Markovian feedback controls, and weak convergence of laws on path space, all stated so that the junk values of Lean's total functions never enter. The objects defined here (the -player game with quantified weak solutions, its payoffs and Markovian -Nash equilibria) are shared with the other missions of this series.
The obvious argument for compares player 1's payoff under a deviation with . A deviation changes the drift of the mean only by , but the dynamics of the mean, , is ill-posed in the limit: the ODE , , has infinitely many solutions . Continuity of the solution map, the usual tool, is unavailable, and one must instead identify the limit law, which comes from the vanishing noise, and show that it is unchanged by the deviation. The second difficulty is that the payoff is unbounded, so convergence of laws does not give convergence of payoffs without a uniform integrability estimate. The proof in the paper is short, but relies on a cited result on the vanishing-noise limit and on a compactness argument in a weak topology for the deviating controls.
EuclideanSpace ℝ (Fin 1) (the platform's EthierKurtz.SDEState 1) and its coordinate is y 0. Controls are real, .Real.sign (), and the control vanishes at , both as printed.Contributions welcome: the existence of weak solutions for bounded measurable Markovian drifts, the vanishing-noise limit of , and Girsanov-type change-of-measure estimates are all reusable beyond this mission.
A directed polymer in random environment is a random walk path reweighted by a random potential that is refreshed at every time step. It is a basic model of a one-dimensional object (a polymer, an interface, a flux line) pinned by impurities, and a discrete version of the KPZ universality class in dimension . A central question is localization: whether the walk's endpoint at time , under the random Gibbs measure, concentrates on a few sites or spreads out like a simple random walk.
For a fixed disorder law there is a critical inverse temperature (Comets–Yoshida, Ann. Probab. 2006). In the low-temperature phase the endpoint has atoms of positive mass, in the Cesàro sense, at a positive fraction of times (Carmona–Hu 2002, Comets–Shiga–Yoshida 2003); in the high-temperature phase it does not. Atoms alone say nothing about geometry: the mass could sit on a few sites that are far apart. Bates and Chatterjee (arXiv:1612.03443v5, Ann. Probab. 2020) prove that in the low-temperature phase the mass also sits on a region of bounded diameter at a positive fraction of times, in every dimension and for every disorder law with exponential moments. Before this, geometric localization was known only for the integrable log-gamma polymer in dimensions (Comets–Nguyen 2016).
Fix . Let be i.i.d. real random variables with law , not supported on a single point, such that for (assumption (1.1)), where is the inverse temperature. For a nearest-neighbour path of length from the origin, its weight is . The endpoint distribution is the total weight of paths ending at divided by the total weight of all paths. The partition function is and the free energy is . The limit exists, and is characterised by for and for .
For and let be the set of probability mass functions on that give mass greater than to some set with .
The proofs work on the space of partitioned subprobability measures: functions on with , modulo translations of each copy of , with a metric that makes compact. The update induces a Markov kernel on ; is its set of invariant probability measures and the minimisers of a free-energy functional . On the mission uses the functionals , the support number (number of copies carrying mass), (the least diameter of a region of one copy with mass ), and , where is the mass of copy .
If , then for every there are and , depending only on , such that
If , then for every and every ,
The goal fixes no constants: and are only asserted to exist.
The theorem shows that the low-temperature phase is detected by the shape of the endpoint distribution, not only by its largest atom: positive-density geometric localization holds if and only if . The determinism of and makes the statement uniform over all environments with the given law. The conditional results 5 and 6 reduce full-density and favourite-region localization to a single property of the limit set , which is open.
The result is proved on paper; nothing in it is machine-checked. A formalization would produce a checked development of the compact space , of the Markov kernel , and of the variational characterisation of the free energy, which also underlies the companion mission on asymptotic pure atomicity of the same paper.
The obvious approach, tracking in , fails because mass escapes to infinity: the sequence has no convergent subsequence in any space of probability measures on . The paper's compactification keeps pieces of mass that drift apart as separate copies, so a limit point can split one copy's mass over several. The semicontinuity of , and (Lemma 7.1) only goes one way for this reason, and positivity of the localized fraction needs the separate identity of Lemma 7.2, which uses strict convexity and the non-degeneracy of . Theorem 5.3 already requires the full variational machinery of §4 (convergence of empirical measures to ), which is the companion mission's subject.
Points are Fin d → ℤ, cells are ℕ × (Fin d → ℤ), and paths are sequences of signed coordinate steps. The environment is a family of independent measurable random variables, each with law , on an arbitrary probability space. The phases are encoded through Theorem A as () and (), with computed under the canonical product environment. Elements of are represented by their representatives, with the topology generated by -balls (no quotient). In the goal, and are chosen before the probability space. Part (a) is stated for all and part (c) for , as printed.
Trivializing encodings are ruled out: requires total mass exactly ; and take values in so that an empty infimum is ; is computed in so that ; the sum in is taken in ; avoids a real infimum over ; is non-degenerate; and the phase hypotheses are limits that exist.
A complete development needs: the metric space and its compactness, the measurability and continuity of , the Wasserstein space (here through the published RWPI.SqrtLasso.transportCost), and the convergence (Theorem 4.9) together with at high temperature (Theorem 5.2), both posed in the companion mission. Contributions to any milestone, and to the shared infrastructure of , are welcome.
How should a set of indivisible items (courses, shifts, inherited objects) be divided among people who have different entitlements but no money to transfer? A classical answer for divisible goods is the competitive equilibrium from equal incomes (CEEI): give every agent a budget of artificial currency, find prices at which every agent can afford her favourite bundle and the market clears. The resulting allocation is Pareto optimal and fair. With indivisible items a CEEI can fail to exist already for one item and two agents with equal budgets: at any price, either both agents can afford the item or neither can.
Babaioff, Nisan and Talgam-Cohen (arXiv:1703.08150; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) study this Fisher market with indivisible goods when budgets are generic: unequal budgets, with a measure-zero set of exceptional budget pairs excluded. Their main result is for two agents with almost equal budgets. This mission formalizes the companion result for two agents with identical additive preferences and arbitrary unequal budgets (Theorem 8.1 of the paper, its informal Theorem 1.4). With identical preferences the division problem is a discrete claims (bankruptcy) problem: one cake of fixed value is split between claimants with different entitlements .
Timeline of the relevant results:
There are indivisible items and two agents. Agent has a valuation that is additive, normalized (), non-negative, monotone and strict (different bundles have different values), and a budget , with . An allocation gives every item to exactly one agent. Item prices price a bundle at .
A bundle is demanded by agent at prices if and for every bundle with . A competitive equilibrium (CE) is a pair in which each is demanded by agent . An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent. It is budget-proportional if for both agents, and anti-proportional if for both, strictly for one.
The truncated share of agent is
the best she can get in a PO allocation that gives her at most her budget share; an allocation gives her the truncated share if . The exceptional set (Definition 6.2) consists of the budget pairs for which two PO allocations , consecutive in agent 's order of preference, satisfy . It is finite. The rectangle (Definition 6.1) is a set of allocations between the truncated-share maximizers of the two agents.
In Lean all objects live in GenericBudgets.IdenticalPrefs: bundle, price, IsDemanded, IsCE, IsPO, IsStandardValuation, IsBudgetProportional, IsAntiProportional, GetsTruncatedShare, IsTruncMaximizer, InRectT, InR.
If , , and for some agent , then
Theorem 8.1 shows that the non-existence of CEEI for identical preferences is a knife-edge phenomenon: for every market with identical strict additive preferences, every unequal budget pair outside a finite set admits a CE, and the CE allocation is as close to budget-proportional as indivisibility allows. It gives a market-based solution to the indivisible claims problem with unequal entitlements, and its CE inherits Pareto optimality from the first welfare theorem (Theorem 2.4 of the paper).
The formalization targets three things on top of the paper. First, a machine-checked proof of the paper's main technical tool, Lemma 6.3, which also drives the paper's main Theorem 7.1 (mission 1 of this series), where it is applied to almost equal budgets instead of identical preferences. Second, precise definitions of the truncated share, the rectangle and the exceptional set , whose informal versions leave conventions implicit (the maximization runs over PO allocations only; is indexed by consecutive PO allocations). Third, verification of the proof chain Proposition 5.1 → Lemma 6.3 → Lemma 8.2 → Theorem 8.1. The statements compile, but none of these results has a machine-checked proof yet.
The reduction of Theorem 8.1 to Lemma 8.2 and the proof of Lemma 8.2 from Proposition 5.1 and Lemma 6.3 are short. The substance is in Lemma 6.3, which must exhibit prices supporting a PO allocation when no allocation gives both agents their budget shares. Demand is a condition over all bundles, so a candidate price vector has to be checked against every bundle each agent prefers, and the paper's construction breaks down on the exceptional budget pairs , which is why they are excluded; the argument is a case analysis over the finite Pareto frontier. The easy case, Proposition 5.1, covers only markets with a budget-proportional or anti-proportional PO allocation; with identical preferences and unequal budgets neither typically exists (no allocation is ever anti-proportional), so Lemma 6.3 cannot be avoided.
Items are Fin m; agents are Fin 2, with indices for the paper's agents , so is b 1 < b 0. Valuations are functions Finset (Fin m) → ℝ bundled with the standing assumptions in IsStandardValuation; identical preferences are the hypothesis v 0 = v 1. An allocation is a map Fin m → Fin 2, so every item is allocated exactly once. Budgets are positive reals summing to . All quantities are real.
Committed conventions and disclosed restrictions:
max: for every PO with .Trivializing formalizations are ruled out: the demand condition quantifies over every bundle with strict inequality, allocations must assign every item, prices are non-negative, the truncated share is maximized over PO allocations only (not over all allocations), and the budget hypothesis excludes only the finite set for one agent, never all unequal budgets.
Proposition 5.1 and Lemma 6.3 are posed with the same statement as in mission 1 of this series; a proof of either transfers verbatim. Contributions welcome: the finite-frontier infrastructure (existence and uniqueness of the truncated-share maximizer), Proposition 5.1 through budget-exhausting combination pricing, and Lemma 6.3.
A failed buyer can leave a supplier with goods it can no longer sell through an existing order. A failed supplier can leave a buyer without inputs for future production. In a network, either loss can weaken another firm and start a sequence of defaults. Birge, Capponi and Chen model these effects together with two responses: suppliers reroute unsold goods to other buyers, and buyers seek replacement suppliers. Their accepted manuscript asks whether the resulting market decisions and the default cascade determine a single outcome. The issue matters when a network's resilience or fragility is measured from that outcome: a measure based on an unspecified equilibrium would not be well defined.
A supply chain order network has finitely many firms and goods . An order is the nonnegative quantity of good that firm promises to deliver to firm . The network also records each good's original price , each firm's initial equity , its safety stock and holding cost , and a realized net production cost . The realization is fixed throughout this mission; the source treats it as random when comparing network performance later in the paper. Rerouting one unit costs firm an amount ; an unfilled unit of demand incurs back-order cost . These costs and the orders and stocks are nonnegative. The basic model is on pp. 8–17 of the manuscript.
If firm defaults, a promised delivery to it is not made. Write for this undelivered order, and for firm 's total amount of good available to reroute. If a supplier defaults, write for the buyer 's lost input. After using safety stock, that buyer's unserved demand is , where . These are the quantities in equations (1)–(5).
The rerouted market for good contains firms with . At price , firm can sell up to . Aggregate demand at price is , with inverse demand . The sourcing market contains firms with . At switching cost , firm can replace up to units. Aggregate supply is , with inverse supply . In either market, an efficient allocation maximizes the stated integral objective over the capacity box, and allocates proportionally to capacity among firms quoting the same price or cost. A partial equilibrium additionally makes every active firm's quoted price or cost a best response to all nonnegative unilateral deviations. These are Definitions 2.1–2.2 and 3.1–3.2.
A firm's ex-post net worth combines original-order revenue, production and stock costs, rerouting revenue and cost, and back-order and replacement-supplier costs exactly as in equation (10). A firm defaults when its net worth is strictly negative. Starting with no undelivered orders or unserved demand, the update maps and mark all orders affected by firms that default after each market has reached its partial equilibrium. A market stable state is both the limit of that sequence and a fixed point of the update. A general equilibrium combines such a state with a partial equilibrium in every market (Definitions 3.3–3.4 and equation (18)).
The goal is Proposition 4.3, stated on p. 24:
The quadruple consists of rerouting prices , switching costs , undelivered orders , and unserved demand . The claim includes existence and uniqueness of the full outcome, not merely of its default set. The milestone list follows the paper's dependency path: Propositions A.3 and A.6 identify the unique efficient allocations in the two markets; Propositions 4.1 and 4.2 identify their partial equilibria; Lemma A.7 states that greater disruption cannot increase any firm's partial-equilibrium net worth; and Lemma A.8 states that the default updates are bounded and increasing. The numbered results and their equations are in the E-Companion, EC pp. 4–12, and the main text, p. 22.
Proposition 4.3 makes the network's outcome a function of its order commitments, stocks, prices, market functions, and realized production costs. Later comparisons of network structures can therefore refer to the equilibrium without choosing among several price or default profiles. The result also separates local market choice from the way losses spread through the network: a firm can reroute or switch optimally and still fail once the effects of other failures are accounted for.
The paper proves the result in its E-Companion, EC pp. 12–13. This mission concerns a Lean statement of that known result and the reusable definitions needed to check a proof. The draft propositions are open proof obligations; this proposal does not claim machine-checked proofs of them. The two market allocation predicates, the default update, and the cascade limit can also support later formal work on the paper's resilience results.
The market and network conditions interact. An arbitrary fixed point of the default update need not be the state reached from zero; using only the fixed-point equation loses the uniqueness asserted by the paper. Conversely, knowing a cascade limit does not by itself show that the limit is fixed, because the update changes discontinuously when a firm's net worth crosses zero. At the market level, the price and switching-cost equilibria must be established from optimization and best-response conditions. Writing the formulas for the claimed equilibrium prices into those definitions would leave the central market claims unproved.
Firms are Fin N and goods are Fin M, with ; the source numbers both from one, while Lean numbers them from zero. Orders and all default matrices are real valued and coordinatewise ordered. Active markets may be empty, as at the start of the cascade. Market objectives are ordinary real interval integrals over finite capacity boxes. The standing conditions include the paper's smoothness, concavity, and monotonicity assumptions on demand wherever it is positive and on the supply function, plus inverse identities and continuity on the quantity ranges used by the model. The inverse functions remain general data tied to and ; no linear demand or supply curve is imposed.
Several domain conventions make the displayed formulas meaningful. Assumption 2.1's minimum order is read over positive-order suppliers of a good; over all firms it would force zero safety stock whenever a nonsupplier exists. The inverse supply is nonnegative on feasible quantities, with , so the claimed switching cost belongs to the nonnegative strategy space. Demand inverse at zero is fixed to the reservation price. Assumptions 4.1–4.2 apply at each positive active-market total; for the general-equilibrium goal they are required for every binary profile the cascade can visit. Differentiability at those totals is explicit. Initial equity and the order, stock, holding, rerouting, and back-order data are nonnegative; the realized net production cost can have either sign. The model uses the p. 23 convention for prices and costs outside active markets.
An efficient allocation remains an optimizer of equations (7) or (9), with proportional tie handling; a partial equilibrium remains a best response to every admissible deviation. The general equilibrium includes both the limit from zero and the fixed-point condition. These clauses exclude an equilibrium that is true by definition or a fixed point unrelated to the default cascade. The source's informal statement that every firm “supplies, consumes, or purchases” a good has no separate activity flag in this model; a firm with no internal order can still have outside production or consumption represented in . Milestone statements involving arbitrary disruption profiles restrict them to the feasible order box , where the market inverses are defined.
Approximate message passing (AMP) is a family of iterative algorithms driven by a large random matrix. It was introduced for compressed sensing by Donoho, Maleki and Montanari (PNAS 2009), and it is also used for low-rank matrix estimation, regression and spin-glass optimization. Its main appeal is that, for Gaussian random matrices, the empirical distribution of its iterates is tracked exactly in the large-dimensional limit by a scalar or low-dimensional recursion called state evolution. Bolthausen (CMP 2014) and Bayati and Montanari (IEEE Trans. Inf. Theory 2011) proved this for Gaussian matrices. Those proofs condition on the matrix through linear observations, and that conditioning argument works only for Gaussian entries.
In practice, and in the compressed-sensing phase transition that motivates the paper, the matrices are not Gaussian: Bernoulli, Rademacher and other sub-Gaussian ensembles are used. Bayati, Lelarge and Montanari (arXiv:1207.7321, Ann. Appl. Probab. 25(2), 2015) prove that the asymptotic behaviour of AMP with polynomial nonlinearities is universal: it depends on the law of the matrix entries only through their variances. This mission formalizes that universality theorem, Theorem 3 of the paper, together with the main steps of its proof.
Fix a dimension and a degree bound . For each , an AMP instance consists of three objects:
The AMP orbit is
where is the Jacobian. The second term, the memory or Onsager term, is absent at . A sequence of random instances indexed by is -regular if it satisfies the following conditions:
The proof also uses an auxiliary message-passing iteration. It consists of messages with and
Monomials are written for .
Let and be two -regular sequences. They share the polynomials and the initial condition, and for all . Then for every and every family of polynomials of degree at most with coefficients bounded by ,
In each milestone depends only on , as Note 2 of the paper specifies.
Theorem 3 lets results proved for Gaussian matrices be transferred to every sub-Gaussian ensemble with the same variance profile. In the paper, it is the first link of a chain:
The universality of the weak-neighborliness threshold for non-Gaussian matrices, observed numerically by Donoho and Tanner (Phil. Trans. R. Soc. A 2009), is a consequence of this chain.
The result has been proved since 2012. No machine-checked proof of it, or of any AMP state-evolution statement, is known to exist. The mission asks for a formalization of the published proof, or of any other argument. Two pieces of the proof are useful elsewhere: the absolute-moment bound for sub-Gaussian variables and the moment comparison of the message-passing iteration.
The first idea is a Lindeberg-type swap: replace the entries of by those of one at a time and bound each change. This does not work directly. Every iterate depends on all entries through nested polynomial layers. The memory term also couples consecutive iterates through the squares . A single swap therefore changes every coordinate of every later iterate, and the per-swap errors have to be summed over swaps with a total error of .
Two features of the statement make it delicate. Only second moments of the entries are matched, so every contribution of higher moments of the entries must be shown to vanish in the limit. In addition, the AMP orbit is not itself a message-passing iteration: its moments match those of (Proposition 3) only because of the memory term, and without that term they do not. A formal proof also has to establish finiteness of all the moments involved, which the paper takes for granted.
Vectors in are Fin q → ℝ, and indices are 0-based. A polynomial is given by its coefficient vector over the exponent vectors of total degree at most , as in (4.10) of the paper. This keeps random polynomials in a measurable space. The Jacobian is the explicit sum of formal partial derivatives. A sorry-free sanity file checks it against the analytic derivative on an example and checks the memory term on a small instance.
The orbit is computed by recursion on , with no memory term at . The memory term uses itself, not its expectation . All random objects live on one probability space. The two sequences of Theorem 3 share one coefficient process and one initial condition.
Three readings of the printed Definition 4 are disclosed:
HasSubgaussianMGF), not only for ;Every expectation appearing in a target is also asserted to be finite. Without that, a bound or a limit could hold only because Lean assigns the value to the integral of a non-integrable function. Squared Euclidean norms are written as sums of squares, never as the sup norm that Mathlib puts on Fin q → ℝ. The deterministic identities of the tree expansion (Lemma 1, Lemma 3) and the first claim of Lemma 2 are not posed, because they need the labelled-tree families of Definition 6. Contributions of that tree machinery are welcome. Moment bounds for sub-Gaussian variables and polynomial moment estimates for sums of independent variables are reusable well beyond this mission.
A firm can lose a planned input when one of its suppliers defaults. Safety stock can absorb some of that loss, while the rest becomes demand for replacement supply. A network with more buyer and supplier links spreads orders across more firms, but the resulting benefit depends on which firms default, how much each link carries, and the price of replacement supply. Birge, Capponi, and Chen study this interaction in a supply chain model with firm defaults, switched demand, and market prices. Their Theorem 5.1 asserts that a particular order-preserving form of diversification improves the network's resilience. This mission formalizes that comparison in the notation and conventions of the accepted manuscript, including its E-Companion proof.
The question is relevant to supply chain design because adding a link alone does not specify how much business moves to it. The theorem compares two networks that retain each firm's total incoming and outgoing order quantities. It therefore isolates the effect of redistributing those orders among more partners. The result concerns a precise resilience metric: the fraction of a network's baseline out-of-stock cost reduced by holding safety stock. It does not claim that diversification prevents all defaults or reduces every component of systemic loss.
There are firms and goods. The order quantity is the amount of good that firm promises to deliver to firm . Good has price . Firm has initial equity and a unit holding cost for safety stock of good . Its realized net production cost is . Two networks and share prices, equity, holding costs, firms, and goods; their order quantities may differ. The source calls this five-part data a supply chain network, with a stock profile that is specialized here to a common scalar for the resilience comparison (§2, pp. 8–9; §5.1, p. 25).
A tiered network places each firm in a tier . A positive order of good runs from tier to tier . Tier 1 firms supply good 1, tier firms buy good , and every intermediate firm both buys and supplies its designated goods. The undirected graph underlying positive orders is connected. The model's supplier set contains firms delivering good to , and its buyer set contains firms receiving good from (§5.2–5.3, pp. 26–27).
For a common realization and safety stock , the fundamental-default set contains firms whose initial net worth is strictly negative:
The switched demand of firm for good is . The inverse supply function prices the aggregate replacement demand for good . Firm 's cost sums holding cost and switched-demand cost over every good. The network's resilience ratio is its aggregate reduction in this cost divided by aggregate cost at zero safety stock (§5.1, p. 25).
For each firm, is more diversified than when total incoming and outgoing orders are unchanged, and , and an expanded neighbor set divides orders into quantities no larger than the old quantities. Where a neighbor set is unchanged, its individual order quantities are unchanged. This is the complete condition of Definition 5.3, with the supplier good indexed as as required by §5.2.
The goal is Theorem 5.1: for two tiered networks sharing their non-order data and tier assignment,
for every admissible common safety stock and common realized production-cost vector . The three milestones are the tier-grouped expression for total cost, its order comparison between and , and equality of their zero-stock baseline costs. They are the steps of the displayed chain in the E-Companion, EC p. 18, rather than separate numbered lemmas.
The theorem gives an order-sensitive comparison of the paper's out-of-stock metric. It says that, under the stated redistribution constraints, the same amount of uniform safety stock offsets at least as large a fraction of baseline cost in the more diversified network. It supports comparisons of network designs with equal firm-level order totals. It does not rank networks with different equity, prices, or holding costs, and it does not address the paper's distinct contagion-based fragility metric (§5.1–5.3).
The result is proved in the paper; the open work here is its machine-checked formalization. The definitions of tiered order networks, fundamental defaults, switched demand, and the resilience ratio give reusable interfaces for later results about the same model. The draft Lean theorems state the full result and the three intermediate targets, with proofs left for solvers. The comparison also makes the paper's indexing and cost conventions explicit so those interfaces can be audited independently.
The default set depends on the order network, even though the two networks use the same realized costs. Thus a cost comparison cannot begin by treating defaulted firms as an unrelated common parameter. Moreover, switched demand takes a positive part after subtracting safety stock, and the inverse supply curve is evaluated at an aggregate across firms. Merely comparing individual orders or counting more links does not determine the resulting total cost. The final resilience ratio has a baseline-cost denominator that can be zero. The formalization has to cover that boundary case as well as positive baseline cost.
Firms use Fin N; goods and tiers use the paper's one-based natural-number indices. Both and are positive. Orders and holding costs are nonnegative, prices are nonnegative, and initial equity is nonnegative (the source assumes every firm is initially solvent, p. 9). A tiered network has only consecutive-tier positive orders, has activity appropriate to every firm's tier, and has a connected underlying undirected graph. The two networks share , , , the inverse supply curves, and the tier map. The source's tier-constant rerouting cost does not occur in the resilience metric and is not represented in these statements.
The paper prints Assumption 2.1 as a minimum over all firms. Since non-suppliers have zero orders, that literal reading would force and empty the theorem of its intended positive-stock content. The formalization reads the bound over actual suppliers, with . It uses monotone inverse supply curves, as implied by Assumption 2.3, and explicitly requires their values to be nonnegative for nonnegative demand; the latter is an additional convention corresponding to nonnegative inverse supply prices. These choices appear in the definitions and in the statement audit notes.
The printed supplier-order superscript in Definition 5.3 uses , while §5.2 says firm buys good ; the Lean definition uses the latter. The E-Companion's cost chain drops holding costs for goods a firm does not buy, although §5.1 sums them for all goods. The formalized cost and tier-grouped milestone retain the full sum. The paper states an almost-sure comparison under a random cost vector; its proof is pointwise, and the goal quantifies over every common realization. Each network computes its own default set. Lean sets , so a zero baseline cost requires no extra positive-denominator assumption. These conventions rule out a vacuous zero-stock reading or a cost formula weakened by omitting terms.
Heat flow gives an analytic way to describe how functions spread on a space. Optimal transport gives a metric way to describe how probability measures move on the same space. On a smooth Riemannian manifold, a lower Ricci curvature bound constrains both motions. The problem addressed by Ambrosio, Gigli and Savaré is to identify the corresponding relationship when the underlying space need not be a manifold. A Dirichlet form can specify a heat flow even when there are no smooth coordinates, while a Wasserstein distance can measure transport between probability measures. Theorem 4.17 connects these two descriptions for Riemannian energy measure spaces.
The paper proves the implication from the Bakry–Émery condition to the Riemannian curvature-dimension condition . Its printed theorem is an equivalence; the paper cites the reverse implication from earlier work in the proof on p. 58. This mission targets the implication established here, with the source's exact assumptions.
Let be a complete, separable metric space with a Borel measure . A Dirichlet form assigns a nonnegative energy to square-integrable functions, is quadratic and lower semicontinuous, and decreases under normal contractions. Its associated heat flow evolves a function over time. The associated carré du champ measures the energy density of a function. Functions with energy density at most one define an intrinsic distance
For the Riemannian energy measure space in this mission, this intrinsic distance is the metric of . The structure also requires the paper's upper regularity and continuous-representative properties. The growth condition controls the measure of large balls. In the condition, a weak second-derivative inequality for the heat flow has curvature parameter and no finite-dimensional correction term. These assumptions are stated at the start of §4 and govern the §4 milestones even when an individual theorem does not repeat them. See Definitions 3.6 and 3.16 and the opening of §4.
Write for the probability measures with finite second moment, for their quadratic Wasserstein distance, and for entropy relative to . The heat flow has a dual action on measures. The target asks for a curve from every that satisfies the following evolution variational inequality against every of finite entropy, at every :
The definition also includes full support, local finiteness, the exponential growth condition, and the length-space property. See Definition 3.1.
The goal is the forward implication of Theorem 4.17:
Three milestones supply central results from the paper. The final assertions of Theorem 3.17 give the dual measure flow and its absolute continuity after positive time. Corollary 3.18 identifies with the contraction on probability densities. A companion item, Theorem 4.8, gives an entropy bound for when has finite second moment:
The third milestone, Theorem 4.16, bounds the distance and entropy at the heat-evolved endpoint of a regular curve :
The milestone list follows the source labels and constants in §4.
The conclusion turns an analytic curvature bound on a heat semigroup into a transport statement about entropy on probability measures. It therefore identifies a concrete set of Dirichlet-form hypotheses under which the heat evolution has the metric behavior demanded by . The result applies in the paper's metric measure setting, where the space may lack a smooth tensor calculus. The conclusion carries convergence from every initial measure in and the inequality for all finite-entropy comparison measures.
The mathematical implication is proved in the cited paper. The proposed Lean statements are open proof targets: their declarations compile with placeholders, and no machine-checked proof of this implication is asserted here. A complete development would connect Dirichlet-form calculus, probability measures, entropy, and Wasserstein geometry in reusable interfaces. The dual-flow and regular-curve definitions are especially useful beyond this theorem.
The heat flow is initially specified on square-integrable functions, whereas the target is an inequality for probability measures, including measures without an initial density. A bound on by itself controls functions almost everywhere; it does not immediately produce the pointwise dual flow or the right derivative of required by Definition 3.1. The action estimate also begins with regular curves, while the target quantifies over every initial measure in . These changes of domain and regularity are the central mathematical obstacles; simply renaming the heat semigroup as a measure flow leaves the target unjustified.
Lean uses real-valued function representatives for , with almost-everywhere congruence in the Dirichlet form and heat flow. Measures use the Borel sigma algebra. The source uses its -completion; the formalization treats quantities invariant under -almost-everywhere equality, and this convention is explicit in the definition layer. The metric is complete and second countable, and its equality with is part of the energy-measure-space predicate. A sigma-finiteness instance is carried where entropy or measure operations need it; it follows from the source's measure-growth setting. The dual flow and the extension are bound by predicates that specify their action on densities. The mollifier for a regular curve is bound by the conditions of (2.17), while the action is the infimum of squared admissible speeds, which equals the integral of the squared metric derivative.
Wasserstein costs use , and entropy uses extended real values. Theorem 4.8 restricts to positive numbers, so the ball mass and used in its formula have the intended domain. Theorem 4.16 also uses , making meaningful, including at . The goal requires an EVI flow beginning at each and the inequality at every positive time; allowing a vacuous flow or checking only almost every time would not express Definition 3.1. Contributions may establish the milestone statements and the companion Theorem 4.8, develop the omitted intermediate estimates from §4, or prove the goal from the source's full argument.
Competitive equilibrium is a way to divide goods when each participant has a budget reflecting her entitlement. With divisible goods, proportional value is a natural fairness target. Indivisible goods make that target unavailable in some markets: a single item cannot give two agents positive fractions of its value. The question becomes what fairness a market outcome can guarantee without dividing an item or assuming that agents value items additively. Babaioff, Nisan and Talgam-Cohen, §2.3 and §3 place this question in a discrete Fisher market, where budgets determine purchasing power but leftover money has no value to agents.
The paper introduces an -out-of- maximin share to express the entitlement of an agent whose budget is at least . Its Proposition 3.2 says that every competitive equilibrium provides this share. The result applies to any number of agents and to arbitrary cardinal preferences; it does not require the additive assumptions used for the paper's equilibrium existence results. The same paper compares the conclusion with the earlier one-out-of- guarantee for nearly equal budgets and explains that other rational shares can give a stronger benchmark in a given market. Babaioff, Nisan and Talgam-Cohen, §3.3
Let be a finite set of indivisible items and a finite set of agents. Agent has a valuation for each bundle and a positive budget . The budgets are normalized by . An allocation partitions all items: each item belongs to exactly one agent's bundle. A price vector gives each item a nonnegative real price , and the price of a bundle is . Babaioff, Nisan and Talgam-Cohen, §2.1–2.2
An allocated bundle is demanded when it costs at most and every bundle that strictly prefers costs more than . A competitive equilibrium (CE) is an allocation and price vector for which each agent demands her allocated bundle. Demand compares with every subset of , including bundles assigned to other agents and unions of several such bundles. Money is an allocation device in this model; an agent's valuation concerns her bundle alone. Babaioff, Nisan and Talgam-Cohen, Definition 2.1
For and , consider every partition of into labeled parts. Empty parts are permitted. For each partition, an adversary can leave the agent any parts, so the smallest value of a union of exactly parts is her guarantee for that partition. The agent chooses the partition that maximizes this worst-case value. This is her -out-of- maximin share. The allocation guarantees the share when is at least the resulting maximin value. Babaioff, Nisan and Talgam-Cohen, Theorem 1.2 and Definition 3.1
For every agent , every competitive equilibrium, and every pair of natural numbers with and , the goal is Proposition 3.2:
The three milestones record the paper's intermediate claims in order: the total price of all items is at most the total budget; among parts, some have price at most of the total; and a bundle an agent can afford is no better for her than the bundle she demands. The goal quantifies over every eligible rational share rather than selecting a single fixed denominator. Babaioff, Nisan and Talgam-Cohen, proof of Proposition 3.2
Two companions record the first welfare theorem, which makes a CE allocation Pareto optimal under strict preferences, and the appendix's coalition form of justified envy. The latter excludes the single case in which the comparing agent's bundle and the coalition's union are both empty, because the printed strict comparison is false there. These companions provide context for the equilibrium notion; neither changes the valuation generality of Proposition 3.2. Babaioff, Nisan and Talgam-Cohen, Theorem 2.4 and Claim A.8
The proposition gives a fairness conclusion conditional on equilibrium existence. It covers agents with different entitlements and nonadditive valuations, using a share that the agent herself evaluates through a partition of the items. The result does not assert that an equilibrium exists for every market. It says that any equilibrium already present meets all the stated rational-share benchmarks simultaneously. The paper uses this to relate competitive outcomes to maximin guarantees previously studied for nearly equal budgets. Babaioff, Nisan and Talgam-Cohen, §3
A machine-checked development would add a reusable account of finite allocations, bundle prices, demand, and maximin shares, plus a certified bridge between equilibrium and fairness. The draft Lean items in this mission are open statements with sorry; the local build checks their types and imports, not their mathematical proofs. The equivalence of the chosen maximin encoding with the finite max–min formula is checked separately in a sorry-free sanity file. Formal proofs of the goal and its milestones remain solver work.
The main formal issue is to keep the quantifiers and boundary cases aligned with the fairness definition. The guarantee concerns every partition into parts, including empty parts, and the worst choice among subsets of exactly parts. A benchmark formed from one convenient partition, from at most parts, or from a restricted family of affordable bundles would have a different meaning. The total price comparison also depends on every item being allocated exactly once. The appendix companion has a separate edge case: strict envy cannot follow from demand when the two compared bundles coincide as the empty set.
Items are Fin m, agents are Fin n, and valuations are real-valued functions on finite item sets. An allocation is a function from items to agents, so feasibility and market clearing are part of its type. A partition into parts is a function from items to Fin d; it allows empty parts. Prices and budgets are real. The goal assumes positive budgets with sum one, nonnegative prices through the CE predicate, and . The case is allowed; the budget condition implies . The Lean maximin guarantee is written as a quantified comparison rather than using a real supremum or infimum, avoiding default values on empty extrema. A sanity theorem relates it to the finite max–min expression under its proper domain conditions.
The paper's normalization and arbitrary-preference scope are retained in the goal. Strict preferences are used only for the first-welfare and appendix companions. There, injective valuations exclude the paper's exception for identical items, and the appendix claim additionally excludes the case in which the comparing agent's bundle and the coalition's union are both empty. The mission's setting is repeated locally because no published platform definition has the same bundle market and budget conventions; the related housing, divisible-goods, and convex-economy models use different objects.
Contributions should preserve full market clearing, demand over every item bundle, nonnegative prices, all -part partitions, and exactly selected parts. The definitions and finite averaging milestone can be reused in other fair-division developments. Proving the three source milestones and the goal, or improving the formal treatment of the appendix edge case, are within scope.
Mean field games (Lasry–Lions 2006, Huang–Malhamé–Caines 2006) describe Nash equilibria of stochastic differential games with very many symmetric players. In this description each player interacts with the others only through the empirical distribution of their states. The mean field game is meant to be the limit of the -player games as . Making that link rigorous has two halves:
For closed-loop equilibria, where players react to the observed states of all others, both halves are harder than for open-loop equilibria. A single player's deviation changes the feedback of the whole system.
This mission covers the converse half of D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020).
Timeline.
Fix a horizon , a compact convex action set in a real normed space, an initial law and coefficients
The -player game.
with independent Brownian motions and i.i.d. initial states of law .
The mean field game. A flow is a strong MFE if some Borel feedback satisfies two conditions:
A strong RMFE is the relaxed analogue.
The assumptions are:
Under Assumptions A, B and C, if is a strong MFE, there are two families of objects:
such that
The goal asserts no rate, so any quantitative improvement still implies it.
The result. Theorem 2.11 says that the strong MFE is a faithful idealization: every classical mean field equilibrium is approximately realized by Markovian feedback equilibria of large finite games. No continuity of the equilibrium feedback and no master equation are required. Together with the paper's main limit theorem (mission 1 of this series), it locates strong MFE inside the set of limits of closed-loop equilibria. The paper's Section 2.4 explains why the same converse is open for weak MFE.
Formalizing it. The result is proved on paper but has no machine-checked proof. A complete development would produce several reusable pieces:
None of these is in Mathlib.
The obvious argument has every player use , invokes the McKean–Vlasov limit, and passes optimality to the limit. It fails at two places:
Representation.
EuclideanSpace ℝ (Fin d).ProbabilityMeasure with the weak topology and the Borel -field.Set.Icc 0 T with the compact-open (uniform) topology.Committed choices.
Ruled out. Because equilibria quantify over solutions, a profile whose state system has no solution would be an equilibrium vacuously. For this reason every existence conclusion (the goal, Theorem 3.10, Proposition 3.4(a)) also asserts that the chosen profiles have solutions, and strong (R)MFE requires the equilibrium SDE to have one.
Infrastructure. A complete proof needs Girsanov's theorem, strong existence for SDEs with bounded measurable drift, measurable selection, tightness on path space, and total-variation propagation of chaos. Each is reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.4(b), the weak half of Proposition 3.7, and Theorem 2.7 are outside this mission.
In the multi-armed bandit problem a learner repeatedly chooses one of actions and observes only the loss of the action it chose. Two models of the environment dominate the literature. In the stochastic model the losses of each arm are drawn i.i.d. from a fixed distribution, and the optimal pseudo-regret grows like , where is the gap between the mean loss of arm and that of the best arm (Lai and Robbins, 1985). In the adversarial model the losses are arbitrary and the optimal rate is (Audibert and Bubeck, 2010). Algorithms that are near-optimal in both models without knowing which one they face are called best of both worlds.
Timeline:
There are arms and rounds . In round the learner draws an arm from a probability vector in the simplex , the environment fixes losses , and only is observed. The environment may adapt to the past actions and use its own randomization, modelled by a seed drawn once from a probability measure . The pseudo-regret is
with the expectation over the seed and the learner's draws; a minimizing arm is a best arm in hindsight .
α-Tsallis-INF is online mirror descent on the simplex. With , regularization parameters and learning rates , set
The learner keeps importance-weighted loss estimates , their sums , and plays . The potential splits the regret into a stability term and a penalty term .
In the stochastically constrained regime the loss differences have fixed means, , with a unique best arm ( for ). Then and . Write . Theorem 4 uses
With , for every ,
Lemma 17 (Hessian control along a mirror step); Lemma 11, cases 1 and 4 (instantaneous stability); Lemma 20 and Lemma 12, part 2 (penalty); Lemmas 14 and 16 (scalar inequalities for the learning-rate factors); displays (26) and (30) of Appendix D, the stability and penalty bounds under the parameters of Theorem 4.
Lemmas 20 and 12 cover any causal unbiased loss estimator satisfying the bandit feedback assumptions; the other bandit bounds use the importance-weighted estimator.
The theorem shows that the logarithmic stochastic rate is not special to the -Tsallis entropy: for every , tuning the regularizer to the gaps gives pseudo-regret of order in stochastically constrained environments. This places the log-barrier () and entropic () regularizers of earlier algorithms in one family, and isolates the role of asymmetric regularization. Unlike Theorem 1, it needs the gaps to tune , so it is a statement about the reach of the method rather than a practical algorithm.
The result is proved in the paper; no part of it has a machine-checked proof. Formalizing it produces a complete verified analysis of an online-mirror-descent bandit algorithm with time-varying, non-monotone learning rates, including the stability–penalty decomposition, the Hessian control of Lemma 17 and the explicit constant chase of Appendix D. The analysis also checks two points the paper leaves open: the printed bound has where its proof gives , and Appendix D applies Lemma 12, which assumes non-increasing learning rates, to a rate that increases for a few early rounds when is small.
The obvious argument bounds each round's stability by (Lemma 11, case 1) and sums. That bound contains the best arm, whose weight tends to one, so it grows polynomially in and cannot give a logarithmic rate. The arm has to be removed from the stability, which needs a shifted second-order expansion where losses become slightly negative, and that is only controlled once (Lemma 17). The early rounds before must be paid for separately, and the asymmetric and the learning rate interact through constants that must be tracked exactly for the self-bounding step to close.
Arms are Fin K with and the paper's arm is i - 1. Rounds start at 1; an action sequence is h : ℕ → Fin K with h 0 unused. The adversary is the published RegretBandits.Adversarial.Adversary (losses in depending on past actions only) composed with a seed drawn from a probability measure, with losses measurable in the seed. Expectations are explicit: an integral over the seed of a finite sum over action paths weighted by . The algorithm is an argmax predicate on the weight function, never a choice function. is a real supremum over the simplex. Logarithms are natural, and real powers are Real.rpow with nonnegative bases.
The goal takes ; the endpoints , where the paper's learning rate and regularizer are limits, are not stated. The regime "stochastically constrained with a unique best arm" is replaced by the two consequences the proof uses: the self-bounding inequality and . Every such regime satisfies both, so the formal statement is at least as strong as the printed one. The constant in the first term is the one the proof reaches. A trivial formalization is ruled out: the expectation is a genuine probability law, the gaps are tied to the losses through the self-bounding hypothesis, and the weights are determined by the algorithm, so the bound cannot hold vacuously.
A complete development needs the explicit law of a bandit run with an adaptive randomized adversary, unbiasedness of the IW estimator, convex conjugates and Bregman divergences on the simplex, and elementary real analysis for Lemmas 14 and 16. The run-law and the stability–penalty decomposition are reusable for any mirror-descent bandit algorithm. Proofs of any milestone, and of the scalar Lemmas 14 and 16 in particular, are welcome independently.
Runtime monitoring checks a running system against a specification by inspecting its trace of events as it is produced. Policies on data, such as "every published report was approved within the last 10 days" or "each value stored in in reaches out within 5 time units", quantify over data values and constrain the time between events. Metric first-order temporal logic (MFOTL) expresses such policies: it extends first-order logic with past and future temporal operators that carry intervals of allowed time differences.
Basin, Klaedtke, Müller and Zălinescu (J. ACM 62(2), Article 15, 2015) give a monitor for MFOTL properties with bounded. It allows negation and quantification over the infinite domain without restriction, because every relation it manipulates is represented by a finite automaton: the input structures are automatic structures. The paper implements it in the prototype tool MonPoly-Reg (§6). Its correctness rests on Theorem 3.9: the monitor reports exactly the violations of , at every time point.
A signature has finitely many constants and predicates with arities. Formulas are built from and by , , and the temporal operators (previous), (next), (since) and (until), where is a nonempty interval of with . A formula is bounded if every in it has .
A temporal structure assigns to each time point relations and a time stamp ; constants are rigid, , and exceeds every bound. Satisfaction is Definition 2.2; for example holds at if holds at some with and holds at all . For with free variables , the satisfying set is
A domain representation is a regular language over a finite alphabet with a surjection whose equality relation is regular. A relation is regular if the words (the letter-by-letter convolution, padded with ) with form a regular language.
The monitor (Fig. 2) reads one element per loop iteration. It extends each to with auxiliary relations (and , for since and until) for every temporal subformula , built incrementally by the constructions of §3.4 once a list of pending triples says that enough of the future has been read. When is complete it outputs the set with , where is with each top-level temporal subformula replaced by the atom .
For every input satisfying the restrictions of §3.1 and every bounded :
where each output is followed by line 11 setting to the next index. This records counter values reached inside the while loop, including values that may never appear at a loop entry. Part (ii) excludes the vacuous reading of (i).
Theorem 3.9 makes a sound and complete monitor for the safety fragment , bounded: every violation at every time point is reported, nothing else is, and every output is a finitely represented (regular) set even though it may be infinite. It covers unrestricted negation and quantification, which finite-relation monitors (§4 of the paper) cannot handle. The incremental constructions of §3.4 are the template reused by later MFOTL monitors.
The paper gives a mathematical proof of its monitor's correctness. This mission asks for a Lean proof that checks the MFOTL semantics, automatic relations over , and the correctness of this particular monitor, including the until construction whose printed version is defective (see Formalization scope).
Two parts are hard. The regularity claims need the fundamental property of automatic structures: first-order definable relations are regular, which requires closure of padded convolution languages under Boolean operations, cylindrification, permutation of tracks and projection, the last with removal of trailing padding. The arithmetic constraints of the since and until constructions additionally need successor and offset relations definable from .
The scheduling argument is the other part. Correctness of a build at requires that every input relation, at time points up to for until, was built before and not discarded since. Following only the syntax of does not settle this: a needed relation for a subformula at a later time point may be built in the same iteration as 's.
The domain is , as §3.1 assumes. Relations are sets of lists of natural numbers, ordered by the sorted free variables. Interval upper bounds are in ; intervals carry the proof that they are nonempty. The representation is a single parameter shared by the hypothesis "every is regular" and the regularity claims of the conclusions; it is never chosen existentially. The binary predicate interpreted as is a hypothesis.
Two hypotheses on besides boundedness are the paper's own "without loss of generality" assumptions: each temporal subformula occurs once in (§3.6), and the direct subformulas of each , subformula have the same free variables (§3.4; achieved by padding with , as in §3.5). No other restriction is placed on .
The printed until construction (§3.4.4) is repaired: the guard of is " for all ", since the printed guard empties in the paper's own example of §3.5; keeps only tuples with , since otherwise a -witness at time point survives to time point when ; and time-stamp equations are encoded additively. Lemma 3.8(i) reads and adds . "Effectively computable" in Theorem 3.9(i) is not formalized. Part (ii) uses the output at index as the record of the line-11 increment to ; for , the counter is initialized by line 2. Loop-entry states alone can skip counter values reached within one iteration.
The monitor is a state machine whose builds and outputs are computed only from its store of relations; it never consults the satisfaction relation or satisfying sets. A formalization in which line 7 reads the semantics would turn Theorem 3.9(i) into a restatement of Lemma 3.4, and is ruled out. A build whose input is missing stores nothing, so a monitor that silently fails would violate (ii).
Contributions welcome: the theory of automatic relations (reusable beyond this mission), the semantic halves of Lemmas 3.4–3.8, and the scheduling invariants.
A directed polymer in a random environment is a random walk whose paths are weighted by the disorder they encounter. The walk favors paths with large accumulated weight, and its endpoint distribution can concentrate on a small number of sites even though the number of possible paths grows exponentially. Understanding how much probability remains spread across many small endpoint masses is a basic question about localization. The distinction matters especially beyond exactly solvable polymer models, where explicit formulas for the endpoint law are rarely available. Bates and Chatterjee study this question for independent disorder in every spatial dimension under a finite exponential-moment condition Bates and Chatterjee, 2021.
The paper separates two temperature regimes using the limiting free energy. Earlier localization statements detected persistent large atoms. The target here asks whether those atoms account for all endpoint probability in a time-averaged sense. It also specifies the complementary high-temperature behavior, where a suitable vanishing mass threshold captures asymptotically none of the probability. The result is Theorem 1.1 of the preprint, restated as Theorem 6.3 Bates and Chatterjee, 2021, pp. 16, 43.
Fix . A path starts at the origin in and makes one of its nearest-neighbor moves at each integer time. The environment consists of independent, identically distributed real random variables with common law . The disorder law is nondegenerate: it is not concentrated at one number. An inverse temperature determines the weight of a path of length :
The endpoint mass function is the sum of weights of paths ending at , divided by the sum of all path weights. Thus is a probability mass function on . For , the -atoms are the sites , and is their total mass. The strict inequality matters at a threshold equal to an atom mass.
Write for , with , and . The standing condition is that this exponential moment is finite for every . The paper's Theorem A characterizes the high-temperature phase by and the low-temperature phase by Bates and Chatterjee, 2021, pp. 4–5.
The goal is both clauses of Theorem 1.1. For every positive deterministic sequence , low temperature gives
At high temperature there exists a positive deterministic sequence for which the same average converges almost surely to . The sequence in this second clause is selected independently of the realized environment. Together the clauses characterize the paper's stronger, almost-sure form of asymptotic pure atomicity Bates and Chatterjee, 2021, Theorems 1.1 and 6.3.
The milestones are fifteen statements of the paper, in the order the proof of the goal uses them:
The low-temperature conclusion rules out a residual diffuse component in the time-averaged endpoint law. A vanishing threshold may still be used to collect almost all of the polymer's probability. The high-temperature clause shows that this property distinguishes the phases under the stated moment assumption. The result strengthens a statement that only asks for a positive amount of mass on large atoms, and gives an almost-sure conclusion for the Cesàro averages Bates and Chatterjee, 2021, §§1.2.3, 6.
A formal development would supply a reusable compactification of endpoint probability measures and a checked route from its invariant laws to localization observables. The milestones expose the pieces that need separate verification, and the compactification and variational formula are reusable for the companion mission on geometric localization. The paper proves the mathematical theorem; this mission asks for its Lean proof and the supporting definitions. A compiled statement with sorry is a proof obligation, not a completed machine-checked result.
The endpoint distribution may move through space as time grows, so ordinary pointwise convergence of mass functions does not capture concentration. The compact state space used by the paper permits separated clusters to live on different copies of . Its distance identifies translated representatives and loses information about remote mass. A direct application of weak convergence to the event also fails at a threshold, because the mass-above-threshold functional is not continuous. The proof must handle its one-sided semicontinuity and the limiting behavior of the update law Bates and Chatterjee, 2021, §§2–3, 6.
Lean represents sites as Fin d → ℤ and paths as finite step sequences, so the starting point, the choices per step, and the normalization of are explicit. An environment is a measurable independent family on a probability space with common law . The unused time-zero row comes from indexing cells by ; only rows with index at least one enter the polymer. The moment condition includes the full interval , and the disorder law must be nondegenerate. Both phase predicates refer to the canonical product environment, making the classification depend on , , and rather than on an arbitrary realization.
Partitioned subprobability measures are structures of nonnegative summable functions with mass at most one. Their topology is generated by the paper's distance balls. The Borel representation identifies states at distance zero, corresponding to the paper's separation quotient . Finite partial isometries carry the degree penalty through an infimum over admissible degrees. The update uses an extended nonnegative sum before conversion to a real denominator. The intended probability law requires the almost-sure finiteness of that denominator and measurability of the update. The real-valued energy integrals require the stated moment condition; a default value for a nonintegrable integral cannot serve as the paper's expectation, and a non-measurable update would make the pushforward the zero measure, which is not the paper's object either. The infimum is taken over the set itself, never as a real infimum whose empty inner range defaults to . The intermediate results in §§3–4 and Lemma 5.1 use the standing range. Theorems 1.1 and 5.2 explicitly include . Wasserstein cost imports the published RWPI.SqrtLasso.transportCost definition.
Solvers can contribute proofs of the compactness, continuity, variational-formula, invariant-law, and atom-functional milestones, or of reusable supporting results such as Lemma 2.11 (measurability of the update) and Corollary 2.5 (when ). The strict positivity of thresholds, nondegenerate disorder, genuine probability laws, and full phase hypotheses are essential: removing any of them could make a formally easy statement unrelated to Theorem 1.1.
A set-valued predictor returns, for each input , a set of plausible responses rather than a single guess. Such sets are used wherever a model's output feeds a decision with asymmetric costs: a medical classifier that lists every diagnosis it cannot rule out, a segmentation model that marks every pixel that may belong to a tumour, a protein-structure predictor that reports a range of distances. Bates, Angelopoulos, Lei, Malik and Jordan, Distribution-Free, Risk-Controlling Prediction Sets (J. ACM 68(6), 2021), calibrate a nested family of such predictors so that a chosen loss is controlled with high probability, without distributional assumptions.
Calibration says nothing about which family to calibrate. Any nested family can be made risk-controlling; families differ in how large their sets are, and large sets are uninformative. §4 of the paper asks which family is best in the population: which predictor achieves a given risk with the smallest expected set size. For a weighted miscoverage loss (Theorem 7, §4.2) the answer thresholds a weighted conditional density, in the spirit of the optimality results of Sadinle, Lei and Wasserman (2019) for classification. Theorem 8 (§4.3) extends the answer to every loss of integral form. This mission formalizes Theorem 8.
Let take values in with law , marginal , and conditional law of given . Prediction sets are subsets of a measurable space (in the paper's examples ). A set-valued predictor is a map .
Fix a finite measure on and a nonnegative cost ; is the cost of leaving out of the prediction set when the true response is . The loss of a set is the total cost of what it leaves out,
and the risk of a predictor is (§2.1). Larger sets have smaller loss. The conditional expected cost of omitting at is
and for the threshold predictor of display (11) is
It includes exactly the points whose omission is expected to cost at least . The size of a set is its -measure, , and the expected size of a predictor is .
In Lean: setLoss μ ℓ y S, risk P μ ℓ T, condLoss κ ℓ x z, thresholdSet κ ℓ lam x and expSize P μ T in the namespace RiskControl.Optimal.
For every and every set-valued predictor (with measurable graph),
No constant is involved; the statement is uniform over , , and .
The result. Theorem 8 identifies the population-optimal shape of a set-valued predictor for every loss that charges for omitted points through a nonnegative cost and a finite measure. It justifies building nested families by thresholding an estimate of the conditional expected cost: if the estimate were exact, no other predictor with the same or smaller risk could have smaller sets on average. It contains the weighted-miscoverage case (Theorem 7) when is discrete and is counting measure, and it covers losses for which no such special case exists, such as costs that depend on the distance between and .
Formalizing it. The proof on p. 27 is a chain of eight displays. A machine-checked version settles the measure-theoretic points the chain passes over: the conditional expectation inside an integral over a random set, the cancellation of possibly infinite terms, and the range of . To our knowledge no formal proof of Theorem 8 or of the Neyman–Pearson-type optimality results it generalizes for set predictors exists in Lean or Mathlib.
The natural reading of the proof subtracts the quantity from both sides of the risk comparison to pass from complements to sets. Nothing in the setting makes this quantity finite, so that step is not valid as written, and a proof that follows the displays literally breaks there. The theorem itself does not need finiteness of , and no such hypothesis is in scope.
The other obstacle is measure-theoretic bookkeeping. The conditional expectation is indexed by a point of a second space, and must be a jointly measurable function of before it can be integrated over the random set ; here it is given by a regular conditional distribution, and every integral over needs the measurability of the graph of .
The development needs Mathlib's composition of a measure with a kernel, Tonelli's theorem for kernels and lower integrals over sections of a measurable set. Lemmas about expected -sizes of random sets (milestone 4) and about moving a kernel integral inside a set integral (milestone 1) are reusable beyond this mission. Proofs of the milestones, and of the goal by other routes, are welcome.
Sparse recovery asks when a vector with few nonzero coordinates can be reconstructed from fewer linear measurements than unknowns. A related geometric question asks how many faces of a high-dimensional cross-polytope survive a random linear projection. The two questions meet at the same threshold: uniqueness of a minimum-one-norm solution corresponds to a face of the projected cross-polytope. For Gaussian measurement matrices this threshold was known before the work of Bayati, Lelarge and Montanari, from Donoho's face-counting analysis (Donoho 2006); the same curve was later identified as the transition of approximate message passing (Donoho, Maleki and Montanari 2009). Their 2015 paper establishes the same weak-neighborliness curve for a broader class of independent sub-Gaussian entries with a nonzero Gaussian component. The result addresses the universality question posed for these projections: does the asymptotic transition depend on the full entry distribution or only on broad features of the matrix law?
The mathematical theorem is established in that paper. This mission records its statement in Lean and leaves the machine-checked proof open. The relevant statement is Theorem 2 on page 5 of the pinned arXiv version 2, rather than a claim about every random projection without a Gaussian component.
The cross-polytope is the unit ball for the coordinate one-norm in :
For an matrix , the projected polytope consists of all with . Write for the number of nonempty faces of whose affine dimension is . The weak neighborliness level of a random sequence means that, for every , the ratio converges in probability to one, while the analogous ratio with converges in probability to zero. Both limits belong to the definition; the first alone would record only survival below a candidate threshold.
The matrices have rows for a fixed sampling ratio . Within each matrix, the entries are independent, centered, unit-variance, and sub-Gaussian with one scale factor independent of . They also admit a decomposition , where and the entries of are independent standard normal variables, jointly independent of . The theorem imposes no independence between matrices with different values of Bayati–Lelarge–Montanari, Theorem 2.
Let and be the density and distribution function of a standard normal random variable. The paper defines its phase boundary through a positive parameter :
Footnote 3 states that decreases from one to zero on the nonnegative half-line, so each has exactly one positive parameter. The goal, Theorem 2, says that whenever , the sequence has weak neighborliness in probability. The Lean theorem spells out this parameter relation; it does not apply an inverse function at an argument outside a proved range.
The milestone list covers the two scalar results identifying the boundary, a deterministic condition for exact recovery, and the compressed-sensing transition. With standard normal and , the scalar function is
Lemma 8 gives its unique positive minimizer and its minimum value. Lemma 9 relates that minimum to both sides of the boundary. The scalar state evolution , with and soft thresholding, has slope at the origin and is concave (Lemma 7). Lemma 10 shows that a two-time correlation map satisfies on . Theorem 10, cited from Bürgisser and Cucker, bounds the probability that a Gaussian-perturbed rectangular matrix has a small least singular value:
Lemma 5 gives a recovery condition based on an approximate dual certificate and singular-value bounds. Theorem 8 states that minimum-one-norm recovery succeeds with probability tending to one below the boundary and fails with probability tending to one above it Bayati–Lelarge–Montanari, pp. 39–41, 60–61.
The goal would certify that the same face-count transition applies to every entry law in the stated class, including laws that are not identically distributed across the matrix. The conclusion is geometric: it counts faces of an actual projected one-norm ball. The recovery milestone provides a second way to state the threshold for sparse signals. Together they make the normalization and the two sides of the transition explicit, so future variants can compare their assumptions and conclusions with a fixed formal statement.
No machine-checked proof of Theorem 2 or of the selected milestones is known. The declarations are open Lean statements over explicit definitions. A complete development would formalize the known argument in the paper, including the probabilistic estimates and the bridge from recovery probabilities to face counts. Sharper results that remove the Gaussian component would be separate theorems with their own hypotheses.
The count of surviving faces depends on many supports and sign patterns simultaneously. Matching means and variances of matrix entries does not make their finite-dimensional face counts equal. Likewise, controlling recovery for one fixed signal does not immediately control the fraction of all faces. Near the boundary, exact recovery also requires uniform singular-value information for many column submatrices. These are the points where elementary concentration for a single entry or a single support is insufficient. The source paper treats the geometric statement and the recovery transition under a Gaussian-component condition; a proof that silently assumes full Gaussianity would miss its universality claim.
Vectors are functions on Fin n, and every one-norm is an explicit sum of absolute values. The squared Euclidean norm is a sum of coordinate squares; the default norm on Fin n → ℝ is not used for it. Face counts reuse the published Grunbaum2003.faceCount definition, with dimension for nonnegative ; negative dimensions have zero nonempty faces. The two limits in weak neighborliness use convergence in measure, which expresses convergence in probability here. The printed lower ratio has a zero denominator for , so that limit is stated for . Ratios at small may involve zero denominators, but the asymptotic assertion concerns arbitrarily large .
Theorem 2 uses variance one and an Gaussian component. Theorem 8 instead uses variance and an component, exactly as printed. Sub-Gaussianity uses Mathlib's moment-generating-function predicate for all real parameters; this is the operative two-sided reading of the paper's stated scale condition. The scalar Gaussian expectation in is accompanied by an explicit integrability conclusion in Lemma 8, excluding Lean's zero value for a nonintegrable integral. The restricted least singular value is the infimum of output norms on unit column vectors. This gives zero when a wide submatrix has a kernel and is the bound needed by Lemma 5. The state-evolution map is written as a function of , and its derivative at is a right derivative. In Lemma 10 the law of is the three-atom mixture on , with the split of the mass between the two infinite atoms left free. The page's clause is stated for , since the derivative equals at . Theorem 10 quantifies and , which the page leaves implicit.
The random-matrix predicates require measurability, independence within each , the stated marginal laws, and independence of from . They leave the matrix law otherwise arbitrary. The weak-neighborliness predicate contains both face-ratio limits and ; neither the goal nor a milestone defines the threshold by assuming its conclusion. A full proof needs reusable facts about Gaussian integrals, independence of finite arrays, random face counts, restricted singular values, and the relation between projected faces and unique one-norm recovery. Contributions establishing those facts or closing any of the listed theorem statements are within scope.
Mean field games (MFG) were introduced by Lasry and Lions (2007) and by Huang, Malhamé and Caines (2006) as limits of stochastic differential games with many symmetric players. The model is only meaningful if equilibria of the -player games actually converge to equilibria of the limit game. That convergence depends on what information the players use. For open-loop equilibria, where controls are functions of the noise, it was established in general by Lacker (2016) and Fischer (2017). For closed-loop equilibria, where a player's control is a feedback on the observed states of all players, the deviation of one player changes the state processes of all others, and the only general results before this paper (Cardaliaguet, Delarue, Lasry and Lions, 2019) required a unique MFE and a smooth solution of the master equation.
Timeline:
Fix a dimension , a horizon , a compact convex control set in a normed space, an initial law on , and bounded continuous functions , , , where ranges over the probability measures with the weak topology (Assumption A). Assumption B asks that be convex for each .
In the -player game, player picks an admissible closed-loop control : a measurable, non-anticipating function of time and of the paths of all states. The states solve
with independent Brownian motions and i.i.d. initial states of law , and player receives . A closed-loop -Nash equilibrium is a profile from which no player gains more than by a unilateral deviation. The random empirical measure flow is an element of .
A function of , with a measure flow, is semi-Markov if it depends on only through . A weak MFE is a filtered probability space carrying a random flow , a Brownian motion and a state with , with independent, a semi-Markov control driving , optimality of against every semi-Markov alternative (the alternative state being driven by the same and ), and the consistency condition . When is deterministic this is the usual (strong) MFE.
Under Assumptions A and B, if , , and is a closed-loop -Nash equilibrium of the -player game, then
and every subsequential limit in law is the law of the flow of a weak MFE. No constant and no rate is asserted.
Without convexity (Theorem 3.9) the same holds with weak relaxed MFE, and Proposition 3.7 identifies weak relaxed MFE flows with weak MFE flows under Assumption B. The proof path of Section 5 is: tightness of the path-space empirical measures (Lemma 5.1), a projection lemma (Lemma 5.2), the realization of a randomized Fokker–Planck equation by a semi-Markov relaxed control (Lemma 5.3), identification of the limiting dynamics with the limiting average value (Theorem 5.4), approximation of relaxed by continuous controls (Lemma 5.5), and the limit of unilateral deviations (Proposition 5.6). Two supporting results come from Section 2.1 (well-posedness of the -player system) and Appendix A (Corollary A.7).
The theorem shows that the mean field game is the correct limit of closed-loop -player games without any uniqueness assumption, which is the regime where the master-equation method is unavailable. The price is the limit object: a weak MFE, whose measure flow may be random and whose control may depend on the past of the flow. The paper also shows (Proposition 7.2) that this randomness genuinely occurs, so the result cannot be strengthened to strong MFE in general. Combined with the converse (Theorem 2.11, mission 2 of this series), it characterizes which MFE arise as closed-loop limits.
The result is proved in the paper; nothing in it is machine-checked. A formalization produces a checked definition of closed-loop -player games and of weak semi-Markov MFE, which are reusable for any MFG convergence result, and it would make explicit the measurability bookkeeping (semi-Markov controls, completed filtrations, conditional laws) that the paper outsources to its appendices.
The obvious argument fails at the deviation step. In the open-loop setting a deviating player leaves the other players' states unchanged; here the other players' feedback controls react to the deviation, so the state of every player changes. The paper's way around this is to identify the limit with semi-Markov controls and show that the value of a deviation can be approximated by -player deviations of a specific form; making this work requires relaxed controls, a measurable projection onto the filtration of the (random) flow, and well-posedness of SDEs with bounded measurable drift and random coefficients. A newcomer's first idea, passing the Nash inequality to the limit with Markovian limit controls, does not work, because the limit flow is random and the limit control must see its past.
EthierKurtz.SDEState d; Brownian motion is the platform's EthierKurtz.IsStandardBrownian. is Mathlib's ProbabilityMeasure with the weak topology and the Borel -field of that topology. Paths and flows are continuous maps on with the uniform topology.NSol is inhabited and the weak MFE predicate is satisfiable (checked for ), so neither the hypotheses nor the conclusion of the goal holds vacuously; the conclusion asserts the existence of a weak MFE with the limiting flow law, not a property of an arbitrary one.A lower bound on Ricci curvature can be expressed in two ways that make sense far beyond smooth manifolds. The Eulerian way bounds the gradient of the heat semigroup: Bakry and Émery's -calculus gives . The Lagrangian way bounds how heat flow moves probability measures in optimal transport distance: . On Riemannian manifolds the two are equivalent (von Renesse–Sturm 2005). Kuwada (2010) showed that the equivalence is a general duality between a pointwise gradient bound with a constant and -contraction with the same constant, valid on length metric measure spaces.
Ambrosio, Gigli and Savaré (arXiv:1209.5786v4, Ann. Probab. 2015) needed this duality in a setting with no doubling or Poincaré inequality, where the semigroup comes from an abstract Dirichlet form and is only defined almost everywhere. Their §3.2 builds the dual semigroup on probability measures and proves the contraction (Theorem 3.5). Combined with their Theorem 3.17 it gives Corollary 3.18, the step that links the Bakry–Émery condition to -contraction and, later in the paper, to .
Let be a complete separable metric space with a Borel measure of full support such that for every ball (condition (MD)). The space is a length space if is the infimum of the lengths of curves joining to (3.2).
A Dirichlet form on is a lower semicontinuous quadratic form with dense domain that does not increase under normal contractions; it is strongly local if whenever and have disjoint supports. Its heat flow solves in . It is mass preserving if (2.12).
denotes bounded Lipschitz functions, the slope, and the Borel probability measures. The Wasserstein cost is
Two hypotheses on the semigroup, with bounded on every :
for . Under (3.15) the map extends uniquely to a weakly continuous dual semigroup , and is the pointwise version of (Proposition 3.2).
Under (MD), the length property, (2.12), (3.15) and (3.16), for every and ,
The constant is left free; the goal is the duality itself, not a particular curvature bound.
The theorem turns a pointwise, infinitesimal estimate on functions into a global estimate on measures. In the paper, with it gives the -contraction of the heat flow under (Corollary 3.18). That contraction is an ingredient of the identification of the heat flow with the gradient flow of the entropy (Theorem 4.17). The argument of §3.2 avoids doubling and local Poincaré assumptions on the metric measure space (p. 26), which is what makes it usable for the general Energy measure spaces of the paper.
The result is proved in the literature: in Kuwada's paper, and in the form posed here in §3.2 of the source. As far as a search of the Prove2Me catalogue shows, none of it is formalized: there is no Wasserstein distance on a general metric space, no dual semigroup of a Dirichlet form, and no Hopf–Lax semigroup on metric spaces. The mission asks for formal proofs of the known argument; the dual semigroup, Lemma 3.3 and the Hopf–Lax estimates are reusable on their own.
The semigroup acts on classes, while (3.16) and the contraction are statements at every point; the bridge is the pointwise version , which exists only through the dual semigroup and its weak continuity. The direct approach, applying the gradient bound along a geodesic between and , fails because is not a supremum over Lipschitz functions of a linear quantity. The route goes through the quadratic Kantorovich duality and the Hopf–Lax semigroup on a metric space, neither of which is available in Mathlib, and through limits of integrals against varying measures . Passing from Dirac masses to arbitrary needs a measurable selection of optimal plans.
IsHeatSemigroup, IsDualSemigroup), not constructions. IsDualSemigroup requires for probability densities and weak continuity on , which determines on . Choosing as anything else (e.g. the identity) does not satisfy the predicate, so the goal is not trivialized that way. Dropping the length property would change the statement.Contributions welcome: the quadratic Kantorovich duality on Polish spaces, Hopf–Lax calculus on length spaces, measurable selection of optimal plans, and the portmanteau-type Lemma 3.3.