Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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.
Large traders who must unwind a position by a deadline face a trade-off between trading fast, which moves prices against them, and trading slowly, which exposes them to price risk. When many traders liquidate at once, each one's execution price also depends on the aggregate selling rate of the others. Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and a hard liquidation constraint: every position must be zero at the terminal time . Single-player liquidation with this constraint leads to backward equations with singular terminal values (Ankirchner, Jeanblanc and Kruse, SIAM J. Control Optim. 2014; Graewe, Horst and Séré, Stoch. Proc. Appl. 2018). Earlier MFG models of execution (Cardaliaguet and Lehalle, Math. Financ. Econ. 2018; Carmona and Lacker, Ann. Appl. Probab. 2015) allow no liquidation constraint. This mission formalizes the paper's first main result: the constrained game has a unique equilibrium under a weak-interaction condition.
Fix and a probability space carrying an -dimensional Brownian motion , where is the one-dimensional common noise, and an initial portfolio independent of . Let be the filtration of and that of , both augmented by null sets. The cost coefficients are bounded nonnegative -progressive processes (interaction), (risk aversion) and (temporary impact), with bounded away from zero.
A player's trading rate produces the position . The admissible strategies are . Given an -progressive aggregate rate , the cost is
and is its essential infimum over . A process solves the MFG (1.7) if some optimal strategy given satisfies for a.e. .
The equilibrium is described by the conditional mean-field FBSDE (2.3):
Solutions are sought in weighted spaces: if , and if is essentially bounded. The weak-interaction condition (Assumption 2.3) asks for with , and . The decoupling uses the solution of the singular Riccati BSDE , .
Under Assumption 2.3 the FBSDE (2.3) has a unique solution
is optimal, is the optimal position, is the unique solution of the MFG (1.7), and
The milestones follow the paper's proof: Fact 2.2 on the weighted spaces; Lemma A.1, existence and uniqueness of with the bounds (A.1), and ; the decay estimate (2.9), ; Lemma 2.5, an a priori estimate for the decoupled system (2.11) with homotopy parameter ; Lemma 2.6, explicit unique solvability at ; Lemma 2.7, the continuation step ; Proposition 2.8, unique solvability of (2.3) with (2.10) and a norm bound; the boundary limit (2.15); and Proposition 2.9, optimality, the equilibrium property and the value formula.
The theorem gives a complete equilibrium description for constrained liquidation with many players and stochastic, partially common market data: the equilibrium rate is the conditional expectation of the decoupled feedback rate given the common noise, and its value is explicit in terms of the Riccati solution. It is the basis of the paper's other two results, the -Nash property of the equilibrium in the -player game (Theorem 3.3) and the approximation by penalized games (Theorem 4.6), which are separate missions in this series.
The result is proved in the paper; none of it is machine-checked. A formal development would contain the first formal treatment of BSDEs with singular terminal value and of a conditional (common-noise) mean-field FBSDE. Shorter proofs of individual steps, in particular of the a priori estimate and the continuation step, are welcome.
The obvious approach fails at the terminal time. Standard FBSDE theory requires a terminal condition for ; here only is known, and is undetermined. The decoupling coefficient blows up like , so the driver of the equation for is singular, and the classical monotonicity method of Hu–Peng and Peng–Wu, applied to in unweighted spaces, does not close. The paper works instead with weighted norms that encode the rate at which and vanish at , and runs the continuation on the triple . The mean-field term is a conditional expectation given the common-noise filtration, not an expectation, so it remains random and has to be controlled pathwise in the weighted norms.
Time is ℝ≥0; processes are real valued and has coordinates, coordinate being . The Itô calculus is the published definition Peng1990.SMP.Stochastic (standard Brownian motion, , Itô integrals, BSDEs in integrated form). The explicit choices:
ℝ≥0∞.The interaction term must stay conditioned on : conditioning on makes it itself and collapses the game. The constraint and the admissibility condition cannot be dropped either. The degenerate instance satisfies all hypotheses but decouples the game.
A complete development needs the following, all reusable beyond this mission: martingale representation for the augmented filtration ; existence of progressive versions of conditional expectation processes; Doob's inequality on ; and linear BSDE solution formulas.
A constraint satisfaction problem (CSP) asks whether variables can be assigned values so that every constraint, drawn from a fixed finite set of relations, holds. The algebraic approach to CSPs explains their complexity through polymorphisms, the operations that preserve all constraint relations; this programme culminated in the CSP dichotomy theorem of Bulatov and Zhuk (2017). A promise CSP (PCSP) pairs each relation with a weaker relation : given an instance that is promised to be satisfiable with the -constraints, one must distinguish it from instances that are not even satisfiable with the -constraints. Approximate graph colouring (is a 3-colourable graph 100-colourable?) and -SAT are PCSPs, and their complexity is not captured by the classical theory.
Brakensiek and Guruswami (arXiv:1704.01937) developed the polymorphism theory of PCSPs and classified the Boolean, symmetric, folded case.
Timeline.
Fix the Boolean domain . A promise relation of arity is a pair with , and a family is a finite set of promise relations, possibly of different arities. A function is a polymorphism of if, whenever , applying coordinate-wise gives a tuple in ; is the set of functions that are polymorphisms of every member of .
A relation is symmetric if it is closed under permuting coordinates. Every symmetric relation has the form , where is the Hamming weight. A function is folded if , and idempotent if and ; a family is folded (idempotent) if all its polymorphisms are. For odd the paper singles out three function families:
and their negations . Finally, is -fixing if some set of at most coordinates satisfies whenever vanishes on .
Let be a finite, folded, symmetric family. If there are odd with
then
No value of is fixed: the goal asserts only that one bound works for all arities.
The milestones follow the paper's proof:
Theorem 4.13 is the structural half of the paper's main dichotomy (Theorem 2.16): a folded symmetric Boolean PCSP is polynomial-time solvable if it has one of the six families as polymorphisms for every odd arity, and NP-hard otherwise. Hardness follows by feeding the -fixing structure into a Label Cover reduction (Theorem 5.3). Bounded "fixing" or junta-like structure of all polymorphisms is the standard route from algebra to NP-hardness for PCSPs. This theorem is the cleanest Boolean instance of it, and it underlies later classifications of symmetric Boolean PCSPs.
The result has been proved and published since 2018. To our knowledge none of it has been formalized. A formalization supplies a checked Boolean polymorphism toolkit (Hamming-weight relations, folding, idempotence, relaxations), checked closure computations under alternating-threshold and majority operations, and a uniform-constant Frobenius-type lemma. All of these can be reused by other Boolean PCSP missions.
The obvious argument fixes a polymorphism and bounds its relevant coordinates directly from a constraint that , or violates. This gives a bound that depends on the arity , and an -dependent bound is trivial ( always works). The work is in making the constant uniform. The proof has to replace by a single canonical promise relation that does not depend on , classify exactly which symmetric relations exclude and , and use an additive-combinatorics lemma whose constants depend only on that relation's arity. Its bounded version must hold with the same constants. The non-idempotent polymorphisms need a separate reduction through the negated family .
The domain is Bool (false ). A family is a pair of relational structures 𝔸 𝔹 : RelStruct τ ar Bool from the published definition PCSPBLPAff_Symmetric_Setting, with [Fintype τ] (finitely many relations) and 𝔸.rel R ⊆ 𝔹.rel R (promise). IsPolymorphism 𝔸 𝔹 f from that file is Definition 2.4. Coordinates are Fin L, so the 1-based sign of becomes . Anti-functions negate the output. Family properties (folded, idempotent, non-degenerate) quantify over polymorphisms of every arity . A folded or idempotent family has no nullary polymorphisms, so admitting changes nothing. The constants , , and are quantified before the arity and the function (respectively before ). A statement that lets the constant depend on or is trivially true and is not the goal.
Out of scope are the complexity conclusions: "PCSP() is NP-hard" (Theorems 2.16 and 5.3) and item 2 of Lemma 2.13 (transfer of tractability). The cited inputs for those conclusions are also out of scope: the PCP theorem with parallel repetition (Proposition 5.2) and Schaefer's theorem. No complexity predicate appears in any statement.
A complete development needs the following, with Mathlib's Nat.frobeniusNumber as a starting point for Lemma 4.9:
Contributions are welcome at any milestone, including separate proofs of the closure computations and of Lemma 4.9.
A trader who must sell a large position within a fixed horizon faces a trade-off: selling fast moves the price against her (temporary price impact), selling slowly exposes her to price risk. Since Almgren and Chriss, this optimal liquidation problem has been studied as a stochastic control problem with a terminal state constraint: the remaining position must be zero at the horizon . When many traders liquidate at the same time, each trader's sales also depress the price that the others receive (permanent price impact), and the problem becomes a game.
Fu, Graewe, Horst and Popier (arXiv:1804.04911v3) study this game in the mean-field limit. Their §2 constructs a mean-field equilibrium through a singular conditional mean-field FBSDE. Their §3, the subject of this mission, justifies the limit: the strategies computed from the mean field game are an approximate Nash equilibrium of the finite game with traders, with an error of order . Without such a result, the mean-field equilibrium describes a model nobody plays; with it, the equilibrium is a usable approximation for large but finite markets.
The approximation of -player games by mean field games goes back to Huang, Malhamé and Caines (2006) and Lasry and Lions (2007); Carmona and Delarue (SIAM J. Control Optim. 51, 2013) proved an -Nash property for a McKean–Vlasov class with state interaction and a rate . The present game differs in three respects: players interact through their controls (the average trading rate), there is a common noise observed by all, and each player's state must reach zero at time .
A single probability space carries a one-dimensional Brownian motion (the common noise, which drives the benchmark price and is observed by every player), for each player a -dimensional Brownian motion (the private noise), and i.i.d. initial portfolios with law ; all of these are mutually independent. Player observes , , and chooses a trading rate ; her position is and must satisfy . Given the profile , her conditional cost is
where (permanent impact), (temporary impact) and (risk aversion) are nonnegative bounded processes. Under Assumption 3.1 they are the same deterministic measurable functionals of for every player, so the players are statistically identical.
In the mean field game, the average is replaced by a process adapted to the common-noise filtration , and an equilibrium is a with for the representative player's best response . The paper characterizes it through the FBSDE (2.3),
with ; the optimal rate is . Player 's mean-field strategy comes from the same FBSDE with her own data.
For a positive function with , where , and admissible sets , there is a function , independent of and , with
The goal asserts only the shape of the bound, not its constant.
The result turns the mean-field equilibrium of §2 into a statement about the finite market: when all traders use their mean-field strategies, a trader who deviates can save at most in conditional expected cost. The error bound depends on the trader's own initial position only through , and the rate is dimension-free, in contrast with the rates of state-interaction games, because the interaction runs through the empirical mean of the controls rather than through an empirical measure.
The paper's proof of Theorem 3.3 is short but rests on several facts it states without proof: the Yamada–Watanabe-type Lemma 3.2 (whose proof is referred to other papers), the identification (3.2) of a common conditional mean, and the moment bound (3.3) attributed to Proposition 2.8. This mission makes each of these a separate machine-checkable statement. As far as we know, none of these results, nor any optimal-liquidation mean field game, has a machine-checked proof.
The estimate (3.5) is a law-of-large-numbers bound for the average of processes that are not independent: all of them depend on the common noise . The obvious argument, expanding the square and using independence, fails as stated; the cross terms vanish only conditionally on , and only once one knows that every is the same measurable functional of . That is Lemma 3.2, a Yamada–Watanabe-type statement for a singular FBSDE with a conditional mean-field term, which needs strong uniqueness of the FBSDE in the class and is the main technical step. The terminal constraint makes the backward component singular at ( blows up like ), so standard Lipschitz FBSDE theory does not apply. Finally, the deviation is constrained only through a conditional second-moment bound , and the comparison with the mean-field cost uses the optimality of (Proposition 2.9) against .
Everything is stated on one probability space carrying all players, with players indexed by ; the -player game uses players (the paper's , shifted by one). Time is and the processes are real valued. Choices made explicit:
The development reuses the Itô-calculus definitions of Peng1990.SMP.Stochastic (standard Brownian motion, , Itô integrals, BSDEs). Contributions useful beyond this mission: conditional independence given a common noise for functionals of independent inputs, a Yamada–Watanabe argument for FBSDEs, and conditional Cauchy–Schwarz bounds for time integrals. Proofs of any milestone, and of the facts from §2 they rely on, are welcome.
Brands are routinely held responsible for the labour and environmental practices of their suppliers. A brand that is linked in public to a non-compliant supplier loses consumer willingness to pay, and firms answer this risk by auditing their suppliers. Supply networks are not trees, however: one supplier often serves several competing brands. Chen, Qi and Dawande (SSRN 2889889, Manufacturing & Service Operations Management, 2020) ask how the position of a supplier in such a network, and in particular its centrality (the number of buyers it serves), affects which suppliers get audited when buyers decide on their own, and when they audit jointly.
This mission formalizes the paper's answer for unilateral auditing by competing buyers (Sec. 4.2, Proposition 2). A companion mission treats joint auditing (Proposition 3).
Two buyers source from three suppliers: an independent supplier for each buyer , and a common supplier that serves both. Each supplier complies with social-responsibility standards with probability . In stage 1, buyer chooses an auditing effort on and on , and audits at most one of them: . Auditing a supplier with effort costs , with a fixed cost and ; effort means no audit and costs nothing.
A non-compliant supplier that passes the audits is discovered in public with probability . Hence causes damage to with probability , and causes damage to both buyers with probability , independently. A buyer with at least one exposed supplier suffers the MWTP damage : his demand intercept drops from to . Each exposed supplier is then paid per unit instead of , so a buyer with exposed suppliers has unit cost .
In stage 2 the buyers compete in quantities with inverse demands , (Dixit 1979; Singh and Vives 1984). Its equilibrium profit for is , in closed form (Lemma 1). Buyer 's ex ante expected profit is the expectation of over the eight damage outcomes, minus his audit costs; is symmetric. Three conditions on (p. 8) make all stage-2 quantities positive.
An equilibrium is a profile , , in which each buyer's strategy is a best response to the other's, with the tie-breaking rule of p. 10: a buyer who is indifferent between auditing and not auditing does not audit. Two explicit efforts, (eq. (1)) and (eq. (2)), are rational functions of the parameters; is a buyer's optimal effort on his independent supplier when the rival audits nobody, and is the symmetric solution when both audit their independent suppliers.
Assume and . There exist such that for every , writing , , , ,
In every equilibrium the common supplier receives zero effort.
Lemma 1 (stage-2 equilibrium), the OA.2 expected-profit display, the best-response function (OA-9) with and as its values, the dominance inequality (OA-11), Lemmas OA5 and OA6 (the two kinds of auditing equilibria and their threshold ranges), the monotonicity facts (OA-14)–(OA-15), Lemma OA7 (the order of the thresholds) and Lemma OA8 (no equilibrium audits ). The thresholds of the milestones are the explicit ones the proof defines in (OA-10), (OA-12), (OA-13).
The result separates network position from competition. Without downstream competition (, Proposition 1) there is a Pareto-dominant equilibrium in which one buyer audits the common supplier. With competition, Proposition 2 shows that the common supplier, the most central and therefore the most consequential source of risk, is never audited: auditing it would also protect the rival, who free-rides. This inefficiency is what motivates the paper's analysis of joint auditing (Proposition 3) and of social welfare (Proposition 4).
The result is proved in the paper, partly by omission: the e-companion leaves the proof of Lemma OA8 and the case to the reader. No machine-checked version exists. A formal proof would give a complete case analysis of a two-stage game with a discontinuous fixed cost, a constrained strategy set and a tie-breaking rule, and would check the paper's closed forms, several of which are printed with small slips.
The first-order conditions alone do not determine the equilibria. The fixed cost makes each buyer's payoff discontinuous at zero effort, so every candidate must be compared with no audit, and the best response is a choice among three regimes (audit , audit , audit nobody). Uniqueness claims therefore require excluding every profile in the constrained strategy set, including those where a buyer audits the common supplier, for which the paper gives no proof. The threshold comparisons rest on monotonicity in the rival's effort, and the expected profit is multilinear in the four efforts (plus the quadratic audit costs), with coefficients that are differences of squared Cournot quantities whose signs depend on the p. 8 conditions.
All objects live in the namespace SupplierAudit.Competition. The source is the authors' accepted manuscript on SSRN (2889889); main-text printed pages equal PDF pages, and e-companion page ec is PDF page .
Params carries and the standing assumptions , , , , , and the three conditions of p. 8. The theorems add (competition, Sec. 4.2). is a separate real argument and the goal quantifies over .CournotDuopoly). The model's stage-2 profit is the closed form for all ; Lemma 1 states that it is the game's unique equilibrium.A formalization in which equilibrium is plain Nash, efforts range over all of , a buyer may audit both suppliers, or "interior" is a hypothesis on the equilibrium efforts themselves would state a different (and in places false or vacuous) theorem; these are ruled out by the definitions above. Proofs of any milestone are welcome, as is reusable infrastructure for linear Cournot duopolies and for finite expectations over independent Bernoulli events.
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.
Many quantities in stochastic control, mathematical finance and stochastic differential games depend on the whole past of a Brownian path rather than on its current position: the price of an Asian or lookback option, the value of a control problem with delay, the solution of a non-Markovian backward stochastic differential equation (BSDE). For Markovian problems the value is a function and solves a parabolic PDE, and the theory of viscosity solutions (Crandall, Ishii and Lions) gives existence, uniqueness and stability without any smoothness. For path-dependent problems the value is a functional of the path, and the corresponding equation is a path-dependent PDE (PPDE), written with the horizontal and vertical derivatives introduced by Dupire (SSRN 1435551) and developed into a functional Itô calculus by Cont and Fournié (arXiv:1002.2446). Classical solutions of PPDEs rarely exist, so a weak notion is needed.
Timeline:
Fix and . Let be the space of continuous paths with , the canonical process, the filtration it generates, the Wiener measure and . On the pseudometric is . For , is the space of continuous paths on vanishing at , with Wiener measure , and the space of càdlàg paths on . The concatenation follows up to and then , and .
A functional on has the Dupire derivatives , the derivative under a bump of the path, and , the right derivative in time along the stopped path. is the class of functionals that agree on continuous paths with some whose derivatives , , exist and are bounded and -continuous.
The equation is the semilinear PPDE
For , and are the infimum and supremum of expectations under the Girsanov measures , . A bounded -continuous is a viscosity -subsolution if at every with for every test function that touches from above in the sense
where is a class of stopping times with open level sets. Supersolutions use and . A viscosity subsolution is an -subsolution for some , the same at every point. The candidate solution is , where solves the BSDE with terminal value and generator under .
Under Assumption 4.2 ( bounded, progressively measurable, continuous in , uniformly continuous in , Lipschitz in ; bounded and uniformly continuous) and Assumption 4.4 (an extension of to càdlàg paths, continuous and Lipschitz), for every viscosity subsolution and supersolution ,
and consequently is the unique viscosity solution with terminal condition .
In the order the proof uses them: Example 2.5 (hitting times lie in ); Proposition 5.4 ( is uniformly continuous); Theorem 4.3 ( is a viscosity solution); Lemma 5.7 (partial comparison when one of is smooth) and its form under the weaker condition (5.11); the bound of (6.3) between the Perron envelopes
Lemma 6.3 (classical solutions built from an ODE with random coefficients); and Theorem 6.1, .
Theorem 4.6 makes the definition of the paper a well-posed one: existence (Theorem 4.3) without uniqueness would allow any number of solutions, and the comparison principle is what identifies the BSDE value as the solution. It gives a path-dependent nonlinear Feynman–Kac formula, characterising non-Markovian BSDEs analytically, and it is the template on which the fully nonlinear theory, path-dependent games and non-Markovian control were later built.
The result is proved, in this paper, and the proof is not known to have been machine-checked. The formalization contributes a precise Lean account of the definitions (Dupire derivatives through extensions to càdlàg paths, the stopping-time class , Girsanov measures, the piecewise class ) and a checked proof of comparison. Pieces of independent value are a functional Itô formula for functionals, Girsanov's theorem on the canonical space, comparison for BSDEs, and optimal stopping under the nonlinear expectation .
The classical proof of comparison doubles variables and uses the Crandall–Ishii lemma, which rests on local compactness of the state space; is infinite-dimensional and not locally compact, so that route fails. The paper instead proves comparison when one side is smooth (Lemma 5.7), and then shows that the Perron envelopes and , built from piecewise-smooth super- and subsolutions, coincide. That equality needs an approximation of an arbitrary square-integrable BSDE integrand by processes that are piecewise differentiable in time with uniformly continuous derivative, so that the resulting functionals lie in (Lemmas 6.3–6.5). The partial comparison relies on optimal stopping under , which the paper treats with heuristic arguments in Remark 3.11 and references to later work, so that step will need its own development.
Time is with a fixed horizon ; paths take values in Euclidean and are constant after . is encoded as continuous paths vanishing on and as càdlàg paths constant on , so . Filtrations are the raw ones generated by the canonical process. The Wiener measure is a hypothesis on finite-dimensional laws, and is its image under the shift. The stochastic integral and BSDE solutions are those of the platform definition Peng1990.SMP.Stochastic.
Conventions and readings, all disclosed in the items:
No trivializing reading is available: the test functions are exactly the functionals satisfying (3.6), the measures exactly the Girsanov measures with , and the stopping times exactly . A test set that is too large makes sub- and supersolutions scarce and the comparison principle weaker, a test set that is too small makes them abundant and the principle false, and neither is the case here.
The source is arXiv:1109.5971v2, the IMS electronic reprint of the Annals of Probability article; its printed page numbers equal the PDF's. Lemmas 6.4 and 6.5 (the approximation of ) are part of the proof but not stated as items. Contributions welcome: the functional Itô formula, Girsanov on , BSDE comparison and stability, and the optimal stopping theory under .
Best-subset selection with ridge shrinkage, , is a mixed-integer program that statisticians want to solve to certified optimality at the scale of modern data ( up to features). Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) built a branch-and-bound solver, L0BnB, whose node relaxations are solved in the primal space by active-set coordinate descent instead of by an interior-point method. Branch-and-bound prunes a node only with a valid dual bound, a certified lower bound on the node's relaxation value. A primal method returns an approximate minimizer, not such a bound, so the solver must turn an inexact primal point into a dual feasible point and needs to know how much is lost in doing so. This mission formalizes the paper's answer, its main theorem (Theorem 3).
Data are with columns , , and parameters . The reverse Huber penalty is for and for . The penalty equals if and otherwise. The reduced relaxation (5) is
Throughout, the columns of and have unit norm (the standing assumption of Section 3 of the paper).
Algorithm 2 (active-set coordinate descent) returns a point in the box such that the set
is empty: no coordinate outside the support wants to move. Write , , and let be an optimal solution of (5) with . The primal gap is .
The two duals of (5) (Theorem 2 of the paper) are, with ,
the latter under . The dual variables built from are , and . The dual points built from are , with a maximizer of (25) and a maximizer of under the constraints (27).
If , with when and when ,
If ,
The paper states these as (29) and (30); the goal states the expressions its proof establishes.
In the order the proof uses them: the closed-form coordinate updates (14) and (15); Proposition 3, ; the bound ; Lemma 2, which bounds coordinate by coordinate and makes it vanish off the support; inequality (53); the closed form (28) of ; the optimality conditions (58); the bound (57) on the support; and inequality (56).
The result. In both regimes the loss of the dual bound is controlled by the primal gap times the sparsity of the iterate, with constants depending only on and ; the number of features does not enter. Since L0BnB seeks solutions with , the cheap dual bound obtained from an inexact primal solution is nearly as good as the exact one, which is what allows pruning without an interior-point solve at every node. The paper notes that with plain coordinate descent in place of Algorithm 2 the same argument gives in place of .
Formalizing it. The result is proved in the paper; it has no machine-checked proof. The mission produces a checked version of the main theorem with explicit constants, a formal model of what "output of an active-set method" means for the analysis, and reusable closed forms for the boxed soft-thresholding updates of an - or reverse-Huber-penalized box-constrained least squares problem.
The bound is not a consequence of weak duality alone: weak duality says only that each dual value is below the primal optimum, and says nothing about how far the constructed dual point is from the dual optimum. The obvious estimate, a Lipschitz bound on or summed over all coordinates, gives a loss proportional to . Getting instead requires showing that the dual contribution of every coordinate outside vanishes exactly, which uses the emptiness of through Proposition 3 and the closed forms (14)–(15) of one-dimensional nonsmooth box-constrained problems. On the support, the loss must be bounded using the structure of and at coordinates where hits the box, which is where and (58) enter.
Indices are Fin p; norms are explicit sums; is Real.sign with ; is max a 0. The unit norms of the columns of and of are hypotheses, never built into the definitions, and each theorem assumes only the ones it uses. is any point of the box minimizing over the box. The output of Algorithm 2 is modelled by its two properties used in the paper: and ("" encoded as " is not a minimizer"); the iterations are not formalized. and are arbitrary maximizers satisfying (25) and (27). The dual variables (23)–(24) are defined by their formulas; their optimality (Theorem 2, a separate mission) is neither assumed nor needed, and the goal is an inequality between explicit numbers.
Instantiations of . (29) is stated as (55): becomes with decided by . (30) is stated as (59): becomes . The proof's final rearrangement of (29), which counts instead of , is not used.
A formalization that takes , or , that drops the hypothesis , or that replaces the constants by an existential "" would be trivial or a different statement; the goal quantifies over every optimal , every box-feasible with and every maximizer , , with the explicit constants above.
Needed infrastructure: one-dimensional convex minimization on an interval with piecewise penalties, Cauchy–Schwarz for finite sums, and first-order optimality conditions for box-constrained composite problems. Proofs of any milestone are welcome independently.
Best subset selection with a ridge term, the -regularized least squares problem
is a standard model for sparse linear regression. It can be solved to certified optimality by branch-and-bound (BnB) over a mixed integer formulation, and the speed of BnB depends on how tight the lower bounds of its node relaxations are. Two mixed integer formulations are in common use: the Big-M formulation, which links each coefficient to a binary indicator through a box (Bertsimas, King and Mazumder, 2016), and the perspective formulation, which replaces by an auxiliary variable constrained by a rotated second-order cone (Frangioni and Gentile, 2006; Günlük and Linderoth, 2010). Which formulation gives the stronger continuous relaxation decides which one a solver should be built on.
Hazimeh, Mazumder and Saab (2021) compare the relaxations in Section 2. Their Proposition 2 compares the interval relaxation of the Big-M formulation with that of the perspective formulation without a box, , studied by Dong, Chen and Linderoth (2015). This mission formalizes that comparison.
Fix a design matrix , a response , parameters and a bound . Write and for for every .
The Big-M formulation (2) is
Its interval relaxation replaces by ; its optimal value is . Eliminating gives the equivalent form (37),
The reverse Huber penalty is for and for , and . The interval relaxation of has the value (6),
Let be the set of minimizers of , and, as in (9),
The comparison runs through the scalar function and through .
The mission also contains the scalar inequality (39) as a supporting statement (not a milestone): for and , .
Proposition 2 says that neither relaxation dominates the other. For a tight Big-M bound the Big-M relaxation yields the larger lower bound; for a loose one, provided some optimal solution of lies in the box, the perspective relaxation does. Equivalently, with the other data fixed, a small favours the Big-M relaxation and a large favours (p. 8). Together with Proposition 1 of the same paper, which shows that the box-constrained perspective relaxation beats both when , this motivates the paper's choice of as the formulation on which its BnB solver is built.
The proposition is proved in the paper (Appendix A, pp. 29–30). No machine-checked proof of it, of the reformulation (37), or of any property of the reverse Huber penalty exists on the platform. The mission produces a formal statement of both inequalities with every hypothesis explicit, and the definitions of the two relaxation values in a form that later missions on perspective relaxations can reuse.
The scalar inequalities (39) and Lemma 1 are elementary but split into cases at the kink of the reverse Huber penalty, , and at the sign of . The passage from coordinatewise inequalities to optimal values is where care is needed. is defined over pairs , and its identification with a minimum of over a compact box requires eliminating and showing attainment. For (11) a pointwise comparison of and on the box only bounds by the box-restricted value , not by , which is an infimum over all of ; the hypothesis is what closes this gap, and dropping it gives a statement the paper does not prove.
All declarations live in the namespace L0BnB.BigMvsPR. Vectors are Fin p → ℝ, is a Matrix (Fin n) (Fin p) ℝ, and is X *ᵥ β. Every norm is an explicit sum: , and is . The reverse Huber penalty is an if on .
Optimal values are real infima (sInf): over the feasible pairs of the interval relaxation, over all of , over the box. For each set of values is nonempty () and bounded below by , so no infimum takes Lean's junk value. is defined as the displayed minimum (6); its identification with the interval relaxation of is a result of Dong, Chen and Linderoth that the paper cites and does not prove, and it is not part of this mission. is the set of minimizers of , as the paper uses it in the proof of (11).
All theorems assume . The paper remarks that Proposition 2 applies for any ; is excluded because and divide by . The goal is stated for optimal values, not for the objective functions at a single point: a pointwise comparison of and is a milestone, not the proposition. Milestone (37) is stated with IsLeast, so it asserts attainment as well as the value.
The paper states no bounds in this result, so no constants are instantiated. Contributions welcome: proofs of the scalar lemmas, of (37) (which needs compactness of the box and continuity of ), and of the goal.
Mean field games (MFGs) were introduced by Lasry and Lions (Jpn. J. Math. 2007) and by Huang, Malhamé and Caines (Commun. Inf. Syst. 2006) as limits of stochastic differential games with many symmetric players whose interaction runs through the empirical distribution of their states. An MFG is a fixed point problem for one representative player facing a flow of measures, and it is much easier to analyse than an -player game. The justification for studying it is a converse statement: a solution of the MFG should yield strategies that are nearly optimal for every player of the finite game when is large. Results of this type were proved by Huang, Malhamé and Caines for linear-quadratic models and by Carmona and Delarue (SIAM J. Control Optim. 2013) in the strong formulation with Lipschitz data.
Carmona and Lacker (arXiv:1307.1152v2; Ann. Appl. Probab. 25(3), 2015) set up MFGs in a weak formulation: controls change the law of the state through a Girsanov density instead of entering the state equation. This allows measurable, path-dependent data and controls that need only be progressively measurable. Their Theorem 4.2 is the finite-player approximation in this generality. This mission formalizes it.
Let with the sup norm, and fix a measurable weight . is the set of probability measures on with , carrying the topology : the weakest topology making continuous for every measurable with . The control set is a compact convex subset of a normed space, and carries the weak topology.
The data are a volatility , a drift , a running reward and a terminal reward , where is a whole path, and . On a probability space with an initial value and an independent Wiener process , let solve , . A control (an -valued progressive process) and a measure define a new probability with density
under which has drift . The reward is . A pair is a solution of the MFG (Definition 3.4) if some maximizes and reproduces the input: and for a.e. . Under the standing assumptions the optimal control is a function of the path, the closed-loop control.
The -player game. On a probability space with independent Wiener processes and i.i.d. initial values , let solve (the drift has no mean field term under (F.1)). The distributed controls are : each player uses only their own state. A deviation is any process that is progressively measurable for the filtration of all states (full information). A profile changes the probability to , with density the Doléans exponential of . Player then receives
with and .
Under (S), (C) and (F), there is a sequence , , such that for all , and ,
No rate is claimed; the theorem asserts only that the gain from deviating vanishes uniformly over players and deviations.
Theorem 4.2 states the sense in which an MFG solution solves the finite game. It covers path-dependent and merely measurable coefficients, interaction through the law of the controls, and full-information deviations against distributed strategies. In the paper it underlies the applications of §6: the price impact model, where Proposition 6.1 adds the rate , and the flocking model. The result is qualitative: it gives no rate in general.
The result is proved in the paper. No machine-checked proof of it or of its lemmas exists on the platform. The mission produces a formal statement layer for weak-formulation MFGs: path space, with , Girsanov densities over Itô versions, Definition 3.4, and the -player game. It then asks for the formal proof of the theorem. Missions 1 and 2 of this series (existence and uniqueness of MFG solutions) use the same model encoding. The strong-formulation result of Carmona and Delarue is a separate statement with a separate model and is not part of this mission.
The obvious route replaces by and by in and appeals to the law of large numbers. This fails for two reasons. First, the expectation is taken under , which depends on the deviation , and may depend on all players' states. The convergence therefore has to be uniform over a class of measures and requires uniform integrability of the densities. Second, is neither metrizable nor separable. Continuity in does not reduce to sequences, and dominated convergence does not hold for nets, so the almost sure convergence of empirical measures does not by itself transfer to the rewards. The remaining step asks whether full information helps the deviating player against the limiting environment. It is not a direct consequence of the optimality of in the mean field problem, which is posed over a smaller filtration.
Fin d → ℝ. is C(Set.Icc 0 T, Fin d → ℝ) with its Borel σ-field. Time is ℝ≥0; only matters.ProbabilityMeasure A with the weak topology and its Borel σ-field. Progressive measurability uses the canonical filtration on .Peng1990.SMP.Stochastic Itô layer. "Strong solution" therefore includes square integrability, and .⨆.Two readings of the goal would make it trivial, and the statement excludes both. If were allowed to depend on or , the bound would carry no content. If the deviation were evaluated under the undeviated measure instead of , the game would be a different one. (F.4) is genuine continuity, not the sequential continuity of (E).
A complete development needs:
The Girsanov and BSDE comparison results are reusable well beyond this mission and are welcome as separate contributions, as are proofs of Lemma 5.6 and of the bound.
A learning algorithm picks a hypothesis from a dataset ; its generalization error measures how far the empirical risk the algorithm sees is from the population risk it is judged by. Classical bounds control this error through the complexity of the hypothesis space (VC dimension, Rademacher complexity) or through the algorithm's stability. An information-theoretic approach instead controls it through how much the output reveals about the data. Russo and Zou (arXiv:1511.05219) introduced this view for adaptive data analysis, and Xu and Raginsky (arXiv:1705.07809) turned it into a general framework for learning algorithms; the framework underlies a large later literature on mutual-information and conditional-mutual-information generalization bounds.
Expected-value bounds of the form say nothing about a single run of the algorithm. A learner usually needs the error to be small with high probability. This mission formalizes Xu and Raginsky's high-probability result, Theorem 3, which gives a sample size sufficient for with probability at least under an information budget.
Timeline. 2016: Russo and Zou bound the expected bias of adaptively selected statistics by mutual information, for finite hypothesis classes. 2016: Bassily, Nissim, Smith, Steinke, Stemmer and Ullman (arXiv:1511.02513) introduce the "monitor technique" to convert expected bounds into high-probability bounds for differentially private and stable algorithms. 2017: Xu and Raginsky adapt the monitor technique to mutual information, obtaining Theorem 3 and its byproduct Theorem 4.
There is an instance space with an unknown probability measure , a hypothesis space , and a nonnegative loss . A learning algorithm is a Markov kernel : it receives a dataset of i.i.d. draws from and outputs a random . The joint law of data and output is .
The population risk and empirical risk of are
The empirical-risk vector is . For random variables with joint law , the mutual information is , the Kullback–Leibler divergence from the joint law to the product of the marginals. The algorithm's information budget is .
A real random variable is -subgaussian if for all . The standing assumption is that , , is -subgaussian for every ; a loss with values in qualifies with .
If , then for any and , every sample size
the probability being under .
The result. Theorem 3 shows that a sample complexity polynomial in and logarithmic in , the same order as for a data-independent hypothesis (where Chernoff–Hoeffding gives ), still suffices for a data-dependent one, provided the information budget is small relative to . It requires only subgaussian losses, whereas the earlier high-probability bounds of differential privacy apply to bounded losses or bounded-difference functions. Since , any algorithm with small input-output mutual information (the Gibbs algorithm, noisy empirical risk minimization, adaptive compositions of such) inherits the guarantee. Theorem 4 improves Russo and Zou's bound on the expected absolute error.
Formalizing it. The result is proved in the paper; to the best of current knowledge no machine-checked version exists. The mission produces a Lean statement of the theorem with the correct domain of validity (see the scope section), and its proof will require a reusable layer of measure-theoretic information theory: mutual information of joint laws, its additivity over independent pairs, the data-processing inequality, a bound by the logarithm of the number of values of a discrete variable, and the Donsker–Varadhan route from mutual information to expectations of subgaussian functions.
The obvious argument fails at the step from an expectation to a probability. Markov's inequality applied to Theorem 4 gives a sample size of order , quadratic in . A union-bound or Chernoff argument per hypothesis does not apply, because depends on and the deviation at the selected hypothesis is not a sum of independent terms. The paper's route runs independent copies and selects the worst one; the delicate part is bounding the information the selection itself adds, which needs the chain rule and data processing for mutual information on general (non-discrete) spaces, and an expectation bound that holds uniformly over every selection rule.
Lean conventions:
Fin n → Z with law Measure.pi, taken from the published LearnStability.Characterization.Setting (sampleLaw, risk, empRisk); the algorithm is a Markov kernel; the joint law is sampleLaw μ n ⊗ₘ κ.HasSubgaussianMGF of the centred loss with variance proxy .I ≤ ENNReal.ofReal ε. Expectations of nonnegative quantities (, ) are lower Lebesgue integrals; Lemma B.2's signed expectation is a Bochner integral whose integrand is integrable under the hypotheses.Fin m; the sign is a Bool read through sgn.Two printed slips are corrected in the Lean and disclosed in the item notes: the proof of Lemma B.2 claims is -subgaussian under the product of marginals (false; the centred version is), and (B.6) bounds the negative of the quantity in (B.4) ((B.7) is still correct).
The hypothesis is , not the stronger , and the goal mentions neither the parallel copies nor the monitor; a formalization that strengthened the hypothesis, dropped the measurability of the loss (so that the law of collapses to the zero measure and every mutual information is ), or allowed would be a weaker, vacuous or false statement.
Welcome contributions: chain rule and data processing for klDiv-based mutual information, additivity over independent products, the bound for finitely-valued outputs, and the Donsker–Varadhan decoupling lemma; these are reusable across the series and beyond.
A mean field game describes the Nash equilibria of symmetric players whose states interact only through their empirical distribution, in the limit . The law of large numbers for the equilibria — convergence of the empirical measure of the -player equilibrium to the mean field equilibrium — was proved in the diffusion setting by Cardaliaguet, Delarue, Lasry and Lions through the master equation (arXiv:1509.02505), and refined by Delarue, Lacker and Ramanan into fluctuation estimates and a central limit theorem in a companion paper (Electron. J. Probab. 2019). The next question is the size of rare deviations: the probability that the -player equilibrium empirical measure flow stays near a flow different from the mean field limit decays exponentially in , and the exponent is a rate function. Delarue, Lacker and Ramanan (arXiv:1804.08550) prove such a large deviation principle (LDP), including the case of a common noise affecting all players, for which no LDP was previously known even for McKean–Vlasov particle systems.
Timeline. Dawson and Gärtner (1987) proved the LDP for the empirical measure flows of weakly interacting diffusions without common noise, with time-independent coefficients and deterministic initial states, using the action functional adopted here. Budhiraja, Dupuis and Fischer (Ann. Probab. 2012) gave a weak-convergence proof for the empirical measure of paths. For mean field games, master-equation methods gave limit theorems, including LDPs, for finite state spaces without common noise (Cecchin–Fischer, arXiv:1704.00984; Cecchin–Pelino, arXiv:1707.01819; Bayraktar–Cohen, arXiv:1707.02648), and Lacker and Ramanan proved an LDP for static games (arXiv:1702.02113). The present paper (arXiv v1, 2018; Ann. Probab. 2020) treats diffusion-based games, with common noise.
On a filtered probability space live a -dimensional Brownian motion (the common noise), independent -dimensional Brownian motions , and i.i.d. initial states with law . The whole initial-state family is independent of the joint noise family, as specified for (6.1). Player of controls
with running cost and terminal cost . With the Hamiltonian , its minimizer and , a classical solution of the Nash system (2.6) gives the equilibrium states
The master equation (2.8) is a PDE for on involving derivatives in the measure argument. Assumption A asks for Lipschitz (with exponent for the Wasserstein metric), non-degenerate , moments of , classical solutions of the Nash systems, and a classical solution of the master equation with bounded derivatives; B or B′ controls .
The state space is : flows of probability measures with finite first moment, continuous for the 1-Wasserstein distance , with the uniform metric . The rate function uses the drift and the Dawson–Gärtner action functional
with over test functions, and off absolutely continuous paths. With common noise, the drift is shifted along the mean path: is for the drift , , and
where is the orthogonal projection onto the image of . is relative entropy.
If , A and B or B′ hold, and for every , then for open , compact and closed ,
Exponential equivalence of the Nash flows and the McKean–Vlasov particle flows (Corollary 6.1); a weak LDP for the noises and initial states (Proposition 6.15); uniform continuity of the McKean–Vlasov solution map (Lemma 6.16); the shifted action (Lemma 6.4); identification of the contracted entropy (Lemma 6.17); the weak LDP for general weakly interacting systems with common noise (Theorem 6.8) and its transfer to the Nash flows (Theorem 6.13); compactness after centering (Proposition 6.11); removal of the -relaxation on compacts, and the full LDP without common noise (Proposition 6.10); explicit forms of (Proposition 6.5, Theorem 6.6). A companion item states Theorem 3.9: without common noise, a full LDP with the good rate function .
The result quantifies how unlikely atypical equilibrium behaviour is in large games: rare macroscopic deviations of the equilibrium empirical measure flow cost , and the rate function makes explicit that the common noise moves the mean of the population for free in the directions of the image of . When the rate function has non-compact level sets, which is why the principle is weak and why the closed-set bound carries the -relaxation.
The proof transfers the LDP from the McKean–Vlasov particle system to the Nash system through the master equation, a method that applies beyond this model. Nothing in this paper is formalized: there is no large deviation principle, no Wasserstein space of measure flows, no derivative on Wasserstein space and no mean field game on the platform. A formal development produces reusable definitions (weak and full LDPs, the Dawson–Gärtner action functional, ) and checked proofs of the contraction and exponential-equivalence steps. The exponential estimate behind Corollary 6.1 (Theorem 4.3) is the companion mission's milestone and rests on estimates quoted from the companion central-limit-theorem paper.
The obvious route — exponential equivalence plus the Dawson–Gärtner LDP for the particle system — fails twice. The particle drift is time-dependent and the initial states are random, which the classical results do not cover; and with common noise there is no LDP to transfer. The proof instead freezes the noise: it proves a weak LDP for the pair (empirical measure of initial states and idiosyncratic paths, common noise path), which needs Sanov's theorem in the topology and the Brownian support theorem, and contracts it through the McKean–Vlasov solution map. The contraction principle requires the rate function to be good, and it is not when ; uniform continuity of the solution map and the -enlargements replace goodness.
Time is with ; paths are continuous maps on , and solutions of the SDEs are path-valued, adapted, and satisfy the integral equations almost surely. Players are indexed from . Probability measures with finite -th moment are guarded by an explicit predicate, and is the published WassersteinDRO.Duality.wassersteinDistance, kept in . Derivatives in , , are genuine derivatives; derivatives in the measure are normalized flat-derivative witnesses. Relative entropy is Mathlib's klDiv. Logarithms of probabilities are in ; open, closed and compact sets are those of the uniform metric, and is a supremum over . The action functional is an infimum over all distributional time derivatives, with test functions and distributions from Mathlib. The common-noise paths are -dimensional.
Standing assumptions are carried explicitly: the filtered space and noises of §2.3, joint independence of initial states and noises from §6.1, Assumption A (with the Borel measurability of ), B or B′, where the paper assumes it, and, for §6, Condition 6.3 and non-degenerate . Two disclosed additions: Theorems 3.9, 3.10 and 6.13 assume bounded (Condition 6.3(2) requires it; Assumption A does not imply it), and Theorem 6.13 assumes . The solutions of the Nash systems, the master equation and the SDEs are hypotheses; existence is not posed.
A rate function identically or , or bounds over a restricted family of sets, would trivialize the statements: the seminorm is a supremum over all test functions, exactly off absolutely continuous flows, and the bounds quantify over every open, compact or closed set. A complete development needs Sanov's theorem in , the Brownian support theorem, the contraction principle, Dawson–Gärtner's analysis of distribution-valued paths, and stochastic calculus for the particle systems; each of these is reusable, and contributions to any of them are welcome.
The discrete optimal transport problem of Kantorovich asks for the cheapest way to move a probability histogram onto a histogram when moving a unit of mass from to costs . Its optimal couplings are vertices of a polytope and are typically sparse: they rely on a few routes. Two communities have reasons to blur them. In transportation planning, observed traffic is more diffuse than linear-programming predictions, which led to the "gravity" model of Wilson (1969) and Erlander (1980), as recounted in Peyré and Cuturi, §4.1. In machine learning and statistics, adding an entropy term to the objective turns the linear program into a strictly convex problem that Sinkhorn's matrix-scaling algorithm solves at scale (Cuturi, 2013).
Every use of the entropic problem raises the same question: what does the regularized solution approximate? Chapter 4 of Peyré and Cuturi's Computational Optimal Transport answers it in Proposition 4.1 for the two extreme regimes of the regularization strength .
Timeline. Cominetti and San Martín (1994) studied the convergence of entropic penalties for linear programs, including first-order expansions near and . Peyré and Cuturi (2019) record the transport case as Proposition 4.1, with a short compactness proof.
Fix sizes . A histogram is a vector of the probability simplex . Given , , the set of couplings is
nonnegative matrices with row sums and column sums . For a cost matrix write . The Kantorovich problem is .
The discrete entropy of a coupling is
with . For the entropic problem is
whose unique minimizer is . The maximum-entropy optimal coupling is the optimal coupling of the Kantorovich problem with the largest entropy. The Gibbs kernel is and the Kullback–Leibler divergence between matrices is .
In Lean these are couplings, frob and IsOptimalCoupling in CompOT.Assignment, and entropy, entObjective, IsEntropicOptimal, IsMaxEntropyOptimal, gibbs and klMat in CompOT.EntropicLimit.
For , and any cost matrix ,
The result. Proposition 4.1 justifies the entropic regularization as an approximation scheme: for small the regularized plan converges to an exact optimal plan, and specifically to a canonical one, the most diffuse among all optimal couplings, so the limit does not depend on any tie-breaking. The value converges to the transport cost, which is what makes Sinkhorn-based estimates of transport distances meaningful. For large the plan becomes the independent coupling , which explains the interpolation between optimal transport and maximum mean discrepancy studied later in the book. The KL projection identity (4.7) is the starting point of Sinkhorn's algorithm, so this mission also supplies the bridge to the next missions of the series.
Formalizing it. The proposition is a known result with a complete proof in the source; the work is formalizing it in Lean 4 with Mathlib. To our knowledge none of these statements, nor the discrete entropic transport problem itself, has a machine-checked proof in Mathlib or on the platform. A formal proof also pins down the convention for zero entries, on which the statement silently depends.
The obvious argument passes to the limit in the optimality of , but this only shows that limit points are optimal for the Kantorovich problem; it does not identify which optimal coupling is the limit when the optimal set is a face of the polytope rather than a vertex. Identifying it requires a second-order argument at the level of the entropy, and the convergence of the whole family (not just a subsequence) rests on the uniqueness of the maximum-entropy optimal coupling, which in turn needs strict concavity of on a set that may contain matrices with zero entries, where the logarithm is singular. Existence and uniqueness of face the same boundary issue: the minimizer may a priori sit on the boundary of the polytope.
Indices are 0-based (Fin n, Fin m); histograms are functions Fin n → ℝ in Mathlib's stdSimplex; matrices are Matrix (Fin n) (Fin m) ℝ with the product topology, so convergence is entrywise. Entropy uses (Real.negMulLog); the book's remark that at a zero entry is not used, since it would contradict the continuity of invoked in the book's proof and make (4.3) degenerate. Optimality is expressed by predicates (a minimizer over ), never by a real infimum, so no junk value of an empty infimum appears. The limit is taken from the right. The values and appear as the objectives at and .
In the goal, and are given by hypotheses (any family solving (4.2) for every , any solution of (4.3)). This is not a vacuous formalization: milestones 1 and 2 assert that such objects exist and are unique, so the hypotheses are satisfiable and determine them. Standing assumptions are exactly those of the book: , , ; no positivity of , or is assumed.
A complete development needs: compactness of the transport polytope, continuity and strict concavity of on , and the Gibbs inequality on finite sums. These are reusable for the Sinkhorn and entropic-duality missions of this series. Proofs of any milestone are welcome independently.
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.
Second order dynamical systems with vanishing damping are continuous-time models of accelerated first-order methods. The system is the continuous limit of Nesterov's accelerated gradient method (Su, Boyd, Candès 2016), and its trajectories converge weakly to a minimizer of a convex when (Attouch, Chbani, Peypouquet, Redont 2018). Two modifications of this system have been studied separately. A Hessian-driven damping term damps oscillations and keeps the fast rates (Attouch, Peypouquet, Redont 2016). A Tikhonov regularization term with selects one minimizer, the one of minimum norm, and can turn weak convergence into strong convergence (Attouch, Chbani, Riahi 2018).
Boţ, Csetnek and László (arXiv:1911.12845v2, Math. Program. 2021) study the system with both terms. Their results split into two regimes according to how fast decays. This mission covers the slow-decay regime of §4.1, where and the trajectory approaches the minimum-norm minimizer in a weighted average sense.
Timeline. 2016: Su, Boyd and Candès derive the continuous model of Nesterov's method. 2016: Attouch, Peypouquet and Redont add Hessian-driven damping (, ) and prove fast rates and weak convergence. 2018: Attouch, Chbani and Riahi add Tikhonov regularization without Hessian damping and prove, among other results, strong ergodic convergence to the minimum-norm minimizer when . 2020: Boţ, Csetnek and László combine both terms and extend that ergodic result (their Theorem 4.2).
Let be a real Hilbert space, , , , and . The data satisfy the paper's General assumption:
A global -solution of system (5) is a twice continuously differentiable with
The set is nonempty, closed and convex, so it has a unique element of minimum norm, the minimum-norm minimizer . For the Tikhonov approximation curve is
the unique minimizer of a strongly convex function. Finally, measures the distance of the trajectory to , with derivative .
If and , then every global -solution satisfies
No rate and no constant is asserted, so the goal does not depend on any particular choice of .
The result shows that slow Tikhonov regularization still selects the minimum-norm minimizer when Hessian damping is added: the weighted time average of tends to zero and the trajectory comes arbitrarily close to infinitely often. The hypothesis is only , well below the threshold that the paper needs for its fast rates, and no growth condition on beyond the divergence of is imposed. It complements Theorem 4.4 of the same paper (a separate mission), which reaches full strong convergence under fast decay, , plus further conditions.
On the formal side, the theorem and its milestones are proved in the paper and in the cited literature, but none of them has a machine-checked proof. The work splits into an energy estimate for a nonautonomous second order ODE in a Hilbert space (Lemma 4.1), two facts about the Tikhonov curve that underlie the whole theory of Tikhonov regularization of convex problems (milestones 2 and 3), an integrated differential inequality (46), and a l'Hospital-type averaging step. The Tikhonov-curve facts are reusable for any formal treatment of viscosity selection and minimum-norm solutions.
The obvious attempt, a Lyapunov function that decreases along the trajectory and controls , fails because is not a stationary point of the perturbed system: in general. The distance to therefore need not decrease, and pointwise convergence is not available under the slow-decay hypothesis alone. The comparison point has to move along the Tikhonov curve , whose convergence to comes without a rate. The available bound controls only a weighted integral of corrected by , so the passage from (46) to the goal needs both and the divergence of the weight. In the formal setting the Tikhonov-curve limit is itself a nontrivial weak-compactness argument in a Hilbert space, which the paper does not spell out.
InnerProductSpace ℝ H, CompleteSpace H). is gradient g, and is the Fréchet derivative of gradient g at applied to . "Twice Fréchet differentiable" means and are differentiable; Lipschitz continuity on bounded sets is stated on every closed ball around the origin.Filter.liminf, whose value on an unbounded function is a default. is boundedness from above of the image of , and membership is integrability on .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.
Large optimization models often split their variables into blocks that can be handled separately. A method can then solve one smaller approximation problem per iteration instead of the full problem. The block successive convex approximation (BSCA) method of Razaviyayn, Hong and Luo allows the block approximation to guide the search without requiring it to be a global upper bound on the original objective. This matters when an upper bound is awkward to construct but a locally accurate convex model is available. The question is what such a run can approach: a small objective value by itself does not certify first-order optimality.
The paper develops this result after its successive upper-bound minimization methods. Theorem 4 of the pinned preprint gives the limit-point guarantee for BSCA with an Armijo step search. The mission records that result and the numbered relations (31)–(34) and (39) that organize the argument, using the 2012 preprint as the sole source for statement indices and page numbers.
The decision vector is a block vector , with block in a nonempty, closed, convex set . The feasible set is . A continuously differentiable objective assigns each feasible vector a real value. A point is stationary when for every direction whose full step lies in . For a smooth objective, is the derivative of in direction .
For block , the function approximates the objective as the trial block varies around a current point . Its directional derivative at agrees with the objective derivative in the corresponding one-block direction, as in equation (30). Each is strictly convex on , and varies continuously with its trial block and feasible base point. Strict convexity is a condition in the trial block for each fixed ; it does not say that is jointly convex in both arguments.
At iteration , a cyclic schedule chooses one block . A minimizer of over replaces that block in ; all other blocks of equal those of . The search direction is . With and an initial trial length , the Armijo rule chooses the largest member of satisfying
then sets . The selected minimizer can be any one of the block minimizers; the definition does not prescribe a hidden tie-breaking rule.
The first targets identify descent and line-search existence. Equation (31) says the chosen block direction has a nonpositive derivative. Equation (32) says a strict descent direction admits a trial index. The later milestones state the vanishing scaled derivative (33), a subsequence with vanishing search directions (34), and limiting block optimality following (39).
The goal is Theorem 4: for every limit point of the sequence generated by cyclic BSCA,
This is a limit-point assertion. It does not assert convergence of the entire iterate sequence, a convergence rate, or global optimality of a stationary point.
Theorem 4 identifies what an accumulation point of BSCA must satisfy even though its block models need only local first-order agreement rather than global upper bounds. In a nonconvex problem, stationarity is a meaningful first-order conclusion but need not be a global minimum. The exact role of the step search is important: accepting some Armijo step gives decrease, whereas the theorem's limit-point claim uses the largest acceptable member of the geometric trial sequence.
This mission asks solvers to supply machine-checked proofs for a known paper theorem and its stated supporting relations. The draft statements compile as open theorems; they are not proofs. The reusable output includes a block run predicate, an explicit first-order agreement predicate, and a bridge between feasible-direction stationarity and an extended-real objective on the full block space. These objects also make subsequent variants of cyclic block methods easier to state precisely.
A simple decrease argument shows that objective values do not increase, but the accepted step sizes may approach zero. Therefore decrease alone does not imply or that a limit point minimizes every block model. The paper's key limit statement singles out a convergent subsequence on which a fixed block is updated and finds a further subsequence with vanishing directions. Passing block optimality to the limit then requires continuity of the approximation and feasible limit points. The cyclic schedule is needed to cover all blocks, while first-order agreement turns block optimality into stationarity for the original smooth objective.
Lean uses the published TsengBCD.Stationary.X for the finite product of Euclidean block spaces, its extended-real lower directional derivative, and its stationary-point predicate. The product has the sup norm rather than the paper's Euclidean product norm; in finite dimension the notions of convergence used here agree. Blocks and iterations are indexed from zero. The paper's cyclic choice is reindexed so the step from to updates block . The existence of the schedule already rules out zero blocks.
The objective is a real function on the full block space, with ContDiff ℝ 1 expressing the paper's continuous differentiability. This makes the Fréchet derivative used in the Armijo test equal to the paper's lower directional derivative at the points in question. For stationarity, the objective is extended by outside , so infeasible directions cannot silently become admissible. The approximation derivative remains extended-real because the paper assumes only convexity for that function. ContinuousOn is taken on the product of a feasible trial block and a feasible base point.
Two points are explicit in the formalization. First, ensures that a convex combination of and stays in ; the paper prints only positivity. Whether Theorem 4 holds without this restriction under a different global interpretation of and remains a separate question. Second, Figure 4 mixes and in the approximation, direction, and update lines. The run follows the adjacent prose and proof, all of which construct the direction at the current iterate. For (33), the existence of a limit point makes explicit the proof's standing situation and gives the decreasing objective a finite limit. An arbitrary unrelated sequence, an Armijo step that is not the largest accepted trial, or an objective extension that gives a default zero derivative off is outside this scope.
The remaining proof work includes feasibility of every iterate, first-order agreement along the selected block, the Armijo existence statement, the subsequence claim, passage of block minimization to the limit, and the final stationary-point equivalence. The finite-dimensional convex analysis and topology involved are reusable beyond this one algorithm.
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.
Scattered subspaces are a central object of finite geometry. An -subspace of an -dimensional vector space over defines an -linear set of the projective space , and when is scattered this linear set has the largest possible number of points for its rank. Maximum scattered subspaces give rise to maximum rank distance (MRD) codes, to translation caps, and to two-intersection sets and the associated two-weight codes and strongly regular graphs (Polverino 2010; Sheekey–Van de Voorde 2020).
Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2, Combinatorica 41, 2021) generalised the notion to -scattered subspaces, which meet every -dimensional -subspace in dimension at most , and proved that such a subspace has dimension at most unless it defines a subgeometry. This mission concerns the extremal case: subspaces attaining , and the way they meet hyperplanes.
Timeline.
Let be finite fields, , and let be an -dimensional vector space over , viewed also as an -dimensional vector space over . A hyperplane of is an -dimensional -subspace.
Fix an integer with . An -subspace of is -scattered if and every -dimensional -subspace satisfies . It is maximum -scattered if no -scattered subspace of has larger -dimension.
Put and suppose . For an -subspace of dimension , let be the number of hyperplanes with . The proof works with the Gaussian binomial coefficients , the -Pochhammer symbols , the elementary symmetric values of , and the sums
If is a maximum -scattered -subspace of of dimension , then for every hyperplane of
The result. Theorem 2.7 says that a maximum -scattered subspace of dimension has only possible intersection dimensions with hyperplanes. Its linear set therefore meets hyperplanes in few sizes, which links these subspaces to sets of few intersection numbers and to codes with few weights. Inside the paper, the upper bound is the input to §3: it shows that the Delsarte dual of a maximum -scattered subspace of dimension is maximum -scattered (Theorem 3.3). That theorem in turn gives maximum -scattered subspaces when does not divide .
Formalizing it. The theorem is proved in the paper, but no machine-checked version exists. Beyond the geometry, the mission produces a library of finite -series facts: Gaussian binomials as rational functions of , the -binomial theorem in both forms, Carlitz's inversion formula, and the elementary symmetric evaluation . Some of these are proved on the platform in a different Mathlib environment, but they are not available in this one. Counting statements about subspaces over finite fields (hyperplanes through a subspace, ordered independent tuples) are also needed and are reusable.
The lower bound is a dimension count. The upper bound is not: the obvious approach bounds from the scattered property alone, but the -scattered condition controls intersections with -dimensional subspaces, and hyperplanes have dimension , which is far larger. No pointwise argument is known; the paper determines the distribution only through its first moments, given by a double count, and then shows that a specific nonnegative combination of the vanishes. The moment identities hold only for (Lemma 5.7 needs each independent vectors of to stay independent over ), and closing the argument requires exact evaluation of a triple -series with signed Gaussian binomials and quadratic exponents.
F, a finite field K with [Algebra F K], and a finite-dimensional K-module with a compatible F-module structure (IsScalarTower F K V). We take finrank K V, finrank F K and Fintype.card F.IsHScattered.Proofs of any milestone, of standard counting facts for subspaces of finite vector spaces, and of the -series lemmas are welcome.
A constraint satisfaction problem (CSP) asks whether variables ranging over a finite domain can be assigned values so that every constraint from a fixed finite list of relations is satisfied. A central organizing principle of the algebraic theory of CSPs is that the complexity of is governed by its polymorphisms, the functions that preserve every relation of when applied coordinate-wise. For this principle to be usable, one needs to know which sets of functions arise as polymorphism sets. For ordinary relations this goes back to the Galois theory of clones and relations. Pippenger (Galois theory for minors of finite functions, Discrete Mathematics, 2002) characterized the families of functions that are the polymorphism sets of pairs of relations, allowing infinitely many pairs.
Promise constraint satisfaction problems (PCSPs) relax CSPs: every constraint comes as a pair , and the task is to distinguish instances satisfiable with the strong relations from those unsatisfiable even with the weak relations . Approximate graph colouring and -SAT are PCSPs. Brakensiek and Guruswami (arXiv:1704.01937v2, SIAM J. Comput. 2021) develop an algebraic theory of PCSPs based on polymorphisms. In §6.2 they prove a finite version of Pippenger's characterization: the families of the form for a finite family of promise relations are exactly the families satisfying three explicit conditions. This mission formalizes that theorem and its CSP analogue (§6.3).
Fix a finite set . A family of functions over consists, for every arity , of a set of functions .
A promise relation of arity is a pair of subsets of with . A finite family of promise relations is indexed by a finite set of relation symbols, each with its own arity . A function is a polymorphism of if for every and all , applying coordinate by coordinate gives a tuple in :
is the family of all polymorphisms of .
For and a map , the projection (or minor) is
A family is projection-closed if whenever has arity and . It is finitizable if there is a finitized arity such that for every arity and every ,
Finally is the identity, a function of arity .
The finite family is existential together with its signature and arities; nothing about its shape is fixed in the statement.
A CSP is a finite family with for every pair. With a clone (for of arity and of arity , the function of arity is in ):
Theorem 6.5 identifies the polymorphism families of finite promise templates intrinsically, without reference to relations. Together with the Galois correspondence of §6.1 (if then is definable from , so reduces to ), it justifies studying PCSPs entirely through families of functions closed under minors, the viewpoint later systematized by the theory of minions (Barto, Bulín, Krokhin, Opršal, arXiv:1811.00970). Lemma 6.8 recovers, in the same language, the description of polymorphism clones of finite CSP templates as the finitely related clones.
The results are proved in the paper; to our knowledge none of them has a machine-checked proof. The mission produces a Lean formalization of both directions, built on the published definitions of relational structures and polymorphisms already used by other PCSP missions on the platform, and reusable definitions of projections (minors), projection-closed and finitizable families, and clones.
The arguments are elementary, and the difficulty lies in uniformity and finiteness. For Claim 6.6, a single arity must detect every failure of the polymorphism condition for functions of every arity , so has to be bounded independently of ; an argument that handles each arity separately does not give finitizability. For Lemma 6.7, a finite family of promise relations has to be produced from alone. The general Galois connection between functions and relations produces infinitely many relations (one for each arity and each witness of non-membership), and the content of the lemma is that the three conditions allow a finite family instead. In both directions the encoding matters: functions of arity must be compared with tuples of a relation, and coordinates, projections and the identity must be matched exactly, with no degenerate arity left over.
A family of functions is FunFamily D := (L : ℕ) → Set ((Fin L → D) → D), with a finite type with decidable equality. Coordinates are 0-based (Fin L), and is fun y => f (y ∘ π) with π : Fin L → Fin R. A finite family of promise relations is a finite type τ of symbols with arities ar : τ → ℕ and two structures 𝔸 𝔹 : RelStruct τ ar D with 𝔸.rel R ⊆ 𝔹.rel R; polymorphisms are the published IsPolymorphism (definition PCSPBLPAff_Symmetric_Setting), and a CSP uses one structure on both sides.
All function arities are positive. The paper's "" is read as positive integers: "" is compared at every arity , projection-closure and finitizability quantify over , and the finitized arity is at least . Including arity would make the necessity direction false as stated (with every empty the paper's finitized arity is ).
The clone condition of Lemma 6.8 is the paper's displayed one (p. 30): act on disjoint blocks of inputs, and the composed function has arity .
A trivializing formalization is ruled out by the statement's shape: the finite family, its signature and its arities are all existentially quantified (fixing a single relation would turn the necessity direction into a special case), is part of every family (without it fails), and finitizability is an equivalence for every function, members and non-members alike.
The development needs only finite types and functions; no complexity theory is involved. Proofs of the milestones, and reusable lemmas about projections (composition of projections, projections along injective maps), 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.A manufacturer that sells through a retailer can also open a direct sales channel. The direct channel lets the manufacturer reach consumers, but it competes with the retailer, whose orders generate wholesale revenue. The manufacturer can further choose whether the two channels carry products of the same quality. These decisions interact because quality changes both consumer demand and the retailer's response. Ha, Long and Nasiry study this interaction in a sequential supply-chain game. Their fixed-quality-cost extension asks what happens when a high-quality design can be converted into a lower-quality variant without paying a separate production cost for each unit (Ha, Long and Nasiry, §6.2).
The main result is specific to this cost regime. With a cost per unit that rises with quality, different products can be attractive across the channels; with the paper's one-time cost of creating quality, Proposition 6(i) asserts equal qualities when the direct channel makes positive sales. This mission targets that fixed-cost proposition in the authors' manuscript, including its game and the reduced-profit claims used in the e-Companion (Ha, Long and Nasiry, pp. 20, 36–37).
The market has mass one of consumers, indexed by a taste for quality uniformly distributed on . A consumer buying a product of quality at price receives surplus . The manufacturer offers quality through her own direct channel and quality through the retailer. The ratio therefore records which channel has higher quality. The manufacturer pays a fixed cost of quality , with , and a direct selling cost per unit. The retailer has zero selling cost. Unlike a unit production cost, this fixed cost is paid once and does not scale with either channel's quantity (Ha, Long and Nasiry, pp. 7–8, 20).
The manufacturer first chooses wholesale price and qualities . After observing them, the retailer chooses its order . The manufacturer observes that order and chooses her direct quantity . When , market-clearing prices are
When , the retailer's product has higher quality, and the corresponding prices are
The manufacturer receives wholesale revenue plus direct-channel revenue, less the direct selling cost and fixed quality cost. The retailer receives its retail margin times . Encroachment means on the equilibrium path, rather than the mere existence of a direct channel (Ha, Long and Nasiry, pp. 8, 11, 15, 36).
For a subgame-perfect equilibrium of the fixed-cost game, the goal is Proposition 6(i):
The formal statement assumes . At , the high-direct-quality reduced profit is independent of , so the printed claim fails to force ; this is a substantive qualification of the manuscript's standing convention. The goal concerns the complete game, with contingent actions at every decision node, rather than only the closed-form optimization problem (Ha, Long and Nasiry, pp. 20, 36).
The milestone list follows the authors' two quality regimes. The e-Companion gives best responses, wholesale prices, and reduced profits in each regime. In the high-direct-quality regime, Claim 3 concludes that an optimum with positive direct sales has . In the low-direct-quality regime, Lemma 2 concludes that an optimum either has or lies at no encroachment. The latter alternative is outside the strict encroachment-feasible set used by the Lean milestone. Footnote 2 supplies a one-variable sign inequality used in the analysis of that regime (Ha, Long and Nasiry, pp. 36–37).
Proposition 6(i) determines the manufacturer's quality choice conditional on active direct sales: both channels carry quality . It narrows the set of equilibrium outcomes that the fixed-cost model can support and distinguishes the role of a one-time design cost from the paper's earlier variable-cost model. The paper states a separate profit comparison in Proposition 6(ii); this mission does not formalize it because the e-Companion omits its proof and the fixed-cost no-encroachment benchmark for that comparison is not stated (Ha, Long and Nasiry, pp. 20, 37).
A complete Lean development would connect the reduced-profit calculations on page 36 to subgame-perfect play in the three-stage game, and establish the optimization claims over their stated feasible sets. The definitions of two-quality inverse demand, contingent strategies, and nodewise optimality are reusable for related channel games. The goal and milestones here are draft statements, without machine-checked proofs of their economic conclusions.
The manufacturer chooses quality and wholesale price before the retailer's order, yet the direct quantity is chosen only after that order. Consequently, the retailer's payoff depends on the manufacturer's continuation response, and the first-stage choice must account for both later decisions. The reduced profit also changes at , where the higher-quality channel switches. A calculation for one regime alone does not establish the full-game claim. The strict region matters: its boundary represents no encroachment and supports a different alternative in Lemma 2 (Ha, Long and Nasiry, p. 36).
Lean uses real wholesale prices and qualities, positive and , and nonnegative quantities. Wholesale price has no sign restriction in the manuscript. The market has unit size and the retailer's selling cost is zero. The two inverse-demand expressions are applied to all nonnegative quantities, following the paper's algebraic game model. A profile contains a stage-one action, a retailer order rule for every observed , and a direct-quantity rule for every observed . Subgame perfection requires feasible best replies at every such history, including histories off the equilibrium path. Fixed cost is , paid once, while is a per-unit selling cost.
The reduced profits and are used only on their respective open encroachment-feasible domains, where the displayed denominators are positive. Claim 3 is stated for a joint maximizer in ; keeping fixed while moving to can leave that feasible set. Lemma 2 excludes the no-encroachment boundary in its Lean statement. Neither reduced profit replaces the full-game payoff in the goal. Contributions that connect the subgame formulas to arbitrary equilibrium profiles, prove the sign inequality, or establish the two optimization results are within scope (Ha, Long and Nasiry, pp. 36–37).
Discrete optimal transport between two histograms is a linear program. Its feasible set, the transportation polytope, has been studied since Hitchcock (1941) and Kantorovich, and the structure of its vertices underlies the classical algorithms for the problem: the north-west corner rule produces a vertex, and the network simplex moves from vertex to vertex. A linear program with a nonempty bounded feasible set attains its minimum at a vertex, so knowing what vertices look like tells us what optimal transport plans can be assumed to look like.
This mission is the fourth of a series formalizing G. Peyré and M. Cuturi, Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019). It covers §3.4.1 of the book, Tree Structure of the Support of All Vertices of U(a, b) (pp. 405–407), whose single numbered result, Proposition 3.4, states that the support of a vertex is a forest. The book credits the result to Brualdi, Combinatorial Matrix Classes (2006, Theorem 8.1.2).
Fix integers and histograms , . The transportation polytope is
the set of nonnegative matrices whose row sums are and whose column sums are . Histograms are nonnegative and sum to one; is the set of couplings between them. The cost of a plan for a cost matrix is .
A point of a set is an extremal point (vertex) of if, whenever and , necessarily .
Take source nodes and target nodes . The complete bipartite graph between them has the edges . For a matrix , the support is the set of edges with , and the support graph is . A transport plan is a flow on the complete bipartite graph, with leaving node and entering node ; records the edges the flow actually uses.
If is an extremal point of , then
For , and any cost , some minimizer of over is an extremal point of .
Proposition 3.4 is the sparsity statement of discrete optimal transport: a vertex of moves mass along at most source–target pairs, out of possible. With the companion, some optimal plan is that sparse. This is what makes the network simplex method a combinatorial algorithm on spanning trees of the bipartite graph (§3.5 of the book), and it is the reason the north-west corner rule (§3.4.2) can produce a feasible vertex with a tree support. The same fact, specialized to and uniform histograms, is one step on the way from Kantorovich's relaxation back to Monge's assignment problem.
The result is classical and proved; it has not, to our knowledge, been formalized. Mathlib has the transportation polytope only implicitly (no dedicated definition), and it has the edge count of trees (SimpleGraph.IsTree.card_edgeFinset) but not the corresponding bound for forests. The mission produces a machine-checked link between the convex geometry of and the combinatorics of its support graph, reusable by later missions of the series on the network simplex and on the assignment problem.
The convex-geometric half is elementary; the work is in the passage between a cycle of a graph and a matrix. The cycle is an object of Mathlib's graph library (a closed walk with distinct vertices in a graph on ), while the perturbation is a matrix indexed by . An informal picture of a cycle as a list of edges hides what the matrix statement needs: each source and each target must be visited at most once, and Mathlib's cycles are walks whose distinctness conditions have to be carried to the matrix level.
The edge bound for forests is not packaged in Mathlib either: it counts the edges of a tree, a connected acyclic graph, while the support graph of a vertex is in general disconnected, and the empty graph must be handled.
All objects live in the namespace CompOT.Vertices. Indices are Fin n and Fin m (0-based; the book's ). Matrices are Matrix (Fin n) (Fin m) ℝ, and is the set of matrices with nonnegative entries, row sums and column sums . Extremality is the book's midpoint definition, relative to the set: the points in range over only. This rules out the trivializing reading in which range over all matrices (no point would then be extremal and the goal would be vacuous); conversely, the sanity file shows a non-extremal coupling, so extremality is not automatic either.
The support graph is a SimpleGraph (Fin n ⊕ Fin m) with Sum.inl i adjacent to Sum.inr j exactly when and no other adjacencies. The book calls the edges directed, but the cycles of its proof alternate between sources and targets, so "no cycles" is Mathlib's SimpleGraph.IsAcyclic of this undirected graph. The number of nonzero entries is the cardinality of .
The goal, feasibility milestone and companion carry , , the book's standing notation for histograms (p. 360). These hypotheses make the index sets nonempty, so natural-number subtraction in the bound agrees with the book's integer expression.
Useful infrastructure, reusable beyond this mission: the forest edge bound for finite simple graphs, and the correspondence between cycles of a bipartite graph and signed matrices with zero line sums. Contributions of either as standalone lemmas are welcome.
Let be an -dimensional vector space over the finite field . Viewed over the subfield , has dimension , and its one-dimensional -subspaces form the Desarguesian spread. An -subspace of is scattered if it meets every element of this spread in an -subspace of dimension at most one. Scattered subspaces define scattered -linear sets in . Through these linear sets they are connected to projective two-weight codes, strongly regular graphs and maximum rank distance (MRD) codes. In 2000 Blokhuis and Lavrauw proved that a scattered subspace has dimension at most , and a sequence of papers showed that this bound is attained whenever .
Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2; Combinatorica 41, 2021) replace the one-dimensional spread elements by all -dimensional -subspaces. This gives a hierarchy of conditions, the -scattered subspaces, that refines the scattered case. For and dimension these subspaces had already been identified with -linear MRD codes by Sheekey and Van de Voorde. This mission formalizes the paper's main theorem, the dimension bound for -scattered subspaces.
Timeline.
Let be finite fields, so , and let be a vector space over of dimension . Every -subspace of is also an -subspace. For an -subspace of , denotes its -span.
Definition 1.1. Let . An -subspace of is -scattered if and every -dimensional -subspace of satisfies . In Lean this is HScattered.Bound.IsHScattered F K h U, with F , K , and = Module.finrank K V.
An -subspace defines a subgeometry of if some -basis of is also an -basis of (HScattered.Construction.DefinesSubgeometry F K U, a definition shared with the other missions of this series). In coordinates, is then inside .
A rank distance code of , , is a set of -linear maps from an -dimensional to an -dimensional -space, with distance .
If is an -scattered -subspace of , then either , defines a subgeometry and is -scattered, or
The disjunction is inclusive. The statement holds for every in the range , including .
The result. Theorem 2.3 is the upper end of the theory of -scattered subspaces. It shows that the bound decreases with : a stronger intersection condition forces a smaller subspace. Every subspace reaching the bound is a maximum -scattered subspace. The rest of the paper builds on such subspaces. Its constructions show the bound is sharp when . Its intersection numbers with hyperplanes lie in . Its Delsarte-type duality sends maximum -scattered subspaces to maximum -scattered ones. Each of these statements presupposes the bound. For , the bound is the geometric counterpart of the Singleton bound for MRD codes.
Formalizing it. The theorem is proved in the paper; it has no machine-checked proof. A formalization would provide a Lean model of -scattered subspaces over a field tower and a rank-metric Singleton bound, and the bound itself as a reusable lemma for the companion missions on constructions, hyperplane intersections and duality. The case is attributed in the paper to Blokhuis–Lavrauw and is not reproved there, so a complete formal proof must also supply that case.
The obvious approach is to count. Every -dimensional -subspace meets in at most vectors. But these subspaces overlap heavily, and a double count of incidences between vectors of and -dimensional subspaces does not produce a bound of the form . The -scattered condition must be used on subspaces of every dimension at once, which is the content of Proposition 2.1. The argument for does not carry over directly either: the paper treats , with , and as separate cases. The case rests on a coding-theoretic input (Result 4.6), and the middle case needs auxiliary subspaces whose existence (Lemma 2.2) holds only when .
F, K with [Algebra F K]. is a finite-dimensional K-module with a compatible F-module structure ([IsScalarTower F K V]). The parameters are = Fintype.card F, = Module.finrank F K and = Module.finrank K V.Submodule F V and -subspaces are Submodule K V. The intersection is S.restrictScalars F ⊓ U.IsHScattered.Finset of linear maps. The minimum distance enters as a lower bound on all pairwise rank distances, with .Ruling out trivial readings. Without the range , every spanning subspace would be "-scattered" for , and of dimension would refute the goal. Without the spanning condition, would satisfy the bound vacuously. Both conditions are part of the definition, and the goal is the inclusive disjunction for every -scattered .
Cited inputs. Result 4.6 is Delsarte's theorem [13], numbered in this paper and posed here with sorry. The case of the goal is the Blokhuis–Lavrauw bound [4], which the paper cites without proof and says can be obtained by adapting its argument (Zullo's thesis [30]). It is not an item: a complete proof of the goal must cover it.
Infrastructure. A proof needs: dimension arithmetic for restriction of scalars in a tower; the rank–nullity theorem for -linear maps; the count of roots of a -polynomial , for Lemma 2.2; and a rank-metric Singleton bound. The Singleton bound and Lemma 2.2 are reusable beyond this mission. Contributions are welcome on any milestone, on the case, and on the reduction for .