On Shor's channel extension and constrained channelsResearch Paper
Motivation
In this paper we give several equivalent formulations of the additivity conjecture for constrained channels, which formally is substantially stronger than the unconstrained additivity. To this end a characteristic property of the optimal ensemble for such a channel is derived, generalizing the maximal distance property. It is shown that the additivity conjecture for constrained channels holds true for certain nontrivial classes of channels. Recently P. Shor showed that conjectured additivity properties for several quantum information quantities are in fact equivalent. After giving an algebraic formulation for the Shor's channel extension, its main asymptotic property is proved. It is then used to show that additivity for two constrained channels can be reduced to the same problem for unconstrained channels, and hence, "global" additivity for channels with arbitrary constraints is equivalent to additivity without constraints.
This mission is the statement-level formalization of On Shor's channel extension and constrained channels (arXiv:quant-ph/0306196v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2: constrained versus asymptotic extension additivity (Theorem 2: constrained versus asymptotic extension additivity, PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Continuity bounds on the quantum relative entropyResearch Paper
Motivation
The quantum relative entropy is frequently used as a distance, or distinguishability measure between two quantum states. In this paper we study the relation between this measure and a number of other measures used for that purpose, including the trace norm distance. More precisely, we derive lower and upper bounds on the relative entropy in terms of various distance measures for the difference of the states based on unitarily invariant norms. The upper bounds can be considered as statements of continuity of the relative entropy distance in the sense of Fannes. We employ methods from optimisation theory to obtain bounds that are as sharp as possible.
This mission is the statement-level formalization of Continuity bounds on the quantum relative entropy (arXiv:quant-ph/0503218v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
25 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §VI, Theorem 4: sharp lower bound for every UI norm (seed headline) (§VI, Theorem 4: sharp lower bound for every UI norm (seed headline), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
4 results of the paper are not stated yet, because the library lacks an interface they need:
§V.B, Theorem 3: printed logarithmic continuity bound (deferred): A corrected Fannes modulus or a source-justified local distance domain for the logarithmic continuity bound; the unrestricted printed inequality cannot be asserted. (source-ambiguity)
§VII.A, unnumbered printed series (48) (deferred): A corrected Taylor series for (46): powers beta^(k-1) and (1-beta)^(k-1), with a plus (-1)^k term. The independently valid leading coefficient is already stated. (source-ambiguity)
§VII.B, Theorem 6: complete bound plus fixed-dimension sharpness wording (deferred): An exact fixed-dimension, fixed-actual-minimum sharpness domain, including the residual-eigenvalue condition, or a corrected dimension-independent sharpness claim. (source-ambiguity)
§VIII, Theorem 7: full asymptotic statement (converse deferred): A support-reducing/invariance hypothesis with an audited converse, or a bound using the minimum positive eigenvalue of the full sigma_n instead of its compression. (source-ambiguity)
Strong Converse and Stein's Lemma in the Quantum Hypothesis TestingResearch Paper
Motivation
The hypothesis testing problem of two quantum states is treated. We show a new inequality between the error of the first kind and the second kind, which complements the result of Hiai and Petz to establish the quantum version of Stein's lemma. The inequality is also used to show a bound on the first kind error when the power exponent for the second kind error exceeds the quantum relative entropy, and the bound yields the strong converse in the quantum hypothesis testing. Finally, we discuss the relation between the bound and the power exponent derived by Han and Kobayashi in the classical hypothesis testing.
This mission is the statement-level formalization of Strong Converse and Stein's Lemma in the Quantum Hypothesis Testing (arXiv:quant-ph/9906090v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quantum Stein lemma at every fixed positive error (§3, Theorem 2, (10): quantum Stein lemma, corrected positive-error domain, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
1 results of the paper are not stated yet, because the library lacks an interface they need:
§5, unnumbered quantum variational identity and Golden–Thompson comparison: A source-specified quantum active-rate attainment domain, singular-state log-exponential convention, and nonzero-order equality-case domain for the combined p.8 identity. (source-ambiguity)
We consider quantum channels with one sender and two receivers, used in several different ways for the simultaneous transmission of independent messages. We begin by extending the technique of superposition coding to quantum channels with a classical input to give a general achievable region. We also give outer bounds to the capacity regions for various special cases from the classical literature and prove that superposition coding is optimal for a class of channels. We then consider extensions of superposition coding for channels with a quantum input, where some of the messages transmitted are quantum instead of classical, in the sense that the parties establish bipartite or tripartite GHZ entanglement. We conclude by using state merging to give achievable rates for establishing bipartite entanglement between different pairs of parties with the assistance of free classical communication.
This mission is the statement-level formalization of Quantum broadcast channels (arXiv:quant-ph/0603098v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 and its explicit nonregularization limitation (seed paper result) (Theorem 1 and its explicit nonregularization limitation (seed paper result), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
5 results of the paper are not stated yet, because the library lacks an interface they need:
Unnumbered remark: regularized two-EPR capacity formula: Capacity converse and zero-resource completion of the regularized two-EPR witness union (source-ambiguity)
Appendix A unnumbered result: support reduction preserving all three information quantities: A true same-finite-T support-reduction assertion preserving all three information quantities (source-ambiguity)
Properties of Conjugate Channels with Applications to Additivity and MultiplicativityResearch Paper
Motivation
Quantum channels can be described via a unitary coupling of system and environment, followed by a trace over the environment state space. Taking the trace instead over the system state space produces a different mapping which we call the conjugate channel. We explore the properties of conjugate channels and describe several different methods of construction. In general, conjugate channels map M_d to M_d' with d < d', and different constructions may differ by conjugation with a partial isometry. We show that a channel and its conjugate have the same minimal output entropy and maximal output p-norm. It then follows that the additivity and multiplicativity conjectures for these measures of optimal output purity hold for a product of channels if and only if they also hold for the product of their conjugates. This allows us to reduce these conjectures to the special case of maps taking M_d to M_d' with a minimal representation of dimension at most d. We find explicit expressions for the conjugates for a number of well-known examples, including entanglement-breaking channels, unital qubit channels, the depolarizing channel, and a subclass of random unitary channels. For the entanglement-breaking channels, channels this yields a new class of channels for which additivity and multiplicativity of optimal output purity can be established. For random unitary channels using the generalized Pauli matrices, we obtain a new formulation of the multiplicativity conjecture. The conjugate of the completely noisy channel plays a special role and suggests a mechanism for using noise to transmit information.
This mission is the statement-level formalization of Properties of Conjugate Channels with Applications to Additivity and Multiplicativity (arXiv:quant-ph/0509126v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
30 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 / paper headline: conjugation preserves multiplicativity and entropy additivity (Theorem 5 / paper headline: conjugation preserves multiplicativity and entropy additivity, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
17 results of the paper are not stated yet, because the library lacks an interface they need:
Corollary 11: filtered noisy complement for Pauli-diagonal channels: A consistent full source statement: Corollary 11: filtered noisy complement for Pauli-diagonal channels (source-ambiguity)
Theorem 14: explicit shift-clock formula (58): A consistent full source statement: Theorem 14: explicit shift-clock formula (58) (source-ambiguity)
Theorem 15: additional equality/decomposability assertion: A consistent full source statement: Theorem 15: additional equality/decomposability assertion (source-ambiguity)
Theorem 16: subgroup/coset equality characterization: A consistent full source statement: Theorem 16: subgroup/coset equality characterization (source-ambiguity)
Theorem 18 (Stinespring): cited general C-star dilation theorem: A consistent full source statement: Theorem 18 (Stinespring): cited general C-star dilation theorem (source-ambiguity)
Unnumbered CQ extremality claim (cited [16]): A consistent full source statement: Unnumbered CQ extremality claim (cited [16]) (source-ambiguity)
Unnumbered formulas (37)–(40): diagonal Weyl action: A consistent full source statement: Unnumbered formulas (37)–(40): diagonal Weyl action (source-ambiguity)
Unnumbered cyclic axis-state formula (46)–(47): A consistent full source statement: Unnumbered cyclic axis-state formula (46)–(47) (source-ambiguity)
Example 1: composite-dimensional decomposable image: A consistent full source statement: Example 1: composite-dimensional decomposable image (source-ambiguity)
Example 2: eight-label support and formula (49): A consistent full source statement: Example 2: eight-label support and formula (49) (source-ambiguity)
Example 3: combinations of axis QC channels: A consistent full source statement: Example 3: combinations of axis QC channels (source-ambiguity)
Unnumbered: Pauli support subgroups determine block decompositions: A consistent full source statement: Unnumbered: Pauli support subgroups determine block decompositions (source-ambiguity)
Unnumbered corollary (59): set representation of the pure image: A consistent full source statement: Unnumbered corollary (59): set representation of the pure image (source-ambiguity)
Example 5: depolarizing bound attainment and product nonattainment: A consistent full source statement: Example 5: depolarizing bound attainment and product nonattainment (source-ambiguity)
Unnumbered appendix claim: strict product-bound nonattainment: A consistent full source statement: Unnumbered appendix claim: strict product-bound nonattainment (source-ambiguity)
Unnumbered appendix classification and Bell/product comparison: A consistent full source statement: Unnumbered appendix classification and Bell/product comparison (source-ambiguity)
Example 6: basis dependence of decomposability: A consistent full source statement: Example 6: basis dependence of decomposability (source-ambiguity)
Monogamy of entanglement and other correlationsResearch Paper
Motivation
It has been observed by numerous authors that a quantum system being entangled with another one limits its possible entanglement with a third system: this has been dubbed the "monogamous nature of entanglement". In this paper we present a simple identity which captures the trade-off between entanglement and classical correlation, which can be used to derive rigorous monogamy relations. We also prove various other trade-offs of a monogamy nature for other entanglement measures and secret and total correlation measures.
This mission is the statement-level formalization of Monogamy of entanglement and other correlations (arXiv:quant-ph/0310037v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1, Eqs. (2)–(3): complementarity of entanglement and classical correlation (Theorem 1, Eqs. (2)–(3): complementarity of entanglement and classical correlation, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
1 results of the paper are not stated yet, because the library lacks an interface they need:
Section III: two-way secret-key sandwich: Operational two-way public-discussion secret-key capacity on finite tripartite states with evaluated Eve-plus-transcript security and arbitrary private local memory. (hard)
On Quantum Fidelities and Channel CapacitiesResearch Paper
Motivation
We show the equivalence of two different notions of quantum channel capacity: that which uses the entanglement fidelity as its criterion of success in transmission, and that which uses the minimum fidelity of pure states in a subspace of the input Hilbert space as its criterion. As a corollary, any source with entropy rate less than the capacity may be transmitted with high entanglement fidelity. We also show that a restricted class of encodings is sufficient to transmit any quantum source which may be transmitted on a given channel. This enables us to simplify a known upper bound for the channel capacity. It also enables us to show that the availability of an auxiliary classical channel from encoder to decoder does not increase the quantum capacity.
This mission is the statement-level formalization of On Quantum Fidelities and Channel Capacities (arXiv:quant-ph/9809010v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
23 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entanglement and minimum-subspace capacities coincide (Abstract; Theorem 1 and Corollary 1, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
2 results of the paper are not stated yet, because the library lacks an interface they need:
Lemma 3, Eq.(29): A correct source-specified sequential-fidelity estimate replacing the false printed 2 eta bound. (source-ambiguity)
Lemma 4, Eq.(35): A correct source-specified two-output squared-fidelity bound replacing the false 1-epsilon1-epsilon2 estimate. (source-ambiguity)
Majorization theory approach to the Gaussian channel minimum entropy conjectureResearch Paper
Motivation
A longstanding open problem in quantum information theory is to find the classical capacity of an optical communication link, modeled as a Gaussian bosonic channel. It has been conjectured that this capacity is achieved by a random coding of coherent states using an isotropic Gaussian distribution in phase space. We show that proving a Gaussian minimum entropy conjecture for a quantum-limited amplifier is actually sufficient to confirm this capacity conjecture, and we provide a strong argument towards this proof by exploiting a connection between quantum entanglement and majorization theory.
This mission is the statement-level formalization of Majorization theory approach to the Gaussian channel minimum entropy conjecture (arXiv:1111.1986v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Single-use reduction: C1 iff C2 iff C3; C4 is sufficient (C1–C4; Appendix 1, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
2 results of the paper are not stated yet, because the library lacks an interface they need:
Infinitesimal two-mode squeezer, (6),(8)–(9): A quantified exact infinitesimal majorization statement with a controlled approximation remainder (source-ambiguity)
(16)–(17), Appendix 4d, A.34–A.50: A consistent explicit positive row-subunital, column-stochastic beta-function kernel for general k (source-ambiguity)
Selected references
Majorization theory approach to the Gaussian channel minimum entropy conjecture, arXiv:1111.1986v1, https://arxiv.org/abs/1111.1986v1
Multipartite quantum correlations and local recoverabilityResearch Paper
Motivation
Characterizing genuine multipartite quantum correlations in quantum physical systems has historically been a challenging problem in quantum information theory. More recently however, the total correlation or multipartite information measure has been helpful in accomplishing this goal, especially with the multipartite symmetric quantum (MSQ) discord [Piani et al., Phys. Rev. Lett. 100, 090502, 2008] and the conditional entanglement of multipartite information (CEMI) [Yang et al., Phys. Rev. Lett. 101, 140501, 2008]. Here we apply a recent and significant improvement of strong subadditivity of quantum entropy [Fawzi and Renner, arXiv:1410.0664] in order to develop these quantities further. In particular, we prove that the MSQ discord is nearly equal to zero if and only if the multipartite state for which it is evaluated is approximately locally recoverable after performing measurements on each of its systems. Furthermore, we prove that the CEMI is a faithful entanglement measure, i.e., it vanishes if and only if the multipartite state for which it is evaluated is a fully separable state. Along the way we provide an operational interpretation of the MSQ discord in terms of the partial state distribution protocol, which in turn, as a special case, gives an interpretation for the original discord quantity. Finally, we prove an inequality that could potentially improve upon the Fawzi-Renner inequality in the multipartite context, but it remains an open question to determine whether this is so.
This mission is the statement-level formalization of Multipartite quantum correlations and local recoverability (arXiv:1412.0333v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §2, (2.1); §3: local recoverability from the multipartite information gap (§2, (2.1); §3: local recoverability from the multipartite information gap, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
6 results of the paper are not stated yet, because the library lacks an interface they need:
§2, unnumbered: approximate local recovery implies a small information gap: Uniform converse to approximate JOINT local recovery with unprimed-only dimensions (source-ambiguity)
§8, unnumbered: geometric CEMI is faithful: Faithfulness of the unrestricted extension/recovery fidelity supremum in (8.1) (source-ambiguity)
§§6–6.1, unnumbered: exact optimal total communication cost: Multipartite partial-state-distribution protocol and operational infimum in nats (hard)
§6.2: MSQ discord is twice the coherence-restoration and loss cost: Measurement Stinespring outputs connected to forward/reverse multipartite communication costs (hard)
§6.3: one-sided discord is twice the state-redistribution coherence cost: Measurement coherence restoration by actual two-party redistribution with passive B (hard)
Majority vote is a basic method for amplifying correct outcomes that is widely used in computer science and beyond. While it can amplify the correctness of a quantum device with classical output, the analogous procedure for quantum output is not known. We introduce quantum majority vote as the following task: given a product state ∣ψ1⟩⊗⋯⊗∣ψn⟩ where each qubit is in one of two orthogonal states ∣ψ⟩ or ∣ψ⊥⟩, output the majority state. We show that an optimal algorithm for this problem achieves worst-case fidelity of 1/2+Θ(1/n). Under the promise that at least 2/3 of the input qubits are in the majority state, the fidelity increases to 1−Θ(1/n) and approaches 1 as n increases. We also consider the more general problem of computing any symmetric and equivariant Boolean function f:{0,1}n→{0,1} in an unknown quantum basis, and show that a generalization of our quantum majority vote algorithm is optimal for this task. The optimal parameters for the generalized algorithm and its worst-case fidelity can be determined by a simple linear program of size O(n). The time complexity of the algorithm is O(n4logn) where n is the number of input qubits.
This mission is the statement-level formalization of Quantum majority vote (arXiv:2211.11729v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
61 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quantum majority vote: Theorem 1.2 (Quantum majority vote: Theorem 1.2, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
3 results of the paper are not stated yet, because the library lacks an interface they need:
Lemma 2.1 (Schur’s Lemma).: A specified identifying intertwiner between isomorphic coordinate representations. (source-ambiguity)
Corollary 2.12.: Compatibility of arbitrary input/output representations with entrywise complex conjugation. (source-ambiguity)
Theorem C.3.: The continuity convention for the cited classification of finite-dimensional SU(2) representations. (source-ambiguity)
Robust Learning of Consumer Preferences: the Myopic Tracking Policy is worst-case asymptotically optimal for identifying the top-ranked productResearch Paper
Motivation
A company that is about to launch a product often has several candidate versions of it (designs, packagings, feature bundles) and wants to know which one consumers like best. A common way to find out is to ask: show an arriving consumer a few versions and record which one they pick. Each such query costs time and money, and consumer answers are noisy, so the question is how to choose what to show, and when to stop asking, so that the most preferred version is found with a prescribed reliability using as few consumers as possible.
Y. Feng, R. Caldentey and C. T. Ryan, Robust Learning of Consumer Preferences (SSRN 3215614; Operations Research, doi:10.1287/opre.2021.2157), treat this as a sequential hypothesis test in the style of best-arm identification (Garivier and Kaufmann, 2016; Kaufmann, Cappé and Garivier, 2016). The difference from a bandit is in the feedback: an action is a set of versions, and an observation is a choice from that set drawn from an unknown choice model. The paper asks for a policy that is good not for one choice model but uniformly over a large nonparametric class of them, and shows that a simple likelihood-based policy achieves this.
Setting
There are K≥2 versions, [K]={1,…,K}. A display set is a subset S⊆[K] with ∣S∣≥2; S is the collection of display sets. A preferencef gives, for each S∈S and X∈[K], the probability f(X∣S) that a consumer shown S picks X. A rankingσ is a permutation of [K], rank 1 being the top.
For 0<p<1, the class Mp of p-separable preferences (Definition 1) consists of the f with f(X∣S)>0 exactly for X∈S, ∑X∈Sf(X∣S)=1, and a ranking σf such that within every display set, f(X′∣S)≤f(X∣S) iff σf(X)<σf(X′) (for X=X′), and moreover f(X′∣S)≤pf(X∣S) whenever σf(X)<σf(X′). The goal is to identify the top-ranked versionσf−1(1).
An admissible policyπ chooses, after each history Ht=(S1,X1,…,St,Xt), a distribution λt+1 over display sets for the next consumer; it stops at a stopping time τ and selects dτ∈[K]. It is δ-accurate if for every f∈Mp it stops almost surely and Pfπ(dτ=σf−1(1))≤δ; a family Π={πδ} is accurate if each πδ is δ-accurate (Definition 2).
With DS(f∥g)=∑k∈Sf(k∣S)logg(k∣S)f(k∣S) and Dλ=∑Sλ(S)DS, Chernoff's information is
where Mp(f) is the set of preferences in Mp with a different top-ranked version. The ordinal attraction (OA) preferences are fσOA(X∣S)=1−p∣S∣1−ppσ(X∣S)−1, where σ(X∣S) is the rank of X within S.
The Myopic Tracking Policy (MTP, Algorithm 1) with threshold β fits the OA ranking of maximum likelihood to the votes so far, stops when the generalized log-likelihood ratio against every OA ranking with a different top reaches β, and otherwise shows the top-n versions of the fitted ranking with probability λ∗OA([n]), an explicit distribution given in (7).
that is, for every choice of the initial display set S1 the family {MTPβ(δ)} is accurate and its worst-case rate is at most that of every accurate family. The goal states the shape of the result and does not fix the optimal value.
Milestones
The OA preferences are the hardest instances: MpOA⊆argminMpI∗ (Theorem 3, via Lemmas 4–5), and OA alternatives suffice to compute I∗ on them (Corollary 1).
The optimal display distribution is explicit and unique (Theorem 4, via Lemmas 6–9, a primal–dual certificate), and I∗OA has a closed form with two-sided bounds (Proposition 2).
Any δ-accurate policy needs Efπ[τ]≥kl(δ,1−δ)/I∗(f), and liminfδ↓0Ef[τ]/log(1/δ)≥1/I∗(f) (Theorem 1).
MTP has limsupδ↓0Ef[τ]/log(1/δ)≤1/I∗OA (Theorem 6), errs with probability at most C~1e−β (Lemma 10), and is δ-accurate for β≥C1+log(1/δ) (Theorem 7), with constants depending only on K.
Significance
The theorem says that one fixed, computable policy is optimal against the hardest consumer population in a nonparametric class, without knowing the population. Its display rule is static and sparse: only the K−1 nested sets of top-ranked versions are ever shown. The value 1/I∗OA gives a closed-form benchmark for the number of consumers any reliable test must survey, and Proposition 2 shows it barely depends on K. The lower bound (Theorem 1) is a change-of-measure argument that applies beyond this model, for example to identifying the top-k versions or the full ranking.
The results are proved in the paper; none is formalized. A formalization would produce a reusable discrete framework for sequential testing with set-valued actions and categorical feedback (finite-history laws, stopping times, expected stopping times in [0,∞]), a formal treatment of Chernoff-type max-min information over a choice-model class, and a machine-checked LP duality certificate for the optimal display distribution. It would also pin down the exact hypotheses: two printed statements need correction (see Formalization scope).
Difficulty
The class Mp is infinite and nonparametric, so the usual best-arm identification arguments, which track an estimate of the true instance, do not apply directly: MTP only ever estimates within the OA family, even when the truth is not OA. The upper bound must show that the drift of MTP's log-likelihood process under an arbitrary f∈Mp is at least I∗OA, which rests on the dominance structure of Lemmas 4–5 and on the optimality of the fixed distribution λ∗OA. The accuracy proof must control the error probability uniformly over Mp with a threshold independent of f and p. Computing I∗ on OA preferences reduces to a linear program over all rankings with a different top, whose explicit primal and dual solutions require the identities of Lemmas 6–9.
Formalization scope
Everything is finite or discrete and no measure theory is used. Versions are Fin K and rankings are Equiv.Perm (Fin K) with 0-based ranks (rank 0 is the top); the restricted rank σ(X∣S) stays 1-based. A preference is a function DS K → Fin K → ℝ. A policy is given by its display rule (a function of the history into ℝ≥0∞), a stopping predicate on histories, and a selection function; the law of a history is the explicit product ∏ℓλℓ(Sℓ)f(Xℓ∣Sℓ), E[τ]=∑tP(τ>t) in [0,∞], and I∗, I∗OA and all rates are in [0,∞]. Limits as δ↓0 are along 𝓝[>] 0. MTP's uniform tie-break enters as a mixture in the display rule; for β>0 stopping and selection do not depend on it.
Added hypotheses and readings, each disclosed in the items: (A-3) is required for X=X′ only (as printed it is unsatisfiable at X=X′); 0<p<1 and K≥2; δ∈(0,1); β>0 (Algorithm 1's input); the initial display set S1 is arbitrary. Theorem 1's first inequality is stated for δ≤1/2, since it fails for δ close to 1. Theorem 6's final sentence (equality for OA preferences) is not formalized, since it fails for bounded thresholds. The constants of Lemma 10 and Theorem 7 are quantified after K and before p.
Trivializing formalizations are ruled out: Definition 1 is non-vacuous (an OA preference is shown to lie in M1/2), the alternative sets require membership in Mp, top-rankedness is tied to the (A-3) ranking, and the goal includes the accuracy of MTP. Without it, a tiny threshold would stop after one vote.
Not in scope: Theorem 2 (a different policy for finite classes), Propositions 1 and 3–7, Corollaries 2–3, and the numerical study. Contributions to any milestone are welcome. The finite-history probability layer and the lower-bound argument are reusable for other sequential identification problems.
E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. https://arxiv.org/abs/1407.4443
The Privacy Paradox and Optimal Bias–Variance Trade-offs in Data Acquisition: The Minimax-Optimal Allocation Rule Is Constant Then Inversely Proportional to the Square Root of the Virtual CostResearch Paper
Motivation
Data marketplaces buy personal data from many individuals to estimate population statistics. Two features set such pricing apart from an ordinary procurement auction. First, each data owner has a private cost of sharing, so the buyer must design a menu of payments that elicits these costs truthfully. Second, data are correlated across people: an individual who refuses to share still loses privacy when similar people share. Liao, Su, Ziani, Wierman and Huang call the consequence the privacy paradox: privacy-conscious people may join a platform because abstaining does not protect them (arXiv:2105.14262, §1; published in Mathematics of Operations Research, 2024).
The paper asks how an analyst with a fixed budget should design such a mechanism when the goal is statistical: to estimate a population mean while trading off the bias caused by non-participants against the variance caused by sampling only some participants. The answer extends the optimal-auction framework of Myerson (Math. Oper. Res. 1981) and the data-procurement mechanisms of Roth and Schoenebeck (EC 2012) and Chen, Immorlica, Lucier, Syrgkanis and Ziani (EC 2018) to a setting with participation externalities and an adversarial correlation between data and costs.
Setting
Agents are split into groups i=1,…,I. An agent in group i has a cost c drawn from a density fi on the support [cmin,cmax], with distribution function Fi. At a fixed desired participation profileθ∗ the privacy cost of a participant is hi(c)=cbi with 0≤bi<1, a non-participant suffers gi(c)≤hi(c), the gap hi−gi is strictly increasing, and participants receive a benefit w.
The analyst posts a menu: a selection probability Ai(c~) and a payment Pi(c~) for a reported cost c~. A participant with true cost c who reports c~ has expected utility
uˉi(c~∣c)=Ai(c~)[Pi(c~)−c+hi(c)]−hi(c)+w.
The menu is truthful if reporting c~=c maximizes this utility. An agent joins if some report gives utility at least −gi(c), and the menu inducesθ∗ if the fraction of joining agents of group i is θˉi∗=Fi(c^i) for a threshold c^i. The virtual cost is
ϕi(c)=c−hi(c)+(1−bi)fi(c)Fi(c).
For the statistical problem, Appendix C of the paper discretizes the costs and sorts all virtual costs of participants as 0<ϕ1<⋯<ϕK, with cell probabilities πk>0 summing to θˉ∗. Given s agents, a budget B, a constant l collecting the participation terms, and a weight γ∈(0,1] on the variance, the analyst chooses Ak∈(0,1] and an adversary chooses the data probabilities pk∈[0,1] in the min-max program
subject to the budget ∑kπkϕkAk+l≤B/s, under the standing condition B/s−l>0.
Formalization targets
Goal: Theorem 2 (discrete form)
There are constants χ, η, ϕ^ and a feasible, non-increasing allocation
Ak∗={χ,η/ϕk,ϕk≤ϕ^,ϕk>ϕ^,
such that maxpU(A∗,p)≤maxpU(A,p) for every feasible A. The constants are left existential, as in the printed theorem; the case analysis that identifies them belongs to the milestones.
Milestones
Theorem 1, both directions: a menu is (strictly) truthful and induces θ∗ if and only if Ai is non-increasing (strictly decreasing) and Pi is the explicit payment (15); and Corollary 1: under that menu an agent participates if and only if c≤c^i.
The payment identity: expected payment equals expected virtual cost plus ∑iqiθˉi∗(hi(c^i)−gi(c^i)−w), which turns the budget into the linear constraint of the program.
Lemma 2 and Lemma 3: the best responses of the adversary and of the analyst.
Claims 1–4: monotonicity and gluing properties of the auxiliary functions Q(m,z), R(m,z) and existence of the thresholds they define.
Corollary 2 in its discrete form: under the low-budget condition (56), Ak∗∝1/ϕk together with p≡1 is a saddle point.
Significance
Theorem 1 is a participation-aware version of Myerson's characterization: it shows that the analyst loses nothing by restricting to monotone allocation rules with one explicit payment, and it pins down the payment that realizes a target participation rate. Theorem 2 then solves the analyst's worst-case bias–variance problem: the optimal selection probability is flat for cheap agents and decays like the inverse square root of the virtual cost for expensive ones. This shape explains when the mechanism can be strictly truthful (a strictly decreasing rule, Corollary 2, in the low-budget regime) and when only weak truthfulness is possible (a flat region, larger budgets).
The paper proves Theorem 2 for discrete costs and passes to continuous costs by letting the number of cells grow without bound, a step it asserts without proof. The mission formalizes the discrete theorem that Appendix C actually proves, together with both directions of Theorem 1. None of these results has a machine-checked proof yet.
Difficulty
The goal is a min-max statement about a program that is convex in the allocation and concave in the adversary's choice, with a coupled budget constraint. The natural first idea, to solve each player's first-order conditions and plug them into each other, does not by itself produce a solution: the analyst's best response clips at 1, the adversary's best response may be interior on some cells and at the boundary on others, and which cells are which depends on the budget. The paper resolves this by a case analysis on the ratio (B/s−l)/(γθˉ∗) against the values of Q(m,1)/R(m,1), with thresholds obtained from intermediate-value arguments, and each case requires its own multiplier and its own adversary strategy.
For Theorem 1 the obstacle is that the paper's envelope argument differentiates the allocation rule, while the theorem quantifies over all monotone rules, which need not be differentiable. The "only if" direction must be recovered from the convexity of the maximal utility as a function of the true cost.
Formalization scope
All statements live in the namespace PrivacyParadox.Alloc and use one definitions file. The group layer fixes one desired profile, so h, g, b and w are functions of the cost or numbers; their dependence on participation rates and correlation strengths plays no role in Theorems 1–2. The discrete layer indexes cells by k=1,…,K as the paper does, with real-valued data and Real.sqrt.
The formalization commits to the following conventions, each disclosed in the item it affects:
0≤b<1; the paper's Assumption 1 only gives h≤c, and b=1 breaks strict truthfulness.
Allocations are strictly positive. In Lean p/0=0, while the paper's objective is +∞ at Ak=0, pk>0; without this convention the zero allocation would look optimal.
The sorted virtual costs are strictly increasing, as the sorted list of p. 25 prints them.
0<γ≤1 and 0<θˉ∗≤1.
The "only if" half of Theorem 1 assumes θˉi∗<1, since at θˉi∗=1 other payments induce the same participation.
Participation is "some report reaches the outside option", which agrees with the paper's "the best report" whenever the maximum is attained.
Two trivializing readings are excluded: the goal compares A∗ with every feasible allocation, so it is not the best-response property of Lemma 3, and it asserts the existence of A∗ rather than assuming an optimizer of the stated form.
A complete development needs elementary real analysis (interval integrals of monotone functions, Fubini on a triangle, the intermediate value theorem) and finite-dimensional convex optimization (first-order optimality for a concave quadratic on a box and for a separable convex program with one linear constraint). The latter two are reusable well beyond this mission. Proofs of milestones are welcome in any order. The continuous form of Theorem 2, Lemma 1 (the derivation of the objective from the Horvitz–Thompson estimator), Propositions 1–2 and Properties 1–4 are not part of the mission.
Selected references
G. Liao, Y. Su, J. Ziani, A. Wierman, J. Huang, The Privacy Paradox and Optimal Bias–Variance Trade-offs in Data Acquisition, arXiv:2105.14262v1, 2021; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2105.14262
A. Roth, G. Schoenebeck, Conducting Truthful Surveys, Cheaply, Proceedings of the 13th ACM Conference on Electronic Commerce, 2012. https://doi.org/10.1145/2229012.2229076
Y. Chen, N. Immorlica, B. Lucier, V. Syrgkanis, J. Ziani, Optimal Data Acquisition for Statistical Estimation, Proceedings of the 2018 ACM Conference on Economics and Computation, 2018. https://doi.org/10.1145/3219166.3219195
D. G. Horvitz, D. J. Thompson, A Generalization of Sampling Without Replacement from a Finite Universe, Journal of the American Statistical Association 47(260):663–685, 1952. https://doi.org/10.1080/01621459.1952.10483446
Convex Optimization for Bundle Size Pricing Problem: the Cross-Moment-Model Profit Is Concave in Choice ProbabilitiesResearch Paper
Bundle size pricing and why its tractability matters
In bundle size pricing (BSP) a seller of many products offers a menu of bundles in which the price of a bundle depends only on its size, the number of items in it. Customers choose which items to put in a bundle and which size to buy. Season tickets for theatres and sports teams, cable-TV channel packages and streaming plans priced by the number of simultaneous devices are priced this way, and BSP is known to recover much of the profit of full mixed bundling with only a handful of prices (Chu, Leslie and Sorensen 2011).
Choosing the optimal size prices is hard. For given prices, the customer's value for the best bundle of size s is a maximal partial sum of order statistics of the item valuations, and the seller's expected profit depends on the joint law of these sums across sizes. Even when that law is known, it is not known whether the resulting pricing problem is tractable.
Li, Sun and Teo (2021) replace the exact choice model by the cross moment model (CMM) of Mishra, Natarajan, Tao and Teo (2012): only the mean vector and the covariance matrix of the bundle valuations are specified, and choice probabilities are those of the extremal distribution, among all laws with these two moments, that maximizes the customer's expected surplus. Their main result (Theorem 2) is that the seller's profit, written as a function of the choice probabilities, is concave, so the pricing problem becomes a concave maximization over a simplex. This mission formalizes that result.
Setting
Let m be the number of bundle sizes. Let ω∈Rm be the mean valuation vector, c∈Rm the vector of bundle costs, and Σ∈Rm×m the covariance matrix of the bundle valuations (the outside option, with value 0, is excluded). Write e for the all-ones vector. The simplex and its interior are
Δm={x∈R+m:e⊤x≤1},int(Δm)={x∈Rm:e⊤x<1,x>0}.
A point q∈Δm is a vector of choice probabilities: qs is the probability that the size-s bundle is bought, and 1−e⊤q the probability of buying nothing.
For a positive semidefinite matrix A, A1/2 denotes its unique positive semidefinite square root, and A⪰B means that A−B is positive semidefinite. Define
where Diag(x) is the diagonal matrix with diagonal x, and diag(X) below is the vector of diagonal entries of X. In the paper, Theorem 1 and Lemmas 1–2 show that for Σ≻0 every q∈int(Δm) is the CMM demand at exactly one price vector, namely p=ω+∇f(q) with
The statement is uniform in m, ω, c and in the positive definite Σ; it fixes no constant.
Milestones, in the order of the paper's proof
S(x)⪰0 for x∈Δm (proof of Theorem 1, p. 25).
S(λx+(1−λ)y)=λS(x)+(1−λ)S(y)+λ(1−λ)(x−y)(x−y)⊤⪰λS(x)+(1−λ)S(y), and the same inequality for T (proof of Lemma 6, p. 27).
Lemma 6 (p. 27): for x,y∈Δm and λ∈[0,1],
(T(λx+(1−λ)y))1/2⪰λT(x)1/2+(1−λ)T(y)1/2.
For g(q)=−q⊤∇f(q): g(q)=−21tr(T(q)1/2)+21q⊤Σ1/2(T(q))−1/2Σ1/2q (p. 28).
The epigraph {(q,t):g(q)≤21t} equals a linear matrix inequality in a bordered matrix, lifted to three constraints in auxiliary variables z and Z (p. 28).
q↦tr(T(q)1/2) is concave on Δm (p. 28).
{(q,Z):T(q)1/2⪰Z,q∈Δm} is convex (p. 28).
For Σ≻0, ∇f(q) above is the gradient of f at every q∈int(Δm) (p. 9).
Significance
Concavity of π turns bundle size pricing under the cross moment model into a concave program over the simplex: a local maximizer is global, and the problem can be passed to a conic solver through the semidefinite representation of milestone 5. The paper uses this to price bundles directly from two moments of the valuation distribution, and notes that the same reduction approximately solves other bundle pricing problems once they are written as multidimensional pricing problems. Before this result it was known that CMM choice probabilities are computable by convex optimization (Ahipaşaoğlu, Li and Natarajan 2018), but not whether pricing under CMM is tractable.
The result is proved in the paper; it has no machine-checked proof. The mission produces a formal statement of Theorem 2 against the explicit function (6), and the chain of the paper's proof as separately provable milestones. Several of these are reusable beyond the paper: Loewner concavity of x↦Diag(x)−xx⊤, Loewner concavity of the square root composed with it, and the Schur-complement description of a bordered linear matrix inequality over the reals.
Difficulty
The function π is not a composition of standard concave functions: it contains the inverse square root (T(q))−1/2 of a matrix that depends quadratically on q, inside both a diagonal extraction and a quadratic form. The scalar composition rules for concavity do not apply to matrix-valued maps, and the second derivative of q↦(T(q))−1/2 has no usable closed form. What is needed is the operator monotonicity and operator concavity of the matrix square root on positive semidefinite matrices (Horn and Johnson 1990). Mathlib has the corresponding results only for elements of C⋆-algebras, through the continuous functional calculus; real symmetric matrices with the Loewner order are a separate instance whose square root, monotonicity and concavity must be connected to that theory or proved directly.
Formalization scope
Everything is stated inside BSPConvex.CMM. Vectors are Fin m → ℝ and matrices Matrix (Fin m) (Fin m) ℝ; Σ is named Sig. The objects Δm, int(Δm), S, T, f, M(q)=Σ1/2(T(q))−1/2Σ1/2, ∇f (defined by the displayed formula), π (written literally as (6)), g and the bordered matrix are definitions in one file. A1/2 is CFC.sqrt under open scoped MatrixOrder, and A⪰B is (A - B).PosSemidef throughout. (T(q))−1/2 is (CFC.sqrt (T q))⁻¹, the matrix inverse.
The formalization departs from the page in three disclosed ways:
The goal and milestones 4, 5 and 8 are stated on int(Δm), not on Δm. On the boundary, T(q) is singular, (T(q))−1/2 is undefined in the paper, and Lean's inverse returns 0, which would make π a different function there.
Milestones 2, 3, 6 and 7 assume only Σ⪰0 (a covariance matrix), not Σ≻0; milestone 2 holds for all x,y∈Rm.
The interpretation of π as the expected profit under CMM rests on Theorem 1 and Lemmas 1–2, which are not formalized; the mission poses concavity of the explicit function (6). The strong concavity of f cited on p. 9 is not stated.
A formalization that defines π through g or f so that concavity is definitional, or that states the theorem on a set where it is vacuous, does not count: π is the literal expression (6), and int(Δm) is nonempty for every m (it contains qi=1/(m+1)).
Contributions welcome beyond the milestones: a real-matrix version of operator monotonicity and concavity of the square root, the Schur complement criterion for real block matrices with a positive definite block, and differentiability of A↦tr(A1/2) on positive definite matrices.
S. D. Ahipaşaoğlu, X. Li, K. Natarajan, A convex optimization approach for computing correlated choice probabilities with many alternatives, IEEE Transactions on Automatic Control 64(1):190–205, 2018.
V. K. Mishra, K. Natarajan, H. Tao, C.-P. Teo, Choice prediction with semidefinite optimization when utilities are correlated, IEEE Transactions on Automatic Control 57(10):2450–2463, 2012.
K. Natarajan, C.-P. Teo, On reduced semidefinite programs for second order moment bounds with applications, Mathematical Programming 161(1–2):487–518, 2017.
C. S. Chu, P. Leslie, A. Sorensen, Bundle-size pricing as an approximation to mixed bundling, American Economic Review 101(1):263–303, 2011. https://doi.org/10.1257/aer.101.1.263
R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1990.
Joint Product Framing (Display, Ranking, Pricing) and Order Fulfillment Under the Multinomial Logit Model for E-Commerce Retailers: Randomized Framing and Fulfillment Loses O(√θ) Against DET'Research Paper
Motivation
An online retailer decides, for every arriving customer, how to frame its catalog: which products are displayed, in which section or position, and at which of several price points. Framing changes demand. A product on a promotional banner sells more than the same product further down the page. The retailer must also decide which fulfillment center (FC) ships each order, and shipping costs depend on the distance from the FC to the customer. With limited inventory in each FC, framing and fulfillment interact: showing a product to a far-away customer can drain the stock that a closer, cheaper future order would have used.
Lei, Jasin, Uichanco and Vakhutinsky (SSRN 3282019; Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2021.1012) model this as the joint framing and fulfillment (JFF) problem. Customers choose by the multinomial logit (MNL) model. The paper builds the Randomized Framing and Fulfillment (RFF) policy from a deterministic relaxation, and proves that its relative loss against the optimal policy vanishes at rate θ−1/2 as the market is scaled by θ. The work was carried out with data from a major U.S. retailer: 56 products in 27 FCs (§6).
Setting
There are I products, J customer regions, K FCs and Rframing groups; group r can hold at most Qr∈N+ products, and group R means "not displayed". A framing assignment is a map ϕ:[I]→[R]. The feasible ones form
Ω(Q)={ϕ:#{i:ϕ(i)=r}≤Qr∀r}.
In each of T periods at most one customer arrives, from region j with probability λj. Product i in group r has attraction vijr>0 for r=R, with vijR=0, and price pir. A region-j customer who sees ϕ buys i with probability vijϕ(i)/(1+∑kvkjϕ(k)). The order is shipped from an FC k that holds the product, at cost cijk, and FC k starts with Cik units. J∗ is the optimal expected total profit (OPT').
The deterministic counterpart DET' replaces the 0/1 framing by fractions xijrt∈[0,1], with
(10a) ∑ixijrt≤Qr;
(10b) ∑rxijrt=1;
fulfillment fractions yijkt∈[0,1] with (10c) ∑kyijkt=θij(xjt) and (10d) ∑t,jyijkt≤Cik.
DET' maximizes ∑t,i,jRij(xjt)−∑t,j,i,kcijkyijkt, and its value is JD.
ConstrDist turns a fractional framing x of one region into a distribution over Ω(Q), in three steps:
It pads x with fictitious rows so that column sums become integers, giving a framing matrix (rows sum to 1, column r sums to Q~r=⌈∑ixir⌉).
It writes that matrix as a convex combination of integral framing matrices; each of these is an assignment.
It re-scales the resulting weights by the MNL denominators.
RFF runs ConstrDist on an optimal DET' solution for every region and period. Each period it samples ϕ, hides out-of-stock products, samples an FC k with probability proportional to yijkt,D, and ships from k, or from the cheapest FC with stock if k is empty. The scaled problem has horizon θT and inventories θC; its values are JD(θ), J∗(θ) and JRFF(θ).
Formalization targets
Goal: Theorem 2 (p. 23)
There are M>0 and θ0 such that for all θ≥θ0, every optimal DET'(θ) solution and every choice of decompositions in ConstrDist,
0≤JD(θ)−JRFF(θ)≤Mθ,
and DET'(θ) has an optimal solution. Moreover, if J∗(1)>0, then J∗(θ)>0 for large θ and
1−J∗(θ)JRFF(θ)=O(θ−1/2).
The constants depend on the instance only.
Milestones
Lemma 2 (p. 16): the padded matrix is a framing matrix, and integral framing matrices are feasible assignments.
Decomposition (p. 14, shown in §4.3): every nonnegative framing matrix is a convex combination of integral framing matrices.
Lemma 3 (p. 16): the re-scaled distribution satisfies (7a)–(7c), i.e. ∑ϕρj(ϕ)=1, ∑ϕρj(ϕ)θij(ϕ)=θij(x) and ∑ϕρj(ϕ)Rij(ϕ)=Rij(x).
The result shows that a policy computed once from a deterministic program loses only O(θ) in absolute terms, despite three complications:
choice probabilities are nonlinear in the framing;
the framing is a combinatorial object;
inventory sits in several locations.
Lemma 3 is the reusable part. For MNL demand, any fractional framing can be realized exactly in expectation, for purchase probabilities and revenues simultaneously, by a randomization over feasible assignments. This makes fluid-based policies available for display, ranking and pricing decisions alike.
Status. The statement is published, but its printed proof is incomplete. EC 2 bounds RFF by a variant that ignores stock-outs and asserts that RFF "will generate zero profit" at a stock-out. RFF does not do that: it hides the product or re-routes the order, which changes all later inventories. The step is not justified. The statement was checked at planning by exact dynamic programming on four small instances, up to θ=64; (JD−JRFF)/θ stayed between 3.7 and 11. A complete proof, formal or informal, is new. None of these results has a machine-checked proof.
Difficulty
The obvious argument compares RFF with its deterministic plan period by period. Lemma 3 makes the expected sales and revenues match the plan exactly, and the total deviation of sales from plan is O(θ). That argument controls a policy that never runs out of stock. RFF does run out: after a stock-out it hides products and re-routes orders. So its later inventory, and hence its later framings and costs, differ from the plan in a path-dependent way. The difficulty is to bound the profit lost through this feedback by O(θ), uniformly over every optimal DET' solution, including time-varying ones, and every decomposition. A second, smaller difficulty is that DET' is not a linear program in x. Lemma 5 and stationarity both need its reformulation as one.
Formalization scope
Model. An instance is one structure, with indices in Fin types; the no-display group is the last index. The standing assumptions are bundled in one predicate:
I,J,K≥1 and R≤I;
λj∈[0,1] with ∑jλj≤1;
vijR=0<vijr for r=R;
Qr≥1 and QR≥I.
Departures from the page, all disclosed in the items.
∑jλj≤1 is the formal reading of "at most one customer per period".
QR≥I is added; without it RFF can be infeasible.
θ∈N, so that θT is an integer.
The FC set is [K]; the page's "FC 0" in (8c) is undefined.
Ties in RFF's re-routing are broken by least index.
The decomposition milestone assumes nonnegative entries.
Values.JD is the supremum of the DET' objective, and the goal asserts that an optimum exists. J∗ is defined by the Bellman recursion of OPT'. JRFF is the exact expected profit of RFF, computed by backward recursion over (period, inventory). All expectations are finite sums; there is no measure theory.
Ruled out.JRFF is RFF's own expected profit, with its stock-out handling. Replacing it by the value of an idealized policy that ignores stock-outs, or by a sum of per-period fluid revenues, is a different and much weaker statement.
The goal quantifies over all optimal solutions and all decompositions. The decomposition milestone and the existence clause keep it from being vacuous.
Infrastructure. The decomposition milestone is the rectangular, integer-column-sum version of Birkhoff–von Neumann, which is included as a referenced item. The Charnes–Cooper reformulation of DET' as a linear program is needed for Lemma 5 and stationarity. Both are reusable beyond this mission.
Contributions welcome. Proofs of any milestone, and a complete proof of Theorem 2.
Selected references
Y. M. Lei, S. Jasin, J. Uichanco, A. Vakhutinsky, Joint Product Framing (Display, Ranking, Pricing) and Order Fulfillment Under the Multinomial Logit Model for E-Commerce Retailers, Manufacturing & Service Operations Management, 2021. SSRN version: https://ssrn.com/abstract=3282019; published version: https://doi.org/10.1287/msom.2021.1012
G. Birkhoff, Tres observaciones sobre el álgebra lineal, Univ. Nac. Tucumán Rev. Ser. A 5, 1946, 147–151.
A. Charnes, W. W. Cooper, Programming with linear fractional functionals, Naval Research Logistics Quarterly 9, 1962, 181–186. https://doi.org/10.1002/nav.3800090303
G. Gallego, R. Ratliff, S. Shebalov, A general attraction model and sales-based linear program for network revenue management under customer choice, Operations Research 63(1), 2015, 212–232. https://doi.org/10.1287/opre.2014.1328
Dynamic Learning and Market Making in Spread Betting Markets with Informed Bettors: the inertial policy deters bluffing, drives the spread line to the median and has O(log T) regretResearch Paper
Motivation
In a spread betting market a market maker quotes a line s for a quantity whose outcome X is not yet known (a point spread in sports, a price level in finance), and bettors wager on either side of it. The market maker earns a commission on every bet and would like her line to sit at the median of X, where both sides are equally likely and she carries no directional risk. She does not know the median: she must learn it from the bets themselves. Some bettors are informed: they know the median, and they can bet many times. An informed bettor who sees that the market maker learns from bets has an incentive to bluff, betting against his information to push the line the wrong way and then profiting from the mispriced line later.
Birge, Feng, Keskin and Schultz (SSRN 3283392, published in Operations Research, 2021, doi:10.1287/opre.2021.2109) show that natural Bayesian pricing policies are exploited in this way (their Theorem 1: non-converging lines and regret linear in the horizon) and design an inertial policy that is not. This mission formalizes the positive half of the paper: under the inertial policy the informed bettor's best response is an honest threshold strategy, the line converges to the correct median, and the market maker's regret grows only logarithmically.
Setting
The outcome is X=m+ε with unknown median m∈{m0,m1}, sL<m0<m1<sH, and noise ε with c.d.f. Fε. Under hypothesis Hi the median is mi and X has c.d.f. Fi(x)=Fε(x−mi); write Fˉi=1−Fi and fi for the density. Assumption 1 requires the noise density fε to be continuously differentiable, symmetric around zero, and strictly positive on ∣x∣≤max{sH−m0,m1−sL}. The commission rate is c∈(0,1).
Bets t=1,2,… arrive one at a time. The market maker quotes st; a bet is dt=+1 (on X>st) or dt=−1 (on X<st). The winner is paid 1−c, the loser pays 1. At each bet the informed bettor chooses an action at∈{+1,0,−1}, possibly at random and based on the public history and his own past actions; at=±1 is a bet, and at=0 leaves the bet to a myopic bettor, who bets +1 with probability Fˉi(st). The informed bettor's expected payoffs per bet are ji+(s)=(1−c)Fˉi(s)−Fi(s) and ji−(s)=(1−c)Fi(s)−Fˉi(s), his total expected profit over T bets is Viπ,ξ(T), and a best response maximizes liminfTViπ,ξ(T) when this is bounded, and liminfTViπ,ξ(T)/T otherwise. The market maker's regret is
her loss relative to a market maker who knows the median, and Δπ(T)=maxiΔiπ,ξi∗(T) against best-responding bettors.
The inertial policyπI tracks the net bet count Zt=∑ℓ<tdℓ (Z1=0) and quotes st=s~(Zt). With α=F1(m0), a residual probability sequenceρ:Z+→(0,21−α) fixes s~ through F1(s~(z))=21−ρ(z) and F0(s~(−z))=21+ρ(z) (Proposition 2). The paper's choice is
ρ(z)=r0+rz1,r0=[21−F1(2m0+m1)]−1,r>0.
The informed bettor's candidate best response is the threshold strategyξ1∗(z)=I{z<zˉ}, ξ0∗(z)=−I{z>−zˉ}, with zˉ=inf{z:2ρ(z)ρ(z−1)−ρ(z)−ρ(z−1)>21−2−cc}, and the admissible range of r is (0,rˉ) with the explicit rˉ=min{2,rˉ0,rˉ1} of (G.2)–(G.4). Write dt=∣st−mi∣.
Formalization targets
Goal: Theorem 4 (p. 17)
For every c∈(0,1), i∈{0,1} and r∈(0,rˉ):
zˉ∈Z∪{−∞}andξi∗is a best response;Zt→±∞a.s.,dt→0a.s.;t=1∑TEiπI,ξi∗[dt]→∞,t=1∑TEiπI,ξi∗[dt]=O(TlogT),ΔπI(T)=O(logT).
The first clause is (T3:2) of Theorem 3; it is part of the goal because the probability in Theorem 4 is defined by the best response.
Milestones
In proof order: Proposition 2 (residual-probability representation); Lemma 4 (a discrete Dynkin formula); Lemmas G.1 and G.2 (properties of ρ and of zˉ); Lemma L.1 (a product-series test); Lemma L.2 (occupation sums); Lemmas 1–3 (the value function Jˉi: finiteness, continuation profit, Bellman equation); Theorem 3 (bounded profit, threshold best response); Lemma 5 (regret as an additive functional ∑tE[l(Zt)]); Lemma H.1 (ρ is slowly vanishing and regular); Lemma L.4; Proposition K.2 (the general slowly vanishing case); Proposition 3 (rates for ρ(Zt) and l(Zt)).
Significance
The result shows that a market maker facing a strategic, informed, repeat bettor can still learn: a policy that moves its line only gradually removes the incentive to bluff, so the informed bettor bets honestly when the line is far from his median and abstains otherwise. The line then converges to the truth almost surely, and the cost of learning is O(logT), against Ω(T) for Bayesian policies in the same market. Proposition K.2 extends the analysis to every slowly vanishing ρ and generic threshold, which explains the choice ρ(z)∼1/z: decaying faster makes the market state recurrent, slower makes the regret larger.
The results are proved in the paper; none of them has a machine-checked proof. A formalization checks a long chain of exact computations (closed-form solutions of birth–death difference equations, a Bellman verification over history-dependent strategies) whose constants and boundary cases are easy to get wrong. Lemma 4, Lemma L.1 and Lemma L.2 are general facts about Markov chains and product series, usable outside this model.
Difficulty
The market state Zt is a birth–death chain whose drift vanishes: under H1, for large z it moves up with probability 21+ρ(z)≈21+rz1. It is transient only because ρ decays no faster than 1/(4z), and it grows like t, so large-deviation arguments, which need the drift to dominate the noise, do not apply. The paper instead evaluates every quantity exactly through difference equations. The best-response claim is harder still: it must hold against every history-dependent randomized strategy, including bluffing ones, and the Bellman equation alone does not imply optimality for a total-reward criterion (every constant shift of a solution is a solution); finiteness and nonnegativity of Jˉi and the identification of the threshold strategy's actual profit with Jˉi are needed as well.
Formalization scope
All statements live in the namespace SpreadBetting.Inertial. A structure Market bundles c,m0,m1,sL,sH and the noise density fε, and Market.Standing collects the model's ranges, the fact that fε is a probability density, and Assumption 1. The c.d.f. is Fε(x)=∫−∞xfε, and Fi−1 is the generalized inverse inf{x:p≤Fi(x)}, certified by Proposition 2. Residual probabilities are functions N→R used at z≥1 and extended to Z by (E.1).
Expectations are exact finite recursions over bet histories, not integrals. A strategy maps the list of past (bet, own action) pairs and the current state Zt to a probability vector over actions. The market state is a function of the public history and determines st. The best response (2.3) ranges over all such admissible strategies, and its liminfs and suprema are taken in EReal. Almost-sure statements use the path law of the market-state chain on Z, from the published GittinsIndex definition (BanditAlgorithm.markovChainMeasure; coordinate t is Zt+1). O(⋅) is the paper's Definition 1; "diverges at rate O(g)" means divergence to +∞ together with the bound.
The threshold zˉ, the bound rˉ and the policy ρ(z)=1/(r0+rz) are explicit, so none of the statements is trivially true. In particular, the goal does not take ξi∗ as a free strategy pinned by hypotheses, does not use a junk value for an infinite liminf, and does not restrict deviations to Markov strategies. Added hypotheses are disclosed item by item: r∈(0,rˉ) on Lemma 1, whose proof uses it, and measurability and integrability on Lemma 4.
Contributions are welcome at every level: the general Lemma 4 and Lemma L.1, the difference-equation lemmas (L.2, L.4), the properties of ρ and zˉ, and the Bellman verification of Theorem 3. A proof of the goal needs Borel–Cantelli or a transience criterion for birth–death chains on the path space, Mathlib's Ionescu–Tulcea construction, and elementary real analysis for the asymptotics of products ∏(21−ρ)/(21+ρ).
Selected references
J. R. Birge, Y. Feng, N. B. Keskin, A. Schultz, Dynamic Learning and Market Making in Spread Betting Markets with Informed Bettors, SSRN working paper 3283392, version of April 14, 2020. https://ssrn.com/abstract=3283392
J. R. Birge, Y. Feng, N. B. Keskin, A. Schultz, Dynamic Learning and Market Making in Spread Betting Markets with Informed Bettors, Operations Research, 2021. https://doi.org/10.1287/opre.2021.2109
R. Durrett, Probability: Theory and Examples, 5th ed., Cambridge University Press, 2019 (recurrence of birth–death chains). https://doi.org/10.1017/9781108591034
A Statistical Learning Approach to Personalization in Revenue Management: High-Probability Revenue Gap Bound for Decisions from the ℓ1-Constrained Logit Maximum Likelihood EstimateResearch Paper
Motivation
Retailers and platforms increasingly set prices and choose which products to display per customer, using observed customer attributes (location, device, purchase history). The decision rule is usually built in two steps: fit a choice model to historical transactions, then optimize prices and assortments as if the fitted model were the truth. Chen, Owen, Pixton and Simchi-Levi (Management Science, 2021; author manuscript SSRN 2579462) ask how much revenue this "estimate, then optimize" procedure loses, as a function of the amount and richness of the historical data. Their answer is a non-asymptotic, high-probability bound on the revenue gap for a feature-dependent multinomial logit model that covers personalized pricing and personalized assortment in one framework.
The estimation side builds on the econometrics of the conditional logit model (McFadden, 1974), whose classical theory is asymptotic. The finite-sample tools come from high-dimensional statistics: concentration of sample covariance matrices of sub-Gaussian vectors (Vershynin, 2012) and strong-convexity arguments for M-estimators.
Setting
There are J products and a no-purchase option 0. A customer arrives with a feature vectorz∈Rd, scaled so that ∥z∥∞≤1. The seller offers an assortmentS⊆[J] and sets a pricepj∈[pmin,1] for each product, 0<pmin≤1; the price box is P=[pmin,1]J. For product j the feature–price vector is x=(z,pj)∈Rd+1.
The parameter is θ=(γ1⊤,β1,…,γJ⊤,βJ)⊤∈RJ(d+1). The mean utility of product j is Vj=⟨γj,z⟩+βjpj. Under the multinomial logit (MNL) model the customer buys j∈S with probability
Pz(j;S,p,θ)=1+∑l∈SeVleVj,
and buys nothing with probability 1/(1+∑l∈SeVl). The expected revenue is fz(S,p;θ)=∑j∈SpjPz(j;S,p,θ).
The data are n past transactions (zi,Si,pi,yi), where yi is the observed choice. The negative log-likelihood is ℓn(θ)=−n1∑ilogPzi(yi;Si,pi,θ). Given a radius R with ∥θ∗∥1≤R, the constrained MLEθ^ minimizes ℓn over ∥θ∥1≤R.
Two assumptions govern the data. Assumption 1: the outcomes are conditionally independent given features and prices and follow the MNL model at the true parameter θ∗, and for each j the vectors xij=(zi,pij) are independent across i (not necessarily identically distributed) and sub-Gaussian with norm at most ψ. Assumption 2: every product was offered in at least νn transactions, and the averaged second-moment matrix ΣIj=nj1∑i∈IjExijxij⊤ over the transactions Ij offering j has smallest eigenvalue at least ρ>0.
Given a family S of feasible assortments, (S∗,p∗) maximizes fz(⋅,⋅;θ∗) over S×P (the oracle decision) and (S^,p^) maximizes fz(⋅,⋅;θ^).
Formalization targets
Goal: revenue convergence rate (Theorem 2, p. 17)
For every ψ there is Cψ, and for every R a constant C(R,ψ), such that whenever n≥4Cψlog(νn)/(νmin(ρ,1)2), with probability at least 1−1/n−2J/(νn), for every feature vector z,
The constants are unspecified, as on the page; only their dependence is fixed.
Milestones
Lemma EC.1 (p. ec2): Diag(q)−qq⊤ is positive semidefinite with smallest eigenvalue at least minjqj⋅q0.
The constant c (p. ec4): Pz(j)Pz(0)≥c=e−R/[1+e−R+(J−1)eR]2 on the feasible set.
Lemma 2 (p. 16, corrected): with probability at least 1−2J/(νn), ℓn is strongly convex on the ℓ1 ball with parameter η=e−Rνρ/(2[1+e−R+(J−1)eR]2).
Lemma 1 (p. 15): with probability at least 1−1/n, ∥∇ℓn(θ∗)∥∞≤2log(2nJ(d+1))/n.
(4)–(5) (p. 15, sharpened): for an η-strongly convex function minimized over a convex set, ∥θ^−θ∗∥2≤N∥∇f(θ∗)∥∞/η.
Theorem 1 (p. 14): with probability at least 1−1/n−2J/(νn), ∥θ^−θ∗∥2≤2e−Rνρ[1+e−R+(J−1)eR]2n2J(d+1)log(2nJ(d+1)).
Lipschitz bound (proof of Proposition 1, pp. 17–18): ∣fz(S,p;θ)−fz(S,p;θ′)∣≤4JJ(d+1)∥θ−θ′∥2.
Proposition 1 (p. 17): the revenue forecast error is at most 2νρC(R,ψ)J4(d+1)log(2nJ(d+1))/n for all decisions and bounded features, with the same probability.
Significance
The result. The theorem quantifies the value of historical data for personalized revenue management. The loss shrinks as O~(1/n) and degrades with 1/ν (products rarely offered in the past) and 1/ρ (features and prices that are nearly collinear in the data). This makes precise two practical warnings of the paper: price experimentation must not be correlated with customer features, and every product must have been explored. The bound is uniform over customers, so it is an out-of-sample guarantee. It specializes to customized pricing (Corollary 1) and to personalized assortment with fixed prices (Corollary 2), and the parameter rate of Theorem 1 matches the Cramér–Rao rate up to logarithmic factors.
Formalizing it. The paper's results are proved but none has been machine-checked. A formal development would produce a verified finite-sample theory of the constrained logit MLE: the softmax Hessian bound, strong convexity of the log-likelihood with high probability, the gradient concentration, and the transfer to revenue. Two printed statements need care, and the mission states the corrected forms: Lemma 2 needs an additional sample-size condition (see Formalization scope), and the printed (5) loses a factor 2 relative to what Theorem 1 uses.
Difficulty
The deterministic parts (Lemma EC.1, the constant c, the Lipschitz bound, the step (4)–(5)) are finite-dimensional calculus. The main obstacle is Lemma 2. Its proof needs the empirical second-moment matrices nj1∑i∈Ijxijxij⊤ to be within ρ/2 of their expectations in operator norm, for independent but non-identically distributed sub-Gaussian vectors, with a sample size depending on ψ only through a constant. The standard references state this for identically distributed vectors. Mathlib has no matrix concentration of this kind, and an ε-net argument with a Bernstein-type bound must be built. A second obstacle is the randomness of the decision itself: the optimal decisions are argmax selections, so the bad event is controlled through Theorem 1's event and not through measurability of the decision.
A first attempt often tries to bound the gap by the parameter error directly through the optimization problem. That fails: the argmax is not Lipschitz in θ. The paper's route compares revenues of fixed decisions, which needs the bound of Proposition 1 uniformly over all decisions.
Formalization scope
The model is one definitions file in the namespace PersonalizedRM.RevenueGap. The parameter is EuclideanSpace ℝ (Fin J × Fin (d+1)), so ‖θ‖ is the Euclidean norm; ∥θ∥1 is an explicit sum and ∥∇ℓn∥∞ is a bound on every fderiv partial derivative. Outcomes are Option (Fin J) (none is no purchase). Historical assortments are deterministic. The conventions committed to are:
Outcomes. Assumption 1(a) and well-specification are encoded by realizing yi as an inverse-CDF draw from the MNL law at θ∗, driven by uniform variables independent of each other and of all features and prices.
Assumption 2.λmin≥ρ is written as a quadratic-form bound, and ν is any positive constant with nj≥νn. Two printed requirements are dropped, which strengthens every statement: ν≤1/J (false for overlapping assortments) and the unused clause maxi,jλmin(Exijxij⊤)>0.
Probability. "With high probability" means probability at least 1−1/n−2J/(νn), the event of Theorem 1. Every probabilistic statement bounds the outer measure of the bad event.
Sample size.n≥1 is assumed.
Lemma 2 correction. The milestone adds νn≥4CψJ(d+1)/min(ρ,1)2. As printed, the lemma fails when d+1>n: the empirical second-moment matrix is then singular, so ℓn cannot be strongly convex.
Sharpened (5). Milestone 5 states the constant 1 instead of the printed 2.
Theorem 1, Proposition 1 and Theorem 2 are stated exactly as printed.
Constant order. The constants are quantified in the order ∀ψ∃Cψ∀R∃C(R,ψ), before J, d, n, ν, ρ and the data. A constant chosen after the data could be made large enough that the right-hand side exceeds the trivial bounds (revenue gap ≤1, parameter error ≤2R), and the statements would be empty.
Infrastructure. A complete development needs:
MNL softmax derivative and Hessian identities;
Hoeffding's inequality (on the platform);
a covariance concentration bound for independent sub-Gaussian vectors;
Weyl's inequality (on the platform);
the strong-convexity estimate (5).
The concentration bound and the softmax Hessian bound are reusable beyond this mission. Contributions to any milestone are welcome, as are proofs of the generic lemmas as separate theorems.
Not formalized: Corollaries 1–2 (specializations of the goal), Proposition 2 (the mixing-data rate, stated only up to O~), and the numerical study of §5.
R. Vershynin, Introduction to the Non-Asymptotic Analysis of Random Matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027
Dynamic Pricing of Relocating Resources in Large Networks: the Lagrangian policy is within O(√(ln n/n)) of optimal in hub-and-spoke networksResearch Paper
Motivation
Ride-hailing, car-sharing and bike-sharing platforms price trips whose execution moves the resource itself: a car that takes a passenger from the suburbs to the airport is no longer available in the suburbs. Each price therefore sets both the revenue of the current request and the future spatial distribution of the fleet. Choosing prices to maximise long-run revenue is a Markov decision problem whose state, the number of resources at each location, has a number of configurations exponential in the number of locations. Exact dynamic programming is impossible at the scale of a city.
Balseiro, Brown and Chen (SSRN 3313737, version of May 23, 2020; published in Management Science, doi:10.1287/mnsc.2020.3735) study hub-and-spoke networks and propose a Lagrangian policy. The capacity constraint coupling the locations is relaxed with a dual variable, the relaxation separates into one small problem per spoke, and the per-spoke solutions are implemented in the real system. Earlier work on this model (Waserhole and Jost, 2016; Banerjee, Freund and Lykouris, 2016) uses fluid relaxations that lead to static prices, depending on the origin and destination but not on the resource levels. These are within a factor m/(m+n−1) of the fluid bound, hence asymptotically optimal when the number of resources m grows faster than the number of locations n. When m and n grow at the same rate, which is the regime of a large city with few vehicles per area, no static policy is asymptotically optimal (the paper's Example 5.1). The Lagrangian policy is a dynamic, state-dependent policy that is computable and asymptotically optimal in that regime.
Setting
A hub (location 0) and nspokesi∈[n] share m resources. In each period one request arrives: it asks to relocate a resource from spoke i to the hub, type (i,0), with probability qi0>0, or from the hub to spoke i, type (0,i), with probability q0i>0; these probabilities sum to one and are independent across periods. The provider picks a demand leveld∈[0,1], equivalently a price. The request is fulfilled with probability d if its origin holds a resource and is lost otherwise; the expected revenue is rij(d). Assumption 2.1: each rij is strictly concave on [0,1], rij(0)=0, maxrij≤rˉ, max∣rij′∣≤ωˉ, and the maximiser is interior.
The state is the vector of spoke levels x∈X={x∈Nn:∑ixi≤m}, the hub holding x0=m−∑ixi. The optimal average revenueVOPT (problem (1)) is the supremum, over non-anticipative feasible policies, of the long-run average expected revenue.
Penalising the spoke resources with a dual variable λ≥0 yields, for each spoke, the spoke problem (6): maximise ∑xpi(x)[qi0ri0(di(x,i,0))+q0ir0i(di(x,0,i))]−λ∑xxpi(x) over a distribution pi on [0:m] and controls satisfying the birth–death balance equations pi(x)q0idi(x,0,i)=pi(x+1)qi0di(x+1,i,0). Its value is hiλ. The relaxation value is Vˉλ=mλ+∑ihiλ (4), the Lagrangian bound is VR=minλ≥0Vˉλ (9), and the perturbed dual is VR(δ)=minλ≥0Vˉλ−δλ (11), with optimal solution λ∗(δ). The Lagrangian policyπ(δ) (Definition 3.1) applies the controls of optimal solutions of (6) at λ∗(δ), spoke by spoke, and drops a hub request when the hub is empty. Vπ(δ) is its average revenue and P[X0(δ)=0] the stationary probability that the hub is empty. In the relaxed system the hub may go negative; there the spokes are independent with laws pi.
Formalization targets
Goal: Corollary 4.7
Under Assumption 4.1 (E[X~i(δ)]≤c for every spoke, c>0 independent of n) and with b=1/(1+c), for 0≤δ<m,
VOPT−Vπ(δ)=O(lnn/n)when m and n grow at the same rate.
Milestones
The milestones follow the paper's proof. The spoke problem solves the spoke Bellman equation (Proposition 3.2), the relaxation's value is independent of the initial state, equals mλ+∑ihiλ and bounds VOPT (Proposition 3.1), and the controls are monotone (Proposition 3.3). The relaxed and original chains have stationary laws ∏ipi and a unique μ (Corollaries B.10, B.11). The perturbation costs at most rˉδ/(m−δ) (Lemma 4.2), continuation-value differences are at most ωˉ (Lemma A.10), and the relaxed–original gap is controlled by hub depletion (Lemma 4.3), giving Theorem 4.1,
Vπ(δ)≤VOPT≤VR≤Vπ(δ)+rˉm−δδ+(rˉ+ωˉ)P[X0(δ)=0].
Stochastic dominance between the two systems (Lemma 4.4) gives P[X0(δ)=0]≤P[X~0(δ)≤0] (Corollary 4.5). The spoke laws are log-concave (Proposition B.9), log-concave generating functions are dominated by geometric ones (Lemma A.14), a concentration bound for sums of log-concave variables follows (Lemma A.12), and the relaxed depletion probability is at most exp(−2bδ2/(m+n)) (Proposition 4.6).
Significance
The result. A policy computed from n independent problems of size m+1 loses only O(lnn/n) per period against the optimal policy of a problem with exponentially many states. No static policy achieves a vanishing gap. Theorem 4.1 also yields a practical certificate: VR is a computable upper bound, and the gap is governed by one observable quantity, the hub-depletion probability. The same structure extends to several hubs (the paper's Theorem 6.1).
Formalizing it. The result is proved in the paper; nothing here is open, and no part of it has been machine-checked. A formal proof would check a chain that combines average-reward dynamic programming, convex duality and sensitivity analysis, a coupling argument between two Markov chains, and a concentration inequality for log-concave variables. Several of these steps are stated in the paper with brief or cited arguments (the Bellman equation of the spoke problem, the class structure of the chains, Keilson's factorial-moment inequality behind Lemma A.14).
Difficulty
The natural first idea is to use the Lagrangian policy at the optimal dual λ∗ of (9). At λ∗>0 the relaxation keeps zero resources in the hub in expectation, so the real hub is empty a constant fraction of the time and every hub request lost there costs a constant. The perturbation δ is what makes the argument work. The key step is then to compare the relaxed system, where spokes are independent and the hub may go negative, with the original system, where the hub constraint couples all spokes. This needs both a loss bound per depletion event (Lemma A.10, which rests on the monotonicity of Proposition 3.3) and a pathwise coupling (Lemma 4.4). A Chebyshev bound on the hub level gives only a polynomial rate. The exponential rate requires the log-concavity of every spoke law and a geometric domination of its generating function.
Formalization scope
No measure theory. Policies are deterministic functions of the observed history (past request types and fulfilment outcomes) and the current request type. The finite-horizon expected revenue is a finite recursion, and VOPT is the supremum over feasible policies of the limsup of its time average. Stationary distributions are finite probability vectors, via the published definition MarkovChain.IsStationary. Sums of independent ℕ-valued variables are iterated convolutions.
Primitives. The revenue functions rij are primitives satisfying Assumption 2.1. Request types are Fin n ⊕ Fin n, spoke levels Fin (m+1), the hub level is m−∑ixi, and the original chain lives on X.
Definitions.hiλ is defined as the value of (6); Proposition 3.2 is stated as "(6)'s value solves (5)". The Lagrangian policy is built from any optimal solutions of (6) at any optimal λ∗(δ), with the paper's controls (1 and 0) above the support.
Disclosed choices. Assumption 4.1 is assumed only at the δ in use. "Grow at the same rate" is κ1n≤m≤κ2n, with the constant C and the threshold N0 chosen before the network.
Non-vacuity. The goal includes an attainment clause: λ∗(δ), optimal solutions of (6) and a stationary distribution exist. A proof cannot pass through empty hypotheses, and suprema and infima are taken over nonempty, bounded index sets.
Not formalized. Proposition 2.1 (continuous-time utilisation), Proposition 2.2 (Bellman equation (2)), Lemma 4.8 (primitive sufficient conditions for Assumption 4.1), §5–§6 and the appendices on algorithms are not formalized.
Reusable pieces. The log-concavity and convolution vocabulary and Lemmas A.12/A.14 are independent of the model and reusable. Contributions to the class structure of finite birth–death product chains, and to Keilson's moment inequality (Lemma A.13), are welcome.
J. Keilson, A threshold for log-concavity for probability generating functions and associated moment inequalities, Annals of Mathematical Statistics 43(5), 1702–1708, 1972.
S. Janson, Tail bounds for sums of geometric and exponential variables, Statistics & Probability Letters 135, 2018. https://arxiv.org/abs/1709.08157
S. Banerjee, D. Freund, T. Lykouris, Pricing and optimization in shared vehicle systems: an approximation framework, 2016. https://arxiv.org/abs/1608.06819
A. Waserhole, V. Jost, Pricing in vehicle sharing systems: optimization in queuing networks with product forms, EURO Journal on Transportation and Logistics 5(3), 293–320, 2016.
Display Optimization for Vertically Differentiated Locations Under Multinomial Logit Preferences: Revenue Lower Bound for the Assignment Rounded from Dynamic-Programming ActionsResearch Paper
Motivation
Retailers, online travel agencies and search engines display products in an ordered list or on a physical layout, and customers inspect only a prefix of it. Display optimization asks how to assign products to positions so as to maximize expected revenue when each customer considers only the products shown in the first k positions, with k random. Aouad and Segev (SSRN 2709652; Management Science 67(6), 2021) study this problem with vertically differentiated locations (every customer who sees position k+1 also sees positions 1,…,k) and multinomial logit (MNL) choice within the consideration set. The model covers assortment planning over time and product framing on web pages, and it was calibrated on Expedia hotel-search data in the paper's case study.
The paper's headline claim (Theorem 1.1) is a polynomial-time approximation scheme, obtained by a dynamic program over approximate assortments followed by a rounding of its actions into an assignment. The rounding analysis, Section 5.2, contains a self-contained chain of combinatorial inequalities about the rounded assignment. That chain is the subject of this mission.
Setting
There are n items. Item i∈[n] has a price ri>0 and an MNL preference weight wi>0; write ρi=riwi and, for an assortment S⊆[n],
ρ(S)=i∈S∑ρi,w(S)=i∈S∑wi,R(S)=1+w(S)ρ(S),
the expected revenue of offering S to an MNL customer with a no-purchase option of weight 1. An assignmentA is a bijection from positions [n] to items; A[k] is the set of items in positions 1,…,k, Rk(A)=R(A[k]), and with position weights λk>0 the objective is
R(A)=k=1∑nλkRk(A).
The algorithm fixes an accuracy ϵ∈(0,1/5) and a guessed position kmid. A sequence of dynamic-programming actions consists of events e1,…,eT∈[n] and pairs (Sj−,Sj+) of item sets (a sub-assortment and a super-assortment), starting from e1=1, S1−=S1+={i1} and ending at eT=n, ST−=ST+=[n]. Consecutive actions must satisfy seven constraints, (8)–(14) of the paper: nestedness Sj−1−⊆Sj−1+⊆Sj+, the accuracy bounds ρ(Sj−1+∖Sj−1−)≤4ϵ2ρ(Sj−1−) and the same for w, a cardinality constraint linking sets to events, and three growth conditions on the proxies
αj=1+w(Sj+)ρ(Sj−)
depending on the position of ej−1,ej relative to kmid. With jmid the last index whose event is at most kmid, the actions are rounded into blocks Δ1,…,ΔT of new items (from Sj− before jmid, from Sj+ after), and the rounded assignmentA~ lists the blocks in order, each by non-increasing price. The block boundaries are e~j=∣Δ1∪⋯∪Δj∣, and I~j are the position intervals between consecutive boundaries, split at kmid.
Formalization targets
Goal: the rounded assignment dominates the DP proxies
For every 1≤kmid≤n−1, every feasible action sequence and every rounded assignment A~,
Claim 5.5: k↦Rk(A~) is unimodal on each [e~j,e~j+1].
Significance
The goal is the step that converts the dynamic program's value into a revenue guarantee for an actual assignment: whatever action sequence the dynamic program returns, the assignment built from it earns at least (1−8ϵ) times the interval-weighted minima of the program's proxies. Any repaired analysis of the scheme has to pass through a statement of this form, since the rounding of §4.4 is the only link between the program's actions and a display.
The remaining half of the paper's argument is not true as printed. Lemma 5.4, R(A~)≥(1−15ϵ)R(A∗), and with it the approximation clause of Theorem 1.1, fail for the paper's own algorithm: with n=4, w=(32,1,32,4), ρ=(4,16,64,8), λ=(0.85,0.45,0.40,0.34) and ϵ=1/80, no feasible action sequence can place item 2 first, and every rounded assignment earns at most 75364/16625≈4.53 against an optimum of 165804/16625≈9.97. A formal proof of the true half isolates precisely where the published argument stops working. No part of this chain has a machine-checked proof.
Difficulty
The rounding discards items. Before jmid, block Δj keeps only the part of the sub-assortment Sj− that is new with respect to Sj−1+, so the prefix of A~ can carry less ρ-mass than Sj−. A loss bounded by the per-step accuracy 4ϵ2 would accumulate over up to n steps; Lemma 5.2's constant 1−8ϵ is independent of T, and holds only because the growth constraint forces ρ(Sj−) to grow geometrically, which the obvious step-by-step bound does not use. The second obstacle is that the revenue between two block boundaries is not monotone; bounding it by the boundary values requires the unimodality of Claim 5.5, which depends on the price order inside each block and on the MNL convex-combination structure, not on the dynamic program.
Formalization scope
Items are Fin n; positions and DP indices are 1-based natural numbers as on the page, and an assignment is an equivalence Fin n ≃ Fin n from the 0-based position k−1 to the item at position k. A DP sequence stores events and set pairs as functions on ℕ, read through accessors implementing the root convention eT+1=eT, ST+1=ST and S0+=∅. Feasibility is exactly the boundary and root conditions plus (8)–(14), with (11) written without natural-number truncation and (14) in the lower-bound form printed on p. 19. The rounded assignment is a predicate: block contents fixed by Δj, non-increasing prices within a block, ties in any order.
Conventions and additions relative to the page:
1≤kmid≤n−1 is assumed. For kmid=n the construction of §4.4 can leave an item unplaced, so no rounded assignment exists and the statement would be vacuous.
The approximate assortments range over all subsets of [n] rather than the families of Lemma 2.5, events may repeat, and Assumptions 2.1–2.2 enter only as positivity of prices and weights. Each of these makes the statements stronger.
Every statement quantifies over all feasible action sequences, not only the optimal one.
Theorem 1.1, Lemma 5.4, Lemma 5.1 and inequalities (17)–(19) are not formalized, because they fail for the paper's algorithm (counterexample above).
Feasibility and rounding are the page's constructions; neither predicate builds in Lemma 5.2, Lemma 5.3 or any revenue property, so the goal cannot be obtained by unfolding a hypothesis. A sorry-free sanity check exhibits an instance (n=3, kmid=2) satisfying all hypotheses at once.
The development needs only finite sums over Finset, real arithmetic and induction over the block index. Contributions of all milestones are welcome; the identity and Claim 5.5 are reusable for any MNL ranking or display model.
Selected references
A. Aouad and D. Segev, Display Optimization for Vertically Differentiated Locations Under Multinomial Logit Preferences, Management Science 67(6):3519–3550, 2021; authors' version of 31/07/2019, SSRN 2709652. https://ssrn.com/abstract=2709652 — DOI https://doi.org/10.1287/mnsc.2020.3664
Heteroscedastic Exponomial Choice: Under Independent Exponential Utility Errors with Choice-Specific Rates, Every Choice Probability Is a Closed-Form ExponomialResearch Paper
Motivation
Random utility models are the standard way to turn utilities into demand in operations management, marketing and economics. A consumer facing n products assigns each a random utility and buys the one with the highest realization; the choice probabilities are the market shares that pricing and assortment models optimize. The multinomial logit, built on i.i.d. Gumbel errors, has closed-form choice probabilities, but its errors have the same variance for every product, and this forces the independence-of-irrelevant-alternatives property.
Alptekinoğlu and Semple (SSRN 3232788, forthcoming in Operations Research) replace the Gumbel errors by exponential errors with a product-specific rate. Uncertainty about a product's value can then differ across products, for example between a familiar brand and a new entrant. Their earlier exponomial choice model (Alptekinoğlu & Semple, Operations Research 64(1), 2016) is the special case of equal rates. The paper's first result is that this heteroscedastic model still has choice probabilities in closed form, a finite combination of exponentials of linear functions of the utilities. Its pricing analysis rests on that formula.
Setting
There are n≥2 choices, N={1,…,n}. Choice i gives the random utility
Ui=ui−zi,
where ui∈R is the ideal utility of choice i and zi is an exponential random variable with error rateλi>0, with density fi(z)=λie−λiz and distribution function Fi(z)=1−e−λiz for z≥0 (both 0 for z<0). The errors z1,…,zn are independent, and they are not identically distributed. Since zi≥0, the ideal utility is the largest utility choice i can ever deliver.
The choice probability of choice i is
Qi(u,λ)=P{ui−zi≥uj−zj∀j∈N,j=i}.
Write Bi={j:uj≥ui} and Bi+={j:uj>ui} for the choices that are better and strictly better than i, and Wi−={j:uj<ui} for the strictly worse ones. Let Li=∑j∈Biλj and Li+=∑j∈Bi+λj. The exponomial term of choice i is
Gi(u,λ)=Liλiexp[−j∈Bi∑λj(uj−ui)].
The proof also uses the distinct values a1<⋯<al of u1,…,un, and the sets B(x)={j:uj≥x}.
Formalization targets
Goal: Theorem 1 (p. 6)
For every i∈N,
Qi(u,λ)=Gi(u,λ)−k∈Wi−∑Lk+λi⋅Gk(u,λ).
The statement holds for arbitrary real utilities, ties included, and arbitrary positive rates.
Milestones
Equation (1), p. 6.Qi=∫0∞∏j=i[1−Fj(uj−ui+z)]fi(z)dz=∫0∞λiexp[−∑jλj(uj−ui+z)+]dz.
Display (16), p. 43. With ui=ak, this integral equals λi times a sum, over the levels ak,ak−1,…,a1, of differences of tail integrals ∫c∞exp[−∑j∈B(aw)λj(uj−ui+z)]dz.
The first integral, p. 43.λi∫0∞exp[−∑j∈Biλj(uj−ui+z)]dz=Gi.
The combined terms, pp. 43–44. For 1≤w<k, the two integrals from ak−aw combine to
The negative terms, p. 44. The term of level aw equals −∑k′∈Wi−,uk′=aw(λi/Lk′+)Gk′.
Significance
The result. Theorem 1 makes the HEC model usable. Every later result of the paper starts from (3): the continuity and the partial derivatives of Qi (Theorem 2), the expected consumer surplus (Theorem 3), log-concavity (Theorem 5), and the monopoly and oligopoly pricing results. Unlike the multinomial logit, the closed form shows how the rate of each worse product enters through Lk+, so substitution patterns are not proportional. With equal utilities it reduces to Qi=λi/(λ1+⋯+λn), and with equal rates it gives the exponomial model of 2016.
Formalizing it. The theorem is proved in the paper. The proof in Appendix C is short and leaves the integration steps to the reader. No machine-checked proof of the theorem or of any step of its proof is known. The mission asks for a complete Lean proof that starts from the probability itself, a product of exponential laws, so that the integral representation (1) is part of what is proved and not assumed. It also produces general facts about the maximum of independent shifted exponential variables, which have uses beyond this paper.
Difficulty
The obvious argument has two steps, and both hide work. Step one conditions on zi and integrates the product of survival functions. In Lean this is a computation of a product measure of a non-rectangular set, a Fubini argument over Rn with the marginal of one coordinate split off. Step two integrates a function exp[−∑jλj(uj−ui+z)+] whose exponent is piecewise linear with breakpoints at the gaps ui−uj. The breakpoints coincide when utilities tie, and the formula is stated through the distinct levels a1<⋯<al precisely to handle that. Regrouping the telescoping display (16) by level, and identifying each regrouped term with the strictly worse choices at that level, is bookkeeping over a sorted enumeration of a finite set. It is easy on paper and has to be done with care in Lean.
Formalization scope
Choices are Fin n. The errors are the coordinates of a point of Fin n → ℝ under Measure.pi (fun j => expMeasure (lam j)), Mathlib's product of exponential laws. Qi is the real value of this measure on the closed event {z:uj−zj≤ui−zi∀j=i}, with the weak inequality as printed. All values are real. Every statement assumes n≥2 and λj>0, the standing assumptions of p. 4. Integrals ∫c∞ are Bochner integrals over (c,∞). Lk+ is defined for every k, with value 0 at a choice of maximal utility, where the paper leaves it undefined; the theorems use it only for k∈Wi−, where it is at least λi>0. The levels a1<⋯<al are the increasing enumeration of the set of values of u, indexed from 0 in Lean.
Qi is defined as a probability. It is neither the integral (1) nor the closed form (3), either of which would make the goal a computation or a tautology.
A complete development needs the product-measure computation behind (1) and the exponential integral ∫c∞e−a−bzdz=e−a−bc/b. It also needs facts about sorted enumerations of finite sets of reals. The first two are reusable for any model with independent exponential errors. Proofs of the milestones in any order are welcome, as are alternative proofs of Theorem 1 that bypass them.
Not in scope: Corollary 1, Theorems 2–14 and the pricing results, which build on Theorem 1.
Selected references
A. Alptekinoğlu and J. H. Semple, Heteroscedastic Exponomial Choice, forthcoming in Operations Research; SSRN 3232788, version of August 8, 2020. https://ssrn.com/abstract=3232788 (journal DOI 10.1287/opre.2020.2074)
A. Alptekinoğlu and J. H. Semple, The Exponomial Choice Model: A New Alternative for Assortment and Price Optimization, Operations Research 64(1):79–93, 2016. https://doi.org/10.1287/opre.2015.1459
Distributed Stochastic Optimization with Large Delays: Under Polynomially Growing Delays, Asynchronous SGD with Tuned Step-Sizes Drives the Mean-Square Gradient Norm to ZeroResearch Paper
Motivation
Large-scale learning problems, such as empirical risk minimization over millions of samples, are solved in practice by stochastic gradient descent (SGD) run on many processors at once. In a master–worker system, or in a multi-processor system with shared memory, a worker reads the current parameter, computes a stochastic gradient and writes its update back. Other workers update the parameter in the meantime, so by the time a gradient is applied it is stale: it was evaluated at an older iterate. In heterogeneous clusters these delays are not bounded in any useful sense, and they can grow with the run.
The classical analyses of asynchronous gradient methods (Bertsekas and Tsitsiklis, Parallel and Distributed Computation, Prentice Hall 1989, reprinted by Athena Scientific 1997) and of asynchronous SGD for machine learning (Agarwal and Duchi, NeurIPS 2011; Recht et al., Hogwild!, NeurIPS 2011; Lian et al., NeurIPS 2015) assume bounded delays. Zhou, Mertikopoulos, Bambos, Glynn and Ye (arXiv:2107.02919, Mathematics of Operations Research, 2022) show that the delays may grow without bound, polynomially in the iteration count, as long as the step size shrinks to match. This mission formalizes their first main result, Theorem 1, on general nonconvex objectives.
Setting
Let (Ξ,μ) be a probability space and F:Rd×Ξ→R a random function. The objective is
f(x)=E[F(x;ξ)]=∫ΞF(x;ξ)dμ(ξ),
to be minimized over x∈Rd. Write ∇F(x;ξ) for the gradient of F(⋅;ξ) in x.
Assumption 1 asks that F(⋅;ξ) be differentiable for μ-almost every ξ, that the stochastic gradient have bounded second moment, supxE∥∇F(x;ξ)∥22≤B<∞, and that its mean x↦E[∇F(x;ξ)] be L-Lipschitz.
Distributed asynchronous SGD (DASGD, Algorithm 3 of the paper) starts at X0=x0 and updates
Xn+1=Xn−αn+1∇F(Xs(n),ωn+1),
where αn>0 are step sizes, (ωn) is an i.i.d. sequence with law μ, and s(n)≤n is the iteration at which the gradient applied at step n was requested. Its delay is n−s(n).
Assumption 2 couples delays and step sizes. It requires one of four regimes:
bounded delays, with ∑αn2<∞ and ∑αn=∞;
delays O(np) with 0<p<1, and αn∝1/n;
delays O(n), and αn∝1/(nlogn);
delays O(nq) with q≥1, and αn∝1/(nlognloglogn).
Formalization targets
Goal: Theorem 1
If Assumptions 1 and 2 hold and infxf(x)>−∞, then
n→∞limE[∥∇f(Xn)∥22]=0.
The goal covers all four regimes at once, through the disjunction in Assumption 2. It fixes no constant: B, L and the regime's parameters are arbitrary.
Milestones
Remark 1:f is differentiable, ∇f=E[∇F], and ∇f is L-Lipschitz.
The Jensen bound:∥∇f(x)∥22≤B.
(B.4):E∥∇f(Xs(n))−∇f(Xn)∥2≤LBˉ∑r=s(n)n−1αr+1, where Bˉ bounds E∥∇F∥2.
(B.5): the expected one-step descent inequality with its delay term.
Delay sums: in each of the four regimes, ∑nαn+12<∞ and ∑nαn+1∑r=s(n)n−1αr+1<∞, and ∑nαn+1=∞ in regimes 2–4. These are the paper's case (1) and (B.8), (B.9) and (B.10).
Lemma 1:∑nαn+1E∥∇f(Xn)∥22<∞.
Lemma 2:E∥∇f(Xn+1)∥22−E∥∇f(Xn)∥22≤Cαn+1.
Lemma A.4: if an,bn≥0, ∑an=∞, ∑anbn<∞ and ∣bn+1−bn∣≤Kan, then bn→0.
Significance
The result. For a general nonconvex smooth objective, convergence to a minimizer cannot be expected. The standard guarantee is that the gradient vanishes, and Theorem 1 gives it in mean square, which also implies convergence in probability of ∥∇f(Xn)∥2 to zero. The theorem shows that asynchronous SGD stays stable under delays that grow without bound, and it identifies the price: each step up in delay growth costs a logarithmic factor in the step size. A step size of order 1/(nlogn) is, up to a loglogn factor, sufficient for every polynomial delay process. The guarantee does not depend on whether the architecture is master–worker or shared-memory, since only s(n) enters.
Formalizing it. The paper proves the result, but no machine-checked version of any asynchronous or delayed SGD guarantee exists on Prove2Me or in Mathlib. A formal proof would check the step most prone to error in such analyses: the conditioning that makes a stale stochastic gradient unbiased given the past. The page's own chain before (B.5) has a constant slip (B where B belongs), which the printed (B.5) absorbs. The delay-sum estimates (B.8)–(B.10) are asymptotic computations with logarithms, and the paper states them with "∼Kˉ". The reusable parts are the differentiation-under-the-integral lemma (Remark 1) and the series lemma A.4.
Difficulty
Without delays, the descent inequality telescopes directly: the cross term ⟨∇f(Xn),∇F(Xn,ωn+1)−∇f(Xn)⟩ has zero conditional mean. With delays, the gradient is unbiased for ∇f(Xs(n)), not for ∇f(Xn). The discrepancy has to be paid for out of the step sizes accumulated over the delay window. When the window grows polynomially, it is a sum over polynomially many past steps, and finiteness of the total penalty depends on the precise step-size law. A cruder bound that ignores the logarithmic factors fails in regimes 3 and 4.
A second obstacle is that a finite weighted sum ∑αn+1E∥∇f(Xn)∥22<∞ gives only a liminf. The paper's own counterexamples (p. 10) show that it does not imply convergence. The increment bound of Lemma 2 is what closes the gap.
Formalization scope
Space and gradients.Rd is EuclideanSpace ℝ (Fin d), and ∇ is Mathlib's gradient. gradient returns 0 at points of non-differentiability, so the goal also asserts that f is differentiable.
Probability spaces. The noise space (Ξ,μ) carries F. A separate probability space (Ω,P) carries the i.i.d. sequence ωn (measurable, independent, each with law μ).
Iterates. The iterates are characterized by the recursion as a hypothesis, which has exactly one solution.
Delays. The delay schedule s is deterministic with s(n)≤n. "dn=O(nq)" is read on received gradients as n−s(n)≤K(s(n)+1)q.
Step sizes. "αn∝φ(n)" means αn=cφ(n) for all n from some N on, with every αn>0.
Moments.B and L are named parameters: square integrability together with the bound B, and L-Lipschitzness of E[∇F].
Disclosed additions.F(x;⋅) is integrable, and (x,ξ)↦∇F(x;ξ) is jointly measurable.
Integrability. Every expectation in a conclusion carries its integrability as a conjunct.
A Lean integral of a non-integrable function is 0, and gradient is 0 where f is not differentiable. Those conjuncts are there so that the goal cannot be proved through either junk value. The goal is also stated for all four regimes, with the delay inside the recursion, so it is not the classical bounded-delay theorem.
A complete development needs:
conditional expectation against the past iterates and independence of ωn+1 from X0,…,Xn;
the descent lemma for L-smooth functions;
differentiation under the integral sign;
asymptotic estimates for sums of 1/(rlogrloglogr).
Contributions of the real-analysis milestones (Lemma A.4, the delay sums) are welcome independently of the probabilistic ones.
Selected references
Z. Zhou, P. Mertikopoulos, N. Bambos, P. W. Glynn, Y. Ye, Distributed Stochastic Optimization with Large Delays, Mathematics of Operations Research, 2022; arXiv:2107.02919v1. https://arxiv.org/abs/2107.02919
D. P. Bertsekas, J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989; reprinted by Athena Scientific, 1997.
B. Recht, C. Ré, S. Wright, F. Niu, Hogwild!: A Lock-Free Approach to Parallelizing Stochastic Gradient Descent, NeurIPS 2011. https://arxiv.org/abs/1106.5730
X. Lian, Y. Huang, Y. Li, J. Liu, Asynchronous Parallel Stochastic Gradient for Nonconvex Optimization, NeurIPS 2015. https://arxiv.org/abs/1506.08272
Tail-Optimized Caching for LLM Inference: Expected-Tail-Optimized LRU Is an Optimal Online Caching Policy for Tail Excess Latency in the Stochastic Conversation ModelResearch Paper
Why caching policy matters for LLM serving
A large language model serving a multi-turn conversation re-reads the whole conversation history at every turn. The intermediate attention state of that history, the KV cache, can be stored in GPU memory and reused, so that only the uncached part of the prompt must be recomputed before the first output token appears. GPU memory is scarce, so a server must decide, after every turn, which blocks of which conversations to keep. Production systems such as vLLM (Kwon et al., 2023) use least-recently-used (LRU) eviction for this (vLLM prefix caching).
Service-level objectives for LLM inference are written in terms of tail latency: the fraction of requests whose time-to-first-token exceeds a threshold. Zhang, Li, Moallemi and Peng (arXiv:2510.15152v1, 2025) measure this by the Tail Excess Latency (TEL) of a request: the number of uncached blocks above a threshold. They propose a variant of LRU aimed at the tail and prove that its expected version is optimal in a stochastic model of conversation arrivals. This mission formalizes that optimality theorem, Theorem 2 of the paper, together with the steps of its proof.
The stochastic conversation model
The cache holds C blocks. A request of conversation θ whose history has length Lθ, whose new prompt has length Q and of which Xθ blocks are cached pays the Tail Excess Latency
TEL=(Lθ+Q−Xθ−ξ)+,
where ξ≥0 is the latency threshold expressed in blocks.
Conversations are born at rate λconv>0 and die at rate μ>0. While active, conversation i sends requests as a Poisson process of rate λˉi>0. Each prompt length Qi is drawn from a known, possibly conversation-specific law; each response length Ai from an arbitrary law. Caches are not shared between conversations.
Deaths are never observed, so the decision-maker keeps a belief turn-arrival rateλi=λˉie−μ(t−last turn of i) for each conversation. The belief state is (λ,L,X): belief rates, conversation lengths and cached blocks of the conversations that have arrived so far. Between arrivals every λi is multiplied by the decay factor d=e−μτ, where τ is the inter-arrival time. The next request comes from conversation j with probability λj/(λconv+∑iλi), or from a new conversation with probability λconv/(λconv+∑iλi). After serving conversation θ with prompt Q and response A, its rate resets to λˉθ, its length grows by Q+A, and the server chooses a new cache vector Y subject to
Yθ≤Lθ+Q+A(9),Yi≤Xi(i=θ)(10),∑iYi≤C.
The belief update is the paper's: it decays the return rate with elapsed time and does not otherwise condition on the observed silence.
the cache that minimizes the expected TEL of the next turn under the current beliefs.
Formalization targets
Goal: Theorem 2
For every ET-LRU policy σ (any tie-break), every policy π whose decisions always satisfy (9), (10) and the capacity constraint, every number M of requests and every well-formed belief state z,
Ezσ[k=1∑MTELk]≤Ezπ[k=1∑MTELk].
Milestones
The next-turn expected TEL equals the objective of (8), up to normalization and a term no decision affects (§5, pp. 8–9).
The finite-horizon Bellman optimum VM⋆ of App. B lower-bounds the value of every admissible policy (p. 17).
The marginal-cost identity P(Li+Qi−ξ≥Xi)=E[(Li+Qi−ξ−(Xi−1))+]−E[(Li+Qi−ξ−Xi)+] (p. 19).
Lemma 1: the greedy token-by-token eviction of Algorithm 2 solves (8) (pp. 19–20).
The exchange inequality: evicting a token from a conversation of strictly smaller ranking score λiP(Li+Qi−ξ≥Xi) never increases the optimal cost-to-go (pp. 18–19).
ET-LRU attains VM⋆ from every well-formed state (pp. 17–19).
Milestones 2 and 6 together give the goal.
Significance
ET-LRU is myopic: it looks one turn ahead. Theorem 2 says that in this model nothing is lost by myopia over any horizon. Setting ξ=0 with homogeneous rates turns (8) into "keep the blocks of the most recently active conversations", so the theorem yields an optimality statement for LRU for average latency. With deterministic prompt lengths it yields the optimality of the paper's Tail-Optimized LRU. With zero prompt and response lengths after the first turn it reduces to unit-page caching (p. 9), the setting in which Belady (1966) characterized the offline optimum. The paper reports that no such optimality result for LRU under stochastic arrivals had been established before.
The result is proved in the paper; nothing in it is machine-checked. A formalization adds a checked statement of the model (arrival law, belief dynamics, constraints and objective), whose conventions are easy to get wrong in prose, and a checked version of an exchange argument that the paper gives in compressed form. The greedy implementation (Lemma 1) is an instance of separable convex resource allocation and is reusable on its own.
Difficulty
The obvious argument compares ET-LRU's decision with another feasible decision and charges the difference to the next turn alone. That fails: a cache choice changes the state from which every later decision is made, and a cheaper next turn could in principle leave a worse state. The proof must show that the ranking of conversations by λiP(Li+Qi−ξ≥Xi) is consistent with the optimal cost-to-go at every later stage, under every possible next arrival, including arrivals that refill a conversation's cache and arrivals of new conversations. Ties in the ranking require care: two evictions of equal current score can have different future costs.
The invariant λi≤λˉi (a belief rate never exceeds the rate a conversation resets to) holds on every reachable state and is needed: exact dynamic-programming computations find states with λi>λˉi from which ET-LRU is not optimal.
Formalization scope
Everything lives in the namespace TailOptCaching.ETLRU, in one definitions file and eight theorem files.
Indices. Conversations are numbered 0,1,… in arrival order (the paper's 1,2,…); with n arrived conversations the next new one is n.
Values in [0,∞]. Costs and values are ℝ≥0∞; (z)+ is ENNReal.ofReal z; expectations over prompt and response lengths (laws PMF ℕ) are tsums, and the expectation over the decay factor is a lintegral. If a prompt-length law has infinite mean, every value is ∞; that is the correct reading, not a loophole.
Decay law. The law of d=e−μτ is any probability law on (0,1] that depends on the belief rate vector. The paper's law (inter-arrival hazard λconv+e−μs∑iλi) is one such law, so the statements cover the paper's model.
Policies are Markov and deterministic: functions of the stage, the belief state and the current arrival (θ,Q,A). ET-LRU is any policy whose every decision minimizes (8); its existence is a separate item.
Well-formed states: 0<λi≤λˉi for arrived conversations, Xi≤Li, ∑iXi≤C, and zeros beyond the arrived conversations.
Integer thresholdξ∈N is assumed in milestones 3–5, where the ranking criterion must equal the marginal cost; the goal and milestones 1, 2 and 6 allow any real ξ≥0.
Ties and binding capacity. The exchange milestone uses a strict inequality between scores, and is stated for a cache that exceeds the capacity by exactly one token (the page's setting); with slack capacity the comparison can fail.
The goal must not be trivialized: the horizon M is arbitrary (with M=1 the claim is the definition of ET-LRU), the competing policy is any admissible policy, not one of index type, the decay factor is not fixed to 1, and the Bellman optimum is defined independently of ET-LRU.
Not formalized here: Theorem 1 (the hindsight-optimal policy, App. A), the forced-caching variant (App. C) and the experiments. Contributions of proofs of any milestone are welcome. The finite-horizon Bellman machinery and the greedy allocation lemma are the parts most likely to be reused.
Selected references
W. Zhang, Y. Li, C. C. Moallemi, T. Peng, Tail-Optimized Caching for LLM Inference, arXiv preprint, 2025. https://arxiv.org/abs/2510.15152v1
L. A. Belady, A study of replacement algorithms for a virtual-storage computer, IBM Systems Journal 5(2), 1966. https://doi.org/10.1147/sj.52.0078
Self-adjoint differential operators assosiated with self-adjoint differential expressions: Self-Adjoint Extensions Are Restrictions of the Adjoint Cut Out by m Asymmetry-Form ConditionsResearch Paper
Why self-adjoint extensions
In quantum mechanics an observable is a self-adjoint operator, not just a symmetric one. A differential expression such as −d2/dx2 on an interval or a half-line first defines a symmetric operator on smooth functions with compact support, and this operator usually has many self-adjoint extensions or none. Each extension is a different physical theory, with its own spectrum and dynamics, and choosing one amounts to choosing boundary conditions. Voronov, Gitman and Tyutin (arXiv:quant-ph/0603187) give a self-contained account of this problem written for physicists. Its abstract result is a description of all self-adjoint extensions that does not require computing the deficient subspaces.
Timeline. von Neumann (1929–30) classified the self-adjoint extensions of a closed symmetric operator through isometries between its deficient subspaces. The classical treatments are Akhiezer–Glazman and Naimark (Linear Differential Operators), and the Cayley-transform form is in Teschl's Mathematical Methods in Quantum Mechanics (2009), Theorem 2.26. Voronov, Gitman and Tyutin (2006) restate the finite-index case as a restriction of the adjoint by asymmetry-form conditions (their Theorem 3, (35)). They then remove the deficient subspaces from the description altogether (Theorem 15). For differential operators this gives self-adjoint boundary conditions in terms of boundary forms (Theorem 16).
Setting
Let H be a complex Hilbert space whose inner product (⋅,⋅) is linear in the second argument. Let f^ be a linear operator with domain Df⊆H. It is symmetric if Df is dense and (η,f^ξ)=(f^η,ξ) for all ξ,η∈Df. It then has an adjoint f^+ extending it and a closure fˉ with domain Dfˉ, and f^⊆fˉ⊆f^+. An operator g^ is self-adjoint if g^+=g^, domains included.
The deficient subspaces are D+=ker(f^+−i) and D−=ker(f^++i). The deficiency indices are m±=dimD±.
The asymmetry form of the adjoint is the sesquilinear form on Df+
ω∗(η∗,ξ∗)=(η∗,f^+ξ∗)−(f^+η∗,ξ∗).
It vanishes identically exactly when f^+ is symmetric.
Vectors w1,…,wm∈Df+ are linearly independent modulo Dfˉ if ∑kckwk∈Dfˉ forces c1=⋯=cm=0. Given such vectors, f^U denotes the restriction of f^+ to their joint ω∗-annihilator:
Theorem 3, existence (p. 19): self-adjoint extensions exist iff m+=m−. This one is already proved on the platform and is referenced.
Theorem 3, (33)–(35) (p. 20): for U∈U(m) and eU,k=e+,k+∑lUlke−,l, the self-adjoint extensions are exactly the operators cut out by the eU,k, and distinct U give distinct extensions.
(141) (p. 65) and (142)–(143) (p. 66): the eU,k are admissible, and admissibility and the cut-out operator are invariant under wk↦∑aXakwa+ξk with detX=0 and ξk∈Dfˉ.
Proof of Theorem 15, pp. 67–68: for admissible wk=∑aXake+,a+∑aYake−,a+ξk, both X and Y are nonsingular and YX−1 is unitary.
Significance
The result. Theorem 15 lists all self-adjoint extensions of f^ as solutions of m linear conditions on Df+. The vectors wk can be any vectors of the adjoint's domain satisfying two checkable conditions. For a differential operator, ω∗ reduces to a boundary form [wk,ψ]ab, and Theorem 16 of the paper turns Theorem 15 into a recipe for self-adjoint boundary conditions that never solves f^+ψ=±iψ. In von Neumann's parametrization that equation must be solved, and doing so is often the hardest part of a concrete calculation. The price is redundancy: families related by a nonsingular matrix give the same extension.
Formalizing it. The mathematics is known: von Neumann's theory is classical and Theorem 15 is proved on pp. 65–68. The Prove2Me platform has Teschl's Cayley-transform version of the existence criterion as a machine-checked proof. To our knowledge, the first von Neumann formula for LinearPMap, the asymmetry-form description of the closure, and the unitary-matrix parametrization are not formalized in Mathlib or on the platform. This mission produces those statements, together with Theorem 15 itself.
Difficulty
The forward direction rests on the unitary parametrization of Theorem 3, which in turn rests on the direct-sum decomposition of Df+. Each of these steps requires working with Dfˉ rather than Df, because f^ need not be closed. The converse is the substantial part. Linear independence modulo Dfˉ and isotropy ω∗(wk,wl)=0 are conditions on the wk as whole vectors. They say nothing directly about the deficient components, and relating an arbitrary admissible family to the deficient-subspace description of Theorem 3 is where the work lies. A count of dimensions alone does not give self-adjointness. Showing that a restriction of f^+ is symmetric is easy; showing that its adjoint is no larger than itself is not.
Formalization scope
H is a complex Hilbert space (InnerProductSpace ℂ H, CompleteSpace H), and operators are LinearPMaps H →ₗ.[ℂ] H. The adjoint, closure, extension order and self-adjointness are Mathlib's f.adjoint, f.closure, f ≤ g and IsSelfAdjoint g (g† = g). Mathlib's inner product is conjugate-linear in the first slot, as in the paper.
Symmetry is the published TeschlQM.Shared.IsSymmetric, which includes density. The initial operator is not assumed closed.
Deficient subspaces are kernels of the adjoint at z=i: kerAdd f.adjoint (-I)=ker(f+−i) and kerAdd f.adjoint I=ker(f++i), from the published TeschlQM.SelfAdjoint.addScalar. The index hypotheses are Module.finrank … = m with 0 < m, which forces both indices to be finite. Theorem 1 and (18)–(19) keep a general z with Imz=0, as the paper does.
ω∗ (asymForm) is defined only on f.adjoint.domain. Families are indexed by Fin m. Linear independence is modulo f.closure.domain. The operator (144) is cutOut f w, which is f.adjoint restricted to the annihilator.
The goal is not trivialized by its encoding. The extension in (144) is f^+ restricted to an explicitly defined subspace, not an operator chosen to fit. The conclusion is genuine self-adjointness, g†=g, not symmetry on the cut-out domain. Without the hypothesis m>0, an index with infinite-dimensional deficient subspaces would satisfy finrank = 0, so that hypothesis is kept.
A complete development needs the following: the first von Neumann formula for unbounded LinearPMaps; closures of symmetric operators; the identity Ran(f−z)⊥=ker(f+−zˉ); and the unitary-matrix parametrization. These are reusable beyond this mission, for example for Sturm–Liouville realizations and Theorem 16 of the paper. Contributions of any of them are welcome, as are proofs routed through the published Cayley-transform results.
Selected references
B. L. Voronov, D. M. Gitman, I. V. Tyutin, Self-adjoint differential operators assosiated with self-adjoint differential expressions, preprint, 2006. https://arxiv.org/abs/quant-ph/0603187 (v2 is the cited version)
J. von Neumann, Allgemeine Eigenwerttheorie Hermitescher Funktionaloperatoren, Math. Ann. 102 (1930), 49–131. https://doi.org/10.1007/BF01782338
N. I. Akhiezer, I. M. Glazman, Theory of Linear Operators in Hilbert Space, Dover, 1993 (reprint of the 1961/1963 translation).
M. A. Naimark, Linear Differential Operators, Part II, Ungar, 1968.
G. Teschl, Mathematical Methods in Quantum Mechanics, Graduate Studies in Mathematics 99, AMS, 2009, Theorem 2.26. https://doi.org/10.1090/gsm/099
Online Hypergraph Matching with Delays: Randomized Batching with Depth-k Greedy Is 1/d-Competitive for Online-(k, d)-Max-MatchingResearch Paper
Motivation
Ride-pooling platforms receive trip requests one at a time and must decide, within a short waiting window, which requests to group into a shared vehicle. A request that is not grouped before its window closes is served alone or lost. Online hypergraph matching with delays is the combinatorial core of this decision: requests are vertices that arrive over time, feasible groups of up to k riders are weighted hyperedges, and the platform must commit irrevocably to disjoint groups while every member of a group is still waiting. Pavone, Saberi, Schiffer and Tsao (arXiv:2009.12022, 2020; journal version Technical Note — Online Hypergraph Matching with Delays, Operations Research, 2022) determine the optimal competitive ratio of this problem in the utility-maximization setting. For k≥3 no online algorithm beats ratio 1/d, where d is the waiting time (their Theorem 1, via the adversarial secretary problem), and their Theorem 3 achieves 1/d with a polynomial-time algorithm for every fixed k. This mission formalizes the achievability half.
Setting
Requests 1,…,n arrive one per time step; request i arrives at time i and disappears at time i+d. A hyperedgee is a non-empty set of requests, its diameter is diam(e)=maxe−mine, and each hyperedge carries a weight w(e)≥0. A shareability hypergraph with parameters (n,d,k) is a finite edge set E of subsets of [n]={1,…,n} with diam(e)<d and ∣e∣≤k for all e∈E (Definition 1, p. 2). A matching is a set M⊆E of pairwise disjoint hyperedges, of weight w(M)=∑e∈Mw(e). In Online-(k, d)-Max-Matching (Definition 2, p. 3) a hyperedge may be chosen only after all its vertices have arrived and before any of them disappears, and choices are irrevocable.
Greedy (Algorithm 5, p. 15) scans a finite edge set in non-increasing order of weight, ties broken arbitrarily, and keeps every edge disjoint from those already kept.
Randomized-Batching (Algorithm 1, p. 5) draws a shift Z uniformly from {0,…,d−1} and cuts time into windows
Vz,i={v∈[n]:z+id≤v≤z+(i+1)d−1},i∈Z,
with batch edgesEz,i={e∈E:e⊆Vz,i} and Ez=⋃iEz,i. At the end of each window it runs an offline subroutine on the batch Wz,i=(Vz,i,Ez,i,w) and commits the result Mz,i; the output is Mz=⋃iMz,i.
Depth-k Greedy (Algorithm 2, p. 7) is the subroutine. With L and R the first and last k vertices of the batch, it enumerates the restricted matchingsML,R (Definition 18, p. 19), the matchings whose every edge meets both L and R; it extends each M∈ML,R by Greedy on the edges avoiding the vertices of M, and it returns the heaviest extension.
Formalization targets
Goal: Theorem 3, p. 7 (competitive clause)
For every shift z, Mz is a matching of E whose edges each lie inside one window, and for every matching M of E
EZ[w(MZ)]=d1z=0∑d−1w(Mz)≥dw(M).
The statement holds for every weight-sorted tie-breaking of Greedy.
Milestones
With Mℓ={e∈M:diam(e)>d−k} and Ms=M∖Mℓ:
Batch decomposition (proof of Theorem 2, p. 6): the windows partition [n], the batches are disjoint, and w(Mz)=∑iw(Mz,i).
Observation 1 (p. 6): ∑z=0d−11[e∈Ez]≥d−diam(e).
Lemma 4 (p. 14): Greedy returns a matching G with w(G)≥k1w(M) for every matching M of a rank-k hypergraph.
Observation 3 (p. 19): an edge of a window with diam(e)>d−k meets both L and R.
Condition (3) for Depth-k Greedy (p. 19): w(Mz,i)≥w(Mℓ∩Ez,i)+k1w(Ms∩Ez,i).
Reduction (4) (p. 18): any subroutine satisfying (3) on every batch gives d1∑z∑iw(Mz,i)≥w(M)/d.
Significance
Theorem 3 closes the gap left by the general guarantee of Theorem 2 and Lemma 2 (p. 6), under which any ρ-competitive offline subroutine yields ratio ρ/d. With plain Greedy this gives only 1/(kd) (Corollary 1, p. 7), and an exact subroutine gives 1/d but is NP-hard for k≥3. Together with the 1/d upper bound of Theorem 1, Theorem 3 settles the optimal competitive ratio of Online-(k, d)-Max-Matching for k≥3 and shows that it is attained in polynomial time for each fixed k. The batching-plus-restricted-enumeration pattern applies to other online problems in which items have a bounded lifetime.
The result is proved in the paper. To our knowledge none of it is machine-checked: no hypergraph matching model, no Greedy guarantee for weighted k-set packing, and no batching argument exists on the platform. Lemma 4, the classical 1/k guarantee of Greedy for weighted rank-k hypergraph matching, is cited in the paper without proof ([6, 8]); its formalization is reusable on its own.
Difficulty
The natural attempt is to run Greedy inside each batch. It loses the factor 1/k on every edge, and the random shift recovers that factor only for edges that survive batching for at least k of the d shifts, that is, edges of diameter at most d−k. A long edge, with diameter above d−k, lies in Ez for fewer than k shifts, so its 1/k loss is never compensated and the bound degrades to 1/(kd). Long edges therefore have to be recovered exactly in every batch. The exact optimum is intractable, so a different handle on long edges is needed. The formal work also has to deal with windows truncated at the ends of [n], with the first partial window, and with arbitrary tie-breaking inside Greedy.
Formalization scope
Vertices are natural numbers and V=[n]; hyperedges are Finset ℕ, edge sets are Finset (Finset ℕ), and weights are a function Finset ℕ → ℝ, read only on E. The definitions file HyperMatchDelay.Batching.Model fixes these conventions:
Hyperedges are non-empty, an assumption the paper leaves implicit. d≥1 and k≥1 are hypotheses.
Greedy's arbitrary tie-breaking is an ordering oracle σ listing each edge set in non-increasing weight order. Every statement about Greedy holds for every such oracle, independently in every call.
Windows are indexed by i∈{−1,0,…,⌊n/d⌋} and are pairwise disjoint. This replaces the paper's 0≤i≤n/d, which misses the first z requests, and Algorithm 1's overlapping last batch.
Definition 18's condition L∩R=∅ is dropped. It fails for batches with fewer than 2k vertices and no argument uses it.
The maximizer in Depth-k Greedy is a fixed choice; all maximizers have the same weight.
The expectation over Z is the average d1∑z=0d−1, and the long/short threshold diam(e)>d−k is compared in Z.
The running-time clauses of Theorem 3 and Lemma 4 are not formalized, since there is no cost model. The goal does not assume condition (3) as a hypothesis, and its subroutine is Depth-k Greedy as defined, with Greedy inside it. A single batch containing all of E, or an exact offline subroutine, would make the statement a different and easier claim, and the formalization rules both out.
Contributions are welcome on every milestone. Lemma 4 and Observation 1 are independent of the rest. Lemma 4 is the most reusable item: a general Greedy guarantee for weighted set packing.
Selected references
M. Pavone, A. Saberi, M. Schiffer, M. W. Tsao, Online Hypergraph Matching with Delays, arXiv:2009.12022v1, 2020. https://arxiv.org/abs/2009.12022 (page and theorem numbers in this mission refer to this version; page numbers equal PDF page indices).
M. Pavone, A. Saberi, M. Schiffer, M. W. Tsao, Technical Note — Online Hypergraph Matching with Delays, Operations Research, 2022 (journal version; not consulted for this mission).
P. Berman, A d/2 approximation for maximum weight independent set in d-claw free graphs, Nordic Journal of Computing 7(3), 178–184, 2000 (reference [6] of the paper, cited for Lemma 4).
B. Chandra, M. M. Halldórsson, Greedy local improvement and weighted set packing approximation, Journal of Algorithms 39(2), 223–240, 2001 (reference [8] of the paper, cited for Lemma 4).
Efficient Allocations in Double Auction Markets: Repeated Double Auctions Drive the Consumer Surplus to Zero at Rate 1/t and Their Cluster Points Are Individually Rational Pareto AllocationsResearch Paper
Motivation
Double auctions match buy and sell orders at a common price. Stock exchanges, commodity markets and electricity markets use them at their opening and closing auctions and to trade multi-asset portfolios. Economists have long asked how efficient the resulting allocations are. Laboratory work starting with Smith (1962) found that repeated double auctions with few traders reach competitive outcomes quickly (Smith 1962). Since then the phenomenon has been documented in many experimental studies, but it had remained largely unexplained by theory (Pennanen, §1).
Pennanen (arXiv:2001.02071v2, Mathematics of Operations Research 2022) takes agents who bid their indifference prices in a multi-asset double auction, and shows that repeating the auction drives the economy to an efficient allocation. The total surplus left on the table decays like 1/t.
Setting
A finite nonempty set I of agents trades a finite set J of assets. Agent i holds a portfolio xi∈RJ, and an allocation is x∈RI×J. Short positions are allowed and there is no free disposal. Agent i has a utilityui:RJ→[−∞,+∞] with effective domain domui={xi∣ui(xi)>−∞}. All prices are quoted in a numeraire portfoliog∈RJ, for example cash.
Assumption 1 holds throughout: each ui is upper semicontinuous and concave (its hypograph is convex), and ui(xi+rg)>ui(xi) for xi∈domui and r>0.
At the endowment xi0, agent i bids the indifference price
Di(xi)=sup{r∈R∣ui(xi0+xi−rg)≥ui(xi0)},
the most the agent would pay for xi without losing utility. The auctioneer solves the market clearing problem
maximize i∈I∑Di(xi)subject toi∈I∑xi=0,(P)
whose optimum value CS(x0) is the total consumer surplus available at x0. A market clearing price is a vector p that is a supergradient of every Di at a solution xˉ. Agent i then receives xˉi and pays p⋅xˉi units of g. An allocation with CS(x)=0 is a double auction equilibrium.
In the repeated auction the agents re-bid from their new positions:
xit=xit−1+xˉit−(pt⋅xˉit)g,
where xˉt and pt clear the t-th auction, whose indifference prices are built from xt−1.
Two further conditions are used. Assumption 3: no nonzero x with ∑ixi=0 has every xi a direction of recession of ui. Assumption 5: for every r>0 there is δi>0 with ui(xi+rg)≥ui(xi)+δir on the ball B(r). Assumption 4, which is needed only for Pareto efficiency, says that an agent who is not at the lowest possible utility can give away a little of g and stay in domui.
Formalization targets
Goal: Theorem 16
Under Assumptions 1, 3 and 5:
the iterates (xt) are bounded;
CS(xt) decreases to 0, with
CS(xt)≤t1i∈I∑δiui(xit)−ui(xi0);
every cluster point xˉ is a double auction equilibrium and is individually rational, ui(xˉi)≥ui(xi0);
under Assumption 4, every cluster point is also Pareto efficient.
The constants δi are those of Assumption 5 at one radius R that is large enough for the whole sequence. The statement holds for every admissible choice of them.
Milestones
The milestones are the results that the proof of Theorem 16 uses, in attack order:
Lemma 2: regularity of Di.
Theorem 4: market clearing prices are Lagrange multipliers.
Remark 6: every auction is a Pareto improvement.
Lemma 9: (P) recast in terms of utilities.
Monotonicity of CS along individually rational reallocations.
Boundedness of the set of feasible individually rational allocations.
The radius reduction in Assumption 5.
The per-auction utility gainui(xit)≥ui(xit−1)+δiCSi(xt−1).
Theorem 11: Pareto allocations coincide with double auction equilibria.
Significance
Theorem 16 is a welfare theorem for a mechanism that is actually used. Agents bid myopically, nobody computes a Walrasian equilibrium, and the allocation still becomes efficient. The result also gives a convergence rate. Together with Theorem 11 it identifies the limits of the mechanism with the Pareto allocations, so studying where repeated auctions end up comes down to studying Pareto efficiency.
The theorem is proved in the paper. No part of it, and none of its model, has a machine-checked proof. The formalization would check an argument that runs entirely in extended-real convex analysis, with utilities that may take the value −∞, such as Cobb–Douglas utilities on the positive orthant. It would also settle points the printed proof leaves implicit. One is the radius at which Assumption 5 is applied. Another is that the endowments must lie in the utility domains, which some lemmas need explicitly.
Difficulty
The obvious route bounds each agent's gain per auction by δi times the agent's surplus and then telescopes. That route needs a single constant δi valid along the whole sequence, which in turn needs the iterates and the surpluses to be bounded in advance. Boundedness is the step a newcomer cannot get from compactness or from Lipschitz estimates. It comes from recession analysis of the superlevel sets of upper semicontinuous concave extended-real functions, through Rockafellar's characterization of bounded closed convex sets. Mathlib has none of this.
A second difficulty is attainment. Several steps use ui(xi0+xˉi−Di(xˉi)g)≥ui(xi0), so the supremum defining Di must be attained. Attainment comes from upper semicontinuity, not from the definition. The cluster-point claims also need upper semicontinuity, in order to pass the monotone utilities to the limit.
Formalization scope
Utilities are functions (J → ℝ) → EReal, with I, J finite types and I nonempty. Concavity is convexity of the real hypograph, which is Rockafellar's definition. Mathlib's ConcaveOn does not apply because EReal is not a module. The indifference price and CS are EReal suprema. A supergradient requires D(xˉ) to be finite, which is Rockafellar's convention. Without that requirement a bid of +∞ would satisfy (4) vacuously and the goal would be trivial.
ui∞(d)≥0 is encoded as the property that λ↦ui(x+λd) is nondecreasing for every x∈domui, which the paper quotes from Rockafellar's Theorem 8.6. B(r) is the closed sup-norm ball. The paper fixes no norm, and Assumptions 2 and 5 are unaffected by the choice.
The sequence in Theorem 16 is any sequence the mechanism generates: purchases and prices satisfying the market clearing conditions at the current allocation. Existence of solutions and prices is not part of the goal. The rate is stated with the real values of ui(xit) and ui(xi0). Proving these values finite is part of the proof, and nothing in the statement assumes it.
The goal must not be trivialized. Bounded iterates, finite utilities along the sequence and CS(xt)→0 are conclusions, not hypotheses. The constants δi are universally quantified at a radius whose existence is claimed, not chosen existentially.
The following additions are disclosed on the items concerned. Lemma 2, the boundedness milestone and the first half of Theorem 11 assume xi∈domui, without which they fail. Lemma 9's solution correspondence assumes a finite optimum value.
The development needs extended-real concave analysis: upper semicontinuous concave functions, their recession cones, and attainment of suprema. This layer is reusable beyond this mission. Contributions are welcome on any milestone. The recession-cone boundedness and Lemma 9 are good entry points.
Selected references
T. Pennanen, Efficient allocations in double auction markets, Mathematics of Operations Research, 2022; arXiv:2001.02071v2. https://arxiv.org/abs/2001.02071v2
Model-Free Bounds for Multi-Asset Options Using Option-Implied Information and Their Exact Computation: Under No-Arbitrage with Bid–Ask Spreads, the Superhedging Price ϕ(f) Equals sup_{μ∈Q} ∫f dμResearch Paper
Motivation
A trader who quotes an exotic option written on several underlying assets (a basket call, a spread option, a best-of option) needs a price range that does not rest on a particular stochastic model. What is observed in the market is a finite set of liquid derivatives (vanilla calls and puts on each asset, and possibly some traded basket options), each with a bid price and an ask price. A model-free price bound for the exotic payoff is the range of prices consistent with these quotes and with the absence of arbitrage. Its upper end can be computed in two ways: as the cheapest static portfolio in the traded derivatives that dominates the payoff in every state of the world, or as the largest expected payoff over all probability measures that price the traded derivatives inside their bid–ask spreads.
The equality of these two numbers is a superhedging duality. For a single asset with exact (zero-spread) prices it goes back to the model-independent pricing literature of Hobson and others; Bouchard and Nutz (2015) proved a one-period duality and a fundamental theorem in a nondominated framework without spreads. Neufeld, Papapantoleon and Xiang (arXiv:2006.14288, Management Science 2023) extend the one-period result to a market where the derivatives are traded with bid–ask spreads and the payoffs are arbitrary Borel functions on a Polish state space, and then use the minimisation side to compute bounds exactly by cutting-plane algorithms.
Setting
Let Ω be a Polish space with its Borel σ-algebra, and let P(Ω) be the set of all Borel probability measures on Ω; there is no reference measure. Fix m∈N traded derivatives with Borel payoffs g1,…,gm:Ω→R, collected in g:Ω→Rm, with bid pricesπj and ask pricesπj, πj≤πj.
A static position y∈Rm pays ⟨y,g⟩(ω)=∑jyjgj(ω) and costs
π(y)=j=1∑myj+πj−yj−πj,
since long positions are bought at the ask and short positions sold at the bid. The cost π is sublinear, not linear.
No-arbitrage (Assumption 2.1): for every y∈Rm, if ⟨y,g⟩(ω)−π(y)≥0 for every ω∈Ω, then ⟨y,g⟩(ω)−π(y)=0 for every ω∈Ω.
For a Borel payoff f:Ω→R, the superhedging price is
ϕ(f)=inf{c+π(y):c∈R,y∈Rm,c+⟨y,g⟩≥fon Ω}∈[−∞,∞],
and the set of pricing measures is
Q={μ∈P(Ω):πj≤∫Ωgjdμ≤πj,j=1,…,m}.
The proofs also use the box Δ=∏j[πj,πj] and the set C={⟨y,g⟩−π(y):y∈Rm}−L+0 of payoffs super-replicable at zero cost, where L+0 is the set of nonnegative Borel functions.
Formalization targets
Goal: the superhedging duality (Theorem 2.4(iii))
Under Assumption 2.1, for every Borel f:Ω→R,
ϕ(f)=μ∈Qsup∫Ωfdμ.
The identity is stated in [−∞,∞] and covers the case ϕ(f)=+∞ of payoffs that no static portfolio dominates.
Milestones
In the order of the proof in Appendix EC.4:
the support-function identity π(y)=maxq∈Δ⟨y,q⟩;
Lemma EC.4.1: under Assumption 2.1, C is closed under pointwise convergence;
Theorem 2.4(i): ϕ(f)>−∞;
Theorem 2.4(ii): there is y with ϕ(f)+⟨y,g⟩−π(y)≥f, so the infimum is attained when ϕ(f)<∞;
Lemma EC.4.2: Δ∩relint(Γν)=∅ for every ν∈P(Ω), where Γν is the set of moment vectors ∫gdμ of measures μ≫ν integrating ∣f∣+∑j∣gj∣; in particular Δ∩relint(Γ)=∅;
the duality for f bounded from above;
weak duality ϕ(f)≥supμ∈Q∫fdμ, which needs no no-arbitrage assumption.
Significance
The duality turns a maximisation over an infinite-dimensional set of probability measures into a minimisation over R×Rm, a finite-dimensional problem with infinitely many constraints. This is what makes the exact computation of model-free bounds in the paper possible: for continuous piecewise affine payoffs, the minimisation side is solved by cutting-plane algorithms whose subproblems are linear and mixed-integer programs. Parts (i) and (ii) say that the upper bound is never −∞ under no-arbitrage and that it is realised by an actual static hedge. Lemma EC.4.2 also yields the paper's fundamental theorem (Theorem 2.3), which characterises no-arbitrage by the existence of pricing measures dominating any given probability measure.
The result is proved in the paper; it has no machine-checked proof. A formalization would also give a checked version of the closedness lemma for cones of super-replicable payoffs, which is the step most often adapted from Bouchard–Nutz in later work on one-period robust pricing, and a reusable statement of the extended-valued duality with an explicit convention for non-integrable payoffs.
Difficulty
The obvious route is finite-dimensional linear programming duality. It fails because the constraint c+⟨y,g⟩≥f is indexed by every ω in an uncountable Polish space and the dual variables are measures; the paper uses a semi-infinite Fenchel duality theorem (Borwein–Lewis), whose constraint qualification is exactly the relative-interior condition of Lemma EC.4.2. Proving that condition requires constructing, from any ν, an equivalent-type measure with finite moments, and separating a polyhedron from a convex set properly. A second difficulty is the passage to unbounded f: it rests on the closedness of C under pointwise limits (Lemma EC.4.1), proved by an induction on the number of coordinates along which the hedge positions yn diverge; compactness of the unit sphere alone does not suffice because the bid–ask cost π is not linear.
Formalization scope
The Lean development lives in the namespace ModelFreeBounds.Duality, with one definition file Market. Conventions:
Ω carries [TopologicalSpace Ω] [PolishSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω]. Indices are Fin m and vectors in Rm are functions Fin m → ℝ; relint is intrinsicInterior ℝ.
The standing assumptions (Borel gj, πj≤πj) form the structure Market.Standing.
Assumption 2.1, the superhedging constraint, L+0 and the convergence in Lemma EC.4.1 are all pointwise on every ω, not almost sure.
ϕ(f) is an infimum in EReal with inf∅=+∞; the right-hand side of (2.3) is a supremum in EReal over the subset Q of measures, equal to −∞ when Q=∅.
∫Ωfdμ for a Borel f that need not be integrable is ∫f+dμ−∫f−dμ with ∞−∞=−∞. The paper fixes no convention; the duality holds under either choice.
Q includes μ-integrability of every gj, which the real bounds on ∫gjdμ presuppose. Integrability of ∣f∣+∑j∣gj∣ in Γν and Γ is written as integrability of f and of each gj.
Ω is assumed nonempty only in Theorem 2.4(i), Theorem 2.4(ii) and the "in particular" part of Lemma EC.4.2, which are false for Ω=∅ (there ϕ(f)=−∞ and Γ=∅); the goal holds for Ω=∅ with both sides −∞.
The following formalizations would trivialise the statement and are excluded: a real-valued ϕ (where an unbounded infimum becomes 0), the Bochner integral for f (which is 0 on non-integrable f), Q without the integrability of the gj, no-arbitrage stated almost surely under a fixed measure, Q over sub-probability or arbitrary measures, and a finite Ω.
A complete development needs: semi-infinite or infinite-dimensional Fenchel duality for linear maps into Rm+1 (Mathlib has finite-dimensional separation theorems but not this duality), proper separation of a polyhedron from a convex set in Rm, and the measure-theoretic construction of measures with prescribed null sets and finite moments on a Polish space. The closedness lemma and the support-function identity are independent of the duality and are natural first contributions. Contributions of any milestone, of alternative proofs of the goal, or of reusable infrastructure (extended-valued integrals, relative-interior constraint qualifications) are welcome.
B. Bouchard, M. Nutz, Arbitrage and duality in nondominated discrete-time models, Annals of Applied Probability 25(2), 2015. https://doi.org/10.1214/14-AAP1011
J. M. Borwein, A. S. Lewis, Partially finite convex programming, Part I: Quasi relative interiors and duality theory, Mathematical Programming 57, 1992. https://doi.org/10.1007/BF01581072