Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The Turán problem asks for , the largest number of edges in an -vertex graph with no copy of a fixed graph . For even cycles the answer is still not known in general: Bondy and Simonovits proved in 1974, and the order of magnitude is known to be sharp only for .
The generalized Turán problem replaces edges by copies of another graph : how many copies of can an -vertex graph contain if it has no copy of ? Its systematic study was started by Alon and Shikhelman (arXiv:1506.03807, 2016). Gerbner, Győri, Methuku and Vizer (arXiv:1712.07079, J. Combin. Theory Ser. B, 2020) treat the case where both and the forbidden graph are cycles. This mission formalizes their Theorem 11, the case , , which is the one case of the paper where the asymptotics, including the leading constant, are determined exactly for every .
Timeline:
All graphs are finite and simple. For graphs and , is the number of copies of in : the number of subgraphs of isomorphic to (unlabelled copies). is the cycle on vertices. A graph is -free if it has no subgraph isomorphic to (not necessarily induced). The generalized Turán number is
In Lean, vertices are Fin n, is Mathlib's cycleGraph a, is G.copyCount H, the -free condition is CycleFree {2 * k} G, and is exCyc n H A.
The proof works with the following objects, all defined in the mission's definitions file. The codegree of two vertices is their number of common neighbours. A pair of distinct vertices is fat if it has at least common neighbours. A copy of with vertices in cyclic order has the two opposite pairs and ; it is a fat if both opposite pairs are fat. A greedy run processes the fat 's in an arbitrary order and picks from each one of its four edges that has been picked the fewest times so far; the multiplicity of an edge is the number of times it is picked. is the complete bipartite graph with classes of sizes and (bipGraph n a).
For every ,
The is a sequence depending only on . At the statement says .
The result. Theorem 11 gives the exact leading constant for the maximum number of four-cycles in a graph without a -cycle. The extremal number of edges of such a graph is only known up to a constant factor, and only for is even its order known; counting four-cycles instead of edges turns the problem into one with a clean answer, attained by the unbalanced complete bipartite graph . The same upper bound on four-cycles is used again in the paper's Theorem 10, on the number of 's in -free graphs.
Formalizing it. The theorem is proved in the paper; it has not been formalized. A complete development needs counting of four-cycles through codegrees, the greedy multiplicity bookkeeping of §4.1, an argument producing long cycles in graphs with many fat four-cycles, and the Bondy–Simonovits theorem, which is itself not in Mathlib. The milestones isolate each of these; Theorem 1 is a stand-alone classical theorem of independent value.
The non-fat four-cycles give the main term directly. The difficulty is that fat four-cycles can a priori be numerous: a dense bipartite graph has of them. One must show that -freeness forces them down to , which is . The argument that bounds the non-fat ones does not transfer: a fat pair can lie in arbitrarily many four-cycles as an opposite pair, and nothing a priori bounds the number of fat pairs by less than . The bound must instead come from the global absence of , which is a statement about long cycles, while the objects being counted are short ones; Claim 2 is where the two meet, and its bookkeeping (new vertices must avoid the current cycle, and the four-cycles that fail to extend it must be outnumbered) is the core of the proof. The upper bound then still rests on the Bondy–Simonovits theorem, whose proof is a substantial argument of its own.
Graphs are SimpleGraph (Fin n) (or a general finite vertex type for the per-graph milestones). Copies are unlabelled (copyCount); a labelled count would be 8 times larger for . is an sSup over naturals; with forbidden lengths at least 3 the set is nonempty and finite, so it is a true maximum, which a sorry-free sanity file in the workspace checks. Landau notation is in with fixed first: is a real sequence chosen before and the graph, with the equality holding for all large , and the of Theorem 1 is an explicit constant chosen before and the graph. The constant is computed in .
Statements that are trivially true are ruled out: the goal states both the upper and the lower bound as an equality, the maximum is not a junk sSup, copies are unlabelled, constants and functions are fixed before the graph, and the forbidden family is exactly .
Two hypotheses differ from the page, both in Claim 2. The paper's standing graph is -free, which would make Claim 2 vacuous (its conclusion at is a ); the milestone assumes instead the property its proof uses, that any vertices have at most common neighbours. It also assumes that the edge is picked at least once, which follows from the multiplicity bound when and is needed for the base case at . The fat-four-cycle milestone states the explicit bound that the proof establishes, rather than the obtained after Theorem 1.
Contributions welcome: proofs of any milestone; a formal proof of the Bondy–Simonovits theorem, reusable well beyond this mission; general lemmas on counting four-cycles via codegrees and on copies in complete bipartite graphs.
An equation driven by fractional Brownian motion can respond to a rapidly varying coefficient even when that coefficient has no useful pointwise limit. Hairer and Li study this issue for fractional Brownian motion with Hurst index above one half. Their Section 3 isolates a deterministic averaging statement: if the time antiderivatives of the coefficients approach those of a limiting coefficient in a suitable negative Hölder norm, the solutions approach the limiting solution in probability. This statement supplies a common target for averaging models whose fast variables have very different origins. The authors use it later with mixing fast processes, and also present a quasi-periodic example. The result and its role in the paper are stated in Hairer and Li, Section 3.
The problem sits at the boundary of two familiar views of differential equations. A pathwise Young equation is defined from individual sufficiently regular paths, whereas the available estimates for the oscillating coefficient and the fractional Brownian driver involve probability and conditional expectation. The mission records the precise point where these descriptions meet. It treats the published article, rather than a preprint, and targets its Theorem 3.13.
An -dimensional fractional Brownian motion with index is a centered Gaussian process with independent coordinates and covariance
The paper works with a two-sided process and . It uses a version whose sample paths are locally -Hölder for every . The mission names that version condition separately, because the covariance law alone does not select particular sample paths. The relevant past sigma algebra at time is generated by increments with . These conventions come from pp. 1826 and 1831–1832 of the article.
For a path on , write for its homogeneous Hölder seminorm and for its supremum norm. The norm on is . A Young integral is the limit of left-point sums over partitions of as the largest cell shrinks to zero. A Young solution from is an -Hölder path satisfying its integral equation at every time, with value at time zero. Here means bounded, twice continuously differentiable maps with bounded derivatives through order two; means -Hölder in time with values in . These are the paper's conventions on pp. 1829 and 1835–1838.
The negative Hölder bound means that the time antiderivative of has increments bounded by , and that the difference of those increments at spatial points is bounded by . Both bounds apply on the time window in question when . This is equation (3.12) in the article. It measures cancellation over time; it does not require itself to be small.
The goal is the part of Theorem 3.13. Let be , let the limiting be autonomous and in , and suppose . The exponents satisfy , , , and . For Young solutions with the same starting point,
the target is
The milestone list follows the statements used around this target: the Hölder composition estimate of Lemma 2.1, the RKHS estimate of Lemma 3.3, the fractional Brownian integral estimate of Lemma 3.4, the stochastic sewing lemma of Lemma 3.5, the Young case of (3.18) from Lemmas 3.10 and 3.12, the Kolmogorov inclusions (3.24), and the deterministic stability estimate of Lemma 2.2. Each is a separate formal theorem. The authors' proofs follow their statements in Sections 2 and 3 and the Appendix; Lemma 3.5 is quoted from Lê, Theorem 2.1 without proof in the article.
The target gives convergence of entire solution paths in a Hölder topology, in probability. In the paper, this lets a model-specific estimate of the negative Hölder distance be used to conclude convergence of the corresponding dynamical system. Theorem A is obtained by adding such an estimate for a stationary mixing fast process; the deterministic statement here isolates the part independent of that model. These uses are described in Sections 1 and 3.
The published paper proves the result. This mission asks for machine-checked proofs of the stated Lean theorems. Its reusable work would include a pathwise Young integral over arbitrary partitions, Hölder norms that retain the value , a two-sided vector fractional Brownian motion interface, and stochastic estimates for time-dependent integrands. The goal and milestones in this proposal are statements with proof placeholders; the local build checks their types, not their proofs.
Pointwise control of is unavailable: a rapidly oscillating function can be large at most times and still have small time antiderivatives. Applying a pathwise Young stability estimate directly to therefore leaves a coefficient norm that need not tend to zero. The integral estimate must connect cancellation measured by with bounds on the driven equation. The dependence on the past of the fractional Brownian motion makes this step more delicate than an estimate for a deterministic integrand. The required estimates and their domains appear in Lemmas 3.4–3.12.
Time is for the two-sided driver; coefficient and solution assertions use with . State spaces are finite-dimensional real Euclidean spaces. The goal takes from the standing setting of Section 3.1, and it assumes the locally Hölder version of described on p. 1826. The solutions are required almost surely to satisfy the Young equation from the same . This requirement fixes the processes to the equations; the convergence claim cannot be obtained by choosing arbitrary paths. Probability of the norm event uses the measure of that set, and the conclusion is convergence in probability in the full norm.
The Lean definitions use for path and process seminorms, so unbounded suprema are not replaced by a default real value. The negative Hölder hypothesis uses real bounds instead of an infimum that could be meaningless on an empty class. The Young integral quantifies over every monotone partition and the mesh limit of its left-point sums. The fBm definition includes Gaussianity, means, and every cross-coordinate covariance; its path version is explicit. Interval integrals in the coefficient bound are applied to time-continuous coefficients in the goal. Lemmas 3.4 and 3.10 use the increment filtration, the case needed for this theorem.
The paper's Lemma 2.2 needs a common initial value for its homogeneous-seminorm estimate; the formal statement includes it and records the printed issue. The paper writes the limiting coefficient with a time argument but uses an autonomous coefficient in (3.23), which the goal adopts. This proposal covers the equation. The final extension in Theorem 3.13 and the conditional-expectation estimate (3.19) remain outside its current items. Contributions that close these gaps, or supply a general conditional Wiener integral matching the article's notation, would extend the development.
An -year term assurance pays a benefit if the insured person dies in one of the first policy years. It can pay only once. This matters when calculating the second moment: claims in different years cannot both occur, so the cross-products between them are zero.
Actuarial Mathematics I established finite expected present values, second moments and variances for general collections of contingent payments. This mission applies those results to one life and a fixed-term death benefit. It proves the familiar term-assurance formulas from reusable death-year events, rather than treating them as isolated actuarial notation.
Let be a probability space and let be a measurable curtate future lifetime: the number of complete future years lived before death. For , define the event of death during policy year by
Each event is measurable. The events are pairwise disjoint: if , then .
Fix a policy term and a constant annual discount factor . A unit benefit is payable at time if death occurs during year , for . Its random present value is
When , the sum is zero. The implementation uses the previously published `ActuarialValuation.presentValue` definition with the schedule of death-year events, reusing the general valuation machinery. The theorem statements allow any real , so the finite algebra also holds beyond the economic setting . The positive discount factors customary in the source are a special case.
The capstone proves these three identities together.
Expected present value:
Second moment:
Variance:
The second-moment simplification comes from the mutual exclusivity of distinct death-year events, not from independence. In the general double sum from Actuarial Mathematics I, every off-diagonal intersection of death-year events is empty, leaving a single sum.
The milestones proceed from measurability of each death-year event to disjointness across years, vanishing products of distinct death-year indicators, the finite present-value representation, the expected value, the second moment and the variance. The proposal gives each mathematical statement and Lean target type separately. The capstone combines the three moment identities for the same , , and .
The project uses the existing `ActuarialValuation` namespace and imports published Mission I results where they apply. All dates are annual, and benefits are payable at the end of the year of death. Multiple lives, benefits payable immediately on death, stochastic discounts, select-life models and whole-of-life infinite sums are outside the scope of this capstone.
A complete proof provides a reusable one-life mortality event model and a verified finite-term insurance valuation formula. The model can support a later mission on pure endowments and endowment assurances, where survival-to-term events complement death-in-term events, and another on temporary annuities, where survival events are nested rather than disjoint.
The results also make it straightforward to compare the traditional actuarial single-sum variance formula with the general dependent-cashflow theorem proved in Mission I.
The main mathematical source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 2 §2.4.3 for curtate future lifetime, Chapter 3 §3.1.1 equation (3.4) for disjoint-event moments, and §3.2.2 equation (3.8) for term-assurance present value, mean and variance.
These established actuarial formulas are not new mathematical conjectures. The contribution is a precise formal link in Lean from a curtate-lifetime model to the general contingent-payment valuation layer.
The death-year set must be shown measurable from the measurability of . The disjointness arguments must also cover degenerate cases such as . The generic second-moment theorem uses an ordered double sum. The proof must remove only terms justified by , retain the diagonal terms and use the correct end-of-year exponent .
All formal declarations are written for Prove2Me's pinned Mathlib revision `0df444a360eaa60ab8c11dca51a86af692955474`. No local Lean compiler is used. Any private preflight compilation, if needed, is performed through Prove2Me's remote system.
Principal component analysis (PCA) asks for the -dimensional affine subspace that best fits a cloud of points in in the least-squares sense. When is very large, or the points arrive as a stream or are spread over many machines, one wants to replace the data by a small summary on which the cost of every candidate subspace can still be evaluated, up to a factor . Such a summary is a coreset. Coresets for the -subspace problem are the building block of the streaming and distributed PCA and projective clustering algorithms of Feldman, Schmidt and Sohler (SIAM J. Comput. 49(3), 2020), whose sizes depend on and only, not on or .
For linear subspaces (through the origin) the paper's Theorem 17 gives a deterministic coreset of points read off the singular value decomposition. Data are rarely centred, though, and subtracting the mean before the computation does not survive the union of coresets with different means (p. 616). Section 4 of the paper repairs this: Theorem 19 gives a coreset for affine -subspaces whose points already carry the mean, at the price of doubling the size and weighting the points. This mission formalizes Theorem 19.
A data set of points in is a matrix whose rows are the points. For a nonempty set and a point , . The cost of is
and for weights on the rows of the weighted cost is . The squared Frobenius norm is .
A singular value decomposition (SVD) of is a factorization with and orthogonal and rectangular diagonal with nonnegative, nonincreasing diagonal entries . keeps the first diagonal entries and sets the rest to ; the -rank approximation is (Definition 1).
The mean row is and the centred matrix is , whose rows are .
Algorithm 1, subspace-Coreset, sets , returns the matrix of the first rows of (all other rows are zero), the weights , and .
Algorithm 2, affine--subspace-Coreset, runs Algorithm 1 on , obtaining with , and returns
together with .
Let , and , and let be the output of Algorithm 2 for any SVD of . Then , , , and for every affine -dimensional subspace of ,
Theorem 17 rests on Corollary 16 and Claim 3 of the paper; those are milestones of the companion mission Turning Big Data into Tiny Data … I and are not posed again here.
The result. Theorem 19 gives a deterministic summary of weighted points and one scalar that preserves the cost of every affine -subspace within , for arbitrary data, with no assumption on the mean. Because its points carry the mean, coresets of different data sets can be merged, which the merge-and-reduce streaming constructions of the paper's later sections need. Any -approximate PCA solution computed on the coreset is then a -approximate solution for the full data.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any coreset theorem, exists on the platform. A complete development would produce the cost identities for sums of squared distances to linear and affine subspaces in Lean, the effect of centring and orthogonal translation on these costs, and the use of the SVD truncation as a summary, all of which are reusable for other PCA, low-rank approximation and projective clustering results.
The obvious construction, centring the data, computing the linear coreset of the centred data and adding the mean back, fails: the linear coreset need not have mean , and translating a subspace by changes the cost of a point set by a multiple of that depends on the number of points (p. 617). The paper's construction has to match both the mean and the total weight of the original data while keeping the linear-subspace guarantee, and the formal proof has to carry this through the reduction of an arbitrary affine subspace to a linear one plus an orthogonal translation. Beneath it lies Theorem 17, which needs the SVD-based estimate of the companion mission (Corollary 16) and the passage from the -row matrix to the nonzero rows of . Distances to subspaces in Lean are infima over sets, so the identities for an orthonormal basis of must themselves be established.
Matrix (Fin n) (Fin d) ℝ, read as points of EuclideanSpace ℝ (Fin d). is Metric.infDist. Linear -subspaces are Submodules of finrank ; affine ones are AffineSubspaces whose direction has finrank , and is AffineSubspace.mk' t L. The SVD and are the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every statement holds for an arbitrary SVD; none is chosen.Games with many interacting players appear in economics, epidemiology and network engineering: firms competing in a market, individuals deciding whether to vaccinate, agents in a social network choosing an effort level. When every player interacts with every other player symmetrically, mean field game theory replaces the finite game by a limit with a continuum of players. Real interactions are rarely symmetric: who influences whom is described by a network, and large networks are described in the limit by a graphon (Lovász, Large networks and graph limits, 2012).
Graphon games combine the two ideas. Parise and Ozdaglar (2018) studied deterministic graphon games with continuous strategy sets. Carmona, Cooney, Graves and Laurière (2019) introduced idiosyncratic random shocks, giving a stochastic graphon game in which each player's state is perturbed by independent noise, and proved existence, uniqueness and stability of Nash equilibria as well as convergence of finite network games to the graphon limit. This mission formalizes their existence theorem (Theorem 3.15).
The players form the interval with Lebesgue measure . Each player chooses an action ; a strategy profile is a function , defined up to -null sets.
A graphon is a symmetric, Borel-measurable function with . It acts on through the graphon operator
A state map and a noise law on define the state of a player who takes action , feels aggregate , and receives shock . Assumption 1 asks that and that has mean zero and a finite second moment.
The aggregate felt by the players under a profile is the solution of
A player choosing against aggregate pays . Assumption 4 asks that be continuously differentiable and -strongly convex uniformly in , and that be -Lipschitz in . Assumption 5 asks that be bounded: for some finite . The best response is the unique minimizer of .
A Nash equilibrium is a profile such that, for -a.e. player and every action ,
The statement fixes no constants and asserts no uniqueness.
The existence theorem holds under mild hypotheses: unlike the uniqueness result of the same paper (Proposition 3.17), it needs no smallness condition linking , and . Boundedness of the state map takes its place. Existence of a graphon equilibrium is the starting point for the paper's §4, where graphon equilibria are shown to be limits of equilibria of finite network games and to yield -Nash equilibria for them.
The result is proved in the paper; no part of it is machine-checked. A complete formalization yields reusable pieces beyond this mission: square-integrable kernel operators on with their operator norm, the Hilbert–Schmidt compactness of such operators, Lipschitz dependence of minimizers of uniformly strongly convex functions on a parameter, and Schauder's fixed-point theorem on a Banach space, which is not in Mathlib.
A contraction argument does not apply: the best-response-of-aggregate map is Lipschitz with constant , which may exceed under the hypotheses of the theorem. Existence therefore rests on a compactness fixed-point theorem in the infinite-dimensional space . That requires compactness of the integral operator , which Mathlib does not provide for kernel operators, and Schauder's theorem itself, which Mathlib does not have. A bounded convex set in is not compact, so Brouwer-type finite-dimensional arguments do not transfer directly.
All statements live in the namespace GraphonGames.Existence and share one definitions file.
unitInterval with volume. Profiles and aggregates are functions with MemLp _ 2 volume; equalities between them are almost-everywhere equalities.Trivializing encodings are excluded: the operator norm is not a real supremum that could collapse to ; an equilibrium must come with its aggregate solving (6), be square-integrable, and beat every action for almost every player; and no norm is converted to a real number where it could be infinite.
The results of §4 (Theorems 4.3, 4.7, 4.9 on finite network games) and the uniqueness and stability results (Proposition 3.17, Theorem 3.20) are not posed in this mission. Contributions welcome include Schauder's fixed-point theorem, the compactness of Hilbert–Schmidt integral operators on , and the contraction argument behind Proposition 3.1.
An online decision maker often sees information about a customer, patient, or request before choosing an action. A bandit with covariates models this setting when the reward of every available action is initially unknown and only the reward of the chosen action is observed. A method must learn which action works best for which covariates while paying for exploratory choices. Perchet and Rigollet studied this problem for smooth reward functions and measured how quickly a policy can approach the performance of an oracle that knows every arm's mean reward Perchet and Rigollet, 2013.
A fixed grid divides the covariate space at one resolution everywhere. It can spend pulls distinguishing arms in regions where their difference is already large, while leaving too few observations in regions where they are close. Adaptively binned successive elimination (ABSE) instead refines a region only while several arms remain plausible there. The paper proves a regret rate controlled jointly by the smoothness of the reward functions and the probability of encountering near ties. Its Theorem 5.1 is the target of this mission.
There are arms and covariates in the unit cube , with . At time , the policy sees , chooses an arm, and sees that arm's reward. The random vectors consisting of the covariate and all potential arm rewards are independent across times. Covariates have a common probability law with a density between constants . Every reward lies in ; for arm its conditional mean given is . The paper does not require the complete reward vectors to be identically distributed across time. These conventions come from §3.1, pp. 10–11.
At , write . Write for the largest mean strictly below , and set when every arm ties. The difference is the positive gap wherever a genuinely suboptimal arm exists. The smoothness condition requires for every arm, with the Euclidean norm, , and . The margin condition, with , , and , says
These are the assumptions defining the paper's class §3.2, pp. 12–13.
ABSE starts with the whole cube. Each live dyadic cell runs a copy of successive elimination on its inherited arms. One round pulls each remaining arm once. After a complete round, an arm is eliminated if its empirical mean falls more than twice the radius below the largest empirical mean, where is the cell's side length and uses . The cell splits after its specified stopping round if it has at least two active arms and is below the maximum depth . Each child receives the survivors. The policy takes as parameters and uses the current covariate and rewards it actually observed Policy 3, p. 22.
The goal is the finite- part of Theorem 5.1, p. 22. Fix , , , with , , and . There is one constant , depending on these parameters but not on , or the machine, such that for every , every and every machine of the class,
Here is ABSE and is its cumulative regret against an arm of maximum conditional mean at each covariate. The goal asserts the shape of the rate with an unspecified constant, which is the paper's form.
In attack order:
The result provides a performance guarantee for a policy that adapts its spatial resolution to observed evidence, under a class of nonparametric reward functions. It permits a direct comparison with a fixed-bin policy under the same smoothness and margin conditions. The paper proves the rate and discusses optimality in a minimax sense when §5, pp. 22–27. This mission asks for a machine-checked proof of the stated finite- regime; the Lean goal and milestones are currently open statements, so the paper's proof is the mathematical source rather than a completed formal proof.
A completed development would make the stochastic model, adaptive policy, cell geometry, and concentration estimates reusable for other contextual bandit analyses.
The main difficulty is the feedback loop between decisions and observations. A cell receives samples only when the covariate lands there, and its available arms depend on eliminations in its ancestors. Applying an ordinary concentration inequality to a fixed sequence of arm rewards does not by itself justify the bound at these random birth and stopping times. The formal proof must track the inherited active sets and the samples collected after each birth, then combine local error bounds across the tree. The appendix's maximal inequality controls a range of round counts; the regret argument also uses the small probability of covariates with nearly tied arm means §5, pp. 23–27 and Lemma A.1, p. 28.
Lean uses EuclideanSpace ℝ (Fin d) and a probability measure on its unit cube. The lower density bound ensures every valid dyadic cell has positive probability, so its conditional mean is defined by a real quotient. A consistent half-open boundary assignment turns the paper's cells, which are specified up to Lebesgue-null boundaries, into a partition on every path. The policy is a recursive state machine: at time it receives , chooses an arm from its prior state, and updates with only the reward of that arm. It does not receive the unknown means or any unobserved potential reward. The existential constant in the goal is quantified before , , the sample space, and the machine.
The finite- goal includes . The printed theorem omits it, although the proof uses it. Without it, a two-arm machine with constant means and has regret from the policy's first exploratory round, while the printed bound tends to zero when is large. The clause reads the margin condition as , the limit of for , because the page does not define it. The (5.3) milestone uses : the printed ordinary logarithm can be nonpositive at a finest cell, while the left side is a positive integer. The cell parameter and bursting after a full round follow Policy 3 and the proof where nearby prose or pseudocode differs. Lemma A.1 adds and , both implicit on the page. The constants and are existential and placed after the class parameters, because the page's explicit omits the margin constant .
The probabilistic error displays (5.6)–(5.9) and (5.11)–(5.14) are not milestones. They are statements about the events and , which the page leaves undefined for cells that are never born or never finish rounds. The decomposition (5.8) also leaves out arms of that were eliminated at an ancestor of . A faithful encoding of these events is welcome as a contribution.
A complete proof needs measurable recursive policies, conditional expectations and independence, dyadic-cell volume and nesting facts, concentration for arm observations at adaptive times, and sums over tree depths. Contributions establishing these interfaces and the paper's intermediate bounds are welcome. The result must apply to every machine in the stated class. Each of the following would change the theorem: a policy that reads the unknown or unobserved rewards (the oracle has zero regret), a constant chosen after the machine, a covariate law that is not a probability measure on the cube, Hölder continuity in the sup norm instead of the Euclidean norm, or dropping the density lower bound (cells of zero mass would make a junk value). The paper's proofs are in §5 (pp. 23–27) and its Appendix (p. 28).
Retailers set prices and stock levels without knowing how demand responds to price. They must learn the demand curve from their own sales while still earning money, which is the exploration–exploitation trade-off of dynamic pricing with learning (den Boer 2015). Two features of practice make the problem harder than the textbook bandit. First, demand is censored: when the shelf runs empty, the firm sees only its sales , not the demand . Second, firms change prices rarely, because of menu costs and customer reaction, so a policy may change its price at most times over the whole horizon (Cheung, Simchi-Levi and Wang 2017).
Chen, Chao and Wang study a firm facing both features at once, in a parametric model where the demand distribution is known up to a parameter. For the well-separated case they give an algorithm, Algorithm-I, whose regret grows as , and they show that no admissible policy does better in general. This mission formalizes the upper bound. A companion mission formalizes the lower bound.
A firm sells one product over periods . At the start of period it holds inventory (with ). It chooses a price and an order-up-to level with , and the order arrives at once. Demand then has probability mass function on , where and the parameter lies in , . Unmet demand is lost, and the firm observes only the sales . Leftover stock carries over, . Each unit left over costs and each lost sale costs . The single-period expected profit is
For each , is an optimal price, , and the clairvoyant value is .
A policy's decision in period may depend only on past decisions and past sales. The regret of a policy is
The family is well-separated (Definition 1) if for every price the pmfs , , are pairwise distinct.
Algorithm-I splits the horizon into stages of lengths for , with . Stage uses one price and the order-up-to target . The target equals the planned level , raised by when so that the sales carry information. At the end of the stage the algorithm computes the censored-data maximum-likelihood estimate (5). It then sets the next stage's decisions to a maximizer of (6). It changes its price at most times.
Under Assumption A (regularity of and of near the true ), Assumption 1 (Fisher-information bounds, a positive lower bound on the pmf, strict monotonicity of ), Definition 1, and the condition that every optimal order-up-to level exceeds , there is such that for all large
The constant may depend on the model, the true parameter and the algorithm's inputs. The rate is the content.
The upper bound shows that a budget of price changes costs only a regret even under censoring. With of order the rate drops to logarithmic (Theorem 3 of the paper). Together with the matching lower bound (Theorem 2), it identifies the exact price of limiting price changes in this model. Theorem B1 is a general transfer principle, from a large-deviation bound on an estimate to a optimality gap of the plug-in decision. It allows continuous and discrete decisions together and needs no unique optimizer. It is reusable for any parametric learning problem with that structure. Proposition 1 is a large-deviation bound for maximum likelihood from censored, dependent, non-identically distributed data. The paper notes that such results were not previously available in the statistics literature.
The results are proved in the paper's appendices. None of them has a machine-checked proof. A formalization would check the regret decomposition (23), the stagewise bookkeeping with ceilings, and the large-deviation argument for the censored MLE. It would also make the reading of several loosely stated steps exact (see Formalization scope).
The obvious argument plugs a consistent estimator into the optimizer and bounds the regret by the estimation error. It fails twice. The error of is of order , so a Lipschitz bound on the profit would give regret of order per stage, which is too large. The rate of Theorem B1 needs the first-order condition at an interior optimum and the exact gap between optimal and suboptimal discrete levels. Second, the data are censored and dependent. The censoring level depends on carried inventory, which depends on past demand and on past prices. The classical large-deviation results for maximum likelihood assume i.i.d. uncensored samples (Borovkov 1998) and do not apply. Proposition 1 needs a separate argument that the inventory target is reached in most periods with high probability.
The model is encoded with a scalar parameter. , and are as above. The pmf is positive exactly on and sums to one, and is allowed. The expected profit is built from these sums. is the finite maximum for a price selection , not a real supremum. Periods are 0-based in Lean, while stages keep the paper's indices. Expectations and probabilities are sums over demand paths weighted by , the law of the path under the algorithm, taken in . Every regret summand is nonnegative.
Algorithm-I reads demand only through sales. Step 2's arg max is any maximizer of the censored product likelihood, which exists by compactness. Step 3's arg max is , any maximizer of , together with the price of Assumption A(iii). This is the decision the proof of Theorem B1 analyses. Proposition 1's "large enough " is read as "large enough , uniformly in the stage and in ". Theorem B1 is stated for a scalar price and level and a parameter in .
Three hypotheses are added and disclosed. Differentiability of in is presupposed by Assumption 1. Finiteness of the mean demand is needed for (4) when . The condition is needed because Step 1 defines the target only for . "The optimal order-up-to level exceeds " is read for every optimal level.
A trivializing formalization is ruled out. Regret and probabilities are path sums of nonnegative terms, not Bochner integrals that vanish on non-integrable inputs. is a real power. The hypotheses are jointly satisfiable: a Bernoulli instance with , , , satisfies all of them, together with explicit selections, and this has been verified in Lean.
A complete development needs the following:
Theorem B1 and the model definitions are reusable for the paper's later results (Theorems 3, 5, 6), which repeat these arguments. Contributions to any milestone are welcome, including alternative proofs of Proposition 1.
Life insurers and pension schemes promise cashflows whose payment depends on future events. A term assurance pays if the insured dies within a stated period. A pension pays when a member survives to an instalment date. A contingent survivor pension may continue after the member dies. These liabilities differ in the events triggering payment, but share one mathematical operation: discount the amounts payable and aggregate them to obtain a random present value. Expected present value is used in premium setting and liability valuation, while the second moment and variance quantify how much the discounted liability can vary.
The open textbook Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, §3.1, introduces uncertain discounted cashflows using indicators, and derives their expected values in equation (3.3). Its treatment also distinguishes independent indicators from indicators connected through death or survival. This mission establishes a finite-horizon generalisation of those identities that handles arbitrary dependencies among payment-triggering events.
Fix a measurable sample space with a probability measure . A finite set indexes distinct payment obligations. Each obligation has a non-negative integer payment date , a deterministic cashflow amount , and a measurable event that triggers payment. The deterministic discount function assigns a multiplier to each date. Write for the real-valued event indicator, equal to one on and zero otherwise.
The random present value is
The same date can support multiple obligations with distinct contingencies, such as member and survivor payments, pension tranches and expenses. The index distinguishes obligations even when their payment times coincide. Amounts may be positive, zero or negative and triggering events can be mutually exclusive, nested, independent or arbitrarily dependent. Finite schedules also allow no obligations. Each present value is bounded and has finite first and second moments because the schedule is finite, amounts are deterministic real numbers, and indicators are bounded.
The capstone theorem proves the expected present value, second moment and variance identities for the same random variable . The expected present value is
The second moment retains all dependence terms, including pairs of different obligations payable on the same date:
Consequently,
The finite identity for expected present value specialises the textbook's equation (3.3). The general joint-event second-moment identity extends its §3.1.1 discussion to arbitrary dependence. The goal combines all three formulas in a single result, with supporting milestone theorems for integrability, square-integrability, one-event expectation, the finite-schedule expectation formula, pairwise event interactions, the second moment and the variance.
A single reusable statement should allow a future mission to specify the trigger events and payment schedule of a policy and immediately obtain its discounted mean and variance. A life assurance can use disjoint death-year events, and an annuity can use nested survival-to-payment events. A guaranteed pension, deferred benefit, survivor pension or multiple-decrement model can use more general indicators. Later missions can also specialise the variance expression when events are known to be independent or mutually exclusive.
Examples of why the dependence assumptions matter. Write for each discounted obligation amount:
These specialisations use the same capstone rather than different definitions of actuarial present value.
The mathematical identities are established results of elementary probability and financial mathematics. The formalisation contribution is a stable actuarial cashflow interface connecting the relevant Lean measure-theoretic and probability results. It does not assert that the classical equations are newly discovered, or that general insurance reserving, stochastic interest rates or continuous-time survival models have already been formalised.
The event indicator is a bounded random variable, but its mathematical expectation is represented in Lean by integration against a measure. The development must reconcile the real-valued integrals with event probabilities represented as extended non-negative reals. Moreover, expanding the square of a finite random cashflow sum requires pairwise intersections without adding an independence assumption. The usual simplification that removes cross-terms is invalid for nested survival events or arbitrary dependent payment events.
The target also uses the real-valued variance from Mathlib. Its general API permits variables outside , so a faithful proof must establish square-integrability for the finite event-based present value rather than use any default value for an undefined or infinite variance.
The initial development is discrete-time and finite-horizon, with distinct payment obligations indexed by a finite set. Each obligation has a nonnegative integer payment time. Different obligations may have the same payment time. Discount multipliers and payments are deterministic real values; no positivity assumption is needed for the algebraic identities. Each trigger is a measurable event and the underlying measure is a probability measure. Empty index sets and zero or negative payments are included. The joint-event formula remains valid when the same outcome triggers more than one payment.
Use Mathlib's existing MeasureTheory.Measure, MeasurableSet, integration and ProbabilityTheory.variance rather than redefining them. A lightweight namespace ActuarialValuation should define the random present value and retain clear time and cashflow parameter names. Supporting results should be small and import only genuine mathematical dependencies. The formalisation uses a generic obligation index type and a payment-time function into the natural numbers. The event family and amounts are indexed by obligations rather than by time.
There is no finite-to-infinite inference in the target; infinite sums require separate convergence results. There are no mortality rates, hazard functions, Markov transition kernels or stochastic discount factors in this mission. Those are targets for later missions, building on the valuation layer.
First-order hyperbolic systems of balance laws model open-channel flow (the Saint-Venant equations), gas pipelines, traffic and heat exchangers. In most of these applications the state can be acted on only at one end of the domain, so stabilizing an equilibrium is a boundary control problem. For systems without source term (), static boundary feedback built from a Lyapunov function works (Coron–Bastin–d'Andréa-Novel 2008); with a source term, Lyapunov functions of the diagonal form can fail (Bastin and Coron 2011, recalled in Remark 1 of the paper). Backstepping, introduced for parabolic equations by Krstic and Smyshlyaev, replaces the search for a Lyapunov function by an invertible integral change of variables that maps the linearized plant to a target system whose stability is evident.
Coron, Vazquez, Krstic and Bastin (arXiv:1208.6475v1, 2012; SIAM J. Control Optim. 51(3), 2013) design such a feedback for the linearization of a quasilinear system and prove that it stabilizes the nonlinear system locally in . This mission formalizes that main result, Theorem 4.1.
The state is on , , governed by
The standing assumptions (§2) are: , , are ; with on ; ; . Write and ; the paper treats .
The scaling , , , removes the diagonal of the linearization, which becomes with , , , and antidiagonal with entries , . The kernels solve a pair of first-order hyperbolic equations on the triangle with boundary data on its diagonal and on the edge ((3.32), (3.33), (3.36), (3.37)). The gain is .
The closed loop adds a dynamic extension:
with , , and , determined by the initial profile through two linear functionals , . The norm is on .
For every there are such that every classical solution with satisfying the compatibility conditions (4.16), (4.18) obeys
Write for the full kernel , , , and .
Theorem 4.1 shows that a feedback computed entirely from the linearization, by solving linear kernel equations, is a valid local stabilizer of the quasilinear system in , the natural space for classical solutions of quasilinear hyperbolic systems. The dynamic extension is what makes the result usable: without it, the static feedback imposes artificial compatibility conditions (4.17), (4.19) on the initial data.
The result is proved in the paper (§5 and Appendix B); none of it is machine-checked. A formal proof needs a rigorous treatment of the Volterra transformation and its inverse in , the three-level Lyapunov argument (, , ), and the comparison of these functionals with the norm. The formalization also records corrections to the printed formulas: the sign of in (4.1), the entries of in (4.7), the initial values (4.26), and the admissible decay rates (see below).
The obvious argument — the linear closed loop is exponentially stable, so the nonlinear one is locally stable — fails for hyperbolic systems: the nonlinear terms contain a derivative of the state, so they are not small in relative to , and an estimate does not close. One must control , and simultaneously, each with its own Lyapunov functional whose weight depends on the state, and exchange time derivatives for space derivatives through the equation, which is possible only while and stay small.
States are Fin 2 → ℝ, matrices Matrix (Fin 2) (Fin 2) ℝ, indices 0-based. A solution is one function (space first) with the PDE imposed on and the boundary conditions for ; this is the theorem restricted to classical solutions, since Mathlib has no Sobolev spaces. Global existence is not asserted. Coefficient functions are defined on all of with global regularity and sign conditions on . , norms are sums of norms, as on p. 11; uses .
Added or corrected relative to the page, all disclosed in the items:
Trivializing formalizations are ruled out: , and every milestone constant are quantified after the data and before the solution; the kernels are pinned down by all their equations and boundary conditions (unique by Theorem A.1 of the paper); the corrected , are the ones every classical solution has, so no small initial profile is excluded; and the norm contains .
Not formalized: Lemma 5.2 (its printed bound (5.38), , fails for profiles with small and large , and (5.37) compares a matrix with a scalar), and Lemmas B.1–B.4, B.7, B.8. Contributions of a reusable theory of Volterra integral transformations on with kernels, and of the comparison between sup and norms of solutions of hyperbolic systems, are welcome.
The adjacency matrix of an Erdős–Rényi random graph contains a large deterministic mean as well as random fluctuations. The mean affects the largest eigenvalue, while the centered fluctuations determine much of the remaining spectrum. A local spectral law must describe both pieces at a resolution fine enough to distinguish eigenvalues within a narrow energy window. Erdős, Knowles, Yau and Yin established such estimates for a broader class of sparse symmetric matrices and their noncentered rank-one deformations in Spectral statistics of Erdős–Rényi graphs I. This mission formalizes the paper's Theorem 2.9, with the centered-matrix law and eleven intermediate results of the paper as milestones.
The paper treats the graph matrix through a model that also allows other sparse distributions. Its parameters and separate sparsity from the size of the deterministic mean. That separation matters: the normalized resolvent trace can obey a local semicircle law even when the deformation produces a distinguished top eigenvalue. The formal target therefore concerns the deformed matrix itself, rather than replacing it with the centered matrix.
For each size , let be a real symmetric random matrix. Entries indexed by the upper triangle are independent, centered, and have variance . Their higher moments obey
The sparsity parameter lies between and , and the logarithmic parameter satisfies , with and . Define and the noncentered matrix , where . The projection has every entry equal to . These are Definitions 2.1 and 2.2 of the source paper, pp. 5–6.
For a complex number with , the resolvents are and . Their normalized traces are and . The comparison object is the semicircle density and its Stieltjes transform . Put and for a fixed . These definitions appear in Section 2, pp. 7–9.
An -dependent event has -high probability when its failure probability is at most for all sufficiently large . The spectral estimates below refer to single events on which the claimed bound holds at every simultaneously.
Theorem 2.9 assumes and . Its first conclusion is that, with -high probability, every satisfies
Under the additional bound , its second conclusion controls every entry at every :
The constants are universal and positive. The probability exponent may depend on the fixed parameters named in the theorem. Both conclusions, including the extra condition on in the second, are retained from Theorem 2.9, pp. 9–10.
The milestones follow the paper's own sequence of numbered results.
The trace estimate gives quantitative control over spectral mass at local scales, including near the edges . The entrywise estimate says more: each resolvent entry is close to the diagonal semicircle approximation with an error that records both sparsity and finite-size effects. The paper's later results derive density-of-states and eigenvector statements from these local controls. Those consequences are outside this mission's goal.
The intended formal development supplies reusable definitions of sparse symmetric ensembles, high-probability events, semicircle transforms, and complex resolvents, followed by exact statements of the paper's estimates. Mathlib contains no local semicircle law, for Wigner or for sparse matrices, and no Stieltjes transform of the semicircle distribution; the local law, the large deviation bounds and the interlacing lemma are each reusable beyond this paper.
The deterministic rank-one comparison controls the normalized trace but does not by itself control each entry of . The entrywise estimate must account for the deformation and for fluctuations caused by sparse entries. Near the spectral edges, the stability scale of the semicircle transform changes with ; a bound that is uniform in the bulk does not automatically retain the paper's edge behavior. The theorem also asks for one event covering a continuum of values, so a collection of separate fixed- probability bounds has the wrong quantifier order. These are substantive parts of Sections 3–7, beyond algebraic manipulation of resolvents.
Lean represents all on one probability space and takes their entries to be real, symmetric, measurable random variables, independent in the upper triangle. Conditions involving and the moments hold for all sufficiently large ; this avoids impossible small- parameter bounds and matches the asymptotic theorem. The moment order is real, as in the paper. Each finite expectation has an explicit integrability condition. A single positive constant is used for the moment, sparsity, and deformation bounds: replacing several fixed constants by their maximum preserves all three inequalities.
Matrix indices use Fin N rather than the paper's . The resolvent is a complex matrix formed by coercing the real matrix before subtracting . Every result that uses it restricts eventually or explicitly; its inverse at a singular input is never used to make a claim. The semicircle transform is defined by the paper's integral, and uses Lean's nonnegative square root, implementing the positive part. The high-probability predicate evaluates the measure of arbitrary sets, so it can state the intersection over all without a separate measurability assumption on that intersection. Positive and positive square-root arguments follow eventually from the model and .
The deterministic Lemmas 3.2, 3.4, 3.10, 6.1 and 7.1 are stated for every real symmetric matrix and every with (Lemma 3.2 on ); the paper's is contained there. Minors keep the original index names, and is only used for . is the explicit expression of (3.15). Ordered eigenvalues are the sorted roots of the characteristic polynomial. Statements the paper makes "for fixed " (Lemmas 4.1, 7.7, Proposition 7.6) are uniform in : one threshold serves every . The unnamed constants , , are chosen after the fixed parameters and before the random matrices; the universal come first.
Trivializing encodings are ruled out: every resolvent is taken at , so the junk inverse of a singular matrix never enters; the model is satisfiable (independent Rademacher signs divided by with and satisfy it for large ); each event of the goal is one intersection over all , not a family of pointwise bounds; the constants appear in the paper's order; and the goal is about with allowed to be large, so it does not reduce to Theorem 2.8.
Part (iii) of Lemma 3.8 is not a milestone: the printed (3.22) omits the diagonal variance term , without which it fails for Rademacher variables with . Contributions of proofs of any milestone, and of the missing groundwork (Stieltjes transforms of measures, Schur complements of resolvents, moment bounds for sums of independent variables), are welcome.
A decision maker who must choose to minimize an expected cost rarely knows the distribution of the uncertain parameter ; what is available is a sample . Sample average approximation (SAA) replaces by the empirical distribution. Data-driven distributionally robust optimization (DRO) instead minimizes the worst case of the expected cost over a set of distributions built from the data, which protects against the error of the empirical distribution at small . Many such sets have been proposed: moment sets (Delage and Ye, 2010), -divergence balls (Ben-Tal et al., 2013), Wasserstein balls (Mohajerin Esfahani and Kuhn, 2018).
Bertsimas, Gupta and Kallus (arXiv:1408.4445v3; Mathematical Programming, 2018, doi:10.1007/s10107-017-1174-z) observe that each such set can be read as the confidence region of a statistical goodness-of-fit (GoF) test, and call the resulting method Robust SAA. A basic question for any such method is whether, as , its objective, optimal value and optimal solutions converge to those of the full-information problem. The paper answers it for all data-driven DROs at once, with a single property of the test.
The support of is closed, and is the set of Borel probability distributions on with the topology of weak convergence. The data are i.i.d. from an unknown . A data-driven uncertainty set (DUS) map assigns to each sample a set ; it is the confidence region of the test that rejects a hypothesis exactly when . Decisions lie in a closed set , the cost is , and the robust objective is the worst-case expectation
A test is uniformly consistent (Definition 3) if, for every data-generating , almost surely every sequence that does not converge weakly to lies outside for infinitely many . The admissible instances are those satisfying three assumptions: (1) is equicontinuous in uniformly over ; (2) is bounded, or is coercive in uniformly over a set of positive -probability and bounded below off ; (3) is bounded, or there is a growth function with whose expectation the DUS tracks: almost surely. The convergence conditions are (18) uniformly on compact subsets of ; (19) convergence of optimal values; and (20) every sequence of robust minimizers has a limit point, and all its limit points are true minimizers.
For a DUS map with nonempty sets,
The statement carries no rates and no constants; it is a characterization, so it does not depend on any particular test.
The result. Theorem 2 reduces the asymptotic analysis of a data-driven DRO to a property of a statistical test, which can be checked once per test rather than once per optimization model. The paper uses it to classify DUSs: the and G-tests on a finite support and the Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling tests on the line are uniformly consistent (Theorems 4–5, separate missions of this series), while the test of marginals is not even consistent and so cannot give convergence for every cost. The necessity direction makes the property sharp: a weaker test always admits a well-behaved cost on which the DRO fails to converge. Theorem 3 explains the remaining cases where a DRO converges for one given cost.
Formalizing it. The result is proved in the paper (§10.5), but its proof leans on several standard facts used without detail: the portmanteau theorem, uniform integrability arguments from Billingsley's Convergence of Probability Measures, the Lévy continuity theorem with the Cramér–Wold device, and coercivity arguments carried over from the paper's Theorem 1. A machine-checked version would fix exactly which regularity of the cost these steps need; three such conditions are stated explicitly here (see the scope section). No part of the result is formalized elsewhere to our knowledge; the platform has no notion of a data-driven uncertainty set or of uniform consistency.
Uniform consistency is a statement about weak convergence, while (18)–(20) are statements about expectations of an unbounded, -dependent cost under the members of . Weak convergence controls expectations only of bounded continuous functions, so the "only if" side must recover convergence of from Assumption 3, which requires uniform integrability, and then upgrade pointwise convergence to uniform convergence on compacts and to convergence of minimizers when is unbounded. The tempting route through a single limiting minimization problem fails: the sets change with the sample, the worst case is a supremum over infinitely many distributions, and the minimizers of could escape to infinity unless coercivity on transfers to every member of . The "if" side needs, from the mere failure of uniform consistency, a single admissible cost whose worst-case objective detects every failure of weak convergence.
Points are EuclideanSpace ℝ (Fin d), distributions are ProbabilityMeasure ↥Ξ (whose topology is weak convergence), and the data live on the canonical product space with the product law, 0-indexed. "Almost surely" is ∀ᵐ, and in Definition 3 one null set serves every sequence . An expectation over a member of is when the integrand is not integrable, never Lean's default . Minima in (19)–(20) are infima in the extended reals, so the empty and unattained cases need no special treatment; (20) applies to sequences that are minimizers for all large .
Four hypotheses are added to the page, each used by the paper's own proof: every is nonempty (otherwise the worst case is and uniform consistency is vacuous); is continuous on ; the set of Assumption 2b is open; the growth function of Assumption 3b is continuous, with as fixed on p. 10 of the paper. Theorem 3 additionally assumes Assumption 2, which its proof uses. Proposition 4 assumes the rejection events are measurable. A formalization in which the worst case uses the raw Bochner integral, the supremum ranges over a possibly empty set, or (20) requires minimizers at would make the statements false or vacuous, and is ruled out.
A full development needs weak convergence and the portmanteau theorem (in Mathlib), uniform integrability and its relation to convergence of means under weak convergence, the strong law of large numbers for the growth function and the empirical measure, the Lévy continuity theorem in several dimensions (in Mathlib, via characteristic functions), and a countable convergence-determining class of bounded continuous functions. The uniform-integrability step and the path characterization of local uniform convergence (Proposition 9) are reusable beyond this mission. Contributions to any milestone are welcome; Proposition 9 is self-contained and deterministic.
Bayesian inference, statistical physics and machine learning all ask for samples from a probability distribution on whose density is known only up to a constant, . The unadjusted Langevin algorithm (ULA) is the Euler–Maruyama discretisation of the Langevin diffusion, whose invariant law is . It needs only gradients of , has no accept/reject step, and is therefore cheap in high dimension. Without the Metropolis correction, however, the chain does not leave invariant, so its usefulness rests on quantitative bounds: how far, in total variation, the law of the -th iterate is from , as an explicit function of the dimension , the step sizes and the regularity of .
Durmus and Moulines (arXiv:1507.05021, Ann. Appl. Probab. 27(3), 2017) gave such bounds for constant and decreasing step sizes. Earlier work of Dalalyan (arXiv:1412.7392, 2017) treated strongly log-concave targets with constant steps. Durmus and Moulines cover nonincreasing step sequences and, among other regimes, potentials that are only strongly convex outside a ball; this mission formalizes that case.
Write and for the Euclidean norm and inner product of . The total variation norm of a difference of probability measures is
which ranges in .
The potential satisfies two assumptions:
The point is a minimiser of , and .
The Langevin diffusion is , with a standard -dimensional Brownian motion. Its transition semigroup is .
ULA with step sizes is the chain
with i.i.d. standard Gaussian. Its one-step kernel is , and is the law of started at . Write , and let .
The explicit constants use
Let , and let be positive and nonincreasing with . Then for all and ,
The three constants are explicit:
The paper's proofs follow each statement in the body of the paper (§4.1, §4.12, §5, §5.1).
The theorem bounds the sampling error of ULA in total variation non-asymptotically, with a dimension-free contraction rate and constants polynomial in . With steps decreasing to zero and cumulative step size diverging, its bound gives convergence of to ; for constant steps, the paper reports iteration counts of order at a prescribed precision in Table 2. H3 covers log-concave targets whose potential can lack strong convexity inside a ball.
The result is proved in the paper but, as far as the platform's catalogue shows, not formalized anywhere. A formalization adds machine-checked versions of several reusable pieces:
The ULA chain is not reversible with respect to , so the spectral and Dirichlet-form tools of reversible MCMC do not apply to it directly. The bound must instead compare the chain with the continuous diffusion.
That comparison needs Girsanov's theorem on path space and a uniform control of along a time-inhomogeneous chain.
The rate of the diffusion itself is the second obstacle. Without global strong convexity, synchronous coupling gives no contraction inside the ball . An explicit rate requires a reflection coupling together with return-time estimates, and it has to be transferred through the time change between and .
The state space is the published EthierKurtz.SDEState d, i.e. EuclideanSpace ℝ (Fin d), and Brownian motion and strong solutions are the published EthierKurtz.IsStandardBrownian and EthierKurtz.SolvesBrownianSDE. The conventions are:
Measure.bind with the Gaussian kernel . Steps are indexed from , and for .Several hypotheses are added or read in a particular way, and each is disclosed in the item's statement:
The citations [20] (existence of solutions), [27] (Lindvall), [32] (Meyn–Tweedie) and Girsanov's theorem are used inside the proofs and are not restated.
The library work needed is substantial: Itô calculus for the reflection coupling, Girsanov's theorem, Pinsker's inequality in this norm, and generator–drift arguments for the moments of . Contributions of any of these as standalone platform theorems are welcome.
A McKean–Vlasov control problem asks a planner to steer a stochastic differential equation whose coefficients depend not only on the current path of the state but also on its (conditional) distribution. Such problems describe the cooperative optimum of a large population of interacting agents: when each agent reacts to the empirical distribution of all others and a social planner chooses everybody's control, the limit as the population grows is a McKean–Vlasov control problem (Lacker 2017). When all agents are also exposed to a common noise (a shared source of randomness, such as a market factor), the relevant distribution is the conditional law of the state given that noise.
Bellman's dynamic programming principle (DPP) is the standard route from a control problem to its Hamilton–Jacobi–Bellman equation and to verification arguments. For McKean–Vlasov dynamics it fails in the naive state variable, because the problem is time-inconsistent; it can be recovered by taking the (conditional) law of the state as the state.
Timeline. Laurière and Pironneau (2014) and Bensoussan, Frehse and Yam (2013–2017) proved a DPP for densities of the state law. Pham and Wei (2017, SICON) proved a DPP over closed-loop controls in a Markovian setting with a common-noise filtration, under regularity assumptions; Pham and Wei (2018, ESAIM:COCV) treated the case without common noise. Bayraktar, Cosso and Pham (2018, Trans. AMS) obtained a randomised DPP, again Markovian and without common noise. Djete, Possamaï and Tan (2022) proved the DPP for the general non-Markovian problem with common noise, under Borel measurability of the coefficients only. This mission formalizes their DPP for the weak formulation.
Fix a horizon , dimensions , a nonempty Polish space of control values, a point and an exponent . Let with the uniform norm, the Borel probability measures on with the weak topology, and the path stopped at time . The coefficients are maps , and ; all are Borel measurable, and depend on the path and the measure only through their restrictions to (non-anticipative).
A weak control with initial condition consists of a probability space carrying two filtrations (the second models the common noise), a state , Brownian motions (idiosyncratic) and (common) on , a predictable -valued control , and measure-valued processes and , such that , an integrability condition of order holds, a compatibility condition between the two filtrations holds, and
The reward and the value function are
with and . Each weak control also carries , where is a Borel isomorphism of onto a subset of , and the continuous conditional-law process of given .
is upper semi-analytic (every superlevel set is analytic), and for every stopping time of the canonical filtration of with values in , setting ,
The canonical reformulation on with weak control rules (Definition 4.1): Lemma 4.4(i) (weak controls and weak control rules correspond), Corollary 4.6 (), Lemma 4.7 (analytic graphs, u.s.a.), Lemma 4.8 (stability under conditioning at a stopping time), Lemma 4.9 (dependence on the initial law only through ), (4.10) (moment truncation , analytic and u.s.a.) and Lemma 4.10 (universally measurable -optimal families and concatenation).
The result. The theorem gives the DPP for McKean–Vlasov control with common noise in a non-Markovian setting, with no regularity on the coefficients beyond Borel measurability and no integrability on the rewards. It is the starting point for the dynamic programming (HJB) equation on the space of probability measures, for the Markovian corollaries of §3.2 of the paper, and, through the equivalence of formulations in the companion work, for the strong formulations treated in the second mission of this series.
Formalizing it. The result is proved on paper; nothing of it is machine-checked. A formal development needs a working theory of weak controls with conditional laws, a controlled martingale problem on a space of measure-valued paths, and analytic-set measurability in continuous time. None of these exists in Mathlib, and the analytic-selection layer on Prove2Me (Bertsekas–Shreve, Chapter 7) is stated but not yet proved.
The obvious argument conditions an optimal-ish control on its information at the stopping time and pastes in near-optimal controls from the conditioned states. Each step fails without additional structure: is not known to be measurable, so is not obviously meaningful; conditioning a weak control on its information at need not yield a weak control, because the conditional-law constraint involves the common-noise filtration and a compatibility condition between filtrations; and choosing a near-optimal control for each conditioned state is a selection problem over an uncountable family of probability spaces. The state of the problem is a law, which is itself defined only up to null sets, so random-time evaluations such as need a continuous version.
The Lean development lives in the namespace MKVDPP.Weak. Conventions:
Type (universe 0).EthierKurtz.HasBrownianItoIntegral) of integrands that are a.s. square integrable on , taken against the shifted Brownian motions , ; no condition, which would shrink .The goal does not mention the canonical space , weak control rules or any selection; a formalization of that is empty, or a value function that is constant, would trivialize it. A sanity file exhibits a weak control in the degenerate case for every , so the structure is satisfiable.
Infrastructure a complete development needs: conditional laws and r.c.p.d. on Polish spaces, the predictable -algebra, stochastic integrals against a filtration, the Stroock–Varadhan martingale problem, Itô's formula, and analytic sets with the Jankov–von Neumann selection theorem. The analytic-selection results and the martingale-problem/SDE correspondence are reusable well beyond this mission. Contributions on any milestone, and on proving the referenced Bertsekas–Shreve selection theorems, are welcome. Out of scope: Theorem 3.4 (it rests on the companion paper), the Markovian results of §3.2, and the HJB discussion of §3.3.
A controller may act on a large population of interacting particles while all particles also experience a shared random disturbance. In the population limit, the state of a representative particle depends on the distribution of states conditional on the common noise. The controller therefore influences both its own state and the conditional population law. The usual state variable for dynamic programming must carry that law, and a future decision may use only information available from common noise. Djete, Possamaï and Tan establish a dynamic programming principle for this setting in McKean–Vlasov optimal control: the dynamic programming principle, Theorem 3.2. Their result permits path dependent coefficients and merely Borel reward functions, so ordinary continuity arguments do not determine the value function's measurability.
The paper distinguishes a weak formulation, in which the stochastic basis varies with the control, from a strong formulation on a fixed space. This mission concerns the latter, restricted to controls predictable from common noise, under the paper's Lipschitz and growth Assumption 2.8. The companion mission treats the weak dynamic programming principle, Theorem 3.1. The present mission asks for a machine checked account of the strong formulation and of the transfer between its intrinsic, fixed space and canonical descriptions.
Fix a horizon . A state trajectory belongs to . The two driving noises are a dimensional idiosyncratic Brownian motion and an dimensional common Brownian motion . The control space is nonempty and Polish. At time , the controlled drift and diffusions may depend on the stopped state path , the control , and the conditional law of the stopped state and control given common noise. The running and terminal rewards are and .
A strong control has a continuous state satisfying the controlled stochastic equation, the conditional laws required by the paper, finite quadratic control energy, and an predictable for the common noise filtration. Its reward is the expected running reward from to plus the terminal reward. The value is the supremum of these rewards over such controls from initial path law . The initial law lies in , the laws with a finite second moment. The coefficient hypothesis uses the quadratic Wasserstein distance and one constant for both a Lipschitz bound and a quadratic growth bound. These conditions are Assumption 2.8 of the source paper, p. 8.
The paper also fixes a canonical probability space carrying an initial path and Brownian increments after . Its common noise predictable controls form . Proposition 2.10 says this fixed space computes the same value as the intrinsic strong formulation. The precise probability law on is characterized by the initial stopped path law and independent standard Brownian increments; the paper does not choose a unique construction.
The goal is Theorem 3.2, p. 10. It first asserts that the value on is upper semi analytic: each strict superlevel set is analytic. For an initial pair and a stopping time for the raw common noise filtration on , it then asserts
Here is the law of the stopped state conditional on information from common noise at . The milestone sequence follows the paper's supporting results: strong solution existence and uniqueness (Theorem A.3(i)); equivalence of intrinsic and fixed space values (Proposition 2.10); induction of canonical rules from strong controls (the forward clause of Lemma 4.4(ii)); the canonical value identity (Corollary 4.6); the Wiener represented rule class and its value (Lemma 4.11); analytic rule graphs and value measurability (Lemma 4.12); and stability of a strong rule under conditioning at a stopping time (Lemma 4.13(i)). Each is a source indexed target, rather than an invented intermediate assertion.
The identity permits the value after a random common noise stopping time to be evaluated from the stopped conditional state law. This is the form needed to compare control decisions before and after a random observation time. Upper semi analyticity supplies measurable superlevel sets for the value even when and lack continuity. The paper proves these statements mathematically; the mission seeks their Lean formalization, not a new theorem about the underlying control problem.
A complete formalization would also provide reusable definitions of conditional measure valued flows, Brownian motion relative to a filtration over a shifted interval, a local Itô equation, and canonical martingale control rules. The two published Ethier–Kurtz definitions supply the local Itô relation and probability augmentation of a filtration. They are shared infrastructure rather than new statements of this paper.
The state law in the coefficients is conditional on common noise and changes with the control. A pathwise solution of the state equation must therefore remain consistent with its own conditional law. A naive argument that restarts an ordinary diffusion at does not establish that consistency for a restarted control. It also does not ensure that a restarted control remains predictable from common noise. The paper's canonical rule formulation and its conditioning and measurability results address those obstructions. The reward may be unbounded and extended real valued, so the expectation convention and its behavior at infinite positive and negative parts matter to the statement itself.
Paths are continuous maps on compact real intervals with uniform norm; is Mathlib's Euclidean space, including . Probability measures carry weak convergence topology, and is its finite second moment subtype. The product of path space and uses Mathlib's product metric; matrix norms are Frobenius. Supremums range over admissible controls, solutions and conditional law versions. They are EReal valued, so the empty supremum is . The signed expectation is positive part minus negative part with , as in the paper. The model fixes a Borel embedding of into and a cemetery control for invalid reconstructed paths.
The Lean statements pin the paper's implicit “well defined” stochastic integral to a pathwise square integrable local Itô relation and almost surely integrable drift. A conditional law equality stated for almost every pair is expressed in Fubini form. The localized processes printed in Definition 4.1 define its local martingale requirement. The terminal law and the stopped law in the target are quantified as versions of their stated conditional distributions. The fixed canonical law is any law satisfying the paper's initial distribution and Brownian conditions; the target is stated for every such family. These conventions rule out free conditional laws, arbitrary future stopping times, and a value that is solely because a formalization made the control class empty. A full development must establish nonemptiness and version independence as part of the cited supporting theory.
The scope ends with Theorem 3.2 and the listed milestones. Lemma 4.13(ii), the more involved measurable selection and concatenation result, remains a future contribution. Theorem 3.4 uses a separate companion result; the Markovian corollaries and the heuristic Hamilton–Jacobi discussion of §3.3 are outside this mission.
Systems of two first-order hyperbolic equations with opposite transport speeds model open-channel flow (the Saint-Venant equations), gas pipelines, heat exchangers and traffic. In such systems one boundary is actuated, the other boundary reflects, and the coupling terms move energy between the two families of waves. Boundary feedback design for them is a standard problem of distributed-parameter control.
The backstepping method designs a feedback by means of an invertible Volterra integral transformation that turns the plant into a target system whose behaviour is known in closed form. Coron, Vazquez, Krstic and Bastin (arXiv:1208.6475; SIAM J. Control Optim. 51(3), 2013) carry out this design for a general linear hyperbolic system with spatially varying speeds and couplings, in §3 of their paper. The resulting linear feedback is the controller they later apply to a quasilinear system. This mission formalizes the linear result.
Timeline:
Let be functions on with , let be continuous, and let . The state solves
so travels to the right and to the left. The boundary conditions are and , where is the control. The norm is .
The kernels are functions on the triangle that solve
with and . The control law (3.48) is
The target system is with and , for . The direct transformation is (3.23), with the full kernel of (3.30)–(3.37). The inverse transformation is (3.38), with solving (3.40)–(3.47). The finite time is
For , every classical solution of the closed loop satisfies
Here depends on and the data but not on the solution.
The theorem shows that a single linear boundary feedback, computed once from the coefficients, drives every state of the system to zero in exactly the time . That time is the sum of the travel times of the two characteristic families across . Exponential stability at every rate follows. The same feedback, rescaled, is the controller of the paper's main result, Theorem 4.1: local exponential stabilization of a quasilinear system, the subject of mission 3 of this series. The well-posedness of the kernel equations, Theorem A.1, is mission 1.
The result is proved in the paper. As far as is known, none of it has been machine-checked. A formal proof needs Volterra transformations of vector-valued functions with differentiation under a variable-limit integral, explicit solutions of transport equations along characteristics, and estimates for integral operators with continuous kernels. These tools apply to backstepping designs well beyond this paper.
Proposition 3.1 and the two mapping statements are calculations: an integration by parts and the explicit solution along characteristics. The difficulty of Theorem 3.2 is the step "the transformation is invertible", which the paper's proof takes for granted. The goal hypothesizes only , so it is not enough to state the mapping and the inverse separately. The solver has to recover the full state from the target state: either build the remaining kernels and the inverse kernel , or argue directly from the closed subsystem. Both routes need existence or uniqueness for Goursat-type problems, which the paper proves only in Appendix A. A second, routine obstacle is that the uniform constant must be extracted from the finite-time interval using bounds on the kernels.
w : ℝ → ℝ → Fin 2 → ℝ, space first, with Lean index 0 for the paper's first component.Three trivializing readings are excluded. The constant is quantified after the data and before the solution, so it cannot depend on the solution. The finite-time claim is vanishing for every , with exactly (3.8), not for some unspecified time. The kernels are pinned down by all four of (3.32), (3.33), (3.36), (3.37). With coefficients a solution exists (the paper's Theorem A.2), and a sanity file checks that the hypotheses admit a non-zero closed-loop solution.
Welcome contributions: lemmas on differentiating , transport equations along characteristics, and the invertibility of Volterra operators with continuous kernels.
The paper's proofs are on pp. 3–5 (Proposition 3.1), p. 5 (§3.2), p. 6 (§3.3) and p. 7 (Theorem 3.2).
The characteristic polynomial of an ordinary graph records spectral information in coefficients that can also be described by finite graph configurations. The classical Harary–Sachs theorem is an instance of this connection. For a uniform hypergraph, the adjacency object is a tensor rather than a matrix, and its characteristic polynomial is defined through a multivariate resultant. Clark and Cooper's hypergraph theorem gives a corresponding coefficient formula. It identifies the configurations that replace the elementary subgraphs of the graph case and assigns them weights determined by directed Eulerian structures. The result makes a tensor spectral invariant accessible through finite combinatorial objects.
The article appeared as Gregory J. Clark and Joshua N. Cooper, A Harary-Sachs theorem for hypergraphs, Journal of Combinatorial Theory, Series B (2021), DOI 10.1016/j.jctb.2021.01.002. This mission follows the pinned arXiv version 2, whose page and theorem numbers are used below.
A simple -graph has a fixed vertex set of labeled vertices and a set of distinct edges, each containing exactly vertices. Isolated vertices remain part of . The normalized adjacency hypermatrix gives an ordered -tuple the value when its underlying set is an edge, and zero otherwise. This normalization makes every ordering of the other vertices contribute the intended total weight.
The characteristic polynomial is the multivariate resultant of the coordinates of . The resultant is characterized by three conditions: it vanishes exactly when homogeneous coordinate polynomials have a nonzero common complex root, it evaluates to one on the coordinate monomials, and it is irreducible over the complex coefficient field. Its degree in is . The codegree- coefficient is the coefficient of ; this degree is fixed from the source theorem and is not read from an implementation of .
A multi-hypergraph is a multiset of -element edges. It is Veblen when the degree of every vertex is divisible by . Its flattening discards repeated edges, so is an infragraph of when every edge of its flattening belongs to . Components use only vertices covered by edges; a labeled object may still sit in a larger ambient vertex set with unused vertices.
A rooting of is a sequence of its edges, each assigned a root vertex in that edge, with roots in nondecreasing order. An edge rooted at contributes a directed arc to every other vertex of the edge. Summing these arcs with multiplicity produces a directed multigraph . An Euler rooting has balanced in- and out-degrees and connected positive-degree vertices. Its arborescence number counts spanning trees of these active vertices directed toward a specified root, with parallel arcs distinguished. For connected , its associated coefficient is
For disconnected , is the product of the coefficients of its connected components. These conventions follow Definitions 6–10 in the source.
The supporting targets identify when a monomial differential operator contributes to a matrix trace, and show that an Euler rooting determines a connected Veblen multi-hypergraph. The operator identity is counted by Euler tours with distinguishable parallel arcs. The resultant-to-trace identity quoted in the paper is also a milestone:
Here is the paper's sum over positive compositions of , and is its differential trace from Equation (1).
The goal uses the labeled form of Theorem 14. Let be the set of ordered -tuples of connected labeled Veblen infragraphs whose edge counts sum to . Then
The paper prints the equivalent sum over isomorphism classes, using automorphism groups and the copy weight . The labeled expression is the result before that grouping. The isomorphism-class statement is outside this mission's Lean target and remains a separate formalization task.
The theorem expresses a coefficient of a resultant, defined algebraically over complex common roots, as a finite rational weighted sum over hypergraph configurations. It extends the graph case while preserving the exact normalization, sign, component count, and coefficient index. The formula can be used to study low codegree coefficients by enumerating finite Veblen infragraphs and their Euler rootings. Clark and Cooper also use associated coefficients to compare different hypergraph structures in the paper.
The formal development separates the resultant, the differential trace, and the combinatorial counts into reusable definitions. It would provide machine-checked statements of the paper's main equality and several links between those definitions. The Lean theorems in this draft are open targets with sorry placeholders; compiling their statements does not constitute a machine-checked proof of the paper's claims.
The ordinary matrix determinant has a direct expansion by permutations. A tensor characteristic polynomial is a multivariate resultant, so that expansion does not directly reveal which hypergraphs contribute to a coefficient. The trace side uses repeated partial derivatives, and repeated hyperedges can create several distinct rootings with the same directed arc multiplicities. Counting only a multiset of root assignments loses those orderings and changes the coefficient. The Eulerian condition, arborescence multiplicities, and factorial factors must agree simultaneously for the algebraic and combinatorial expressions to match.
The Lean representation uses Fin n vertices, finite sets of simple edges, multisets of repeated edges, rational adjacency weights, and complex polynomials only for the resultant criterion. It assumes , , and . The source fixes , and the latter two bounds expose the domain in which the printed coefficient expansion and its proof use . An isolated vertex of counts in and in , while isolated vertices do not pad a multi-hypergraph component.
The formalization takes a polynomial satisfying the resultant's common-root, normalization, and irreducibility properties as an input. Separate sanity proofs give witnesses in the one-variable degree-zero and degree-one cases; degree one covers the first goal-domain degree when . The characteristic polynomial is evaluated from this polynomial, never defined by the trace identity. Rootings are sequences, arborescences are directed toward the least positive-degree vertex, and the associated coefficient is calculated on covered vertices. The goal uses the labeled sum, so no automorphism is computed on an ambient padded vertex set. Contributions formalizing the omitted isomorphism-class equivalence, the BEST circuit count, and proofs of the stated targets are welcome.
A graph may have enough symmetry for every edge to look the same while its vertices still fall into two distinct classes. Such a graph is semisymmetric when it has constant valency, is edge-transitive, and is not vertex-transitive. Conder, Zhou, Feng and Zhang study this phenomenon among bi-Cayley graphs, graphs equipped with a group acting freely on two vertex orbits. Their dihedral case supplies examples related to questions of Marušič and Potočnik about semisymmetric tetracirculants. It also asks how small the valency of a semisymmetric graph with this specific group action can be. The paper states that six is the minimum and that examples occur at every valency with odd (Conder et al., Theorem 1.5 and its introduction, p. 3).
The authors develop the bi-Cayley setting and the relevant automorphism actions before reaching the dihedral result. The lower bound appears as Theorem 6.1, while Example 6.2 defines a graph family and Proposition 6.4 gives a semisymmetry criterion for its odd- members (Conder et al., pp. 11–13). This mission targets those claims within a single formal graph model. The final sentence of Theorem 1.5, concerning an edge-regular family, depends on the separate Theorem 6.5 and is outside this goal.
Let be a finite group. Choose subsets with , , , and . The graph has two labelled copies of each element of , written and . For each , it joins to when , joins to when , and joins to when . These are unoriented edges. Right multiplication by preserves the graph and acts regularly on each of its two vertex copies (Conder et al., pp. 1 and 4).
A bi-dihedrant is a bi-Cayley graph whose group is dihedral. Write for the dihedral group of degree . Graph valency is the number of neighbours of a vertex. Connectedness is required throughout the paper. For a semisymmetric graph the common valency exists by definition, but the formal statements quantify over every vertex so that the numerical claims refer to the actual graph degree (Conder et al., definitions on p. 4 and Theorem 6.1 on p. 11).
The constructed family uses , , and a residue of multiplicative order modulo whose even-power sum vanishes: . For , put and . Set . Then (Conder et al., Example 6.2, pp. 12–13).
Right multiplication gives a subgroup , and is its normaliser. For and the paper's permutations are and ; the sets and of (2.2) collect those that preserve the edge rules. A graph is normal edge-transitive when , not merely , is transitive on edges (Conder et al., pp. 4–5).
The milestones, in attack order, are Proposition 2.1(b) (one may assume ), Proposition 2.2 (the normaliser ), the opening step of the proof of Theorem 6.1 ( for a semisymmetric graph), Theorem 6.1, the claims of Example 6.2, and Proposition 6.4.
For every connected semisymmetric bi-dihedrant over , , and every vertex ,
This is Theorem 6.1 and the first claim of Theorem 1.5. The milestone for the proof's opening step records that semisymmetry forces ; the theorem itself still ranges over all valid (Conder et al., Theorem 6.1, p. 11).
For each odd integer , there is a connected semisymmetric bi-dihedrant such that
Example 6.2 is the first milestone toward this claim: under its hypotheses is connected, , every vertex has degree , and for lies in and permutes the neighbours of cyclically, so the graph is normal edge-transitive (Conder et al., p. 13). Proposition 6.4 is the second: under the defining conditions for , odd and modulo imply semisymmetry (Conder et al., Proposition 6.4, p. 13). An auxiliary arithmetic theorem states the parameter existence needed to apply it for every odd .
The lower bound excludes semisymmetric bi-dihedrants of valency at most five. The existence assertion says that six is attained and places examples at an infinite sequence of larger valencies. Together these claims distinguish the restrictions imposed by a dihedral bi-Cayley action from edge transitivity alone. The construction also gives a concrete family on which questions about stronger automorphism properties can be posed (Conder et al., §6, pp. 11–14).
The result is proved in the cited paper; this mission seeks a machine-checked version of its first two Theorem 1.5 claims. The definition of a bi-Cayley graph, the precise graph symmetry predicates, and the arithmetic parameter family are reusable beyond this particular lower bound. The statements here are open proof targets in Lean, with their mathematical content fixed before proof development. The edge-regular claim from the theorem's final sentence requires additional source results and remains a separate formalization target.
Edge transitivity alone does not make a graph vertex-transitive: a semisymmetric graph is precisely the regular case where that inference fails. The lower bound therefore cannot be obtained by treating every vertex as lying in one automorphism orbit. In the dihedral case, the proof must account for both the rotations and reflections in the connection set, and for the constraints that connectedness and graph automorphisms impose on low-valency possibilities (Conder et al., proof of Theorem 6.1, pp. 11–12).
The existence statement has a distinct arithmetic requirement. Proposition 6.4 is conditional on satisfying Example 6.2 and . The paper asserts examples for every odd without spelling out parameters for all such . The auxiliary arithmetic statement records that remaining obligation explicitly; a proof of the conditional proposition alone would not establish the quantified existence claim.
Lean represents the two vertex copies by H ⊕ H and the dihedral group by Mathlib's DihedralGroup n. The graph is a SimpleGraph built from the three edge rules above, with the inverse-closure and loop-exclusion conditions retained in BiCayData. Semisymmetry uses the full graph automorphism group, unoriented edge transitivity, and constant graph degree. The source's standing finite, connected, simple, and undirected conventions are explicit through finite groups, simple graphs, and connectedness hypotheses. The goal and Theorem 6.1 use , the range of dihedral groups in §6; the existence examples are also required to be connected.
The definitions do not set valency equal to , replace a graph degree by a formula, or make an edge-transitivity claim true by ranging over an empty edge set. The setting requires valid inverse-closed side sets rather than silently symmetrising an invalid one. The arithmetic hypothesis uses the multiplicative order in and enumerates the indices of by . Normal edge-transitivity in Example 6.2 is stated for the subgroup and semisymmetry for the full group ; the two are not interchanged. The restriction in the lower bound is that of Theorem 6.1 and is a disclosed hypothesis of the goal: and are abelian, and the paper treats bi-Cayley graphs over abelian groups separately. The auxiliary parameter statement is not in the paper; it is supplied so that the existence claim has a complete proof path. The third sentence of Theorem 1.5 is not formalized. Contributions establishing the structural lower bound, the family criterion, or the arithmetic existence statement are all within scope.
A graph is symmetric when its automorphism group moves any vertex, edge or arc to any other, and -arc-transitive when it moves any walk of length without immediate backtracking to any other. Tutte's work on cubic graphs made -arc-transitivity a central measure of symmetry in algebraic graph theory, and most constructions of highly symmetric graphs start from a group acting regularly on vertices (Cayley graphs) or semiregularly with a few orbits.
Bi-Cayley graphs are the case of two orbits: a group acts semiregularly by right multiplication with exactly two vertex orbits. The Petersen graph, the Gray graph (the smallest cubic semisymmetric graph) and the smallest member of Bouwer's family of half-arc-transitive graphs are all bi-Cayley graphs, and all of them are edge-transitive. Deciding edge-transitivity of a bi-Cayley graph is hard in general, but the subgroup of automorphisms that normalise the semiregular group is explicitly known, which makes the "normal" version of the question tractable.
C. H. Li asked whether 3-arc-transitive bi-normal Cayley graphs exist and asked for a description of the 2-arc-transitive ones (Li, Proc. Amer. Math. Soc. 133, Question 1.2(a) and Problem 1.3(b), as cited in the paper, p. 2). M. Conder, J.-X. Zhou, Y.-Q. Feng and M.-M. Zhang answered both through their Theorem 1.1 (arXiv:1606.04625v1; J. Combin. Theory Ser. B, 2020). This mission formalizes that theorem and the lemmas its proof uses.
Let be a finite group with identity . Let with , and . The bi-Cayley graph has vertex set , two disjoint copies of (the copy of in is ), and edges , and for , , , . The main theorem concerns , where is bipartite with parts , and every vertex has neighbours.
For , is an automorphism of ; these form the subgroup , and
is its normaliser. For (written as an exponent, ) and the paper defines the permutations
and the sets of those with , , , and of those with , , .
An -arc is a sequence of vertices in which consecutive vertices are adjacent and . A subgroup is transitive on -arcs if any -arc can be mapped to any other by an element of ; 1-arcs are arcs. is normal edge-transitive if is transitive on edges, and normal locally arc-transitive if the stabiliser is transitive on the neighbourhood . acts semisymmetrically if it is edge-transitive but not vertex-transitive. is the setwise stabiliser of in .
Let be connected, with and . Then
where (a) for some ; (b) is transitive on ; (c) for some and . Furthermore, if , is not transitive on the 3-arcs of .
A companion item, Lemma 3.1, shows that a connected normal edge-transitive has ; it explains why the goal is stated for .
Combined with Lemma 3.1, Theorem 1.1 reduces 2-arc-transitivity of the normaliser of to three conditions on and the single set , all checkable in the group without building the graph. Its second part rules out normal 3-arc-transitive bi-Cayley graphs of valency at least 3, which settles Li's question on 3-arc-transitive bi-normal Cayley graphs negatively. Proposition 3.3 is the arc-transitive versus semisymmetric dichotomy for normal locally arc-transitive bi-Cayley graphs, the starting point of the paper's later constructions of semisymmetric and half-arc-transitive examples.
All results are proved in the paper (Proposition 2.2 by citation). None of them has a machine-checked proof that this mission knows of. Mathlib has simple graphs, graph isomorphisms and normalisers, but no bi-Cayley graphs, no -arcs and no transitivity notions for subgroups of . A formal proof would supply the first verified description of the normaliser of a semiregular group with two orbits, reusable for any bi-Cayley or bi-circulant result.
The bulk of the work is Proposition 2.2. That and preserve edges exactly under the conditions of (2.2) is a direct computation. The converse is harder: every automorphism normalising must be one of these permutations composed with some . That needs the conjugation action of on to induce an automorphism of , and to preserve the partition into -orbits.
The 3-arc clause looks like a stabiliser count, but it holds only once has at least two neighbours besides : for the graph is a cycle of length , the normaliser is the whole dihedral automorphism group, and that group is transitive on 3-arcs. Any proof must use at exactly this step.
The vertex set is H ⊕ H (Sum.inl h , Sum.inr h ). The data is a structure of three Finsets carrying the side conditions , , , and . Adjacency is given directly by the three edge rules. is the group Γ ≃g Γ, is the subgroup generated by the , and is its Subgroup.normalizer. Automorphisms of are MulAut H, and is the image of under . and are permutations of H ⊕ H, and "" means that some element of has as its vertex map. Products are written pointwise to avoid the composition-order convention of the group of graph automorphisms. An -arc is a function on Fin (s+1).
The paper assumes throughout that groups and graphs are finite and graphs connected; each theorem carries Fintype H and connectivity. Three hypotheses are added to the printed Theorem 1.1, each needed for the statement to be true or non-vacuous: (the paper's normalisation of a bi-Cayley triple, used by conditions (b) and (c) and by the proof); (for the graph is , which has no 2-arcs, so 2-arc-transitivity would hold vacuously while (c) fails); and for the 3-arc clause (false for cycles). Lemma 3.2 carries the same and , and Proposition 3.3 carries .
Trivializing formalizations are ruled out in four ways. 2-arc-transitivity is never vacuous, since guarantees 2-arcs. and are never symmetrised silently, since the side conditions are data rather than repairs. Every transitivity statement is about , not the full . Valency is the degree in the graph, never a formula in .
Contributions are welcome at every level: proofs of the milestones, a general library of bi-Cayley graphs and their normalisers, and lemmas on -arcs and stabilisers in SimpleGraph. The definitions are repeated identically in the companion missions on bi-abelian graphs and bi-dihedrants.
A Cayley graph turns multiplication in a group into adjacency between vertices. Every Cayley graph is vertex transitive: multiplying every vertex by the same group element moves any chosen vertex to any other. A bi-Cayley graph starts with two copies of a group and permits edges both within and between the copies. Its built-in group action is transitive on each copy, but it need not exchange them. This makes bi-Cayley graphs a setting for distinguishing edge, vertex, and arc transitivity. Conder, Zhou, Feng and Zhang study these distinctions and their consequences for graph constructions in Edge-transitive bi-Cayley graphs.
For abelian groups, the paper proves a strong restriction: once a connected bi-Cayley graph is edge transitive, it is also vertex transitive. Its half-arc-transitive examples face additional local restrictions, including a minimum valency of six. The paper exhibits a graph of valency six in Example 4.3, so the numerical bound is attained in its class. The result separates these graphs from semisymmetric graphs, which are edge transitive but not vertex transitive. The claims and example appear in Proposition 1.3 and §4.
Let be a finite group and let be subsets of . Require , , , and . The graph has vertices , two labelled copies of . For , an element gives an edge from to ; an element gives an edge from to ; and an element gives an edge from to . The inverse closure of and makes the within-copy edges undirected. Excluding from those two sets excludes loops. This is the construction on p. 1.
Every acts by right multiplication . The subgroup of graph automorphisms has two vertex orbits, and . Its normaliser in is useful for describing further symmetries. For a group automorphism and group elements , the paper defines permutations , which preserve the two copies, and , which exchange them. Their precise edge-preservation conditions are the sets and of equation (2.2). The mission includes those definitions and the relevant part of the normaliser characterization, Proposition 2.2.
A graph is vertex transitive if its full automorphism group can move any vertex to any other, and edge transitive if it can move any undirected edge to any other. Arc transitivity asks the same for ordered adjacent pairs. A graph is half-arc-transitive when it is vertex and edge transitive but not arc transitive. A semisymmetric graph has constant valency, is edge transitive, and is not vertex transitive. These are the paper's definitions on p. 4. Valency means the actual number of neighbours of a vertex.
The central target is the corrected reading of Proposition 1.3: for connected over an abelian ,
and, if is half-arc-transitive,
The attack path records the normaliser characterization in Proposition 2.2, both parts of Proposition 4.1, its explicit bipartition step, and Proposition 4.2. The companion Corollary 4.4 expresses the absence of connected semisymmetric examples over abelian groups.
The vertex-transitivity conclusion collapses one apparent possibility in the symmetry classification: an edge-transitive bi-Cayley graph over an abelian group cannot be semisymmetric. For half-arc-transitive graphs, the theorem rules out involutions in the within-copy connection sets, forces even set sizes, and excludes valencies below six. Example 4.3 supplies an attained bound, with and valency six. These are concrete restrictions on any later classification or construction in this family; they follow from §4.
The mathematical results are proved in the cited paper. The mission asks for machine-checked Lean proofs of their statements and for a reusable finite bi-Cayley graph interface. The setting includes the right regular action, its normaliser, the two families of candidate automorphisms, and the transitivity predicates. The proof obligations are open in this local proposal; a successful development would make the abelian argument and its underlying graph-action lemmas available for later formalizations of bi-Cayley graphs.
The right multiplication action gives only two known vertex orbits, one for each copy of . Edge transitivity alone does not name an automorphism that swaps them. Inversion is an automorphism of an abelian group, but its induced copy-swapping permutation preserves graph edges directly only in the relevant bipartite case . The paper must account for edge-transitive graphs whose connection sets initially allow edges inside the copies. For the valency bound, the absence of arc transitivity restricts how a vertex stabiliser can permute its neighbours; degree counting without those orbit constraints cannot yield . These are the points at which a proof must use the full automorphism action rather than just the visible right regular subgroup.
Lean uses the vertex type , with Sum.inl h for and Sum.inr h for . The group and graph are finite; the graph is simple and undirected by construction, and every theorem assumes it is connected. The finite sets retain the conditions , , , and . The graph's degree, rather than a separately defined cardinality formula, represents valency. “Involution” means an element of order exactly two. All graph-level transitivity predicates quantify over the full automorphism group; the normaliser appears only in the separate Proposition 2.2 milestone. The paper's exponent notation for group automorphisms is rendered as function application, while remains right multiplication.
The printed first sentence of Proposition 1.3 says every connected bi-Cayley graph over an abelian group is vertex transitive. That sentence is false: the connected generalized Petersen graph is a bi-Cayley graph over and is not vertex transitive. Proposition 4.1(b), which the paper uses to establish Proposition 1.3, includes the missing edge-transitivity condition. The Lean goal states that corrected condition explicitly. It does not add an assumption to the half-arc-transitive clause, since half-arc-transitivity already entails edge transitivity. Proposition 4.2 prints two clauses labelled “(a)”; they are treated as distinct clauses while its quotation retains the printed labels.
The definition of the graph keeps and inverse closed as data; no graph constructor silently symmetrises arbitrary sets. Transitivity is taken over actual edges or arcs, and the degree bound is checked at every vertex. Contributions to the graph-action lemmas, the normaliser result, Proposition 4.1, and the vertex-stabiliser analysis behind Proposition 4.2 are all within scope. The Cayley-graph isomorphism in Proposition 2.2(b) is outside this mission's stated milestone because it is not used by the target.
Ride-hailing, freelancing and delivery platforms are intermediaries that post a price to buyers and a price to sellers and then match the two sides. Both sides are forward-looking: an agent who arrives can wait before requesting, and an agent who requests waits until she is matched, at a cost per unit of time. Chen and Hu, Pricing and Matching with Forward-Looking Buyers and Sellers (SSRN 2859864; Manufacturing & Service Operations Management 22(4), 2020, doi:10.1287/msom.2018.0769), measure simple pricing and matching policies against an upper bound that holds for every policy. This mission formalizes that upper bound in its mechanism-design form: no incentive-compatible two-sided dynamic mechanism earns more than the expected value of a clairvoyant assignment problem in virtual values.
The bound extends the virtual-value approach of Myerson (1981) and its bilateral-trade version by Myerson and Satterthwaite (1983) from a single static trade to a market with random arrivals on both sides, waiting costs and a timing constraint that matched units change hands at the same instant.
Over a horizon , buyers arrive as a Poisson process of rate . A buyer has type : arrival time and valuation , drawn with continuous positive density and c.d.f. , independently of the arrival time. Sellers arrive as an independent Poisson process of rate , with types and costs of continuous positive density and c.d.f. . The paper assumes and that the virtual value and the virtual cost are increasing (Assumptions 1–2). Write for the realized arrivals.
A direct mechanism assigns to every buyer an outcome : the time at which she leaves, the indicator that she receives a unit, and her payment . Every seller receives likewise, now paid to her. The balancing condition requires that at every the number of buyers who receive a unit at equals the number of sellers who deliver one at . The buyer's utility is and the seller's is , with waiting costs . The intermediary's profit is
Incentive compatibility (ICd) asks that no buyer gain, in the interim expectation over all other agents, by reporting another valuation or a later arrival time ; individual rationality (IRd) asks that her interim utility be nonnegative. (ICs) and (IRs) are the seller counterparts. Problem (B′) maximizes over feasible mechanisms subject to these constraints; its value is .
The comparison object is the clairvoyant assignment problem (B): knowing in advance, choose a partial matching of buyers to sellers maximizing
its optimal value is .
For every feasible, well-defined mechanism satisfying (ICd), (IRd), (ICs) and (IRs),
with integrable. This is the last display of the proof of Lemma 1 (Online Appendix p. 4), .
Lemma S.3 (Supplemental Note p. 3), the seller envelope bound with information rent , is posed as a further theorem of the mission, the mirror image of Lemma S.1; it is not listed as a milestone.
Here (ICd′) and (ICs′) are the one-dimensional constraints in which the reported arrival time is the true one; Lemmas S.1–S.4 are stated under these weaker hypotheses, as in the paper.
Lemma 1 of the paper, for every pricing policy and matching policy , is the benchmark against which the paper's main theorem measures its waiting-adjusted fixed-price policy, and is in turn bounded by a deterministic fluid value (Lemma 2). Lemma 1 is the composition of two facts: the revelation principle (Lemma 3) and the mechanism-design bound posed here. The second carries the analytic content: it is where the envelope theorem, the exchange of integrals that turns payments into virtual values, and the timing argument appear.
The result is proved in the paper; its proofs are in the Online Appendix (Section A.2) and the Supplemental Note (Section A). No machine-checked proof of it, or of a dynamic two-sided Myerson bound of this kind, is known. A formal proof would also yield a reusable two-sided, Poisson-arrival version of the interim envelope and revenue-equivalence identities.
Each agent's type is two-dimensional, an arrival time and a valuation or cost, and arrival can only be misreported later. The relaxation to (ICd′)/(ICs′) makes the screening problem one-dimensional, but the interim expectation ranges over a random population whose size is itself random. Turning into an integral of interim payments requires the Mecke formula for the Poisson process, and the envelope argument must be carried out for interim utilities that are only known to be suprema of affine functions, using no differentiability of the mechanism. The pathwise step is combinatorial: the balancing condition at each instant pairs buyers with sellers discharged together, and those pairs must be compared with an optimal matching of (B), with duplicate types and unmatched agents handled.
A frequent first idea, bounding payments by valuations directly, gives only the first-best surplus , which is not the target; the information rents must be extracted.
The primitives are the published bilateral-trade environment MechanismDesign.BilateralTrade.Environment (densities on intervals, cdfB, cdfS, psiB , psiS , Regular Assumptions 1–2), and (B) is AssignmentGame.CoreLP.worth of the published assignment game, with sellers as rows and buyers as columns. The conventions committed to are:
WellDefined: outcomes are Borel in the listed types, interim payments are integrable, and total absolute payments are integrable. Integrability of and of the virtual-surplus sums is part of each conclusion.A trivializing formalization is ruled out: the mechanism class is not restricted beyond the paper's feasibility, the constraints are not vacuous (the null mechanism satisfies them, so ), and expectations are of integrable functions. The goal quantifies over mechanisms rather than taking a supremum, which is equivalent because the class is nonempty.
A complete development needs the Mecke formula for the Poisson-count representation, an envelope theorem for suprema of affine functions on an interval, Fubini on the type space, and an exchange argument for matchings. All of these are reusable beyond this mission. Contributions of any of them, of the milestones in any order, or of alternative proofs are welcome.
The associahedron is the -dimensional simple polytope whose faces correspond to the sets of pairwise non-crossing diagonals of a convex -gon, ordered by reverse inclusion: its vertices are the triangulations of the polygon and its facets are the diagonals. It appears in homotopy theory (Stasheff), in the theory of cluster algebras of type , and as the secondary polytope of a convex polygon. Many explicit realizations are known, and a natural question is which of them are genuinely different.
Ceballos, Santos and Ziegler (arXiv:1109.5544, Combinatorica 2014) compare realizations up to normal isomorphism: two polytopes are normally isomorphic if some linear isomorphism of the ambient spaces sends every cone of one normal fan to a cone of the other (their Definition 2.1). This notion ignores the right-hand sides of the defining inequalities and keeps only the linear structure of the facet normals, which is what the classical constructions fix.
One family of realizations is due to Hohlweg and Lange (arXiv:math/0510614, Discrete Comput. Geom. 2007): one associahedron for every sign sequence . The constant sequence gives Loday's associahedron (arXiv:math/0212126), and the alternating sequence gives, up to normal isomorphism, the Chapoton–Fomin–Zelevinsky associahedron (arXiv:math/0202004). This mission formalizes the classification of the Hohlweg–Lange family up to normal isomorphism, Theorem 4.9 of Ceballos–Santos–Ziegler.
Fix . The vertices of a convex -gon are its positions in counterclockwise order. A diagonal joins two distinct non-adjacent positions; two diagonals cross when their endpoints are distinct and alternate around the boundary. The dihedral symmetries are the maps and modulo .
For , the sign word assigns signs to the labels . The polygon places the labels from left to right, positive ones above a horizontal line and negative ones below; going counterclockwise, it visits the negative labels in increasing order and then the positive labels in decreasing order. For a diagonal with labels , the set consists of the labels strictly below the diagonal, and is obtained from it by replacing by and by . The facet of for the diagonal has normal vector , the characteristic vector of taken modulo . In coordinates this is the vector
The normal fan of is the collection of cones , one for each set of pairwise non-crossing diagonals. Two facets are parallel when their normals are negative multiples of each other. The reflection of is (all signs flipped), and its reversal is read backwards.
For all ,
Both directions are content.
The theorem gives an exact count. The number of normally non-isomorphic Hohlweg–Lange associahedra equals the number of sign sequences of length up to reflection and reversal, which is for (OEIS A005418). Together with Hohlweg–Lange's identification of the constant and alternating sequences, it shows that Loday's associahedron and the Chapoton–Fomin–Zelevinsky associahedron are not normally isomorphic for . It is one of the two classifications on which the paper's main result (Theorem 6.1, that the Hohlweg–Lange and Santos families meet only in the Chapoton–Fomin–Zelevinsky associahedron) rests.
Bergeron, Hohlweg, Lange and Thomas (Isometry classes of generalized associahedra, Sém. Lothar. Combin. 61A, 2009) classified the same family up to isometry of normal fans and obtained the same classes. As Remark 4.10 of the paper explains, that classification does not imply this one, because a normal isomorphism need not be an isometry. Combining the two gives Proposition 4.11, that normal isomorphism and isometry coincide for this family.
Theorem 4.9 is proved in the paper; no machine-checked version is known. A formalization would supply the first formal treatment of the crossing graph of polygon diagonals and its automorphisms (Lemma 2.2), of the Hohlweg–Lange normal vectors, and of linear isomorphisms of simplicial fans given by rays on diagonals.
The "if" direction needs two explicit linear isomorphisms. Their action on the sets is not diagonal by diagonal: and have different boundary edges, so the matching of diagonals goes through a mirror image and through the sign swaps of Remark 4.2. One must show that this matching preserves the cone structure, not just the set of normals.
The "only if" direction cannot compare the two polygons by label, since and order their labels differently around the boundary. A linear isomorphism of fans first has to be turned into a combinatorial object. Linearity has to be used twice: it maps rays to rays and preserves cones, which yields a crossing-preserving bijection, and it preserves opposite pairs of normals. Lemma 2.2 then reduces that bijection to one of dihedral symmetries. The remaining step is a case analysis showing that a symmetry preserving the parallel pairs, and the four distinguished diagonals they determine, is a reflection or reversal of . Comparing the multisets of normal vectors alone is not enough: every gives exactly parallel pairs with the same normals .
Fin (n + 3), diagonals are Sym2 (Fin (n + 3)), and crossing, diagonal and triangulation come from the published definition ChvatalArtGallery.FanPartition.Triangulation, used as a reference item. Signs are Bool, and is a function Fin (n - 1) → Bool. Positions and labels are kept apart: hlLabel n σ p is the label at position p.LinearEquiv that sends every cone of the first fan to a cone of the second.Join-the-shortest-queue (JSQ) is the basic load-balancing rule for a system of parallel single-server queues: every arriving customer joins a queue of minimal length. It is optimal in several senses for homogeneous servers and is the reference policy against which cheaper rules (power-of- choices, join-the-idle-queue) are measured. In the Halfin–Whitt regime, where the arrival rate is with for a fixed , Eschenfeldt and Gamarnik (arXiv:1502.00999) proved that the suitably centred and scaled numbers of queues of length at least one and at least two converge, on finite time intervals, to a two-dimensional reflected diffusion. Braverman (arXiv:1801.05121) justified the interchange of limits (the stationary distributions of the -server chains converge to the stationary distribution of the diffusion). One ingredient of that result is that the diffusion is exponentially ergodic, so it has a unique stationary distribution that is approached at a geometric rate. This mission formalizes the analytic core of that ingredient: a Foster–Lyapunov drift condition for the diffusion's generator.
Timeline. Eschenfeldt and Gamarnik (2015) proved the process-level diffusion limit, the first analysis of JSQ in this regime. Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) showed that a class of load-balancing schemes shares the same diffusion limit. Braverman (arXiv 2018, v2 2019; Math. Oper. Res. 45(3), 2020) proved tightness of the scaled stationary distributions and exponential ergodicity of the limit, which together give the interchange of limits.
The state space is the closed quadrant . For write , , . On the boundary these are one-sided derivatives, and denotes the twice continuously differentiable functions in this sense.
The diffusion limit solves
with a standard Brownian motion and a nondecreasing regulator that increases only when . For with the reflection condition , its generator acts by
The construction of the Lyapunov function uses an auxiliary integer and the fluid operator
the generator of the deterministic fluid path , . A smoothed indicator (a piecewise cubic that rises from at to at ) and two levels define the PDEs
each with the reflection condition. Their solutions are written explicitly in terms of the fluid hitting times (through the Lambert W function) and , and the curves that split into regions .
For every there exist , , a compact set and with on , as in , and , such that
The constants are unspecified and depend only on ; the statement involves no .
By the criterion of Down, Meyn and Tweedie (Ann. Probab. 23, 1995, Theorem 5.2), a drift inequality of the form (5.2) with compact and implies that the diffusion is positive Harris recurrent and exponentially ergodic in the -norm (Theorem 3 and Corollary 1 of the paper). Together with tightness of the prelimit stationary distributions (mission 1 of this series), this gives convergence of the stationary distributions of the JSQ chains to that of the diffusion. That justifies approximating steady-state JSQ performance by the diffusion.
The construction itself is reusable. Solving the fluid-model PDE and exponentiating the solution is a general route from fluid stability to exponential ergodicity of a diffusion. This mission writes that route out for one reflected diffusion with explicit hitting-time formulas.
Status: the result is proved in the paper; no part of it has a machine-checked proof. Theorem 3 and Corollary 1 are not posed, because they rest on the cited Down–Meyn–Tweedie theory and on the existence of the reflected process, neither of which Mathlib has.
The reflecting boundary rules out the first candidates. The condition excludes exponentials of linear functions such as unless . The natural candidate from the fluid model, the exponential of the fluid time needed to reach a box, has a discontinuous integrand and is not in , so cannot be applied to it. The milestone functions , are given piecewise across the curves , and the lines , through implicitly defined hitting times. Three things are hard: regularity across these interfaces, the Lambert W asymptotics as , and second-derivative bounds that hold uniformly on the unbounded domain with the stated dependence on and .
ℝ × ℝ, and is Set.Iic 0 ×ˢ Set.Ici 0. Partials are fderivWithin ℝ f Ω in the coordinate directions, which are one-sided at boundary points. is ContDiffOn ℝ 2 f Ω.WithTop ℝ, with when no solution exists, and its real value is used only where it is finite. (the curve ) is the solution of a nonlinear system whose uniqueness is Lemma 5.Mean field control studies the optimal control of a very large population of interacting agents through the limit in which the population is replaced by its distribution. The limit problem is a McKean–Vlasov (MKV) control problem: the dynamics and the cost of a representative agent depend on the law of its own state. Such problems arise in systemic risk, crowd motion, energy management and the planning of large distributed systems; the reference account is Carmona and Delarue, Probabilistic Theory of Mean Field Games with Applications I–II (Springer, 2018).
MKV control problems are rarely solvable in closed form, and grid-based numerical methods suffer from the dimension of the state. A practical alternative is to simulate a finite population on a time grid, parametrize the feedback control by a neural network, and minimize the simulated cost by stochastic gradient descent. Carmona and Laurière, Convergence analysis of machine learning algorithms for the numerical solution of mean field control and games: II — the finite horizon case (Ann. Appl. Probab. 32(6), 2022, doi:10.1214/21-AAP1715), quantify how close this computable proxy is to the true optimum. This mission formalizes the statement of their main result and of the propositions and lemmas its proof is built from.
Fix a horizon , a state dimension , a control dimension (controls take values in ), an initial law on , a drift , a volatility (not controlled), a running cost and a terminal cost ; ranges over , the probability measures with finite second moment, compared with the Wasserstein distance .
Problem 1 (the MKV problem). On a probability space carrying a -dimensional Wiener process and an independent , minimize over progressively measurable square-integrable controls
where is the law of .
Problem 3 (the -agent problem). agents with independent Wiener processes and i.i.d. initial states use a common feedback function ; the law is replaced by the empirical measure , and the cost is .
Problem 2 (the computable proxy). With and , the agents follow the Euler scheme
with i.i.d. Gaussian increments , and is the expected time-discretized cost. The feedback ranges over , the one-hidden-layer neural networks from to with hidden neurons and activation ; is -periodic, of class , with .
The standing assumptions (§2.2 and Appendix A of the paper) make affine in (A1), make differentiable in (in in the sense of the L-derivative) with Lipschitz derivatives (A2)–(A3), make strongly convex in (A4), and add the regularity (B1)–(B3), (C1)–(C3). Under them the reduced Hamiltonian has a minimizer , the Pontryagin forward–backward system has a solution with marginal flow , and for a regular decoupling field . The optimal feedback is .
for a constant depending only on the data and on , for all .
Lemma 18 (Lipschitz continuity of ), Proposition 10 (network approximation of a function and its first two -derivatives at rate on ), (C.2) (moment bounds uniform in ), Proposition 13 (stability of under feedbacks close on a ball), Lemma 19 (time regularity of the particle system) and Lemma 14 (strong error of the Euler scheme).
The theorem certifies the standard deep-learning approach to mean field control: the value computed by minimizing the simulated finite-population, discrete-time cost over networks is, up to an explicit error with separate rates for population size, network width and time step, no larger than the true MKV value. The rates also expose where the method loses: the term is a curse of dimensionality in the network step (Remark 11).
The result is proved in the paper (§3 and Appendices B–D); the proof of Proposition 7 is a modification of Carmona–Delarue, Vol. II, Theorem 6.17. None of it is formalized. A formal development would provide the first machine-checked bridge between a stochastic control problem of McKean–Vlasov type and a concrete learning architecture, and its intermediate results (moment and stability estimates for interacting particle systems, the strong error of an Euler scheme with constants independent of the number of particles, simultaneous approximation of a function and its derivatives by periodic networks) are reusable on their own.
Each step rests on research-level analysis. Proposition 7 needs the Pontryagin principle for McKean–Vlasov control, the propagation of chaos for the optimally controlled system, and the Fournier–Guillin rate for empirical measures, whose exponent and logarithmic correction at appear in the bound. Proposition 8 requires approximating the optimal feedback together with its first two derivatives in , because the time-discretization step needs regularity of the approximating network; standard universal approximation results give no control of derivatives, and the available simultaneous approximation results hold only for periodic functions, which forces a localization to a ball whose radius must be balanced against the approximation rate. Proposition 15 cannot be obtained from classical Euler estimates for a system of equations, whose constants grow with : the estimates must be done agent by agent through the empirical measure.
is Fin d → ℝ with the sup norm; every constant is existential, so all statements are norm-independent. Time is ℝ≥0 for processes. Solutions of (2.2) and (3.2) use the published Itô-process predicate Peng1990.SMP.IsItoProcess (for , with continuous paths and the natural filtration of the initial data and the noise); the backward equation of the Pontryagin system uses Peng1990.SMP.SolvesBSDE; is the published WassersteinDRO.Duality.wassersteinDistance. Problem 2 is law-level: the Euler scheme is a deterministic map of initial positions and increments, integrated against ; Lemma 14 couples it with the continuous system through the Brownian increments, as the paper does.
The hypotheses are bundled as Coeff ((A1)–(A4), (B1), (B3), (C1), with witnesses for every derivative; the L-derivative is the Fréchet derivative of the lift on ) and DecouplingField ((2.6), existence of a solution of (2.7) on some Problem-1 space, , (B2), (C2), (C3)). Disclosed readings: 's L-convexity is (A4) without and with right-hand side ; unique solvability of (2.7), uniqueness and Lipschitz continuity of are not assumed (the last is Lemma 18); Proposition 13 lets its constant depend on bounds for , as its proof does; Proposition 15 reads the first bound of (3.16) as . Infima are stated pointwise (), never as a real ⨅, and throughout. The hypothesis bundle is not vacuous: a sorry-free check exhibits the model , , , with , satisfying every assumption on any Problem-1 space. Junk values cannot trivialize the goal: the costs are Bochner integrals whose integrability follows from the assumptions, so a non-integrable cost would only make the claimed inequality harder, never vacuous.
Contributions are welcome at every level: proofs of the milestones, in particular the self-contained Lemmas 14 and 19, (C.2) and Proposition 13; infrastructure for the L-derivative, Itô's formula for the published Itô processes, empirical-measure convergence rates, and trigonometric approximation of periodic functions.
The two-dimensional directed polymer is a random walk whose paths are reweighted by a random space-time environment. Its logarithmic partition function is a discrete counterpart of the height field of the two-dimensional Kardar–Parisi–Zhang equation. At the intermediate-disorder scale, the random weighting becomes weaker as the walk grows, yet its fluctuations remain visible. Caravenna, Sun and Zygouras prove that throughout the subcritical regime , spatial averages of the centred log-partition function converge to Gaussian fluctuations described by an additive stochastic heat equation (Theorem 1.6, p. 6).
The polymer formulation matters because it is a concrete finite-path model: each partition function is an average over finitely many nearest-neighbour walks, while its limit retains the effect of disorder at every scale. The same paper treats the continuum KPZ equation separately; this mission takes its stated polymer theorem as the target. Earlier work in dimension studied a different intermediate-disorder scaling and a Wiener-chaos limit (Alberts, Khanin and Quastel, 2014). The two-dimensional result concerns a distinct regime and a different limit.
Let be the simple symmetric random walk on . Starting at , it chooses each of its four nearest-neighbour steps with probability . Write , and let be an independent copy. Their expected overlap through time is
For a fixed , the disorder strength is . The environment consists of independent, identically distributed real random variables with mean zero, variance one and finite exponential moments at all sufficiently small positive arguments. Its logarithmic moment generating function is . The law also obeys the paper's concentration assumption (1.20): convex 1-Lipschitz functions of any finite collection of environment variables have stretched-exponential deviations from a median, measured with Euclidean distance (pp. 5–6).
For a length- walk from , sum over times , exponentiate, and average over paths. The result is the partition function . Where is finite, its centring gives . A restricted function samples disorder only from the space-time sites in . Section 2 uses an early window near the start and a late window to define , its remainder , and (pp. 7–9).
At macroscopic time and position , the fluctuation field is
The floor of a vector is componentwise. In the numerator, uses the disorder strength ; the field is divided by , exactly as in (1.23).
For every and smooth compactly supported test function , Theorem 1.6 asserts
The tested limit is centred Gaussian. Its variance is , where
The milestone list follows the paper's stated results: second-moment bounds (3.2)–(3.4), higher moments for some (3.12), a left-tail bound (Proposition 3.1) and the negative and logarithmic moments it yields (3.14)–(3.16), vanishing spatial averages for two error terms (Propositions 2.1–2.2), replacement by the late-window term (Proposition 2.3), and the Gaussian limit for that term (Proposition 2.4). These are the exact result labels used in Sections 2 and 3 (pp. 8–13).
The theorem identifies the fluctuation law of the logarithm of the polymer partition function for every strictly below the critical value . The coefficient records the disorder strength in the limiting covariance, and the time reflects the two-dimensional walk's covariance convention. Without the spatial averaging and normalization, the statement would concern a different observable; the theorem characterizes a field tested against compactly supported functions (Theorem 1.6 and Remark 1.7).
The result is proved in the cited paper. This mission asks for a machine-checked proof of that known result and its curated supporting statements. The reusable output includes a finite-path polymer model on , a precise restricted partition function, the disorder concentration assumption, and the Gaussian covariance functional. The published atomic polymer model already supplies the space-time cells, steps, walk positions and log moment generating function; this mission extends that common base to the centred, spatially shifted model of this paper.
Pointwise size does not identify the limiting spatial fluctuations. The early-window partition function captures much of at a fixed site, yet its averaged logarithm vanishes at the target scale. The small remainder cannot simply be discarded: after division by the early-window function, its late-time component carries the Gaussian limit. The paper separates these effects in Propositions 2.1–2.4 and needs moment and left-tail control to keep the logarithmic expression meaningful (Sections 2–4). A direct Taylor expansion of around its mean would lose this distinction.
Lean uses finite sequences of four-neighbour steps and the Euclidean norm on . Disorder is a family indexed by positive walk times and lattice sites; the time-zero row of its ambient type is unused. The full and restricted partition functions are finite walk averages. The concentration assumption quantifies over Euclidean 1-Lipschitz convex functions and their medians. The test class of Theorem 1.6 is ; the four Section 2 propositions use . Treating “smooth” as analytic would make compactly supported tests trivial, so the Lean statement uses the smooth differentiability order.
The target additive stochastic heat observable is represented by its Gaussian law and the kernel above; the random field itself is not formalized, and the statement does not need it. The kernel takes extended nonnegative values because it is infinite on the diagonal; the diagonal has zero area in the tested covariance integral. Moments and convergence use extended nonnegative integrals. The paper assumes exponential moments only near zero, so bounds whose printed form quantifies over every are stated for all sufficiently large , avoiding default values of the logarithmic moment generating function at early indices. The spatial sums have finite support because the test functions do. Replacing the Euclidean norm by the sup norm would change the early window (a square instead of a disc), the kernel and the class of 1-Lipschitz functions in (1.20), so all of these are Euclidean. The polymer propositions are stated for every window exponent below a threshold, as in (2.2), and the passage from the time-1 lattice averages of Propositions 2.1–2.4 to the general-time integral of Theorem 1.6 is part of the proof work, not of the statements. Contributions to the polymer moments, left-tail estimate, replacement propositions and Gaussian limit all feed the stated goal.
A retailer that decides which variants of a product to stock (its assortment) trades off the revenue each variant brings against the operational cost of carrying it. The classical model of this trade-off uses the multinomial logit (MNL) model of consumer choice: a consumer who does not like what the store offers simply buys nothing (van Ryzin & Mahajan 1999). In practice a consumer who does not like what the store offers can also go elsewhere. Cachon, Terwiesch and Xu (working paper, December 2002; published in MSOM 7(4), 2005) add this consumer search to the MNL model and ask how it changes the retailer's optimal assortment.
They study two search models. In the overlapping assortment model (§3.1), a consumer who searches pays a search cost and then finds a competitor carrying every variant, so search can only reveal variants the store does not carry. This mission formalizes the paper's Theorem 6 about that model: when search is cheap, the store's best response is to carry everything.
There are variants, , and an assortment is a subset ; write for the variants the store does not carry. A consumer's utility for variant is , where is the variant's expected net utility and the shocks are independent with the zero-mean Gumbel distribution function , with scale and Euler's constant. The no-purchase option is a "faux variant" with utility . Its preference is , and is the preference of not buying.
Without search, variant has the MNL demand (2), . Following Theorem 1, put and
the probability that every option the store offers, including not buying, has utility at most . The best utility outside the store, , has a density . A consumer whose best in-store utility is searches when the expected gain exceeds the cost,
and the search threshold is the solution of , equation (4). Theorem 3 gives the resulting demand,
When the store carries everything there is nothing to search for (p. 28: "If the retailer offers the full assortment, there will be no consumer search"), so .
Variant earns margin per unit and costs to carry, where is concave and increasing (economies of scale). The retailer's profit is
As printed, the second line of (13) writes where is meant; the definition uses the latter.
If the full assortment is profitable, , then there is a such that
The threshold depends on the data but is one number for all assortments .
Theorem 6 separates the overlapping model sharply from the no-search MNL model and from the paper's independent-assortment model. In those two models every variant in an optimal assortment must earn a strictly positive profit, because dropping a loss-making variant only shifts demand to the remaining ones. In the overlapping model the assortment also controls whether consumers leave: carrying an unprofitable variant can pay because it removes a reason to search. Theorem 6 is the extreme form of this effect, stating that the motive to prevent search can override the profitability of individual variants entirely (§4.3, p. 17).
The paper gives only a short sketch of the proof. The steps it asserts without proof are the existence and uniqueness of , its monotonicity and limits in , and the explicit density . This mission states each of them as a milestone. No machine-checked version of any of these results is known.
The search threshold is defined only implicitly, through an improper integral of the density of a maximum of Gumbel variables. Each property the theorem needs (that the equation has exactly one root, that the root moves monotonically with , and that it escapes to as ) has to be read off the integral. That means controlling on the whole real line: its convergence, its strict decrease, and its limits at .
The final comparison is not a direct consequence of either. A variant's profit tends to rather than to , so the conclusion depends on the sign of , and must be chosen uniformly over all assortments.
The shared model is the definition AssortSearch.FullAssort.Model, which builds on the published MNL share RetailVariety.Structure.share. Its conventions:
Fin n, numbered from 0; the paper's variant is index . The no-purchase option is not a variant: is a separate positive real.Real.eulerMascheroniConstant.Finset (Fin n), including , whose profit is .Several formalizations would make the goal trivial or empty, and each is excluded:
A complete development needs the integral calculus of the Gumbel tail ( and its derivative in ) and the product-measure computation of the law of a maximum of independent variables. Both are reusable beyond this paper, for instance in other search and extreme-value models. Contributions are welcome on any milestone, and on helper lemmas such as the continuity of and its limits at .