Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Classical mean-field theory describes diffusions that interact symmetrically, each feeling the empirical average of all the others, and shows that as every particle behaves like an independent copy of a single McKean–Vlasov process. Many systems of interest are not symmetric: neurons, agents in a financial network, or oscillators interact through a graph, and particles in different parts of the graph feel different neighbourhoods. A graphon is the limit object of dense graph sequences (Lovász, Large Networks and Graph Limits, AMS 2012), and it is the natural way to describe the interaction structure of such systems in the limit.
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) study a continuum of diffusions indexed by labels whose interaction is weighted by a graphon, and prove laws of large numbers and rates of convergence for -particle systems on graphs sampled from the graphon. This mission targets their uniform rate of convergence for weights sampled from a Lipschitz graphon (Theorem 3.2).
Write with Lebesgue measure. Fix a horizon and let with .
On one probability space, are i.i.d. -dimensional Brownian motions and are independent initial states with laws , independent of the Brownian motions. Given a graphon and coefficients , the graphon particle system (2.1) is
with . The particles are independent but not identically distributed, and their laws are coupled through the -integral.
The -particle system (3.1) uses the same randomness at the labels :
so particle and the continuum particle at share their initial state and Brownian motion.
The hypotheses are:
Under Conditions 2.1, 2.3 and 3.2 there is such that
The result. Theorem 3.2 gives a quantitative propagation of chaos for heterogeneous interactions: with weights sampled from a blockwise Lipschitz graphon, every particle of the finite system, not just an average particle, is within in root-mean-square path distance of the continuum particle with the same label. The rate matches the classical mean-field rate (e.g. Sznitman 1991), so heterogeneity of the interaction costs nothing in the exponent. The same estimate covers the deterministic weighted graph and the random graph sampled from (in the annealed sense), and it is the dense counterpart of Theorem 4.2 for percolated graphs.
Formalizing it. The result is proved in the paper (§6.3); it has no machine-checked proof. A formal development would produce a reusable account of graphon particle systems and their finite- approximations: graphon-weighted McKean–Vlasov drifts, couplings through shared noise, and the decomposition of the interaction error into a Lipschitz feedback term, a law-of-large-numbers term and a Riemann-sum discretization term.
The obvious approach is to compare with directly and close a Gronwall inequality. The difficulty is that the comparison involves the empirical, graph-weighted average of the other particles, which is neither the graphon average nor an average of independent terms. Three different errors must be controlled simultaneously and uniformly in : the feedback of all particles' errors into particle , the fluctuation of a sum of independent but non-identically distributed terms whose weights may themselves be random, and the error of replacing an integral over labels by a sum over the grid . The last needs regularity of the law in the label , which is itself a theorem about the graphon system (Theorem 2.1(b)) and fails at block boundaries of , where only the small number of boundary cells saves the rate. Averaging over , as in the law of large numbers of Theorem 3.1, is not enough: the goal bounds the maximum.
Fin d → ℝ with the sup norm; matrices are measured entrywise. All statements are norm-invariant because every constant is existential. Particle is Lean's i : Fin n with label ; time is ℝ≥0; is Mathlib's unitInterval.Peng1990.SMP.Stochastic definitions; an SDE with random initial value is stated as an Itô process for . Each continuum particle uses the natural filtration of ; the -particle system uses the natural filtration of the weights, initial states and Brownian motions at the labels.WassersteinDRO.Duality.wassersteinDistance 2, valued in ; expectations of nonnegative quantities are lower Lebesgue integrals.Policy gradient methods optimize a parameterized policy by gradient descent on its expected total cost. They are a staple of reinforcement learning and of simulation-based optimization in operations research, but the objective is nonconvex in the policy parameters, and the standard theory guarantees convergence only to a stationary point. J. Bhandari and D. Russo (arXiv:1906.01786v3, Operations Research, 2024, DOI 10.1287/opre.2021.0014) identify structural conditions under which every stationary point is globally optimal.
Their first result (Theorem 1) requires the policy class to be closed under policy improvement. That excludes many classes used in practice, where it is known only that some member of the class is optimal: base-stock policies in finite-horizon inventory control are the standard example (Bertsekas, Dynamic Programming and Optimal Control, 1995). For stationary policy classes, containing an optimal policy is not enough: the paper's Example 1 has a policy class that contains the optimal policy, and policy gradient still gets stuck in a bad local minimum. Theorem 3 shows that for finite-horizon problems with a non-stationary policy class (separate parameters for each period), containing an optimal policy suffices, together with a single-period regularity condition imposed only at the optimal cost-to-go. This mission formalizes Theorem 3.
A Markov decision process consists of a state space , nonempty feasible action sets , a bounded measurable cost , a transition kernel , a discount factor and an initial distribution . A policy is a measurable map with ; is the set of all of them. The cost-to-go is , the loss is , and the discounted state-occupancy measure is . An optimal policy has pointwise for all ; . With the Bellman operator , the weighted policy-iteration objective is
A parameterized policy class is for a convex , and . A point is stationary for if is differentiable at and for all .
The finite-horizon structure (Condition 3) embeds a time-inhomogeneous problem in this discounted formulation: the states split into stages ; from a state in , , every feasible action leads to ; and is a costless absorbing state. The parameter is a concatenation , the parameter set is a product , and on the action depends only on . The stage objectives are .
Condition 4 asks that for every , the problem has no suboptimal stationary points. Assumption 3 asks that for every . Condition 0 asks that the policy-iteration objective be continuously differentiable in the parameters.
Under Conditions 0, 3 and 4 and Assumption 3, if is an optimal policy for some , then every stationary point of on satisfies
Theorem 3 covers finite-horizon dynamic programs in which a structured class of time-varying policies is known to contain an optimal policy, but is not closed under policy improvement: the paper's Example 8, multi-period inventory control with base-stock policies, is the motivating case. Policy gradient on such a class has no suboptimal stationary points, so any method that finds a stationary point finds a globally optimal policy, optimal among all policies and not only within the class. Condition 4 involves only the Bellman objective of the optimal cost-to-go , which often has regularity (for instance convexity) that the cost-to-go of an arbitrary policy lacks.
The result is proved in the paper. To our knowledge no part of it, nor the policy gradient theorem for deterministic policies on general state spaces, has a machine-checked proof. Formalizing it requires a measure-theoretic treatment of occupancy measures, the stage-wise decomposition of the weighted policy-iteration objective, and the backward induction of App. D.2.
The obvious approach reasons stage by stage directly on , but couples the stages: changing changes the distribution of states visited after stage . The paper's argument instead passes through the policy gradient theorem, which turns stationarity of into stationarity of single-period problems weighted by the occupancy measure of the current policy. These single-period problems involve , while Condition 4 speaks about ; relating them requires a backward induction over stages in which almost-sure equality on stage is transported to stage through the balance equation. This step needs the occupancy measures of all policies in the class, including policies other than , to be equivalent to , which is where Assumption 3 enters. The naive variant with a stationary policy class fails (Example 1).
The state and action spaces are arbitrary measurable spaces (the paper takes Borel subsets of Euclidean spaces; no argument uses that structure). Cost and kernel are given on all state-action pairs; the cost is bounded. Policies are deterministic, stationary and measurable; parameters live in EuclideanSpace ℝ (Fin d), so gradients and norms are Euclidean. is never defined as an infimum: an optimal policy is a hypothesis, with . Stages and sub-vectors are numbered from by a measurable stage index and a block index on coordinates; the product structure of is encoded as closure under exchanging one block.
Hypotheses beyond the printed sentence of Theorem 3, all disclosed in the item statements: Assumption 3 (announced on p. 17 as required, used in the proof); Condition 0 (needed for Lemma 6, which the proof invokes), in a joint form that the proof of Lemma 6 uses and that implies the printed partial-map form; the standing Assumptions 1 and 2 of §2; and, inside Condition 4, differentiability of on , the premise of Definition 1. The Bellman operators carry the factor omitted in the printed (3)–(4). The stage-wise balance equation is stated for ; the printed range fails at the absorbing state.
A formalization in which the goal assumes the stage-wise characterization (31), the balance equation, or on any stage is not Theorem 3; neither is one where "contains an optimal policy" means optimal only within . Stationarity includes differentiability, so a junk zero gradient never makes a point stationary.
Needed infrastructure: occupancy measures as series of iterated kernels and their balance equation, the cost-to-go as a bounded measurable function, the performance difference identity, the policy gradient theorem, and the decomposition of integrals over the stage partition. The occupancy-measure and policy gradient results are reusable for every mission of this series; contributions of these general lemmas are welcome.
Policy gradient methods optimize a parameterized control policy by gradient descent on its long-run cost. They underlie much of modern reinforcement learning, from REINFORCE and actor-critic methods to trust-region and proximal policy optimization, and they are used in operations problems such as inventory control and optimal stopping. Their objective is almost never convex in the policy parameters, even in textbook problems, so the classical guarantees of first-order optimization do not explain why they reach good policies.
Bhandari and Russo (arXiv:1906.01786v3, Operations Research, 2024, doi:10.1287/opre.2021.0014) identify structural conditions under which this non-convex landscape is benign. Their Theorem 1 shows that, for a policy class closed under policy improvement, every stationary point is globally optimal. This mission formalizes their Theorem 2, the quantitative version: approximate stationarity implies approximate optimality, a gradient dominance (Polyak–Łojasiewicz-type) inequality that yields convergence rates.
Timeline. Polyak (1963) introduced the inequality for unconstrained problems. Kakade and Langford (2002) proved the performance difference lemma for finite Markov decision processes. Fazel, Ge, Kakade and Mesbahi (2018) established gradient dominance of policy gradient for linear-quadratic control, and Agarwal, Kakade, Lee and Mahajan (2021) for tabular policies with direct and softmax parameterizations. Bhandari and Russo (preprint 2019, journal 2024) give a single condition-based argument covering general state spaces and several of these examples.
A Markov decision process has a measurable state space , feasible action sets , a bounded expected cost , a transition kernel , a discount factor and an initial distribution . A stationary policy maps states to feasible actions; is the set of measurable such policies. Its cost-to-go is , its discounted state-occupancy measure is , and its loss is . An optimal policy has for every .
The Bellman operator is and is its optimality version. The weighted policy iteration objective is
A policy class is with convex, and the policy gradient objective is . For , the map is the single-period problem that one step of policy iteration within the class would solve.
A function is -gradient dominated over (, ) if for all
The hypotheses are Condition 0 (differentiability of in the policy and occupancy arguments), Condition 1 (closure: for every some minimizes over all of ) and Condition 2.B (each single-period objective is -gradient dominated over ). The effective concentrability coefficient is the smallest with for all , .
If Conditions 0, 1 and 2.B hold and , then
It is stated for every satisfying the concentrability inequality, which is the page's statement at .
The remark of §3 that differentiable -strongly convex functions are -gradient dominated and convex ones -gradient dominated, and Corollary 1: under Conditions 0 and 1, convexity (strong convexity) of every single-period objective makes gradient dominated of degree one (two).
Gradient dominance of degree two gives linear convergence of projected gradient methods, and degree one gives sublinear rates, so Theorem 2 converts structural knowledge about one-step policy improvement into iteration complexity for the multi-period problem. The constant makes explicit the dependence on the initial distribution: an exploratory with small is what the guarantee needs. The paper instantiates the conditions for tabular MDPs, linear-quadratic control, optimal stopping with threshold policies, and finite-horizon inventory control.
The result is proved in the paper. As far as is known, none of it is machine-checked: Mathlib has convexity, strong convexity, gradients and Markov kernels but no discounted dynamic programming on general spaces, no occupancy measures and no policy gradient theorem. The formal development would supply the general-space performance difference identity and the policy gradient theorem, reusable for every other result of the paper and for related work on policy optimization.
The policy gradient objective is not convex, so the usual derivation of a Polyak–Łojasiewicz inequality from convexity is unavailable. Gradient dominance of the single-period objective does not transfer to by comparing the two functions: they differ by how a change of policy moves the state distribution, these terms do not vanish, and the minimum of over is not the minimum of . The mismatch between , and is unavoidable, which is why a concentrability factor appears in the constants. On a general state space each identity also needs the right measurability and integrability (the measurable-selection assumption is what makes measurable), and Condition 0 must be strong enough to justify a total-derivative expansion.
All declarations live in PGLandscape.GradDom. and are arbitrary measurable spaces; the cost is bounded and measurable and, like the kernel, given on all of . Policies are measurable maps; the cost-to-go is a series of integrals against -step kernels; is a measure of total mass one. The parameter space is EuclideanSpace ℝ (Fin d), so is the Euclidean gradient and the norm. is for an optimal given as a hypothesis; no real infimum over policies is used.
Committed conventions and disclosed additions:
A formalization that assumes gradient dominance of , the closure bound, or a finite state space would not be this theorem; the goal assumes only Conditions 0, 1, 2.B and concentrability.
Contributions welcome: Markov-chain lemmas for iterKernel (summability, measurability, the fixed-point equation ), the general-space performance difference identity, and proofs of any milestone.
Policy gradient methods search for a policy by changing a finite vector of parameters. The method can reach a stationary point of its objective without finding an optimal policy: a small change in the available parameters might not represent the policy improvement that the underlying control problem calls for. Bhandari and Russo identify a condition on the policy class that limits this obstruction. Their exact-closure result rules out suboptimal stationary points; their approximate-closure result measures the residual cost when the class can represent policy improvements only approximately. This mission formalizes the latter statement, Theorem 5 of Bhandari and Russo, Global Optimality Guarantees for Policy Gradient Methods, using the arXiv v3 text and numbering.
The result concerns the optimization landscape rather than a particular gradient algorithm or convergence rate. It applies to structured policy classes in discounted control problems, including settings with general state spaces. The paper also discusses state aggregation as a source of small approximation error in Lemma 15; that example motivates the error condition, while the target here is the general guarantee of Theorem 5. The error is measured in the states visited by each current policy, so the condition describes what the restricted class can do where improvement affects that policy's performance.
A Markov decision process has a measurable state space , a measurable action space , and a nonempty feasible action set at each state . Choosing incurs a bounded cost and changes the state according to a probability kernel . A discount factor reduces future costs, and an initial probability measure specifies where evaluation begins. A stationary policy is a measurable choice .
The cost-to-go is the expected sum of discounted costs when starting at and following . The discounted occupancy measure is the normalized, discounted distribution of visited states when the initial state has law . The policy's objective is . The factor puts on the scale of a per-period cost. An optimal policy minimizes cost-to-go at every state. Section 2, pp. 5–8 supplies these objects and Assumptions 1 and 2: absolute continuity of with respect to , and measurable selection of a Bellman-minimizing action for bounded measurable value functions.
A parameter belongs to a convex set and determines a feasible policy . The policy gradient objective is . A stationary point is a feasible parameter with for every . The Bellman optimality operator selects the smallest one-step cost plus discounted future value among feasible actions. The weighted policy improvement objective evaluates the one-step Bellman update from a candidate policy , averaged under the current policy's occupancy measure. Section 5.1, pp. 12–14 introduces its smoothness and stationary-point conditions.
The target is Theorem 5, p. 26. Condition 5 says the restricted class has inherent Bellman error : for each current policy in the class, a class member gets within of the best one-step weighted Bellman objective over all feasible policies. Condition 2.A says stationary points of that weighted one-step objective are global minima over . Condition 0 supplies differentiability. For a nonnegative coefficient satisfying the effective concentrability inequality (13), the goal is continuous differentiability of and, at every stationary point,
The paper defines as the least coefficient satisfying (13). The Lean statement quantifies over an admissible ; its conclusion therefore includes the bound at when that coefficient is finite. The milestone list follows the paper's supporting statements: occupancy domination after (2), Bellman inequalities (5), the performance difference identity (29), the policy gradient formula in Lemma 6, the stationary policy-improvement identity in Lemma 7, and the Bellman-error bound displayed in the proof of Theorem 5.
The bound turns a property of the policy class into a quantitative guarantee about every stationary parameter. If and a finite concentrability bound applies, the stated cost gap is zero. For positive error, it separates the approximation error from the factor that reflects evaluation under the exploratory start distribution and the effective planning horizon. Thus a small gradient alone is not the claim; the structural conditions on the one-step objective and the policy class determine what stationarity means for long-run cost. Theorem 5 and its discussion, §8 make this interpretation explicit.
The paper proves Theorem 5. The declarations in this mission currently compile as open theorem statements; they are not machine-checked proofs. A complete development would formalize the links among discounted kernels, occupancy integrals, Bellman operators, and gradients on the parameter space. The general measurable-state MDP definitions would be reusable for other discounted control results, while the stationary-point and approximate-closure predicates provide a vocabulary for further policy-gradient theorems.
A stationary point of need not be a minimum of the one-step Bellman objective by definition. Condition 0 and Lemma 6 connect their gradients, and Condition 2.A then links stationary points to minima of the restricted one-step objective. Approximate closure only compares that restricted minimum with the unrestricted one up to . The final result also requires moving an error measured under to one under and relating Bellman residual to the optimality gap. Each comparison has a distinct measure or operator, and losing a discount factor changes the constant in the theorem.
The Lean model uses arbitrary measurable spaces for and and measurable stationary policies, extending the paper's Borel-subset setting. The cost and kernel are defined on all and are uniformly bounded there; feasibility still restricts every policy and Bellman minimization to . These extensions let Condition 0 evaluate nearby parameter values even when their policies need not be feasible. The representation uses Mathlib kernels, measures, Bochner integrals, and Euclidean parameter vectors. It fixes , a probability initial distribution, nonempty feasible action sets, an optimal policy, and the paper's Assumptions 1 and 2. The goal carries a nonnegative concentrability coefficient and Conditions 0, 2.A, and 5; it does not assume exact closure or the Bellman-error conclusion it is meant to establish.
Two corrections to the printed assumptions are explicit. The Bellman operators contain , consistently with equations (6) and (7), although displays (3) and (4) omit it. Condition 0 asks for joint continuous differentiability near the current parameter pair, the form used by the proof of Lemma 6; the printed condition lists two partial maps. The theorem's is constrained to be nonnegative to represent the paper's effective concentrability coefficient. Definitions use pointwise optimality rather than a real-valued infimum over policies, and Bellman minimization uses the nonempty feasible-action subtype. These choices prevent default values of ill-bounded infima or non-integrable functions from turning the target into an empty claim. The needed contributions are proofs of the six milestones and the final bound, plus supporting measurable-kernel and gradient facts.
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.
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.
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.
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.
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.
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.
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.
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.
Many allocation problems divide indivisible goods among agents who are entitled to different shares but cannot pay with real money: course seats among students, shifts among workers, inherited items among heirs. A standard mechanism gives each agent a budget of artificial currency and lets a market run. When budgets are equal this is the competitive equilibrium from equal incomes (CEEI) of Varian (1974), the basis of the course-allocation mechanism of Budish (2011). With indivisible items, however, an equilibrium can fail to exist: one item and two agents with equal budgets already admit none, because whoever does not get the item could afford it at any price the owner can pay.
Babaioff, Nisan and Talgam-Cohen (arXiv 2017; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) ask whether this failure is robust or a knife edge, and answer for two agents with additive preferences: an arbitrarily small, strict inequality between the budgets restores existence. Budish's approximate CEEI perturbs budgets randomly for the same reason; this mission formalizes the exact two-agent result.
A discrete Fisher market has a set of indivisible items and two agents. Agent has a valuation assigning a real value to every bundle , and a budget . Valuations are additive (), normalized (), non-negative, monotone ( when ) and strict (different bundles have different values). Budgets are normalized, ; money has no value to the agents.
An allocation is a partition of all items between the agents. Item prices give bundle prices . Agent demands if and for every bundle with . A competitive equilibrium (CE) is a pair in which each agent demands her own bundle. An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent.
Agent 's budget-proportional share is (her budget times ). Her truncated share is the best value she gets in a PO allocation that gives her at most that share:
The Lean development uses the same names: bundle σ i for , price, IsCE, IsPO, IsStandardValuation, GetsTruncatedShare.
For every two-agent additive market there is such that every budget pair with
admits a CE in which for both agents. The goal fixes no value of ; it asserts only that one exists for each market.
Two companion statements are drafted without being milestones: Theorem 4.4 (second welfare theorem) and Theorem 5.2 (a budget-proportional allocation implies a CE).
The result. Theorem 7.1 shows that the non-existence of CEEI with indivisible goods is a measure-zero phenomenon for two additive agents: equal budgets are the only bad point near equality, and the equilibrium obtained is also fair in the truncated-share sense. It justifies tie-breaking by tiny budget differences in practice. It is the two-agent base case of the paper's main open question (§9.1, p. 20), whether generic almost-equal budgets guarantee a CE for more than two agents; the paper also leaves open two agents with arbitrary generic budgets and non-identical preferences (p. 21). For arbitrary, not almost-equal, budgets, Segal-Halevi (AAMAS 2018) shows that genericity does not guarantee existence for four additive agents.
Formalizing it. No machine-checked proof of any result of this paper is known. The paper's own argument for one case of the goal is incomplete: in Case 2(b) of the proof of Theorem 7.1 (p. 19) it asserts that the two candidate allocations are mirror images of each other and that the rectangles are empty. Both claims fail on an explicit three-item market. Theorem 7.1 itself held in every one of 6000 markets checked numerically during planning, including that one, where a CE with truncated shares exists at prices proportional to one agent's valuation. A formal proof therefore has to supply an argument the paper does not contain; the two false steps are not posed as milestones.
The milestones 1–5 are finite combinatorics on the Pareto frontier with sign bookkeeping. The difficulty sits in Case 2(b) of the goal: every allocation gives one agent more than and the other less. The natural route, invoking Lemma 6.3, needs some to be empty, and in that case both can be non-empty. Lemma 6.3 does not cover it, and the paper's symmetry argument cannot be repaired by choosing smaller, since in the counterexample the two candidate allocations stay the same for every small . A complete proof must show directly that one of the two "as fair as possible" allocations is supported by suitable prices.
Items are Fin m and agents Fin 2; the paper's agents 1, 2 are indices 0, 1, so "" reads b 1 < b 0. An allocation is a map σ : Fin m → Fin 2, which builds in that every item is allocated exactly once. All quantities are real numbers. Demand quantifies over every bundle, with strict inequality . Prices are non-negative by definition of a CE. The truncated share is a maximum over PO allocations only.
Two conventions are disclosed restrictions or additions:
In the goal is chosen after the valuations and before the budgets. A formalization in which depends on the budgets, demand ranges over a restricted family of bundles, allocations need not allocate every item, prices may be negative, or the truncated share is a maximum over all allocations, would be a different and in several cases trivial statement; all of these are ruled out.
The definitions file GenericBudgets.AlmostEqual.Setting holds the market, CE, PO, the fairness notions, combination pricing, Condition (1), and , and is reusable for any two-agent indivisible-goods market with budgets. Proofs of the milestones, a repaired argument for Case 2(b), and general -agent versions of the CE and PO infrastructure are welcome.
There are two standard ways to do analysis on a non-smooth space. The first starts from an energy: a Dirichlet form on , its heat semigroup and its carré du champ . This is the setting of Bakry–Émery -calculus and of the curvature-dimension condition . The second starts from a metric measure space : slopes of Lipschitz functions, the Cheeger energy, Wasserstein distances, and the synthetic Ricci bounds and of Lott–Villani and Sturm.
Moving between the two requires a dictionary. A Dirichlet form defines a distance, the intrinsic distance (Biroli–Mosco, Sturm). That distance defines a Cheeger energy. The question is whether the energy rebuilt from is the energy we started from. Ambrosio, Gigli and Savaré answer this in §3.3 of their paper on the Bakry–Émery condition and Riemannian Ricci bounds (arXiv:1209.5786, Ann. Probab. 2015). Their answer is the identification used in the main theorem of the paper, .
Timeline:
Let be a set with a σ-additive measure . A Dirichlet form is a lower semicontinuous quadratic form with for every 1-Lipschitz with , and with dense domain . It is strongly local when whenever a.e. for a constant . A function belongs to , with carré du champ , if for all bounded .
Let be the set of continuous with a.e. The intrinsic distance is
An Energy measure space (Definition 3.6) is a strongly local Dirichlet form on a Polish space with a fully supported Borel measure such that is a finite complete distance inducing , and a continuous has its truncations in .
On the metric side, is the slope, and the Cheeger energy is
Condition (MD) asks that be complete and separable, , and balls have finite measure. Condition (ED) asks that every be 1-Lipschitz for (ED.a), and that every Lipschitz with and bounded support lie in (ED.b). is upper-regular (Definition 3.13) if every in a dense subset of is an limit of bounded continuous with bounded upper semicontinuous and .
For an Energy measure space,
and in this case .
The identification lets every metric notion be applied to an energy structure. Once it holds, the Wasserstein gradient flow of the entropy, the formulation and all make sense for the energy. That is the route by which the paper proves that on a Riemannian Energy measure space implies , the converse of the earlier result. Theorem 3.12 gives the one-sided inequality under the single condition (ED.b), and (3.41) says the energy density is the squared minimal weak gradient. Mass preservation is a standing hypothesis of several other results of the paper, and here it comes for free.
All of these results are proved in the paper, partly by citation: the mass-preservation clause rests on [6, Theorem 4.20], and the length property uses a midpoint criterion from Burago–Burago–Ivanov. None of them has a machine-checked proof. Mathlib has no Dirichlet forms, no Cheeger energy and no theory of length spaces built from curve length. This mission produces precise Lean statements of the paper's identification theorem and of the lemmas its proof uses, so that the metric–energy dictionary can be built up and proved one piece at a time.
The inequality is the easy direction once (3.32) is available. Proving (3.32) means bounding the energy density of the Hopf–Lax inf-convolution pointwise by . Only finite minima over a countable dense set lie in , so the bound has to pass to the limit through the lower semicontinuity (2.10) of .
The reverse inequality needs the opposite move: from an -a.e. bound to a pointwise bound on the metric slope at every point. That step is Proposition 3.11. It needs to be upper semicontinuous and to be a length distance. Without upper semicontinuity, an a.e. bound says nothing about the slope at a given point. The obvious idea, testing against the Lipschitz functions given by (ED.b), produces only lower bounds on and cannot give . That is why upper regularity is the exact condition. The length property (Theorem 3.10) is itself proved by contradiction from a Lipschitz test function built from two disjoint balls. On a space that is not locally compact, this needs a completeness argument rather than Hopf–Rinow.
Representation. Elements of are functions . is off , and every predicate is invariant under -a.e. equality. The σ-algebra is Borel (BorelSpace), standing in for its -completion. The topology is the topology of the metric of , and condition (b) of Definition 3.6 says that this metric equals . Completeness and separability are typeclass binders. The carré du champ is a predicate on a density, never a chosen function. Slopes, , and curve lengths take values in . The curve length is the total variation, which agrees with . The truncation profile of (3.27) is a parameter with the properties the paper fixes. "Dense in " means dense for the norm . The minimal weak gradient is required to be nonnegative, which makes its two characterizing conditions determine it. Mass preservation is stated on , with part of the conclusion. In Theorem 3.9 the printed "distance on " is read as a distance on .
Ruling out trivializations. The Cheeger energy is defined from slopes of bounded Lipschitz functions and never through . Upper regularity is Definition 3.13 with a dense approximating set, not the identity .
Infrastructure. A complete development needs carré du champ calculus for strongly local forms (chain rule, (2.9), (2.10)), the Hopf–Lax semigroup on metric spaces, relaxation and minimal weak gradients, and the midpoint characterization of length spaces. Mathlib has none of these, and all of them can be reused beyond this mission. Contributions of any of these pieces, and proofs of individual milestones, are welcome.
Curvature bounds on a smooth Riemannian manifold control diffusion and the behavior of probability measures. Metric measure spaces extend these questions to limits that need not be smooth. A useful curvature condition must continue to hold when a sequence of spaces converges. Ambrosio, Gigli, and Savaré prove that their analytic Bakry–Émery curvature-dimension condition has this stability property for Riemannian energy measure spaces under Sturm–Gromov–Hausdorff convergence Ambrosio–Gigli–Savaré, Theorem 5.8. The result connects a condition stated through heat flow and Dirichlet forms with convergence stated through distances between probability measures.
The article's §5.2 first defines the convergence of spaces and of functions living in different spaces, then states the stability theorem. This order matters: the measure changes with the space, so ordinary convergence of functions on one fixed measured space cannot express the claim Ambrosio–Gigli–Savaré, Definitions 5.4 and 5.6.
A metric measure space consists of a complete separable metric space and a measure . The class contains probability measures with finite second moment. The squared Wasserstein distance is the infimum of the mean squared transport cost over couplings of and .
A sequence Sturm–Gromov–Hausdorff converges to when there is a complete separable ambient metric space and distance-preserving embeddings , including , such that . The embeddings need not be onto. This definition compares measures on different spaces after placing them in one ambient space; it does not assume that the original spaces coincide Ambrosio–Gigli–Savaré, Definition 5.4.
An energy measure space has a strongly local Dirichlet form , its associated heat flow , a carré du champ , and an intrinsic distance agreeing with . The Cheeger energy is the relaxed integral of one half the squared local slope. A Riemannian energy measure space also has the upper-regularity and continuous-representative properties of Definition 3.16. The paper writes in this situation Ambrosio–Gigli–Savaré, Definitions 3.6 and 3.16 and Theorem 3.14.
The Bakry–Émery condition bounds a second-order expression involving the heat flow, the carré du champ, curvature parameter , and dimension parameter . The formalization uses the paper's weak distributional form (2.33), writing ; represents . This is the same and for every source space and for the limit Ambrosio–Gigli–Savaré, Definition 2.4 and (2.33).
Remark 5.5 asserts that the Cheeger energy is invariant under an isometric embedding. Lemma 5.7 supplies two criteria (squared norms, or entropies of bounded densities) for convergence of scalar functions across changing measures and shows that continuous maps of linear growth preserve this convergence. Lemma 5.9 says that, in the RCD setting, both heat-flow outputs and their generators converge. These are the mission's formal milestones Ambrosio–Gigli–Savaré, pp. 63–66.
For Riemannian energy measure spaces with and , Theorem 5.8 asks for
The goal includes the assertion that the limit energy is a Dirichlet form; quadraticity is part of the conclusion. It covers finite and with the same statement Ambrosio–Gigli–Savaré, Theorem 5.8.
The theorem permits analytic curvature-dimension bounds to survive convergence even when the carrier spaces, measures, and spaces vary. Without a stability statement, a bound verified separately on approximating spaces would give no such bound for their metric measure limit. The theorem also ensures that the limit Cheeger energy retains the quadratic structure required for the Riemannian theory Ambrosio–Gigli–Savaré, Theorem 5.8 and its proof.
The result is proved in the cited paper. The remaining work here is a machine-checked development of its definitions and proof, including the convergence of heat flows and generator terms across changing measures. The statements in this proposal are proof targets; they are not presented as already machine-checked. The definitions of SGH convergence and graph-law convergence can also support other stability questions for metric measure spaces.
The difficulty is that each acts on a different , while is an inequality involving the semigroup, its generator, and integrals against . Convergence of the underlying measures alone does not imply convergence of those functions or of their squared terms. In particular, pointwise convergence on a common carrier is not even a statement available before choosing embeddings and representatives. The paper's separate notion of function convergence addresses this gap Ambrosio–Gigli–Savaré, Definitions 5.4 and 5.6 and Lemma 5.9.
Lean keeps the spaces indexed by : Xn n, m n, E n, and P n. The goal uses SGH convergence as an existential ambient realization, rather than assuming the paper's common-space reduction (5.10). The source heat flows and the truncation profile are named by their defining properties; they are the paper's determined objects. The limit heat flow is not assumed to exist: the conclusion is stated for every family satisfying the heat-flow characterization of . Functions represent classes, and the common Setting layer records almost-everywhere invariance. The measurable spaces are Borel; the paper's completed measurable structures are represented through measurable versions and almost-everywhere relations.
The formal goal assumes that has full support on . Definition 3.6 requires this, while §5.2 explicitly warns that the ambient SGH limit may fail to be fully supported. The full-support condition makes the theorem refer to the intended limit carrier. The goal does not assume that the limit already is a Riemannian energy measure space or satisfies .
Function convergence uses graph laws on . The chosen product metric is Mathlib's max metric; any fixed finite product metric yields the same convergence in this setting. The squared Wasserstein distance is extended nonnegative, so a missing finite coupling does not turn into a false real value. The limit energy is defined as , with no free energy parameter. Measurable representatives are explicit when forming pushforwards. Lemma 5.9 is stated on a common, fully supported RCD carrier; this narrows its ambient application and is recorded for review. Contributions to the Cheeger-energy invariance, changing-measure function convergence, heat-flow stability, and final BE passage are all within scope.
Textbook quantum theory starts from postulates about Hilbert spaces, density matrices and completely positive maps, none of which has an evident operational meaning. A long line of work, from Birkhoff–von Neumann quantum logic through Ludwig, Hardy (quant-ph/0101012), Dakić–Brukner and Masanes–Müller (arXiv:1004.1483), asks whether the formalism can instead be derived from principles that speak only about preparations, measurements and their statistics.
Chiribella, D'Ariano and Perinotti (Phys. Rev. A 84, 012311 (2011), arXiv:1011.6451) give such a derivation for finite-dimensional quantum theory. Five axioms (causality, perfect distinguishability, ideal compression, local distinguishability, pure conditioning) describe a broad class of information-processing theories containing classical theory; one further postulate, purification, singles out quantum theory. The paper builds on the framework of operational-probabilistic theories of the same authors (Phys. Rev. A 81, 062348 (2010)).
An operational-probabilistic theory (OPT) has systems , a composite system for every pair, and, for each pair , tests: finite families of transformations from to . Tests with no input are preparation tests (families of states ), tests with no output are observation tests (families of effects ). Composing a preparation test with an observation test yields a joint probability distribution , and parallel composition multiplies probabilities. After identifying objects with the same statistics, the states of span a real vector space of finite dimension , effects are linear functionals on it, and transformations are linear maps. denotes the normalized (deterministic) states.
Standard notions are then defined operationally: refinement and coarse-graining, pure states and atomic effects/transformations (only trivial refinements), completely mixed states (refined by every state), reversible transformations, the face of a state, and perfectly distinguishable families (there is an observation test with ). The informational dimension is the common size of all maximal perfectly distinguishable families of pure states.
For every theory satisfying the six principles and every system , there is a real-linear isomorphism with
and , the size of every maximal family of perfectly distinguishable pure states. In words: the normalized states of every system are exactly the density matrices on .
In the order of the paper: Theorem 6 (maximal distinguishable sets and completely mixed states), Lemma 16 (atomicity of composition), Theorem 8 (pure state / atomic effect duality), Lemma 32 (the informational dimension is well defined), Corollary 15 (), Theorem 9 with Lemma 10 (the invariant state is the uniform mixture of any maximal set), Theorem 10 (spectral decomposition), Theorem 12 (), Theorem 13 (the Bloch ball and for ), Theorem 16 (superposition principle).
The result shows that, inside a class of theories defined by operational requirements, the density-matrix formalism is forced by purification. The intermediate results are of independent interest: an operational spectral theorem (Theorem 10), the dimension formula (Theorem 12) that replaces Hardy's "simplicity" axiom, and the derivation of the qubit Bloch ball (Theorem 13). Corollary 52 of the paper upgrades the goal to transformations (all completely positive trace-non-increasing maps), using a cited result of the 2010 framework paper; it is not part of this mission's goal.
The paper is a physics article with diagrammatic proofs and several steps delegated to the earlier framework paper. A formalization makes every framework assumption explicit and checks the derivation end to end; no machine-checked development of operational-probabilistic theories is known to the proposer.
The derivation never assumes a Hilbert space, so the matrix representation must be built from the principles: first qubits (via the Bloch ball classification, which uses the classification of compact subgroups of ), then projections on faces, the superposition principle and finally a coordinate system on -level systems in which positivity of all states can be checked. Each step relies on many operational lemmas (Choi isomorphism, teleportation, uniqueness of purification up to channels) that in the paper are proved diagrammatically or cited.
Lean namespace InfoDerivQT. A theory is a structure OPT already in quotiented, finite-dimensional form: is modelled as , effects as linear functionals, transformations as linear maps, and tests as families indexed by finite types. The framework records the circuit rules used throughout the paper: the probability rule, product rule, coarse-graining, identity, sequential composition with classical control, classical randomization, rescaled preparations, parallel composition of all kinds of tests, conditioning on one side of a bipartite state, swap and associator, closedness of the state set, and spanning of states and effects. Because transformations are identified with their action on single-system states, this encoding is faithful in the presence of local distinguishability (Eq. (5) of the paper), which every target assumes. The trivial system is not modelled. The six principles are bundled in OPT.SatisfiesPrinciples; quantum theory is a model, so the hypothesis is satisfiable. The choice of framework axioms is the main point for audit: a missing circuit rule could make a target false, an extra one could exclude intended theories.
Contributions welcome: proofs of the milestones, a formal check that finite-dimensional quantum theory is a model of SatisfiesPrinciples, and the Choi isomorphism and teleportation lemmas of Secs. IV and IX as further milestones.
In an -player stochastic differential game each player controls the drift of its own diffusion and is rewarded through a running and a terminal payoff that depend on its own state and on the empirical distribution of all states. A player's strategy can be closed-loop (path-dependent), reacting to the whole observed history of all states, or Markovian (in the engineering literature, "feedback perfect state"), reacting only to the current states and the time. The two lead to two equilibrium notions. A Markovian equilibrium is the object produced by the classical PDE approach (a Nash system of parabolic equations), and it is the natural object for mean field game approximations. A closed-loop equilibrium is the economically more convincing notion, because it rules out profitable deviations to any strategy a player could actually implement.
D. Lacker's paper On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020, doi:10.1214/19-AAP1541) proves limit theorems for closed-loop equilibria as . Its Proposition 2.2, the subject of this mission, shows that under a convexity condition going back to Filippov and Roxin, the Markovian equilibria form a subset of the closed-loop ones. The limit theorems for closed-loop equilibria then apply to Markovian ones as well.
Fix a horizon , a dimension , a number of players , a control set in a real normed space, an initial law on , and functions
Assumption A: is compact and convex, and are bounded and jointly continuous. Assumption B: for each the set is convex; this holds, for instance, if is affine and concave in .
Write . An admissible control is a Borel, non-anticipative map ; the set of these is . A Markovian control is a Borel map , used as ; the set is . A profile drives the states
with independent Brownian motions and i.i.d. initial states of law . Player receives
For , a closed-loop -Nash equilibrium is a profile in with for all ; a Markovian -Nash equilibrium is a profile in with the same inequality, the supremum taken over only.
Under Assumptions A and B, for every ,
The proposition makes the two equilibrium notions comparable: since a priori a Markovian equilibrium is tested only against Markovian deviations, there is no reason for it to survive path-dependent deviations, and without convexity it need not. Under Assumption B, every result about closed-loop equilibria (in the paper: tightness of the empirical measure flows and identification of their limits as weak mean field equilibria, Theorem 2.7) covers Markovian equilibria too, and in particular those built from classical solutions of the Nash system.
The result is proved in the paper; nothing in this mission is open mathematics. To our knowledge none of it is formalized. The mission produces a machine-checked formulation of the -player game with weak solutions, both equilibrium notions, and the comparison; the Markovian projection theorem is a general result of stochastic analysis, used well beyond game theory (local volatility calibration, mimicking theorems), with no formal proof in any proof assistant that we know of.
The obvious attempt is to replace a closed-loop deviation by its "Markovian average", the conditional expectation of the control given the current state. This fails twice. First, and are nonlinear in the control, so averaging the control changes both drift and reward; the convexity of is what allows a single Markovian control to reproduce the conditional drift exactly while not losing reward, and producing it requires a measurable selection that is jointly measurable in time and state. Second, replacing the drift changes the law of the whole state process, so it is not clear that the payoff can be compared at all. Only the one-dimensional time marginals are preserved, and proving that requires the Markovian projection theorem, whose proof rests on uniqueness for a Fokker–Planck equation with merely bounded measurable drift. Neither ingredient is in Mathlib, which has no stochastic differential equations, Girsanov theorem, or Itô formula.
NSol) bundles its own probability space (in Type), filtration, independent Brownian motions jointly forming an -dimensional -Brownian motion, adapted continuous states, i.i.d. initial states of law independent of the noise, and the empirical flow. is evaluated on a given solution, and each -Nash condition is required for every solution of the equilibrium profile and every solution of the deviated profile. This equals the paper's definition because solutions exist and are unique in law (Girsanov, p. 6); proving the goal therefore requires constructing solutions where needed.EthierKurtz.IsStandardBrownian on , made an -Brownian motion by adaptedness and independent increments; is EthierKurtz.SDEState d.NeZero n), , , measurability of every process and control, and the completed filtration of for the strong solution in Theorem 2.14 (platform EthierKurtz.completedBrownianPast). Coefficients and controls take a real time argument, constrained only on .Needed infrastructure: weak solutions of SDEs with bounded drift (Girsanov), strong existence for bounded measurable drift (Veretennikov), Fokker–Planck uniqueness, measurable selection, and disintegration of measures depending measurably on a parameter. The Markovian projection theorem and the Girsanov existence of -player solutions are reusable beyond this mission. Contributions toward any of these are welcome.
Brands that sell consumer goods are held responsible by the public for the labour and safety practices of their suppliers. After the 2013 Rana Plaza collapse in Bangladesh, about 200 clothing brands and retailers signed the Accord on Fire and Building Safety and inspect roughly 1,600 factories jointly; pharmaceutical companies such as Pfizer and GSK audit their suppliers jointly through the Pharmaceutical Supply Chain Initiative (both examples from the paper, pp. 4 and 14). Two features of such supply bases matter for auditing. Competing brands often share a common supplier, so a scandal at that supplier hurts both of them. And brands compete downstream, so a scandal that hurts only a rival can help a brand.
Chen, Qi and Dawande (MSOM 2020; accepted manuscript SSRN 2889889) model two competing buyers with one common and two independent suppliers. Their Proposition 2 shows that, when each buyer audits on his own, competition drives the buyers away from the common supplier: in every equilibrium it is left unaudited. This mission formalizes their Proposition 3. It shows that a coalition that audits jointly, and splits the cost by a Shapley-value rule, does audit the common supplier and is stable. A companion mission (Supplier Centrality … I) covers Proposition 2.
Two buyers source from three suppliers: from its independent supplier , and both from the common supplier . Each supplier is compliant with probability . A non-compliant supplier that passes an audit of effort (probability ) is exposed in public with probability . An independent supplier audited with effort therefore causes damage with probability . The three suppliers offend independently.
If buyer has exposed suppliers, its demand intercept falls from to (by once, however many offend). Each exposed supplier also raises its unit input cost from to . The buyers then play a Cournot game with differentiated products (substitution ). Buyer 's equilibrium profit is , where
The aggregate ex post profit is . Auditing a supplier with effort costs .
Unilateral auditing. Each buyer audits at most one of his two suppliers. is buyer 's expected profit net of his own audit costs. An equilibrium is a pair of mutual best responses in which, by the paper's tie-breaking rule, a buyer who audits strictly prefers it to not auditing. The effort of eq. (2) is a buyer's optimal effort on his own supplier when the rival does not audit.
Joint auditing. The coalition chooses efforts on , auditing at most two suppliers, and pays each audited supplier's cost once. The buyers still compete downstream. With the buyers' expected profits excluding audit costs, the coalition's profit is
The difference of the buyers' profits is . The cost shares are (eq. (3)). The analysis assumes the scenario
There are thresholds such that, for every , an optimal joint plan
The coalition is also stable. At an optimal plan its aggregate profit is at least the buyers' aggregate profit in any unilateral equilibrium. After paying , each buyer earns at least his profit in a symmetric unilateral equilibrium.
The coalition's profit as a sum of unilateral profits (proof of Lemma OA9). Lemma OA9: beats one independent supplier, and beats no audit for . Lemma OA10: with beats with . Lemma OA11: with beats alone for . The fair shares (3). The case analysis with and . Stability.
The result separates two effects of downstream competition on responsible sourcing. Under unilateral auditing, a buyer gains nothing private from auditing the shared supplier: the reduction in risk accrues equally to his rival. The joint coalition removes this free-riding. The common supplier is audited whenever anything is, and the Shapley-type split (3) charges the buyer who also has his own supplier audited for the competitive advantage this gives him ( exactly when ). The paper's welfare comparison (Proposition 4) builds on this proposition and on Proposition 2.
The proof in the e-companion argues through four comparisons of candidate plans and short cost-sharing algebra. None of it is machine-checked. A formal proof fixes the model (in particular which costs the coalition pays and what "at most two suppliers" excludes) and checks each comparison. In one place it also corrects the printed claim: the per-firm stability argument is given only for the symmetric unilateral equilibrium, and it does not extend to the asymmetric one (see Formalization scope).
All objects are explicit polynomials in the efforts. The difficulty is in the comparisons. Lemmas OA9 and OA10 compare different audit plans through the scenario ordering of aggregate ex post profits, an assumption on the stage-2 closed form that is not implied by the standing conditions. The obvious attempt, comparing first-order conditions, fails because the coalition's profit is discontinuous at zero effort (the fixed cost) and the feasible set is not convex: "at most two of three" is a union of faces of the cube. The thresholds , are differences of maxima, so the case analysis has to handle ties and the boundary with weak inequalities. Stability needs the unilateral equilibria of Proposition 2, so the full goal reaches into the companion mission's game.
Params holds with , , , , , and the three positivity conditions of p. 8. Every statement adds (Sec. 4.3 continues the competing case) and the p. 13 scenario as five inequalities between piAgg values. Their arguments count exposed suppliers: is a label, not a damage of .sSup over and . At the profit is a polynomial, so these suprema are attained.Contributions welcome: proofs of Lemmas OA9–OA11, which are self-contained polynomial inequalities; existence of maximizers on the non-convex feasible set (upper semicontinuity); and the link to the unilateral equilibria needed for stability.
Many large convex problems in signal processing, networking and statistics have a separable objective coupled by linear constraints: blocks of variables, each with its own nonsmooth regularizer and its own feasible set, tied together by . The alternating direction method of multipliers (ADMM) is the standard tool for such problems when . For the direct extension of ADMM can diverge, as shown by Chen, He, Ye and Yuan (2016), and convergence guarantees for multi-block variants typically require strong convexity or extra correction steps.
Hong, Chang, Wang, Razaviyayn, Ma and Luo propose the block successive upper-bound minimization method of multipliers (BSUM-M), which updates each primal block by minimizing a local upper bound of the augmented Lagrangian, followed by a dual gradient step, and prove that it converges for any number of blocks without strong convexity of the objective. They also analyse a randomized version, RBSUM-M, in which each iteration updates a single randomly chosen block, primal or dual. Randomized block selection matters when data or computation are distributed and not every block is available at every step. This mission formalizes the randomized half of their main theorem; the cyclic half is a separate mission.
Let with , and consider
The standing assumptions (Assumption A) are: with strictly convex and continuously differentiable; with nonnegative weights; each is a compact polyhedron; the problem is feasible and its primal and dual optimal values are attained.
For the augmented Lagrangian and augmented dual function are
and is the set of minimizers of over . The method works with approximation functions (Assumption B): majorizes in block , touches it with matching gradient at , is strongly convex with modulus and has an -Lipschitz gradient.
RBSUM-M. Fix probabilities summing to 1. At iteration draw with probability . If , take a dual step ; otherwise replace block by
leaving the other blocks and unchanged. The analysis uses the block steps (the minimizer above, computed for every ), the dual step , the gaps , , and the proximal gradient . The error bound with constant is for all and .
Under Assumptions A and B and the error bound, if the stepsizes are either constant and sufficiently small, or satisfy , , then with probability 1
where is the point of nearest to , and every limit point of is a primal and dual optimal pair. The threshold for "sufficiently small" is existential and depends only on the problem data, the , the error-bound constant and .
In the order of the paper: Lemma 2.1 (differentiability of , , the -Lipschitz bound); Lemma 2.3(2) (expected decrease of ); Lemma 2.4(2) (proximal gradient bounded by the block and dual steps); Lemmas 2.5(2) and 2.6(2) (expected change of the dual and primal gaps); and from the proof of Theorem 2.1, (2.24)–(2.25) (expected change of ), (2.28) (constraint violation), (2.29) (the descent estimate with explicit coefficients) and (2.40) (one-step change of ).
The result shows that a randomized, single-block-per-iteration primal-dual method converges almost surely to primal-dual optimal solutions of a multi-block linearly constrained problem, under assumptions that allow a rank-deficient , nonsmooth group-sparse regularizers, and inexact (majorized) block subproblems. The potential function and the way the error bound converts it into a supermartingale estimate are reused in later analyses of multi-block and randomized ADMM-type methods.
The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a checked convergence proof for a randomized augmented-Lagrangian method, a reusable formal treatment of the augmented dual function of a convex program with compact polyhedral constraints, and a precise record of the conventions under which the published statements hold (see the scope section).
The obvious route is to show that decreases. It does not: a dual step increases by , and without strong convexity there is no direct control of the distance to the solution set. The argument has to combine the primal and dual gaps into one potential, bound the residual term through an error bound that holds without strong convexity, and then pass from a conditional-expectation inequality to almost-sure convergence. Under diminishing stepsizes the supermartingale argument only yields , and upgrading this to a limit needs a separate pathwise argument on how fast can move.
Blocks are EuclideanSpace ℝ (Fin (n k)) and the full vector lives in PiLp 2, so norms are Euclidean. is real-valued on all of . The augmented dual function is (the page's (1.9) prints an unconstrained minimum of plus penalty; the constrained reading is the one Lemma 2.1 and (2.19) use). The prox in the proximal gradient includes the constraint set , which is what the proof of Lemma 2.4 needs; the error bound of Lemma 2.2 is a hypothesis of the goal, in its global form on , and is not derived. Lemma 2.2 itself is not part of the mission.
Conditional expectations given are written as the explicit average over the random index, at every state; this is because the index drawn at iteration is independent of . The goal is stated on an arbitrary probability space carrying mutually independent indices with law , for every run from a deterministic start , . Iterations are indexed from as on the page.
Two printed statements are corrected and labelled in their items: Lemma 2.1 asserts (not each ) constant over , and Lemma 2.6(2) uses where the page prints . Statements are not trivialized: the setting is satisfiable (for instance , , , , , ), the stepsize threshold precedes the probability space and the run, and the solution sets entering distances are nonempty under Assumption A. A formalization in which the error bound or the gap bounds are assumed in a form that already contains the conclusion would not count.
A complete development needs: Danskin-type differentiability of and the -smoothness of the augmented dual; first-order optimality and nonexpansiveness of the prox of ; and the Robbins–Siegmund almost-supermartingale convergence theorem in Mathlib's conditional expectation framework, together with a bridge from the explicit index average to condExp. The last two are reusable well beyond this mission. Contributions to any of the milestones, or to these general lemmas, are welcome.
Theorem numbers, equation numbers and page numbers in this mission refer to arXiv:1401.7079v1 (printed page = PDF page − 1); the journal version renumbers them.
In an optimal stopping problem the value function and the gain function agree on the stopping set , and on the continuation set . The smooth fit principle says that, at the boundary between them, meets with matching first derivatives. Smooth fit is one of the boundary conditions in the free-boundary problems that characterise optimal stopping boundaries. It is behind the integral equations for the early-exercise boundary of the American put and for many problems in sequential analysis and finance (Peskir & Shiryaev, 2006). On a finite horizon the value depends on the remaining time, and continuity of the time derivative across is the step that justifies the local time-space calculus applied to (Peskir, 2005).
Before De Angelis & Peskir (2020) such continuity results were proved problem by problem, or under sign conditions that the main examples do not satisfy: on the stopping set and globally, which fails for the American put. Their paper gives two general results. Theorem 8 covers the space derivative, and Theorem 15, the subject of this mission, covers the time derivative on a finite horizon. Both are stated for a strong Markov process realised as a stochastic flow, and both rest on probabilistic regularity of the boundary.
Fix a horizon and . The process is the time-space process . Its first coordinate is time, and is a stochastic flow on a probability space with a right-continuous filtration , adapted to it, with . Its paths are right-continuous with left limits, it is left-continuous over stopping times, and it is strong Markov. The flow is continuous in the space variable if, outside one null set, is continuous for every .
Given continuous functions , and of , write . The value function is
over stopping times bounded by the remaining time . The sets are and inside , and . The problem is well posed if the expected payoffs are integrable and the first entry time into is optimal.
The first hitting time of a set is . A point is probabilistically regular for if . The generator (2.14) acts in the space variable, with diffusion matrix , drift , killing rate and jump measure . Its coefficient formula is tied to the flow by the right derivative at zero of the killed spatial semigroup applied to . The function appears in the hypotheses.
Assume well-posedness, (5.9) ( continuous on and on ), (5.10) () and (5.11) (Lipschitz continuity of and in , uniformly in ), and a continuous flow. Assume the local conditions (5.12)–(5.13) and probabilistic regularity for at every . Then
The result. Theorem 15 turns a probabilistic property of the boundary, which can be checked through sample-path arguments, into the analytic smooth-fit condition in time. Continuity of across is the hypothesis that the change-of-variable formula with local time on curves and surfaces requires. That formula yields the free-boundary integral equations for optimal stopping boundaries. The theorem needs no sign condition on or and no strong Feller property. The time-space process is never strong Feller, which is exactly why the earlier strong Feller route to boundary regularity does not apply here.
Formalizing it. The result is proved in the paper; nothing here is open mathematics. As far as is known no part of it has been machine-checked. Mathlib has stopping times and conditional expectation, but no stochastic flows, no generators of jump diffusions and no optimal stopping in continuous time. A complete development formalizes the proof on pp. 20–23 together with the upper semicontinuity of hitting times of open sets (Lemma 4 and Corollary 6 of the paper, posed in the companion mission on the space derivative).
The infinite-horizon argument (Theorem 13, via Theorem 8) perturbs the starting point and reuses the optimal stopping time of the unperturbed problem. On a finite horizon this fails in the time variable. Shifting the start from to shortens the remaining horizon, so the stopping time optimal for is no longer admissible for . A first-order comparison of payoffs therefore cannot be used. The proof truncates the stopping time and controls the truncated part, which is the role of the identity (5.12) and of the window in (5.13). The convergence of the optimal stopping times has to come from regularity of for the interior and continuity of the flow, not from the strong Feller property.
EuclideanSpace ℝ (Fin m) with . Time is ℝ≥0. Points of the time-space domain are pairs in ℝ × EuclideanSpace ℝ (Fin m), and is Set.Icc 0 T ×ˢ univ.WithTop ℝ≥0) with , and are capped by the horizon.ContinuousOn on .Contributions welcome: the hitting-time lemmas (upper semicontinuity of under a continuous flow), dominated-convergence lemmas for the truncated stopping times, and the two halves (5.17) and (5.20).
An optimal stopping rule chooses when to end a stochastic process in order to collect a terminal reward, possibly after earning or paying a running reward. The resulting value function often solves a free-boundary problem: the state space splits into a region where stopping is optimal and one where continuing is better. Smoothness inside either region does not by itself say what happens where the regions meet. This mission concerns the global first spatial derivative of that value function at the optimal stopping boundary.
De Angelis and Peskir proved that a probabilistic condition on the boundary, together with regularity of the process as a spatial flow and explicit integrability bounds, gives continuous differentiability of the value function across the boundary. Their result applies to standard Markov processes with right-continuous paths and left limits, including jump processes; it is not restricted to diffusions or to a constant discount rate. The source is De Angelis and Peskir, arXiv:1812.04564v2, Theorem 8.
Let , let , and let be a stochastic flow: the same probability space carries a path starting from every state . Time is nonnegative. One right-continuous filtration makes every path adapted and is used for every stopping rule. The process is strong Markov, has right-continuous paths with left limits, is left continuous over stopping times, and starts from . Expectations and probabilities written and in the paper are the expectation and probability of the flow under one measure .
The continuous data are a nonnegative discount rate , a terminal reward , and a running reward . The discount accumulated along the path from is . For every finite-valued stopping time of the common filtration, define
This is the infinite-horizon problem (2.1). It is well posed here when all admissible payoffs are integrable and the first entry time into the stopping set is an almost surely finite optimal stopping time. These conditions ensure that is a real, attained supremum rather than a default value of Lean's real supremum or integral. Define the stopping set , the continuation set , and the boundary relevant to the theorem as . For a state set , the first entry time is and the first strictly positive hitting time is . Both may be infinite.
A boundary point is probabilistically regular for if . It is Green regular for when as through , for every . The paper obtains Green regularity by either strong Feller continuity with probabilistic regularity for , or spatial continuity of the flow with probabilistic regularity for . Lemma 1 and Corollaries 2–3 give the first route; Lemma 4 and Corollaries 5–6 give the second. All six statements use an arbitrary closed , as in Section 3 of the source. Source: §§2–3, pp. 3–11.
The milestone results first establish the two boundary regularity routes. In particular, approaching through , the first route gives in probability; the second gives and almost surely. Equations (4.16) and (4.19) then bound, respectively, the lower and upper limits of each coordinate derivative by . The pointwise part of Theorem 8 concludes
The mission goal is the final sentence of Theorem 8. If the theorem's local hypotheses hold at every , then
The hypotheses include the discounted generator representation (2.14) from the problem setup, continuity and interior regularity of , global regularity of , one positive Lipschitz constant for both and , a spatial flow, the four local bounds (4.4)–(4.7) with one radius at each boundary point, and one of the two probabilistic regularity alternatives. The goal retains all dimensions , all nonnegative continuous discount rates, and the source's full class of standard Markov flows. Source: §2.5 and Theorem 8, pp. 7, 11–12.
The conclusion identifies the derivative of the value function on both sides of the stopping boundary. It strengthens a derivative match along a single direction or a chosen sequence into continuous differentiability on the whole state space. This is relevant to free-boundary formulations of optimal stopping, where interior regularity can be available from a Dirichlet or Poisson problem while boundary regularity remains the missing step. The authors describe that distinction in their discussion of smooth fit and global differentiability. Source: §2.5, p. 8.
The mathematical theorem is proved in the 2020 paper. In this mission, the definitions and statements compile as Lean declarations, while the theorem proofs remain to be formalized. A complete development would supply reusable arguments about hitting times, semicontinuity of hitting probabilities, stochastic flows, and limits of derivatives near a stopping boundary. Those components would also support the paper's finite-horizon spatial and temporal results.
The value is a supremum over stopping rules. Differentiating the reward for a fixed stopping time does not automatically differentiate that supremum, because the optimal time depends on the initial state. Near the boundary, even continuity of the value does not control the duration of the optimal rule from neighboring states. The paper's probabilistic regularity conditions address that duration, while (4.4)–(4.7) provide the integrability needed to pass to derivative limits. A direct appeal to interior differentiability leaves the boundary itself untreated. Source: §§3–4.1, pp. 9–15.
The state space is EuclideanSpace ℝ (Fin d) with ; Fin d indices are the paper's coordinates shifted by one. Balls are open Euclidean balls. Time is , and the entry and hitting times live in so an unattained hit has its intended value. The flow is the process; no separate family of measures is introduced. One common filtration is used for all initial states and is right-continuous. Its finite stopping times are the full admissible class, not only hitting times.
The value uses Bochner expectations and real Lebesgue time integrals. Well-posedness records integrability for every admissible payoff and optimality and almost sure finiteness of . The generator clause acts on smooth functions in the domain of the discounted transition semigroup; it retains the paper's diffusion, drift, killing, and jump terms. The boundary is , and approach through continuation points is expressed by the within-set neighborhood filter. Pointwise continuous differentiability means a Fréchet derivative at equal to and convergence of along ; the goal uses global ContDiff. The local bounds retain all independently indexed starting states and coordinates. Their uncountable suprema are represented by integrable common majorants, with timewise measurable envelopes for the suprema inside time integrals. This convention excludes default integral values from nonmeasurable or nonintegrable expressions.
A formalization restricted to Brownian motion, one dimension, zero or constant discount, continuous paths, bounded rewards, or only one boundary regularity branch would state a different theorem. Contributions toward measurable hitting-time events, the two Section 3 regularity chains, the envelope bounds, and the derivative comparison are welcome.