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?
Hotel rooms, rental cars, cloud servers, operating rooms and rental equipment are reusable resources: a customer occupies capacity for a fixed service time, and the capacity returns to the firm afterwards. Many of these settings also allow advance reservation, where a request made today is for a service that starts later. Lei and Jasin study dynamic pricing in this setting. Prices are posted period by period, demand is non-stationary, and the firm wants revenue close to the best achievable while never booking more units than it owns.
Classical network revenue management, where capacity is sold once and never returns, has an extensive asymptotic theory. In that literature, controls that re-solve or adjust a fluid (deterministic) plan are known to lose a vanishing fraction of the optimal revenue as demand and capacity grow (Gallego and van Ryzin 1997; Jasin 2014). Reusable resources break the standard argument, because each sale removes capacity for a window of time and not for the rest of the horizon. Lei and Jasin give the first control for reusable resources with non-stationary arrivals, deterministic service times and advance reservation whose average loss is in the scale parameter (Lei and Jasin, Operations Research 2020).
A firm manages resource types with integer capacities and sells service types over periods . At most one request arrives per period. A type- request made at the beginning of period uses units of resource during periods . Here is the service time and the reservation lead time.
In each period the firm chooses a demand-rate vector , which is equivalent to choosing prices. A type- request then arrives with probability , independently of the past given , and the expected revenue rate is . The deterministic relaxation DET-H maximizes over , subject to
Its optimal value bounds the optimal expected revenue, and the average loss of a control is . Let be an optimal solution of DET-H. The quantity is the smallest number of periods with inside any service cycle of type that carries positive demand.
The control DPC-B splits the horizon, for each type , into adjacent batches , each with positive-rate periods. In period it posts
where is the batch containing . The rate is set to when fewer than units of some resource are free at the service start . The buffer protects capacity, and the batch term corrects for the demand surprises of the previous batch.
There is a constant , depending only on , the curvature constant of Assumption A5 and a bound on , such that for every instance, every valid batch partition with and every in the stated range,
The constant is uniform in , , , , and , which is what makes the bound informative.
A companion item states Lemma 2 in this setting: stretching in time solves DET-H for the -th system of display (7).
Along the scaling (7), Theorem 3 with gives an average loss of . The non-adaptive control DPC of the same paper achieves (its Theorem 1). The result shows that batch-level feedback improves on the square-root barrier for reusable resources, and it does so with heterogeneous service times and advance reservation, which cover car rental and hotel bookings.
Theorem 3 and its lemmas are proved in the paper's e-companion. No machine-checked proof of them, and no formal model of reusable-resource revenue management, is known. The mission produces a Lean model of the setting: capacity windows with lead times, the availability table , an adapted control on finite sample paths, and its exact path law. On top of that model it states the paper's main bound in full. Several printed steps need repair (see the scope section), so a formal proof would also settle the exact constants.
The obvious route bounds each period's loss by a Taylor expansion around and controls the deviations by a martingale inequality. That route needs the control to coincide with the unprojected corrected rate for the whole horizon, that is, no capacity shortfall and no clipping. Capacity is a moving window of overlapping services with different lengths and lead times, so a shortfall at one period depends on requests made up to periods earlier, in other batches and other types. The batch correction makes the rates depend on past errors, so the errors are martingale differences, not independent variables. The concentration bound must hold uniformly over batches whose number grows with , with a variance proxy that is not the batch length. The early periods, before any service of type has completed, need a separate threshold (the two cases of (EC.17)).
All objects are defined in the namespace ReusablePricing.DPCB. The conventions are fixed as follows.
Fin T → Option (Fin K), recording no request or one request of a type in each period. Expectations are finite sums against the exact path law: the product over periods of the one-period law, whose probabilities are the rates posted given the past. The demand law is never left as a hypothesis.The constant is quantified before the instance, after only , and . Choosing it after the instance would make the bound trivial, because the loss never exceeds .
A complete development needs Freedman- or Doob-type inequalities for bounded martingale differences on finite path spaces, second-order Taylor bounds for functions on boxes in , and window-counting lemmas for capacity. The first two are reusable well beyond this mission. Contributions of any of the milestones, of general martingale tools for finite adapted processes, or of a proof of the companion Lemma 2 are welcome.
Hotel rooms, rental cars, cloud servers, hospital beds and event spaces are reusable resources: a customer occupies a unit for a while and then returns it. Pricing them differs from classical revenue management, where a sold unit is gone for good. A sale now blocks capacity only for the length of the service, so the binding constraint is how many services overlap at once. Lei and Jasin (Oper. Res. 2020) study dynamic pricing in this setting with deterministic service times and, in the general model, advance reservations. They measure a pricing control by its average loss against a deterministic (fluid) benchmark.
The paper has two main results. Theorem 1 bounds the loss of a static heuristic, the Deterministic Price Control DPC(). Theorem 3 bounds the loss of an adaptive variant and is treated in the companion mission (II). This mission formalizes Theorem 1, the lemmas its proof rests on (Lemmas EC.1–EC.2 and the displays (EC.14), (EC.15) of the e-companion), and two structural lemmas of the model: the fluid upper bound (Lemma 1) and the scaling of the fluid solution (Lemma 2).
A firm manages resource types with integer capacities and offers service types over periods . At most one request arrives per period. A type- request uses units of resource for consecutive periods (a service cycle), and divides .
The firm posts a demand-rate vector with . A type- request then arrives with probability , independently of earlier periods given the posted rates, and the firm earns the revenue rate . Writing for realized arrivals and , the capacity free at the beginning of period is
The deterministic relaxation is
with optimal solution . The revenue rates are strictly concave, bounded by in absolute value, and have interior maximizers (A4). Near their gradients and Hessians are bounded by (A5, with margins ).
The quantity of display (2) is the smallest number of periods with in any service cycle that carries positive demand for some type .
DPC() posts, in period , the rate , clamped to , for every type with . It turns off every other type (rate ). The average loss of a control is .
For ,
with depending only on , and , and not on , , , or the other data.
Companion statements: Lemma 1 ( for every feasible non-anticipating control) and Lemma 2 (for integer , solves the DET of the -th system , , ).
Along the scaling (1), choosing of order in Theorem 1 gives an average loss of . A control computed entirely before the selling horizon is therefore asymptotically optimal for reusable resources, with an explicit rate. This bound is the baseline against which the paper's adaptive control (Theorem 3, rate ) is measured.
The proof shows a pattern common to fluid-based revenue management: a high-probability event on which the heuristic follows the fluid plan exactly, a martingale maximal inequality bounding the complement, and a Taylor bound for the cost of the buffer. Reusable resources add one ingredient: capacity is checked over sliding windows of length .
The results are proved on paper; none is machine-checked. The formalization would provide a checked version of the model (sliding-window capacity, at most one arrival per period, turn-off), of the high-probability analysis, and of the uniform constant. The printed proof has slips that a checked proof must repair. In particular, the exponent obtained by EC.3's choice of is ; it differs from the printed one by an amount that a larger absorbs.
The obvious argument says that DPC keeps an buffer, so it rarely runs out of capacity. The difficulty is that "rarely" has to hold uniformly over every sliding window of periods. The rates DPC posts are themselves random, because a type is turned off whenever the realized free capacity is short.
Lemma EC.1 breaks this circularity by induction over periods on a fixed event. A capacity window of length straddles two consecutive cycles, which costs a factor in , and only the periods with positive deterministic demand carry a buffer, which is why appears. The demand errors form a martingale-difference sequence with predictable, path-dependent rates, so (EC.15) needs a pathwise bound on the cumulative rate within a cycle. That bound comes from the DET constraint, not from independence.
Finally, the constant must not depend on the instance. A bound in which may depend on or is trivial, since the loss never exceeds .
Everything is stated in demand rates, as the paper does for DET and in all its proofs. Prices, A1–A3 and the price-derivative part of A5 do not appear. A turned-off type has rate .
A sample path is a function from to "no request" or "one request of type ". Its probability is the product of the per-period probabilities under the rates the control posts, so expectations are finite sums. Expected revenue is , the tower-property form of the proofs. Periods are , and window sums whose upper limit falls below the lower limit are empty.
The standing hypotheses, bundled as Standing φL φU Ψ R n̲, are:
The statements "on " are claimed for every path of positive probability in the event. Theorem 1 quantifies after , , and before everything else. This rules out the trivial reading in which is chosen per instance. Step 2 uses where the printed line has , and for . in Lemma 2 is an integer.
Two definition files carry the model: ReusablePricing.DPC.Model holds the instance, DET, A4–A5, and the -th system; ReusablePricing.DPC.Control holds the path law, DPC, loss, events and general controls. A complete proof needs a finite-path martingale toolkit: a Doob-type maximal inequality for exponential submartingales on a finite product space, and the Bernoulli moment-generating-function bound. It also needs a multivariate mean-value or Taylor estimate on a box and an induction over sliding capacity windows. The martingale tools are reusable beyond this mission. Contributions of those general lemmas, of proofs of individual milestones, and of the optional asymptotic corollary (4) are welcome.
A risk sharing problem distributes an aggregate random loss among agents, each of whom evaluates its share with a risk measure . The smallest achievable aggregate risk is the inf-convolution , and allocations that attain it are optimal. In insurance and in regulated banking the allocation is often required to be comonotonic: every share moves in the same direction as the total loss. This is the no-sabotage, or no-moral-hazard, condition of the insurance literature (Huberman, Mayers and Smith 1983; Carlier and Dana 2003). For risk measures that respect convex order, comonotonic allocations lose nothing (the comonotone improvement of Carlier, Dana and Galichon 2012). For the risk measures most used in practice, Value-at-Risk and its relatives, this is not true, so the comonotonic problem has to be studied in its own right.
Liu, Mao, Wang and Wei (2022) study inf-convolutions of tail risk measures, the risk measures that depend only on the distribution of a loss beyond a fixed quantile. Value-at-Risk, Expected Shortfall and Range-Value-at-Risk are all of this kind. Their Theorem 3 shows that the unconstrained inf-convolution of tail risk measures is again a tail risk measure, with tail parameter the sum of the individual ones. Theorem 4, the subject of this mission, treats the comonotonic constraint, and the tail parameter becomes the maximum.
Fix an atomless probability space : every event of positive probability contains an event of strictly smaller positive probability. Random variables are real measurable functions on , and a positive value is a loss. The distribution function of is , and its left-continuous inverse is for . A quantile uniform of is a random variable, uniform on , with almost surely.
For the tail of beyond its -quantile is . Its distribution function is
A risk measure is a -tail risk measure if whenever and have the same distribution (Definition 1). A -generator of such a is a law-invariant risk measure with for all .
Two random variables are comonotonic, , if on an event of probability one, for all . The comonotonic allocations of and the constrained inf-convolution are
Let be an -tail risk measure, , , let , and let be an -generator of . Then for every and every quantile uniform of ,
and is an -tail risk measure.
Theorem 4 gives an explicit formula for comonotonic risk sharing among tail risk measures. The optimal comonotonic aggregate risk of is computed from the tail alone, by sharing the tail among the generators. As a consequence the constrained inf-convolution depends on only through its distribution beyond the -quantile, with the largest individual tail parameter. Compared with Theorem 3, where the unconstrained tail parameter is , the comonotonic constraint keeps the aggregate as tail-focused as the least tail-focused agent. For a regulator this means that comonotonic sharing among, for instance, Expected Shortfall agents at different levels produces a measure that still ignores the body of the loss distribution beyond a known level.
The result is proved in the paper, through Lemma 2, in Appendix B. No machine-checked proof of it is known. Formalizing it requires the comonotonic additivity of quantiles and the explicit construction of comonotonic allocations from quantile functions and a quantile uniform. Both are reusable well beyond this paper: they underlie comonotonic risk measures, distortion risk measures and the comonotone-improvement literature.
The theorem looks like a change of variables, and the proof in the paper is short. The work is in Lemma 2. Part (a) needs the comonotonic additivity of the left quantile function, on for comonotonic with sum , and has to produce an allocation whose sum equals the tail everywhere, not only almost everywhere. Part (b) runs the other way. A comonotonic allocation of the tail has to be extended below the -quantile, where the tail carries no information, without breaking comonotonicity with or the sum constraint. The extension needs each component of the tail allocation to be bounded below. That bound is a consequence of comonotonicity and of the tail being bounded below, not a hypothesis.
Equalities in law between tails are a second source of friction. The tail is defined through a quantile uniform, which is not unique, and the statements must hold for every choice.
The probability space is atomless in the classical sense (an explicit predicate, stronger than Mathlib's NoAtoms). The domain of every risk measure is , all measurable real functions. The paper allows any convex cone containing that is closed under equality in law and under taking tails; fixing is a disclosed specialization. Individual risk measures and generators are real valued; is valued in the extended reals. The sum constraint of an allocation is pointwise on . Equality in law of tails, , is encoded by (6) as equality of and , and the law of is written through (6) as well. Quantile uniforms are quantified over, never chosen, and the generator relation is required for every quantile uniform. The maximum is the supremum over the finite index set, with agents. The existence of generators (Liu and Wang 2021, Proposition 3.1) is cited by the paper and enters as a hypothesis. Part (iii) of Theorem 4, which needs the comonotone-improvement theorem, is out of scope.
A real-valued infimum for would return on an empty or unbounded-below set and make the identity of (i) partly vacuous; the extended-real infimum and the nonemptiness of (one agent takes everything) rule this out.
A complete development needs the left quantile function and its comonotonic additivity, the existence of a quantile uniform on an atomless space (Föllmer and Schied 2016, Lemma A.32), the distribution of the tail (6), and the measurability of composed with a random variable. All of these are reusable, and contributions of any of them are welcome.
Online bipartite matching with stochastic arrivals models the assignment of display-advertising impressions to advertisers: requests arrive one at a time, each must be assigned irrevocably on arrival or dropped, and the arrival sequence is random rather than adversarial. Since Feldman, Mehta, Mirrokni and Muthukrishnan beat the barrier in the i.i.d. arrival model (FOCS 2009), a line of work has designed algorithms with better guarantees. Jaillet and Lu (Math. Oper. Res. 2014) introduce a whole class of such algorithms, the Random Lists Algorithms, and obtain ratios , and for integral arrival rates, vertex weights and general arrival rates.
Two notions of performance coexist in this literature. One compares expectations, ; the other asks that be large on most realizations, as in Feldman et al. Section 2 of Jaillet and Lu shows that, for every algorithm of their class, the two notions are quantitatively linked by an explicit exponential tail bound. This mission formalizes that section.
A bipartite graph has a finite set of advertisers, a set of impression types, and edges ; means advertiser is interested in type . A fixed number of requests arrive at periods , and their types are drawn i.i.d. from a known distribution on . Every advertiser can receive at most one request.
A list for type is an ordered sequence of advertisers interested in . A Random Lists Algorithm fixes, for each type , a distribution over lists (constructed from an LP solution; the construction is irrelevant here). When a request of type arrives it draws a list from and assigns the request to the first advertiser on the list not yet matched, or drops it if every listed advertiser is matched.
Formally, each request carries an outcome in a finite set determining its type and its list ; outcomes are i.i.d. with law . Starting from , the set of matched advertisers after the -th request is obtained from by adding the first advertiser of outside , if any. Then:
If every list contains only interested advertisers, then for every and every ,
It holds for every instance and every law , with no assumption on the size of .
A supporting theorem, not a milestone, records the fact the display uses without stating it: with interested lists, on every realization.
The display shows that the paper's guarantees, proved for the ratio of expectations, transfer to realizations: when , is at least except with probability . It applies uniformly to the whole class of Random Lists Algorithms, whatever the LP and the list distributions, so it covers each of the paper's later algorithms at once.
The result is proved in the paper; nothing about it is open. It has no machine-checked proof. Formalizing it produces a precise model of list-based online matching (the greedy run, the realization-graph optimum, the joint type–list law) that later formalizations of the paper's competitive ratios can build on, and a worked application of the bounded-differences method to a combinatorial online algorithm.
The concluding display is elementary once Lemmas 1 and 2 are available. The two lemmas need McDiarmid's bounded-differences inequality in one-sided form, which Mathlib does not provide, and the bounded-difference properties of ALG and OPT.
Claim 1 is the step where the naive argument fails. Changing one list can change the assignment of every later request, so ALG is not a sum of local contributions, and a single changed list could a priori cascade into many changed assignments; the claim asserts that the cascade never changes the total by more than one. The analogous property for OPT (changing one request's type moves the maximum matching by at most one) is used in Lemma 2's proof but is not stated in the paper.
Measure.pi). Any joint law of type and list is allowed; every Random Lists Algorithm is the case , . Types and lists are not modelled as independent sequences, which would break .Fin n → Option A that uses only edges and gives each advertiser at most one request; the empty assignment qualifies, so the maximum is over a nonempty set. ALG is for the greedy recursion.Contributions welcome: a one-sided McDiarmid inequality for Measure.pi (reusable well beyond this mission), the bounded-difference property of maximum bipartite matchings, and Claim 1.
In distributed optimization, agents connected by a communication network jointly minimize the average of their private losses, exchanging vectors only with their neighbours. This is the computational model of decentralized machine learning (data held by many machines, no central server), of sensor networks and of multi-agent control. A central family of methods is gradient tracking: each agent keeps, besides its copy of the decision variable, an estimate of the network-wide average gradient, refreshed by mixing with neighbours. Gradient tracking removes the steady-state bias of plain decentralized gradient descent and, for smooth strongly convex problems, converges linearly (Nedić, Olshevsky & Shi 2017; Qu & Li 2018).
Sun, Daneshmand and Scutari (arXiv:1905.02637v2, SIAM J. Optim. 2022) study SONATA, a gradient-tracking scheme in which each agent replaces its loss by a strongly convex surrogate and solves a small local problem per round. The setting is broader than earlier linear-rate results in three ways: the problem may be composite (a convex, possibly nonsmooth regularizer ), constrained (a closed convex set ), and only the average loss needs to be strongly convex, not each local loss. Linearizing surrogates recover proximal gradient tracking; surrogates that keep the full local loss recover DANE- and CEASE-type methods, whose rates improve when the local losses are similar.
Agents hold functions . With , Problem (P) is
Assumption A: is nonempty, closed and convex; each is twice differentiable on an open set and convex; on with ; is convex on . Then on for some constants (display (1)), and .
The network is a connected undirected graph on the agents (Assumption B) and a doubly stochastic weight matrix with , on edges and off edges (Assumption D). Its mixing rate is , the largest singular value of (tensored with ).
Each agent has a surrogate , on , whose gradient in matches at , is -Lipschitz, and which is -strongly convex in (Assumption C). Display (15) supplies constants with on ; , , , .
SONATA (Algorithm 1) with step size starts from , and repeats
With the optimal solution, the analysis tracks the optimality gap , the consensus errors , (deviations from the network averages), the tracking error and the step .
If , there is such that for every , every SONATA run and every agent ,
The goal fixes no rate: it asserts R-linear convergence for all small step sizes, which is the shape the paper proves. The explicit rate of Theorem 3.10 and the iteration counts of Corollaries 3.11–3.14 are not posed.
In the order of the proof: the tracking invariant (19); Lemma 3.1 (per-agent descent); Lemma 3.2 (a lower bound on ); Lemma 3.3 (); Proposition 3.4 (); Proposition 3.5 (consensus errors contract at rate up to ); Proposition 3.6 ( bounded by and ); Proposition 3.8 (the four inequalities (50a)–(50d) for the transformed sequences ); and (54), .
Theorem 3.9 gives a linear rate for distributed composite, constrained optimization with gradient tracking, under strong convexity of the average loss only. It covers, through the choice of surrogate, proximal gradient tracking and the distributed versions of DANE and CEASE, and the constants quantify how much a surrogate gains when local losses are similar. The chain of Propositions 3.4–3.8 is a reusable template: an optimality-gap recursion, consensus recursions and a step bound, closed by a small-gain argument.
The result is proved in the paper; to our knowledge no part of it has been formalized. The mission produces a machine-checked statement of the model and of the full chain. Useful contributions include proofs of the individual milestones, a proof of the goal from the milestones, and the general facts they rest on.
The obvious argument fails in two places. First, the local step does not descend on by itself: the tracker is not , and the surrogate's curvature differs from 's, so Lemma 3.1 must compare Hessians of and along a segment through (15), and the descent holds only up to the tracking error. Second, no single quantity contracts: contracts up to consensus errors, consensus errors contract up to , and is bounded back by . No Lyapunov function is given, and the loop gain of (55) involves every constant of the problem, so showing it can be pushed below 1 for some is where the step-size threshold comes from. Also, is not an assumption: it must be derived from connectivity and Assumption D.
Agents' vectors live in EuclideanSpace ℝ (Fin d), stacked vectors are Fin m → EuclideanSpace ℝ (Fin d), and their norm is always the Euclidean norm written out (), never Lean's sup norm. Hessians are derivatives of gradients; Loewner bounds are quadratic-form inequalities. The surrogate's gradient and Hessian are in its first argument. is the operator norm of on Euclidean . Time is 0-based.
A SONATA run is a relation: is any minimizer of the local problem, and any minimizer of on . Assumption A gives no lower semicontinuity of , so minimizers need not exist in general; the paper assumes they do, and so does the formalization, without adding a hypothesis on . A sanity file exhibits instances of all assumptions and of runs (including a nonconstant one), so the run predicate is not empty. " convex" is read as convexity on plus a positive semidefinite Hessian on ; is convex on only. The constants of (1) and (15) are parameters: each statement holds for every valid choice. All of Assumptions A–D are hypotheses of every statement (the paper's standing assumption of §3.3).
Trivializing formalizations are ruled out: is not assumed in place of Assumptions B and D; is chosen before the step size, the starting point and the run; is required; norms of stacked vectors are Euclidean. Two printed slips are handled openly: in Proposition 3.4 is stated with positivity only when or (at , (41) gives ), and is kept as printed in (52d) although (47) has 3. In Lemma 3.2, Lean's makes the bound trivial when .
A full development needs: the mean-value and Taylor estimates for functions with bounded Hessian on a convex set, first-order optimality for constrained convex minimization, the spectral bound for graph-compliant doubly stochastic matrices (posed elsewhere on the platform as StochGradTrack.Const.lemma_1 for a closely related model), and elementary estimates on finite maxima. These are reusable beyond this mission.
Systems of particles that interact through a singular pair potential and are driven by independent noise are used to model vortices in viscous fluids, collective motion of micro-organisms, aggregation phenomena and, more recently, the training dynamics of wide neural networks and stochastic gradient methods. When is large, one expects the empirical measure of the particles to be close to the solution of a deterministic nonlinear PDE, the mean-field limit. Proving this with an explicit rate is difficult when the interaction is singular, because the classical coupling arguments need a Lipschitz force.
The modulated-energy method (Duerinckx 2016, Serfaty 2020, Nguyen–Rosenzweig–Serfaty 2021) measures the distance between the particles and the limit through a renormalized Coulomb/Riesz energy and closes a Gronwall argument on it. Rosenzweig and Serfaty (arXiv:2108.09878) extended it to systems with additive noise in the sub-Coulombic range. This mission formalizes their first main result, Theorem 1.1: the expected modulated energy grows at most linearly in time (polynomially for logarithmic interactions). A companion mission covers their uniform-in-time Theorem 1.2.
Fix and . Positions live in with Lebesgue measure. A real matrix satisfies for all (gradient flows , Hamiltonian flows antisymmetric, and mixtures). The interaction potential is admissible: it satisfies ten assumptions (i)–(x), with model cases () and (). In short: is even, blows up at , is superharmonic on a punctured ball , is smooth off the origin with (plus a logarithm when ), has a Fourier transform comparable to , has a doubling property near , admits a superharmonic extension to when , has a Calderón–Zygmund kernel condition when , and satisfies .
The particle system (1.1) is
with distinct initial points, , and independent standard Brownian motions in . The mean-field equation (1.5) is
for a bounded probability density , solved in the class . The modulated energy (1.6) is
the diagonal being removed to discard the infinite self-interaction of each particle.
There are depending on only and, for every , , admissible and value of , a constant and a threshold such that for all and
The exponent and the constant are left unspecified, as in the paper.
In the order the proof uses them:
The theorem is a quantitative mean-field limit for singular interactions with additive noise on the whole space, covering conservative and dissipative dynamics at once. Since controls a negative-order Sobolev distance between and , it gives convergence of the empirical measure, at a rate in that deteriorates at most linearly in for . Its proof isolates estimates (the decay of the nonlinear equation, the sign of the diffusion term, the commutator bound) that are reused for the uniform-in-time result of the companion mission.
The paper's results are proved; none of them has a machine-checked proof. Formalizing the theorem requires the modulated-energy machinery (smeared charges, Fourier positivity, commutator estimates), a Carlen–Loss decay argument, and an Itô-free treatment of the stochastic system. The milestones of §§2–3 are classical harmonic analysis (Riesz potentials, the Gross–Carlen log-Sobolev inequality) and are of independent use.
A direct Gronwall argument on fails twice. The diffusion term has no sign for a general configuration, because the singularity of at the origin is integrated against a signed measure with atoms; its control needs a second modulated-energy estimate for , which is a potential of order and may be super-Coulombic, hence the extension of assumption (viii). The commutator term requires , and bounding it by alone produces exponential growth in time; the polynomial bound needs the time decay of , which for a nonlinear, non-divergence-free drift is not given by comparison with the heat equation. Finally, the Itô computation for along the singular dynamics needs truncation and stopping times, since is not at collisions.
All objects are defined in one module RieszMF.Linear.Setting. Space is EuclideanSpace ℝ (Fin d) with Lebesgue measure; derivatives are iteratedFDeriv with operator norms, is Mathlib's Laplacian, and the Fourier transform is Mathlib's . Assumption (iv) is read with a constant for each ; (vi) and (1.17) as Fourier transforms paired with Schwartz functions vanishing near the origin; (iii) pointwise on the punctured ball; one radius for (iii), (v), (vii), (viii); in (viii). Assumption (vii) for is printed as for , which together with (ii) is unsatisfiable; it is stated as .
The solution of (1.5) is a mild solution (3.1) in with continuity in the norm, with each a probability density; every integral of (3.1) is required to converge. Because the noise is additive, a solution of (1.1) is a measurable process whose paths almost surely are continuous, never collide, and satisfy the integral equation with the Brownian path; no stochastic integral appears. Brownian motions are Mathlib's IsBrownianReal coordinates, jointly independent over all coordinates. Expectations are lower Lebesgue integrals of nonnegative quantities, and Proposition 6.3 is stated in with positive and negative parts on opposite sides, so no and no default value of a divergent integral enters.
The constants follow the paper's dependency lists: depends on only and is chosen before ; and are chosen after and , before the data, , the configuration, the probability space and . A formalization with constants chosen after , or the configuration, with , with a junk-zero integral in or in (3.1), or with an empty solution class does not count. Corollary 5.6 is posed exactly under its printed assumptions, although its proof for uses the superharmonicity of , which those assumptions do not list.
Contributions welcome: proofs of the milestones, a Lean development of Riesz potentials and of the sharp log-Sobolev inequality on , and the well-posedness of the mean-field equation that the goal takes as a hypothesis (Proposition 3.1 and its global continuation, not posed here).
Banks and insurers hold capital against the risk of their positions, and regulators compute that capital with a risk measure, a functional that maps a random loss to a number. The two standard ones are the Value-at-Risk (VaR), a quantile of the loss, and the Expected Shortfall, an average of the upper quantiles (BCBS 2019). Both look only at the upper tail of the loss distribution. Liu and Wang (2021) called such functionals tail risk measures.
When a total loss is split among several agents, each judging its share with its own risk measure, the smallest total capital achievable is the inf-convolution of the agents' risk measures, and a split attaining it is an optimal allocation. Embrechts, Liu and Wang (2018) computed the inf-convolution for VaR and Expected Shortfall agents. Liu, Mao, Wang and Wei (SSRN 3490348, version of January 16, 2022; published in Mathematics of Operations Research, 2022) extend this to agents with general tail risk measures. This mission formalizes their Theorem 2: one agent uses a VaR, the other an arbitrary monetary tail risk measure.
Let be an atomless probability space: every event of positive probability contains an event of strictly smaller positive probability. A random variable is a measurable map , a positive value being a loss, and is the set of all of them. Its distribution function is . For a level the left and right VaR are
A small is a high quantile. The quantile function is , and denotes a random variable that is uniform on with almost surely.
A risk measure is monotone if a.s. implies . It is translation-invariant if for every constant , and monetary if it is both. For , the -tail of has distribution function (display (6) of the paper). A risk measure is a -tail risk measure if whenever and have the same law.
The allocations of between two agents are the pairs with , and the inf-convolution is
For and the paper introduces the truncation
Let , let be a monetary -tail risk measure, and let . For every and every choice of :
Theorem 2 gives a closed form for the inf-convolution and an explicit optimal allocation. The VaR agent takes the loss above the -quantile, minus a constant, and the other agent keeps the rest, which has the same -tail as the truncated . No convexity, law-invariance or distortion structure is assumed for beyond its being a monetary tail risk measure. The theorem generalizes Theorem 5.3 of Wang and Wei (2020, Insurance: Mathematics and Economics 93), which required a distortion risk measure. Specialized to , it gives . Part 4 says that the tail parameters add: the representative agent of a VaR and an -tail agent is an -tail agent. This is the two-agent instance of the paper's Theorem 3. Parts 1 and 3 together contrast the left and right VaR: an optimal allocation always exists for , while for the value is only a limit.
The result is proved in the paper. As far as a search of the platform shows, it has no machine-checked proof, and the platform has no development of quantile-based risk measures on a general atomless probability space. The mission produces the definitions of left and right VaR, tails, tail risk measures and inf-convolution on , and a checked proof of the theorem.
The upper bound in part 1 is a single allocation. The lower bound must hold against every allocation . It reduces to comparing the distribution function of with that of , but only on the -tail. Turning that comparison into needs both monotonicity and the tail property of . Monotonicity is almost-sure and pointwise, the tail property is distributional, and no coupling between and is given, so the two cannot simply be chained. Part 3 needs an interchange of a limit and an infimum together with the one-sided continuity . Part 4 needs the law of the -tail of to depend only on the -tail of . All of this rests on careful quantile bookkeeping: left versus right inverses, and strict versus weak inequalities at atoms of .
Random variables are functions , and the domain is , the measurable functions. The paper allows any convex cone containing that is closed under equality in law and under taking tails, and fixing is one of the instances it names. The probability space is atomless, as §2.1 assumes throughout. , the VaRs and are encoded as above. is not chosen: parts 1–3 are asserted for every uniform with a.s. The equality in law of tails is encoded through display (6), as equality of and . The risk measure is real-valued; the paper allows the value , but the agents of §2.3 are real-valued. Monotonicity and translation invariance are required on , with monotonicity for almost-sure inequalities.
Allocations sum pointwise. The inf-convolution takes values in the extended reals, so no junk value from a real infimum arises. Part 3 is a one-sided limit in the extended reals, which asserts both that the limit exists and its value. Part 4 uses extended-real versions of "monetary" and "tail risk measure". The level ranges and are hypotheses.
Dropping the tail hypothesis on makes part 1 false: on integrable losses the expectation is monetary but not a tail risk measure. A real-valued infimum in place of the extended one would make the inf-convolution a junk when it is . A choice of by Classical.choose would weaken parts 1–3 to one uniform. None of these is used.
A complete development needs quantile calculus for and (right-continuity of , the Galois connection ), the distribution of , and basic facts on infima in EReal. The quantile lemmas are reusable for every other mission of this series and for any formalization of VaR. Proofs of the milestones, and of the folklore fact that inf-convolutions of monetary risk measures are monetary, are welcome as separate contributions.
Estimating an unknown parameter from a noisy linear measurement is the basic problem behind Kalman filtering, signal recovery and linear inverse problems. A Bayesian statistician picks the estimator that minimizes the mean square error under a prior distribution; a minimax statistician guards against the worst prior in some family. The Bayesian answer depends on a prior that is rarely known, and the minimax answer is often intractable.
Nguyen, Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (Math. Oper. Res. 48(1), 2023) bridge the two by letting nature choose the joint distribution of parameter and noise from a ball of radius around a nominal distribution in the type-2 Wasserstein distance. At the problem is Bayesian; as grows it becomes more conservative. For a normal nominal distribution they show that this distributionally robust problem is solved by an affine estimator, that a normal distribution is least favourable, and that both are computable from a finite convex program. The paper extends the Wasserstein Kalman filter of Shafieezadeh-Abadeh et al. (NeurIPS 2018), which treated a joint normal ball on , to the model with independent parameter and noise.
The parameter is and the observation is , with a known observation matrix and noise independent of . Write for the probability distributions on with finite second moments.
The nominal distribution is a product with radii . Three ambiguity sets of product distributions appear:
Then .
For normal with ,
The left side is the Gelbrich MMSE problem (2.1), the right side the dual problem over normal priors (3.3). The Wasserstein problem (1.7), , and its dual (3.1), , lie between them, so all four values coincide.
Companion statements, not milestones: Theorem 3.5 (problem (3.3) equals the finite program (3.4)), Corollary 4.2 (the optimal affine estimator and the optimal normal prior form a Nash equilibrium on ) and Corollary 4.3 (the minimax estimator from a maximizer of (3.4)).
The sandwich theorem says that robustifying the MMSE problem against Wasserstein uncertainty around a normal distribution costs nothing in tractability: the optimal estimator is affine, the worst-case distribution is normal, and both follow from a convex program in the covariance matrices. The resulting estimator is a Kalman-type update with a least favourable covariance in place of the nominal one, which is what makes the result usable in filtering. The paper also extends it to elliptical nominal distributions (Section 5) and develops a Frank–Wolfe method for (3.4) (Section 6).
The results are proved in the paper; none of them is machine-checked. A formalization adds a checked account of a minimax argument that combines optimal transport (the Gelbrich bound and its equality for normal laws), nonlinear semidefinite programming (Propositions A.3 and A.4) and Bayesian estimation for Gaussian laws. The appendix statements are general facts about the Gelbrich ball of covariance matrices and serve beyond this paper.
The left side of the goal is an infimum over affine estimators of a supremum over an infinite-dimensional set of distributions; the right side reverses the order and restricts nature to normal laws while allowing every estimator. Weak duality gives at once. For the reverse inequality, Sion's minimax theorem cannot be applied to the distributions directly: is not convex, since mixtures of normal laws are not normal, and is not compact in any useful topology. The equality has to pass through the finite matrix problems, where the worst covariance matrices must be shown to stay bounded away from singularity so that the normal noise covariance remains positive definite. That is the role of Lemma A.5 and of the hypothesis .
EuclideanSpace ℝ (Fin d). The risk is a lower Lebesgue integral in , and every optimal value is a - or EReal-valued infimum or supremum restricted by a membership predicate. The finite programs (2.2), (3.4), (A.3), (A.5), (A.6), (A.9) take values in EReal.multivariateGaussian. , means, covariances, the PSD square root and the Gelbrich ball are the published definitions WassersteinDRO.Gelbrich.{wassersteinDistance, meanVector, covarianceMatrix, psdSqrt, meanCovarianceUncertaintySet}.sSup/sInf would make the goal trivial or false. A sanity check exhibits a member of whenever , and an affine estimator.Proofs of any milestone are welcome, and so are reusable lemmas on the Gelbrich ball, the matrix square root and Gaussian conditioning.
Many stochastic models evolve on two time scales: a fast component that equilibrates quickly and a slow component driven by it. Planetary motion, climate models, geophysical flows and intracellular reaction networks are standard examples, and multiscale numerical methods for them approximate the slow component by a reduced equation. Such approximations are only useful with an error bound, and for the fully coupled case, where the fast and slow equations each depend on both components and the slow equation contains a large fluctuating drift, rates of convergence were missing.
Röckner and Xie (Ann. Probab. 49 (2021) 1205–1236) treat this case with only Hölder continuous coefficients and obtain explicit rates in four regimes. This mission poses the first regime, the classical averaging principle.
Timeline. Papanicolaou, Stroock and Varadhan (1977) proved the diffusion approximation for with a compact fast state space and time-independent coefficients. Pardoux and Veretennikov (2001, 2003, 2005) treated a noncompact homogeneous case with and by martingale problems and the Poisson equation. Rates for the averaging principle when were obtained by several authors, e.g. Givon (2007) and Liu (2010). Röckner and Xie (2021) give rates for the fully coupled system with Hölder coefficients in all four regimes.
Let (fast) and (slow), . For small parameters tending to , with , the two-scale system (1.4) is
with , and independent Brownian motions .
Freezing gives the frozen equation (1.7), with generator , , and invariant probability measure . A function is centered if its -average vanishes for every . The standing assumptions are: (Aσ), uniform nondegeneracy of ; (Ab), ; (AG), uniform nondegeneracy of ; (AH), is centered; and (2.7), the analogue of (Ab) for , small.
The averaged coefficients of Regime 1 are and , and the averaged equation (2.9) is , .
Regularity is measured in weighted Hölder classes: (index in , in , polynomial growth in ), its bounded version , the time-dependent , the class of measurable functions of polynomial growth, and for test functions.
In Regime 1, and , assume , with , and . Then for every and ,
The result. The theorem gives a rate for the weak error of the averaging principle under Hölder regularity only, and the rate depends only on the regularity in the slow variable , not on . It covers the fully coupled case, in which the slow equation contains the singular drift , and it identifies the extra condition under which this drift averages out. For it reduces to the rate (Remark 2.5), optimal for . Error bounds of this kind are what heterogeneous multiscale methods need to be quantitative.
Formalizing it. The result is proved in the paper; nothing in it is machine-checked. A formalization needs an Itô calculus for weak solutions, the elliptic Poisson equation in with parameter (the companion mission's Theorem 2.1), and the parabolic Kolmogorov equation of the averaged SDE. The two fluctuation lemmas are stated for general centered functions and are reusable for other limit theorems.
The obvious argument writes through the Kolmogorov equation of the averaged SDE and Itô's formula, which leaves and . Both integrands are centered but only Hölder continuous in , so the standard corrector argument, which applies Itô's formula to the solution of the Poisson equation along , needs derivatives in and that do not exist. The term with is a central-limit-scale fluctuation, which is why its control needs the regime conditions. Existence and regularity of the averaged coefficients also have to come from the Poisson equation, since is not explicit.
Spaces are EuclideanSpace ℝ (Fin d). Coefficients are , a matrix, , a matrix. The Itô layer (Brownian motion, Itô integral, Itô processes, SDE solutions) is the published Peng1990.SMP.Stochastic. A solution of (1.4) is a weak solution: any filtered probability space, any Brownian motion for that filtration, any progressive process satisfying the integral equation. The theorem compares every weak solution of (1.4) with every weak solution of (2.9). The paper does not prove existence for (1.4), so the statement is conditional on solutions, as it is used in the paper. A sanity file shows the parameter hypotheses are consistent (, ) and that (2.7) holds for a bounded dissipative drift.
Committed conventions and readings of the page:
A formalization in which the expectations are junk Bochner integrals, the constant depends on , or a single strong solution is fixed would be a different and weaker statement; the posed statements rule these out.
Not posed: Regimes 2–4 of Theorem 2.3 and Lemma 4.4(ii)–(iv). The printed differs by a factor in the term from the generator used in the proof, so a faithful statement needs a correction that is left to moderation. Regime 2 needs the Poisson solution in the averaged drift. Lemma 5.2 is also not posed: as printed, solves (5.1) only for time-independent coefficients, and its class has time index above , which the paper's notations do not define. Contributions toward Itô's formula for these processes, the Poisson equation (companion mission 1) and parabolic Schauder theory are welcome.
A contextual bandit is a sequential decision problem: in each round a learner sees a context (a user's features, a patient's covariates), picks one of actions, and observes the reward of that action only. Applications include recommendation, dynamic pricing and adaptive clinical decisions. The difficulty is statistical and computational at once: the learner must explore to learn which action is best for which context, and the class of models it learns over is typically huge.
A long-standing question was whether contextual bandits can be solved optimally with nothing more than an offline regression oracle, a black-box supervised learning routine that fits a predictor of rewards to i.i.d. data. Earlier optimal algorithms either required a cost-sensitive classification oracle called many times per round (the "monster" of Agarwal et al., 2014) or an online regression oracle that must handle adversarially generated data (Foster and Rakhlin, 2020). Simchi-Levi and Xu (2022) answered the question with FALCON+, which calls an arbitrary offline regression oracle once per epoch, or times in total, and whose regret is governed by the oracle's estimation error.
Timeline:
There is a finite set of actions and a set of contexts. In round nature draws a context and a reward vector from a fixed unknown distribution ; the learner sees , picks and observes . The conditional mean reward is , and is an action maximizing . The regret after rounds is
An action selection kernel gives a probability distribution over actions for each context. The offline regression oracle takes samples and returns a predictor . It satisfies Assumption 2 with error function if, for every kernel , when the samples are i.i.d. with and , then with probability at least ,
FALCON+ runs in epochs given by a schedule . In epoch it sets and for ; it obtains by feeding only the data of epoch to the oracle (); and in every round of the epoch it plays
where maximizes . The epoch of round is .
If and for , then for every and , with probability at least ,
The paper states Theorem 2 as an bound; this is the explicit inequality its proof establishes, with the additive terms kept. It holds for every oracle, error function and schedule satisfying the hypotheses, so it is the shape of the result rather than a rate for a particular class.
In attack order: Lemma A.2 (each oracle call is accurate with probability ; the good event has probability ); Lemma A.3 (the kernel is induced by a randomized policy on ); Lemma A.4 (the conditional expected regret of a round is the implicit regret of ); Lemmas A.5 and A.6 (low predicted regret and bounded divergence ); Lemma A.7 (prediction error of implicit rewards on ); Lemma A.8 (true and predicted implicit regret agree up to factor 2 and ); Lemma A.9 (); Lemma A.10 in expectation; the Azuma display (A.10); and Lemma A.10 with high probability.
Theorem 2 makes contextual bandits reducible to offline regression with no loss in rate: for any function class with an estimation-error bound, plugging that bound into the theorem gives the regret. With empirical entropy this yields , matching the known lower bound, and for linear classes it improves the best known bound when (Examples 1–2 of the paper). The oracle is called once per epoch on i.i.d. data, so any off-the-shelf supervised learner can be used, with a guarantee transferred automatically.
Formalizing the result produces a machine-checked offline-to-online reduction, independent of the function class. The paper's result is proved, but it has no machine-checked proof; the platform has formal statements for the online-oracle algorithm SquareCB and for the classification-oracle algorithm of Agarwal et al., not for this reduction. The milestones isolate reusable facts about inverse-gap-weighted kernels (Lemmas A.3, A.5, A.6) and an epoch-wise induction pattern (Lemma A.8) that recur in later work on bandits and reinforcement learning with regression oracles.
The obvious argument fails at the regression step. A natural approach feeds all past data to the oracle, but those data are adaptively collected and not i.i.d., so an offline guarantee does not apply to them; FALCON+ uses only the previous epoch's data, which are i.i.d. given the past, and the analysis must make this conditional application of Assumption 2 rigorous on a product space (Lemma A.2). The second obstacle is that the oracle's error is measured under the kernel of the previous epoch, while regret is incurred under the current one. Transferring the error across epochs requires the divergence and the two-sided comparison of true and predicted implicit regret in Lemma A.8, proved by induction on epochs with exact constants; a one-sided bound does not close the induction.
Lean representation and conventions:
Fintype with the discrete σ-algebra. The paper claims Theorem 2 for arbitrary , but its detailed proof (App. A.1–A.6) is "under the condition that "; the uncountable case (App. A.7) is not formalized. No bound depends on .A trivializing formalization is ruled out: the goal is a bound on the realized regret of the run of Algorithm 2, whose oracle sees only samples of the previous epoch; it is not a bound for an algorithm that is handed or its population error, or that observes the full reward vector.
Infrastructure needed: conditional application of an i.i.d. guarantee inside a product measure (Fubini over Measure.infinitePi), Azuma–Hoeffding for bounded martingale differences (proved on the platform as bounded_diff_martingale_two_sided), and finite-sum algebra for inverse gap weighting. The kernel lemmas A.3, A.5 and A.6 are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal from the milestones.
Poisson equations for the generator of an ergodic diffusion are a standard tool in stochastic averaging, homogenization and diffusion approximation: to show that a fast ergodic component averages out in a slow equation, one writes the fluctuation as and applies Itô's formula to . This requires a solution whose regularity is controlled in two variables at once: the fast variable , in which the operator is elliptic, and the slow variable , which enters as a parameter.
Fix , a matrix field and a vector field on . The frozen operator acts on functions of with held fixed:
The Poisson equation (1.1) is for all , for each parameter .
The standing assumptions are:
Under these, for each the frozen diffusion has a unique invariant measure . Since constants solve , the equation is only solvable for centered right-hand sides, for every (1.3), and the solution is fixed by requiring it to be centered as well.
Regularity is measured in weighted Hölder classes. () means and , uniformly in . adds derivatives in , with a -Hölder top derivative. The subscript denotes the bounded version, and asks the same of together with growth bounds on and .
If (Aσ), (Ab) hold and with , , then for every centered there is a unique centered with . For some ,
and, for , .
The theorem supplies the corrector used in Theorem 2.3 of the same paper, the weak convergence rate of the slow component of a fully coupled multiscale SDE to its averaged limit. Its form, regularity in matching that of the data and no derivative of in , is what lets the rates depend only on the regularity of the coefficients in the slow variable. The transfer formulas (3.9)–(3.10) also show that averaged coefficients inherit the -regularity of , a question that comes up in every averaging or homogenization limit.
The result is proved in the paper. None of it is formalized: Lean and Mathlib have no fundamental solutions of non-divergence elliptic operators, no Schauder theory and no invariant measures of diffusions. The mission poses the statements, so that the proof can be built in layers and the parts that do not depend on the Gaussian kernel bounds (the transfer formulas given a solution, the induction in Steps 3–4) can be proved separately.
Existence and the estimates (2.1)–(2.2) rest on the probabilistic representation and on Gaussian bounds and ergodic decay for the fundamental solution of (Lemma 3.1, cited from Ladyzhenskaya–Solonnikov–Ural'tseva and Pardoux–Veretennikov II, Proposition 3). The coefficients are only Hölder in , so the Hessian bound needs the cancellation (3.3), not just a size estimate on . The obvious approach to -regularity, differentiating or in , needs derivatives of the invariant density in the parameter, which are hard to control. The paper's route, differentiating the equation and using the transfer formula to recenter, only works if the differentiated right-hand side is again centered. That centering is the content of Lemma 3.2.
EuclideanSpace ℝ (Fin d); , are fderiv and iteratedFDeriv ℝ 2 in , is iteratedFDeriv ℝ j in , with operator norms. -derivatives in the milestones are directional.Hemivariational inequalities were introduced by Panagiotopoulos in the 1980s to model mechanical problems whose energy functional is neither convex nor smooth: nonmonotone friction, adhesion, delamination and unilateral contact with nonmonotone multivalued laws. Where a variational inequality expresses the optimality condition of a convex energy, a hemivariational inequality expresses a stationarity condition of a locally Lipschitz energy through Clarke's generalized directional derivative. When in addition the admissible set depends on the unknown state, as in contact problems with a solution-dependent gap or in Nash-type equilibrium problems with coupled constraints, the problem becomes a quasi-hemivariational inequality.
Zeng, Migórski and Khan (SIAM J. Control Optim. 59 (2021)) treat a general form of this problem that contains a multivalued operator , a bifunction and a constraint map at once. Their existence theorem for it, Theorem 3.8, is the base of an optimal control result (Section 4) and of an application to a frictional contact problem in elasticity (Section 5). This mission formalizes the existence part, Sections 2 and 3 of the paper.
Let be a real reflexive Banach space with dual and pairing , and let , be real Banach spaces. The data are: a nonempty closed convex set ; a multivalued constraint map ; a multivalued operator ; a function ; a locally Lipschitz functional ; bounded linear operators and ; a functional ; and an auxiliary function .
For a locally Lipschitz , the Clarke generalized directional derivative and the generalized gradient are
Problem 1.1 asks for and such that and
Its solution set is . Fixing the constraint set gives Problem 3.3: find and with the same inequality for all ; its solution set is . The variational selection maps to the solution set of Problem 3.3 with replaced by ; its fixed points are exactly the solutions of Problem 1.1.
The hypotheses of the paper (p. 1250) are: has nonempty, compact, convex values and is upper semicontinuous; is -stably pseudomonotone with respect to , where and is weakly sequentially upper semicontinuous in the limsup sense (3.1); is convex and l.s.c. in its first argument, concave and u.s.c. in its second, and vanishes on the diagonal; has nonempty closed convex values and satisfies two Mosco-type conditions (HK); a bounded set meets every and, if is unbounded, a coercivity condition (3.2) holds at each point of . Theorem 3.8 adds that is compact, is convex, and whenever strongly and weakly (3.19).
Under all hypotheses of Theorem 3.8,
nonemptiness, boundedness and weak closedness of ; and its convexity when is convex. 4. Theorem 3.8 (i): the same characterization for Problem 1.1, with replaced by . 5. Two claims from the proof of Theorem 3.8 (ii): the graph of is sequentially weakly closed, and is bounded.
Theorem 3.8 is the existence result on which the rest of the paper rests: the optimal control problem of Section 4 minimizes over , and Section 5 casts an approximate static elastic contact model, with a multivalued normal compliance condition and a frictional law with slip-dependent friction coefficient, in the form of Problem 1.1 on a space of displacements. The theorem unifies several existence results for variational, hemivariational and quasi-variational inequalities: for single-valued , , , and , its Corollary 3.9 reduces to an earlier existence result for quasi-variational inequalities (Remark 3.10), and Theorem 3.4 removes the compactness of required in earlier work (Remark 3.6).
The results are proved in the paper. None of them, nor Clarke's calculus on a Banach space, nor Kluge's fixed point theorem, has a machine-checked proof to our knowledge. A formalization adds a checked version of a proof that combines a KKM-type fixed point theorem, Minty's trick for pseudomonotone multivalued operators, and a fixed point argument for the variational selection.
The obvious route to Problem 1.1 is to fix , solve the inequality on , and take a fixed point of the solution map. Two steps resist. First, the solution map is multivalued and its values are only weakly closed, so a Schauder- or Kakutani-type theorem in the norm topology does not apply; the fixed point theorem must work with sequentially weakly closed graphs, and the graph closedness of has to be proved by passing to the limit in inequalities in which converges only weakly while the test points must converge strongly. That passage uses the compactness of , the upper semicontinuity of , condition (3.19) and the Mosco-type conditions together. Second, in the "there exists " form of the problem the inequality is not stable under weak limits in , which is why the Minty reformulation and the stable pseudomonotonicity with the auxiliary function are needed.
All spaces are real normed spaces with CompleteSpace; is V →L[ℝ] ℝ with the operator-norm topology; reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual ℝ V. No inner product and no finite dimension is assumed. Multivalued maps are total functions V → Set _, constrained on only. Weak convergence means for every ; "weakly closed" is sequential weak closedness, which for the bounded sets and in a reflexive space agrees with weak closedness. Adjoints are composition: , . is a real Filter.limsup and is used only under LocallyLipschitz J. Every , infimum and limit in the hypotheses (, (3.1), (3.2), (3.19)) is written with explicit – quantifiers, so no default value of a real or can make a hypothesis vacuous.
Four corrections to the printed hypotheses are built in and stated in each item's note: the pairing in (3.2) is (the page's does not typecheck); is nonempty for ; the condition (3.2) assumed in Theorem 3.4 refers to a bounded set that meets ; and for Theorem 3.8 (ii) and the boundedness of , (3.2) in (HC0) holds uniformly in (one for each ), which is what the proof on pp. 1260–1261 uses. With (3.2) only at each fixed , as printed, can be unbounded; the counterexample is in the note of Theorem 3.8 (ii). Theorem 3.8 (i) and the graph-closedness of keep (HC0) as printed. A formalization in which may have empty values, may be empty or disjoint from , is a Hilbert or finite-dimensional space, a real default value makes the conditions on or (3.19) vacuous, or "bounded" or "weakly closed" is dropped from the conclusion, would be a different and weaker theorem.
The development needs Clarke's calculus on a Banach space (Proposition 2.5, which relies on the Hahn–Banach theorem), Eberlein–Šmulian or Kakutani's theorem on weak compactness of bounded closed convex sets in reflexive spaces, Mazur's lemma, a KKM-type fixed point theorem in Hausdorff topological vector spaces, and Kluge's fixed point theorem. These pieces are reusable beyond this mission: Clarke's calculus for every nonsmooth optimization statement on Banach spaces, and the fixed point theorems for variational and quasi-variational inequalities in general. Contributions of any of them, of alternative proofs, and of proofs of the milestones in any order are welcome.
Mean field control asks a central planner to steer a large population of interacting agents. Each agent's state follows a stochastic differential equation whose coefficients depend on the agent's own state and on the empirical distribution of the population; as the population grows, the system is described by a single McKean–Vlasov equation whose coefficients depend on the law of the solution itself. The planner's value is then a function of time and of a probability measure, and its dynamic programming equation, the HJB master equation, is a partial differential equation on the Wasserstein space of measures.
C. Wu and J. Zhang (Ann. Appl. Probab. 30(2), 2020) develop a viscosity theory for such master equations in a path-dependent setting and apply it to McKean–Vlasov control with closed-loop controls, i.e. controls that depend on the observed state path rather than on the driving Brownian motion. Closed-loop information is the natural one when the noise is not observable, and it is the information structure relevant for games; but the value function is then not known to be smooth, so classical solutions are out of reach. This mission formalizes the paper's §5: the value function of the closed-loop problem with piecewise constant controls is a viscosity solution of the HJB master equation.
Fix and a horizon . The path space is with the uniform norm, the canonical process is , and is its natural filtration. is the set of probability measures on with ; is the law of the stopped path . On the pseudometric is
with the 2-Wasserstein distance on laws of paths.
The data are a control set and coefficients , , , satisfying Assumption 5.1: measurability and adaptedness, boundedness of by , Lipschitz continuity of and uniform continuity of in , local uniform continuity in , and positive definiteness of .
An admissible control (5.3) is piecewise constant: for a partition , with -measurable. The controlled law agrees with on and solves, for a Brownian motion ,
The value function (3.20) is
and is the same supremum over the controls (5.12) whose pieces depend on the path before only through finitely many values .
The HJB master equation (3.22) is with , where
Viscosity solutions (Definition 4.4) are defined by test functions that satisfy a functional Itô formula on , where is the set of laws agreeing with on under which is a semimartingale on with drift and diffusion bounded by , and touch from above or below at on that set.
Under Assumption 5.1, is finite on and is a viscosity solution of (3.22).
The result characterizes the closed-loop value function through a PDE on the space of path laws without assuming any smoothness of . Combined with a comparison principle for (3.22), which the paper leaves open, it would identify the closed-loop and open-loop values (Remark 5.9). The regularity result (Theorem 5.7) is itself delicate: Example 5.6 shows that a natural restricted class of closed-loop controls produces a value function that is discontinuous in , and the piecewise constant class (5.3) is chosen to avoid this.
The theorems are proved in the paper; none of them is formalized. A formalization would supply a machine-checked path from a path-dependent McKean–Vlasov control problem to its HJB master equation, together with reusable statements on weak solutions of path-dependent McKean–Vlasov equations, their uniform moment bounds, and the dynamic programming principle in the Wasserstein space.
Definition 4.4 requires , and the central difficulty is continuity in . Closed-loop controls are functions of the observed path; changing the initial law from to changes the information available to the control, and when is degenerate a control adapted to cannot be written as a function of the -path. The obvious argument, transporting an -optimal control for along an optimal coupling of and , fails for exactly this reason (Example 5.6).
Time is and every statement quantifies over and . Paths are continuous maps with the sup norm and Borel -algebra; is the published WassersteinDRO.Duality.wassersteinDistance with . Brownian motion and Itô integrals are the published EthierKurtz.IsStandardBrownian and EthierKurtz.HasBrownianItoIntegral.
Committed conventions:
The test classes are not vacuous: constant functions satisfy every clause of the test-function class, and Assumption 5.1 holds for , , . A formalization that makes or the admissible set empty, or that lets be , does not prove the theorem.
Needed infrastructure: weak existence and uniqueness for path-dependent McKean–Vlasov SDEs with Lipschitz coefficients; Burkholder–Davis–Gundy-type moment bounds; measurable selection on Polish spaces; couplings and gluing on of a path space. The moment bound and the McKean–Vlasov well-posedness are reusable beyond this mission. Contributions to any milestone are welcome.
Master equations are partial differential equations whose state variable is a probability measure. They arise as the Hamilton–Jacobi–Bellman equations of mean field control problems, where a planner steers a large population through its distribution, and as the limit description of large games. Their basic computational tool is an Itô formula for functions of measures: if is a semimartingale with law at time , how does evolve? For functions on the Wasserstein space this formula is due to Buckdahn, Li, Peng and Rainer (Ann. Probab. 2017) and Chassagneux, Crisan and Delarue (arXiv:1411.3009), with the derivative in the measure introduced by Lions through the lifting to random variables.
Many models are path dependent: exotic options, rough volatility, and control problems with constant controls all lead to functions of the law of a whole path rather than of its time marginal. Wu and Zhang (Ann. Appl. Probab. 2020) extend the measure derivative and the Itô formula to this setting, following Dupire's functional Itô calculus (Dupire 2009). This mission formalizes §2 of their paper: the derivative of a function of a path law and the functional Itô formula of Theorem 2.7. It is the first of three missions on the paper; the other two treat viscosity solutions of master equations and McKean–Vlasov control.
Fix and . Continuous paths form with . Càdlàg paths form with the Skorokhod distance
the infimum over continuous strictly increasing bijections of . The canonical process is , with natural filtration ; is the path stopped at .
is the set of probability measures on with , with the Wasserstein distance whose cost is . The state space is with the pseudometric
where is the law of .
For the time derivative is the right derivative . The spatial derivative comes from lifting to on square-integrable path-valued random variables of an atomless Polish probability space: the Fréchet derivative of under the perturbation has the form . The second derivative is the pathwise (Dupire vertical) derivative of . consists of the continuous with continuous derivatives, bounded , and .
is the set of laws of Itô processes with , and square integrable.
For , and ,
The formula is the chain rule of calculus on path laws. It is what makes functions admissible test functions for viscosity solutions of path-dependent master equations, and what identifies the value function of a McKean–Vlasov control problem with a solution of its HJB master equation (§§4–5 of the paper, the other two missions of this series). Without it, the notion of viscosity solution in that paper has no link to the underlying dynamics.
The result is proved in the paper. It has no machine-checked proof: Lean's Mathlib has neither the Skorokhod space, nor Wasserstein spaces of path laws, nor a derivative with respect to a measure. Formalizing it would also produce a reusable Lean account of càdlàg path spaces and of the Lions derivative, both of which are absent today.
The obvious argument would expand along the time marginals of . That fails for path-dependent : the stopped laws do not change continuously when a path is perturbed after , and the perturbation of the derivative's definition leaves the space of continuous paths. This is why the paper passes to càdlàg paths and the Skorokhod distance. Any argument then has to control and its derivatives along laws of discontinuous paths, which is where the joint continuity of all derivatives in under and convergence of laws in become unavoidable. Separately, Theorem 2.2 must show that a derivative defined through one probability space is a deterministic function of the stopped path, and atomlessness of that space is essential to it.
Paths are functions on , constant after ; is C(Set.Icc 0 T, ℝ^d) with the sup norm, embedded in . carries the -algebra of the evaluations. Distances, sup norms and are -valued. A law in is given with an explicit representation: a filtered probability space, a standard Brownian motion with independent increments, progressively measurable bounded coefficients, and the Itô integral of the published EthierKurtz.HasBrownianItoIntegral. The goal holds for every representation of , and (2.20) is stated in drift form: , the stochastic integral having mean zero.
The class fixes together with its derivatives and states that they are the derivatives (2.7), (2.16), (2.18). It also requires and to be -adapted, a property the paper's has by Theorem 2.2. Without these clauses every continuous function would qualify, and (2.20) would be false. The printed is read as . The proof's computations are stated in dimension . Limits indexed by are stated for .
A complete development needs: the Skorokhod space and the fact that its Borel -algebra is the evaluation -algebra; Wasserstein distances on it; dominated convergence for path laws; and Itô's formula for the drift–diffusion representation. These are reusable well beyond this mission. Contributions to any milestone, or to these foundations as separate lemmas, are welcome.
The alternating direction method of multipliers (ADMM) solves problems of the form and is a standard tool in signal processing, statistics and distributed optimization (Boyd et al., 2011). For convex problems ADMM is known to be the Douglas–Rachford splitting (DRS) applied to a dual problem. Themelis and Patrinos (arXiv:1709.05747v4, SIAM J. Optim. 30(1), 2020) show a primal equivalence that holds without convexity: one ADMM step is one DRS step on the problem
where and are image functions (their Theorem 5.5). Their nonconvex DRS theory (Theorem 4.3) requires the first summand to have a Lipschitz continuous gradient. Convergence guarantees for nonconvex ADMM therefore rest on knowing when is smooth and with which constants. Section 5.4.2 of the paper answers this question in Theorem 5.13, the target of this mission.
Let be a matrix, viewed as a linear map with transpose and spectral norm , and let . The image function (Definition 5.1) is
the least value of on the fibre . It can be (empty fibre) or (unbounded below). Write for the set of minimizers on the fibre.
A differentiable is -smooth if , and -hypoconvex if is convex; is the class of -smooth functions (§2.2). For hypoconvexity is -strong convexity; for it allows nonconvexity.
The paper introduces smoothness relative to a matrix (Definition 5.12). A differentiable belongs to with constants if
whenever . The condition only concerns points whose gradient is orthogonal to , which includes every minimizer of on a fibre.
Finally, denotes the smallest nonzero singular value of a nonzero matrix (p. 5).
Let be surjective and lower semicontinuous, and suppose that for some the function is level bounded for every . Then is real-valued, -smooth and -hypoconvex on in each of three cases:
In the order the proof uses them: properness of image functions (Proposition 5.2(i)); lower semicontinuity of and nonemptiness of ; strict continuity of and nonemptiness of its limiting subdifferential; the subgradient transfer (Proposition 5.3); the identity (5.7) relating subgradients of to gradients of at fibre minimizers; strong convexity of image functions (Proposition 5.4); and the subdifferential characterization of smoothness (Lemma 2.1).
Theorem 5.13 is what makes the DRS convergence results of the paper apply to ADMM in practice: Theorem 5.6 of the paper assumes is smooth, and this theorem gives conditions on and under which that assumption holds, with explicit constants that enter the admissible penalty parameters. Case (i) is weaker than requiring itself to be : the paper's example , satisfies it with although is not globally Lipschitz. Case (iii) recovers the convex setting with a constant governed by the conditioning of . Propositions 5.3 and 5.4 and Lemma 2.1 are general tools of variational analysis that apply beyond this theorem.
The result is proved in the paper, with parts of the argument delegated to Rockafellar–Wets (Thms. 1.32, 9.13, 10.13) and to Nesterov's cocoercivity theorem. No machine-checked version is known to exist. A formalization would also need image functions, regular and limiting subdifferentials on , and parametric minimization, none of which Mathlib currently provides.
The image function is defined by an infimum, so smoothness of cannot be read off a formula. The proof goes through the limiting subdifferential: it shows that is lower semicontinuous and strictly continuous, so that is nonempty, relates each subgradient of to a gradient at a fibre minimizer, and then applies a subdifferential characterization of functions (Lemma 2.1). The obvious shortcut, an envelope or implicit-function argument that differentiates through the minimizer map , fails: need not be single valued or continuous in cases (i) and (iii). Limiting subgradients also require a compactness argument (uniform level boundedness) to pass from regular subgradients at nearby points to minimizers on the limit fibre.
Spaces are EuclideanSpace ℝ (Fin n), matrices are continuous linear maps with ContinuousLinearMap.adjoint as transpose and the operator norm as , and "surjective" is Function.Surjective. is real-valued; the image function imageFn is an EReal infimum over the fibre, and the conclusion asserts that it equals a real function that is -smooth and -hypoconvex. Regular and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff. The three cases are three separate implications, each with the constants printed in the theorem. In case (iii), is passed as a number with the hypothesis that is the least value of over unit vectors , which equals the smallest nonzero eigenvalue of for surjective . For this set is empty and case (iii) is vacuous.
The goal does not assume that is real-valued, differentiable or strictly continuous, nor that fibre minimizers exist outside case (ii). A statement making any of these assumptions would be trivial or circular. Definition 5.12 keeps its range guard; dropping the guard would turn case (i) into ordinary smoothness.
Three points differ from the printed text, and each is disclosed in the item concerned:
The definitions of this mission (image function, relative smoothness, strong convexity of extended-valued functions) are reusable for any analysis of ADMM or of marginal functions. Proofs of the milestones, of Lemma 2.1 as a standalone result, and supporting variational-analysis lemmas are all welcome.
Binary polynomial optimization asks for the maximum of a polynomial over . Linearizing each monomial by a new variable turns the problem into a linear program over the convex hull of a set of 0/1 points, the multilinear polytope of the hypergraph whose edges are the monomials. Global solvers such as BARON build polyhedral relaxations of this polytope at every node of their branch-and-bound trees, so valid inequalities that are as strong as possible, that is, facet-defining, translate directly into smaller root gaps.
Del Pia and Khajavirad introduced running intersection inequalities in The running intersection relaxation of the multilinear polytope (Math. Oper. Res. 46 (2021) 1008–1037, doi:10.1287/moor.2021.1121). They generalize the flower inequalities of the same authors (SIAM J. Optim. 2018), which are facet-defining when the support hypergraph is -acyclic, to support hypergraphs that are not. This mission formalizes the paper's sufficient condition for a running intersection inequality to define a facet (§2.4, Proposition 4) together with the structural results it rests on.
Timeline. Crama (1993) studied the standard linearization; Del Pia and Khajavirad (2017, Math. Oper. Res.) proved that the multilinear polytope is full dimensional and gave lifting theorems for facets; flower inequalities followed in 2018; running intersection inequalities and the facet conditions formalized here appeared in 2021.
A hypergraph has a finite node set and a set of subsets of of cardinality at least two. Its multilinear set is
and its multilinear polytope is .
A multiset of sets has the running intersection property if its elements can be ordered so that each , , is contained in a single earlier . Such an ordering defines and . A leaf of is an element that comes last in some such ordering.
Fix an edge (the center) and edges , , adjacent to (the neighbors), such that the multiset has the running intersection property. Choose an ordering of , and for each with a node . The running intersection inequality is
where is the number of connected components of the hypergraph . Its support hypergraph has node set and edge set . An inequality defines a facet of if it is valid and the face it cuts out is nonempty of dimension .
Assume
Then the running intersection inequality defines a facet of for its support hypergraph .
Lemma 1 (p. 1011, leaves and reorderings), Lemma 2 (p. 1011, components ), Proposition 1 (p. 1012, validity), and the full dimensionality of (cited on p. 1016 from [12]):
Corollary 2 (p. 1017): and for suffice. Proposition 2 and Corollary 1 (pp. 1013–1014): the multiset , hence the system of inequalities, does not depend on the ordering. Proposition 3 (p. 1014): necessary conditions for a facet of the running intersection relaxation .
Proposition 4 certifies a large family of facets of multilinear polytopes whose support hypergraphs contain cycles that flower inequalities cannot handle. Together with the lifting theorems of Del Pia and Khajavirad (2017), it yields sufficient conditions under which these inequalities define facets of the multilinear polytope of general hypergraphs (p. 1015); §2.5 of the paper reports that running intersection cuts reduce BARON's root-node relaxation gap on image-restoration instances. Proposition 3 and Example 1 show that condition 1 is necessary while conditions 2–3 are not, so the result is a sufficient condition and not a characterization.
The results are proved in the paper; none is formalized. A Lean development would provide the first machine-checked library for the running intersection property (orderings, leaves, the multiset of -sets), the connected-component count of Lemma 2, and the multilinear polytope as a convex hull with an exact dimension count, all reusable for the companion missions on the tightness of for kite-free -acyclic hypergraphs and its strictness otherwise.
Validity (Proposition 1) decomposes over the connected components of ; the facet claim does not, because a face of codimension one is a global object and the neighbors of different components, and the nodes shared between neighbors, interact in it. Conditions 2 and 3 are exactly where this interaction is controlled, and Example 1 of the paper shows that dropping condition 3 does not destroy facetness, so no simple equivalence is available to fall back on. Formally, three nontrivial ingredients have no Mathlib counterpart: the combinatorics of running intersection orderings (Lemma 1, Proposition 2), the count of connected components of a hypergraph with loops and parallel edges (Lemma 2), and the affine dimension of a convex hull of 0/1 points in a space indexed by nodes and edges.
Nodes form a finite type α; every hypergraph's space lives inside α ⊕ Finset α → ℝ, with the coordinates outside pinned to in the definition of , so is meaningful. Orderings are lists indexed from . The number of components is that of the 2-section graph on the node set. An inequality is given by its data: center, a set of distinct neighbors other than , an ordering of whose traces form a running intersection ordering of , and the choice ; the first sum runs over neighbors, so a node chosen for two neighbors has coefficient . "Defines a facet" requires a nonempty face and compares dimensions as , so the empty face can never qualify and no truncated subtraction occurs. The facet statement is about for the support hypergraph only, not for a larger host hypergraph, which would require the lifting theorems. The reading is used where the page's "for all " would otherwise be contradictory (Corollary 2, Proposition 3(i)); Lemma 2 is stated for lists of nonempty sets, which covers its use on .
Contributions welcome: proofs of the milestones, a reusable library for the running intersection property and -acyclic hypergraphs, and the full-dimensionality proof.
In a financial market with a single probability model, the Optional Decomposition Theorem describes the processes that can be dominated by trading. If a process is a supermartingale under every equivalent martingale measure, then it can be written as an initial value plus a stochastic integral against the stock price, minus an increasing process that represents consumption. El Karoui and Quenez proved it for diffusion models (SIAM J. Control Optim. 33 (1995)) and Kramkov for locally bounded semimartingales (Probab. Theory Related Fields 105 (1996)). It is the step that turns the superhedging price, a supremum of expectations over martingale measures, into an actual dynamic hedging strategy.
Model uncertainty replaces the single model by a set of probability measures that may be mutually singular. This happens, for example, when volatility is only known to lie in an interval. There is then no reference measure, "almost surely" becomes "quasi surely" (outside a set that is null under every model), and the classical proofs, which rely on one dominating measure, do not apply. Bouchard and Nutz (Ann. Appl. Probab. 2015, arXiv:1305.6008) built the discrete-time theory of this setting: no-arbitrage, the fundamental theorem of asset pricing, superhedging duality and, in §6, a nondominated optional decomposition. This mission formalizes that last result.
Timeline:
Fix a Polish space , a horizon and . Let for . Then is a single point and , and a point of is read as the first coordinates of a path. The -field is the universal completion of .
For each and each node a nonempty convex set of probability measures on is given, and its graph is an analytic set. The set of possible models consists of all products whose kernels take values in . A set is -polar if it is null under every . A property holds -quasi surely (q.s.) if it holds outside a polar set.
Stock prices are Borel. A strategy is predictable: is a function of the first coordinates. The wealth at time is
NA() holds if q.s. implies q.s. A martingale measure is a probability under which is a martingale. The set
contains those that are absolutely continuous with respect to some (written ). A function with values in is upper semianalytic if every set is analytic.
At one node , the increment defines a one-period market under , with its own no-arbitrage condition NA() and one-period martingale measures . The conditional sublinear expectation is
Let NA() hold and let be an adapted process such that is upper semianalytic and in for all and . Then the following are equivalent:
at every arbitrage-free node where q.s.
The decomposition is the dynamic counterpart of superhedging duality. Duality identifies the price . The optional decomposition, applied to the process of conditional superhedging prices, produces one strategy that superhedges under all models at once and a nonnegative increasing process recording the surplus. The proof works in a nondominated model with one strategy that is measurable in the universal completion, and this is what makes the theorem usable under volatility or model uncertainty, where no single model can be singled out. The equivalence also characterizes the processes that are supermartingales under every : up to a polar set they are exactly the wealth processes of strategies that consume.
The result is proved in the paper; no part of it has a machine-checked proof, on the platform or in Mathlib. Mathlib has martingales, conditional expectation and analytic sets. It has no quasi-sure analysis, no product of measurable selectors of a random set of measures, no conditional sublinear expectation and no superhedging. The mission produces a machine-checked development of the one-period-to-multi-period machinery of the paper (Theorem 4.5, Lemmas 4.6 and 4.10) and of the decomposition itself.
With one dominating measure, the classical proof works under a fixed equivalent martingale measure and uses conditional expectations and a single null-set structure. Here the measures in may be mutually singular, so conditional expectations under different disagree off their supports, and no countable family of measures controls all null sets. The proof has to work node by node, . Every object built at a node (the worst-case conditional expectation, a near-optimal measure, a hedging ratio) must then be glued back together measurably in . Borel measurability is not preserved by taking suprema over the random set . Upper semianalyticity is, but only together with measurable selection theorems for analytic sets (Jankov–von Neumann) and the universal completion. The first idea, which is to apply the classical theorem under each separately, fails. It gives one strategy per model, and in general uncountably many models cannot be aggregated into one strategy.
The Lean development uses the following conventions.
Fin t → Ω₁, and measures are Borel. -measurability is universal measurability, which is the published platform definition BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable.V t : (Fin t → Ω₁) → ℝ, so adaptedness is built into the type.H u is the paper's .EReal, with . Suprema over are taken in EReal.The increasing process must be adapted and nondecreasing on every path. Dropping monotonicity would make condition 2 trivially true, with for any . Integrability and supermartingale properties are always stated with explicit -integrability, so Bochner integrals of non-integrable functions cannot make a statement vacuous.
The development needs the following infrastructure:
These pieces are shared with the companion mission Arbitrage and Duality in Nondominated Discrete-Time Models I, which formalizes the superhedging theorem. Contributions to either side are welcome. The paper derives (ii) ⇒ (i) from Lemma A.1, a classical fact about local and generalized martingales under one measure, which is not posed as a milestone here.
Master equations are partial differential equations whose state variable is a probability measure. They arise as the dynamic programming equations of mean-field control problems, as the limits of large particle systems, and as the pricing equations of options on a whole population. Their coefficients and solutions are functions on a Wasserstein space, which is infinite dimensional, and classical (smooth) solutions are known only under strong regularity assumptions (Cardaliaguet–Delarue–Lasry–Lions 2019). A notion of weak solution for which existence, comparison and uniqueness can all be proved is therefore the basic missing tool.
C. Wu and J. Zhang (Ann. Appl. Probab. 2020) propose such a notion for parabolic master equations on the space of laws of continuous paths, in the spirit of the viscosity theory for path-dependent PDEs of Ekren, Keller, Touzi and Zhang (Ann. Probab. 2014). This mission formalizes its §4: the definition of viscosity solutions and the comparison principle that makes them unique.
Fix a horizon and a dimension . The canonical space is with the uniform norm , the canonical process is , and . is the set of probability measures on with ; is the law of the stopped path . The state space is with the pseudometric
where on laws is the 2-Wasserstein distance. A function has a time derivative , a path derivative and a second derivative , defined through a functional Itô formula along semimartingale laws.
The master equation (3.1) is
with a generator that is continuous in , Lipschitz in , and Lipschitz in in the averaged sense (3.2) of Assumption 3.1.
For , is the set of laws that agree with up to time and under which is a semimartingale on with drift bounded by and half squared diffusion bounded by . Test functions at are functions on touching from above or below there, (4.2). is an -viscosity subsolution (supersolution) if () for every such test function, and a viscosity solution if it is both for one (Definition 4.4). The Perron envelopes , of (4.17) are the infimum of piecewise classical supersolutions above and the supremum of piecewise classical subsolutions below .
Under Assumption 3.1 and , if is a viscosity subsolution, a viscosity supersolution, , the classes are nonempty, and
then on , and is the unique viscosity solution with terminal condition .
The comparison principle is what turns a definition into a theory: it gives uniqueness, it identifies value functions of mean-field control problems with the solution of their master equation, and it is the input of stability and convergence arguments for numerical schemes. Theorem 4.13 reduces well-posedness to condition (4.19), and the authors verify (4.19) in examples (§4.6) via Theorem 4.14. The compactness of (Lemma 4.1) is the device that replaces local compactness, which the Wasserstein space lacks; it is reusable for any viscosity theory over semimartingale laws.
These results are proved on paper. No machine-checked development of viscosity solutions on Wasserstein spaces, or of the path-dependent functional Itô calculus on laws, is known to exist. A formalization would produce a checked notion of viscosity solution for master equations, the compactness of bounded-characteristic semimartingale laws, and the comparison machinery, and would expose the points where the printed proofs are sketched (see below).
The obvious route, copying the finite-dimensional theory, fails at two places. First, the doubling-of-variables argument for comparison needs a penalization on the state space that is smooth and coercive; on under neither is available, which is why comparison is reached through partial comparison and Perron envelopes. Second, maxima of need not be attained on Wasserstein balls, which are not compact; the theory therefore tests only on , and Lemma 4.1 (via Zheng's tightness criterion for semimartingale laws and uniform integrability of ) is what makes the extrema exist. The printed proof of Theorem 4.13 opens with " is lower semicontinuous and is upper semicontinuous"; as printed the directions are swapped (an infimum of functions continuous in is upper semicontinuous in ), and the members of are only càdlàg in , so the continuity of needed for the conclusion requires an argument of its own.
Time is , and every condition is imposed only at , . is the Euclidean space, matrices are real matrices with the Frobenius norm, and . is the published WassersteinDRO.Duality.wassersteinDistance on laws of paths; Brownian motion and the Itô integral are the published EthierKurtz definitions. Membership in is the existence of a representation of as the law of an Itô process from time with , (§2.4). A object is a record of a function and three derivative functions, and the functional Itô formula (2.25) is required in drift form for every representation, which equals (2.25) because the stochastic integral has mean zero. Test sets encode "" literally, and the data of a test function at are its values at , . The Perron envelopes are extended-real infima and suprema over the classes (4.18); (4.19) is stated with a real-valued .
Two readings are fixed. Assumption 3.1(i) is continuity of for fixed continuous of linear growth. "" in Theorems 4.6 and 4.11 is replaced by the larger class it is used through (Remark 4.3(i)): data continuous on lying in for all , , , so those statements are at least as strong as printed.
The definitions cannot be satisfied vacuously: every test set requires a witness law in , the class contains the constants (checked in Lean), and a viscosity solution uses one for both halves. The semi-jets range only over -measurable continuous arguments of linear growth, as printed.
Contributions are welcome at every level: the moment bound (4.1) and Lemma 4.1 need tightness and uniform-integrability results for semimartingale laws on path space that Mathlib does not have; Theorems 4.7 and 4.9 are self-contained manipulations of the definitions; Theorems 4.6 and 4.11 and Proposition 4.12 need the compactness lemma and the Itô identity of test functions.
Games with many interacting agents, such as traffic participants, users of a shared communication channel or firms in a market, are rarely solvable exactly: a Nash equilibrium of an -player stochastic game requires each agent to track the whole population, and its computation grows with . Mean-field game theory replaces the population by its limiting distribution. A single representative agent faces a deterministic flow of state distributions, and consistency requires that this flow is the one the agent's own optimal policy generates. The equilibrium of this limit problem is then used as an approximate equilibrium of the finite game, with each agent acting only on its own state.
Most of this theory concerns risk-neutral agents, who minimize an expected cost. Saldi, Başar and Raginsky (arXiv:1808.03929; Math. Oper. Res. 2020) treat discrete-time agents with an exponential utility of the discounted cost, the classical risk-sensitive criterion that penalizes the variance of the cost as well as its mean. The paper proves two results: a mean-field equilibrium exists (Theorem 1, the first mission of this series), and the equilibrium policy is an approximate Nash equilibrium of every large enough finite game (Theorem 3, this mission). The risk-neutral counterpart is Saldi, Başar and Raginsky, SIAM J. Control Optim. 2018 (arXiv:1612.07878).
States lie in a Polish metric space , actions in a compact Polish space , and is the set of Borel probability measures with the weak topology. The model consists of a transition kernel , a one-stage cost , an initial law , a discount factor and a risk factor .
In the -agent game, the states are i.i.d. . At each time , agent draws from its Markov policy , and the next states are drawn independently from , where is the empirical distribution of the states. Agent 's cost is
A profile is an -Markov-Nash equilibrium if no agent can lower its by more than by switching to another Markov policy.
In the mean-field game, one agent faces a flow : , with cost . A mean-field equilibrium is a pair in which minimizes and is the flow of state laws that generates.
The hypotheses are Assumption 1 (bounded continuous with , weakly continuous , compact , and a moment function with and ) and Assumption 2. Part (a) of Assumption 2 asks that the moduli
tend to , where is the bounded-Lipschitz metric. Part (b) asks that the equilibrium policy be weakly continuous in the state.
For every there is such that, for every , the profile is an -Markov-Nash equilibrium:
The statement fixes no rate. It is the paper's main approximation result.
The milestones follow the paper's proof. The first seven work in an augmented model, whose state carries the accumulated discounted cost, so that the exponential criterion becomes a terminal cost . They are: Proposition 6 (the augmented model has the same finite-horizon costs); Lemma 5 (the augmented flow ); Proposition 7 (propagation of chaos, ); Proposition 8 (convergence of the augmented cost); Proposition 9 (propagation of chaos with one deviating agent); Proposition 10 (the deviating agent's state law); Proposition 11 (the deviating agent's augmented cost). The last three are stated in the original model: Theorem 4 (the finite-horizon limits (14)–(15)), Corollary 1 (the infinite-horizon comparison), and the first display of the proof of Theorem 3 (deviations may be restricted to weakly continuous policies).
Theorem 3 justifies the use of a mean-field equilibrium as a decentralized policy in risk-sensitive games with many players. The equilibrium is computed once, from a single-agent problem, and each agent uses only its own state, yet no agent of a large enough population gains more than by deviating. The result extends the risk-neutral approximation theorem to the multiplicative criterion. Because the exponential cost does not decompose over time, the risk-neutral argument cannot be applied directly: the proof first passes through the augmented model and a finite-horizon truncation.
The result is proved in the paper; none of it is formalized. The mission formalizes the statement and the proof's intermediate results. That requires the -agent law, a product of kernels driven by the empirical measure, built from Mathlib's Ionescu-Tulcea construction, and propagation of chaos for an interacting Markov chain on a Polish space. Alternative proofs of any milestone are welcome, as are quantitative versions of the limits.
The cost is the expectation of a product of one-stage factors, not a sum, so the convergence of the empirical measure gives no direct control of it. The paper therefore enlarges the state with the accumulated cost, and the finite-horizon limits must then be transferred back to the infinite horizon through a uniform tail bound. The coupling between agents runs through the empirical measure, which enters both the transition and the cost. Propagation of chaos (Proposition 7) is an induction over time that needs continuity of and in the measure argument uniformly in (Assumption 2-(a)) and a conditional variance bound. The deviating agent is not exchangeable with the others: its state law must be compared with that of a mean-field chain under its own policy (Proposition 10), uniformly over arbitrary sequences of deviations. Finally, a best response may be only measurable. The reduction to weakly continuous deviations, which the paper takes from its risk-neutral predecessor, is needed before any weak-convergence argument applies.
Lean namespace RiskSensMFG.Nash. The definitions are in four files: the model, policies, the single-agent law and the flow (Model); the mean-field equilibrium, , total variation and Assumption 2-(a) (Equilibrium); the -agent game (Game); and the augmented model (Augmented). Conventions:
ProbabilityMeasure with the weak topology and its Borel -field (not the Giry one), and is a Markov Kernel. The standing assumptions , and measurable are a predicate Model.Standing. Assumption 1 is stated in full, including the moment function, although the proof of Theorem 3 does not use parts (d)–(e).Fin N, and the paper's Agent 1 is index 0; limits in are taken along so that Agent 1 exists. The empirical measure of the empty configuration is set to and enters no statement.No hypothesis is vacuous: a sorry-free check exhibits a model satisfying the standing assumptions, Assumptions 1 and 2 and the equilibrium condition simultaneously, with . This rules out the trivial reading in which a non-integrable integrand makes every cost and every profile an -equilibrium. Theorem 1 (existence of the equilibrium) is the other mission of the series; here the equilibrium is a hypothesis.
In online allocation, requests arrive one at a time and each must be accepted or rejected on arrival, using a limited budget of resources. Revenue management, ad allocation and hiring all fit this pattern. A natural benchmark for an online policy is the prophet, or Offline: the decision maker who sees the whole arrival sequence in advance and acts optimally on it. The regret of a policy is the expected gap between Offline's value and the policy's value. Policies that track a fixed solution of a fluid relaxation lose on the order of (Proposition 1 of the paper), so the question is whether a simple adaptive policy can achieve regret bounded independently of and of the budget.
The simplest such problem is the multi-secretary problem: hire at most of sequentially arriving candidates, each drawn i.i.d. from finitely many ability classes. Arlotto and Gurvich (Stochastic Systems 2019) showed that a budget-ratio policy has regret bounded uniformly in and , using a martingale argument. Vera and Banerjee (SSRN 3158062; Management Science 2021) introduced the compensated coupling, a sample-path identity that expresses the regret of any online policy as the compensation Offline must be paid to follow it. They used it to prove constant regret for a simple re-solve-and-threshold rule, the Fluid Bayes Selector, with the explicit constant . This mission formalizes that result together with the compensated coupling it rests on.
A finite-horizon online decision problem has states , arrival types , actions , a transition function , a reward function , and a set of feasible actions in each state. Time is counted as time to go: decisions are made at , and is the type arriving at time-to-go . A standing assumption requires the best feasible reward in every state to be attained and to lie in a fixed bounded interval.
Given the whole arrival sequence, Offline's value obeys the Bellman equation
An online policy chooses a feasible action at each time from the arrivals observed so far. Starting from it produces a state process and a value , and its regret on a path is . An action is satisfying for Offline at when it attains the Bellman maximum. The disagreement set is the set of paths on which it does not, and the marginal compensation is the amount by which it falls short.
In the multi-secretary problem there are classes with rewards and arrival probabilities , i.i.d. over time (multinomial arrivals). The state is the remaining budget . Accepting needs , earns and lowers the budget by one; rejecting earns nothing. With , the Fluid Bayes Selector (Algorithm 2, in the rounded form of Appendix B.3) behaves as follows at time-to-go with budget . If it rejects. Otherwise it always accepts class , and it accepts a class iff .
For every horizon and every initial budget ,
where and . The goal keeps the paper's explicit constant: neither nor appears in it.
The result. Theorem 2 gives the best known regret bound for the multi-secretary problem with an explicit, simple constant. The compensated coupling (Lemma 1) holds for any finite-horizon problem with exogenous arrivals. It turns a regret bound into a bound on disagreement probabilities, and the paper reuses it for online packing, online matching and general online allocation, and for Bayes Selectors whose disagreement probabilities are only estimated.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of the compensated coupling, is known to us. The mission produces a reusable formal model of finite-horizon online decision problems with an Offline benchmark. It also produces a formal compensated-coupling identity that applies to any policy, and a binomial Chernoff–Hoeffding bound in elementary finite-sum form. Each of these supports other missions on prophet benchmarks, resolving heuristics and network revenue management.
Comparing the online policy with one fixed offline solution does not work: Offline's optimal decisions change with every future arrival, and tracking a single offline plan only gives regret of order . The compensated coupling avoids this by re-coupling Offline to Online at every step. That shifts the difficulty to two places. The first is an exact description of when Offline's Bellman equation disagrees with the policy, which involves ties between equal rewards and the boundary budget . The second is a bound on the conditional probability of disagreement that is uniform over all budgets. That conditional probability is a binomial tail evaluated at a budget that is itself random but independent of the remaining arrivals.
Lean conventions:
Fin n with [NeZero n], and Lean index 0 is the paper's class .Antitone r, so ties are allowed.θ t is the arrival at time-to-go t, and the counts include the current arrival.The policy is the rounded rule of Appendix B.3, which always accepts class when the budget is positive. Algorithm 2 read literally would reject class when , and the bound , which excludes class , is proved for the Appendix B.3 rule. The policy is defined by its explicit thresholds and not through an arbitrary optimal solution of the fluid LP, because with tied rewards that LP has several solutions.
A formalization that replaced the expectation by a Bochner integral of a non-measurable function, or Offline by a fluid relaxation, would make the bound trivial or a different theorem. Both are excluded by construction.
Contributions are welcome at every level: proofs of the milestones, a proof of Eq. (18) from Mathlib's sub-Gaussian machinery, and lemmas computing Offline's value in the multi-secretary problem (the top- rewards among the remaining arrivals), which are reusable beyond this mission.
Large networks of neurons are often modelled as systems of coupled stochastic differential equations: each neuron carries a low-dimensional state (a membrane potential and recovery variables, as in the FitzHugh–Nagumo model), receives synaptic input from the other neurons with a transmission delay, and is perturbed by noise. Because the number of neurons is large, one studies the mean-field limit: as the population grows, each neuron should evolve independently of every other fixed neuron, driven by its own noise and by an averaged population input. This asymptotic independence is called propagation of chaos, and the limiting single-neuron equation is a McKean–Vlasov equation.
Mehri, Scheutzow, Stannat and Zangeneh (arXiv:1805.01654v3, Ann. Appl. Probab. 2020, DOI 10.1214/19-AAP1499) prove propagation of chaos for a model combining features that earlier work treated separately: monotone (one-sided Lipschitz) local dynamics, general path-dependent delays, Lévy-type jump noise, spatial structure with several subpopulations, and a random environment (disorder). Earlier mean-field results for neuronal networks were obtained under global Lipschitz assumptions (Quiñinao and Touboul 2015; Touboul 2014, two papers), for locally Lipschitz coefficients (Baladron, Fasoli, Faugeras and Touboul 2012, with the clarification note of Bossy, Faugeras and Talay 2015) and for one-sided Lipschitz coefficients (Luçon and Stannat 2014; Touboul 2012); with jump noise, only under global Lipschitz or gradient-type local dynamics (Andreis, Dai Pra and Fischer 2018). This mission formalizes the paper's second main result, Theorem 1.8. The first mission of the series formalizes the well-posedness of the McKean–Vlasov equation (Theorem 1.5).
Neurons sit at positions in a bounded set , partitioned into measurable subpopulation regions . The -th network consists of a finite set of positions, and neurons of subpopulation carry the weight . The state of the neuron at solves the network equation (1)
where are evaluated at and at , the last argument being the path of the presynaptic neuron over the delay window . The noises , are independent Brownian motions, , independent compensated Poisson random measures with intensity , and is a random disorder with expectation . Each neuron starts from a path on .
Given a finite measure on with , the McKean–Vlasov equation (6) describes a continuum of neurons , , whose interaction is , with an independent copy of (and likewise for , ). The mean-field equation (5) for a neuron of the network has the same form, with replaced by a process that starts from the same and is driven by the same noises as neuron of the network, while the interaction is computed from the law of the solution of (6).
Under Hypothesis 1.6 and the chaotic initial condition (the are independent, with distributed as for ),
The theorem asserts convergence without a rate, which is the stable form of the result.
The proof also uses Lemma 1.4 (the moment bound for solutions of (6)), which is a milestone of the first mission of this series and is not restated here.
Theorem 1.8 justifies replacing a large, spatially structured network of delayed, jump-driven neurons by a single McKean–Vlasov equation indexed by position. The limit is the object on which neural field models and their bifurcation analysis are built; the theorem identifies the hypotheses on the spatial distribution of neurons (condition (10): the neuron counts per cell, normalized by the weights, converge to ) under which that replacement is valid in a random environment.
The result is proved in the paper; no machine-checked proof exists. Formalizing it requires a coherent Lean layer for strong solutions of delay SDEs with jumps, mean-field interaction terms, Poisson random measures with product marks, and independence of countable families of drivers. The intermediate bounds of §3 are explicit and quantitative, and each is a self-contained target.
The interaction of the network is an empirical average over finitely many neurons, while the limit uses an expectation over a continuum of positions. The difference splits into three errors of different nature: a fluctuation term, whose control requires that the limit processes of distinct neurons be independent (which holds only because each is driven by its own noise and starts from an independent initial condition); a spatial discretization error within each cell, which requires a quantitative regularity of the solution of (6) in the position variable; and a counting error between the neuron counts and the measure . A naive comparison of the network with (6) directly, without the coupled processes of (5), gives no pathwise relation and does not work. The coefficients are only one-sided Lipschitz in the local variable, so moment bounds must come from monotonicity rather than from global Lipschitz estimates, and the disorder enters the constants through exponentials whose integrability is exactly assumption (H6).
Positions are EuclideanSpace ℝ (Fin k), states EthierKurtz.SDEState d, and subpopulations Fin P (0-based). Neurons carry labels in ℕ with an injective position map, so is a finite set of labels and is countable. Brownian integrals are the published EthierKurtz.HasBrownianItoIntegral per coordinate, compensated jump integrals the published JacodTodorov10.LLN.HasCompInt, and all Poisson measures of the network form one (𝓕_t)-Poisson random measure on a product mark space. Integrands are cut off after the horizon . All expectations, suprema and the disorder expectation are taken in , so no statement can be satisfied by a junk value of a real integral or supremum; (H6) states the boundedness of its supremum explicitly. The copy enters only through its law: the solution of (6) lives on its own probability space and the mean-field terms are expectations over it.
Conventions and corrections, all disclosed in the items: the theorem is stated for every family of solutions of (1), (5) and (6) (hypotheses), not for "the" solutions; (H1′) is printed with and is read as ; carries the expectation of (17), which the display on p. 20 omits; the second Gronwall inequality on p. 21 (constant ) drops a factor of and is not posed; the coefficients' path argument carries the product σ-algebra; the filtration satisfies the usual conditions (Appendix A); the solution class of (6) is a bound for every time. The solution notions are not trivializing: every stochastic integral is tied to the given noise by a published predicate, the mean-field terms are computed from the solution of (6) itself, the limit processes share the network's noise and initial conditions, and the finite constant of the integrated bound is quantified before and .
Reusable beyond this mission: the strong-solution predicate for jump SDEs with delay, the noise predicates for countable families of drivers, and the network and mean-field interaction terms. Contributions toward a stochastic calculus for these predicates (Itô's formula for with jumps, Gronwall arguments with left limits) are welcome.
Sinkhorn distributionally robust optimization (Wang, Gao and Xie, arXiv:2109.11926) hedges a learning or decision problem against distribution shift. It minimizes the worst-case expected loss over all distributions within an entropically regularized optimal-transport distance (the Sinkhorn distance) of a nominal distribution . Strong duality, the subject of the first mission of this series, reduces the problem at a fixed Lagrange multiplier to minimizing an objective of nested-expectation form,
A logarithm sits between the two expectations, so a mini-batch of samples gives a biased estimate of and of its subgradients, and stochastic gradient methods do not apply directly. Problems of this shape are known as conditional stochastic optimization (Hu, Chen and He 2020, 2021; references [54], [55] of arXiv:2109.11926v5). The paper's algorithmic contribution is a biased stochastic mirror descent (BSMD) for this objective, with two subgradient estimators and explicit complexity guarantees. This mission formalizes that guarantee, Theorem 2 of the paper.
The decision lives in a closed convex set . A norm on satisfies with (Assumption EC.1), and has dual norm . A distance generating function is continuously differentiable on and -strongly convex with respect to . It induces the Bregman divergence and the prox-mapping .
The data are a probability measure and a Markov kernel on a measurable space , fixed , and a loss . Assumption 2 requires three things: (I) is convex in ; (II) it is -Lipschitz in for the Euclidean norm; (III) for . Write .
The level- approximation replaces the inner expectation by an average of i.i.d. draws:
Its sample subgradient is . The SG estimator is . The RT-MLMC estimator draws a level with probability and returns , where is the antithetic difference between the level- subgradient and the average of its two half-sample versions. BSMD iterates , , with a fresh sample at every step.
For let , , and . With the SG estimator and
or with the RT-MLMC estimator, and
the average of the iterates is δ-optimal:
Theorem 2 converts into sample complexities: draws from with either estimator. From , SG needs draws and RT-MLMC . The -rate matches the lower bound for general convex stochastic programming. This is what makes Sinkhorn DRO computationally competitive with empirical risk minimization, and it is the inner oracle of the paper's bisection search over (Theorem 3, not part of this mission). Lemma EC.7 is a reusable statement in its own right: mirror descent with uniformly biased stochastic subgradients loses only an additive .
The result is proved in the paper, partly by citation: the bias and variance bounds are attributed to Hu et al. and the BSMD bound to Nemirovski et al. To our knowledge none of it is machine-checked. The mission produces a self-contained Lean proof and, along the way, a formal mirror-descent analysis with biased oracles and an MLMC variance bound for log-sum-exp functionals.
The obvious route is to treat as an unbiased stochastic subgradient of and cite standard stochastic mirror descent. That fails because is a subgradient of , not of . Closing the gap requires the uniform bias bound of Lemma EC.6 (I), a second-order Taylor bound for on against the variance of a sample mean. The RT-MLMC bound requires the antithetic cancellation in to be exhibited explicitly. The naive bound gives no decay in , and the estimator's second moment then grows like instead of . Finally, the expectation over a run of dependent iterates needs a careful product-measure argument: the iterate is a function of , and is independent of it.
Representation. is EuclideanSpace ℝ (Fin d). The mirror norm is a function with the norm axioms and Assumption EC.1, and its dual norm is a real supremum over its unit ball. is a gradient within .
Prox-mapping. It is a map characterized by its argmin property on .
The kernel. is an arbitrary Markov kernel. This contains the paper's Gibbs kernel , which the BSMD analysis never uses.
Subgradients. "" always means a selected subgradient; no differentiability of the loss is assumed. and are given in explicit chain-rule form, the same selected subgradients in every block.
Randomness. A run of length is driven by i.i.d. samples under Measure.pi. The RT-MLMC sample is , with level reading the first draws.
Measurability and integrability. The prox-mapping and the subgradient selector are measurable. Every expectation in a conclusion comes with its integrability, which rules out a vacuous reading in which a non-integrable quantity has expectation .
Explicit forms of the paper's . The paper writes and ; its proof (p. ec20) yields the hyper-parameters stated above. They are fixed in the goal, not quantified existentially:
The max 1 guards enforce the paper's and . The sample counts are not stated as Lean claims, since they follow by construction: per iteration, one draw from , plus draws from for SG or in expectation for RT-MLMC. Remark EC.1 prints the latter as .
Two corrections to the printed text.
Contributions welcome. Proofs of the milestones. A reusable Lean development of stochastic mirror descent with biased oracles. The MLMC bias and variance lemmas for of a sample mean. A follow-up mission on the bisection search (Theorem 3).
Distributionally robust optimization (DRO) hedges a decision against uncertainty in the data distribution. It minimizes the worst-case expected loss over an ambiguity set of distributions around a nominal one, typically the empirical distribution of the data. Ambiguity sets built from the Wasserstein (optimal-transport) distance are standard in operations research and machine learning, because they contain distributions with supports different from the nominal one. A known drawback is that the worst case is attained at discrete distributions, which is unrealistic when the true distribution is continuous.
Wang, Gao and Xie (arXiv:2109.11926v5) replace the Wasserstein distance by the Sinkhorn distance, the entropically regularized optimal-transport cost of Cuturi (NeurIPS 2013). Their main theorem is a strong duality result: the infinite-dimensional worst-case problem over a Sinkhorn ball equals a one-dimensional convex minimization. This mission formalizes that theorem.
Timeline:
Let be a measurable space. The data are:
For a probability distribution , the Sinkhorn distance (Definition 1, with reference measures and ) is
where is the set of couplings with these marginals. The primal value is the worst-case expected loss over the Sinkhorn ball,
The dual problem uses three more objects. The kernel distribution is . The adjusted radius is . The dual value is
where the objective at is .
Assumption 1 requires:
Condition 1 asks for some with for -a.e. .
Under Assumption 1:
(III) If , then when the dual objective is finite at some , and otherwise.
(IV) If and Condition 1 holds, then is the unique dual minimizer if and only if
The milestones are the numbered lemmas of the paper's proof, in the order the proof uses them:
The result. Theorem 1 turns a supremum over an infinite-dimensional set of distributions into a scalar convex program. That program can be solved by first-order methods using only samples from and from the kernels , which is the basis of the paper's algorithm (Section 4). The proof also constructs the worst-case distribution: it is absolutely continuous with respect to , not discrete. Theorem 1(IV) says exactly when the ambiguity constraint is binding. The finite-support conic reformulation (Corollary 1) and the closed form for linear losses (Example 1) both follow from the theorem.
Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. Formalization adds two things. First, it pins down the extended-valued conventions: , and all take values in , and the paper does not specify how undefined expectations and the objective are treated. Second, it checks every case of the proof, including the degenerate ones. Doing so has already corrected two statements; see Formalization scope.
Weak duality (Lemma 1) is Lagrangian relaxation plus the Gibbs principle. The difficulty is the reverse inequality . Interchanging the supremum over distributions with the infimum over requires a minimax theorem. The usual minimax theorems need compactness or semicontinuity in the distribution variable. The paper's setting has neither: is an arbitrary measurable space, is only measurable and may be , and is arbitrary. So a minimax theorem cannot be applied directly.
The proof instead constructs near-optimal primal distributions from the dual minimizer. This needs three separate cases:
Each case needs integrability facts about in which and interact. Disintegrating couplings (Assumption 1(IV)) and making the extended-valued expectations meaningful are a further source of work in Lean.
All values (primal value, Sinkhorn distance, dual objective) are EReal. Expectations are the published DupacovaWets.Consistency.expect: , with lower Lebesgue integrals in and the convention . The Bochner integral appears only in , which every theorem assumes finite.
Further conventions:
essSup f ν, not as a limit. Logarithms are ENNReal.log, so and ; .withDensity measure. Families are Markov kernels on all of .Hypotheses added to the page:
"" is read as "-a.e.". "" is read as " is the unique dual minimizer".
Corrections to the paper:
No statement involves an constant.
A formalization that lets an undefined Sinkhorn integrand evaluate to (Mathlib's ) is ruled out: it would put every distribution into the ball and make the theorem trivial. The combined integrand and the convention exclude this.
A complete development needs:
The first two are reusable well beyond this mission. Contributions toward any milestone, and toward these general lemmas, are welcome.
Classical arbitrage pricing fixes one probability measure describing the market and asks for the cheapest way to dominate a payoff -almost surely. When the model itself is uncertain, this choice is not available: a trader who only trusts a family of possible models wants a hedge that works under every one of them. Two literatures meet here. Robust (model-independent) finance studies hedging that must hold for all paths, as in the martingale-optimal-transport approach to option bounds (Beiglböck, Henry-Labordère, Penkner, 2013). Nondominated model uncertainty studies families with no single reference measure, as in the quasi-sure analysis of Denis–Martini (2006) and the volatility-uncertainty literature. Bouchard and Nutz (2015) give a discrete-time framework that contains both extremes (all measures on a path space; a single measure) and prove the fundamental theorems and superhedging duality for it.
Timeline of the dominated and robust predecessors:
Fix a horizon and a Polish space . Paths are , and holds the first coordinates. Information at time is the universal completion of the Borel -field of .
For each and history , a nonempty convex set of probability measures on describes the possible laws of the next coordinate. Its graph must be an analytic set. The set of models consists of all products whose kernels choose . A property holds -quasi surely (q.s.) if it holds -a.s. for every .
There are stocks with Borel prices and options , Borel on , bought or sold at time at price . A semistatic strategy consists of a predictable and a vector ; its terminal gain is
No-arbitrage NA() says that a gain which is q.s. nonnegative is q.s. zero. The superhedging price of a claim is
The dual objects are the martingale measures , meaning for some . Under the stock is a martingale and for all ; they form the set . Given a weight , set . Expectations of arbitrary measurable functions use the convention with .
Let be a random variable with , let NA() hold, and let be upper semianalytic with . Then
and some satisfies -q.s.
The milestones follow the paper's proof:
The superhedging theorem identifies the robust price of a claim as a supremum of linear prices. This turns a hedging problem into an optimization over measures, which is how robust option bounds are computed in practice. Remark 1.4 of the paper gives another consequence: every martingale inequality follows from a pathwise inequality . The first and second fundamental theorems make the nondominated framework a complete analogue of the classical theory. NA() is equivalent to and sharing their polar sets, and replicable claims are those whose price is the same under every martingale measure.
All results are proved in the paper. None of them, nor the classical dominated discrete-time FTAP, is formalized in Lean or Mathlib as far as is known. A formalization produces machine-checked statements of the model (analytic random sets, products of universally measurable kernels, quasi-sure analysis) and proofs of the fundamental theorems on top of it. Alternative arguments and extensions (portfolio constraints, infinitely many options) are also welcome.
There is no reference measure. Two dominated tools therefore fail. Closedness in cannot be applied, because convergence must hold quasi surely. A Hahn–Banach separation in a single space cannot produce martingale measures either. The paper argues one period at a time instead and glues the periods together measurably. That gluing is where the work lies. The one-period dual value and the one-period hedge must depend measurably on the history , but the value function of a Borel claim need not be Borel. The argument therefore runs in the class of upper semianalytic functions and needs measurable selection theorems for analytic sets. A recursion that tries to keep everything Borel breaks down at the first step.
Fin t → Ω₁ with [PolishSpace Ω₁] [BorelSpace Ω₁]. Measures are Borel measures, and -measurability is universal measurability. The published definition BertsekasShreve.AnalyticSelection.Measurability is reused for this.ProbabilityMeasure with the weak topology. is generated by Borel Markov kernels lying in almost surely; this is the paper's equivalent formulation on p. 4.H u is the paper's , a universally measurable function of the first coordinates.EReal. Expectations of non-integrable functions are the extended expectation . Prices are EReal infima with , and suprema over are EReal suprema.Two encodings would trivialize the mission and are excluded. Replacing by an arbitrary set of measures drops the product structure that the theorems need. Bochner integrals for would return on non-integrable claims and make the duality meaningless. Neither encoding is used.
A complete development needs:
The selection and kernel infrastructure is reusable well beyond this paper, for instance in dynamic programming on Borel spaces. Contributions of these foundations are welcome.
Policy gradient methods are the main family of reinforcement learning algorithms that search directly over a parameterized class of stochastic policies , , by stochastic gradient ascent on the expected discounted return. They underlie REINFORCE, actor-critic methods and their deep-learning descendants. The return is a nonconvex function of , and the gradient is available only through Monte Carlo samples of trajectories, so the basic question is what the iterates of such a method converge to.
Classical analyses of actor-critic algorithms (Konda and Tsitsiklis, 2003) use the ODE method of stochastic approximation and assume that the gradient estimate is unbiased. In the infinite-horizon discounted setting, a trajectory of finite length cannot by itself produce an unbiased sample of the gradient. Zhang, Koppel, Zhu and Başar (arXiv:1906.08383, SIAM J. Control Optim. 58(6), 2020) resolve this with random horizons: drawing the trajectory lengths from geometric distributions makes the resulting estimate exactly unbiased and almost surely bounded. They then prove convergence of the resulting random-horizon policy gradient (RPG) algorithm with the supermartingale convergence theorem, an optimization argument that also yields rates. This mission formalizes that first part of the paper (§2–§4 and App. A.1–A.4). The paper's later results on escaping saddle points are not part of it.
A finite Markov decision process is a tuple : finite state and action sets, transition probabilities , rewards and a discount factor . A stochastic policy gives a probability vector on at each state. Its value and Q-function are the expected discounted returns from a state, respectively a state-action pair.
A parameterized policy assigns to each a policy . Fix an initial state . The objective is
The score function is . The discounted state-occupancy measure is , and .
Assumption 3.1 asks for and for a differentiable policy whose score exists, is -Lipschitz in and is bounded in norm by . Two constants recur below:
The RPG algorithm (Algorithm 3) works as follows at the current iterate :
Assumption 4.1 is the Robbins–Monro condition , .
Under Assumptions 3.1 and 4.1, almost surely
and almost surely every cluster point of satisfies . The page states the conclusion as "", where is the set of stationary points. Read literally, that asserts convergence of , which fails when has no stationary point at all (one state, two actions, a softmax policy). The goal states what the proof on p. 30 concludes.
With constant stepsize and Assumption 3.1 only, for every ,
The theorem shows that Monte Carlo policy gradient, with a sampling scheme that can be implemented from simulated trajectories alone, behaves like an exact stochastic gradient method on a smooth nonconvex objective. It needs no ODE approximation, no two-timescale critic and no assumption that the estimate is unbiased: unbiasedness is proved (Theorem 3.4). The same estimates give the finite-time bound of Corollary 4.4 and are the starting point of the paper's second part, which adds perturbations to escape saddle points.
To our knowledge none of these results has been machine-checked. The mission's work is to formalize the known proof: the infinite-horizon policy gradient theorem with a vector parameter, the smoothness bound with its explicit constant, the exact law of the random-horizon estimator and its moments, and the supermartingale argument. The formal statements also repair three misprints of the source: the conclusion of Theorem 4.2, the tail of (A.22), which is read as , and the of Corollary 4.4, which is replaced by its explicit form (A.37).
Each step of the argument is standard on paper. The work is in the parts that the paper treats in one line:
PolicyValue, QFunction, OccupationDist, IsPolicy, IsTransitionKernel). is EuclideanSpace ℝ (Fin d), and is Mathlib's gradient.rpgLaw θ is the law of , built from the geometric horizons, the trajectory probabilities and EstQ. A run is a filtered probability space carrying and with on every path, adapted, and the conditional law of given equal to rpgLaw θ_k.rpgLaw would assume Theorem 3.4 and turn the goal into generic SGD; that encoding is ruled out. A sorry-free example shows that the run hypothesis is satisfiable and that rpgLaw is a probability measure.Tendsto of the partial sums to . "Cluster point" is MapClusterPt.rpgLaw. These are reusable for every Monte Carlo policy gradient analysis.