Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
General Entanglement Breaking Channels establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let and be integers. Fix density matrices and positive semidefinite matrices , and define the complex-linear Holevo map on all matrices by
For every positive finite reference dimension and every density matrix on ,
Here the cone consists of finite sums with nonnegative real coefficients and includes zero. If, in addition, is a POVM, meaning , then is completely positive and trace-preserving, and every such joint output is a separable density matrix: it is a finite convex combination of product density matrices.
This is precisely the measure-and-prepare implication of Theorem 4 and its printed channel specialization. It applies to entangled inputs without purity, orthogonality, or independence restrictions on the prepared states.
Formalization Note The general part uses the frozen separable-positive-cone predicate because unrestricted positive effects need not preserve trace. The channel part uses normalized separability. The identity always acts on the reference factor.
Let and be integers. Fix density matrices and positive semidefinite matrices , and define the complex-linear Holevo map on all matrices by
For every positive finite reference dimension and every density matrix on ,
Here the cone consists of finite sums with nonnegative real coefficients and includes zero. If, in addition, is a POVM, meaning , then is completely positive and trace-preserving, and every such joint output is a separable density matrix: it is a finite convex combination of product density matrices.
This is precisely the measure-and-prepare implication of Theorem 4 and its printed channel specialization. It applies to entangled inputs without purity, orthogonality, or independence restrictions on the prepared states.
Formalization Note The general part uses the frozen separable-positive-cone predicate because unrestricted positive effects need not preserve trace. The channel part uses normalized separability. The identity always acts on the reference factor.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Let and let be complex-linear. A finite Holevo representation with density matrices and positive semidefinite effects exists if and only if breaks entanglement in the separable-positive-cone sense.
For every supplied such representation, trace preservation is equivalent to being a POVM. For every supplied representation (2) with unit output vectors , it is equivalent to ; the input vectors need not be unit or nonzero.
This identifies measure-and-prepare maps without presupposing complete positivity or trace preservation.
For , let be the set of complex-linear entanglement-breaking, trace-preserving maps on . Then
Thus is EBT for any two EBT maps and any . Convexity refers to maps on all operators and supports the paper's study of extreme channels.
Let and let be a unitary matrix on . Then
This records that unitary dynamics preserves some entanglement. The dimension restriction corrects the printed sentence: at unitary conjugation is EBT. The correction requires independent source moderation.
Correction to the printed source.
Printed: Conjugation with a unitary matrix is not EBT, without any stated dimension exception.
Corrected: Restrict the unitary-channel assertion to d at least two.
Reason: At d=1 every joint state is separable across the one-dimensional acted-on system; the identity channel is EBT.
Let and let be a density matrix on . Define the replacement map on all operators. Then
Here pure means for a unit vector . Both ambient convex sets are recorded, as supported by the point-channel paragraph and Theorem 5(A),(B).
Let , let be density matrices, and let be positive semidefinite. For arbitrary orthonormal bases and , set . Then, on every operator ,
If the effects form a POVM the Kraus family is normalized. In the CQ case , the reduced family is , and is normalized. In the QC case , it is , normalized when is a POVM. For pure-output CQ maps it further reduces to , with unit .
These are explicit operator-sum witnesses; square roots are the positive matrix square roots.
Let and let be complex-linear. Write . The following six conditions are equivalent:
If preserves trace, the corresponding six-way equivalence holds with a POVM in A, EBT in B, normalized separable density in C, in D, and trace-preserving positivity tests in E,F. Empty general representations are allowed for the zero map. This supplies all the theorem's characterizations, including its continuation on page 5.
Let and let be an extreme CQ map in the source's terminology: for an orthonormal basis and unit vectors ,
Then is an extreme point of the convex set of EBT maps. The vectors may coincide or be dependent. The source-defined class is therefore distinguished from convex extremality itself.
Let , let be an orthonormal basis of , and let be arbitrary unit vectors. For the supplied representation ,
No orthogonality or independence assumption on outputs is imposed. This characterizes which pure-output CQ maps remain extreme in the larger channel set.
Let . If is EBT and is an extreme point of the set of CPT maps, then
Explicitly, an orthonormal input basis and unit output vectors realizing Eq.(8) exist. Neither Choi rank nor a -term Kraus representation is assumed: those are proof conclusions. This identifies the overlap of EBT with the extreme points of CPT.
The two dimension regimes for extreme EBT maps are:
whereas, for every integer , there exists an extreme EBT endomap of that is not CQ.
The qubit proof is attributed by the paper on page 8 to Ruskai [18], quant-ph/0302032. The paper supplies the higher-dimensional counterexamples, including the qutrit example. The result separates EBT extremality from pure-output CQ structure in higher dimensions.
Let and be orthonormal bases of . Put and set
These effects form a POVM, and the computed map is an extreme EBT map which is QC and is not CQ.
The third displayed effect corrects the source's repeated to , as forced by the word trine, normalization, and the proof. Independent source moderation is required. This is a concrete witness rather than a free existential channel.
Correction to the printed source.
Printed: The third effect is printed as (2/3)|g_+><g_+|, duplicating the second.
Corrected: Replace only that third effect by (2/3)|g_-><g_-|.
Reason: The narrative calls this a trine POVM and its proof uses that POVM. The changed effect cancels the off-diagonal entries; the printed effects do not sum to I.
Let and let be a von Neumann measurement: mutually orthogonal Hermitian projections summing to . If some has rank greater than one, then
The actual computed pinching map is used. A rank-two block can retain entanglement, distinguishing such block projections from rank-one dephasing.
Let and let satisfy . If , then the channel with this actual Kraus list satisfies
The empty normalized list is impossible for . The result gives a lower bound on the size of every Kraus representation of an EBT map; its cited ingredients are [11], or [8] with [2].
Let , let be CPT, and let for the unit maximally entangled vector . If , then
where is matrix transpose, a complex-linear map. The exact rank and TP hypotheses are retained; the low-rank separability ingredient is attributed to [10].
Let be a separable density matrix on , with . Suppose both and its first marginal have rank . Then there exist , nonnegative weights summing to one, and unit vectors , such that
The rank is independent of the ambient dimensions. First proved in [10], the lemma receives a new proof here and bounds the length of separable decompositions under a matching marginal-rank assumption.
Fix an orthonormal basis of . Let , , , and . The computed channel
is extreme in EBT, is not CQ, and is not extreme in CPT. Its distinct rays have overlap , and the only Hermitian projections commuting with all four pure densities are , ruling out an orthogonal block split.
Its positive rank-one Holevo form is essentially unique: in any finite representation with strictly positive weights , unit output vectors , and unit input vectors , each pair of pure densities equals for some . The sum of weights belonging to each ray is . This permits splitting and merging weights and arbitrary vector phases; it makes no assertion about arbitrary mixed-output or zero-effect presentations.
For each i, the plane reflection U_i=I-2|v_i⟩⟨v_i| is unitary, and on every operator X the final page-12 construction is explicitly realized by Phi(X)=(1/4)X+(3/16) sum_(i=0)^3 U_i X U_i†. The five nonnegative coefficients sum to one.
Let and let be a real Hilbert–Schmidt orthonormal basis of Hermitian matrices, with and the remaining matrices traceless. For a density matrix , put , which is real. Then
The printed is corrected to its reciprocal, as forced by trace normalization. This coordinate description is used in the map factorization; independent source moderation of the correction remains required.
Correction to the printed source.
Printed: The source prints w_0=d^(1/2) with G_0=d^(-1/2)I and trace rho=1.
Corrected: State w_0=d^(-1/2); all other displayed coefficient formulas are retained.
Reason: Directly Tr(rho G_0)=Tr(rho)/sqrt(d)=1/sqrt(d); rho=I/2 is a concrete counterexample to the printed exponent.
In the preceding Hermitian basis, let be density matrices and positive semidefinite effects, . Define , and for the computed Holevo map. Then
Moreover, is a POVM if and only if the first row of is . Both factors have rows and columns. The product corrects the printed according to those dimensions and the unchanged entrywise formula. Independent moderation of this correction is required.
Correction to the printed source.
Printed: The source prints T=W^T U although W and U are d^2 by N.
Corrected: Use T=W U^T and retain the source's unchanged entrywise sum t_jn=sum_k w_jk u_nk.
Reason: W^T U has shape N by N, while W U^T has the required d^2 by d^2 shape and exactly the printed entries.
Let , let be the Hermitian coordinate basis above, and let be CQ or QC. Let be its full -by- coordinate matrix and the density matrices. Then
The second dimension is affine in the trace-one hyperplane, following the separation of the identity coordinate on page 12. A linear-dimension interpretation would fail at . This bounds the geometry of the output-state set.
Correction to the printed source.
Printed: The source calls the density image a subspace of dimension at most d-1.
Corrected: Interpret this as an affine span over the real numbers within the trace-one hyperplane.
Reason: Equation (23) fixes the identity coordinate; the convex hull of d density outputs has affine dimension at most d-1. Linear dimension zero already fails for the d=1 state.
These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.
Qubit Entanglement Breaking Channels.
Let be complex-linear, completely positive and trace preserving. Let and . Then
The inequality is the positive-semidefinite operator order. This provides an operator test on the normalized Choi state.
Let , and let be the trace-preserving canonical Bloch map . If it is entanglement breaking, then
There is no unitality assumption. This is a necessary condition for the general translated channel.
Let be a completely positive trace-preserving qubit map with . Suppose independent unitary changes of input and output bases put it in canonical form with parameters . Then
This makes the necessary condition sufficient in the unital case.
For , let have translation and diagonal Bloch parameters . These maps are completely positive and trace preserving, and
Moreover, for every there is with and not entanglement breaking. Thus small diagonal-parameter sum does not suffice for translated channels.
For and , let . Then
Whenever this holds, is CQ and equals , where and . This includes , when the image is a point.
Let be a QC qubit channel: it measures a POVM and prepares one of two orthogonal pure states. There are qubit unitaries and a CQ map such that
A CQ map measures rank-one orthogonal input projectors and prepares density matrices. The assertion relates these two channel subclasses without identifying their definitions.
Set , , , and . Set , with , and define
The effects form an extreme three-outcome POVM, each is a density matrix, and is EBT, neither CQ nor a point channel, and not extreme in the EBT set. Thus extreme measurement data need not produce an extreme channel.
Let be a CPT qubit map in the fixed canonical basis, and let . Then is completely positive, and changing any individual translation coordinate to preserves complete positivity. In addition,
Here CP denotes complete positivity. These are all three numbered assertions, together with the any-coordinate translation invariance explained immediately before the proposition.
Let be a CPT qubit map in canonical form. Then
The planar regime includes degenerate lines and points. This is a sufficient condition only.
Let with , and set . The canonical point map is CPT and CQ, is a density matrix, and on every operator it satisfies
If , there is a unit vector with , and the map is extreme in both the CPT and EBT sets. This identifies the pure-output endpoint of the point-channel family.
Let be a CPT canonical qubit map. If exactly one coordinate of is zero, then
Also, when , . If both are nonzero and equality holds, then . Thus a truly planar image stays strictly inside the Bloch sphere.
In a fixed diagonal basis, let , and . Then
The theorem determines both the entire parameter octahedron and exactly its six extreme points.
In the real vector space of complex-linear qubit maps, let be the unital trace-preserving entanglement-breaking maps, and the unital CQ maps. Then
The channel sets allow arbitrary input and output bases. This is a statement in map space, not only in one diagonal parameter slice.
Fix any translation , and define . Then
Inversion negates and leaves fixed. Infeasible translations are permitted; both sides can be empty.
Let be the trace-preserving entanglement-breaking complex-linear qubit maps, and the CQ maps. Then
These are both conclusions of the main theorem. It does not assert that every CQ map is extreme. The proof gap concerning intersecting planes on p.15 is recorded separately, without becoming a theorem hypothesis.
Suppose is EBT and for a chosen coordinate . It belongs to the real convex hull of canonical CQ maps satisfying and having at most one nonzero coordinate of . Moreover, if denotes the CPT parameter slice fixing only and , then
This preserves the canonical coordinate plane, including point-channel endpoints; the other translation coordinates may vary.
For a CPT canonical qubit map with ,
For fixed with and , its EBT slice is exactly . This includes the filled square and its collapsed endpoints; a negative radicand is not totalized into an extra radius-zero slice.
Fix and . Let consist of canonical EBT maps with these fixed parameters and either or . Let be all CQ maps canonical in the same basis. Then
This gives the same-basis decomposition on the illustrated parallelogram. It neither covers the entire slice nor requires CQ summands to retain .
Let be EBT, with for all three coordinates. There are input/output unitaries and such that, writing ,
Here consists of canonical CQ maps for which for some . Also . Thus summands are canonical in the rotated basis and need not be canonical in the original one.
Only these reviewed original-paper statements are in scope. Definitions have reviewed bodies; target proofs remain open (sorry). Reviewed deferrals are excluded. No theorem proof or whole-paper formal proof is claimed.
Separability Criterion for Density Matrices establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let and index orthonormal bases of two nonempty finite-dimensional complex Hilbert spaces, with no requirement that their dimensions agree. Let be a density matrix on their tensor product, so is positive semidefinite and . Suppose it is separable: for some finite ensemble of density matrices on the first subsystem and on the second, and real weights summing to one, . Define its first-subsystem partial transpose by . Then
Equivalently, all eigenvalues of the Hermitian matrix are nonnegative. This is a necessary condition for separability, with no assertion of a converse.
Formalization Note The unspecified ensemble in Eq. (1) is represented by an arbitrary finite ensemble in the paper's finite-dimensional setting. Allowing zero weights is equivalent to the printed positive-weight convention after deleting zero-weight terms; normalization excludes an empty ensemble.
Let and index orthonormal bases of two nonempty finite-dimensional complex Hilbert spaces, with no requirement that their dimensions agree. Let be a density matrix on their tensor product, so is positive semidefinite and . Suppose it is separable: for some finite ensemble of density matrices on the first subsystem and on the second, and real weights summing to one, . Define its first-subsystem partial transpose by . Then
Equivalently, all eigenvalues of the Hermitian matrix are nonnegative. This is a necessary condition for separability, with no assertion of a converse.
Formalization Note The unspecified ensemble in Eq. (1) is represented by an arbitrary finite ensemble in the paper's finite-dimensional setting. Allowing zero weights is equivalent to the printed positive-weight convention after deleting zero-weight terms; normalization excludes an empty ensemble.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Let be a density matrix on two nonempty finite subsystem spaces with basis sets and . Define , transposing only the first subsystem. Then
The assertion holds for arbitrary subsystem dimensions and requires no separable decomposition. It makes the eigenvalue test a test on a Hermitian matrix.
Let be a density matrix on , with nonempty finite basis sets. Let and be arbitrary complex unitaries on the respective subsystem spaces, and set . Writing for transposition of the first subsystem only, one has
as polynomials in . Hence the two partial transposes have the same eigenvalues with algebraic multiplicities. This expresses the criterion's independence of local basis choices.
For two qubits, let , , and , where . Let . Its characteristic polynomial is
In particular, if , then is positive definite and satisfies the necessary separability criterion. The calculation identifies the effect of white noise, whose random fraction includes all four Bell components equally.
Let satisfy , and let . Set and . If , then, for ,
The negative eigenvalue obstructs separability. Both the determinant and spectral conclusions are retained.
Let be the two-qubit singlet density matrix and let . Define and . Then
Thus even an arbitrarily small positive singlet fraction in this family produces entanglement. The zero-fraction endpoint is excluded by the source's positivity condition.
Let be a density matrix on two nonempty finite subsystem spaces and , and let . Group the copies so that the first observer holds all registers and the second holds all registers. In these coordinates let denote the product with entries , and put . Then
The last implication holds independently of separability. This is the finite-copy stability that prevents strengthening this algebraic test by taking identical copies.
These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.
Reversing quantum dynamics with near-optimal quantum and classical fidelity (Barnum, Knill) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be an ensemble of density matrices on a finite-dimensional Hilbert space, indexed by a finite label set , with probabilities , . Write and , and let be the generalized inverse square root (non-zero eigenvalues inverted, zero eigenvalues kept). The pretty good measurement (PGM) has effects . For density matrices let be the Bures–Uhlmann fidelity.
Then the success probability of the PGM, and therefore the optimal success probability over all measurements (POVMs with one outcome per label), satisfy
the sums running over ordered pairs of distinct labels.
This bound expresses the error of state discrimination through pairwise overlaps only; it is the tool behind the polynomial query complexity of the hidden subgroup problem (Childs, Theorem 10.1).
Formalization Note The paper writes the left side of (39) as and opens (38) with , which is reversed relative to its own Corollary 4 and false in general (two equiprobable pure states with overlap 0.9). Its proof establishes the bound for the PGM success probability and then for the optimal ; that is what is stated. The reversal map of Eq. (35)–(36) is not formalized: for of form (35), classical fidelities of reversal are exactly measurement success probabilities on the ensemble.
Let be an ensemble of density matrices on a finite-dimensional Hilbert space, indexed by a finite label set , with probabilities , . Write and , and let be the generalized inverse square root (non-zero eigenvalues inverted, zero eigenvalues kept). The pretty good measurement (PGM) has effects . For density matrices let be the Bures–Uhlmann fidelity.
Then the success probability of the PGM, and therefore the optimal success probability over all measurements (POVMs with one outcome per label), satisfy
the sums running over ordered pairs of distinct labels.
This bound expresses the error of state discrimination through pairwise overlaps only; it is the tool behind the polynomial query complexity of the hidden subgroup problem (Childs, Theorem 10.1).
Formalization Note The paper writes the left side of (39) as and opens (38) with , which is reversed relative to its own Corollary 4 and false in general (two equiprobable pure states with overlap 0.9). Its proof establishes the bound for the PGM success probability and then for the optimal ; that is what is stated. The reversal map of Eq. (35)–(36) is not formalized: for of form (35), classical fidelities of reversal are exactly measurement success probabilities on the ensemble.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Potential-Function Proofs for First-Order Methods (Bansal, Gupta) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the regret bound of online mirror descent with a constant step size.
Let be a finite-dimensional real vector space with an arbitrary norm , and let be the dual norm of a linear functional . Let be a convex body (closed, convex, with nonempty interior). Let be differentiable functions that are convex over . Let be differentiable and -strongly convex with respect to for some , i.e. for all , and let be its Bregman divergence. Fix a step size and a starting point . Mirror descent produces and, for , where ; here minimizes over . Then for every such run and every ,
With the Euclidean norm and it recovers the regret bound of projected online gradient descent; with negative entropy on the simplex it gives the Hedge bound.
Formalization Note The source prints the second sum as ; is a typo for and is corrected. Gradients are Fréchet derivatives, whose operator norm is the dual norm. The first iterate is the Bregman projection of (equal to when ).
This is the regret bound of online mirror descent with a constant step size.
Let be a finite-dimensional real vector space with an arbitrary norm , and let be the dual norm of a linear functional . Let be a convex body (closed, convex, with nonempty interior). Let be differentiable functions that are convex over . Let be differentiable and -strongly convex with respect to for some , i.e. for all , and let be its Bregman divergence. Fix a step size and a starting point . Mirror descent produces and, for , where ; here minimizes over . Then for every such run and every ,
With the Euclidean norm and it recovers the regret bound of projected online gradient descent; with negative entropy on the simplex it gives the Hedge bound.
Formalization Note The source prints the second sum as ; is a typo for and is corrected. Gradients are Fréchet derivatives, whose operator norm is the dual norm. The first iterate is the Bregman projection of (equal to when ).
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Quantum Amplitude Amplification and Estimation (Brassard, Høyer, Mosca, Tapp) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the overlap identity for Fourier phase states (Brassard, Høyer, Mosca, Tapp, Lemma 10), which yields the outcome distribution of Fourier-transform phase estimation.
Let be an integer. For a real number , the phase state on the -dimensional register with orthonormal basis is
For reals , let be the distance on the circle . Let , , and . Then:
The inner product is conjugate-linear in its first argument. Taking gives the probability of outcome when is measured, which is the paper's Theorem 11 and the lecture notes' Proposition 3.11.
Formalization Note The phase state is the shared definition bhmtPhaseState M ω on EuclideanSpace ℂ (Fin M), and is circDist ω0 ω1 = |(ω0 − ω1) − round(ω0 − ω1)|, which equals the minimum in Definition 9.
This is the overlap identity for Fourier phase states (Brassard, Høyer, Mosca, Tapp, Lemma 10), which yields the outcome distribution of Fourier-transform phase estimation.
Let be an integer. For a real number , the phase state on the -dimensional register with orthonormal basis is
For reals , let be the distance on the circle . Let , , and . Then:
The inner product is conjugate-linear in its first argument. Taking gives the probability of outcome when is measured, which is the paper's Theorem 11 and the lecture notes' Proposition 3.11.
Formalization Note The phase state is the shared definition bhmtPhaseState M ω on EuclideanSpace ℂ (Fin M), and is circDist ω0 ω1 = |(ω0 − ω1) − round(ω0 − ω1)|, which equals the minimum in Definition 9.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
In a Proof-of-Stake (PoS) cryptocurrency, new coins are not mined with computing power: before each date the protocol picks one coin holder at random, with probability equal to the fraction of coins she holds, and pays her a reward of new coins. A common claim in the cryptocurrency press is that this makes the rich richer: larger holders are selected more often, so their holdings should grow faster. Roşu and Saleh (Management Science 67(2), 2021) test this claim in a model that is, for a buy-and-hold investor, a generalized Pólya urn whose number of added balls varies with time.
Their first result (Proposition 1) is that an investor's share is a martingale with an almost-sure limit whose mean is the initial share, which the paper itself calls standard for Pólya urns. The sharper question is whether shares are stable in the strict sense: does the limiting share concentrate at the initial share when the economy starts with many coins? The answer depends on how fast the reward grows with the coin supply, and Proposition 4 locates the threshold exactly.
Time is discrete, . Fix a probability space with a filtration . Initially coins are outstanding, and the tracked investor (investor 1) holds of them. At each date the protocol pays a deterministic reward , so the coin supply is
Let , -measurable, indicate that investor 1 is selected at . She never trades, so her coins follow , and her share is . The PoS selection rule is
The other investors enter only through . The power reward is for , with constants .
The variance sequence is , , the paper's (A12). Proposition 1 gives an almost-sure limit . For the goal, the initial share is fixed and the initial supply varies: model has and .
For and ,
The statement fixes no constant and no rate. It is the full equivalence, as printed.
The result. Proposition 4 separates two regimes of PoS reward schedules that grow with the supply. For sublinear growth () a large economy keeps every holder's share near its starting value: the protocol does not redistribute wealth. For linear or faster growth () the limiting share has the maximal variance whatever the initial supply. The share then ends near or with probability bounded away from zero, even though its mean is unchanged. Proposition 3 of the same paper covers non-increasing rewards. Together they say which PoS implementations give stable shares.
Formalizing it. The paper's proofs are short and informal. This mission produces a machine-checked version of the model and of the equivalence, and a reusable Lean treatment of a time-inhomogeneous two-colour Pólya urn: the martingale property, the closed-form variance recursion, and the variance of the limit. None of these results has a machine-checked proof on Prove2Me or in Mathlib.
The "if" direction combines Lemma 5 with Chebyshev's inequality. Lemma 5 needs a Riemann-sum comparison: the sum is bounded by . This uses that is increasing and is decreasing, and the details matter at the first index. The step from the variances of to the variance of the limit needs dominated convergence for squares.
The "only if" direction is where the printed argument is loose. The page lets inside a statement about . What is true and needed is that for each fixed the ratio stays bounded below in , so . The tail bound (A31) must then be derived from the exact variance alone, uniformly in . Neither Doob's convergence theorem nor Chebyshev's inequality gives this lower bound directly.
All objects are defined in the namespace PoSShares.Stability. A Model Ω carries the filtration, , , and the indicators . coinSupply, coins, share, IsPoS and IsPowerReward are its supply, coins (5), share (1), selection rule and power reward. aSeq and alphaSeq are (A12) and (A16), both started at index with value . Committed conventions:
μ.real.Trivializing formalizations are ruled out:
IsPoS is satisfiable for every , and , and the power reward rule has a solution for all .limUnder default.A complete development needs Mathlib's conditional expectation and conditional variance, the martingale convergence theorem for bounded martingales, the law of total variance, Chebyshev's inequality, and integral comparison for monotone functions. The urn lemmas (milestones 1–5 and 8) apply to any deterministic reward schedule and are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Lemma 5.
An online allocator must commit to an action after each arrival, although later arrivals can change which actions would have been best. Revenue management and online resource allocation use regret to measure the expected reward lost against a benchmark. If the benchmark sees too much future information, this gap can grow with the horizon even when the online controller behaves optimally. Vera, Banerjee, and Gurvich use a benchmark whose extra information can be chosen for the application, and relate regret to two quantities that can be studied separately: how often the online action disagrees with an informed action, and how accurately a proposed value function satisfies a Bellman equation (Vera–Banerjee–Gurvich, 2020, §§2–3).
The paper proves constant-regret application results for online probing, dynamic pricing, and learning by combining this framework with estimates particular to each model. This mission isolates the framework's Theorem 5 and the displayed statements leading to it. Its result is known on paper; the work here is to give the model, the conditional expectations, and the regret bound machine-checkable statements.
There are decision periods, indexed by time to go . At the start of period the controller is in state and observes an input . It selects an action from a nonempty feasible set , collects real reward , and moves to . The initial state is the fixed state .
The observed filtration is generated by the arrivals . A non-anticipative policy chooses an -measurable action from the current state. Offline has the augmented filtration , where is a fixed sigma-algebra carrying extra information. Offline's value is the feasible-action maximum in the conditional Bellman equation (2), with . Its expected initial value is the benchmark for the online policy's expected reward. Regret is their difference.
A relaxed value and a Bellman loss obey the Bellman inequalities if initially bounds the conditional Offline value, ends at zero, and at each state is at most one feasible action's immediate reward plus its expected relaxed continuation and . An action meeting this inequality is satisfying. A maximum-loss bound controls the shortfall of every feasible action. For a policy with action on its actual trajectory, is the event that is not satisfying under this same and .
Proposition 1 concerns a feasible -adapted policy that always takes satisfying actions. It bounds its shortfall from Offline by the expected accumulated Bellman loss:
The proposal also states the one-step displayed inequality from its proof, where a conditional continuation at a fixed state and action becomes the conditional continuation of the policy's random trajectory.
Theorem 5 concerns a feasible non-anticipative policy. It states the pathwise-compensation expectation bound and, when is nonnegative, the paper's two-term bound:
The milestones include the paper's maximum-loss, compensated one-step, and iterated displays on the route to this target. The first inequality is also stated for signed ; only the second requires .
The theorem turns a regret analysis into two concrete estimates. An application can count or bound the periods when the online action fails the informed satisfying-action test, and can separately quantify the error in its chosen relaxed value. Neither quantity alone certifies small regret; the theorem supplies the inequality connecting both to the benchmark's actual reward gap. The paper's constant-regret claims use application-specific bounds on these terms (Vera–Banerjee–Gurvich, 2020, §§4–6).
A complete formalization would establish the conditional-expectation and measurability infrastructure needed to apply this template to other finite-horizon allocation models. The paper gives a proof of Theorem 5, but the theorem and its applications have no machine-checked proofs in this mission. The proposal records the open Lean statements and a statement-only non-vacuity check for the exact Bellman value with zero loss.
Definition 5 describes a satisfying action for a fixed state and action, while Theorem 5 evaluates it at a random state and a policy's random action. The conditional expectation in that definition cannot simply be substituted syntactically for the conditional expectation of the ensuing trajectory. Countable states and finite actions make the substitution meaningful, but measurability of the selected state and action still has to be established. The same issue appears in the maximum-loss display. Time runs backward, so the information at contains the information at ; a forward-indexed filtration would change the conditional expectation in the paper's formulas.
The second displayed inequality presents a separate statement issue: removing from is valid only for nonnegative . The paper allows signed Bellman losses elsewhere, so nonnegativity is attached to that inequality rather than to the definition of Bellman inequalities.
The Lean model uses a countable state type, a finite nonempty action type, real rewards, and an explicit nonempty feasible-action set. The probability space carries a probability measure, measurable arrivals, and an auxiliary sub-sigma-algebra . The observed and augmented information families are plain sigma-algebra families because their order decreases with time to go. The index is terminal; decision sums and hypotheses use exactly . Offline's value is defined by the feasible-action Bellman recursion and is never a free benchmark variable.
The source bounds the maximum reward above. This formalization additionally bounds feasible rewards, , and in absolute value over the finite horizon, and requires measurable reward, transition, and feasibility data. These assumptions ensure the real integrals and conditional expectations have their intended values. Definition 4 is an almost-sure real upper bound rather than a supremum that could take a default value. The feasible-action maximum in the Bellman inequality is represented by a feasible witness. The source's family is represented by the single sigma-algebra it generates, .
The goal covers every feasible -adapted state-feedback policy; RABBI is in this class. Proposition 1 retains its distinct -adapted policy class. The disagreement event uses the same as the Bellman inequalities. The maximum-loss display follows Definition 4's parentheses and sign, correcting a printed slip on p. 14. The nonnegative-loss condition corrects the second inequality of the printed Theorem 5. A complete development needs reusable lemmas on finite feasible maxima, measurable state-feedback trajectories, conditional expectations under decreasing information, and integration of finite sums. Contributions to those lemmas and to the five stated milestones are in scope.
Public buyers of medicines, school meals, computers and similar goods often run a framework agreement. A central agency selects an assortment of products through an auction and fixes their unit prices. Public offices then buy from that menu as needed, each choosing what suits it. The European Union awarded €80 billion through framework agreements in 2010, 17% of all public procurement by value. Chile's ChileCompra bought US$3 billion this way in 2018, 22% of the country's public procurement (figures as cited in the paper's introduction). Two decisions are bundled in such a mechanism: which differentiated products to put in the assortment, and at what prices. A larger assortment serves heterogeneous users better; a smaller one lets the buyer extract lower prices from the suppliers, whose costs are private.
Saban and Weintraub (Operations Research, 2021; author version SSRN 3453144) model this trade-off as a mechanism-design problem and ask a structural question: how much does the buyer lose by being restricted to linear prices, where users pick quantities from the posted menu and every supplier is paid its unit price times the quantity sold, compared with a centralized planner who could dictate allocations and arbitrary transfers? Their answer for the Hotelling model of horizontal differentiation, Theorem 4.1, is the goal of this mission.
There are suppliers . Supplier has a private unit cost in a finite set of positive reals, drawn independently with probability mass function and cdf . A profile is .
A unit mass of consumers sits uniformly on ; supplier is located at , with . A consumer at buying from at price has utility , with transportation cost . Allocations (no outside option) give gross consumer surplus , minus times the total transportation cost, and consumer surplus . The demand for an assortment and prices is a maximizer of over with for .
The virtual cost of type is
where is the predecessor of in (itself for the lowest type). Virtual costs are assumed strictly increasing (Assumption 3.1).
In a direct mechanism with allocation and transfers , supplier of type reporting gets interim utility . The two problems are:
denotes the optimal value. Every DecLin mechanism is a Cent mechanism with the same value, so always.
Let . If (1) some profile has for all , and (2) every and consecutive virtual costs differ by at most , then
The proof runs through the following statements, in attack order:
The theorem identifies a regime where linear pricing, the format actually used in framework agreements, loses nothing relative to the best mechanism with arbitrary transfers. In general it does lose: the paper's Example 4.1 has (values and ). The conditions say that virtual costs are close relative to the transportation cost, so that every supplier is in the optimal assortment for some profile and costs can be moved one supplier at a time without leaving the assortment. This gives a design guideline: when products are differentiated enough relative to cost uncertainty, posting unit prices suffices. The companion result for two-part tariffs (Proposition 4.1) and the affine-demand analogue (Theorem 4.2) are outside this mission.
The theorem has a complete proof in the paper (Appendix F and the electronic companion), but no machine-checked version exists. A formal proof would check the discrete-type envelope argument (Proposition 3.1), the explicit Hotelling demand as an optimal-transport maximizer, and the linear-algebraic consistency argument, which has gaps at ties (see Formalization scope). Each of these is reusable: the discrete Myerson characterization applies to any procurement or auction model with finite type spaces, and the Hotelling demand result applies to any model of spatial competition on a segment.
The obvious argument is: solve Cent by Proposition 3.1, then pick prices equal to virtual costs, which induce the right demand. This fails because prices must do two jobs at once. They must reproduce the centralized allocation through consumer choice, which pins down price differences among active suppliers profile by profile, and they must reproduce the interim transfers (11), which pins down averages of across profiles. Prices equal to virtual costs satisfy the first and generally violate the second. The question becomes whether one linear system in all prices of all profiles is consistent.
Lemma F.1 converts consistency into the statement that every dependency among the rows is also a dependency of the right-hand side. Proving that requires showing that the coefficients on transfer rows vanish (Step 1), and this is where Theorem 4.1's conditions enter: Lemma F.2's all-active box and connecting paths propagate from one profile to its neighbours. Without such connectivity the profiles split into classes whose transfer constraints conflict, which is exactly what happens in Example 4.1.
The Lean development lives in the namespace ProcureAssort.Hotelling, with one definition item (Setting) and eleven theorem items. Conventions:
Fin n, 0-indexed, ordered by location; is assumed because needs two suppliers. Types are a Finset ℝ per supplier; "consecutive types" means no element strictly between. Profiles are dependent functions; all expectations are finite sums.The goal cannot be satisfied trivially. DecLin ranges only over mechanisms whose allocation is consumer-optimal for the posted assortment and prices, and whose payments are price times quantity. DecLin therefore cannot choose allocations freely or pay lump sums, and an equality with OPT(Cent) is a substantive claim. The hypotheses are satisfiable, for example with two suppliers at and , and uniform.
A complete development needs: finite-type mechanism-design bookkeeping (interim sums, the envelope formula), the Hotelling demand as a maximizer (a one-dimensional transport argument), finite-dimensional linear algebra for Lemma F.1, and the combinatorics of Lemma F.2. Contributions to any milestone are welcome, as are proofs of the Fredholm alternative and of the discrete Myerson lemma in general form.
Misinformation campaigns target specific people in a social network and rely on the network to spread what they plant. Whether such a campaign can succeed depends on how people combine what they see themselves with what their neighbours believe. Mostagir, Ozdaglar and Siderius (SSRN 3474643; Management Science, 2022, doi:10.1287/mnsc.2021.4265) model a network in which a strategic principal injects slanted news into chosen agents. Some agents are Bayesian and know the truth; the rest are DeGroot agents who average their own news-based opinion with their neighbours' beliefs.
The paper asks when society as a whole can be manipulated. Every later result in it — which agents the principal targets, which networks resist manipulation, how the answer depends on the network's density — is a statement about the agents' long-run beliefs. Its Theorem 2 supplies those beliefs in closed form, and that closed form is the subject of this mission.
DeGroot updating (DeGroot, 1974) and its combination with personal Bayesian updates (Jadbabaie, Molavi, Sandroni and Tahbaz-Salehi, 2012) are standard models of non-Bayesian social learning. Stubborn agents in averaging dynamics were studied by Acemoglu, Como, Fagnani and Ozdaglar (2013). The present model adds a principal who corrupts the signals of targeted agents.
There are agents and a binary state with prior . Agent has a signal quality . At each time agent receives a signal :
Agent 's signals are independent over time. Its personal experience is the posterior it would compute taking every signal at face value. With the numbers of and signals among ,
and .
A set of agents is Bayesian. A Bayesian agent knows and always believes it. Each DeGroot agent has weights and with . For a state , its belief follows the DeGroot update
The influence matrix has zero rows for Bayesian agents and row for DeGroot agents. The vector has entry on Bayesians. The unweighted graph has a link when listens to ; for a DeGroot agent this means .
Assumption 1 (pp. 10–11):
Under Assumption 1, for every principal action , each DeGroot agent's personal experience converges almost surely to a constant , and
where the Bayesian entries of the vector are the correct belief. The goal does not fix the constants: the paper computes them only later (display (2), p. 12).
Theorem 2 reduces the paper's manipulation question to linear algebra. A DeGroot agent ends up believing the wrong state exactly when the corresponding entry of crosses a threshold. The principal's targeting problem then becomes a combinatorial problem over in which the network enters only through . The paper's DeGroot centrality (Proposition 2) and its results on dense and sparse networks all start from this formula.
On formalization: the paper proves Theorem 2, but no machine-checked version exists. The mission's statements also record two places where the written argument needs repair. The text attributes the almost-sure convergence of to the martingale convergence theorem, but is a face-value posterior and not a martingale under the corrupted signal law. The proof's step from small increments of to convergence of is also not valid as written. Both claims are true under Assumption 1, and a complete development supplies correct arguments. The supporting results — spectral radius below one for a substochastic matrix with leakage reachable from every row, and convergence of linear recursions with convergent input — are reusable beyond this paper.
Two steps resist the obvious arguments.
First, is a function of the drift of a random walk. Its limit exists only if the walk is transient or . For a targeted agent the walk's step law mixes the principal's message with organic news. For one boundary value of the step has mean zero, the walk is recurrent and oscillates forever. Assumption 1(i) excludes exactly that value. A proof must use it; a martingale argument does not apply.
Second, is substochastic but not strictly so: a DeGroot row sums to , which equals whenever . A row-sum bound alone gives , not . Strict inequality needs every DeGroot agent to reach, in the weighted graph, an agent that leaks weight — a Bayesian or a DeGroot agent with . This uses the interaction of Assumption 1 (ii), (iii) and (iv), with Bayesian agents' outgoing links playing no role in .
Agents are Fin n and the Bayesian set is a Finset. Time is discrete, and the history at time is the signals at times . The state space is a two-element inductive type. The signals are random variables on a probability space . Each agent's sequence is independent over time with the law above; signals of different agents may be dependent. This is deliberate: in the paper all targeted agents receive the same principal stream, so cross-agent independence would exclude the paper's own model. The principal's action is pure (), as §3.2 allows without loss of generality. The DeGroot initial belief can be any value in , and the conclusion holds for every such initial belief on one almost-sure event. "Spectral radius" is Mathlib's spectralRadius ℂ of the complexified matrix. is Mathlib's matrix inverse; no invertibility hypothesis is added, because Assumption 1 implies it. In the graph , a DeGroot agent's links are exactly its positive weights; Bayesian agents' links are free.
The personal experience is the explicit face-value posterior of the given signal process, and the conclusion of the goal includes its almost-sure convergence to the constants used in the limit. The goal therefore cannot be met by an abstract learning rule or a free limit vector.
A complete development needs:
Contributions of any of these, as standalone lemmas, are welcome.
Online marketplaces such as lodging, ride-hailing and freelancing platforms test changes to their product (a new ranking, a new fee display, a new photo layout) with randomized experiments. In a two-sided marketplace these experiments are subject to interference: treated and control units compete for the same scarce supply or demand, so the outcome of one unit depends on the treatment of others, and the stable-unit assumption behind the textbook difference-in-means estimator fails. The resulting bias can be as large as the effect being measured, and platforms routinely choose between randomizing customers (customer-side randomization, CR) and randomizing listings (listing-side randomization, LR) without a principled guide.
Johari, Li, Liskovich and Weintraub (arXiv:2002.05670, Management Science 2022) introduced a tractable model in which this question can be answered. Their analysis shows that which side to randomize depends on market balance, the ratio of the rate of demand to the rate at which supply is replenished. This mission formalizes the demand-constrained half of that answer.
There are finitely many listing types and customer types . Listings of type form a mass , with . Customers arrive at total rate , a share of them of type (). A state records the mass of available listings of each type, and lies in .
An arriving type- customer includes each available type- listing in its consideration set with probability , has utility for it and an outside option of value , and books by multinomial logit. In the mean-field limit the probability that it books a type- listing is
A booked type- listing stays occupied for an exponential time of rate , with and . A steady state is a state balancing the flows:
A two-sided randomization (TSR) design treats a fraction of customers and a fraction of listings. The intervention replaces by , both positive, only when a treated customer meets a treated listing. The experimental system is the same mean-field model on the types and , (0 = control, 1 = treatment), with , , and . The mass vector is written . At its steady state , the rate at which condition- customers book condition- listings is
The global treatment effect is . The naive estimators are
Fix every parameter except and , and consider sequences with (a demand-constrained market). Then for every
and for every and Lebesgue-almost every treatment utility in the positive orthant, there is such that along every such sequence
Theorem 3, together with its supply-constrained mirror (Theorem 4 of the paper, not part of this mission), is the paper's main structural finding. Each naive design is unbiased in one extreme of market balance and biased in the other. When demand is scarce, customers do not compete for listings, so randomizing customers creates no interference, while randomizing listings makes treated and control listings compete for the same customers. This finding motivates the paper's TSR designs, which interpolate between CR and LR according to market balance.
The result is proved in the paper; nothing here is open. To the best of the curators' knowledge, no part of it has a machine-checked proof. The mission produces a formal account of the mean-field model and its steady state, which other models of matching markets with MNL choice and occupancy can reuse. It also makes the informal "generically biased" claim precise: the paper argues it only by saying that the limit "in general" differs from the GTE.
The central step is Theorem 1. The steady-state equation is a nonlinear fixed point, and the objective whose minimizer it is fails to be convex in . Existence and uniqueness therefore need a change of variables under which becomes strictly convex and coercive, followed by a boundary argument. The limit statements then follow from a quantitative bound on and the continuity of the choice probability, but they must hold at boundary designs ( or ), where some types have zero mass.
The LR half carries a second difficulty. Showing that the LR estimator is biased for one parameter value is easy; the claim is that the bias vanishes only on a Lebesgue-null set of treatment utilities. That requires the zero set of a nonzero rational function on an open orthant to be null, a fact Mathlib does not state in ready form.
Everything lives in the namespace TwoSidedExp.DemandLimit. Types are Fintype; treatment conditions are Fin 2. A mean-field system MFSystem Γ Θ carries (eps) and . A Model adds , and Model.expt aC aL is the experimental system. and are arguments, and a sequence of systems is a pair of positive real sequences with .
Conventions the formalization commits to:
Real.log 0 = 0. In (10) the printed is read inside the sums, as in (30).Trivializing formalizations are ruled out explicitly. is never evaluated at instead of the steady state. GTE is built from the experimental system's and , not from a separate formula. The LR half is an almost-everywhere statement with a sequence-independent , not an existential.
Infrastructure that is reusable beyond this mission: strict convexity and coercivity of log-sum-exp-type objectives, and the Lebesgue-nullity of zero sets of nonzero polynomials on . Proofs of any milestone are welcome. So are alternative routes to Theorem 1, for example via a monotone fixed-point argument.
Quantum signal processing transforms the eigenphases of a unitary operator by a sequence of controlled operations and single qubit rotations. To know which transformations such a sequence can realize, one must characterize the matrix functions produced by the sequence. Haah's product decomposition theorem gives such a characterization without the restriction on the projectors used in some earlier quantum signal processing constructions. The result concerns exact functions; the numerical synthesis algorithm and its precision analysis are separate parts of the paper.
Let be a nonzero complex number. A rank one orthogonal projector on is a Hermitian matrix with and trace one. Its complementary projector is . The associated primitive matrix is
For , this matrix is unitary with determinant one. Given such projectors, indexed in their multiplication order, and a constant matrix , the product of interest is
The leftmost primitive factor is , and the product has exactly primitive factors. At the product of primitive factors is the identity and is the constant matrix . Although the physical interpretation uses points on the unit circle, the formula defines at every nonzero complex . These conventions follow §2, equations (2) and (3).
A matrix Laurent polynomial of width is written
where each is a complex matrix and all coefficients outside vanish. The set consists of these polynomials for which whenever . A member has degree when or . The subset consists of members whose nonzero exponents have the parity of , so for every odd integer . The notation conjugate transposes each coefficient while leaving its exponent unchanged: . These are the conventions of Definition 1 and equations (4) and (5).
The goal is all of Theorem 2. First, every product of primitive matrices belongs to . Conversely, every of degree has a unique ordered tuple satisfying the product formula, with and each a rank one orthogonal projector. For , the final projector is determined by the leading coefficient:
The formula includes the assertion that its denominator is nonzero under the theorem's hypotheses; that is a consequence to establish, rather than an extra assumption. The case retains the product characterization and uniqueness, while having no final projector. The milestones state the source's primitive matrix observation, polynomial identities, leading coefficient conditions, degree reduction, and the relation between the two extreme coefficients.
The theorem identifies the Laurent polynomials that admit the specified quantum signal processing product and says that the factors are uniquely recoverable from the matrix function when the number of factors is fixed. This supports the exact synthesis question motivating the paper: whether a desired valued function on the unit circle is achievable by the primitive operations. The formula for also identifies the last factor directly from a coefficient of the target function. Haah's §4 algorithm uses the decomposition, but its numerical guarantees are outside this mission.
The paper proves Theorem 2. The formalization target is a machine checked version of that known theorem and its source stated intermediate claims. The definitions of matrix Laurent polynomial evaluation, parity restricted coefficient families, and primitive projector factors can also support later work on polynomial matrix functions. The mission does not claim that these statements have already been proved in Lean.
Membership in is given only on the unit circle, while coefficient identities needed for the decomposition concern Laurent polynomials throughout . A pointwise unitary identity on the circle must therefore be promoted to an identity of Laurent polynomials before its extreme coefficients can be compared. The main structural difficulty is that a matrix product may lose its highest and lowest powers even when its factors are nonzero. Identifying a projector that lowers the degree must control both extremes at once and preserve the parity and conditions. Uniqueness also depends on fixing exactly factors: extra complementary factors can cancel.
Lean represents a Laurent polynomial by a coefficient family with explicit width support, and evaluates it by a finite sum of integer powers. Equalities of Laurent polynomials are stated for every nonzero complex . The positive integer is represented as a natural number, with integer casts for exponents. The special unitary group is Mathlib's ; the paper's rank one orthogonal projectors are represented by Hermitian idempotence together with trace one. This trace condition is equivalent to rank one for these projectors. An ordered function on supplies precisely factors. The last factor has index in Lean.
The set retains both the width and conditions of and adds the parity condition. It is defined from coefficients, not from the existence of a product decomposition. Allowing rank zero or rank two projectors, dropping unitarity, or allowing a variable factor count would change the theorem. The source's remark that any orthogonal projector yields a member of is read with the rank one condition of equation (2): the literal unrestricted remark fails for and . The singular leading coefficient milestones require , and the last projector formula has the same domain.
The development needs facts about determinants, conjugate transpose, projectors, finite matrix products, and uniqueness of finite Laurent expansions. The Laurent polynomial infrastructure and rank one matrix facts are reusable beyond this theorem. Contributions proving the source stated milestones, their faithful supporting algebraic lemmas, and the main product characterization are in scope. The parity refinement of §3.1, Lemma 4, and the §4 synthesis algorithm with its running time claim are outside this mission.
Many quantum algorithms act on a matrix that is not itself unitary: a Hamiltonian to be simulated, a linear system to be inverted, a projector to be amplified. The standard way to hand such a matrix to a quantum computer is to embed it as a block of a unitary , so that for two orthogonal projectors . The question is then which functions can be produced from a few uses of and .
Gilyén, Su, Low and Wiebe (arXiv:1806.01838, STOC 2019) answered it for polynomials: interleaving and with phase rotations about and applies a polynomial to every singular value of . This quantum singular value transformation (QSVT) recovers Hamiltonian simulation, amplitude amplification, fixed-point search, quantum walks and matrix inversion as instances of one identity, and is now the common language of these algorithms (see the survey of Martyn, Rossi, Tan and Chuang, PRX Quantum 2021).
Timeline.
Let be a finite-dimensional complex Hilbert space, a unitary on it, and orthogonal projectors. The projected unitary is . Put , , . A singular value decomposition of consists of orthonormal bases of and of and numbers with
For , the singular value transformation is when is odd and when is even, with for .
The phase operator of a projector is . For , the alternating phase modulation sequence is the product, from on the left to on the right, of when is even and of when is odd. On the single-qubit side, for , and is said to realize if is the top-left entry of for every .
In Lean these are ProjUnitarySVD U Proj Projt (the decomposition data), svtOdd/svtEven, phaseRefl, altPhaseSeq, reflR and qspRefl, in the namespace QSVT19.Main.
Let and let have degree , parity , and on . Then there is such that for every singular value decomposition of
with for odd and for even . The only constraints on are those that are necessary; no degree-dependent constant appears.
The result. Corollary 18 says that every real polynomial of degree , of definite parity and bounded by on , can be applied to the singular values of with uses of and and one ancilla qubit. Every application in §3.4–§5 of the paper (fixed-point amplitude amplification, singular vector transformation, the pseudoinverse, Hamiltonian simulation, Gibbs sampling) is this corollary applied to a suitable approximating polynomial, so a formal proof makes all of them conditional only on polynomial approximation bounds.
Formalizing it. The result is proved in the paper; none of the statements of this mission has a machine-checked proof on the platform. A formal development would provide reusable infrastructure absent from Mathlib: singular value decompositions over sub-spaces, the two-dimensional invariant-subspace decomposition of a projected unitary (a quantitative form of Jordan's lemma), and the polynomial characterization of single-qubit QSP. Theorem 3 of the paper, the form of the QSP characterization, is already posed on the platform as QAlgorithms.Childs.qsp_characterization; Corollary 8 depends on it.
The obvious argument for Theorem 17 is "restrict to each two-dimensional subspace and read off the QSP product". Making that rigorous means proving that the subspaces of Definition 12 are pairwise orthogonal, invariant under every factor of , and that acts on each pair of bases by exactly the reflection , including the degenerate blocks with , the one-dimensional blocks where contributes a phase , and the complement . The polynomial side is harder still: Lemma 6 factors a nonnegative even polynomial through its multiset of complex roots, grouping roots in , in , on the imaginary axis and in the open quadrant, while tracking degree and parity. Neither step reduces to a library lemma, and an argument that works only for Hermitian , or only when , proves a different theorem.
ι → ℂ for a Fintype ι with the inner product star v ⬝ᵥ w; operators are Matrix ι ι ℂ; "unitary" is U ∈ Matrix.unitaryGroup ι ℂ; "orthogonal projector" is IsStarProjection. The projectors are named Proj, Projt because Π is Lean notation. Indices are 0-based.ProjUnitarySVD U Proj Projt of data: orthonormal families with , , nonnegative non-increasing , and (17). The goal is posed for every such decomposition, with chosen first; the Definition 11 milestone shows that one exists. is a consequence and is not assumed.QAlgorithms_Defs_Hamiltonian. "deg ≤ k − 1" is degree < k and "parity " is parity , avoiding natural-number subtraction.A seller who sells over two periods, at a full price now and a discount later, loses revenue to strategic customers who wait for the discount. Waiting is costly to the customer only through availability risk: if inventory is scarce, the product may be gone by the second period. Inventory is usually known to the firm and not to its customers, so the firm can try to shape how scarce the product looks. Drakopoulos, Jain and Randhawa (SSRN 3191629, version of April 17, 2020) study this as a problem of Bayesian persuasion (Kamenica and Gentzkow, AER 2011) with many receivers: the firm commits to prices and to a signaling policy before it learns its inventory, and then sends each customer a recommendation.
Their two main results separate public from private information. Theorem 1 (p. 15): with a public signal, seen by all customers, the firm earns no more than with prices alone. Theorem 2 (p. 17): with personalized signals, which may depend on each customer's valuation and be randomized independently across customers, a simple Buy/Wait/No mechanism is optimal and strictly beats every public mechanism when the low inventory level is small. Personalized recommendations are the kind of information online retailers and travel platforms send (low-stock alerts, buy-now prompts).
There is a unit mass of customers with valuations distributed on with density and complementary distribution ; the hazard rate is non-decreasing. The firm's inventory is high, (enough for everyone), with probability , and low, , with probability . The monopoly price is , and is the valuation at which a mass of customers lies above.
A straightforward mechanism fixes prices and, after seeing , draws a latent index from a finite set with a state-dependent law; given , each -customer is independently told Buy (in period 1), Wait (buy in period 2) or No. A customer who requests the product in a period with units left and demand of mass from the others gets it with probability : if , if , otherwise (random rationing). The mechanism is obedient if every customer (for almost every ) weakly prefers to follow her recommendation, given the availabilities she can expect conditional on it: (Buy-1)–(No), p. 40. The firm's revenue is the expected value of rationed sales . A mechanism is public when the recommendations depend only on and obedience holds for each realized .
The personalized mechanism (PS1)–(PS2), p. 17, sets . In state it tells customers with to buy and the rest No; in state it tells to buy with probability
and to wait otherwise, tells to wait, and No. The price solves (14) with (15).
If , then (14) has a root , and for every such root the mechanism (PS2) is obedient, its revenue is at least that of every obedient mechanism at any prices, and
The result says that the value of information in this market lies entirely in its personalization: public information is worthless (Theorem 1), and private recommendations strictly raise revenue whenever low inventory is scarce relative to the monopoly market. The optimal mechanism is explicit and has a simple form, with the low-type firm selling out exactly in period 1 and the high-type firm mimicking it as far as incentive compatibility allows; in the paper's uniform example () revenue rises from to . The proof technique, a relaxation to a linear program over signal profiles followed by a dual reduction to a single threshold, is a template for many-receiver persuasion problems with congestion.
The theorems are proved in the paper; none of them has a machine-checked proof. The mission produces a formal model of strategic customers under rationing and personalized signaling, and the formal versions of the five steps. Two printed steps need correction to be true and are stated in corrected form (Lemma 4's tie case, the location of the root of (14)); formal proofs settle that the corrections suffice.
The obvious argument is a pointwise one: for each valuation, the Buy incentive constraint caps the high-state Buy probability given the low-state one, so set every cap tight. It fails because the availabilities in the constraints depend on the aggregate masses that the recommendations themselves create, so the constraints for different valuations are coupled; the paper resorts to an infinite-dimensional linear program and asserts strong duality without proof (p. 41). Lemma 4 is the algebraically heavy step (pp. 46–50): an envelope argument over the threshold combined with the hazard-rate monotonicity. Theorem 2 then needs a one-dimensional optimization in , the existence of a root of (14) (a fixed-point equation, since depends on ), and the case , which the paper never treats.
The paper's game (Definitions 1–2: a continuum of customers, Bayesian Nash equilibrium, sender-preferred selection) is re-expressed as the class its proofs reduce to by the revelation principle (p. 39, footnote 5): obedient straightforward mechanisms with aggregate masses. Revenue optimality over this class is what Theorem 2 asserts after that reduction. The latent index is finite (Fin n, for every n); it carries the correlation between customers' signals that public signals need. Obedience is required for almost every valuation, as in Definition 1.
Committed conventions: , , continuous on and positive on ; , ; and customer mass . Availability is avail above; at zero demand it is with stock left and without. (14) is written . In (PS2)(a) "" is taken as (a null set). (B) is read with . The program (A.16) keeps the no-Buy mechanism (), which the printed version drops. "The optimal mechanism" is stated as "an optimal mechanism" (ties exist). Lemmas 3–4 take , implicit in the paper's divisions; the goal ranges over all prices , including (p. 8). Milestone (16) is stated at the prices of (PS1): and a root of (14).
Trivializing formalizations are ruled out: revenue counts rationed sales, not ; obedience is the printed conditional constraint multiplied by the probability of the recommendation, never divided by a possibly zero probability; availability never uses Lean's ; the goal carries the existence of a root of (14), so "for every root" is not vacuous; the mechanism class contains public and correlated mechanisms; and is the revenue of the mechanism (PS2), tied to the formula (16) by a milestone.
A complete development needs: the density measure on and its tail function , monotonicity and continuity of and its inverse, the quasi-concavity of under a non-decreasing hazard rate, and bounds for the rationing function. The hazard-rate and lemmas are reusable for other pricing models. Contributions of helper lemmas, of a primal proof of Lemma 3 avoiding the duality argument, and of the case are welcome.
Distributionally robust optimization (DRO) guards a data-driven decision against misspecification of the model that generated the data. In its penalized form, the decision maker replaces the sample-average problem , where is the empirical distribution of the data , by
where is a -divergence and controls how far an adversary may move the distribution. Such models are used in operations research, statistics and machine learning (Ben-Tal et al. 2013; Lam 2016; Duchi and Namkoong 2019), and a practitioner must choose . Gotoh, Kim and Lim (arXiv:1711.06565, Operations Research 2021) study this calibration problem. Their first contribution, on which the rest of the paper builds, is an exact description of what the robust model penalizes for small : the worst-case loss of expected reward is, to first order, the variance of the reward divided by the curvature of the divergence. This mission formalizes that theorem (Theorem 2.2) together with its proof chain in Appendix F.
A decision is fixed throughout, so the data enter only through the reward vector with . The nominal distribution is a probability vector with every ; the empirical distribution of distinct data points is . Write
The divergence generator is a function satisfying Assumption 2.1: is closed (lower semicontinuous) and convex, for , for , and is twice continuously differentiable on a neighbourhood of with . Kullback–Leibler (), modified () and Burg () generators all qualify.
For , the worst-case measures of (2.7) are the minimizers, over probability vectors , of
and . The worst-case sensitivity (2.8) of the expected reward is
The proof uses the convex conjugate (F.5) and a Lagrange multiplier for the constraint .
For every satisfying Assumption 2.1, every with positive weights and every , worst-case measures exist for each , and for every choice of them
Theorem 2.2 identifies penalized DRO, for small , with a mean–variance trade-off: the robust objective is (by the expansion (2.6), which the paper cites) , and the theorem gives the derivative of the worst-case mean that underlies that expansion. The paper's calibration method (§§4–6) rests on this: since in-sample robustness acts by penalizing variance, is chosen by trading an out-of-sample reduction in variance against a loss in mean.
The result is proved in the paper; to the best of current searches it has no machine-checked proof. The mission produces a complete formal proof of Theorem 2.2 under the paper's own assumption, a formal treatment of the conjugate duality for penalized -divergence problems on finite supports, and corrected versions of three steps of the printed argument (see Formalization scope).
The theorem is a first-order expansion of an argmin, and the obvious route is to differentiate the optimality conditions at by the implicit function theorem. That step fails under Assumption 2.1: the system defining the multiplier involves evaluated at , and its partial derivative in at requires a third derivative of , which is not assumed. For the multiplier satisfies , so it is not differentiable at , although Theorem 2.2 still holds. A proof therefore has to extract the first-order behaviour of from continuity of at alone. Further work lies in showing that the minimizer is interior and unique for small when is only locally smooth, and in handling extended-real values of and .
ℝ → EReal satisfying Assumption21: lower semicontinuity, pointwise convexity on (with ), for , , for , finiteness and smoothness of the real part on an open interval around , and . Assumption 2.1 is the only hypothesis on : no third derivative, no finiteness on , and no separate (it follows from the assumption).EReal.toReal); every statement that differentiates also asserts or implies finiteness where it differentiates.Fin n. The weights are general, and ; the paper's empirical distribution is , and its variance is the special case. The paper's (2.4) also allows zero weights; these are excluded.stdSimplex. The goal asserts that minimizers exist for every and that the limit holds for every selection of minimizers; it is not a statement about an arbitrary function constrained by hypotheses, and the existence clause rules out a vacuous reading.EReal, LowerSemicontinuous, stdSimplex, deriv, ContDiffOn, HasDerivAt, Filter.Tendsto. A reusable by-product is the local theory of the convex conjugate of a convex function near a point of positive curvature. Contributions of proofs of any milestone are welcome.On-demand ride-hailing platforms replaced street-hailing on the promise that matching a passenger to a car at the moment of the request shortens the wait. Feng, Kong and Wang (SSRN 2960991, later published in Manufacturing & Service Operations Management, doi:10.1287/msom.2020.0880) ask whether that is true in a stylized model and find that it need not be: when all traffic moves in one direction, the street-hailing ("no-call") mechanism never waits longer on average than the platform ("call") mechanism. The question matters to platform designers, to regulators weighing taxi against platform service, and to the queueing literature on spatial matching, where the cost of committing a car to a passenger before it arrives is a recurring theme.
The paper studies the exact systems by simulation and, for proofs, replaces each of them by a birth–death queue whose service rates depend on the number of passengers in the system. This mission formalizes the comparison theorem for those approximations (Theorem 4) together with the results its proof uses.
A circular road of perimeter carries taxis that move clockwise at constant speed . Passengers arrive as a Poisson process of rate at uniformly distributed points of the circle; each requests a ride of exponentially distributed length with mean , so a ride lasts on average. The paper writes for the ride completion rate.
A state-dependent queue has arrival rate and, when customers are in the system, departure rate . Its average waiting time (arrival to pick-up) is given in closed form (Appendix A, p. 34):
and means that both series converge (FiniteWait in Lean, avgWait for the value).
The one-direction call approximation is the queue with rates (1), p. 16:
The no-call approximation is the queue with rates (3), p. 19:
Write and for the two waiting times (W1c, Wnc in Lean, with mu1c, muNC for the rates).
For , and , both waiting times are finite and
Milestones 3 and 4 are statements about every state-dependent queue, not only about the two approximations.
Theorem 4 is the paper's analytical support for its simulation finding (Figure 11(a)) that, with one-directional traffic, the on-demand mechanism's early commitment costs more than it gains: a no-call taxi can pick up a passenger who appeared on its path after the call mechanism would already have dispatched it elsewhere. The paper contrasts this with the two-direction system, where the call mechanism wins at very low and very high load (Theorem 5), so Theorem 4 isolates the effect of the road geometry.
The comparison principle (milestone 4) is used again, without restatement, in the proofs of Theorem 1(4) and Theorem 5. It is a general fact about birth–death queues: the average sojourn time is monotone in the service rates. A formal statement and proof of it is reusable for any model approximated by a state-dependent queue.
Status: the results are proved in the paper (Appendix A). They have not been formalized; no machine-checked proof of any of them is known.
The rate comparison is elementary but casewise: the three branches of (1) meet the two branches of (3), the state falls in different branches of each, and for the call en-route time is not the no-call integral with the exponential removed, so no single identity covers all states.
The central difficulty is the passage from one coordinate to all coordinates. The paper shows that decreases when one rate increases, and concludes that it decreases when all rates increase at once. With infinitely many rates this is not a finite chain of one-coordinate changes, so the coordinatewise statement alone does not give the comparison principle; a limit argument, or a direct argument on all coordinates, is needed, together with the transfer of summability from to .
Theorem 1(1) requires a convergence test for series whose ratios tend to , and the converse needs the strict bound in every state.
lam d v R : ℝ (λ is lam) and k : ℕ. The standing assumptions , , are implicit in the paper and explicit hypotheses of every theorem. The constant is written v / d; the name μ is reserved for rate sequences.ℕ → ℝ used for ; products run over Finset.Icc 1 i, both series start at , and the "" is the term. Lean's gives at , the paper's value.muNC is defined from (3) as printed, not through mu1c and not with its integrals replaced by bounds; no theorem compares waiting times without asserting or assuming FiniteWait (Lean's tsum of a divergent series is ); the index base and the "" follow the paper; and the goal holds for every in the stability region, not a single value.tsum, Summable, Finset.prod, intervalIntegral, Real.exp. Useful contributions beyond the milestones: a general ratio-test lemma for products of rates with a limit, and the comparison principle for birth–death waiting times, both reusable outside this paper.A firm can sell utility tokens before it has produced the good those tokens will buy. The sale supplies cash for production, but the firm can keep some or all of that cash instead. Speculators anticipate both the later value of a token and this diversion incentive when deciding whether to buy. Gan, Tsoukalas and Netessine study the resulting financing and production decisions in a three-period model of an initial coin offering (ICO). Their utility-token analysis identifies a value-to-cost threshold below which the ICO cannot raise cash and, above it, a unique equilibrium design under the paper's demand condition. Gan, Tsoukalas and Netessine, SSRN author version, §§2–3 and Appendix B.1.
The question matters to operations and finance because the funds obtained before production change the firm's later incentive to produce. Selling more tokens supplies a larger budget but leaves the firm with fewer tokens to sell after demand is realized. The model makes that tension quantitative through the ICO cap, production quantity and market token price. Gan, Tsoukalas and Netessine, pp. 7–14.
The firm initially has no wealth and owns utility tokens, redeemable for its future product. It chooses an ICO price and a cap on tokens sold to speculators. There are potential speculators. Each wants at most one token and arrives simultaneously. If tokens sell, the firm may produce units at unit cost , subject to . Customer demand has probability law and cumulative distribution function ; customers value each unit at . Token counts and quantities are represented by real numbers, as in the paper's continuous optimization. Gan, Tsoukalas and Netessine, §2, pp. 7–10.
The market-clearing price of a token after demand is realized is . Write for expected sales. Conditional on sales, the firm maximizes over the production budget. A production rule selects a maximizer at every feasible history; it is determined by this optimization problem rather than prescribed by a closed formula. At the ICO stage a speculator's expected utility is
The participation rule sells all offered tokens when , and otherwise sells none. The firm's expected terminal wealth is ICO receipts less production cost plus the market value of its unsold tokens. An equilibrium consists of production optimality after every feasible history and a pair maximizing this wealth over all and . The market-clearing and participation rules are the model's interpretations of Lemma 1 and Lemma 2(i). Gan, Tsoukalas and Netessine, (1)–(3), (10), pp. 8–10, 12, 34.
Proposition 1 identifies the optimal production quantity in two regimes. Proposition 2 identifies when a cap can support positive sales at a positive ICO price. Lemma 2 and Propositions 12–13 supply the participation and optimal-cap statements recorded as milestones. The main target is Proposition 3, including every part of its conclusion. Gan, Tsoukalas and Netessine, pp. 11–14, 34–35.
If , no feasible ICO design raises cash. If , the equilibrium ICO price and cap exist and are unique. With
the cap is the unique point in satisfying
The remaining conclusions are , all tokens sell, market-period token price equals with expectation , and the full ICO proceeds are used for production: . Gan, Tsoukalas and Netessine, Proposition 3, pp. 13–14.
The result gives a precise failure threshold for a utility-token ICO and ties the successful design to demand, production cost and the amount of tokens retained by the firm. In particular, its cap is below half of the total token supply, and at the optimum the production budget binds. These are statements about the model's incentive problem, with the demand condition required for its uniqueness result. Gan, Tsoukalas and Netessine, discussion after Proposition 3, p. 14.
The paper proves these results mathematically. This mission records their Lean statements as open goals; it does not yet supply machine-checked proofs. Completing the formalization would also develop reusable facts about expected truncated demand, inverse distribution functions, and optimization under a cash budget. The equity-token comparison, extensions and numerical experiments remain separate from this target. Gan, Tsoukalas and Netessine, §§4, 6 and Appendix C.
The firm controls the ICO price and cap before the production decision, while speculator participation responds to the production rule. Raising the cap increases possible receipts but can lower the firm's incentive to produce and therefore the resale value speculators expect. A production optimum for fixed sales does not by itself identify which sales level will occur. The firm's wealth also changes regime when the production budget ceases to bind, so a single smooth optimization statement does not cover the entire feasible set. The uniqueness claim depends on the demand-density condition stated before Proposition 12. Gan, Tsoukalas and Netessine, §§3.1–3.4 and Appendix B.1.
Demand is one probability measure on : is its cumulative distribution function and is the integral of against that same measure. The inverse expression is the infimum of nonnegative with . The paper's is represented by for and for . Because the proofs and the Appendix B.1 condition use a density and its derivative, the formal setting requires a positive differentiable density wherever and . The paper's informal is represented by . These choices are explicit added assumptions or readings of the source's conventions. Gan, Tsoukalas and Netessine, pp. 8–9, 34, 37–38, 46–48.
The Appendix B.1 condition on is applied at interior quantiles , avoiding the support boundary where the paper does not define the derivative. Lemma 2(ii)–(iii) is stated at , because at zero price its printed conclusions fail. The positive boundary price in Proposition 12 is considered on the open viable-cap interval; its printed upper endpoint has no positive solution. Its “unique solution” is the unique positive solution, since zero also solves the first displayed equation. The participation equality there is evaluated at full sales : evaluated after abstention at , it would hold automatically. These boundary readings follow the paper's own adjacent analysis. Gan, Tsoukalas and Netessine, pp. 12–13, 34–35, 45–47.
The production rule is quantified over every rule that truly optimizes the budgeted production subgame. Expected sales is the integral against , never a free function unrelated to . The equilibrium optimizes over all feasible prices and caps; the narrow interval for is a conclusion. The work needed includes measure-theoretic sales identities, quantile behavior, and the firm's regime-dependent optimization. Contributions establishing these facts or proving the named milestones fit this mission. The model here is the base utility-token, simultaneous-arrival model; equity tokens, sequential arrival, the §6 extensions and numerics are outside its scope.
Digital platforms (marketplaces, payment networks, sharing services) need large up-front investments in capacity before any revenue arrives, and their founders typically finance them by selling equity to venture capitalists. Since 2017 an alternative has been available: issuing a platform-specific cryptocurrency (a utility token) in an initial coin offering (ICO), and running the platform on a blockchain whose fee rules are fixed in a smart contract. Whether this is merely a new funding channel or a better business model is a question for operations management, corporate finance and platform economics alike.
J. Chod, N. Trichakis and S. A. Yang (Platform Tokenization: Financing, Governance, and Moral Hazard, Management Science, 2022) answer it in a model in which the entrepreneur's effort is not contractible. They show that the answer depends on the cost of building capacity: when capacity is expensive, equity wins (their Proposition 1), and when it is cheap, tokens win (their Proposition 2). This mission formalizes the second result.
An entrepreneur builds a platform of capacity at cost and exerts effort at private cost . Buyers' inverse demand is and sellers' supply curve is , with , and . Sellers pay a one-time cost to join, cash flows are discounted by , and each token is used times per period. The per-period surplus is
with partial derivatives , in . The entrepreneur's objective in both models is the net present value
In the traditional model the entrepreneur sells an equity share to a venture capitalist and can raise the fee once sellers have sunk their joining cost (holdup), which forces a first-period subsidy. Its equilibrium payoff \Pi^\$$ is the maximum of the objective subject to (1-\alpha)\mathcal F_e/(1-\delta)=\gamma\alpha\alpha\Pi^B\mathcal F_e/(1-\delta)-\alpha\frac1v d_eQ=\gamma\alpha,d(e,Q)Q=vC(Q)\alpha\le1\beta^$\beta^Bd(e,Q)Q\ge vC(Q)$.
With all other parameters fixed and or , there is such that for every both suprema are finite and No value of is fixed: the goal asserts only the existence of a cheap-capacity regime.
Proposition 2 is the paper's headline. It isolates two advantages of tokenization that hold even without any cost or technology difference: token investors are exposed to platform revenue rather than profit, which is less sensitive to effort, so the entrepreneur internalizes more of the marginal value of her effort; and a fee committed on a blockchain removes the holdup problem and with it the subsidy the traditional platform must finance. Together with Proposition 1 it delineates when a platform should tokenize.
The result is proved in the paper (Appendix B, pp. 19–20). It has not been machine-checked. The proof is short but leaves two steps informal: the relaxation of the cap (39) "by continuity", and the existence of optimal solutions behind the printed "max". A formal proof settles both, and fixes the exact hypotheses under which the claim holds (see the scope section).
The algebra of Corollary 1 and of Claim (i) is routine. The difficulty is analytic. The naive argument compares the two programs pointwise in at their largest effort roots, but the payoffs are suprema over non-compact feasible sets, and the comparison only transfers to the suprema if the traditional supremum is attained, or approached at capacities bounded away from and . The relaxation of (39) requires a bound, uniform in small , showing that points violating the cap cannot approach the relaxed supremum; this is where or enters, since with the objective near such points is not controlled as .
Parameters are a structure Params with real fields ; Params.Standing collects the printed assumptions (, , , ) and four the paper uses without stating (, , , ). Powers are Real.rpow, with Lean's for ; the partials , are closed forms, certified by two HasDerivAt helper theorems, and is a closed form certified as the argmax by Claim (ii).
\Pi^\$$ and \Pi^B\max{0,\sup(\text{objective over the feasible set})}0$ is the outside option of not starting the venture, invoked in the last paragraph of the paper's proof.
Departures from the printed statement, all disclosed in the items:
The goal cannot be met vacuously: it asserts that both objective images are bounded above, so the suprema are not Lean's junk value , and the helper piTrad_pos_example states \Pi^\>0k=1K=0.01$), ruling out an empty traditional program.
A complete development needs real-power calculus, the intermediate value theorem, strict concavity of , and a compactness or coercivity argument for the suprema. The coercivity bounds for programs of the form "maximize a concave revenue minus a power cost subject to a first-order condition" are reusable for other effort-and-capacity models. Proofs of any milestone are welcome, as are proofs of the helpers.
Sellers sometimes offer a customer a choice among individual products and a product whose final item is revealed only after purchase. Airlines, for example, can sell a fixed itinerary alongside a discounted option that leaves one feature unspecified. The seller must decide whether this opaque product earns enough to justify limiting how much individual item prices can differ. Elmachtoub and Hamilton study this question for unit-demand customers who know their own values for the possible items. Their 2021 paper identifies two conditions under which the best menu of opaque products earns at least as much as the best separate item prices.
The comparison matters because the opaque menu uses less item-specific pricing information. The seller gives every item one price and gives opaque products of equal size the same price. The theorem says that this constrained format can still match discriminatory pricing when the valuation law is symmetric and either customers assess opaque products pessimistically or valuations have only two levels. The paper also supplies counterexamples outside those conditions; the symmetry and customer-type hypotheses are substantive.
There are items. A customer has a nonnegative valuation vector , sampled from a probability law . A menu option has a price and a valuation. Its utility is valuation minus price. The customer buys one option of greatest utility when that utility is nonnegative. If several options have greatest utility, the customer buys one with the highest price. Remaining ties at the same price do not affect revenue. A customer may also buy nothing, yielding zero revenue.
In discriminatory pricing (DP), the seller assigns a nonnegative price to each item and offers only the individual items. Write for expected revenue and for its optimum over item-price vectors.
In opaque selling (OPQ), the seller offers the items at a common price and also offers every set of at least two items. A set of size costs , independent of which items it contains. A pessimistic customer values at ; a risk-neutral customer values it at . Both value a singleton at its item value. A customer is pessimistic with probability and risk-neutral with probability , independently of the valuation vector. The expected revenue of a price menu is ; its optimum is .
A law is exchangeable if permuting the coordinates of leaves its joint distribution unchanged. Coordinates may be correlated, and they need not be independent. A law is two-valued when there are real numbers such that almost every valuation vector has every coordinate in . This says the same pair applies to the entire vector, rather than allowing a different pair at each coordinate.
For exchangeable , nonnegative valuations, and , the target is
The first case covers any exchangeable law, including discrete laws with ties, when all customers are pessimistic. The second covers every mix of customer types when the valuations take two common values. Neither case requires independent item values. This mission retains both cases in one goal because that is Theorem 1 as stated in the paper.
The milestones trace the two cases. They identify the equal probabilities of valuation-order events, the value of the best opaque subset at a fixed size, the pessimistic dominance case, the three candidate DP price vectors under two values, the conditional revenue identity printed as display (1), the opaque price ladder's revenue for both customer types, and the two-valued dominance case. Each milestone is attached to a passage in the proof of Theorem 1.
The theorem gives a comparison of optimal revenues, not just a comparison of one chosen menu with one chosen price vector. For a seller with exchangeable valuations, it guarantees that size-based opaque prices can recover at least the revenue available from item-specific prices in either named regime. Outside those regimes, the paper's counterexamples prevent extending that guarantee merely by relaxing the hypotheses.
The result is proved in the cited paper; the goal here is a machine-checked version of its statement and proof. A formal development would establish the choice rule for finite menus, expectations for discrete and continuous valuation laws, permutation symmetry, finite order statistics, and the behavior of size-based menus at utility and price ties. These components are reusable in later formalizations of unit-demand pricing and opaque-product models. The present mission starts with unproved Lean theorem statements; compiling those statements does not certify the paper's argument.
One tempting argument treats the opaque menu as discriminatory pricing with the valuation order known to the seller. That comparison overlooks a restriction: the same price must be attached to each product size, so a price that is useful for the highest-valued item need not be useful for every realized ordering. The paper explicitly notes that the apparent information advantage alone would also suggest dominance in settings where dominance fails.
Ties create another obstacle. The probability formulas displayed for DP and OPQ in the selling-model section use inequalities that can count a tied purchase more than once. The paper sets aside ties for exposition in that section, yet the two-valued case necessarily has them. A faithful proof has to use the stated customer choice rule and the highest-price tie-break, rather than treating those displayed sums as definitions for discrete laws. The two-valued case also requires tracking how revenue changes with the number of high valuations, without assuming independent coordinates.
Items are represented by Fin N and valuation profiles by functions Fin N → ℝ; the paper's item indices start at one, while Lean's start at zero. The probability law is a measure on profiles with a probability-measure instance and almost-sure nonnegative coordinates. Exchangeability means invariance of this law under every coordinate permutation. Two-valued support is an almost-sure condition on the whole profile. No independence or density assumption is included.
The menu contains every nonempty item set. Singletons stand for the ordinary items at their common price; sets of equal larger size share an opaque price. All seller prices are nonnegative. Revenue is the highest price among options with maximal nonnegative utility, with zero when no option qualifies. This directly represents the rule on page 8, including discrete laws. The pessimistic valuation is a finite minimum and the risk-neutral valuation a finite average. Customer type is mixed independently of the valuation law, so the OPQ expectation is the -weighted sum of the two type-specific expectations.
Expected revenues and optimal revenues use extended nonnegative reals . The optima are suprema over nonnegative prices; existence of a maximizing price vector is not assumed. This avoids default values for an unbounded real supremum and records possible infinite revenue. Prices for unused cardinalities are nonnegative but have no effect on the menu. The order statistic sorts the coordinates with multiplicity; it is not defined through the subset identity it is meant to satisfy.
The goal is not implied by a degenerate model: the revenue function charges the highest price among utility maximizers and sells only at nonnegative utility; the optimal revenues range over nonnegative prices; exchangeability is invariance under every coordinate permutation. Contributions toward the finite-menu choice lemmas, permutation-invariant integration, order-statistic identity, two-valued DP structure, and the two cases are within scope.
ccd5b53ae01d607eca3b7df8549f418f52245b99bb2dfa050b6f5c4878a3cffe; its printed and PDF page numbers agree.Rewards-based crowdfunding platforms such as Kickstarter and Indiegogo let a creator pre-sell a product before it exists. Most backers cannot judge the product's quality from a campaign page, while some (experts, early adopters, people who have seen a prototype) can. A creator who knows her product is good therefore faces a classical signaling problem: how to convince the uninformed crowd without simply copying what a creator of a worse product could also do. Chakraborty and Swinney (SSRN 2885457, forthcoming in Manufacturing & Service Operations Management, doi:10.1287/msom.2019.0833) show that crowdfunding offers a signaling device absent from ordinary retail: the funding target of an all-or-nothing campaign. The paper sits in the signaling literature that starts with Spence (1973) and Milgrom and Roberts (1986), and uses the equilibrium refinement of Cho and Kreps (1987).
A creator of private type runs an all-or-nothing campaign whose reward is one unit of her product. Backers value the products at ; producing requires a fixed startup cost , with . The number of interested backers is , and , so success is uncertain for both types.
The creator chooses a design : a funding target (the funding constraint) and a reward price . A fraction of the backers is informed and pledges iff . The remaining fraction is uninformed: it sees only , forms a belief about the type and pledges iff does not exceed the believed valuation. If a share of the backers pledges, the campaign succeeds iff ; then the creator collects and pays , otherwise all pledges are refunded. The expected profit is (1):
A separating equilibrium is a pair of distinct designs such that, with the uninformed backers believing exactly at and at every other design, neither type gains from any feasible deviation; in particular the L-type does not gain by mimicking . It survives the intuitive criterion if no off-path design makes one type strictly better off when recognized, while making the other type strictly worse off under any belief. With
the paper's target is
For every , the designs and form a separating equilibrium that survives the intuitive criterion, and every separating equilibrium that survives the criterion has
Proposition 3 says that a high-quality creator signals by raising her funding target, accepting a lower chance of success, and never by lowering her price; signaling is free when the informed fraction is large (). In contrast with signaling by price alone (Proposition 2 of the paper), a separating equilibrium always exists. The closed form is what the paper's later results build on, notably the endogenous quality choice of Proposition 5.
The result is proved in the paper's Online Supplement by calculus and case analysis. As far as is known, no part of it has been machine-checked. A formalization verifies the equilibrium characterization, including the boundary cases the printed proof treats in a sentence (uniqueness fails at , ), and gives a reusable model of all-or-nothing campaigns with a uniform crowd.
The algebra of each step is elementary. The difficulty lies in the equilibrium argument. Showing that the given pair is an equilibrium requires bounding the H-type's profit at every design believed to be low quality, including prices at or below , where the informed and uninformed backers both pledge. The paper checks only the deviation to . The characterization requires turning the intuitive criterion into a maximization of the H-type's profit over the mimicking-proof designs and showing that is its unique maximizer. A natural first idea, to fix and lower the price until mimicking stops (Proposition 2's equilibrium), does not give the maximizer: along raising the target pays more than lowering the price.
Real.sqrt algebra, monotonicity along a curve. All of it is in Mathlib; the model definitions are new. Proofs of any milestone are welcome, and so are alternative proofs of the goal that avoid the derivative.Firms that moved production offshore for low unit costs pay for it in lead time: a slow global supplier forces large safety stocks, and the cost of those stocks grows with demand variability. A recurring question in operations management is when it pays to re-shore part of production to a fast, local, more expensive plant. Adidas's "SpeedFactories" are the example that gives this paper its name. Boute, Disney, Gijsbrechts and Van Mieghem (accepted manuscript, 2020; Management Science 2022) answer this for a linear dual-sourcing policy. Their analysis yields an explicit break-even price for the off-shore supplier, together with a condition under which a small local plant that absorbs only demand variability beats full off-shoring, even when local production costs more per unit than off-shore purchasing.
The dual-sourcing literature (Whittemore and Saunders 1977; Song and Zipkin 2009; Janakiraman, Seshadri and Sheopuri 2015) shows that optimal dual-sourcing policies have no simple structure for general lead times. Xin and Goldberg (2018) proved that tailored base-surge (TBS) policies are asymptotically optimal as the global lead time grows. The present paper combines TBS with a smoothing local replenishment rule and prices the local capacity explicitly.
A firm serves demand , , from finished-goods inventory ; excess demand is backlogged. The demands are independent and identically distributed , where is the standard deviation. Holding costs and backlog costs per unit and period: .
Two sources replenish the inventory:
The TBS-POUT policy with allocation and smoothing parameter orders the constant globally and
locally, where is the safety stock. The inventory evolves by . The long-run average cost is . The optimized dual-sourcing cost is its infimum over .
The benchmark is full off-shoring with the order-up-to policy: order with inventory . Its optimized long-run cost over is .
With the standard normal density and distribution function, and . The paper's standard deviations are
and the break-even price (20) is
If
then is concave on and whenever . Otherwise is convex on , and whenever for some , the allocation is the unique minimizer of on and beats . The smoothing parameter is fixed and arbitrary in .
Proposition 4 is the paper's strategic prescription. It splits the parameter space by one dimensionless product of a financial factor, a variability factor and a service/flexibility factor. On one side, a small SpeedFactory serving only the demand variability is profitable in a price band below the local unit cost. On the other side, re-shoring is all-or-nothing. Since grows like while do not depend on , long off-shore lead times push towards the first regime (Figure 6 of the paper: concave at , convex at ).
The printed proof of Proposition 4 is a single sentence ("readily obtained from the second derivative of "). The content is in the chain behind it: the inventory under TBS-POUT is an AR(1) process, two Gaussian newsvendor problems give its optimal cost, and the order-up-to benchmark has inventory variance . Formalizing the mission machine-checks that chain from the dynamics to the strategic conclusion. None of these results is formalized anywhere to our knowledge. Reusable outputs include the variance of a linear filter of iid noise, the Gaussian newsvendor minimization, and the long-run cost of the order-up-to policy under iid normal demand.
Once the closed forms (13) and (18) are known, the goal is algebra: with , and (21) is equivalent to . The work is in reaching (13) and (18) from the dynamics:
Taking (13) and (18) as definitions would skip all of this and is ruled out.
Lean namespace SpeedFactory.BreakEven, two definition files and eight theorem statements.
d : ℕ → Ω → ℝ on a probability space, mutually independent, each with law gaussianReal μ (σ²). Periods start at ; d 0 is unused. Independence is assumed, although the printed propositions say "identically, normally distributed": (14), and §5 all need it.IsLeast) and unique minimizers, so no junk value of sInf or liminf can make a statement true by accident. The critical fractiles are computed from the quantile, not left free.Contributions welcome: proofs of the milestones, in particular a general Gaussian newsvendor lemma and the AR(1) variance recursion, which are reusable beyond this mission.
Online marketplaces such as Airbnb, Upwork and eBay match buyers and sellers but do not set transaction prices. They earn revenue through commissions (a fraction of the transaction price) and subscription fees (a fixed charge per transaction), and they often differentiate these fees by participant type. Prices then form endogenously, as a competitive equilibrium of the market the fees induce. Choosing revenue-maximizing fees is therefore a bilevel problem: the platform optimizes over fees, and every choice of fees changes the equilibrium prices and trades. Birge, Candogan, Chen and Saban (SSRN 3259716; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2019.0853) show that, despite its nonconvexity, this problem is solved exactly by a convex program, and they characterize all optimal fee profiles. The rest of their paper, which compares commissions with subscriptions and studies how the network shapes revenue, rests on this result.
There are finitely many seller types and buyer types . A bipartite compatibility network says which types can trade; every type has degree at least one. Type consists of a continuum of sellers of mass , and type of buyers of mass . A type- buyer's value is distributed according to on , and a type- seller's reservation value according to on , with . A buyer who trades with a type- seller incurs a disutility . Assumption 1 asks that each be continuous, continuously differentiable and strictly increasing on , with bounded mean. Its inverse is .
The platform picks commissions and subscriptions in : and . A competitive equilibrium consists of prices , flows on and supplies and demands with
markets clearing (, ), and buyers trading only with their cheapest compatible sellers. The revenue problem (3) is
Assumption 2 asks that and be strictly concave in , a regularity condition on both sides of the market. The relaxation (7) is
over flows on with marginals , and .
Let be an optimal solution of (7). Then (i)
and every optimal solution of (3) has supply-demand vector . (ii) For with , with , , and , the pair is optimal if and only if some and some optimal flow of (7) solve the linear system (8a)–(8f).
In the order the proof uses them:
The result turns a nonconvex bilevel problem into a convex network-flow problem with separable concave objective: the optimal supply-demand vector is computed without reference to fees or prices. Part (ii) describes the whole set of optimal fees as solutions of a linear feasibility system, which is what the paper uses to compare fee structures: a subscription-only profile is always optimal (Step (i-2)), and the comparisons with homogeneous and one-sided fees (Propositions 4–6) and the analysis of which network positions earn surplus (Theorems 2–3) start from it. No machine-checked version of these results exists on the platform. The mission formalizes the statement chain of the paper's proof (main text and e-companion), including the equilibrium existence and uniqueness of Proposition 1 and the KKT theory of the relaxation.
The bound is a rearrangement. Equality needs an equilibrium that realizes the optimum of (7), and the natural candidate prices are the dual variables of (7). These need not exist with finite values in general: the objective pieces and can have infinite slope at the boundary, for instance for unbounded supports. The proof therefore needs the boundary-slope facts of Lemma EC.1(ii) and a "special" KKT system in derivative form. Proposition 1 needs its own convex program for the equilibrium and is the deepest milestone. In part (ii) the optimal flow of (7) is not unique, so necessity has to use the flow of the equilibrium, not a fixed optimal flow.
Types are arbitrary finite types; flows are functions whose values off are never read. The upper end of each support is in WithTop ℝ, and is defined from . The standing assumptions of pp. 7–8 (positive masses, , degree at least one, each a continuous CDF extended to ) are explicit hypotheses. Two conventions concern unbounded supports, where . The feasible set of (7) requires when , since the paper's objective is at . For the same sellers, Assumption 2 is posed on ; on with a finite stand-in value it would be unsatisfiable. "Optimal solutions exist" is stated as attainment (IsGreatest). An optimal fee pair is one for which some equilibrium attains . Slopes , are limits of derivatives from inside the interval (footnote 22). Proposition EC.1 is posed only at the instance (7); the general framework problem (EC.1) is not formalized.
Theorem 1(ii) is stated with an optimal flow of (7), because the printed version with the fixed is false when optimal flows are not unique. The sentence "the optimal commission-subscription vector is not unique" is not posed. Ruled out as trivializing: defining the revenue of an equilibrium as instead of (3a); reading "optimal solutions exist" as an unattained supremum; an equilibrium without the buyers' minimum in (2b) or the cheapest-seller restriction (2d); a feasible set of (7) that admits for unbounded sellers at a finite junk cost; and an Assumption 2 that no unbounded seller distribution satisfies.
A complete development needs basic facts on generalized inverses of continuous CDFs, existence and KKT theory for separable concave maximization over a flow polytope (not in Mathlib), and equilibrium existence for Proposition 1. The concave-programming layer is reusable beyond this mission. Proofs of individual milestones, and sanity checks such as uniform or exponential markets, are welcome. The paper's proofs are in its e-companion, which is part of the cited SSRN file (EC.1.1, pp. ec2–ec6; EC.2.1; EC.3.1, pp. ec38–ec44).
Portfolio selection uses observed asset returns to choose weights that balance expected return against variability. Estimates of both quantities can change sharply when the historical sample changes. A distributionally robust model addresses this uncertainty by allowing the return law to vary around the empirical law, then judging a portfolio by its worst variance and worst expected return. In the model of Blanchet, Chen, and Zhou, the allowed laws form a ball defined by an optimal transportation cost. Theorem 1 asks whether this optimization over probability laws can be expressed using only the sample and a norm of the portfolio weights.
The paper presents this equivalence as its first main contribution. Its later sections use statistical assumptions on a return time series to guide the choice of the ball radius and the return target. This mission concerns the finite-sample equivalence itself; those statistical choices are separate results. The distinction matters because the equivalence holds for a given nonnegative radius and target, without imposing a model for how the observations were generated. Theorem 1 and §3 of the preprint make these two roles explicit.
There are assets and observed return vectors . A portfolio is a vector whose weights sum to one. Its return when the asset return vector is is . The empirical law is , so empirical expectations and variances use the population normalization . No independence assumption is needed for this finite-sample problem.
Fix and its Hölder conjugate , so . The endpoint , is included. Moving a return vector to costs . For two probability laws , the transportation cost is the infimum of expected over joint laws whose first marginal is and second marginal is . With radius , the ambiguity set is
For target return , the feasible region contains portfolios whose weights sum to one and whose expected return under every is at least . This is the paper's worst-case mean condition. For any such portfolio, the robust objective is the supremum of over the same ambiguity set. These objects are defined in §§1–2.2 of the preprint.
Proposition 1 identifies the minimum expected return over the ball:
Proposition 3 evaluates the maximum second moment subject to a specified mean . Write , , and . When , its value is
The two displayed steps in the proof of Theorem 1 connect this constrained value to the unconstrained worst variance: , whose maximum over allowed is and is attained at . These milestones retain the paper's constants, feasibility range, and attainment claims. Propositions 1 and 3 and the proof of Theorem 1 give the source statements.
Theorem 1 is the goal. It says that the robust problem (2) and the empirical problem (9) have both the same optimal portfolios and the same optimal value:
The statement also equates the minimizer sets, rather than equating values alone. The paper calls (9) the dual problem; here that name denotes this regularized empirical optimization problem. Theorem 1, p. 6 is the pinned target.
The theorem replaces an optimization over probability laws with a finite-dimensional portfolio objective containing a norm penalty. It gives a precise interpretation of that penalty: its size and exponent follow from the Wasserstein radius and transport norm. It also preserves which portfolios are optimal, so the reformulation supports the portfolio decision itself, not only its reported objective value. The target-return constraint still depends on the worst expected return; Proposition 1 gives its explicit empirical form. These consequences are stated in §2.2 of the preprint.
A complete formalization would establish the finite-sample equivalence and the attained extrema that underlie it. It would also supply reusable results about finite empirical measures, transport balls with quadratic norm costs, and portfolio moments under those balls. The pinned results are proved in the paper; the work here is to give their statements and proofs in Lean under a shared, audited model. The current local proposal consists of statements with proof placeholders, not machine-checked proofs of those results.
The adversary changes the whole probability law, while the robust objective subtracts the square of the law's own mean from its second moment. Maximizing the second moment alone does not therefore give the worst variance. The mean constraint in Proposition 3 and the subsequent optimization over are essential to recovering the centered objective. Attainment also matters: the paper states minima and maxima, whereas a bound on an infimum or supremum would be weaker. At the level of Lean definitions, every law in the quadratic transport ball must have sufficiently integrable portfolio returns for the real moment formulas to express the paper's quantities. These are the central obligations of §2.2 and Appendices A–C.
Return vectors and weights are functions Fin d → ℝ; the sample is indexed by Fin n with . Exponents are extended nonnegative reals to include , while is finite as in the paper's fixed real exponent. The cost takes values in , and the reused transport definition fixes both coupling marginals. The ambiguity set contains all probability laws within the cost radius, with no added moment restriction. The portfolio moments are real Bochner integrals. Showing that the quadratic-cost ball makes these integrals meaningful is part of proving the results.
The robust variance objective uses an extended-real supremum. This represents an empty or unbounded indexing set without the default value of a real supremum. The feasible mean constraint is written as a universal lower bound over the ball, matching the paper's minimum constraint. The goal compares both minimizer sets and infimum values on that feasible region. It cannot be discharged by defining the robust objective to equal the regularized formula, narrowing the ambiguity set, or assuming the desired moment and value identities. Proposition 1 and Proposition 3 retain attainment through IsLeast and IsGreatest.
This mission covers the finite-sample reformulation in §§1–2.2. The time-series assumptions A1–A3, the data-driven choices of and in §3, Theorem 2, and Proposition 4 are outside its scope. Contributions on transport-ball integrability, the two attained extrema, the scalar maximization, and the final equivalence would all support the goal. The general-cost dual formula of Proposition 2 is omitted because the printed formulation has a boundary counterexample at ; a faithful version needs a separate audit of its duality hypotheses.
A seller with one item and several buyers whose values are private but drawn from known, independent distributions can maximize expected revenue with Myerson's optimal auction (Myerson, 1981). That auction depends on every distribution through virtual values, asks buyers to report their values, and allocates through a computation that buyers must trust. A sequential posted-price (SPP) mechanism is far simpler: the seller fixes one take-it-or-leave-it price per buyer and approaches the buyers one at a time. Posted prices are common in practice, and no buyer reports anything. The natural question is how much revenue this simplicity costs, measured as the worst-case ratio between the best SPP revenue and the optimal revenue.
Timeline. Chawla, Hartline, Malec and Sivan (2010) showed that sequential posted prices earn at least of the optimal revenue in the single-unit setting with independent buyers. Azar, Chiplunkar and Kaplan (2018) improved this to for , which gave the best universal bound before the present paper. No SPP mechanism can guarantee more than about even for i.i.d. values (Hill and Kertz, 1982; Correa et al., 2017). Beyhaghi, Golrezaei, Paes Leme, Pál and Sivan (Operations Research, 2021; arXiv:1807.03435) proved the universal bound , valid for every , together with -dependent, multi-unit and matroid results and a bound of for eager second-price auctions. This mission formalizes their single-unit universal bound.
There are buyers . Buyer has a value drawn from a probability distribution on , independently across buyers; the profile has law .
SPP. Given prices , the mechanism approaches buyers in decreasing order of price, offers to buyer while the item is unsold, and sells to the first buyer with at price . Its revenue at the profile is therefore (zero if nobody accepts), and denotes its expectation.
Threshold mechanisms (the benchmark). By the taxation principle (Lemma 1 of the paper, cited from Nisan et al.), a deterministic truthful mechanism is described by thresholds depending only on the other buyers' values: buyer wins and pays when . In the single-unit setting, almost surely at most one buyer weakly exceeds their threshold. The expected revenue is . Define
so that (Equation (1)).
Two pricing rules. Myersonian prices post to buyer the threshold computed on an independent re-sample of the other buyers' values, freshly for each ; MP is the resulting expected revenue and the probability that some buyer has . The uniform price rule posts the same price to everyone; .
The factor-revealing program (FR). With ,
For every , every independent value distributions and every single-unit threshold mechanism with finite expected revenue , there is a vector of nonnegative prices with
The prices depend on the instance; the constant does not.
The intermediate statement , the "best of Myersonian and uniform" form shown first in the proof, is context only: Theorem 1 asserts one deterministic price vector, and that is the goal.
The result. Theorem 1 was the first improvement over for single-unit posted pricing that holds for every number of buyers and for arbitrary (regular or irregular) independent distributions. It quantifies the price of simplicity of posted pricing against the optimal auction, and its method (two pricing rules, each giving one constraint on the revenue curve , and a factor-revealing program over all curves meeting both) is reused in the paper for -dependent, multi-unit, position-auction and eager second-price bounds.
Formalizing it. The result is proved on paper; no machine-checked version exists. A formalization checks the probabilistic core, the solution of an infinite-dimensional program, and the numerical constants. The printed constants carry rounding slips ( is a rounding of ; , printed as ), which the milestones state precisely. The paper's normalization silently assumes that Opt is finite; the formal statement makes that hypothesis explicit.
The Myersonian rule alone gives only , and the paper's example (values uniform on ) shows this is tight for it; the uniform rule alone is also bounded away from 1. The improvement comes only from combining them, and the combination is expressed as an optimization over all decreasing curves : the step that the obvious argument misses is the exact solution of (FR), whose optimum must be guessed and certified for an infinite-dimensional program with a nonlinear constraint. The probabilistic step is subtle as well: the true thresholds are correlated across buyers, and Lemma 2 holds only for the independently re-sampled . Finally, the theorem claims a single deterministic price vector, so the random Myersonian prices and a possibly unattained best uniform price must both be converted into one concrete , with the slack between and absorbing the approximation.
Buyers are Fin n; values have law Measure.pi μ with each μ i a probability measure on ℝ; values need not be nonnegative. Revenues and probabilities are in ℝ≥0∞ (lower Lebesgue integrals and measures), never Bochner integrals, so that a non-integrable revenue cannot become a junk zero. The SPP revenue at a profile is the closed form of the price-ordered sale. A threshold mechanism is a family t i v with t i measurable, nonnegative, independent of coordinate i, and almost surely at most one buyer with t i v ≤ v i. Myersonian prices are read from a fresh copy of the whole profile per buyer, independent of everything else. In (FR) the constraint is encoded as and .
Benchmark. The goal is stated for every single-unit threshold mechanism, which is the taxation-principle form of Lemma 1; for the optimal mechanism's thresholds it is the printed theorem, and the paper's proof never uses optimality. Lemma 1 and Myerson's theorem are cited by the paper and are not part of the mission. The one added hypothesis on the goal, finiteness of Opt, is necessary: without it some single-unit threshold mechanisms have infinite revenue while every posted-price revenue is finite.
Ruled out. The SPP revenue is the revenue of the actual sequential sale, not a free function; thresholds may not depend on the buyer's own value (that would allow full surplus extraction) and must be single-unit feasible (otherwise Opt could be times any posted-price revenue); the constant is the explicit , not an existential one.
Out of scope. Theorem 2 (-dependent bounds), Theorem 3 and Lemmas 3–4 (multi-unit), Lemmas 5–7 and Theorem 4 (position auctions), the partition-matroid claim and Proposition 1 (matroids), Lemma 8 and Theorems 5–6 (eager second-price auctions), Inequality (6) of Lemma 2, the illustration of §4.1, and the numerical tables.
Infrastructure. The development needs the layer-cake formula for lower integrals, independence under product measures, the AM–GM inequality and , all in Mathlib, plus a numerical certificate for the root of a transcendental equation. The threshold-mechanism and SPP definitions are reusable for the multi-unit and matroid results of the same paper. Proofs of any milestone, alternative arguments, and sharper constants are welcome.
Online matching platforms (labor platforms such as Upwork or TaskRabbit, dating sites, short-term rental platforms) make it cheap to contact potential partners, but not cheap to find one who is still available. A worker who has already accepted a job, or a listing that is already booked, keeps receiving applications and keeps being screened. Arnosti, Johari and Kanoria, Managing Congestion in Matching Markets (M&SOM 23(3):620–636, 2021), build a stochastic game-theoretic model of this effect, in which applicants pay to apply and employers pay to screen, and employers cannot see which applicants have already matched. They prove that the model has a unique equilibrium, compute both sides' welfare in it in closed form, and use the formulas to evaluate platform interventions (application limits, application fees, a market-wide wage).
This mission formalizes the equilibrium characterization: the closed-form equilibrium welfare of Theorem 2, together with the existence and uniqueness results (Proposition 2, Theorem 1) and the identities from the paper's endnotes that connect them.
A market has four parameters: , the number of applicants per employer; , the probability that an applicant is qualified for a given employer; , the cost of one application; and , the cost of screening one applicant. Throughout, Assumption 1 holds: . Write .
Applicants choose an application intensity : an applicant sends a Poisson() number of applications, each of which becomes an offer independently with probability , the acceptance probability. The applicant takes the first offer, so the expected payoff is
maximized by the applicant best response
Employers receive a Poisson() number of applications. Each applicant is qualified with probability and still available with probability . An employer either screens sequentially until it hires (screening probability ) or exits. The employer best-response correspondence is
and the employer payoff is (5).
With (), the consistency conditions are
A solution is a mean-field steady state of the strategies . A mean-field equilibrium (MFE) is a pair with a steady state such that and (Definition 1). Equilibrium welfare is and .
There are unique with
the MFE is unique, and in it
The theorem is exact; it has no constants to improve.
Theorem 2 reduces equilibrium welfare on both sides to one scalar, , and splits markets into two regimes (Definition 2): application-limited (; all employers screen; applicants compete in a "tragedy of the commons") and screening-limited (; employers are indifferent and their welfare is zero, by (14) and (16)). All of the paper's later results, including the welfare bounds of Theorem 3, the effect of application limits (Theorems 4–5), application costs (Theorem 6) and wages (Theorem 7), are computed from these formulas.
Proposition 2, Theorem 1 and Theorem 2 are stated in the article but their proofs are in a technical report (Arnosti, Johari, Kanoria 2019, SSRN), not reproduced in the article and not used here. To our knowledge none of these results has a machine-checked proof. A formal development would give a self-contained, checked proof of the equilibrium characterization from the article's definitions alone.
The welfare identities (15)–(16) are algebra once and are known. The root statements are one-variable analysis. The hard part is the equilibrium itself. Proposition 2 is a fixed-point problem: substituting (7) into (6) gives an increasing map , and an increasing map can have several fixed points, so a monotonicity argument alone does not give uniqueness. Theorem 1 then has to handle the correspondence : an equilibrium may sit at the kink with an interior , and the case analysis has to show that exactly one of the regimes , applies and that it pins down .
All objects live in the namespace MatchCongestion.Welfare, over ℝ. The conventions are:
Params.Standing is Assumption 1 together with , , , , which the paper uses without listing them ("costs", a probability). Without , (14) has no root above .IsMFE instead asks for some steady state ; by Proposition 2 the two readings agree.Set ℝ.Real.log.Several formalizations would make the goal trivial or false, and none is used:
(1 - exp (-x)) / x in (6)–(7) would make a spurious second equilibrium;Classical.choose, or in Definition 1, would leave junk values unconstrained;Proposition 1 (the employer's sequential screening problem, specified only in an online appendix), the application-limit model (8)–(9) with Proposition 3, Theorems 3–7 and the finite-system limit theorems 8–10 are out of scope. Contributions of independent interest are a general lemma on unique roots of strictly convex or concave one-variable functions on an interval, and analytic facts about (positivity, strict monotonicity, on ).