Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A directed polymer in a random environment is a random walk whose paths are weighted by the disorder they encounter. The walk favors paths with large accumulated weight, and its endpoint distribution can concentrate on a small number of sites even though the number of possible paths grows exponentially. Understanding how much probability remains spread across many small endpoint masses is a basic question about localization. The distinction matters especially beyond exactly solvable polymer models, where explicit formulas for the endpoint law are rarely available. Bates and Chatterjee study this question for independent disorder in every spatial dimension under a finite exponential-moment condition Bates and Chatterjee, 2021.
The paper separates two temperature regimes using the limiting free energy. Earlier localization statements detected persistent large atoms. The target here asks whether those atoms account for all endpoint probability in a time-averaged sense. It also specifies the complementary high-temperature behavior, where a suitable vanishing mass threshold captures asymptotically none of the probability. The result is Theorem 1.1 of the preprint, restated as Theorem 6.3 Bates and Chatterjee, 2021, pp. 16, 43.
Fix . A path starts at the origin in and makes one of its nearest-neighbor moves at each integer time. The environment consists of independent, identically distributed real random variables with common law . The disorder law is nondegenerate: it is not concentrated at one number. An inverse temperature determines the weight of a path of length :
The endpoint mass function is the sum of weights of paths ending at , divided by the sum of all path weights. Thus is a probability mass function on . For , the -atoms are the sites , and is their total mass. The strict inequality matters at a threshold equal to an atom mass.
Write for , with , and . The standing condition is that this exponential moment is finite for every . The paper's Theorem A characterizes the high-temperature phase by and the low-temperature phase by Bates and Chatterjee, 2021, pp. 4–5.
The goal is both clauses of Theorem 1.1. For every positive deterministic sequence , low temperature gives
At high temperature there exists a positive deterministic sequence for which the same average converges almost surely to . The sequence in this second clause is selected independently of the realized environment. Together the clauses characterize the paper's stronger, almost-sure form of asymptotic pure atomicity Bates and Chatterjee, 2021, Theorems 1.1 and 6.3.
The milestones are fifteen statements of the paper, in the order the proof of the goal uses them:
The low-temperature conclusion rules out a residual diffuse component in the time-averaged endpoint law. A vanishing threshold may still be used to collect almost all of the polymer's probability. The high-temperature clause shows that this property distinguishes the phases under the stated moment assumption. The result strengthens a statement that only asks for a positive amount of mass on large atoms, and gives an almost-sure conclusion for the Cesàro averages Bates and Chatterjee, 2021, §§1.2.3, 6.
A formal development would supply a reusable compactification of endpoint probability measures and a checked route from its invariant laws to localization observables. The milestones expose the pieces that need separate verification, and the compactification and variational formula are reusable for the companion mission on geometric localization. The paper proves the mathematical theorem; this mission asks for its Lean proof and the supporting definitions. A compiled statement with sorry is a proof obligation, not a completed machine-checked result.
The endpoint distribution may move through space as time grows, so ordinary pointwise convergence of mass functions does not capture concentration. The compact state space used by the paper permits separated clusters to live on different copies of . Its distance identifies translated representatives and loses information about remote mass. A direct application of weak convergence to the event also fails at a threshold, because the mass-above-threshold functional is not continuous. The proof must handle its one-sided semicontinuity and the limiting behavior of the update law Bates and Chatterjee, 2021, §§2–3, 6.
Lean represents sites as Fin d → ℤ and paths as finite step sequences, so the starting point, the choices per step, and the normalization of are explicit. An environment is a measurable independent family on a probability space with common law . The unused time-zero row comes from indexing cells by ; only rows with index at least one enter the polymer. The moment condition includes the full interval , and the disorder law must be nondegenerate. Both phase predicates refer to the canonical product environment, making the classification depend on , , and rather than on an arbitrary realization.
Partitioned subprobability measures are structures of nonnegative summable functions with mass at most one. Their topology is generated by the paper's distance balls. The Borel representation identifies states at distance zero, corresponding to the paper's separation quotient . Finite partial isometries carry the degree penalty through an infimum over admissible degrees. The update uses an extended nonnegative sum before conversion to a real denominator. The intended probability law requires the almost-sure finiteness of that denominator and measurability of the update. The real-valued energy integrals require the stated moment condition; a default value for a nonintegrable integral cannot serve as the paper's expectation, and a non-measurable update would make the pushforward the zero measure, which is not the paper's object either. The infimum is taken over the set itself, never as a real infimum whose empty inner range defaults to . The intermediate results in §§3–4 and Lemma 5.1 use the standing range. Theorems 1.1 and 5.2 explicitly include . Wasserstein cost imports the published RWPI.SqrtLasso.transportCost definition.
Solvers can contribute proofs of the compactness, continuity, variational-formula, invariant-law, and atom-functional milestones, or of reusable supporting results such as Lemma 2.11 (measurability of the update) and Corollary 2.5 (when ). The strict positivity of thresholds, nondegenerate disorder, genuine probability laws, and full phase hypotheses are essential: removing any of them could make a formally easy statement unrelated to Theorem 1.1.
Two classical extremal results bound the number of edges of an -vertex graph under a single restriction. Turán's theorem (1941) says that a graph with no clique on vertices has at most edges, the edge count of the balanced complete -partite graph. The Erdős–Gallai theorem (1959) gives the maximum number of edges of an -vertex graph whose largest matching has at most edges. N. Alon and P. Frankl, Turán graphs with bounded matching number (arXiv:2210.15076v1; J. Combin. Theory Ser. B, 2024, DOI 10.1016/j.jctb.2023.12.002), combine the two restrictions. Their Theorem 1.1 determines the maximum for the clique constraint and every (mission 1 of this series). Their Proposition 3.1, the goal here, treats a whole class of forbidden graphs, the color-critical ones, when is large in terms of the forbidden graph and is large in terms of .
Color-critical graphs are the natural class for exact Turán results: by a theorem of M. Simonovits (1968), for a color-critical of chromatic number the Turán graph is extremal for -freeness once is large. Proposition 3.1 is the analogue of Simonovits' theorem under a matching constraint.
All graphs are finite and simple. For a graph , a matching is a set of pairwise disjoint edges, and the matching number is the largest size of a matching. For a graph , is -free if it contains no subgraph (not necessarily induced) isomorphic to . The chromatic number is the least number of colors in a proper vertex coloring. is color-critical if it has an edge with ; examples are complete graphs and odd cycles.
The Turán graph is the complete -partite graph on vertices with classes of sizes as equal as possible; is its number of edges. For and , the graph is the complete -partite graph on vertices consisting of classes of sizes as equal as possible whose total size is , and one further class of size . Its number of edges is .
In the Lean development, vertices of are Fin n; the shared objects of this series live in TuranMatching.Clique.Setting: is matchingNumber, is turanNum n k (Mathlib's turanGraph), is bigGraph n k s, is gNum n k s, color-criticality is IsColorCritical, and the set of vertices of degree exceeding is highDeg G s.
There is such that for every color-critical with there is with: for all and ,
The maximum is stated as an upper bound for every admissible together with an admissible graph attaining . The thresholds and are left existential, as on the page.
The proposition settles, for every color-critical and large parameters, the Turán problem with a bounded matching number, and identifies the extremal graph , which does not depend on beyond its chromatic number. For it agrees with the large- case of Theorem 1.1 of the same paper. The structural steps (few high-degree vertices, the independence of the low-degree side) are reusable in other degree-based arguments under matching constraints.
The result is proved in the paper; none of it is formalized. The mission produces, besides the goal, two classical theorems absent from Mathlib in the forms needed here: the matching-number consequence of Vizing's theorem (milestone 3) and Simonovits' exact Turán theorem for color-critical graphs (milestone 7). Milestone 7 is a cited classical theorem, not a result of Alon and Frankl; it is posed because the proof rests on it. Mathlib currently has Turán's theorem for cliques and the Erdős–Stone–Simonovits density theorem, but not the exact result for color-critical graphs.
Milestones 1, 2, 4, 5, 6 and 8 are elementary counting arguments, though each requires building matchings or explicit counts in Lean. Milestone 8 contains the paper's "easy to see" isomorphism, which in Lean is an identity between two edge counts, with .
Milestone 3 needs Vizing's edge-coloring theorem (a graph of maximum degree is properly -edge-colorable). A naive greedy edge coloring gives only colors, which bounds the edge count by about and is too weak for the comparison in milestones 4 and 5.
Milestone 7 is the hardest item. The density version (Erdős–Stone–Simonovits) gives edges only; the exact bound for color-critical requires Simonovits' stability method, an argument that an almost-extremal -free graph is close to followed by a cleaning step that uses the critical edge.
Graphs are SimpleGraph (Fin n) with decidable adjacency; edges are counted by #G.edgeFinset. The matching number is the supremum, in , of the edge counts of matching subgraphs; the set is nonempty and bounded, so this is the true maximum and not a junk value. is defined as the edge count of the graph , not by a closed formula. Chromatic numbers live in (Mathlib's chromaticNumber), both in the definition of color-critical and in the hypothesis . -freeness is Mathlib's SimpleGraph.Free (no subgraph copy). The vertex type of is any finite type in the lowest universe.
Conventions committed to:
A formalization that states only the upper bound, without an attaining graph, or that places the existential after is fixed as a constant independent of , or that defines or so that they take junk values, is a different and weaker statement and is ruled out.
Infrastructure that would be reusable beyond this mission: a matching-number API on Mathlib's Subgraph.IsMatching (in particular for and the behaviour under induced subgraphs); Vizing's theorem; and Simonovits' theorem. Contributions of any of these, and of partial results toward milestone 7 (for example the case ), are welcome.
A lower bound on the Ricci curvature of a Riemannian manifold and an upper bound on its dimension can be expressed without coordinates in two ways. The Bakry–Émery condition is a property of the heat semigroup and its generator: the iterated carré du champ dominates (Bakry–Émery 1985). The Riemannian curvature-dimension conditions and are properties of a metric measure space, defined through optimal transport (Ambrosio–Gigli–Savaré 2014). A basic test for any notion of "Ricci curvature at least , dimension at most " is its behaviour under products: on a product of manifolds, Ricci curvature bounds combine and dimensions add.
The paper of Ambrosio, Gigli and Savaré (arXiv:1209.5786) proves that and coincide on a natural class of Dirichlet-form spaces, and draws from it, in its §5.1, two tensorization results. The first (Theorem 5.1) is the stability of under products. This had been proved in Ambrosio–Gigli–Savaré 2014 only under a nonbranching assumption on the factors; the equivalence removes that assumption. The second (Theorem 5.2) is the dimensional statement: the product of two Riemannian Energy measure spaces satisfying and satisfies , the bound on the dimension of the product that the smooth case predicts.
Let be a complete separable metric space with a Borel measure . A Dirichlet form is a quadratic, -lower semicontinuous, Markovian functional with dense domain . Its generator is defined by for all , and its heat flow solves . The carré du champ is the density of . For , is the weak form (2.33) of , written through the functional .
The intrinsic distance is . An Energy measure space (Definition 3.6) is a strongly local Dirichlet form on a space whose metric is , with full-support measure and an exhausting function; a Riemannian Energy measure space (Definition 3.16) is in addition upper regular, and every with has a continuous version. An space (Definition 3.1) is a length metric measure space with the growth bounds (MD.b) and (MD.exp) on which the relative entropy has an gradient flow in .
The product (5.1) of and is with
and the Cartesian Dirichlet form (5.2) is
where and .
If and are Riemannian Energy measure spaces satisfying (MD.exp), and , then
In the parametrization the product satisfies with .
implies . 2. Theorem 5.1, p. 60: the product of two spaces is . 3. The elementary inequality of p. 62: for positive and nonnegative . 4. Lemma 5.3, p. 62: under the fibrewise regularity (5.9), for the RCD factors and their Cheeger forms fixed in §5.1.
Theorem 5.1 shows that is closed under products with no nonbranching condition on the factors, the hypothesis under which Ambrosio–Gigli–Savaré 2014 had obtained it. Theorem 5.2 gives the dimensional version for Dirichlet-form spaces, : a product of spaces of finite dimension has finite dimension, with the bound of the smooth case, while the condition alone loses all dimensional information.
Both results are proved in the paper; none of them, nor the objects they are stated for, has a machine-checked proof. The mission produces a Lean statement of the Cartesian Dirichlet form and of the product structure, the statements of the two tensorization theorems, and the characterization of that drives Theorem 5.1. A formal proof would also check the measure-theoretic steps that the paper takes for granted: the measurability of , the Fubini arguments of Lemma 5.3, and the identification of the domain of the Cartesian form (cited from [Ambrosio–Gigli–Savaré 2014], Theorem 6.18).
The obvious argument works fibre by fibre: apply to each section and to each , and add. This fails as stated, because on does not act on the sections separately: is an average over of the semigroup of applied to , weighted by the heat kernel of , so fibrewise gradient and Laplacian bounds have to be transported through this average. For Theorem 5.2 a second step is not fibrewise at all: before any dimensional estimate, the product has to be shown to be a Riemannian Energy measure space whose intrinsic distance is the product distance, which in the paper goes through Theorem 5.1 and hence through the equivalence of Theorem 4.17.
Functions on are X → ℝ, and membership is MemLp f 2 m; every object is invariant under -a.e. equality. Dirichlet forms take values in and are off . Heat flows are passed as functions pinned by the predicate IsHeatSemigroup. is a predicate on a density. is parametrized by ; is when either factor has . The product is WithLp 2 (X × Y), whose metric is the distance (5.1); the plain type X × Y would carry the max-metric. The second term of (5.2) uses , correcting the printed . Factors are σ-finite.
Theorem 5.2 assumes (MD.exp) for both factors: its proof invokes Theorem 5.1, whose factors must be , which a Riemannian Energy measure space with is only under (MD.exp). In Corollary 4.18, the minimal weak gradient is written as , the identity that (QCh) asserts. Lemma 5.3 carries the RCD and Cheeger-form assumptions established at the opening of §5.1. The elementary inequality retains the printed ; applying it to signed Laplacians requires its all-real extension.
The goal is not met by stating on the product with : that is , a strictly weaker claim; nor by defining the product form through the Cheeger energy of instead of (5.2).
A complete development needs the Cartesian form's domain theorem, a pointwise version of the heat semigroups, Theorem 4.17 of the paper and the converse from [Ambrosio–Gigli–Savaré 2014]. The product layer (sections, Cartesian form, Lemma 5.3) is reusable for any tensorization argument on Dirichlet forms. Proofs of the elementary inequality and of Lemma 5.3 are the natural first contributions.
A constraint satisfaction problem (CSP) asks whether variables can be assigned values so that every constraint of a given instance holds. Feder and Vardi conjectured, and Bulatov and Zhuk proved in 2017, that every CSP over a finite set of relations is either polynomial-time solvable or NP-complete, and that the answer is governed by the polymorphisms of the relations: the functions that map tuples of satisfying assignments, coordinate by coordinate, to a satisfying assignment.
A promise CSP (PCSP) relaxes the question. Each constraint comes as a pair of relations ; the input is promised to be satisfiable with every constraint read as , or unsatisfiable even with every constraint read as , and the task is to tell which. Approximate graph colouring ("is this 3-colourable graph 100-colourable?") and -SAT are of this kind. Austrin, Guruswami and Håstad (2017, doi:10.1137/15M1006507) showed that -SAT is NP-hard via polymorphisms; Brakensiek and Guruswami extended the polymorphism view to general Boolean PCSPs and proved a dichotomy for symmetric Boolean families (arXiv:1704.01937v2, SODA 2018, SIAM J. Comput. 2021). Later work by Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970) built the general algebraic theory of PCSPs on this foundation.
This mission takes one ingredient of the dichotomy: the tractable side for two polymorphism families that have no counterpart among tractable CSPs, the Majority and the Alternating-Threshold functions. The paper solves both with the same linear programming test.
The domain is . A finite family of promise relations is , with finite and . An instance has variables and clauses ; a variable may occur several times in a clause. reads each clause with , and with . Since , satisfiability of implies that of .
A function is a polymorphism of if for every and all the tuple lies in . For odd ,
The LP relaxation of has one unknown per variable, and for every clause of it requires to lie in the convex hull of . The §3.2 algorithm loops over the variables: it fixes and re-solves the LP, then, if that is infeasible, fixes and re-solves, and outputs "unsatisfiable" if both are infeasible. If every variable passes, it outputs "satisfiable". In Lean the answer is the predicate LPAlgAccepts 𝔸 X: the LP is feasible and, for each , it has a solution with or one with .
If for every odd , or for every odd , then for every instance
No symmetry of the relations is assumed.
The theorem shows that the Majority and Alternating-Threshold cases of Theorem 3.2 are tractable. Since is fixed, the LP has size linear in the instance, so linear programming decides in polynomial time. Unlike the Zero, One, AND, OR and Parity cases of §3.1, these families cannot be handled by sandwiching a tractable CSP between and : footnote 12 of the paper observes that the closure of or under identification of variables is not a clone. The tractable half of the paper's symmetric Boolean dichotomy (Theorem 2.16) depends on this result. Later work replaced this LP by the Basic LP and BLP+Affine relaxations (Brakensiek–Guruswami 2019, Barto et al. 2021).
The result is proved in the paper; to our knowledge it has no machine-checked proof. The formal content is a finite-dimensional rational convexity argument plus a counting argument on columns of polymorphism inputs. Related platform work: the published PCSPBLPAff.Symmetric.theorem_2 and theorem_3 concern the BLP+Affine algorithm with symmetric or block-symmetric polymorphisms. That is a different relaxation, and is not symmetric.
Completeness is immediate. Soundness is where the difficulty lies. The obvious approach, rounding an arbitrary LP solution, fails. For Majority, a coordinate equal to has no nearest integer, and the LP may admit no solution without such coordinates unless one uses the per-variable solutions the algorithm found. For Alternating-Threshold, there is no fixed threshold at all, and a single LP solution gives no rule for rounding a fractional coordinate. Two further points need care. Getting from a fractional point back to a polymorphism application needs a polymorphism of an arity that depends on the denominators of the hull weights, so a single fixed arity does not suffice. In the Alternating-Threshold case, as printed, the paper pads the inputs with an arbitrary point of , and that step fails at coordinates where both solutions equal or ; the padding point has to come from the support of the hull weights.
The domain is Bool. is a pair 𝔸 𝔹 : RelStruct τ ar Bool with [Fintype τ] and 𝔸.rel R ⊆ 𝔹.rel R, and instances, satisfiability and polymorphisms come from the published PCSPBLPAff_Symmetric_Setting. Coordinates are 0-based (Fin L), so the sign of is . The LP is stated over ; an LP with rational data is feasible over exactly when it is feasible over . The hull condition uses , never . The acceptance predicate also requires the LP itself to be feasible, which matters only for instances without variables. The hypothesis is a disjunction of two universal statements (" for all odd , or for all odd "), not "for every odd , one of the two". A formalization that drops the hull constraint, replaces by in the LP, or lets the acceptance predicate be satisfied without solving the LP would make the theorem trivial or different, and is ruled out by the definitions here.
Out of scope: polynomial running time and the printed conclusion "PCSP(Γ) is polynomial-time tractable" of Theorem 3.2; the polynomial-time solvability of linear programs; the Zero/One/AND/OR/Parity cases (Lemma 3.1, which invokes Schaefer's theorem); and the non-idempotent ("anti-") cases, which go through the reduction of Lemma 2.13(2). The Remark on p. 15 says the algorithm decides but does not find a solution. Only the decision is formalized.
Infrastructure needed: finite convex combinations over , a perturbation lemma for avoiding finitely many hyperplanes in the rational simplex, and counting identities for and on block inputs. The perturbation lemma and the counting identities are reusable beyond this mission. Proofs of any milestone, and alternative arguments (e.g. via the affine-hull algorithm in the Remark on p. 14), are welcome.
In 1997 Maldacena conjectured that super-Yang–Mills theory with gauge group is equivalent to type IIB string theory on (hep-th/9711200). The paper of Gubser, Klebanov and Polyakov (hep-th/9802109), together with Witten's paper of the same year (hep-th/9802150), turned the conjecture into a computational rule: the generating functional of connected gauge theory correlators equals the minimum of the supergravity action subject to boundary conditions at the edge of anti-de Sitter space. The concrete outputs of the paper are two-point functions and operator dimensions, read off from the small-momentum, non-analytic behaviour of solutions of a radial ordinary differential equation.
The mathematical core is classical analysis of modified Bessel functions: which solution is regular in the throat, how splits into , and what the leading non-analytic term of a logarithmic derivative is as the momentum tends to zero. The physical headline, Eq. (46), is that operators dual to massive string states at level acquire dimensions growing like at large 't Hooft coupling.
Let be the AdS radius and the radial coordinate, with the boundary at and the horizon at . For a bulk field with Euclidean momentum , the radial equation is
with for the massless s-wave (Eq. (20)), for the -th partial wave (Eq. (34)), and for a scalar string state of mass (Eq. (40)).
The modified Bessel functions are defined for and real by
The normalised radial profile is , the flux factor is , and the two-point function is (Eq. (26)). For a level- string state , , the Bessel order is (Eq. (41)) and the dimension of the dual operator is (Eq. (45)).
For , with , and : there is a function real-analytic at with
, and as .
Solutions of the radial equation (Eqs. (22), (35), (39)–(41)), regularity selecting (text after (23)), the connection formula (Eq. (42)), the flux factor for integer order (Eqs. (36)–(37)) and non-integer order (Eqs. (43)–(44)), the relation (Eq. (41)) and the asymptotics (45)–(46).
The computation is the prototype of the AdS/CFT dictionary between bulk masses and boundary dimensions, in five bulk dimensions. The massless case reproduces the non-renormalisation of dimensions of operators dual to supergravity fields; the massive case is the first prediction that unprotected operators acquire dimensions growing without bound at strong coupling.
The mathematical statements are classical, but their formalisation needs modified Bessel functions of real order, their connection formula, and asymptotic expansions near with logarithmic terms — material not currently present in Mathlib as far as the drafter checked. None of the statements below has a machine-checked proof yet.
Corrections to the source. Numerical exploration by the drafter (not machine-checked) indicates that the sign of the logarithmic coefficient printed in Eqs. (36)–(37) is reversed (the standard expansion has in ), and that Eq. (27) is inconsistent with Eq. (37) at : the correct leading term for is . The partial-wave milestone is stated with the corrected coefficient. Eq. (44) (non-integer order), which carries the paper's main prediction, agrees with the standard expansions.
The flux factor is a logarithmic derivative of evaluated at the boundary. The leading term of near is a pure power, which contributes only an analytic part; the physical information sits in a subleading term of relative size (or for integer order). Extracting it requires the full series structure of near , not only its leading asymptotics, together with control of the remainder uniformly enough to pass through a logarithm and a derivative.
All functions are real-valued; is defined by its integral representation and by its power series, both used only for . The convention is realised by Lean's . "An analytic function of plus a term plus " is encoded as: there exists with AnalyticAt ℝ A 0 such that the difference is little- of the given power as . Because is not an even integer when (and because of the logarithm in the integer case), the coefficient of the leading non-analytic term is uniquely determined, so the statements are not vacuous. The physics steps (the identification of generating functionals, Eq. (12), and the Fourier transform to position space) are not formalised: the two-point function is defined through the flux factor, Eq. (26). Welcome contributions: general facts about and (differential equation, positivity, asymptotics, series near ), reusable beyond this mission.
In the adversarial multi-armed bandit problem a learner repeatedly picks one of arms and observes only the loss of the arm it picked, while an adversary chooses the losses, possibly reacting to the learner's past choices. The minimax pseudo-regret of this problem is of order after rounds, and the classical algorithm Exp3 achieves only (Auer et al., 2002). Online mirror descent with a Tsallis-entropy regularizer interpolates between Exp3 (negative Shannon entropy) and the log-barrier, and the choice of the Tsallis parameter decides which logarithmic factor appears in the bound.
Timeline:
There are arms and rounds . At round the learner draws an arm from a probability vector in the simplex , the adversary fixes a loss vector , which may depend on and on the adversary's internal randomization, and the learner observes . The pseudo-regret is
with the expectation over both sources of randomness.
The importance-weighted (IW) estimator is and . For and the α-Tsallis regularizer is
with symmetric regularization . α-Tsallis-INF is online mirror descent:
and the potential is . The pseudo-regret splits into a stability term and a penalty term , where is a best arm in expectation in hindsight. Theorem 3 uses the learning rate
The goal fixes the constants of the paper; it holds against every randomized adaptive adversary.
Theorem 3 at the boundaries: (negative-entropy regularizer, rate , bound ) and (log-barrier, rate , bound ).
Theorem 3 gives one anytime bound for the whole Tsallis family. At it is , the minimax rate, without knowledge of ; at it recovers the Exp3 rate and at the log-barrier rate, with constants matching Abernethy et al. without tuning the learning rate to the horizon. It is the adversarial half of the paper's study of α-Tsallis-INF, whose stochastic half (Theorem 4) shows why is the only value that is optimal in both regimes.
The result is proved in the paper. As far as is known, no machine-checked proof of any Tsallis-INF or Poly-INF regret bound exists. The mission produces a formal model of randomized adaptive adversaries together with online mirror descent for bandits, and formal stability and penalty lemmas for the Tsallis family, which are the standard building blocks of later best-of-both-worlds analyses.
The obvious route, bounding the regret of each fixed seed and action sequence and averaging, fails: the IW estimates have second moments of order , which are unbounded, and only their expectation under the learner's own sampling is controlled. The stability term therefore has to be bounded in expectation, for a regularizer whose convex conjugate has no closed form for general . The penalty term involves a learning rate that changes every round, so the potentials of consecutive rounds are not directly comparable. The expectation of the run is over a law that couples the adversary's seed with the learner's random actions, so every step that the paper writes as "take expectations" has to be carried out over that law.
Two features of the printed proof need care. Theorem 3's learning rate is at , where is undefined, and for small it increases between and , while Lemma 12 part 1 assumes a non-increasing sequence of positive learning rates. A complete proof of the goal has to handle these first rounds.
Arms are Fin K with ; action sequences are maps Fin K with and unused. The adversary is a seed drawn from a probability measure together with one published RegretBandits.Adversarial.Adversary K per seed (losses in , depending on past actions only), with losses measurable in the seed. The expectation of a quantity at horizon is . The learner's weights are an argmax predicate on a weight function: for every round, the objective is maximized over the simplex. This is the paper's rule whenever , and at it makes the minimizer of , the uniform vector, which is the initialisation of online mirror descent. No hypothesis on the weights is added beyond this rule. is a real supremum over the simplex, attained because the simplex is compact and nonempty. Powers are real powers; is the natural logarithm.
The goal and the milestones take (the page: ); the boundary values are separate companion theorems, with the limiting regularizers of §3.2 and the limiting learning rates of p. 12, and the log-barrier companion restricts the weights to the open simplex. Lemmas 12 and 20 are stated, as on the page, for any loss estimator that is conditionally unbiased given the seed and the past, depends on the actions through its own round only, and is measurable and integrable under the run law. The page prints the limit of the learning rate as ; the true limit carries an extra factor under the root, and the companion uses the true limit. In Lemma 20 the term sits inside the expectation, since is random under an adaptive adversary.
A trivializing formalization is ruled out: the weights are not chosen by a choice function, and an algorithm whose weights are arbitrary at is excluded because the predicate pins .
A complete development needs: convex conjugates of separable regularizers on the simplex, the stability argument via a second-order bound, telescoping of potentials, unbiasedness of IW estimators under the run law, and elementary real-analysis estimates (Lemma 14, the simplex maximum). The run law, the IW estimator and the potential are reusable in the companion missions on Theorem 1 and Theorem 4. Contributions to any milestone, and to reusable lemmas about the run law, are welcome.
A barycenter summarizes several objects by minimizing a weighted sum of distances to them. For probability histograms, ordinary coordinatewise averages depend strongly on how the bins are labeled. Optimal transport instead lets mass move between bins and charges for those moves through a cost matrix. The resulting Wasserstein barycenter can reflect the geometry of the bins: nearby bins can exchange mass at a lower cost than distant ones. Peyré and Cuturi use this construction in their treatment of variational transport problems, including shape interpolation and the representation of a measure as a barycenter of other measures. The finite histogram problem in this mission is the entropically regularized version developed in §9.2 of their textbook.
The computational question is how to connect three ways of describing the same solution: a histogram that is the barycenter, transport matrices coupling it to the inputs, and vectors of dual potentials. Proposition 9.1 on p. 530 identifies the dual potentials behind the scaling factors of the optimal transport matrices. This is the second proposition numbered 9.1 in the chapter; the one on p. 519 concerns derivatives with respect to histograms.
There are input histograms. Source has bins and a probability vector , while the barycenter has bins. The real matrix gives the cost of transporting a unit of mass from barycenter bin to input bin . A weight vector has nonnegative entries summing to one; denotes the probability simplex on bins. The unregularized barycenter problem (9.10) minimizes over , where is the minimum transport cost with marginals and .
For a regularization parameter , the entropic transport cost minimizes over nonnegative coupling matrices with row marginal and column marginal . Here and , with . The Gibbs kernel is .
The book also writes the regularized barycenter as a weighted KL projection. Its variables are the matrices ; each matrix has column marginal , and every matrix has the same row marginal. That shared row marginal is , so the optimization can be expressed without carrying as a separate variable. The generalized matrix divergence is , using the continuous value at . See (9.15)–(9.17) in Peyré and Cuturi.
The goal is Proposition 9.1 on p. 530. The dual variables are row potentials and column potentials . They maximize
The theorem asserts that the primal and dual optima are attained, that every optimal primal family and every optimal dual family satisfy
and that the dual maximum is the minimum value of the entropic barycenter objective (9.15). The milestone targets are the scalar and matrix versions of the KL conjugate (9.22), followed by the closed form maximizer of one block, corresponding to the update (9.18). These statements retain the source's finite matrix setting and are listed in the order in which their concepts enter the dual formulation.
The scaling formula turns the optimal couplings into a product of a row factor, a fixed positive kernel, and a column factor. It identifies those factors with exponentials of dual potentials and gives a constrained maximization problem whose value is the entropic barycenter cost. Thus a solver can reason about the couplings, the barycenter marginal, or the potentials while referring to one theorem that connects them. The book uses the same variables to describe the iterative scaling updates on pp. 529–531 and later illustrates barycenters of shapes and surface measures; those applications depend on interpreting the matrix factors correctly. Peyré and Cuturi give the mathematical proposition and its argument. A complete Lean proof of the proposition and its supporting KL identities is the work this mission calls for; the statements here are draft targets rather than machine-checked solutions.
The potential program is a constrained optimization problem, while the transport problem constrains nonnegative matrices by two kinds of marginals. Equality of their optimum values must preserve the normalization constants in generalized KL. The exponential form alone does not establish that a proposed matrix has the required marginals, nor does a feasible matrix alone identify dual potentials. In addition, the assertion concerns every optimizer: a choice of zero source weight would leave that source's coupling unconstrained by the objective, and a zero target entry would put a logarithmic column update on the boundary. These are substantive edge cases of the formulas, not merely notation.
Lean uses Fin S, Fin n, and Fin (n_s) for the finite index sets; these are zero based versions of the book's one based indices. Histograms and potentials are real vectors, costs and couplings are real matrices, and the Gibbs kernel is defined entrywise. The theorem requires , , strictly positive weights that sum to one, and strictly positive input histograms that each sum to one. The strict positivity of weights and input entries is an explicit restriction beyond (9.15)–(9.21), needed for a statement about every optimizer and finite logarithmic potentials. Entropy uses on nonnegative couplings. The shared row marginal is constructed by the constraints on the ; it is not a free histogram unrelated to them.
The definition layer includes finite matrix pairing, entropy, generalized KL, the Gibbs kernel, feasibility, and primal and dual objective functions. The KL conjugate identities and the block optimizer are separate theorem targets so they can be reused in other entropic transport developments. The main theorem asserts primal and dual attainment as well as their relationship; it does not assume strong duality or an optimal scaling as an input. The page has slips in the dimensions of the marginal equations and a missing subscript on in (9.17); the Lean statements use the dimensions specified by . The optional cost-gradient Proposition 9.2 on pp. 519–520 and the block update (9.19)–(9.20) lie outside this proposal.
Linear sets are point sets of a finite projective space defined by a subspace over a subfield. They appear throughout finite geometry, for instance in the study of semifields and, through the correspondence studied by Sheekey and Van de Voorde (arXiv:1806.05929), maximum rank distance (MRD) codes; see Polverino's survey (doi:10.1016/j.disc.2009.04.007). In these applications one needs to decide when two linear sets are the same up to a collineation, which can be difficult (Csajbók–Zanella, arXiv:1501.03441; Csajbók–Marino–Polverino, arXiv:1607.06962). The natural candidate answer, "when their defining subspaces are in the same orbit of the semilinear group", is only a sufficient condition: on the projective line there are maximum scattered subspaces in different -orbits defining equivalent linear sets (the two papers just cited).
Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590, Combinatorica 41 (2021)) introduced -scattered subspaces, a generalisation of scattered subspaces, and showed in their §4 that for the sufficient condition is also necessary. This mission formalizes that result, Theorem 4.5.
Let be finite fields and let be an -dimensional vector space over ; it is also a vector space over . The projective space has as points the one-dimensional -subspaces , .
For an -subspace of , the -linear set of is
of rank .
For , the subspace is -scattered (Definition 1.1) if and every -dimensional -subspace of satisfies . The linear set of an -scattered is called -scattered (Definition 4.1); for it is scattered with respect to lines.
The group consists of the bijective additive maps of that are semilinear: for some field automorphism of . Each induces a collineation of , , and these collineations form . Two linear sets are -equivalent if for some ; two subspaces are -equivalent if for some .
For and -scattered -subspaces , of ,
The result. Theorem 4.5 says that, for , an -scattered linear set remembers its defining subspace up to a scalar and up to the semilinear group. The equivalence problem for such linear sets, a geometric question about point sets, becomes the equivalence problem for subspaces, which is algebraic and can be attacked with linearized polynomials. Through the correspondence of Sheekey and Van de Voorde between maximum -scattered subspaces and MRD codes, the paper derives from it (Theorem 4.10, not part of this mission) that two -linear MRD codes with minimum distance , , and left idealiser isomorphic to are equivalent if and only if their associated linear sets in are -equivalent. Lemma 4.4 and Proposition 4.3 are of independent use: they say that the rank and, up to scalars, the subspace of any linear set scattered with respect to lines are invariants of the point set.
The formalization. The theorem is proved in the paper; no part of it, nor any statement about linear sets over a field extension, is machine-checked in Mathlib. The mission produces a formal model of linear sets, of the semilinear group and of its induced collineations that later finite-geometry missions can reuse, together with formal proofs of the four milestones. Proposition 4.2 is quoted from [5] without proof in the paper, so formalizing it means formalizing Bonoli and Polverino's argument.
The "if" direction is a direct computation, . The obvious approach to the converse, reconstructing from point by point, fails because a point of determines only up to a scalar of , and these scalars can a priori differ from point to point. Without the condition they really do differ: for the theorem is false. The step that needs is the rigidity of the intersections of with two-dimensional -subspaces, which is where the quoted result on linear sets of size on a projective line enters. Proposition 4.2 itself is a counting statement about point weights on and is not available in any library.
F, K with [Algebra F K]; is Fintype.card F. is a finite-dimensional K-module with a compatible F-module structure ([IsScalarTower F K V]), and is Module.finrank K V.IsHScattered F K h U includes the range and the spanning condition , as in Definition 1.1. With this forces .K-submodule K ∙ u; linearSet F K U is a Set (Submodule K V) and is its Set.ncard.f : V ≃+ V for which some σ : K ≃+* K gives f (a • v) = σ a • f v. The collineation sends a subspace to Submodule.span K (f '' P). The image is the set f '' U, and is (λ • ·) '' W with .Welcome contributions: the general theory of linear sets (point weights, with equality iff is scattered), the fact that a semilinear map of maps -subspaces to -subspaces, and the counting argument behind Proposition 4.2. These are reusable for every linear-set mission.
Two of the oldest results in extremal graph theory bound the number of edges of a graph under a single structural restriction. Turán's theorem (Turán 1941) determines the maximum number of edges of an -vertex graph with no complete subgraph on vertices. The Erdős–Gallai theorem (Erdős and Gallai 1959) determines the maximum number of edges of an -vertex graph with no pairwise disjoint edges; for it is , attained by a clique on vertices plus isolated vertices, or by vertices joined to everything.
N. Alon and P. Frankl (arXiv:2210.15076, published in J. Combin. Theory Ser. B, 2024, DOI 10.1016/j.jctb.2023.12.002) impose both restrictions at once and determine the maximum for all values of the parameters. Their answer is again the larger of two explicit constructions, and each of the two classical theorems is recovered as a degenerate range of theirs. The question belongs to a line of work on generalized Turán problems with an additional bound on the matching number, which has continued since this paper with other forbidden subgraphs in place of the clique.
All graphs are finite and simple, on the vertex set .
A graph on vertices is admissible for when its clique number is at most and its matching number is at most . Both constructions are admissible when : is -colourable, and every edge of it meets the vertices of the small classes; the Turán graph on of the vertices, with the other vertices isolated, has no disjoint edges.
For and ,
stated as an upper bound for every admissible graph together with an admissible graph attaining it.
The milestones follow the proof of §2 of the paper, in attack order:
A companion item records the paper's parenthetical remark: for the maximum is .
The theorem settles the edge-extremal problem for the two most basic graph parameters, clique number and matching number, jointly and for every admissible parameter value. It contains both classical theorems: when the matching condition is void and the answer is Turán's ; when the clique condition is void and the answer is the Erdős–Gallai bound. The two extremal constructions show that both regimes genuinely occur, and the threshold between them depends on , and together. The same paper's Proposition 3.1 extends the answer to every colour-critical forbidden graph for large and , and the present theorem is the base case of that programme.
The theorem is proved in the paper; it has not been formalized. Mathlib has Turán's theorem (SimpleGraph.CliqueFree.card_edgeFinset_le), Tutte's theorem on perfect matchings, and extremal-graph infrastructure (SimpleGraph.IsExtremal), but no Tutte–Berge formula, no Gallai–Edmonds decomposition, and no Erdős–Gallai theorem for matchings. A formal proof would add the Tutte–Berge formula in the barrier form used here, a reusable Zykov symmetrization argument, and the first machine-checked proof of the Erdős–Gallai matching bound as a special case.
The arithmetic of the proof (milestones 8–10) is short. The difficulty is concentrated elsewhere.
First, the proof starts from a barrier whose removal leaves only odd components with equal to the matching number. This is the Tutte–Berge formula sharpened to a maximal barrier, all of whose components are factor-critical. Mathlib's Tutte theorem covers perfect matchings only, so the deficiency version and the structure of maximal barriers have to be built.
Second, Lemma 2.1, Claim 2.3 and Lemma 2.2 are surgery on an extremal graph. Each modifies the graph (copying a neighbourhood, swapping two classes of in the neighbourhood of a component, merging two components) and must re-verify three things: the number of edges does not decrease, no clique on vertices appears, and the matching number stays at most . The matching bound is re-verified through the barrier, so the components of the modified graph have to be tracked, and the extremality hypothesis has to be used in the right form. In particular, the paper's printed proof of Lemma 2.1 shows only that non-adjacency is transitive on and that non-adjacent vertices of have equal degree; the full "same neighbourhood" conclusion needs a further argument from extremality.
Third, the barrier equation of p. 2 is written with , which presumes that an extremal graph has matching number exactly ; the paper does not prove this, and a solver who wants to chain the milestones needs it.
Graphs are SimpleGraph (Fin n); edge counts are #G.edgeFinset. Clique number at most is G.CliqueFree (k + 1). The matching number is the supremum, in ℕ, of the edge counts of matching subgraphs (Subgraph.IsMatching); the set is nonempty and bounded, so the supremum is a maximum, and the companion sanity file proves iff every matching has at most edges. is Mathlib's turanGraph n k. is an explicit graph on Fin n (vertex in class , all others in class ), and is defined as its edge count, not by a closed formula, so the identity of milestone 8 is a statement about the graph. Extremality is Mathlib's IsExtremal for the admissibility property. The maximality of in Lemmas 2.1 and 2.2 and Claim 2.3 ranges over all extremal graphs together with all their odd barriers of value , because the paper chooses together with .
One hypothesis is added to the paper's statement: . The paper says "every ", but has classes of total size , which is impossible for and , and no nonempty graph has clique number at most . Lemmas 2.1, 2.2 and Claim 2.3 keep the paper's barrier value as a hypothesis, while the barrier milestone itself is stated with .
The goal is an upper bound together with an attaining graph; an upper bound alone would be a weaker theorem. The surgery lemmas carry extremality as a hypothesis, never a hypothesis on the edge count that would presuppose the answer.
Contributions welcome beyond this mission: the Tutte–Berge formula and Gallai–Edmonds decomposition for SimpleGraph, the matching number as a reusable definition, and the Erdős–Gallai matching theorem.
Scattered subspaces are a central object of finite geometry. An -subspace of an -vector space is scattered when every one-dimensional -subspace meets it in -dimension at most one. They give the largest scattered linear sets of projective spaces, and through them constructions of two-intersection sets, two-weight codes, strongly regular graphs and, most prominently, maximum rank distance (MRD) codes. Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2) generalise the notion to -scattered subspaces, which meet every -dimensional -subspace in -dimension at most , prove the dimension bound , and ask when it is attained.
When divides , direct sums of known examples reach the bound (Theorem 2.6 of the paper). For other values of the paper introduces a duality, the Delsarte dual, which turns a maximum -scattered subspace of one space into a maximum -scattered subspace of a space of another dimension. The name comes from Delsarte's duality on MRD codes, which the paper shows corresponds to it (Theorem 4.12). This mission is about that duality: Theorem 3.3 of the paper.
Let be finite fields, with . Write for an -dimensional -vector space; it is also an -space of dimension .
Definition 1.1. For , an -subspace of is -scattered if and every -dimensional -subspace of satisfies . It is maximum -scattered if no -scattered subspace of has larger -dimension. The paper's Theorem 2.3 shows that an -scattered subspace either has dimension and defines a subgeometry, or has dimension at most .
The setting of §3. Let be a -dimensional -vector space, written as a direct sum of -subspaces with and . Let be a -dimensional -subspace of with and , and put
an -subspace of . Every -dimensional -subspace of with arises in this way (Lunardon and Polverino, cited as [21, Theorems 1, 2] in the paper). Let be a non-degenerate reflexive sesquilinear form with companion automorphism (linear in the first argument, ) which takes values in on ; equivalently, extends a non-degenerate reflexive form . Write , an -dimensional subspace. The Delsarte dual of (Definition 3.2) is the -subspace
a subspace of a -dimensional -space.
Suppose is a maximum -scattered -subspace of of dimension , and . Then
The statement holds for every admissible choice of the embedding and of .
The result. Theorem 3.3 converts a maximum -scattered subspace of of dimension into a maximum -scattered subspace of . For it was known through MRD codes; the paper proves it for every . Its consequences in the paper are Corollaries 3.4 and 3.5 and Theorem 3.6: when is even and is odd, maximum -scattered subspaces of exist which the direct sum construction of Theorem 2.6 cannot produce, because does not divide . Theorem 3.3 is also the geometric counterpart of Delsarte duality of MRD codes (Theorem 4.12 of the paper).
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formalization would provide a reusable treatment of sesquilinear forms whose restriction to an -form is controlled, of orthogonal complements across the field extension , and of the passage between , and . Theorems 2.3 and 2.7 are also the goals of companion missions in this series; here they enter as milestones.
The definition of is easy; the content is in two dimension statements. First, must not collapse: is not automatic and depends on the hyperplane condition on , which in turn needs the upper bound of Theorem 2.7, whose proof in the paper is a long counting argument with Gaussian binomials (Section 5). Second, the scattered property must be transported through the duality: a large intersection of with an -dimensional subspace of must be converted into a large intersection of with a hyperplane of . This conversion runs through three different spaces and two different orthogonalities, over and over , and the identification between them requires that have an -basis which is an -basis of . Maximality is a further step that uses the bound of Theorem 2.3 in .
and are finite fields F, K with Algebra F K; is a finite-dimensional K-module with a compatible F-structure (IsScalarTower F K 𝕍). The setting of §3 is a structure DelsarteSetting F K 𝕍 holding (complementary), (with , spanning, ), and with non-degeneracy, reflexivity and . The embedding of into is data, not a theorem; its existence is cited by the paper and is not an item. The paper's is the restriction of to .
Conventions pinned:
F-subspace of the type ↥Λ, and "h-scattered in " is Definition 1.1 with ambient space , including and . The dual is (n − h − 2)-scattered in the quotient 𝕍 ⧸ Γ^⊥, whose dimension is .The form must be non-degenerate and -valued on : with one would get and a zero quotient, and without the subspace is not the paper's Delsarte dual; both conditions are fields of the setting and may not be dropped.
Cited inputs: none of the milestones is proved elsewhere; Theorems 2.3 and 2.7 duplicate the goals of companion missions 1 and 3 and may be closed by importing their proofs once published. Contributions welcome: the sesquilinear-form infrastructure (dimension of orthogonal complements, the extension of from to ), Proposition 3.1, and the transport argument of Theorem 3.3.
A scattered subspace is an -subspace of an -vector space that meets every one-dimensional -subspace of in an -subspace of dimension at most one. Scattered subspaces produce scattered linear sets in projective spaces over finite fields, and through them two-intersection sets, two-weight codes, translation caps and maximum rank distance (MRD) codes. Blokhuis and Lavrauw (Geom. Dedicata 2000) proved that a scattered subspace of has dimension at most , and constructions of that dimension are known whenever is even (see Bartoli, Giulietti, Marino, Polverino 2018 and the references there).
Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2, Combinatorica 41, 2021) replace "one-dimensional" by "-dimensional". The resulting -scattered subspaces interpolate between scattered subspaces () and subspaces meeting every hyperplane in small dimension (), which Sheekey and Van de Voorde (Des. Codes Cryptogr. 2020) showed to be equivalent to MRD codes with an idealiser isomorphic to . For the new notion the paper proves an upper bound on the dimension (Theorem 2.3) and shows that the bound is attained when divides (Theorem 2.6). This mission is the attainment half.
Let be finite fields, so , and let be an -dimensional -vector space with . Every -space is also an -space of dimension . For an integer with , an -subspace is -scattered (Definition 1.1) if
An -scattered subspace of largest possible -dimension is maximum -scattered. Theorem 2.3 of the paper says that an -scattered either has dimension and defines a subgeometry (an -basis of is an -basis of ), or satisfies
Two building blocks appear in the statements. If with and are -subspaces, then is the direct sum of the . For the Gabidulin-type subspace of is
the image of an -linear map, since fixes .
If , divides and , then contains an -subspace that is maximum -scattered and satisfies
Together with Theorem 2.3, the goal settles the largest dimension of an -scattered subspace of whenever and : it is exactly . The subspaces it produces are the input of the paper's Delsarte duality (Theorem 3.3), which turns maximum -scattered subspaces of reaching bound (1) into maximum -scattered subspaces of and so gives constructions also when . The direct-sum theorem is also of independent use: it extends the direct-sum construction for scattered linear sets of Bartoli, Giulietti, Marino and Polverino to every , and Example 2.5 gives the subspace counterpart of Gabidulin codes.
All results in this mission are proved in the paper. To our knowledge none of them has a machine-checked proof; no formal library contains scattered subspaces, linear sets or Gabidulin-type subspaces. The remaining work is formalizing the paper's arguments: the counting of roots of linearized polynomials behind Example 2.5, the Grassmann-formula and quotient-space argument of Theorem 2.4, and the bound (1) of Theorem 2.3, which the companion mission on the dimension bound states as its goal.
The construction itself is short; the work lies in the three ingredients. The obvious approach to Theorem 2.4 fails: an -dimensional -subspace of need not be the sum of its intersections with and , so the intersection cannot be bounded summand by summand. Example 2.5 needs that a nonzero -polynomial has at most roots in , and the root set is an -subspace. Maximality is not a property of a single subspace: it quantifies over every -scattered subspace of and so needs the full upper bound of Theorem 2.3, including the case handled there by Proposition 2.1.
is a finite field F, a finite field K with Algebra F K, so Fintype.card F and Module.finrank F K. is a finite-dimensional K-module with a compatible F-module structure (IsScalarTower F K V), and Module.finrank K V. An -subspace is a Submodule F V; its intersection with an -subspace S is S.restrictScalars F ⊓ U.
Conventions the statements commit to:
IsHScattered; without the range every spanning subspace would be -scattered for .(i : Fin t) → V i) and Submodule.pi Set.univ U. The minimum is given by for all and for some . The second part of Theorem 2.4 assumes .Fin r → K, with the range of the F-linear map , and assumes so that -scattered is within Definition 1.1's range.The goal is not satisfied by a small subspace: both the dimension equality and maximality among all -scattered subspaces of are part of its conclusion.
Results the paper cites without a number (the Blokhuis–Lavrauw bound for , the direct-sum theorem for scattered linear sets) are not items. Theorem 2.3 is restated here because the maximality in Theorem 2.6 rests on it; it duplicates the goal of the companion mission. Useful infrastructure beyond this mission: roots of linearized polynomials over finite fields, dimension formulas for subspaces under restriction of scalars, and direct sums of -scattered subspaces. Contributions on any milestone are welcome, and the goal can be closed from the milestones alone.
A promise constraint satisfaction problem is given by two finite relational structures with a homomorphism . An instance is a finite structure over the same signature, promised to map to ; the task is to find a homomorphism to the weaker structure (or, in the decision version, to tell apart from ). Approximate graph colouring (, ) is the standard example.
The most direct polynomial-time algorithm one can try is linear programming. The basic LP relaxation (BLP) of an instance replaces the 0–1 program "assign one value to each variable, one allowed tuple to each constraint" by probability distributions on values and on tuples, with consistent marginals. Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970v3, Theorem 7.9) characterise exactly when this relaxation decides , in terms of the polymorphisms of the template. The result extends the CSP case of Kun, O'Donnell, Tamaki, Yoshida and Zhou (KOT+12, Theorem 2(5)&(6)) to promise problems.
A relational structure on a set assigns to each symbol of a finite signature a relation , with . A polymorphism from to is a function , , that maps every tuples of , applied coordinatewise, to a tuple of ; these form . A function is symmetric if for every permutation .
A minion on is a nonempty family of functions , , closed under minors for maps ; a minion homomorphism preserves arities and minors. The minion on consists of the convex linear functions with and . The structure has domain and one relation for every rational linear inequality; a finite reduct keeps finitely many of them.
For an instance , the basic LP has variables for elements and for constraints , constrained by and the marginal equations . means that a solution exists in which every is supported on . BLP solves if every with maps to .
pp-constructions combine two operations on templates: an -th pp-power (domains , , relations defined by one primitive positive formula in both structures) and a homomorphic relaxation of (homomorphisms and ).
For a PCSP template , the following are equivalent:
The structure has as elements the rational probability distributions on ; a tuple lies in when some rational distribution on has marginals . The milestones are:
The result. Theorem 7.9 gives a complete, checkable description of the templates on which the basic LP relaxation is a correct algorithm: one needs only to look for symmetric polymorphisms. Through item (3) it places BLP inside the paper's general theory, in which the complexity of depends only on the minion ; BLP corresponds to the single minion . The same pattern later gives the analogous characterisations for the affine relaxation (Theorem 7.19, minion ) and the combined BLP+AIP algorithm of Brakensiek, Guruswami, Wrochna and Živný.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formalization adds minions and pp-constructions over infinite domains, the structure , and a compactness argument for countable structures, all reusable for other relaxation-based algorithms. On the platform, PCSPBLPAff.Symmetric.theorem_2 (symmetric polymorphisms of arbitrarily large arity make BLP+AIP correct) and PCSPBLPAff.Characterization.theorem_4 concern the different BLP+AIP algorithm.
Two steps resist the finite theory. First, Theorem 4.12 (minion homomorphisms correspond to pp-constructions) is proved only for finite templates and fails for infinite ones in general, while and live on ; the link between (3) and (4) must be made by hand through . Second, (2) supplies one symmetric polymorphism per arity, with no compatibility required between different arities, while (1) is a statement about all instances at once. The natural intermediate object, , is infinite, and no single polymorphism of acts on all of it; mapping it to is where finiteness of and countability of enter.
The development builds on the published definitions PCSPBLPAff.Symmetric (relational structures, homomorphisms, polymorphisms, symmetric functions, instances and the BLP polytope IsLPSol). Conventions: signatures are finite with arities ; and are finite and is nonempty, which excludes only the degenerate template , where items (1)–(3) hold and (4) fails. is encoded as the feasibility over of the LP with the vanishing constraints, following the paper's remark after Definition 7.7; dropping those constraints would make item (1) a different, false statement, since the unrestricted LP is always feasible. Item (2) asks for every arity , not only arbitrarily large ones. is defined directly as the convex linear functions (coefficients in summing to ; affine coefficients would give a different theorem). uses non-strict inequalities. The free structure, and are stated with rational values, so is countable.
Left out: the complexity consequences (polynomial-time solvability) and the identification of with the polymorphisms of , which the proof does not need. The cited input [KOT+12, Proposition 12] is replaced by its use in the proof, the milestone on . The proof of Lemma 7.12 on p. 47 omits from the pp-definition; nonnegativity is itself pp-definable in , so the lemma's statement is unaffected.
Contributions welcome: proofs of any milestone, in particular the compactness remark (or a derivation from PCSPBLPAff.Characterization.lemma_16) and Lemma 4.8 for infinite templates.
A multi-armed bandit learner repeatedly chooses one of several actions, observes only the loss of the chosen action, and tries to perform nearly as well as a single fixed action selected in hindsight. Two common loss models make different demands on the learner. In a stochastic model, each arm has a stable mean loss and the learner can gradually distinguish the best arm. In an adversarial model, losses may change with time and even respond to previous choices. A useful bandit algorithm should handle both without first being told which model generated the losses.
Zimmert and Seldin's Tsallis-INF paper analyzes one algorithm in both regimes. Its Theorem 1 gives a square-root guarantee against arbitrary adversarial losses and a logarithmic guarantee when the regret satisfies a self-bounding constraint. The latter condition includes the usual stochastic case with a unique best arm and also permits some adversarial deviations. This mission formalizes the reduced-variance (RV) estimator part of that theorem and six supporting statements from its analysis.
There are arms and rounds . At round , the environment supplies a loss for each arm . The learner draws an arm from a probability vector and observes only . The environment can base its current losses on the actions from earlier rounds. It may also randomize: a seed records its internal random choices, while its response to a history remains adaptive. The learner's random actions are then drawn successively from its history-dependent weight vectors. Expectations below average over both sources of randomness.
The pseudo-regret at horizon compares the learner's expected total loss with the lowest expected total loss of a fixed arm:
For the algorithm studied here, is the vector of estimated losses accumulated before round . The symmetric half-Tsallis regularizer is
The vector maximizes over the probability simplex. With the RV loss estimator, arm has baseline and estimate . This is an estimator based on the one observed loss, even though its update is a vector.
The self-bounding condition chooses gaps with exactly one zero, at , and a constant , as defined in Section 2. It requires
The gaps measure how costly it is to place weight on each non-best arm. In a stochastic bandit with a unique best arm, the usual expected-loss gaps give this relation with Zimmert and Seldin, §2 and §4.1.
The first target is an upper bound for every bounded, randomized adaptive adversary and every :
The paper prints in Theorem 1's display. Its proof yields , the coefficient formalized here; the difference is recorded in the moderation notes. The theorem's other displayed bounds retain their printed constants.
For , set and
Under the self-bounding condition, the same algorithm must satisfy
When , it must also satisfy . The goal states both clauses together with the adversarial guarantee. Its six milestones give a pathwise stability bound from Lemma 19, two per-round stability bounds from Lemma 11, two accumulated penalty bounds from Lemma 12, and a finite tail-sum estimate from Lemma 15.
The adversarial clause limits the cost of learning even when no arm has a persistent advantage. The self-bounding clause gives gap-sensitive logarithmic growth when the learner receives enough information to identify a unique best arm, while allowing the additive deviation . The two guarantees apply to the same weight rule and the same RV estimator Zimmert and Seldin, Theorem 1.
The paper proves its RV claims in prose and equations. A complete Lean proof would make the algorithm's randomized adaptive loss model, its path law, the estimator and the exact constants explicit in machine-checked form. The local theorem statements and definitions in this proposal compile with placeholder theorem proofs; the mission's mathematical results are therefore targets for formalization, not results already machine checked here. The setting definitions may also support formal analyses of other bandit algorithms with adaptive randomized losses.
The learner sees only one loss at each round, so the weight vector depends on estimates whose individual coordinates can be much larger than the observed losses. Bounding the change in the regularized potential by a simple worst-case estimate loses the dependence on the arm weights that the gap-sensitive result needs. The RV estimator reduces this difficulty but can take negative values, which changes the stability calculation. The self-bounding guarantee also compares the theorem's zero-gap arm with a best arm chosen in expectation at horizon ; for these need not coincide. That comparator issue is documented for audit.
The arms are Fin K, with the paper's first arm represented by Lean index zero. Histories are functions on natural-number rounds; entry zero is unused. A referenced published adversarial protocol supplies bounded losses and dependence on past actions. A probability measure on adversary seeds and a finite sum over action paths define the run law. The algorithm is an argmax predicate whose estimates are computed from its own weights and the observed loss. The real-valued simplex supremum defines ; makes that simplex nonempty, and its compactness bounds the objective. The goal requires measurable seeded losses, a probability measure, , in the self-bounding regime, and where is used. The penalty milestones take conditionally unbiased estimators that depend only on actions through their own round, are measurable, and have finite expected absolute size, as required for a sequential run and genuine expectations. Positive, non-increasing learning rates are explicit.
The argmax is taken over every simplex weight vector, and the run law includes every action path with its product probability. These choices rule out an arbitrary weight rule or a zero-valued integral masquerading as the algorithm. The development needs reusable facts about the simplex, measurability and integrability of the finite-path law, positivity of Tsallis-INF weights, and bounds on the real potential. Contributions that establish those facts or close the six milestone theorems fit this mission.
Adam (Kingma and Ba, arXiv:1412.6980) is the default optimizer for training neural networks. It combines a stochastic gradient step with two exponential moving averages: a momentum term and a coordinatewise second-moment estimate that rescales each coordinate of the step. Its convergence theory is delicate: Reddi, Kale and Kumar (arXiv:1904.09237) exhibited convex problems on which Adam with constant hyperparameters fails to converge.
Barakat and Bianchi (arXiv:1810.02263, SIAM J. Math. Data Sci. 3(1), 2021) study Adam on nonconvex objectives through the ODE method of stochastic approximation. In the decreasing-stepsize regime, their Theorem 5.2 proves that the iterates converge almost surely to the critical points of the objective — provided the iterates are almost surely bounded. A stability hypothesis of this kind is standard in stochastic approximation (Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, 1999, doi:10.1007/BFb0096509), and it is often the hardest part to verify. Theorem 5.4 of the paper gives sufficient conditions, on the objective and the stepsizes only, under which almost sure boundedness holds. This mission formalizes that theorem.
Let be a probability space and a measurable space carrying a probability measure . A loss is given, with gradient in , and the objective is
The samples are iid with law (Assumption 4.1). Vector operations below are coordinatewise.
Fix and real sequences (stepsizes), , (moment parameters). Algorithm 5.1 (Adam with decreasing stepsize) starts from , , , and for sets
The weights implement the bias correction of Adam.
The hypotheses are: Assumption 2.2 ( measurable, continuously differentiable for a.e. , integrability at one point, and on each compact ); Assumption 2.3 ( coercive); Assumption 4.2 i) with ( on compacts); Assumption 5.1 (, , , , , , with ); and Assumption 5.3 ( Lipschitz, , and ).
Under Assumptions 2.2, 2.3, 4.1, 5.1, 5.3 and 4.2 i) with ,
Theorem 5.2 of the paper, the almost sure convergence of decreasing-step Adam to the critical set, is conditional on almost sure boundedness. Theorem 5.4 removes that condition for objectives with Lipschitz gradient and quadratic gradient-noise growth, and so turns Theorem 5.2 into an unconditional convergence result in that class. The Lyapunov function — the objective plus a weighted kinetic energy of the momentum — is the discrete counterpart of the energy used for the continuous-time Adam ODE in the same paper; the condition that keeps it decreasing is the discrete trace of the condition of the ODE analysis.
The result is proved in the paper; nothing about Adam is formalized on the platform. A formal proof produces a machine-checked stability theorem for an adaptive, momentum-based stochastic algorithm, together with reusable pieces: the Robbins–Siegmund almost-supermartingale theorem in the conditional-expectation form used here, and the bias-correction lemma, which applies to every exponential moving average with vanishing forgetting rate.
For plain stochastic gradient descent, boundedness follows from the descent lemma applied to alone: is an almost supermartingale. For Adam this fails. The step is not a descent direction for : averages past gradients, so has no sign. The momentum must therefore enter the Lyapunov function, through , and the coordinatewise preconditioner changes from step to step, so and are measured in different weighted norms. Controlling that change is what (9.3) does, and it costs a term of size that must be absorbed by the friction of the momentum update; the margin is exactly . The time-varying weights and produce the further term , which is why Assumption 5.3 iii) is needed. Finally, the conditional expectations involve the next sample through both and , so the second-moment growth condition of Assumption 5.3 ii) has to be used with the right weights.
Points of are EuclideanSpace ℝ (Fin d); the state lives in the product , whose Mathlib norm is the maximum of the three Euclidean norms (the same bounded sets). The gradient of is a function gf : E → Ξ → E that equals the true gradient for -almost every . The run of Algorithm 5.1 is defined along a sample path and then pathwise in . Moments are lower Lebesgue integrals, so no hypothesis is vacuous through the convention that a non-integrable Bochner integral is . Assumption 5.3 iii) is stated as "there is bounding the bracket for all large ", which avoids a real limsup. The algorithm divides by and ; the theorem therefore assumes and , which Algorithm 5.1 needs for to be defined. In the milestones, applied to a function of the next state is the integral of that function over the next sample, , a version of the conditional expectation under Assumption 4.1. In (9.4) the term printed as is , the reading the derivation produces.
The goal asserts a single bound for the whole trajectory almost surely; finiteness of each iterate, boundedness of a projected variant of Adam, and boundedness under an almost-sure bound on are all weaker statements and are not this theorem. The "without loss of generality " of the proof appears only as a hypothesis of the last milestone.
A complete development needs the Robbins–Siegmund theorem (open on the platform as AdaptiveProtection.Convergence.lemma2_robbins_siegmund), differentiation under the integral sign for , the descent lemma for Lipschitz gradients, and conditional expectations given for functions of an independent sample. Proofs of any milestone, and a proof of Robbins–Siegmund in the form used here, are welcome.
A constraint satisfaction problem (CSP) asks for an assignment of values from a finite domain to variables so that every constraint, a tuple of variables required to lie in a fixed relation, is satisfied. The algebraic theory of CSPs rests on a Galois correspondence: the complexity of is determined by the set of its polymorphisms, because holds exactly when every relation of is definable from by a primitive positive formula (Geiger 1968; Bodnarčuk, Kalužnin, Kotov and Romov 1969), and such definitions translate into reductions (Jeavons 1998). This correspondence underlies the CSP dichotomy theorem.
Promise CSPs (PCSPs) relax a CSP by a promise: every constraint comes as a pair with , and the task is to tell instances satisfiable with the -relations from instances not even satisfiable with the -relations. Approximate graph colouring and -SAT are examples. Brakensiek and Guruswami (arXiv:1704.01937v2, §6.1) showed that the Galois correspondence survives this generalisation, with pp-definitions replaced by positive primitive promise definitions (ppp-definitions). This is the starting point of the algebraic approach to PCSPs later systematised by Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970). Pippenger (2002) had earlier proved a variant of the correspondence for pairs of relations, not in this complexity-theoretic form.
Fix a finite domain . A relation of arity is a set , and a promise relation is a pair of relations of arity with . A family is indexed by a set of symbols with arities . In Lean it is a pair of relational structures 𝔸 𝔹 : RelStruct τ ar D, with = 𝔸.rel R, = 𝔹.rel R and (IsPromiseFamily).
A function is a polymorphism of if for every and all the tuple obtained by applying coordinate-wise, , lies in . is the set of polymorphisms of all arities .
A -PCSP is a finite list of clauses, each a symbol applied to a tuple of variables, with repetition allowed. It is read twice: as , with each clause asking its tuple to lie in , and as , with in place of . Let .
Definition (ppp-definability). A promise relation is ppp-definable from a finite family if there are and a -PCSP on variables such that
A family is ppp-definable from if each of its promise relations is.
For a finite family and a family over the same finite domain,
The printed Theorem 6.1 concludes a polynomial-time reduction from to . Its proof opens by reducing to the displayed statement, and the reduction follows from it by substituting gadgets.
The result. Theorem 6.1 shows that the complexity of depends only on : two finite families with the same polymorphisms have polynomial-time equivalent PCSPs. Hardness can then be read off from the absence of structured polymorphisms, and tractability from their presence. The paper's Boolean symmetric dichotomy (its Theorem 2.16) is organised in exactly this way, and the theorem justifies studying families of polymorphisms instead of families of relations. Section 6.2 of the paper, which characterises the sets of functions of the form , is its companion.
Formalizing it. The result and its proof are published, and no machine-checked version is known to exist. This mission produces a reusable definition of ppp-definability for promise families over arbitrary finite domains, built on the published relational-structure vocabulary PCSPBLPAff_Symmetric_Setting. It also produces the closure properties (weakening, transitivity) any later work on gadget reductions between PCSPs will need, and the encoding of the polymorphism relation as a gadget. The complexity-theoretic conclusion, a polynomial-time reduction, is not part of the mission.
The printed proofs are short, but each hides a construction. Transitivity requires substituting a gadget for every clause of an intermediate PCSP: the auxiliary variables of all gadgets are renamed apart, and EQUAL clauses are carried through unchanged. Proposition 6.3 requires one clause for every symbol and every -tuple of elements of , indexed by the finite set of such tuples and laid out on the coordinates of . The goal must handle (so , nullary functions, and with one point), where Proposition 6.3 as printed () does not apply. A tempting shortcut is to read the hypothesis only for arities . With that reading the theorem is false: for and , both unary, every function of positive arity is a polymorphism of both families, yet constant assignments satisfy every , so is not ppp-definable.
𝔸 𝔹 : RelStruct τ ar D with [Fintype τ] and IsPromiseFamily 𝔸 𝔹. is a promise family over any signature τ', possibly infinite; the conclusion is stated relation by relation.IsPolymorphism from the published setting file. PolSubset quantifies over every arity L : ℕ, including . This convention makes the goal true, and no hypothesis is added.Instance over the signature τ ⊕ Unit, whose new symbol has arity 2 and is EQUAL in both readings. The same clause list is read in withEqual 𝔸 (as ) and in withEqual 𝔹 (as ). PPPDefinable requires Ψ.n = k + ℓ. The first variables are Fin.castAdd ℓ, and is Fin.append x y. The two clauses of the definition keep the paper's quantifiers: existence of an extension on the side, and every satisfying assignment on the side. A formalization with two independent instances, or with both readings in , would trivialise the notion and is excluded.Fintype.card (Fin L → D) through any bijection e. The statements hold for every such ordering.PolyTime predicate or placeholder is introduced.Many optimization models minimize a smooth transformation followed by a nonsmooth penalty. A penalty may encourage sparse coefficients, restrict a feasible region, or measure deviation from observed data. Even when the penalty is convex, its composition with a nonlinear map need not be convex. This makes a standard convex optimality certificate unavailable, while numerical methods still need a way to judge whether a small step means that an iterate is close to a stationary solution. Drusvyatskiy and Lewis study this question for the prox-linear method, which repeatedly solves a convex approximation of the composite objective (Drusvyatskiy and Lewis, 2016, §5).
The paper establishes several links among step lengths, near-stationarity, local error bounds, and rates of convergence. The result selected here is Theorem 5.10: a local error bound expressed through the prox-linear step is equivalent, with stated constants, to subregularity of the composite subdifferential. This comparison lets analysts use whichever of the two properties is easier to verify for a given model (Theorem 5.10, p. 20).
Work in Euclidean spaces and . A convex-composite objective has the form . Here is proper, closed, and convex; is finite-valued and convex; and is continuously differentiable. The value of can exclude points from its domain. The paper defines the relevant composite subdifferential by
and calls stationary when . These are the paper's definitions on p. 13; the subdifferential is not replaced by a different generalized derivative (§5, p. 13).
At a current point , the method substitutes the affine approximation for . It then minimizes the prox-linear subproblem
Write its unique minimizer as and the prox-gradient as . Under the stated assumptions, a zero prox-gradient is equivalent to stationarity. The quantitative estimates additionally assume that is -Lipschitz and that the Jacobian is -Lipschitz, with (§5, p. 14).
For a set-valued mapping , subregularity at a graph point with constant means that some neighborhood of satisfies
The error bound in this mission applies this definition to and . The other instance is (Definition 5.7, p. 19).
The goal is the two-way quantitative statement of Theorem 5.10. If is stationary and , then
and
The milestone list follows the paper's quantitative statements: the quadratic comparison (5.2), the gradient inequalities (5.3)–(5.5) of Lemma 5.1, Ekeland's variational principle as Theorem 5.2, the zero-step stationarity claim, the nearby near-stationary point of Theorem 5.3, and the step-length comparison (5.7) from Theorem 5.6. A final companion milestone is the per-step decrease (5.6), , stated at . The Ekeland result is an existing proved platform theorem, included by reference. The other targets are the paper's claims in their original order of dependence (§5, pp. 14–20).
The theorem turns an algorithmic condition, measured by a computed step, into a local property of the objective's first-order geometry. The constants specify how an error bound changes when moved between the two descriptions. In a convergence analysis, either condition can be established and then used through the other formulation without losing track of its quantitative dependence on , , and . The result does not require a convex composite objective, only the convexity of and and the stated smoothness of (Theorem 5.10, p. 20).
The mathematical theorem was proved in the cited paper. The remaining work here is a machine-checked development of its composite subdifferential, the prox-linear argmin, the local subregularity estimates, and the comparison theorem. A general version of Ekeland's variational principle already has a machine-checked proof on Prove2Me; the prox-linear claims in this proposal are open proof targets. The definitions and estimates can also support later formalizations of prox-linear convergence, including the rate results in §§5–6, without building the algorithm into the statement of Theorem 5.10.
The prox-linear step is computed from a convex local model, while the quantity whose stationarity is sought belongs to the original nonlinear composite objective. A small displacement from to alone does not directly give a small subgradient at : the model and the original objective have different first-order behavior away from their common base point. Theorem 5.3 addresses a nearby point and supplies both a distance estimate and a subgradient estimate. Passing from those estimates to a neighborhood-wide error bound is the central issue, especially because the neighborhoods in the definition of subregularity are local to (Theorem 5.3, p. 16; Theorem 5.10, p. 20).
The Lean carrier is EuclideanSpace ℝ (Fin n); dimensions zero are allowed. Objective values use EReal, and properness explicitly excludes and requires at least one finite point. Closedness is lower semicontinuity. The real-valued is embedded into EReal only when forming objective values. The Jacobian is fderiv, and its adjoint represents . The prox-linear point is an argmin predicate, so its definition does not depend on an arbitrary choice of minimizer.
The prox-gradient is represented as a set-valued map through those argmin points. Subregularity uses a neighborhood filter and requires the base graph point and a positive constant. Distance to an empty image on the right side is treated as through a universal bound over its members. The inverse image on the left is nonempty because it contains the base point. In Theorem 5.3, the upper bound on distance to the subdifferential is represented by an attained subgradient; the subdifferential in this convex-composite setting is closed. These choices preserve the paper's claims at empty sets and extended-real values.
The goal retains every positive step size . The companion (5.6) is stated at with : the page announces it for , but for , , the decrease is only when . The linear-rate Theorem 5.5 and the results of §6 are not part of this mission. The first-order and step-length milestones do not require the and assumptions, matching the paper's first sentences. Contributions that establish the argmin properties, the distance conventions, the quantitative milestones, or the final two implications are within scope. A vacuous restriction to points already stationary would miss the neighborhood-wide error bound and is excluded.
Many problems in signal processing, statistics and machine learning ask to minimise a sum of two convex functions, each of which is easy to handle on its own through its proximal operator but not jointly. Operator-splitting methods exploit exactly that structure. The Douglas–Rachford (DRS) and Peaceman–Rachford (PRS) splitting schemes, introduced for linear equations in the 1950s and extended to maximal monotone operators by Lions and Mercier (1979), are the classical examples; applied to the dual of a linearly constrained problem, DRS is the alternating direction method of multipliers (ADMM) of Gabay and Mercier (1976).
Convergence of these methods has been known for decades, but convergence rates in terms of the objective value were established only recently. Davis and Yin (arXiv:1406.4834) showed that for general convex the objective error of relaxed PRS converges at the nonergodic rate , and that this is sharp. The paper behind this mission (arXiv:1407.5210v3) asks how much faster the method becomes when or is more regular. Its Theorem 3.1 answers the question for the case of one smooth function: the best objective error found in the first iterations is , for any stepsize. This matches the rate of forward–backward splitting (FBS), the method one would otherwise use when one of the two functions is smooth, without FBS's stepsize restriction.
Let be a real Hilbert space and let be closed, proper and convex. For the proximal operator is
the reflection is , and the PRS operator is . For write .
Relaxed PRS (Algorithm 1) starts from any and iterates
The choice is DRS and is PRS. Each step computes two auxiliary points,
which are the method's candidate solutions. If is a fixed point of , then minimises . The objective error at a point is .
A function has a -Lipschitz gradient () if it is real-valued and differentiable and for all .
Suppose . If is -Lipschitz and , or if is -Lipschitz and , then
Both cases are part of the goal. The statement fixes no constants: it asserts only the order of the best-iterate error, so it holds for every stepsize .
A companion item states the explicit bounds of the proof of Theorem 3.1 (p. 11), of the form times a case-dependent factor.
The result separates relaxed PRS from FBS. FBS needs to converge, so it needs the Lipschitz constant of the gradient, or a line search to estimate it. Theorem 3.1 says relaxed PRS reaches the same best-iterate order for every , and the companion bounds show how the constant depends on . The theorem and its explicit bounds are part of the paper's catalogue of rates (its Tables 1.1–1.2), which records how the rates of relaxed PRS and ADMM improve under regularity.
The result is proved in the paper. As far as is known, none of these statements is machine-checked. Formalizing it means building the prox calculus for extended-valued convex functions on a Hilbert space (Lemma 1.1, Lemma C.1), the descent and cocoercivity inequalities for smooth convex functions (Theorem A.1), the Fejér-type summability of the fixed-point residual of averaged nonexpansive maps (Fact 1.2), and the summable-sequence rate lemma (Fact 1.1). Each of these is reused across operator-splitting analyses.
The objective errors are nonnegative and, by Proposition 3.1 and Fact 1.2, weighted-summable. They are not monotone, however. A summable nonnegative sequence need not be term by term, which is why only the best iterate gets the little-o rate. A summability argument that ignores this, or that claims the rate for the last iterate, proves something false.
Proposition 3.1 is the substantive step. The upper fundamental inequality contains an inner-product term that does not telescope, and it must be absorbed through the optimality condition (C.2) and the smoothness inequalities (A.1)–(A.2). When the residual term that remains has the wrong sign. It is controlled only by a second use of the Lipschitz gradient, through the regularity term , which costs the factor .
InnerProductSpace with CompleteSpace. are H → EReal, closed, proper and convex in the sense of the published IsProperClosedConvex. A prox map is a map with the published IsProx γ f P, which for determines it uniquely. The subdifferential is the published subgrad.IsSmoothConvex β h (convex, Fréchet differentiable, -Lipschitz gradient), .Asymptotics.IsLittleO along atTop. The best iterate is Finset.inf' over .EReal.toReal, evaluated only where all four values are finite. These points are prox outputs of a proper function, and values of the real-valued smooth function.Contributions are welcome at every level: the prox calculus of Lemma 1.1 and Lemma C.1, Theorem A.1, the summability results, and the final assembly.
Online retailers show their catalogue on a sequence of pages, and most visitors never reach the last one. Which products appear on the first page, and at what prices, therefore decides what a typical consumer can buy at all. Gallego, Li, Truong and Wang (Operations Research, 2020) model this as the product framing problem: the consideration set of a consumer is the set of products on the pages that consumer is willing to view, and the number of pages viewed is random. Their Section 7 adds prices to the problem and asks how a retailer should frame and price jointly when consumers choose by the multinomial logit (MNL) model.
The question connects two literatures. In assortment pricing under MNL with a common price sensitivity, the optimal prices of all offered products are known to be equal (Anderson, de Palma and Thisse 1992; Gallego and Stefanescu, as cited on p. 16 of the paper), and the nested-logit extension of Gallego and Wang (Operations Research, 2014) keeps an adjusted markup constant across nests. In search and ranking models, the order in which products are shown changes which ones are bought. The paper's structural results say what survives of the equal-price rule once consideration sets are nested by page, and which products belong on the early pages.
There are products, , and pages, each holding at most products. A framing places each product on one page or leaves it undisplayed. A consumer views the first pages, where is random with law , independent of the framing. A consumer who views pages considers , the products on pages , so .
Product has a quality and a price , and the price sensitivity is . The mean utility of product is , and the outside option has utility . Under the MNL model a consumer with consideration set buys with probability
and for . The expected revenue from that consumer is , and the total expected revenue of a framing and a price vector is
For a fixed framing, denotes the optimal value of this quantity over all price vectors, as a function of the quality vector .
The goal is the existence of an optimal joint solution with the paper's structure: there are a feasible framing and prices such that no feasible framing with any prices earns more, and
Pages are filled in order until all products are displayed, and the products appear in descending order of quality.
Theorem 5 reduces the pricing problem of a fixed framing from prices to page prices and says that later pages carry higher prices; this is the page-level analogue of the constant-markup property of MNL pricing, and it runs opposite to the ordering found in oligopoly search models (Arbatskaya 2007). Theorem 6 removes the framing decision almost entirely: a joint optimum is obtained by sorting the products by quality and filling pages in that order, leaving only page prices to choose. The paper's approximation algorithm for joint pricing and framing (Theorem 7, NEST-P, with guarantee ) starts from this structure.
None of these statements has a machine-checked proof. A complete development would give the first formal treatment of MNL price optimization with nested consideration sets, including the existence of optimal prices, which the paper takes for granted. The paper's argument for the monotonicity and its envelope-theorem step (19) are informal; a formal proof has to supply both.
The expected revenue is not concave in the prices, even with two products on two pages (Example 1, p. 17), so the first-order condition alone does not identify the optimum, and existence of an optimal price vector has to be argued from the behaviour of the revenue as prices tend to . The within-page equality of prices follows from the first-order condition, but the ordering of page prices needs a global comparison of revenues across consideration sets. In Theorem 6, the obvious exchange argument (swap a higher-quality product forward) does not obviously keep revenue from decreasing when the swapped products have different prices; the paper splits into two cases, and in one of them the improvement comes from continuously moving qualities, which requires control of the optimal value as a function of rather than of a fixed price vector.
Products are Fin n, pages are the natural numbers with , and capacities satisfy . A framing is f : Fin n → ℕ with page f i ∈ [m] for displayed products and f i = 0 for undisplayed ones (the paper's ); feasibility means at most products per page. The law of is a nonnegative function on summing to one. Prices are finite reals: the paper's priced-out products () coincide with undisplayed ones, which the framing already allows. "Descending order" and "increases" are read weakly.
Theorem 5 and (17) are stated for every maximizing price vector and only for products on pages that some consumer reaches (), a restriction the paper never discusses: a product on a page no consumer reaches can carry any price at an optimum. They do not assert that a maximizer exists. Theorem 6 is read existentially ("some optimal solution has this structure"); the universal reading is false when some , because exchanging products between pages and then changes no revenue. (19) is formalized as its stated consequence, the monotonicity of the optimal value , together with the boundedness of the revenues; the envelope identity itself would need a differentiable selection of optimal prices that the paper does not establish.
A trivializing formalization of the goal would take the optimum over framings that are already sorted, over a single fixed framing, or over prices fixed in advance; the goal's optimality clause ranges over all feasible framings and all real price vectors. The development needs elementary calculus of the MNL revenue (HasDerivAt, Real.exp), finite sums over pages, and a compactness or limiting argument for the existence of optimal prices. Pages are those of the authors' accepted manuscript, which differ from the journal typesetting. Proofs of any milestone, and lemmas on MNL pricing reusable beyond this paper (boundedness of , existence of optimal MNL prices, the constant-price property for a single assortment), are welcome.
In classical optimal transport on the real line, one coupling plays a distinguished role: the monotone (Hoeffding–Fréchet) coupling, which sends the -quantile of the first marginal to the -quantile of the second. It is canonical (every initial segment of the first marginal goes as far left as possible) and it is optimal for a whole family of costs at once.
Martingale optimal transport adds the constraint that the coupling be the law of a one-step martingale , . The problem arises in robust (model-independent) mathematical finance: prices of vanilla options fix the marginal laws of and of , and bounds on the price of an exotic option that hold under every arbitrage-free model are values of the martingale transport problem (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). Martingale couplings exist exactly when and are in convex order (Strassen 1965).
Beiglböck and Juillet (arXiv:1208.1509, Ann. Probab. 44(1), 2016) asked for the martingale counterpart of the monotone coupling, and found it: the left-curtain coupling . This mission formalizes its existence and uniqueness (Theorem 1.5), which is the foundation for the paper's later optimality results (Theorems 1.7, 6.1 and 6.3, other missions of this series).
All measures are Borel measures on or . is the set of finite measures with . For :
In Lean these are InM, ConvexLE, ExtConvexLE, IsMartingalePlan, IsLeftMonotone, IsShadow, IsLeftCurtain and targetUpTo in the shared namespace MartOT.Var. The mission's own theorems are in MartOT.Curtain.
For probability measures on with finite first moments,
Existence alone, or uniqueness only among left-curtain plans, is not the goal: the statement says that monotonicity alone singles out one martingale coupling.
Theorem 1.5 identifies a canonical martingale coupling defined by a geometric property of its support alone. The paper then shows that is the unique optimizer of the martingale transport problem for costs with strictly convex (Theorem 1.7) and that it is characterized by the convex-order minimality of Theorem 1.8. The left-curtain coupling has since been studied and generalized in a series of works (for instance Henry-Labordère and Touzi 2016).
The result is proved in the paper. It has, as far as the platform's catalogue shows, no machine-checked proof: no statement about martingale transport plans, shadows or the left-curtain coupling exists on Prove2Me. A formal development would produce reusable infrastructure: the convex order on finite measures of arbitrary mass, shadows, and the passage between the barycentre characterization (4) of martingale plans and their disintegrations.
Existence is not the hard part in the abstract: a left-monotone plan can be obtained as an optimizer for a suitable cost via the variational lemma. The construction through shadows is more delicate: one must show that the shadows of the initial segments increase with (this rests on Theorem 4.8, the shadow of a sum) and that the resulting plan satisfies the martingale property.
Uniqueness is the main obstacle. The classical argument for uniqueness of optimal plans (averaging two candidates and using strict convexity) requires a continuous first marginal and does not apply to arbitrary with atoms. The paper's argument is specific to the problem: it compares with the shadow through the test functions and a case analysis at the support end-points, which needs the measure-theoretic Lemmas 5.1 and 5.2.
MeasureTheory.Measure ℝ and Measure (ℝ × ℝ) with Borel σ-algebras. The goal and Theorems 1.8, 4.18, 4.21 take probability measures (IsProbabilityMeasure) in convex order; Lemma 4.6, the shadow monotonicity, Lemma 5.1 and Theorem 5.3 work in , as the paper's Sections 4–5 do.EReal, through the published ModelRiskOT.Duality.extIntegral), so no Bochner integral of a non-integrable function enters a statement. is encoded by characterization (4) of the paper, not by disintegrations.IsShadow, IsLeftCurtain), never chosen functions: their existence and uniqueness are milestones, not definitions. A formalization that defined by a choice and the left-monotone plan as "the left-curtain plan" would make the goal circular; the goal mentions only and left-monotonicity.Measure.support.BddAbove; at Lean's convention applies.PalmQueueing.Ordering.strassen_cx.Contributions are welcome at every level: proofs of the milestones, auxiliary lemmas on the convex order of finite measures (potential functions , equality of mass and mean), and the equivalence between (4) and the disintegration form of the martingale property.
Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks: a stochastic gradient method that keeps an exponential moving average of past gradients and an exponential moving average of their coordinatewise squares, and divides the first by the square root of the second. Its practical success came well before any convergence theory for nonconvex objectives. Reddi, Kale and Kumar (2018) showed that Adam with constant momentum parameters can fail to converge even on convex problems, which made the question of under which parameter schedules Adam provably converges a live one.
Barakat and Bianchi (arXiv:1810.02263, SIAM J. Math. Data Sci. 2021) answer it through the ODE method of stochastic approximation (Benaïm, 1999). This mission takes the paper's almost-sure convergence theorem for Adam with decreasing stepsizes, Theorem 5.2. Under a stepsize schedule in which and shrink in proportion to the stepsize , the iterates converge almost surely to the critical points of the objective, provided they stay bounded.
Let be a random variable on a measurable space with law , let be an integrand with gradient in , and set
where is the coordinatewise square and is the critical set. Let be iid copies of on a probability space .
Algorithm 5.1 takes stepsizes , weights and a constant . Starting from , and , it computes for , with all vector operations coordinatewise:
The divisions by , are the bias correction.
The stepsizes satisfy Assumption 5.1: , , , and there are with , and . The limiting dynamics is the autonomous ODE on , written , with
Assume Assumption 2.2 (regularity and moments of ), coercive (2.3), coordinatewise (2.4), iid samples (4.1), Assumption 5.1, on compacts (4.2 i) with ), that has empty interior, and that is bounded with probability one. Then, almost surely,
and if is countable, almost surely for some .
The theorem identifies a regime of Adam's hyperparameters, and with , in which the algorithm behaves like a gradient method with vanishing noise: the iterates approach critical points, the momentum dies out, and the second-moment estimate converges to . The condition ties the two averaging rates together. It is the condition under which the paper's Lyapunov function for the continuous dynamics decreases (Lemma 7.5). The argument structure is also a template for other adaptive methods: once the limiting ODE has a strict Lyapunov function, almost-sure convergence of the iterates follows from the same steps.
The paper proves the result on paper; none of it is machine-checked. A formal proof would also be the first formal instance on Prove2Me of the full ODE method for a concrete stochastic algorithm. That pipeline runs from the iterates to a perturbed Euler scheme, then to an asymptotic pseudotrajectory and a limit-set theorem, and finally to convergence. Benaïm's general results are being formalized separately on the platform (the asymptotic-pseudotrajectory definition this mission reuses comes from that effort), so the two developments meet in milestone 3.
The obvious approach is to treat Adam as stochastic gradient descent with a preconditioner and run a descent-lemma argument on . This fails because the update direction is not a descent direction for : lags behind . Any Lyapunov function has to involve the momentum, and alone does not decrease. The continuous-time energy decreases only weakly, and only its perturbation is strict, and only on compact sets. A second difficulty is that the stepsize-dependent coefficients and the bias corrections , make the recursion a non-autonomous perturbation of the Euler scheme of . The remainder must be shown to vanish along almost every path before the general theory applies. Finally, the abstract limit-set theorem needs the semiflow to be well defined on the closed set , where involves and is not Lipschitz at .
is EuclideanSpace ℝ (Fin d). The state space is the product of three copies with Mathlib's max-of-factors norm, which is equivalent to the Euclidean norm of and leaves boundedness and limits unchanged. and are Bochner integrals against the law . Assumption 2.2 makes the integrands integrable, so they are the true expectations. Moments are lower Lebesgue integrals. Algorithm 5.1 is a pathwise recursion adamIter, driven by a random sequence whose index is unused. The iid hypothesis is iIndepFun with every of law .
Two hypotheses are left implicit on the page and are added explicitly. The first is . The second is and : Assumption 5.1 iii) permits , which gives , and Lean's division by zero returns . Lemma 9.1 is stated with and , which its convergence claim needs. Semiflows are Flow ℝ≥0 on the subtype , and the asymptotic pseudotrajectory and limit set are the published StochApproxDyn.LimitSet definitions. The ODE milestones 4–6 hold for abstract , under Assumptions 7.1–7.2 with , as in the paper's §7.
The goal concerns the iterates of Algorithm 5.1 itself. A statement about trajectories of , or one that replaces almost-sure boundedness by a bound uniform in together with deterministic gradients, is a different and much weaker theorem and is ruled out. The interior condition on and the countability of enter exactly as on the page.
A complete development needs the following:
The last two are reusable for any stochastic approximation scheme, and contributions to them are welcome independently of Adam.
Martingale optimal transport asks for the cheapest way to couple two probability laws and on under the extra constraint that the coupling is the law of a one-step martingale. The problem arose in robust mathematical finance: when the prices of all call options at two maturities are observed, the marginal laws of the underlying asset at those maturities are known, and the no-arbitrage bounds on the price of a path-dependent option are the values of a martingale transport problem (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). The paper of Beiglböck and Juillet (arXiv:1208.1509v2, Ann. Probab. 44 (2016)) introduced the structural theory of the one-dimensional problem: a variational principle for optimal plans, a canonical coupling called the left-curtain coupling, and the identification of that coupling as the optimizer for a family of costs.
This mission formalizes that last identification. In classical optimal transport on the line, the monotone (quantile) coupling is the unique optimizer for every cost with strictly convex; the result here is the martingale counterpart, with a different coupling and a different convexity condition.
Let be Borel probability measures on with finite first moment. They are in convex order, , if for every convex (Definition 2.1). A transport plan is a measure on with first marginal and second marginal ; it is a martingale transport plan, , if under the conditional mean of given equals , equivalently
Strassen's theorem says exactly when .
A cost is a function . It satisfies the sufficient integrability condition if for all with , ; then is well defined for every plan. The martingale transport problem is
and a plan attaining the infimum is optimal.
A plan is (left-)monotone (Definition 1.4) if it is concentrated on a Borel set containing no three points with and . For a finite measure , its shadow is the least measure in the convex order among the measures with (Lemma 4.6). The left-curtain coupling is the plan that transports onto for every (Theorem 4.18); writing for the second marginal of , this says .
Let be probability measures, let be differentiable with strictly convex derivative , let satisfy the sufficient integrability condition, and assume . Then
The theorem shows that, for every cost with strictly convex (for instance ), the martingale transport problem has the same optimizer, determined by and alone. In the financial reading, the model-independent bound on the price of the corresponding forward-start payoff is attained by one explicit martingale, the same for the whole family. Remark 6.2 of the paper derives from it that also minimizes the essential supremum of . Theorem 1.9 packages the result as an equivalence of a geometric property (monotonicity), an optimality property and an order property of the curtain; later work on the left-curtain coupling, its explicit construction, and its extensions to higher dimensions and to multiple marginals takes these characterizations as its starting point.
The result is proved in the paper. As far as is known, none of it is formalized: Mathlib has the convex order neither for finite measures nor in the form used here, no martingale couplings, and no theory of shadows. The mission produces the statement layer (convex order on finite measures, martingale plans, extended-real costs, shadows, left-monotone plans, competitors) and asks for a machine-checked proof of the goal and of each milestone. The real-variable milestones (displays around (15)) are self-contained and elementary; the measure-theoretic ones carry the weight.
Optimality is a global property of a measure on , while monotonicity is a pointwise property of its support. Passing from the first to the second requires the variational lemma, whose proof uses a duality theorem for measures with prescribed marginal bounds and a measurable-selection argument; a direct perturbation of along a single bad triple fails because a triple of points carries no mass. The second obstacle is uniqueness of the monotone plan (Theorem 5.3), which needs the shadow construction and the associativity of shadows; monotonicity alone does not visibly pin down the plan. Existence of an optimizer needs weak compactness of , which is not immediate because the martingale condition is tested against bounded measurable, not continuous, functions.
All measures are Borel measures on and ; in the goal are probability measures. Convex order requires finite mass and finite first moment of both sides. Integrals that may be infinite (, for convex ) are computed in the extended reals as (the published ModelRiskOT.Duality.extIntegral), never as Bochner integrals. is encoded by the test-function condition displayed above (the paper's (4)). Shadows and the left-curtain coupling are predicates (IsShadow, IsLeftCurtain); their existence and uniqueness are theorems, and the goal asserts them rather than assuming them. Strict convexity of is strict convexity of deriv h on , with differentiable everywhere. Finiteness of costs is , which is the same as the existence of a martingale plan of finite cost (Theorem 6.1's wording).
A formalization that assumes an optimizer exists, or that asserts uniqueness only among left-curtain plans, is trivial and is not the goal: the statement asserts a plan with the left-curtain property, its optimality, and that every optimal plan equals it.
The development needs: weak compactness of plan sets on ; lower semicontinuity of extended-real cost functionals; the variational lemma (shared with the companion mission on Lemma 1.11); shadows and their order properties; and the uniqueness of monotone martingale plans. The shadow theory and the variational lemma are reusable across the whole series on this paper. Contributions on any milestone are welcome, including proofs of the elementary displays (15) and the rerouting inequality.
Many methods for minimizing a smooth convex function on a Hilbert space can be read as discretizations of second order ordinary differential equations, and the asymptotic behaviour of the continuous trajectories predicts the behaviour of the iterates. The inertial system with vanishing damping is the continuous counterpart of Nesterov's accelerated gradient method (Su, Boyd, Candès 2016); for its trajectories converge weakly to some minimizer of (Attouch, Chbani, Peypouquet, Redont 2018). Two modifications of this system have been studied separately. A Hessian driven damping term reduces oscillations while keeping the fast rate of the values (Attouch, Peypouquet, Redont 2016). A Tikhonov regularization term with selects a particular minimizer: under suitable decay of , trajectories approach the minimizer of minimum norm in the strong (norm) topology (Attouch, Chbani, Riahi 2018).
Boţ, Csetnek and László (arXiv:1911.12845v2, published in Mathematical Programming 2021) combine both terms and ask which properties of the two separate systems survive. This mission formalizes their strong convergence result, Theorem 4.4.
Let be a real Hilbert space, , , , and . The General assumption of the paper (p. 2) is:
A global -solution of the system
is a twice continuously differentiable curve satisfying (5) at every . The set is nonempty, closed and convex, so it has a unique element of minimum norm, denoted . The open ball is . In the Lean development these objects are GeneralAssumption g t₀ ε ε', IsSolution g α β t₀ ε u₀ v₀ x xd xdd and IsMinNormMinimizer g xstar in the namespace TikhonovHDD.Strong, with written minValue g.
Assume, in addition to the above,
that for all , for some and , and that if , while for large , for some , if . Then
and
if there exists such that stays either in or in its complement.
The three cases are exhaustive, so Cases I–III together give the goal.
Theorem 4.4 shows that adding Hessian driven damping does not destroy the selection property of Tikhonov regularization: the trajectory comes arbitrarily close to the minimum-norm minimizer, and converges to it in norm whenever it does not oscillate across the sphere forever. Since , the system still approaches , but the limit is a canonical minimizer determined by alone, not by the initial data. In infinite dimensions this is the difference between weak and strong convergence, a distinction that matters for ill-posed problems and inverse problems, where the minimum-norm solution is the one usually sought. Remark 4.5 of the paper compares the hypotheses with those of Attouch, Chbani and Riahi for the system without Hessian damping: for the lower bound required of when is, in the authors' words, "less tight" than theirs.
The result is proved in the paper; no part of it has a machine-checked proof. Formalizing it requires a Lyapunov-energy argument for a second order ODE in a Hilbert space, the weak lower semicontinuity of convex functions and of the norm, and the passage from weak to strong convergence via convergence of norms. Theorem 3.1 and Lemma A.1 are standalone results reusable for other Tikhonov-regularized inertial systems.
The weak convergence argument for the unregularized system (Opial's lemma) does not identify the limit, and it does not give strong convergence. Tikhonov regularization supplies the identification only through the Tikhonov curve , the minimizer of , and comparing with requires an energy whose derivative is controlled with weights tuned to . The Hessian term produces cross terms of the form that are absent from the system without Hessian damping; the integral hypothesis on and the slow-decay condition exist to absorb them. A direct energy estimate only works when ; inside the ball a different argument is required, and when the trajectory crosses the sphere infinitely often neither argument yields convergence of the whole trajectory, only a liminf statement.
Conventions committed to in Lean:
xd, xdd, ε'; and are continuous there.gradient g; is the Fréchet derivative of gradient g at applied to . "Lipschitz on bounded sets" means Lipschitz on every closed ball centred at .Filter.liminf is not used, since it returns for a function tending to .No statement of the mission has been repaired against the printed text.
A complete development needs: weak lower semicontinuity of convex continuous functions and of the norm on Hilbert spaces; weak sequential compactness of bounded sets; existence of the minimum-norm element of a closed convex set (Mathlib's projection onto closed convex sets); the strongly convex Tikhonov curve and its convergence to ; and calculus for energy functionals along curves on half-lines. Lemma A.1 and the Tikhonov-curve facts are reusable for every Tikhonov-regularized dynamics. Contributions of proofs of individual milestones, of supporting lemmas, and of alternative arguments are welcome.
Sinkhorn's algorithm is the standard method for computing entropically regularized optimal transport between two histograms. It is used throughout machine learning, statistics, imaging and graphics because each iteration is two matrix–vector products followed by entrywise divisions, which parallelize on GPUs and differentiate easily. The same iteration, under the names matrix scaling, RAS or iterative proportional fitting, has been used since the 1930s in transportation planning, economics and contingency-table analysis. Whether the iteration converges, and how fast, determines how many iterations a practitioner must run and which stopping criteria are reliable.
This mission formalizes the global convergence analysis of Sinkhorn's algorithm as presented in Chapter 4 (§4.2, Remarks 4.12–4.14) of G. Peyré and M. Cuturi, Computational Optimal Transport (2019).
Timeline. Sinkhorn (1964) proved that a positive matrix can be scaled to be doubly stochastic, and Sinkhorn and Knopp (1967) extended this to prescribed marginals. Birkhoff (1957) and Samelson (1957) independently showed that a positive linear map is a strict contraction of the positive cone for Hilbert's projective metric, with an explicit ratio. Franklin and Lorenz (1989) combined the two to prove that Sinkhorn's scalings converge linearly in Hilbert's metric at rate . Linial, Samorodnitsky and Wigderson (1998) related the iteration to the permanent.
Fix , a matrix with positive entries (in the book, the Gibbs kernel ), and vectors , with positive entries. Products and quotients of vectors are entrywise. The regularized transport plan has the form , where the scalings solve
Sinkhorn's algorithm alternately enforces each equation:
For vectors with positive entries, Hilbert's projective metric is
which vanishes exactly when and are proportional, and equals the variation seminorm with . Birkhoff's constants of are
Write and for a positive solution of (4.14).
For every ,
so both distances tend to ; for ,
and for the mirrored bound for with the half-step coupling . The book writes the rate as ; the constants stated are those its proof yields.
The result. Theorem 4.2 gives a global linear rate that holds from the first iteration, independent of the starting point, with a ratio computable from alone. Through (4.21) the rate transfers to the dual potentials , and the bounds (4.23) turn the marginal violations versus — which are computed anyway — into certified stopping criteria. Theorem 4.1 alone also yields a quantitative Perron–Frobenius theorem (Remark 4.13).
Formalizing it. All results here are classical and proved in the literature (Birkhoff 1957; Franklin–Lorenz 1989); Theorem 4.1 is quoted by the book without proof. To our knowledge neither Hilbert's projective metric on the positive cone, the Birkhoff–Hopf theorem, nor the convergence rate of Sinkhorn's algorithm has a machine-checked proof in Mathlib. The mission produces a reusable development of and Birkhoff's contraction theorem, and a certified rate and stopping rule for the most widely used optimal-transport solver.
Milestones 1–3 and 5–6 are finite manipulations of maxima of ratios. The central difficulty is Theorem 4.1. The obvious argument — bound entrywise by — only shows that is non-expansive (); it loses the strict contraction entirely. The sharp ratio depends on how acts on the two vectors jointly, which the entrywise argument does not see. The book quotes the theorem without proof, so the argument has to be supplied from Birkhoff's original paper or later expositions.
Lean namespace CompOT.Sinkhorn. Indices are -based (Fin n, Fin m); vectors are functions Fin n → ℝ, matrices Matrix (Fin n) (Fin m) ℝ, and and are the pointwise operations on functions. , and use real iSup/iInf over the finite index sets. Every theorem assumes , and positive entries for , , and every vector passed to , which excludes Lean's junk values for division by zero and logarithms of non-positive numbers. Sinkhorn's algorithm is a run predicate (IsSinkhornRun) stating the recursion (4.15) with ; is not an iterate and is unconstrained. The solution is any positive solution of (4.14), taken as a hypothesis (it exists iff ); the book's histograms are probability vectors, but only positivity is used. in (4.24) is , the solution of the regularized problem (4.2) by Proposition 4.3.
Deviations from the print, all disclosed in the items: the of (4.22) is replaced by the proof's explicit constants; the limit is stated as , since scalings are determined only up to ; the second inequality of (4.23) is false as printed (its right side is for ) and is stated with the half-step coupling the mirrored proof gives.
A definition of without the logarithm, or as a maximum of single-entry ratios, would make the statements different theorems; the definition here is the book's, and (4.21) is a milestone checking it against the variation seminorm. A run predicate not tied to , , , or an unsatisfiable one, is ruled out: the predicate is the recursion itself and is inhabited for every , , .
Contributions welcome: the metric properties of (reusable for Perron–Frobenius and nonlinear consensus), a proof of the Birkhoff–Hopf theorem, and positivity lemmas for Sinkhorn iterates.
A promise constraint satisfaction problem (PCSP) is given by a pair of relational structures with a homomorphism : an instance is promised to be satisfiable in , and it suffices to satisfy it in . The paper of Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970v3) develops the algebraic theory of PCSPs, in which the complexity of is governed by its polymorphisms.
The most prominent example is 1-in-3 versus Not-All-Equal-SAT: given a system of ternary constraints that has an assignment making exactly one variable in each constraint true, find an assignment making the variables in each constraint not all equal. Brakensiek and Guruswami (arXiv:1704.01937) showed that this problem is solvable in polynomial time, although both 1-in-3-SAT and NAE-SAT are NP-complete on their own. Their algorithm, like every tractability result for PCSPs known when the paper was written, works by finding a tractable CSP template with (a "sandwich") and solving the CSP over . For 1-in-3 vs NAE the template used is infinite: the integers with the relation .
Section 8 of the paper shows that this is unavoidable: no finite tractable template can be sandwiched, or more generally pp-constructed, in this way. This separates PCSPs from CSPs: infinite domains are necessary in the sandwich method.
Timeline: Feder and Vardi conjectured the CSP dichotomy (1998); Barto and Kozik characterised the borderline by cyclic polymorphisms (BK12, 2012); Bulatov and Zhuk proved the dichotomy (arXiv:1703.03021, arXiv:1704.01914, 2017); Brakensiek and Guruswami proved 1-in-3 vs NAE tractable (2018); Barto, Bulín, Krokhin and Opršal proved Theorem 8.1 (2019).
All structures here have one ternary relation. For a set and , is the structure with domain and relation . The 1-in-3 structure is and the not-all-equal structure is .
A homomorphism is a map with whenever . A polymorphism of of arity is a map such that, applied coordinatewise to any triples from , it yields a triple in . An operation is cyclic if for all (Definition 8.2).
The proof of Theorem 8.1 works in the following situation: is finite, and are homomorphisms, is a prime and is a cyclic polymorphism of of arity . From it builds the -ary operation
on matrices , and studies zero-one matrices, evaluated in through : their area (the fraction of ones), -equivalence , tameness ( with , or with ), covers (three matrices with exactly one in each position), the line segments (ones in the first positions in row-major order), and almost rectangles (columns of heights then , with step ).
Combined with the theorem of Barto and Kozik (a finite CSP template whose CSP is not NP-complete has cyclic polymorphisms of every prime arity ) and with the paper's Theorem 4.12, the core yields Theorem 8.1: if is pp-constructible from a finite , then is NP-complete. Hence the polynomial-time algorithm for 1-in-3 vs NAE cannot come from any finite tractable CSP, and the infinite template of Brakensiek and Guruswami is necessary. It is a concrete separation between PCSPs and CSPs: a tractable PCSP that is not explained by any finite tractable CSP.
The theorem is proved in the paper; nothing in this section has a machine-checked proof. The mission produces a formal proof of the combinatorial core, a reusable definition of cyclic operations on top of the platform's polymorphism library, and the matrix calculus of §8 (areas, covers, ), which is the part of the argument where index conventions are easiest to get wrong.
Polymorphisms of are not determined by their values on zero-one inputs, and nothing beyond cyclicity is known about . The obvious attempt, to show directly that restricted to depends only on the number of ones, fails: this property does not follow from cyclicity (Remark 8.15 asks whether polymorphisms of that kind always exist, and it is open). The only information available about is the coarse two-valued invariant on zero-one matrices, and the contradiction has to be produced from that invariant alone, uniformly over all finite ; the margin is what keeps the areas involved away from .
Structures are instances of the published PCSPBLPAff.Symmetric.RelStruct with the single-symbol signature Unit of arity ; homomorphisms and polymorphisms are the published IsHom and IsPolymorphism. The domain is Fin 2; is a Fintype with decidable equality. Matrices are functions Fin p → Fin p → Fin 2, row index first; the arguments of are read row-major via finProdFinEquiv; areas are rationals. Cyclicity is s a = s (a ∘ finRotate p), the paper's . The paper renames so that , ; the formalization keeps and evaluates zero-one matrices through it. Definition 8.11 prints column heights , but its proofs use height , so heights range over .
Lemmas 8.7–8.10 are stated with only the hypotheses their proofs use (Lemma 8.8 needs only cyclicity; Lemmas 8.9–8.10 need prime rather than ). Lemmas 8.13 and 8.14 concern a minimal counterexample inside the proof of Proposition 8.12 and are not separate items.
Left out: the NP-completeness conclusion of Theorem 8.1; the reduction from pp-constructibility to a homomorphic relaxation (Theorem 4.12, mission 1 of this series); the fact that a pp-power of a finite tractable CSP template is a finite tractable CSP template; and the cited Theorem 8.3 [BK12], which is never assumed or stated.
The goal ends in False, so it would be trivial if its hypotheses were contradictory for a reason unrelated to . They are not: , the 1-in-3 relation, satisfies every hypothesis except the existence of . No restriction is placed on beyond being a cyclic polymorphism; assuming idempotence or dependence on counts only would assume away the content (Remark 8.15).
Contributions welcome: proofs of the milestones, a general library of cyclic operations and their compositions, and a formalization of Theorem 8.3 or of the pp-power step, which would turn the core into Theorem 8.1 itself.
A large share of the optimization problems solved in statistics, signal processing and machine learning have the composite form
where is smooth and is convex but possibly nonsmooth or extended-valued (a norm penalty, the indicator of a constraint set). The workhorse algorithm for such problems is the proximal gradient method, which takes a gradient step on followed by a proximal step on . Its worst-case rate on convex problems is sublinear, yet in practice it often converges linearly. The classical explanation, going back to Luo and Tseng (1993) Ann. Oper. Res. 46, is an error bound condition: near the solution set, the distance to the minimizers is controlled by the length of the algorithm's own step. Under such a condition the method converges linearly.
The difficulty is that the error bound is stated in terms of the algorithm, not the problem. Drusvyatskiy and Lewis (arXiv:1602.06661, Math. Oper. Res. 43(3), 2018) showed that, for convex problems, it is equivalent to a purely geometric property of : quadratic growth away from the set of minimizers. This mission formalizes that equivalence (§3 of the paper) together with the three comparison results that build it.
Write for Euclidean space with norm , , and . A function is closed if it is lower semicontinuous. For real , the sublevel set is .
The problem is (3.1): is a closed convex function, and is convex, -smooth, with -Lipschitz gradient, . Let be the (nonempty) set of minimizers of and its minimal value. For the proximal map is
the proximal gradient method iterates , and the prox-gradient mapping is
so that and exactly at minimizers.
For , has quadratic growth with constant if on (3.12), and the error bound condition with parameters holds if on the same sublevel set (Definition 3.1, (3.13)).
for every step size and every .
For a closed convex with minimizers and minimal value :
The result. Corollary 3.6 converts a condition on an algorithm into a condition on the objective. Quadratic growth can be checked by hand in many models (strongly convex losses, polyhedral problems, problems with a sharp minimum), and once it holds, Theorem 3.2 gives linear convergence of the proximal gradient method with an iteration count of order , matching the rate familiar from strongly convex problems. The rest of the paper uses this equivalence as its main tool: §4 proves quadratic growth for structured problems under dual strict complementarity, and §§5–8 extend the comparison to prox-linear methods for nonconvex compositions. Theorems 3.3 and 3.4 are statements about a single closed convex function and are of independent use in the analysis of proximal point methods.
Formalizing it. All results here are proved on paper; none of them is machine-checked. The mission produces a Lean statement of the equivalence with the paper's explicit constants, and of the step-length comparison between the forward-backward and the proximal point methods for maximal monotone operators. Formal proofs require the existence, uniqueness and nonexpansiveness of resolvents and proximal maps, the subdifferential sum rule for a smooth plus a convex function, and a quadratic growth argument for convex functions; these are reusable well beyond this paper.
The forward direction is a chain of three inequalities, but each link compares objects that live in different worlds: the subdifferential of , the proximal map of , and the proximal map of evaluated at a gradient-shifted point. The proximal gradient step is not the proximal point step on , and the obvious attempt to compare with directly gives only one inequality (3.10); the reverse comparison (3.11) needs the resolvent of the sum and the Lipschitz constant of . The converse half of Theorem 3.3 (error bound implies growth) is the deepest step: the paper omits its proof and cites Drusvyatskiy–Ioffe and Drusvyatskiy–Mordukhovich–Nghia. It has to pass from a pointwise bound on subgradients to a bound on function values over the whole sublevel set, which no single subgradient inequality provides.
EuclideanSpace ℝ (Fin n); -valued functions are EReal-valued; is real-valued and is computed in EReal. "Closed convex" is the published RockafellarMaxMono.Shared.ProperConvex (never , somewhere finite, convex) together with LowerSemicontinuous.Metric.infDist; is real.GoldenRatioVI.Shared.IsProxPoint (fun y => t * g y) z p (same argmin for ), and resolvents are maps satisfying the published ThreeOpSplitting.Convergence.IsResolvent. Conditions are stated for every such point; existence and uniqueness are facts a solver proves.Metric.infDist 0 (∂h x), which is on the empty set, would turn (3.7) into the false claim that every point of the sublevel set where is empty is a minimizer; this trivializing or falsifying encoding is ruled out.ProxAlg.FixedPoint.subdifferential, the gradient is Mathlib's gradient.Contributions welcome: proofs of the milestones in any order, general lemmas on resolvents of maximal monotone operators and on proximal maps of EReal-valued convex functions, and a proof of the converse half of Theorem 3.3.