Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Quantum Information·Captain: Goku

The Symmetry Group of Gaussian States in L²(ℝⁿ)Research Paper

Motivation

This is a continuation of the expository article \cite{krp} with some new remarks. Let $S_n$ denote the set of all Gaussian states in the complex Hilbert space $L^2 (\mathbb{R}^n),$ $K_n$ the convex set of all momentum and position covariance matrices of order $2n$ in Gaussian states and let $\mathcal{G}_n$ be the group of all unitary operators in $L^2 (\mathbb{R}^n)$ conjugations by which leave $S_n$ invariant. Here we prove the following results. $K_n$ is a closed convex set for which a matrix $S$ is an extreme point if and only if $S=\frac{1}{2} L^{T} L$ for some $L$ in the symplectic group $Sp (2n, \mathbb{R}).$ Every element in $K_n$ is of the form $\frac{1}{2} (L^{T} L + M^{T} M)$ for some $L,M$ in $Sp (2n, \mathbb{R}).$ Every Gaussian state in $L^2 (\mathbb{R}^n)$ can be purified to a Gaussian state in $L^2 (\mathbb{R}^{2n}).$ Any element $U$ in the group $\mathcal{G}_n$ is of the form $U = \lambda W ({\bm {\alpha}}) \Gamma (L)$ where $\lambda$ is a complex scalar of modulus unity, ${\bm {\alpha}} \in \mathbb{C}^n,$ $L \in Sp (2n, \mathbb{R}),$ $W({\bm {\alpha}})$ is the Weyl operator corresponding to ${\bm {\alpha}}$ and $\Gamma (L)$ is a unitary operator which implements the Bogolioubov automorphism of the Lie algebra generated by the canonical momentum and position observables induced by the symplectic linear transformation $L.$

This mission is the statement-level formalization of The Symmetry Group of Gaussian States in L²(ℝⁿ) (arXiv:1101.5041v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The Gaussian covariance set is closed and convex (§1, following (1.3), 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

7 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 7: Normalized Gaussian density operators on L²(R^n), the actual Weyl operators of (2.4), and symplectic implementers defined by (2.9). (hard)
§2, (2.12)–(2.17): The Hilbert–Schmidt ideal as a Hilbert space, its kernel isometry I, full L² dilations and second quantization, linked to the trace-class characteristic transform. (hard)
Theorem 4, (3.11): Constructed normalized multimode Gaussian density and full number-basis thermal spectral operator, together with Weyl and metaplectic actions on L²(R^n). (hard)
Corollary 2, pp.14–15: Normalized squeezed Gaussian L² wavefunctions, their finite tensor product and actual passive second-quantization unitary. (hard)
Theorem 5, pp.15–16: The completed n+n mode Hilbert tensor identification, normalized pure Gaussian joint densities and actual relative trace over the second n modes. (hard)
Theorem 6, pp.16–18: Full multimode number-basis thermal density, Gaussian state predicate and spectral unitary beta on every occupation vector in N^n. (hard)
§2, paragraph after (2.17): A corrected source statement for the printed 12th-root and 12th-power claim. (source-ambiguity)

Selected references

The Symmetry Group of Gaussian States in L²(ℝⁿ), arXiv:1101.5041v1, https://arxiv.org/abs/1101.5041v1

7 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

Quantum Physics of Simple Optical InstrumentsResearch Paper

Motivation

Simple optical instruments are linear optical networks where the incident light modes are turned into equal numbers of outgoing modes by linear transformations. For example, such instruments are beam splitters, multiports, interferometers, fibre couplers, polarizers, gravitational lenses, parametric amplifiers, phase-conjugating mirrors and also black holes. The article develops the quantum theory of simple optical instruments and applies the theory to a few characteristic situations, to the splitting and interference of photons and to the manifestation of Einstein-Podolsky-Rosen correlations in parametric downconversion. How to model irreversible devices such as absorbers and amplifiers is also shown. Finally, the article develops the theory of Hawking radiation for a simple optical black hole. The paper is intended as a primer, as a nearly self-consistent tutorial. The reader should be familiar with basic quantum mechanics and statistics, and perhaps with optics and some elementary field theory. The quantum theory of light in dielectrics serves as the starting point and, in the concluding section, as a guide to understand quantum black holes.

This mission is the statement-level formalization of Quantum Physics of Simple Optical Instruments (arXiv:quant-ph/0305007v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Canonical constraints and passive photon-number conservation (§3.1: canonical matrix constraints and photon-number conservation, PDF p. 9). 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.

Deferred results

32 results of the paper are not stated yet, because the library lacks an interface they need:

§2.1: wave equation and conserved scalar product: Classical wave-action variation and full-line indefinite mode product (hard)
§2.2: canonical quantization and oscillator energy: Complete generalized-mode quantization and electromagnetic energy quadratic form (hard)
§2.3: transfer equation, structure, determinant, inverse: Forward transfer fundamental solution for the impedance ODE (hard)
§2.4: unitary scattering from dielectric transfer data: Normalized asymptotic dielectric modes and their mode-operator basis change (hard)
§3.2: Heisenberg–Schrodinger state correspondence: Bounded observable pairing and conjugation on arbitrary trace-class Fock states (hard)
§3.2: unrestricted single-logarithm implementation recipe: A valid domain for a symmetry-compatible single Hamiltonian logarithm (source-ambiguity)
§3.3: real beam-splitter Hamiltonian: Self-adjoint closure and full-Fock unitary exponential of the beam generator (hard)
§3.3: two-mode amplifier Hamiltonian: Self-adjoint two-mode squeezing generator and its full unitary group (hard)
§3.4, Eq.(3.30): Wigner covariance of simple optical instruments: General finite-mode trace-class Wigner transform and active metaplectic covariance (hard)
§4.2: rotations and general beam-splitter evolution: Closed Jordan–Schwinger exponentials with simultaneous mode and Stokes actions (hard)
§5.1: Lindblad absorption/emission becomes Fokker–Planck drift and diffusion: Weak Wigner generator identity for the unbounded absorption/emission Lindbladian (hard)
§5.2: thermal stationary state: Thermal density, Wigner correspondence and stationary generator domain (hard)
§5.2: exact thermal-loss beam-splitter model and long-time limit: Thermal attenuator semigroup and full-state trace-norm limit (hard)
§5.3: exact thermal-amplifier model: Thermal amplifier channel and unbounded-generator equivalence (hard)
§5.3: balanced gain/loss strictly reduces purity: Quantum heat semigroup purity derivative for every physical input (hard)
§5.3: phase-sensitive Gaussian reservoir model: Squeezed Gaussian reservoir conjugation of the Lindblad semigroup (hard)
§6.2: Lorentz action, unitary amplifier, and number-difference conservation: Full squeezing exponentials and Lorentz conjugation on closed unbounded operators (hard)
§6.3: squeezed-vacuum Wigner density and EPR quadrature widths: Identification of the squeezed state Wigner transform and EPR variances (hard)
§6.3: either reduced squeezed-vacuum state is thermal: Squeezed-vacuum partial trace, Gibbs state and temperature correspondence (hard)
§6.3: maximal entanglement at fixed oscillator energy: Extended oscillator von Neumann entropy under a finite energy constraint (hard)
§6.3: normalized Fock expansion of the two-mode squeezed vacuum: Squeezed-vacuum geometric series linked to its unitary preparation (hard)
§6.3: weak downconversion and the effect of photon-pair postselection: Weak-squeezing asymptotics, nonzero pair conditioning and exact product output (hard)
§6.3: polarization-invariant downconversion produces singlet pairs: Four-mode unitary downconversion and corrected tensor-product squeezed output (hard)
§7.1: moving-medium effective wave equation: Variational Euler–Lagrange interface for the effective moving dielectric (hard)
§7.2: moving light is a massless field in the effective metric: Effective Lorentz metric and scalar d’Alembert operator identification (hard)
§7.3: general null-coordinate wave solution: Both directions of null-coordinate solution classification on horizon-free patches (hard)
§7.3: logarithmic horizon coordinate and wavelength scaling: One-sided horizon coordinate asymptotics with signed branch control (hard)
§7.4: conserved moving-medium mode product: Moving-medium conserved indefinite current with full-line integral domain (hard)
§7.4: local analytic horizon connection and Bogoliubov ratio: Branch-fixed local horizon modes and their normalized Bogoliubov connection (hard)
§7.4: global identification of the pre-collapse vacuum: Quantified horizon-formation history preserving the required analyticity (source-ambiguity)
§7.4: Hawking thermal spectrum in the stated analytic-vacuum model: Stationary analytic-vacuum thermal density with spectral normalization (hard)
§7.5: grey-body scattering of the generated radiation: Exterior variable-epsilon wave scattering and normalized radiation channel (hard)

Selected references

Quantum Physics of Simple Optical Instruments, arXiv:quant-ph/0305007v2, https://arxiv.org/abs/quant-ph/0305007v2

15 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

Formal proofs in real algebraic geometry: from ordered fields to quantifier eliminationResearch Paper

Motivation

This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic properties. The theory of real algebraic numbers and more generally of semi-algebraic varieties is at the core of a number of effective methods in real analysis, including decision procedures for non linear arithmetic or optimization methods for real valued functions. After defining an abstract structure of discrete real closed field and the elementary theory of real roots of polynomials, we describe the formalization of an algebraic proof of quantifier elimination based on pseudo-remainder sequences following the standard computer algebra literature on the topic. This formalization covers a large part of the theory which underlies the efficient algorithms implemented in practice in computer algebra. The success of this work paves the way for formal certification of these efficient methods.

This mission is the statement-level formalization of Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination (arXiv:1201.3731v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

29 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §3.2, Lemma sgp_right_scale (§3.2, Lemma sgp_right_scale, PDF p. 12). 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.

Deferred results

12 results of the paper are not stated yet, because the library lacks an interface they need:

Unnumbered main result: quantifier elimination, including q_elimP: A complete field-parametric qElim implementation: inverse removal, normalization into Boolean combinations of root/sign systems, an environment-independent coefficient-only projection program, and structural quantifier recursion. (hard)
§3.3, Lemma intP: The complete int_rewrite : interval R → R → Prop case definition generating the source rewrite conjunction for open, closed, and infinite endpoints; only the bounded closed/closed case is expanded on PDF p.15. (source-ambiguity)
§4.1, unnumbered derivative/monotonicity correspondence: §4.1, unnumbered derivative/monotonicity correspondence (source-ambiguity)
§5.3.1, unnumbered variation/Cauchy-index identity: §5.3.1, unnumbered variation/Cauchy-index identity (source-ambiguity)
§5.4, weighted remainder-variation feasibility test: §5.4, weighted remainder-variation feasibility test (source-ambiguity)
§5.1 and §6.2.1, closed root/sign decision: Both the IVT-relative closed root/sign algorithm and its coefficient-only closed counterpart, distinguished as required by the pinned node. (hard)
§6.2.2, formal projection commuting diagram: Complete formal coefficient-only projection decF, fixed before all environments, including zero-tail and leading-coefficient degree-drop branching. (hard)
§6.2.2, claimed nonexistence of direct if/lcoef counterparts: §6.2.2, claimed nonexistence of direct if/lcoef counterparts (source-ambiguity)
Theorem 1 (cps-counterpart): Theorem 1 (cps-counterpart) (source-ambiguity)
§6.2.3, universal Boolean-valued DT claim: §6.2.3, universal Boolean-valued DT claim (source-ambiguity)
§6.3, decidability of the full first-order theory: Complete closed-formula Boolean decision sat with an explicit effective body and a named-variable closedness predicate. (hard)
§7.1, existential fragment of nondiscrete fields: §7.1, existential fragment of nondiscrete fields (source-ambiguity)

Selected references

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, arXiv:1201.3731v2, https://arxiv.org/abs/1201.3731v2

30 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

On the Choi-Jamiolkowski Correspondence in Infinite DimensionsResearch Paper

Motivation

We give a mathematical formulation for the Choi-Jamiolkowski (CJ) correspondence in the infinite-dimensional case in the form close to one used in quantum information theory. We show that there is no need to use a limiting procedure to define "unnormalized maximally entangled state" and the corresponding analog of the Choi matrix since they can be defined rigorously as, in general, nonclosable forms on an appropriate dense subspace. The properties of these forms are discussed in Sec. 2. An important question is: when the CJ form is given by a bounded operator. This is the case for entanglement-breaking channels: we prove this in Sec. 3 along with a version of a result of Wolf et al. characterizing CJ operators which correspond to such channels by giving precise definitions of a separable operator and a relevant integral. In Sec. 4 we obtain explicit expressions for CJ forms and operators defining a general Bosonic Gaussian channel. In Sec. 5 we give a decomposition of the Gaussian CJ form into product of the four principal types and a necessary and sufficient condition for existence of the bounded CJ operator.

This mission is the statement-level formalization of On the Choi-Jamiolkowski Correspondence in Infinite Dimensions (arXiv:1004.0196v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 2: separable normalized CJ operators are contractions (Lemma 2: separable CJ operators are contractions, PDF p. 6). 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.

Deferred results

20 results of the paper are not stated yet, because the library lacks an interface they need:

Lemma 1: existence and uniqueness of the CJ form: Trace-class channel, basis conjugation, algebraic-domain sesquilinear form, and bounded-operator trace duality for both equalities in (2). (hard)
Equations (3)–(4) and converse correspondence: Reconstruction of a complex-linear trace-class channel from a normalized positive algebraic-domain form. (hard)
Countable Kraus representation: Countable bounded Kraus operators, strong normalization, and trace-norm-convergent action on every trace-class operator. (hard)
Identity-channel form and weak maximally entangled prescription: Unbounded diagonal tensor functional, closability of its positive form, and weak Phi tensor identity on that form. (hard)
Basis covariance and basis-independent bounded norm: Basis-dependent channel/CJ correspondence and conjugate transpose, including unbounded form pullback. (hard)
Faithful-reference normalized CJ state and recovery: Faithful density spectral purification, tensor channel on full trace class, partial traces and dense-range square-root recovery. (hard)
Proposition 1: entanglement breaking iff separable bounded CJ operator: Trace-class tensor channels, entanglement breaking, operator-valued measures and their weak integral against conjugated input effects. (hard)
General Weyl integral for the CJ form (13): Strongly continuous irreducible finite-mode Weyl systems, channel adjoint, and scalar integrability for matrix elements of (13). (hard)
Gaussian integrals (16)–(18) and sufficient boundedness: Operational Gaussian channel/Weyl model and weak versus norm-convergent Gaussian operator integrals. (hard)
Case 4: noiseless delta form and nonclosability: Distributional Weyl inversion and nonclosability for actual noiseless multi-mode CJ forms. (hard)
Case 3: commuting-noise Gaussian operator: Joint spectral calculus for the strongly commuting unbounded quadratures R_BA. (hard)
Proposition 2: exact norm for nondegenerate commutator defect: Operational Gaussian CJ operator and spectral absolute value of the generally nonnormal matrix Delta_K^(-1) mu. (hard)
Case 1: strictly mixed Gaussian CJ operator (22): Williamson-defined Gibbs quadratic form and spectral exponential of unbounded quadratures. (hard)
Case 2: printed pure-noise kernel formula (source discrepancy): Source discrepancy: the printed quadratic kernel has a missing factor 1/2. (source-ambiguity)
Normal modes and thermal spectral formula (23)–(28): Fock number operators, tensor decomposition of a reducible CCR representation, and unbounded Gibbs functional calculus. (hard)
One-mode norm and non-EB contraction example: Actual one-mode Gaussian channel/CJ operator and EB predicate, including the commuting k=1,m>0 regime. (hard)
One-mode mixed operator (29) and pure boundary: Canonical/Fock transposition, unbounded one-mode quadratic Hamiltonian and its spectral projections. (hard)
Four principal factors, rank counts, and tensor realization: Symplectic extension and unitary tensor realization of the four weak Gaussian form integrals, including singular classical blocks. (hard)
Proposition 3: exact boundedness criterion: Operational Gaussian CJ form across all singular/noise/commutator regimes and its bounded-representability predicate. (hard)
Open-system interpretation and four noise types: Given operational Gaussian reversible dilation, its noise observables, their covariance, commutators and quantum/classical interpretation. (hard)

Selected references

On the Choi-Jamiolkowski Correspondence in Infinite Dimensions, arXiv:1004.0196v3, https://arxiv.org/abs/1004.0196v3

4 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Wolf Pack Activism: Competition for Flow Sustains Successful Engagement Where Delegation Without Flow or Proprietary Blocks CannotResearch Paper

Motivation

Shareholder engagement with corporate management is a public good: when a change of policy raises firm value, every shareholder gains, but only the shareholders who engage pay the cost. Since Grossman and Hart (1980) this free-rider problem has been the standard explanation for why dispersed owners under-monitor management. In practice, however, engagement campaigns are increasingly run by wolf packs: several activist funds, each holding a small block, who engage together even though none could change policy alone.

Brav, Dasgupta and Mathews ask why such packs form when each member's stake is small and most of the capital they invest belongs to outside investors. Their answer is competition for flow. Fund investors observe who engaged and move their capital toward funds that revealed skill by engaging; the fees on that capital are a private, excludable reward for engagement. The paper shows that this flow motive can sustain collective engagement over parameter ranges where it fails both for funds that manage delegated money without flows and for funds that invest only their own money.

Setting

A firm has a unit continuum of shares. There are $N$ skilled and $M$ unskilled activist funds; each holds one block of size $b \in (0,1)$ and cash $c > 0$ , and $(M+N)b \le 1$ . A block consists of a fraction $\phi \in (0,1)$ of the fund's own capital and $1-\phi$ of delegated capital, on which the fund earns a fee $w \in (0,1)$ . The difficulty $\eta$ of changing policy lies in $(b, U]$ with $U > 1$ and is public. Only skilled funds can engage, each at cost $c$ . If $k$ funds engage, engagement succeeds iff $kb \ge \eta$ ; the firm is then worth $P_2 = P_h > 0$ , otherwise $P_2 = 0$ . Write $\alpha = Nb$ and let $K_\eta$ be the least natural number $x$ with $xb \ge \eta$ .

A skilled fund's payoff is $(s\,bP_2 + w f_2 + c\,\mathbf 1_{NE})R_S$ , where $R_S > 1$ is its reinvestment return, $s$ its proprietary fraction and $f_2$ the value of the delegated capital it holds at the end. Three games differ only in $s$ and $f_2$ :

delegated game with competition for flow: $s = \phi$ ; if $k \ge 1$ funds engage, the delegated capital of the $M+N-k$ non-engagers moves evenly to the $k$ engagers;
delegated game without competition for flow: $s = \phi$ ; every fund keeps its own delegated capital $(1-\phi)bP_2$ ;
proprietary blocks game: $s = 1$ and there is no delegated capital.

The fee value of an engager's capital when exactly $x$ funds engage and succeed is (Definition 5)

\hat c(x) = w\Big((1-\phi)bP_h + \tfrac1x (M+N-x)\,b(1-\phi)P_h\Big).

For each $\eta$ the skilled funds play a finite simultaneous game, the $\eta$ -subgame. A maximal success equilibrium (Definition 1) picks, for every $\eta$ , a Nash equilibrium of the $\eta$ -subgame whose probability of successful engagement is maximal among all its Nash equilibria, mixed ones included.

Formalization targets

Goal: Proposition 7

With $\bar c(\eta) = \phi bP_h + \hat c(K_\eta)$ , for every $\eta \in (b, \alpha]$ :

c \in \big(\phi bP_h + w(1-\phi)bP_h,\ \bar c(\eta)\big] \ \Longrightarrow\ \text{flow game succeeds, no-flow game cannot},

c \in \big(bP_h,\ \bar c(\eta)\big] \ \Longrightarrow\ \text{flow game succeeds, proprietary game cannot};

the first range is always non-empty, and the second is non-empty for some $\eta$ when $M+N > 2/w$ . "Succeeds" means that every maximal success equilibrium of the flow game succeeds with probability one at $\eta$ (and one exists); "cannot" means every Nash equilibrium of the comparison game's $\eta$ -subgame has success probability zero.

Milestones

Lemma 2: on each interval $(\hat c(L+1), \hat c(L)]$ (and $(\hat c(K_\eta+1), \phi bP_h + \hat c(K_\eta)]$ ) a pure equilibrium of the flow game with exactly $L$ (resp. $K_\eta$ ) engagers exists; all $N$ engage for $c \le \hat c(N)$ , or for $c \le \phi bP_h + \hat c(N)$ when $K_\eta = N$ .
Proposition 4: in the flow game success occurs iff $\eta \le \alpha$ and $c \le \bar c(\eta)$ ; otherwise no equilibrium involves engagement.
Proposition 3: in the no-flow game the same holds with the threshold $\phi bP_h + w(1-\phi)bP_h$ , by exactly $K_\eta$ funds.
Proposition 2: in the proprietary game the same holds with the threshold $bP_h$ .

Significance

Propositions 2 and 3 formalize the classical underprovision result and its aggravation by delegation: since $w < 1$ , a fund that manages other people's money has weaker incentives to bear private engagement costs. Proposition 7 shows that flows reverse this ranking, and that the reversal against the proprietary benchmark is driven by the number of funds: the larger $M+N$ , the more capital an engager can attract. This is the paper's explanation of why wolf packs of small funds can be more effective than a single large owner, and it underlies the paper's comparative statics in activist capital.

The results are proved in the paper (Management Science, 2022); none of them has been formalized. The mission produces a machine-checked model of threshold engagement games with three payoff regimes on top of a published finite-game vocabulary, and machine-checked proofs that also cover mixed equilibria, which the paper treats in a short argument. Two hypotheses missing from the printed Proposition 7 ( $M \ge 1$ , $N \ge 2$ ) and one endpoint in Lemma 2 are made explicit.

Difficulty

Each pure-profile check is a comparison of two numbers, but three steps need care. First, the cost intervals of Lemma 2 must cover the whole half-line $c \le \bar c(\eta)$ ; this uses that $\hat c$ is strictly decreasing and the endpoint $c = \hat c(N)$ , which the printed lemma excludes. Second, "no engagement" above the thresholds must hold for every mixed equilibrium, so the argument has to work with expected payoffs over all $2^N$ pure profiles rather than with one pivotal fund. Third, a maximal success equilibrium is a family indexed by $\eta$ , and maximality compares it against every mixed equilibrium of each subgame. The naive reading of Proposition 7 as three interval inequalities misses all of the game theory and is not the target.

Formalization scope

The model is one definitions file, WolfPack.FlowEngage.Model, built on the published agt_games vocabulary (AGT.IsPureNash, AGT.IsMixedNash, AGT.profileProb). Players are Fin N (the skilled funds; unskilled funds never act and enter only through $M$ in the reallocation). Actions are Bool, with true = engage. Mixed profiles are weight functions; the success probability sums over the $2^N$ pure profiles. $K_\eta$ is sInf over $\mathbb N$ ; $\hat c$ casts to $\mathbb R$ before subtracting. The proprietary game is the model with the proprietary fraction set to $1$ , all else unchanged (p. 15, footnote 14).

Conventions and additions, all disclosed in the items:

standing assumptions $0<b<1$ , $c>0$ , $U>1$ , $R_S>1$ , $\phi, w \in (0,1)$ from §2, plus $P_h > 0$ , $M \ge 1$ and $(M+N)b \le 1$ , which the model implies but does not display;
$N \ge 2$ in the goal: with $N = 1$ there is no $\eta \in (b,\alpha]$ and the "for some $\eta$ " clause fails;
the reallocation of delegated capital is the off-equilibrium belief fixed in the proof of Lemma 2 (engagers posterior 1, non-engagers below 1), built into the payoff rather than left as a parameter;
Lemma 2 1(c) is stated with $c \le \hat c(N)$ , as its proof shows, instead of the printed $c < \hat c(N)$ .

A formalization in which "success is impossible" quantified only over pure equilibria, in which the comparison game was allowed to choose its own no-engagement equilibrium, or in which "every maximal success equilibrium" ranged over an empty set would be trivial; the goal quantifies over all mixed equilibria of the comparison games and asserts existence of a maximal success equilibrium. Not formalized: Proposition 1 (social optimum), Lemma 1, Corollaries 1–3, Propositions 5, 6, 8, the asymmetric-information extension of Appendix B, and the case $P_l > 0$ . Proofs of any milestone are welcome, as are general lemmas on mixed equilibria of binary-action symmetric games.

Selected references

A. Brav, A. Dasgupta, R. Mathews, Wolf Pack Activism, Management Science 68(8):5557–5568, 2022; accepted manuscript May 2021, LSE Research Online eprint 112118, https://ssrn.com/abstract=2529230. https://doi.org/10.1287/mnsc.2021.4131
S. Grossman, O. Hart, Takeover Bids, the Free-Rider Problem, and the Theory of the Corporation, Bell Journal of Economics 11(1):42–64, 1980. https://doi.org/10.2307/3003400
N. Nisan, T. Roughgarden, É. Tardos, V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 1. https://doi.org/10.1017/CBO9780511800481

7 thms3 active usersReviewed

Completed

Markov Chain Operations Research Probability·Captain: mikedeng1

A Token-Based Central Queue with Order-Independent Service Rates: Under the Assignment and Order-Independent Conditions the Stationary Distribution Has a Product FormResearch Paper

Motivation

Many service systems match heterogeneous customers to heterogeneous resources: jobs to machines in a data centre, patients to beds, orders to couriers, donors to recipients. A recurring question is whether such a system, run first-come-first-served among compatible pairs, has a stationary distribution that can be written down. Two lines of work answered it for special structures: the order-independent queue of Krzesinski (2011, cited as [20] in the paper), where the service rate of the population does not depend on the order of customers, and the multi-type job and server model of Visschers, Adan and Weiss (2012, [22]), where customers are matched to compatible servers under an assignment rule. Redundancy systems with cancel-on-completion fit the first framework and those with cancel-on-start the second (arXiv:1902.02137v1, p. 3); matching models fit the second.

Ayesta, Bodas, Dorsman and Verloop (arXiv:1902.02137v1, later published in Operations Research, 2022) introduce the token-based central queue, which contains both. Their Theorem 1 states that, under an assignment condition and an order-independent condition, the stationary distribution has a product form. The paper's performance results (generating functions of queue lengths, Laplace transforms of waiting and sojourn times) and its applications (heterogeneous M/M/K, multi-server job models, redundancy, matching) are derived from it.

Setting

There is a finite set $\mathcal C$ of customer types and a finite set $\mathcal T=\{t_1,\dots,t_K\}$ of tokens. Type- $c$ customers arrive in a Poisson process of rate $\lambda_c>0$ ; $\lambda=\sum_c\lambda_c$ . A type- $c$ customer can hold only tokens from its compatibility set $\mathcal T_c$ and is served only while it holds one. An arrival that finds a compatible free token claims one, chosen by a randomised assignment rule; otherwise it waits at the end of a central queue as an inactive customer. When a customer leaves, its token passes to the longest-waiting compatible inactive customer, or becomes free if there is none.

The state $x=(T_1,n_1,\dots,T_i,n_i)$ lists the tokens $T_1,\dots,T_i$ held by the active customers in order of arrival and the number $n_j$ of inactive customers that arrived between the holders of $T_j$ and $T_{j+1}$ ; $(0)$ is the empty state and $\phi(x)=i+\sum_j n_j$ . With $\mathcal U(S)=\{c:\mathcal T_c\subseteq S\}$ , write $\lambda_{\mathcal U(S)}=\sum_{c\in\mathcal U(S)}\lambda_c$ , and let $\lambda_t(S)$ be the rate at which arrivals claim token $t$ when $S$ is the set of busy tokens.

The holder of $T_j$ leaves at rate $\mu_{T_j}(x)=\eta(\phi(x))\,s_j(T_1,\dots,T_j)$ with $s_j\ge0$ and $\eta(n)>0$ for $n\ge 1$ ; let $k(T_1,\dots,T_i)=\sum_{j\le i}s_j(T_1,\dots,T_j)$ , so $\mu(x)=\eta(\phi(x))k(T_1,\dots,T_i)$ .

Condition 1 (assignment condition): $\Pi_\lambda(\{T_1,\dots,T_i\})=\prod_{j=1}^i\lambda_{T_j}(\{T_1,\dots,T_{j-1}\})$ does not depend on the order of $T_1,\dots,T_i$ .
Condition 2 (order-independent condition): $k(T_1,\dots,T_i)$ does not depend on the order of $T_1,\dots,T_i$ .

Formalization targets

Goal: Theorem 1 (p. 7)

With $\Pi_k(T_1,\dots,T_i)=\prod_{j=1}^i k(T_1,\dots,T_j)$ and $\alpha_j=\lambda_{\mathcal U(\{T_1,\dots,T_j\})}/k(T_1,\dots,T_j)$ , if the series below converges, then

\pi(x)=\pi((0))\,\frac{\Pi_\lambda(\{T_1,\dots,T_i\})}{\Pi_k(T_1,\dots,T_i)}\prod_{j=1}^{i}\alpha_j^{n_j}\prod_{j=1}^{\phi(x)}\frac{1}{\eta(j)},\qquad \pi((0))^{-1}=1+\sum_{x\neq(0)}\frac{\Pi_\lambda}{\Pi_k}\prod_j\alpha_j^{n_j}\prod_{j=1}^{\phi(x)}\frac1{\eta(j)},

is a probability distribution that satisfies the global balance equations $\pi(x)\sum_y q(x,y)=\sum_y\pi(y)q(y,x)$ of the queue's transition rates $q$ .

Milestones

The paper's proof runs through the identities below, listed in attack order: (1), the departure-rate identities (4), (5), (7), the total exit rate $\lambda+\mu(x)$ , the explicit form (8)–(9) of the global balance equations, the partial balance equations (12), (13), (14) with the rearrangement of $\Pi_k$ and the telescoping identity (29) from Appendix A, and (9) for the product form.

Significance

The product form gives the stationary law of a multi-class, multi-server system with compatibility constraints, with a normalising constant expressed as an infinite series. The paper derives from it the joint generating function of the numbers of waiting customers per type (Theorem 2), the numbers in system (Theorem 4), and the transforms of time-till-token and sojourn time (Theorems 6, 7), and shows that the heterogeneous M/M/K queue, redundancy with cancel-on-start or cancel-on-completion and a family of matching models are special cases.

The result is proved in the paper; nothing here is open. To our knowledge no part of it has been machine-checked. A formal proof would check the bookkeeping of the transition structure, where the printed text has slips (below), and would give a reusable development of product-form verification by partial balance for queues with order-dependent descriptors.

Difficulty

The algebra of the partial balance equations is long but routine once the predecessors of a state are listed correctly. The difficulty is that list. A departure frees a token that passes to the first compatible waiting customer, so the predecessors of a state are indexed by where the departing customer stood, how the waiting customers were split around it, and whether the token was released or reclaimed. The paper's printed list of reclaiming predecessors, $\mathrm{shift}_{k,n}(x,T_j)$ , is stated for $1\le k$ and $k+1<j$ , while the balance equations sum over $0\le k\le j-1$ . The obvious reading of the printed tuple at $k=j-1$ counts customers twice. A second slip sits in Appendix A, in the rearrangement of $\Pi_k$ . A proof that copies the paper's backward formulas into the balance equations proves the wrong identity: the goal is balance for the forward transition rates, from which the predecessor list has to be derived.

Formalization scope

Types and states. Types and tokens are Fintypes with decidable equality (finitely many tokens, as in Theorem 1). A state is a list of (token, count) pairs with distinct tokens. Infeasible descriptors (a waiting customer that could have claimed a free token) are included; the weights vanish on them.
Rates. All rates are real numbers. transitions lists the forward transitions of §4.1 with their rates, and rate y x is the total rate from y to x. The reclaim probabilities use $\lambda_{\mathcal U(\{T_1,\dots,T_l\}\setminus\{T_j\})}/\lambda_{\mathcal U(\{T_1,\dots,T_l\})}$ for a customer waiting behind $T_l$ . The departure rates are defined by (3), with $s$ taking the prefix $[T_1,\dots,T_j]$ .
Added assumptions, disclosed.
- Every type has a compatible token ( $\mathcal T_c\neq\emptyset$ ): the descriptor has no place for a customer that can never be served.
- $k>0$ on non-empty sequences of distinct tokens: the weights divide by $k$ .
- "Stable" is summability of the weights, the reading of §4.4.
Not stated. Uniqueness of the stationary distribution is not part of the goal. The paper obtains it from irreducibility and a theorem of Foster, and the full state type contains infeasible states outside the irreducible class.
Corrections. The shift states for $k=0$ and $k=j-1$ and the $\Pi_k$ rearrangement are corrected, as recorded in the items.
Trivial readings ruled out. The goal is not "the weights satisfy the typed-in equation (8)": it is global balance for the forward rates, with explicit summability so that no unconditional sum is a junk value.
Infrastructure. The development needs finite sums and products over list prefixes, list surgery (insert, remove, merge portions) and permutation invariance. It reuses the published equilibrium-equation predicate FullBalance. Proofs of any milestone are welcome, and so are general lemmas on partial balance for lists of transitions.

Selected references

U. Ayesta, T. Bodas, J. L. Dorsman, I. M. Verloop, A token-based central queue with order-independent service rates, arXiv:1902.02137v1, 2019; Operations Research, 2022. https://arxiv.org/abs/1902.02137v1 (the version read for this mission)
A. E. Krzesinski, Order independent queues, in R. J. Boucherie, N. M. van Dijk (eds.), Queueing Networks, International Series in Operations Research & Management Science 154, Springer, 2011, pp. 85–120 (reference [20] of the paper).
J. Visschers, I. J. B. F. Adan, G. Weiss, A product form solution to a system with multi-type jobs and multi-type servers, Queueing Systems 70(3), 2012, pp. 269–298 (reference [22]).
K. Gardner, S. Zbarsky, S. Doroudi, M. Harchol-Balter, E. Hyytiä, A. Scheller-Wolf, Queueing with redundant requests: exact analysis, Queueing Systems 83(3–4), 2016, pp. 227–259 (reference [14]).
F. G. Foster, On the stochastic matrices associated with certain queuing processes, The Annals of Mathematical Statistics 24(3), 1953, pp. 355–360 (reference [12]; the ergodicity criterion behind uniqueness).

14 thms3 active usersReviewed

Economics Operations Research·Captain: mikedeng1

Managing Opportunistic Consumer Returns in Retail Operations: A Menu of Refunds Earns the Targeted-Refunds Profit if and only if the Optimal Uniform Refund Is at Least the Salvage ValueResearch Paper

Opportunistic returns and restocking fees

Generous return policies raise demand, but they also invite opportunistic returns: customers who buy a product intending to use it briefly and return it for a refund. Retail-industry surveys put the share of such "wardrobing" or renting customers near a tenth of all customers, and retailers answer with restocking fees, return windows, or analytics services that flag suspected renters. Altug, Aydinliyim and Jain (SSRN 3283334; Management Science, 2021, doi:10.1287/mnsc.2020.3777) compare three ways a retailer can set prices and refunds in this situation. Their model extends Su's newsvendor model of consumer returns (Su 2009), in which every customer is an honest returner who returns only after learning that the product does not suit him, and the optimal refund equals the salvage value. The question is whether a retailer who cannot tell renters from honest customers can still do as well as one who can.

Setting

A retailer stocks $Q$ units at unit cost $c$ , sells at price $p$ , refunds $r$ per returned unit, and salvages leftover units at $s < c$ . Aggregate demand $D$ is random. A fraction $X \in (0,1)$ of customers are renters, the rest are honest returners.

An honest returner has a long-term valuation $u_L$ with distribution $G_L$ on $[0, V_L]$ . He buys if $\mathbb E\max\{u_L, r\} \ge p$ , learns $u_L$ , and returns the product iff $u_L < r$ ; so a fraction $G_L(r)$ of honest buyers return.
A renter has a short-term valuation $u_S$ with distribution $G_S$ on $[0, V_S]$ . He buys and returns iff $u_S \ge p - r$ , the rental fee; so a fraction $1 - G_S(p-r)$ of renters transact.

The fraction of customers who transact is $N(p, r) = 1 - XG_S(p - r)$ . A decision with marginal net revenue $M$ earns

M\,\mathbb E\min\Bigl\{\frac{Q}{N}, D\Bigr\} - (c - s)Q.

The three proposals are:

Uniform refunds, program (3): one pair $(p, r)$ for everybody, with $M^u(p,r) = (p-r)(1 - XG_S(p-r)) + (r-s)(1-X)(1-G_L(r))$ and $p \le \mathbb E\max\{u_L, r\}$ . The main-body results concerning $r^u$ treat the case where this inequality binds at the optimum.
Targeted refunds, program (9): the retailer identifies each customer's type and gives renters refund $r_R$ and honest returners refund $r_H$ at a common price $p$ , with $M^t(p, r_R, r_H) = X(p - r_R)(1 - G_S(p - r_R)) + (1-X)\bigl((p-s) - (r_H - s)G_L(r_H)\bigr)$ , $0 \le p - r_R \le V_S$ and $p = \mathbb E\max\{u_L, r_H\}$ .
Menu of refunds, program (11): the retailer offers two pairs $(p_H, r_H)$ , $(p_R, r_R)$ and lets customers self-select, subject to the honest returners preferring their pair with nonnegative surplus, $\mathbb E\max\{u_L, r_H\} - p_H \ge \max\{\mathbb E\max\{u_L, r_R\} - p_R, 0\}$ , and the renters preferring theirs, $p_R - r_R \le \min\{p_H - r_H, V_S\}$ .

Write $\Pi^u, \Pi^t, \Pi^m$ for the three optimal profits and $r^u$ for an optimal uniform refund. Without renters the optimal refund is the benchmark $r^b = s$ .

Formalization targets

Goal: Proposition 6, corrected

\Pi^u \le \Pi^m \le \Pi^t, \qquad \bigl(\Pi^t > \Pi^m = \Pi^u \iff r^u < s\bigr), \qquad r^u > s \Rightarrow \Pi^t = \Pi^m > \Pi^u, \qquad r^u = s \Rightarrow \Pi^t = \Pi^m,

together with the existence of an optimal uniform decision. Hence $\Pi^m = \Pi^t \iff r^u \ge s$ . This is a corrected Proposition 6 (p. 17). As printed, part (b) is an equivalence and part (c) says $\Pi^t = \Pi^m = \Pi^u$ when $r^u = s$ . That fails: in the setting of the paper's Figure 1 with $G_L = U[0,100]$ , $G_S = U[0,20]$ and $s = 30$ , the uniform optimum has $r^u = s$ and prices renters out, while targeted refunds earn strictly more, and so does the menu.

Milestones

In attack order: the closed form (5b) of the binding price; the first two claims of Lemma 1; the benchmark refund $r^b = s$ as a strict maximizer of the honest margin; the upper bounds $\Pi^u, \Pi^m \le \Pi^t$ ; Proposition 4's (10b)–(10c); the strict gain $\Pi^u < \Pi^t$ when $r^u \ne s$ ; Proposition 4's last sentence, $r^t_R \ge s \iff r^u \ge s$ ; the §7.1 claim that $r^t_R \ge s$ gives $\Pi^m = \Pi^t$ ; and Proposition 5's price-refund choice in (12b)–(12c), with its consequence for optimal profit.

Significance

The result says when screening by a price-refund menu is as good as identifying customers. A retailer that can segment customers only by paying an analytics firm learns that the payment buys nothing exactly when its optimal uniform refund is at least the salvage value, and that otherwise the menu degenerates to a single uniform policy. Figure 1 of the paper maps the regions in $(V_S, s)$ where each case occurs.

The proofs of Propositions 1 to 11 sit in an electronic companion that is not part of the working paper, and the printed Proposition 6 is false at the boundary $r^u = s$ . A machine-checked proof therefore settles the corrected statement independently of the missing appendix. No part of the paper has been formalized before.

Difficulty

Each program is a joint optimization over stock, price and refunds, with the stock entering through a newsvendor term whose coefficient depends on the refunds. The comparisons are between suprema of different programs, not between first-order conditions. The obvious approach, comparing the closed forms of Propositions 1, 4 and 5, does not work: Proposition 1 rests on the hypothesis that $xG_S'(x)$ is decreasing, which no distribution with a density on $[0, V_S]$ satisfies, and its threshold $V_S^{LB}$ is only asserted to exist. The case $r^u < s$ is the hard one: it requires showing that the menu's incentive constraints force it back to a uniform policy, which depends on the shape of the targeted profit in the rental fee and hence on the IGFR assumption.

Formalization scope

Everything is real-valued. Valuation laws are probability measures with support exactly $[0, V_L]$ , $[0, V_S]$ , a regular density and the IGFR property (LariviereIGFR.Char.IsIGFR). Demand is a probability law on $(0, \infty)$ with finite mean, and $\mathbb E\min\{Q, D\}$ is SupplyChainTheory.expSales.
Tie rules follow the page (keep iff $u_L \ge r$ , rent iff $u_S \ge p - r$ ).
The uniform program (3) keeps its constraint $\mathbb E\max\{u_L, r\} - p \ge 0$ , and the statements about the optimal uniform refund $r^u$ (Proposition 4's last sentence, Propositions 5 and 6) are made in the case the paper's main body treats (p. 11): that constraint binds at every optimal uniform decision. Program (3) does not carry its cap $p - r \le V_S$ : the paper's own optimum can have a rental fee above $V_S$ .
Refunds are nonnegative in all programs, and $r \le p$ for both menu pairs.
Hypotheses added to the page: $0 < s$ (at $s = 0$ Proposition 6 fails), $c < \mathbb E\max\{u_L, s\}$ (the page's $p > c$ at the benchmark price), and positive demand with finite mean.
$\Pi^u, \Pi^t, \Pi^m$ are suprema over each program's feasible set; their boundedness is a milestone. $\Pi^m$ is never defined by Proposition 5's case split, and $r^u$ is an arbitrary optimal uniform refund, not a closed form; a formalization that defines either by the case split is trivial and is ruled out.
Not formalized: the first-order conditions (5a), (5c), (10a), (10d), (12a); Proposition 1 and Lemma 1's third claim (false); Propositions 2, 3, 7–11.
Reusable infrastructure: the expected-maximum identity (5b), the strict optimality of $r = s$ for honest returners, and attainment of optima for newsvendor programs with continuous valuation laws.

Selected references

M. S. Altug, T. Aydinliyim, A. Jain, Managing Opportunistic Consumer Returns in Retail Operations, SSRN working paper 3283334 (revision of June 26, 2020); Management Science, 2021. https://ssrn.com/abstract=3283334, https://doi.org/10.1287/mnsc.2020.3777
X. Su, Consumer Returns Policies and Supply Chain Performance, Manufacturing & Service Operations Management 11(4), 595–612, 2009. https://doi.org/10.1287/msom.1080.0240
M. A. Lariviere, A Note on Probability Distributions with Increasing Generalized Failure Rates, Operations Research 54(3), 2006. https://doi.org/10.1287/opre.1060.0282

14 thms3 active usersReviewed

Completed

Control Theory Operations Research Stochastic Systems·Captain: mikedeng1

New Venture Creation: A Drift-Variance Diffusion Control Model: The Optimal Policy Is at Most a Two-Interval PolicyResearch Paper

Motivation

An entrepreneur developing a venture repeatedly chooses between strategies that differ in speed, risk and cost: a safe, slow approach or a fast, risky one. Wang and Zenios model this as a drift–variance diffusion control problem (SSRN 3667132; published in Operations Research, 2021, doi:10.1287/opre.2021.2171): the controller chooses not only the drift of a Brownian state but also its variance, and pays a running cost for each choice. Earlier models in which a decision maker switches controls as a diffusion evolves, Radner and Shepp (1996) on corporate risk choice and Harrison and Sunar (2015) on multiple modes of learning, describe their optimal policies through numerical procedures; here the controller chooses drift and variance together, the trade-off between moving fast and moving reliably is the object of study, and the optimal policy is in closed form.

The paper's motivating example (p. 10) suggests that the optimal policy might be complicated: use the safe control near $0$ to avoid failure, the cheaper risky control in the middle, and the safe control again near $U$ to secure the reward. The paper's main result says this never happens.

Setting

There are two controls $i \in \{1,2\}$ . Control $i$ gives drift $\mu_i > 0$ , volatility $\sigma_i > 0$ (variance $\sigma_i^2$ ) and costs $h_i > 0$ per unit time. The state follows

dX(t) = \mu(A(t))\,dt + \sigma(A(t))\,dB(t)

on $[0,U]$ , $U > 0$ , and stops on hitting $0$ (no payment) or $U$ (terminal cost $M < 0$ , i.e. a reward $|M|$ ). The entrepreneur minimizes the expected total cost.

Write $v_i = 2\mu_i/\sigma_i^2$ for the effective drift, $h_i^* = -M\mu_i/U$ for the critical cost (the cost at which control $i$ alone breaks even with no noise), and $\Delta h_i = h_i - h_i^*$ . As in the paper (p. 12), $v_1 < v_2$ throughout.

A $k$ -interval policy (Definition 1) cuts $[0,U)$ at $0 = S_0 < S_1 < \dots < S_k = U$ and uses control $i_j$ on $[S_{j-1},S_j)$ , with $i_j \ne i_{j+1}$ . Its value is the function $W$ that is continuously differentiable on $[0,U]$ , satisfies $W(0) = 0$ , $W(U) = M$ , and on each piece solves

h_{i_j} + \mu_{i_j}W'(x) + \frac{\sigma_{i_j}^2}{2}W''(x) = 0 .

A policy is optimal if its value lies below the value of every interval policy on $[0,U]$ .

Formalization targets

Goal: Theorem 1 (p. 10)

With $v_1 < v_2$ :

\exists\,\pi \text{ optimal with } k(\pi) \le 2, \qquad\text{and}\qquad (h_1,h_2) \ne (h_1^*,h_2^*) \implies \forall\,\pi \text{ optimal},\ k(\pi) \le 2 .

In words: an optimal policy either uses one control throughout or switches exactly once, and away from the critical point no optimal policy switches more than once.

Milestones

Theorem 2 (pp. 12–13): four explicit slopes $d_1^L, d_1^U, d_2^L, d_2^U$ cut the $(\Delta h_1, \Delta h_2)$ -plane into regions (7)–(10) on which "always 1", "always 2", "1 then 2" and "2 then 1" are optimal.
Exhaustiveness (p. 13): one of (7)–(10) always holds.
Lemma 1 (p. 14): $d_1^L < d_2^L < \sigma_2^2/\sigma_1^2 < d_1^U < d_2^U < \mu_2/\mu_1$ and $d_2^L > 0$ , with the elementary Lemmas 20–21.
Lemma 12, analytic form: a $C^1$ , piecewise $C^2$ function with the boundary values that satisfies the HJB inequality lies below every policy value.
The ingredients of Theorem 2 (a) and (c): the static value (54) and inequality (55); the two-interval value (74)/(87); Lemmas 4, 5, 6, 7, 9, 10 and 22 on the test functions $f_1, f_2, F_1, F_2$ .

Significance

The result reduces an infinite-dimensional control problem to a two-parameter family of candidates (which control first, and where to switch), and Theorem 2 identifies the optimum explicitly. Downstream, the paper reads managerial conclusions off the region picture: when both controls are inefficient, when to begin with the safe control and when with the risky one (§4, §8).

The theorem is proved in the paper; nothing here is open. No machine-checked version of any part of it is known. The mission produces a checked version of the analytic core: the closed-form value functions, the sign analysis of the switching functions, a one-dimensional comparison principle (the analytic content of the verification lemma), and the correction of the uniqueness half of Theorem 1 at the critical cost point.

Difficulty

The existence half is a long chain of explicit but delicate calculus. The slopes involve $U/(1 - e^{-v_iU})$ terms whose ordering (Lemma 1) is not visible from the formulas, and the switching point $S^*$ of the two-interval policy is the root of a function $f_1$ built from the derivatives of a piecewise exponential solution whose coefficients are ratios of exponential sums. Showing that $F_1, F_2$ keep their signs away from $S^*$ requires the sign facts of Lemma 22 in exactly the right region.

The uniqueness half looks immediate (two optimal policies have the same value, which cannot solve two different ODEs on an interval) but is false as printed: at $(h_1,h_2) = (h_1^*,h_2^*)$ the affine function $Mx/U$ solves both ODEs, and every interval policy is optimal. The correct statement must exclude that point, and its proof must show that, elsewhere, the optimal value is affine on no interval.

Formalization scope

Mathlib has Brownian motion but no stochastic integral or Itô formula, so the problem is stated analytically, in the objects the paper's proofs manipulate. A policy's value is the unique solution of its ODE boundary-value system with $C^1$ pasting; the identity with the expected cost (Dynkin's formula, the second half of Lemma 12) is not formalized, and optimality is over interval policies, to which the paper restricts (p. 8). Conventions: $L = 0$ , $m = 0$ , $M < 0$ , minimization; $\sigma_i$ is the volatility and $\sigma_i^2$ enters the ODE; $v_1 < v_2$ is an explicit hypothesis; controls are a two-constructor type, policies are structures carrying $k$ , the controls, strictly increasing breakpoints from $0$ to $U$ and distinct adjacent controls.

Corrections relative to the page: Theorem 1's uniqueness half excludes $\Delta h_1 = \Delta h_2 = 0$ ; Lemma 22 (204) is stated strictly; Lemmas 9–10 carry the hypotheses of condition (9) that their proofs use; the exclusivity claim of p. 13 is dropped (only exhaustiveness is stated); (73)'s $\sigma_1^2$ in the control-2 equation is read as $\sigma_2^2$ .

The encoding cannot be trivialized: the value fixes both boundary values and $C^1$ gluing, so no policy has arbitrarily low "values"; optimality quantifies over policies of every length and all their values at every point of $[0,U]$ ; and the policy structure forbids empty pieces and repeated adjacent controls, so $k$ is the true number of intervals.

Needed infrastructure: elementary real analysis (exponential inequalities, derivatives of explicit functions, the intermediate value theorem), a one-dimensional maximum principle for $\mu W' + \frac{\sigma^2}{2}W'' \ge 0$ with piecewise-constant coefficients, and linear independence of $1, x, e^{-v_1x}, e^{-v_2x}$ . The comparison principle and the interval-policy layer are reusable for other one-dimensional switching problems. Proofs of any milestone are welcome, as is a formal Dynkin link once Mathlib has stochastic integration.

Selected references

Z. Wang, S. Zenios, New Venture Creation: A Drift-Variance Diffusion Control Model, SSRN working paper 3667132; Operations Research, 2021. https://ssrn.com/abstract=3667132, https://doi.org/10.1287/opre.2021.2171
R. Radner, L. Shepp, Risk vs. profit potential: A model for corporate strategy, Journal of Economic Dynamics and Control 20(8), 1373–1393, 1996 (as cited on p. 33 of the source).
J. M. Harrison, N. Sunar, Investment timing with incomplete information and multiple means of learning, Operations Research 63(2), 442–457, 2015 (as cited on p. 33 of the source).

19 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Online Advance Scheduling with Overtime: A Primal-Dual Approach: The HOOP-BOT Online Primal-Dual Algorithm Is (1 − 2γmax·Rmax)/(1 + θ*)-CompetitiveResearch Paper

Motivation

Service systems such as outpatient clinics, surgical suites and diagnostic units book requests one at a time. When a patient calls, the scheduler commits at once to a provider and a day, without knowing who will call next. Each provider has a planned working time per day, which can be stretched by overtime at a cost. Keyvanshokooh, Shi and Van Oyen (MSOM 2019; accepted manuscript SSRN 3352166) study this problem when the arrivals are adversarial, and analyse it by competitive analysis: an online policy is judged by the worst case, over all arrival sequences, of the ratio between its value and the value of an offline planner who knows the whole sequence.

The paper sits in the line of online primal-dual algorithms for packing problems: online b-matching (Kalyanasundaram and Pruhs 2000), AdWords (Mehta, Saberi, Vazirani and Vazirani 2005), ad auctions with budgets (Buchbinder, Jain and Naor 2007) and the general framework of Buchbinder and Naor 2009. In all of these, capacity is a hard limit. Overtime turns capacity into a soft limit with a price, and the algorithm must decide when to start paying it.

Setting

There are $n$ servers $i$ , $T$ days $t$ and $m$ customers $j$ , numbered in order of arrival. Server $i$ on day $t$ has a regular capacity $B_{i,t}>0$ and an overtime budget $U_{i,t}\ge 0$ , and server $i$ pays $d_i\ge 0$ per unit of overtime. Customer $j$ needs service time $b_{i,j}>0$ and brings reward $c_{i,j}$ at server $i$ , normalized so that $c_{i,j}/b_{i,j}\ge 1$ .

The offline problem (P) chooses $y_{i,j,t}\in\{0,1\}$ and overtime $v_{i,t}$ to maximize $\sum_{t,i,j}c_{i,j}y_{i,j,t}-\sum_{t,i}d_iv_{i,t}$ subject to: each customer is served at most once; $\sum_j b_{i,j}y_{i,j,t}\le B_{i,t}+v_{i,t}$ ; and $0\le v_{i,t}\le U_{i,t}$ . Its optimal value is $f^*$ . The dual (D) of the LP relaxation minimizes $\sum_{t,i}(B_{i,t}x_{i,t}+U_{i,t}u_{i,t})+\sum_jz_j$ subject to $b_{i,j}x_{i,t}+z_j\ge c_{i,j}$ , $x_{i,t}-u_{i,t}\le d_i$ and $x,u,z\ge 0$ .

The instance parameters are

\gamma_{\max}=\max_{i,j}\frac{c_{i,j}}{b_{i,j}},\quad d_{\max}=\max_id_i,\quad R_{\max}=\max_{i,j,t}\frac{b_{i,j}}{B_{i,t}},\quad \alpha=(1+R_{\max})^{1/R_{\max}},

together with $\lambda=\max(\max_{i,j}\{c_{i,j}/b_{i,j}-d_i\},0)$ and $\zeta=\min(d_{\max},\gamma_{\max})$ .

HOOP-BOT (Algorithm 1) keeps prices $x_{i,t}$ (regular capacity, initially $0$ ) and $u_{i,t}$ (overtime, initially $1$ ). Customer $j$ is offered the server-date maximizing $c_{i,j}-b_{i,j}x_{i,t}$ and is rejected if that value is negative. If it is accepted at $(i,t)$ , then:

while $0\le x_{i,t}<d_i$ , regular capacity is used and $x_{i,t}\leftarrow x_{i,t}(1+b_{i,j}/B_{i,t})+\theta_1c_{i,j}/B_{i,t}$ , capped at $d_i$ ;
otherwise overtime is used: $u_{i,t}\leftarrow u_{i,t}(1+b_{i,j}/(B_{i,t}+U_{i,t}))+\theta_2\bar c_{i,j}/(B_{i,t}+U_{i,t})$ with $\bar c_{i,j}=c_{i,j}-d_ib_{i,j}$ , then $x_{i,t}\leftarrow u_{i,t}+d_i$ and $v_{i,t}\leftarrow v_{i,t}+b_{i,j}$ .

The output $(y,v)$ may exceed capacity by one customer per threshold. The paper converts it into a feasible solution $(\tilde y,\tilde v)$ of value $\tilde f_P$ .

Formalization targets

Goal: Theorem 1 (p. 14)

With $\theta_1=\theta_2=\theta^*$ , where

\theta^*=\frac{(1+R_{\max})(\zeta+\lambda)+\sqrt{(1+R_{\max})^2(\zeta+\lambda)^2+4(1+R_{\max})(\alpha-(1+R_{\max}))\zeta\lambda}}{2(\alpha-(1+R_{\max}))},

for every instance and every tie-break,

\tilde f_P\ \ge\ \frac{1-2\gamma_{\max}R_{\max}}{1+\theta^*}\,f^*.

Milestones

Proposition 2 (p. 19): the prices $(x,u,z)$ are feasible for (D) at every iteration.
Weak duality (proof of Proposition 4, (25), p. 24): $f^*\le g_D$ .
The technical inequality (proof of Lemma 1, p. 20): $\ln(1+x)/x$ is non-increasing on $(0,1]$ .
(15) (proof of Lemma 1, p. 20): along Rule (I), $\tilde x^{(K_1)}+\theta_1\ge\theta_1\alpha^{\sum b_{i,j}/B_{i,t}}$ , so $\tilde x^{(K_1)}>(\alpha-1)\theta_1$ .
Lemma 1 (p. 20): with $\theta_1=\zeta/(\alpha-1)$ , overrunning $B_{i,t}$ forces $\tilde x^{(K_1)}>d_i$ (if $d_i\le\gamma_{\max}$ ) or prices the customer out (if $d_i>\gamma_{\max}$ ).
Lemma 2, (16) (p. 21): with $\theta_1=\theta_2=\theta^*$ , overrunning $B_{i,t}+U_{i,t}$ prices customer $K_2$ out.

Significance

Theorem 1 is the paper's headline result: a worst-case guarantee for online scheduling in which capacity can be expanded at a price. In the proportional case $c_{i,j}=b_{i,j}$ and as $R_{\max}\to 0$ , the paper reads it as a ratio of at least $(e-1)/(e+\sqrt e)\approx 0.4$ , to be compared with the $1-1/e$ upper bound of its Theorem 2. The guarantee underlies the rolling-horizon policy of §5 and the case study of §6.

The formal statements add three things. They fix the hypotheses: the page leaves $R_{\max}<1$ , $b_{i,j}>0$ and the choice of $\theta_1,\theta_2$ implicit. They pin the conversion from almost-feasible to feasible solution, which the paper describes only inside a proof. And they settle the truth of the result. No part of this paper has been formalized before. The technical inequality is shared with the Buchbinder–Jain–Naor mission and is referenced from there.

Difficulty

The obvious argument is the usual primal-dual accounting: bound the dual increase by $(1+\theta)$ times the primal increase at every iteration, sum, and lose a factor $1-2\gamma_{\max}R_{\max}$ when the at most two overflowing customers per server-date are dropped. The step that needs care is the first overtime iteration of a server-date. There the regular price has been capped at $d_i$ while the overtime price still has its initial value $1$ , so the identity $x=u+d_i$ that the per-iteration bound relies on is not yet in force. The initial dual value $\sum U_{i,t}u_{i,t}$ is also not a sum of per-iteration increments. Any proof of the goal has to deal with both points.

Formalization scope

Everything is in ℝ. Indices are Fin n, Fin T and Fin m, with customers $0,\dots,m-1$ in arrival order; $b_{i,j}$ and $c_{i,j}$ are written customer first. The maxima in (1) are suprema over nonempty finite index sets. Algorithm 1 is defined step by step, exactly as printed (Steps 1–13, $u_{i,t}=1$ initially, the tests $0\le c-bx$ , $0\le x<d$ and $x>d$ as printed). Its run is the fold of one step over the customers. The argmax tie-break is a parameter, and statements about the run hold for every selector that returns a maximizer.

Standing assumptions: $n,T,m\ge 1$ ; $B_{i,t}>0$ ; $U_{i,t}\ge 0$ ; $d_i\ge 0$ ; $b_{i,j}>0$ ; $c_{i,j}\ge b_{i,j}$ (the paper's normalization); and $R_{\max}<1$ . The page does not state the last one, but $\theta^*$ divides by $\alpha-(1+R_{\max})$ , which vanishes at $R_{\max}=1$ . $\theta^*$ depends on the whole instance, as it does in the paper.

"Admits competitive ratio $r$ " is formalized through Definition 1 and Proposition 4. There is a feasible $(\tilde y,\tilde v)$ of (P) with $\tilde y\le y$ and $\tilde v\le v$ , differing from $y$ in at most two customers per server-date, whose value is at least $r$ times the optimal value $f^*$ of (P), taken as the greatest objective value of a feasible solution. A statement about a closed-form allocation, a fixed tie-break or an initialization other than $u_{i,t}=1$ would be a different theorem and is excluded. The goal is posed exactly as printed, and the proposers record a counterexample to it. Lemma 1 and (15) are stated for the Rule (I) recursion along the customers allocated to one server-date, abstracted from the run.

Not formalized: the $R_{\max}\to 0$ limit (12); Theorem 2 and Lemma 3 (the $1-1/e$ upper bound); Proposition 1, which fails as printed at the first overtime iteration; Propositions 3 and 5; and the case study. Welcome contributions include proofs of the milestones and reusable facts about multiplicative price updates.

Selected references

E. Keyvanshokooh, C. Shi, M. P. Van Oyen, Online Advance Scheduling with Overtime: A Primal-Dual Approach, Manufacturing & Service Operations Management, 2019 (accepted manuscript, SSRN 3352166). https://doi.org/10.1287/msom.2019.0832, https://ssrn.com/abstract=3352166
N. Buchbinder, K. Jain, J. Naor, Online primal-dual algorithms for maximizing ad-auctions revenue, ESA 2007, LNCS 4698, 253–264. https://doi.org/10.1007/978-3-540-75520-3_24
N. Buchbinder, J. Naor, The design of competitive online algorithms via a primal–dual approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009, 93–263. https://doi.org/10.1561/0400000024
B. Kalyanasundaram, K. R. Pruhs, An optimal deterministic algorithm for online b-matching, Theoretical Computer Science 233(1–2), 2000, 319–325. https://doi.org/10.1016/S0304-3975(99)00140-1
A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized on-line matching, FOCS 2005, 264–273. https://doi.org/10.1109/SFCS.2005.12

8 thms3 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Proximal Gradient Methods with Adaptive Subspace Sampling: Random Subspace Proximal Gradient Descent Converges Linearly in ExpectationResearch Paper

Motivation

Large-scale composite problems $\min_x f(x)+g(x)$ , with a smooth loss $f$ and a nonsmooth regularizer or constraint $g$ , are routinely solved by proximal gradient methods. When the dimension is large, computing the full gradient at every step is expensive, and randomized coordinate descent updates only a few coordinates at a time. Classical proximal coordinate descent, however, requires $g$ to be separable along the coordinates, which excludes total-variation penalties, group norms with overlapping groups, and most constraint sets.

Grishchenko, Iutzeler and Malick (arXiv:2004.13356, Mathematics of Operations Research, 2021) propose a randomized proximal subspace descent (RPSD): the gradient step is taken only along a randomly drawn subspace, while the proximal step is applied to the full vector, so $g$ need not be separable. Their motivation is twofold: random subspaces include coordinate blocks as well as sketching-type projections, and the subspace distribution can later be adapted to the structure that the proximal operator identifies (§3 of the paper, not part of this mission). This mission formalizes the convergence theory of the non-adaptive method, which the adaptive variants build on.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$ . The problem is

\min_{x\in\mathbb R^n} f(x)+g(x), \tag{1}

where $f$ is $L$ -smooth (differentiable with $L$ -Lipschitz gradient) and $\mu$ -strongly convex, and $g:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ is convex, proper and lower semicontinuous (Assumption 1). Problem (1) then has a unique minimizer $x^\star$ . The proximity operator of $g$ with step $\gamma>0$ is

\mathbf{prox}_{\gamma g}(v)=\operatorname*{argmin}_{y\in\mathbb R^n}\Big\{g(y)+\frac1{2\gamma}\|y-v\|_2^2\Big\}.

A selection $\mathfrak S$ is a random linear subspace of $\mathbb R^n$ ; $P_F$ denotes the orthogonal projection onto a subspace $F$ . A selection is admissible if $\mathbb P[x\in\mathfrak S^\perp]<1$ for every nonzero $x$ : no nonzero direction is almost surely missed. The average projection is the matrix

\mathsf P=\mathbb E[P_{\mathfrak S}],

and $\lambda_{\min}(\mathsf P)$ , $\lambda_{\max}(\mathsf P)$ are its extreme eigenvalues. The $\mathsf P$ -norm is $\|v\|_{\mathsf P}^2=\langle v,\mathsf Pv\rangle$ , and $\mathsf Q=\mathsf P^{-1/2}$ .

Given i.i.d. admissible selections $\mathfrak S^1,\mathfrak S^2,\dots$ (Assumption 2), a step size $\gamma$ and a starting point $z^0$ , RPSD (Algorithm 1) sets $x^1=\mathbf{prox}_{\gamma g}(\mathsf Q^{-1}z^0)$ and, for $k\ge1$ ,

y^k=\mathsf Q\big(x^k-\gamma\nabla f(x^k)\big),\qquad z^k=P_{\mathfrak S^k}y^k+(I-P_{\mathfrak S^k})z^{k-1},\qquad x^{k+1}=\mathbf{prox}_{\gamma g}\big(\mathsf Q^{-1}z^k\big).

The auxiliary sequence $z^k$ is updated only inside the random subspace $\mathfrak S^k$ . Its fixed point is $z^\star=y^\star=\mathsf Q(x^\star-\gamma\nabla f(x^\star))$ .

Formalization targets

Goal: Theorem 1 (p. 5)

For every $\gamma\in(0,2/(\mu+L)]$ , the iterates converge almost surely to $x^\star$ , with

\mathbb E\big[\|x^{k+1}-x^\star\|_2^2\big]\le\Big(1-\lambda_{\min}(\mathsf P)\frac{2\gamma\mu L}{\mu+L}\Big)^k C,\qquad C=\lambda_{\max}(\mathsf P)\,\|z^0-\mathsf Q(x^\star-\gamma\nabla f(x^\star))\|_2^2 .

Both clauses are part of the goal: the rate for every $k\ge0$ , and almost-sure convergence.

Milestones

Lemma 1 (p. 3): for an admissible selection, $\mathsf P$ is positive definite, with $\lambda_{\min}(\mathsf P)>0$ and $\lambda_{\max}(\mathsf P)\le1$ .
Lemma 2 (p. 5): with $\mathcal F^k=\sigma(\mathfrak S^1,\dots,\mathfrak S^k)$ ,

\mathbb E\big[\|z^k-z^\star\|_2^2\mid\mathcal F^{k-1}\big]=\|z^{k-1}-z^\star\|_2^2+\|y^k-y^\star\|_{\mathsf P}^2-\|z^{k-1}-z^\star\|_{\mathsf P}^2 .

Lemma 3 (p. 6), for $\gamma\in(0,2/(\mu+L)]$ :

\|y^k-y^\star\|_{\mathsf P}^2-\|z^{k-1}-z^\star\|_{\mathsf P}^2\le-\lambda_{\min}(\mathsf P)\frac{2\gamma\mu L}{\mu+L}\|z^{k-1}-z^\star\|_2^2 .

Display (a) of the proof of Theorem 1 (p. 6): $\mathbb E\|z^k-z^\star\|_2^2\le\big(1-\lambda_{\min}(\mathsf P)\tfrac{2\gamma\mu L}{\mu+L}\big)^k\|z^0-z^\star\|_2^2$ .
Display (b) of the proof of Theorem 1 (p. 6): $\|x^{k+1}-x^\star\|_2^2\le\|z^k-z^\star\|_{\mathsf P}^2\le\lambda_{\max}(\mathsf P)\|z^k-z^\star\|_2^2$ .

Significance

The theorem shows that a proximal gradient method can be randomized along arbitrary subspaces without any separability of the nonsmooth term, at the price of the change of basis $\mathsf Q$ , and that it keeps the usual step-size range of deterministic proximal gradient descent. The rate depends on the sampling only through $\lambda_{\min}(\mathsf P)$ ; for coordinate sampling with probabilities $p_i$ this is $\min_i p_i$ , which recovers the familiar dependence of coordinate methods. The same two lemmas are the template for the adaptive method ARPSD of §3, whose analysis states that Lemmas 2–3 "can be directly extended".

On the formal side, the result is proved on paper but, as far as the platform's index shows, no random-subspace or coordinate-type proximal method with a non-separable regularizer has a machine-checked convergence proof. A complete development would produce reusable pieces: the average projection of a random subspace and its spectrum, the conditional-expectation identity for a random projection update, and a pathwise-to-almost-sure convergence argument for linearly convergent mean-square errors.

Difficulty

Each step is short on paper, and the difficulty lies in what the paper takes for granted. The conditional expectation in Lemma 2 requires the iterates $z^{k-1}$ and $y^k$ to be measurable with respect to the past selections, which in turn rests on the proximity operator being single-valued and measurable, and on the integrability of every quantity being conditioned. The deterministic contraction of Lemma 3 uses two external results, the co-coercivity estimate for strongly convex smooth functions and the nonexpansiveness of the proximity operator, neither of which is stated inside the paper. Lemma 1 needs the spectral theory of a Bochner integral of projections. The step from a summable mean-square error to almost-sure convergence needs the monotone convergence theorem and a Borel–Cantelli-type argument. None of these is deep, but together they account for most of the work.

A frequent first idea is to analyse $x^k$ directly as a randomized proximal gradient iterate; this fails because $x^k$ is not a contraction in any fixed norm along a single random subspace, which is why the paper tracks the auxiliary sequence $z^k$ .

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), matrices are continuous linear maps, $P_F$ is Mathlib's Submodule.starProjection, and inner products are inner ℝ.
A selection is a random subspace: $\mathfrak S^{k+1}=\mathrm{sel}(\xi_k)$ , where $(\xi_k)_{k\ge0}$ are i.i.d. random variables in a measurable space $\Theta$ (so Lean's index $k$ is the paper's $k+1$ ). Definition 2's construction from a covering family is subsumed, since every subspace is a sum of members of the covering family of all subspaces. The map $\theta\mapsto P_{\mathrm{sel}(\theta)}x$ is assumed measurable.
$\mathsf P$ is characterized pointwise by $\mathsf Px=\int P_{\mathfrak S^1(\omega)}x\,d\mathbb P(\omega)$ ; with the measurability hypothesis this is the true expectation, never a junk zero integral.
$\mathsf Q=\mathsf P^{-1/2}$ is encoded as a positive map with $\mathsf Q\mathsf P\mathsf Q=I$ and a two-sided inverse $\mathsf Q^{-1}$ , which determines it uniquely as the positive square root of $\mathsf P^{-1}$ .
$\lambda_{\min}$ and $\lambda_{\max}$ are the Rayleigh infimum and supremum over the unit sphere. Lemma 1 adds $n\ge1$ , because $\mathbb R^0$ has no eigenvalues.
$g$ is the pair $(\operatorname{dom}g,g)$ : proper is a nonempty domain, lower semicontinuity is a closed epigraph. The prox is the published BoydADMM.Prox.IsProx with weight $1/\gamma$ . $f$ is differentiable, StrongConvexOn with modulus $\mu$ , with $L$ -Lipschitz gradient; $\mu>0$ and $L>0$ are explicit.
Added hypothesis: Lemma 3 assumes $\gamma\in(0,2/(\mu+L)]$ , which its proof uses and without which it is false. Lemma 2 and display (b) do not need the upper bound and do not assume it.
The minimizer $x^\star$ and the RPSD run are universally quantified; expectations are Bochner integrals.

The goal cannot be trivialized: $\mathsf P$ is the true average projection, $\mathsf Q$ is the positive square root of $\mathsf P^{-1}$ , admissibility, independence and identical distribution are all kept, the step-size range is exactly $(0,2/(\mu+L)]$ , the runs are universally quantified, and both the rate and the almost-sure convergence are required.

Contributions are welcome on the general infrastructure as well: the spectrum of an average of random orthogonal projections, measurability of the proximity map, and conditional expectations of random projection updates are all reusable beyond this mission.

Selected references

D. Grishchenko, F. Iutzeler, J. Malick, Proximal gradient methods with adaptive subspace sampling, Mathematics of Operations Research, 2021; arXiv:2004.13356v1. https://arxiv.org/abs/2004.13356
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011 (Prop. 12.27, Th. 26.2). https://doi.org/10.1007/978-1-4419-9467-7
S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 2015 (Lemma 3.11). https://arxiv.org/abs/1405.4980
P. Richtárik, M. Takáč, Iteration complexity of randomized block-coordinate descent methods for minimizing a composite function, Mathematical Programming 144, 2014. https://doi.org/10.1007/s10107-012-0614-z

8 thms3 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research+1·Captain: mikedeng1

Multivariate Monotone Inclusions in Saddle Form: The Asynchronous Block-Iterative Saddle Splitting Algorithm Converges Weakly to a Primal-Dual Kuhn–Tucker PointResearch Paper

Motivation

Many problems in convex optimization, variational inequalities, game theory and signal processing are systems of monotone inclusions coupled by linear operators: several unknowns $x_i$ in different Hilbert spaces, each subject to its own maximally monotone, cocoercive and Lipschitzian operators, and tied together through linear maps $L_{ki}$ and composite terms. Bùi and Combettes (arXiv:2002.06135, Mathematics of Operations Research, 2022) introduce a single model, Problem 1.1, that contains a large part of these formulations and design algorithms for it that are fully split (each operator is used separately, set-valued operators through their resolvents and single-valued ones through forward evaluations), block-iterative (only some blocks are updated at each iteration) and asynchronous (updates may use information computed up to $T$ iterations earlier).

The paper places itself after a line of primal-dual splitting methods: Briceño-Arias and Combettes (SIAM J. Optim. 2011, doi:10.1137/10081602x) for a two-operator monotone+skew model, Alotaibi, Combettes and Shahzad (SIAM J. Optim. 2014) for Fejér approximation of a Kuhn–Tucker set, Combettes and Eckstein (Math. Program. B168, 2018) for asynchronous block-iterative primal-dual decomposition, and the projective splitting methods of Johnstone and Eckstein (2020–2021). These earlier methods work in the primal-dual space $\mathcal H\oplus\mathcal G$ . The new idea is to reformulate the problem as finding a zero of a saddle operator on a larger space and to approximate that zero set from outside by half-spaces.

Setting

Let $I$ and $K$ be finite index sets and let $(\mathcal H_i)_{i\in I}$ , $(\mathcal G_k)_{k\in K}$ be real Hilbert spaces, with Hilbert direct sums $\mathcal H=\bigoplus_i\mathcal H_i$ and $\mathcal G=\bigoplus_k\mathcal G_k$ . For every $i$ and $k$ the data are:

$A_i:\mathcal H_i\to2^{\mathcal H_i}$ maximally monotone, $C_i$ cocoercive with constant $\alpha^c_i>0$ , $Q_i$ monotone and $\alpha^\ell_i$ -Lipschitzian, and $R_i:\mathcal H\to\mathcal H_i$ such that $R=(R_i)_i$ is monotone and $\chi$ -Lipschitzian on $\mathcal H$ ;
$B^m_k$ , $D^m_k$ maximally monotone on $\mathcal G_k$ , $B^c_k$ , $D^c_k$ cocoercive with constants $\beta^c_k,\delta^c_k>0$ , and $B^\ell_k$ , $D^\ell_k$ monotone and Lipschitzian with constants $\beta^\ell_k,\delta^\ell_k$ ;
bounded linear $L_{ki}:\mathcal H_i\to\mathcal G_k$ , and vectors $s^*_i\in\mathcal H_i$ , $r_k\in\mathcal G_k$ .

The parallel sum of $B,D:\mathcal G_k\to2^{\mathcal G_k}$ is $B\,\square\,D=(B^{-1}+D^{-1})^{-1}$ . Write $\mathsf B_k=B^m_k+B^c_k+B^\ell_k$ and $\mathsf D_k=D^m_k+D^c_k+D^\ell_k$ . The primal problem (1.1) asks for $\overline x\in\mathcal H$ with

s^*_i\in A_i\overline x_i+C_i\overline x_i+Q_i\overline x_i+R_i\overline x+\sum_{k\in K}L^*_{ki}\Big((\mathsf B_k\,\square\,\mathsf D_k)\Big(\sum_{j\in I}L_{kj}\overline x_j-r_k\Big)\Big)\quad(\forall i\in I).

Its set of solutions is $\mathscr P$ . The dual problem (1.2) asks for $\overline v^*\in\mathcal G$ such that some $x\in\mathcal H$ satisfies $s^*_i-\sum_jL^*_{ji}\overline v^*_j\in A_ix_i+C_ix_i+Q_ix_i+R_ix$ and $\overline v^*_k\in(\mathsf B_k\,\square\,\mathsf D_k)(\sum_jL_{kj}x_j-r_k)$ ; its set of solutions is $\mathscr D$ . The Kuhn–Tucker set $\mathsf Z\subset\mathcal H\oplus\mathcal G$ (2.13) collects the pairs $(\overline x,\overline v^*)$ satisfying the first condition at $\overline x$ and $\sum_jL_{kj}\overline x_j-r_k\in\mathsf B_k^{-1}\overline v^*_k+\mathsf D_k^{-1}\overline v^*_k$ .

On $\mathbf X=\mathcal H\oplus\mathcal G\oplus\mathcal G\oplus\mathcal G$ the saddle operator $\boldsymbol{\mathcal S}$ (2.11) maps $(x,y,z,v^*)$ to the product of the sets $-s^*_i+A_ix_i+C_ix_i+Q_ix_i+R_ix+\sum_kL^*_{ki}v^*_k$ , $\ B^m_ky_k+B^c_ky_k+B^\ell_ky_k-v^*_k$ , $\ D^m_kz_k+D^c_kz_k+D^\ell_kz_k-v^*_k$ and $\{r_k+y_k+z_k-\sum_iL_{ki}x_i\}$ . It splits as $\boldsymbol{\mathcal S}=\mathbf M+\mathbf C$ (Definition 2.4), where $\mathbf C$ collects the cocoercive operators.

Algorithm 3.4 runs, at iteration $n$ , over activated blocks $I_n\subset I$ , $K_n\subset K$ . For $i\in I_n$ it computes a resolvent step $a_{i,n}=J_{\gamma A_i}(\cdot)$ from the delayed iterate $x_{\pi_i(n)}$ ; for $k\in K_n$ it computes $b_{k,n}$ , $d_{k,n}$ from resolvents of $B^m_k$ , $D^m_k$ at the delayed iterate $\omega_k(n)$ . Blocks that are not activated keep their previous values. From these quantities it forms a half-space containing $\operatorname{zer}\boldsymbol{\mathcal S}$ , measured by a number $\Delta_n$ that involves $\alpha=\min\{\alpha^c_i,\beta^c_k,\delta^c_k\}$ . If $\Delta_n>0$ , it moves $(x_n,y_n,z_n,v^*_n)$ toward that half-space with relaxation $\lambda_n\in[\varepsilon,2-\varepsilon]$ ; otherwise the iterate stays put.

Formalization targets

Goal: Theorem 3.5

Under Assumptions 3.1–3.3 (step-size ranges tied to $\alpha$ , $\sigma>1/(4\alpha)$ and $\varepsilon$ by (3.1); every block activated at least once in every $P+1$ consecutive iterations; delays at most $T$ ), if the dual problem has a solution, then every run of Algorithm 3.4 satisfies

\sum_n\|x_{i,n+1}-x_{i,n}\|^2<\infty,\qquad x_{i,n}-a_{i,n}\to0,\qquad v^*_{k,n}-e^*_{k,n}\to0,

together with the analogous statements for $y,z,v^*$ and $b,d$ . There exist $\overline x\in\mathscr P$ and $\overline v^*\in\mathscr D$ with $(\overline x,\overline v^*)\in\mathsf Z$ such that

x_{i,n}\rightharpoonup\overline x_i,\qquad a_{i,n}\rightharpoonup\overline x_i,\qquad v^*_{k,n}\rightharpoonup\overline v^*_k.

Milestones

In attack order:

Proposition 2.2(i)–(ii): $\boldsymbol{\mathcal S}$ is maximally monotone and $\operatorname{zer}\boldsymbol{\mathcal S}$ is closed and convex.
Proposition 2.2(iii)–(iv): zeros of $\boldsymbol{\mathcal S}$ project into $\mathsf Z\subset\mathscr P\times\mathscr D$ , and $\mathscr D\neq\varnothing\Leftrightarrow\operatorname{zer}\boldsymbol{\mathcal S}\neq\varnothing\Leftrightarrow\mathsf Z\neq\varnothing\Rightarrow\mathscr P\neq\varnothing$ .
Proposition 2.5: $\boldsymbol{\mathcal S}=\mathbf M+\mathbf C$ , $\mathbf M$ maximally monotone, $\mathbf C$ $\alpha$ -cocoercive, and the half-spaces containing $\operatorname{zer}\boldsymbol{\mathcal S}$ .
Lemma A.4: the relaxed half-space outer-approximation iteration (A.3) is Fejér monotone and converges weakly when every weak sequential cluster point lies in $Z$ .
Proposition 2.6: the iteration (2.32) on $\mathbf X$ converges weakly to a zero of $\boldsymbol{\mathcal S}$ when its three stated residual conditions hold.
Lemmas A.1, A.2 and A.3: boundedness of resolvent sequences, strong monotonicity of $\gamma^{-1}\mathrm{Id}-A$ , and the vanishing of the delayed differences $x_{\vartheta_i(n)}-x_n$ .

Significance

Theorem 3.5 gives weak convergence of a method that uses each operator of Problem 1.1 separately, needs no inversion of linear operators and no knowledge of $\|L\|$ , and updates nonempty subsets of blocks subject to the coverage windows and bounded delays of Assumptions 3.2–3.3. It produces primal and dual solutions together. Section 4 of the paper derives from it algorithms for variational inequalities over sums of sets and for multivariate convex minimization with infimal convolutions. The hypothesis is dual solvability. Remark 2.3 shows that primal solvability alone is not enough: there are instances with $\mathscr P\neq\varnothing$ and $\mathsf Z=\varnothing$ .

The theorem is proved in the paper. A formalization adds machine-checked foundations that later work in splitting methods can reuse: the saddle operator and its maximal monotonicity; the Fejér outer-approximation principle in Hilbert space (Lemma A.4, cited by the paper from an encyclopedia entry); and the asynchrony lemma (Lemma A.3). To our knowledge none of these results has been formalized before.

Difficulty

The obvious approach would be to show that Algorithm 3.4 is a Fejér-monotone iteration toward $\mathsf Z$ in $\mathcal H\oplus\mathcal G$ . That approach fails: for the general Problem 1.1, no half-space separating the current point from $\mathsf Z$ can be computed from separate operator evaluations (Remark 2.3(iii)). The algorithm instead targets $\operatorname{zer}\boldsymbol{\mathcal S}$ in the larger space $\mathbf X$ . The link back to $\mathscr P$ , $\mathscr D$ and $\mathsf Z$ is Proposition 2.2.

The second difficulty is asynchrony. The half-space at iteration $n$ is built from points computed at earlier iterations, with stale step sizes. To show that the weak cluster points are zeros of $\boldsymbol{\mathcal S}$ , one has to control these delays (Lemma A.3) and use the cocoercive and Lipschitzian terms uniformly over the step-size ranges (Lemmas A.1–A.2).

Formalization scope

Spaces. Every space is a complete real inner product space. $\mathcal H$ and $\mathcal G$ are PiLp 2 over finite index types, and $\mathbf X$ is a nested WithLp 2 product, so all norms and inner products are the Hilbert ones (not sup norms).
Operators. Set-valued operators are maps E → Set E. Monotonicity, maximal monotonicity, zer, cocoercivity, resolvents and weak convergence are the published ThreeOpSplitting.Convergence definitions; inverses and sums of set-valued maps are the published DouglasRachfordPPA.GenDR ones.
Runs. A run of Algorithm 3.4 is a predicate on given sequences that pins every assignment of (3.3). This includes the delayed indices inside the step sizes, the carry-over of inactive blocks (stated at $n+1$ ), the recomputation of $e_{k,n}$ for every $k$ , and $\Delta_n$ with the factor $(4\alpha)^{-1}$ at the current iterates. The resolvents are given maps constrained by the resolvent identity at every positive step.
Constants and assumptions. $\alpha$ is pinned as the least cocoercivity constant. The delay bound $n-T\le\pi_i(n)\le n$ is written without natural-number subtraction. " $\varlimsup\Delta_n\le0$ " in Proposition 2.6 is stated as "eventually $\Delta_n\le\delta$ for every $\delta>0$ ".
Ruling out trivial readings. The run predicate determines every assignment of (3.3), so no free choice of outputs makes the theorem trivial. The hypothesis is dual solvability $\mathscr D\neq\varnothing$ exactly as in (1.2), not the stronger-looking $\operatorname{zer}\boldsymbol{\mathcal S}\neq\varnothing$ (equivalent only by Proposition 2.2). The conclusion is weak convergence to a pair that is simultaneously primal, dual and Kuhn–Tucker. A sorry-free check shows that the goal's hypotheses are jointly satisfiable.
Not included. Theorem 3.7 (strong convergence of a Haugazeau-type variant) with Proposition 2.7 and Lemma A.5, Proposition 2.2(v), and the applications of Section 4.
Reusable parts. The saddle operator and its splitting, Lemma A.4, Lemma A.3, and Lemmas A.1–A.2 are stated in general form and can serve other splitting missions. Contributions of auxiliary results are welcome, for example demiclosedness of maximally monotone operators, Minty's theorem in the published encoding, and Fejér-monotone weak convergence (Opial).

Selected references

M. N. Bùi and P. L. Combettes, Multivariate monotone inclusions in saddle form, Mathematics of Operations Research, 2022; preprint arXiv:2002.06135v3, 2021. https://arxiv.org/abs/2002.06135
H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
L. M. Briceño-Arias and P. L. Combettes, A monotone+skew splitting model for composite monotone inclusions in duality, SIAM Journal on Optimization 21, 2011. https://doi.org/10.1137/10081602x
P. L. Combettes and J. Eckstein, Asynchronous block-iterative primal-dual decomposition methods for monotone inclusions, Mathematical Programming B168, pp. 645–672, 2018 (reference [25] of arXiv:2002.06135).
P. L. Combettes, Fejér-monotonicity in convex optimization, in: Encyclopedia of Optimization, vol. 2, pp. 106–114, Springer, 2001 (reference [22] of arXiv:2002.06135; source of Lemma A.4).

15 thms3 active usersReviewed

Calculus of Variations Operations Research Probability+1·Captain: mikedeng1

Large Deviations for the Single-Server Queue and the Reneging Paradox: The Long-Time Decay Rate of Atypical Reneging Is an Explicit C(γ) Independent of the Reneging RateResearch Paper

Motivation

Customer abandonment, or reneging, is a basic feature of service systems: call centres, emergency departments and online platforms all lose customers who give up waiting. The number of reneging customers is a natural performance measure, and in many-server and single-server models alike it is the quantity managers monitor and are penalised for. Typical (law-of-large-numbers) behaviour of reneging is well understood; the question here is how unlikely atypical amounts of reneging are, over long horizons.

R. Atar, A. Budhiraja, P. Dupuis and R. Wu (arXiv:1903.06870; Mathematics of Operations Research, 2022) answer this for the single-server queue with exponential patience, in the many-arrivals scaling. They prove a sample-path large deviation principle for the pair (queue length, cumulative reneging) and then solve the associated long-horizon variational problem in closed form. The answer has a counter-intuitive feature, which the authors call the reneging paradox: the exponential decay rate of the probability of observing reneging at an atypical long-run rate $\gamma$ does not depend on the reneging rate $\theta$ . Customers who are very patient and customers who are very impatient produce, over long horizons, the same large-deviation cost for the same atypical reneging rate.

Setting

Fix rates $\lambda,\mu,\theta>0$ (arrival, service, per-customer reneging), an initial queue length $x_0\ge0$ and a horizon $T>0$ . Throughout the mission $\lambda\ge\mu$ (the paper's standing assumption from §2.2 on). The Skorohod map on $[0,T]$ is

\Gamma(\psi)(t)=\psi(t)-\inf_{0\le s\le t}[\psi(s)\wedge0],

and the local cost is $\ell(x)=x\log x-x+1$ for $x\ge0$ .

A path is a pair $(\xi,\zeta)$ of continuous functions $[0,T]\to\mathbb R_+$ ; $\xi$ is the queue length and $\zeta$ the cumulative number of reneged customers, both on the fluid scale. A control is a triple $\varphi=(\varphi_1,\varphi_2,\varphi_3)$ of measurable maps $[0,T]\to\mathbb R_+$ that perturb the arrival, service and reneging rates; it is admissible for $(\xi,\zeta)$ , written $\varphi\in\mathcal U(\xi,\zeta)$ , if for all $t\in[0,T]$

\xi(t)=\Gamma\Big(x_0+\lambda\!\int_0^{\cdot}\!\varphi_1-\mu\!\int_0^{\cdot}\!\varphi_2-\theta\!\int_0^{\cdot}\!\varphi_3\,\xi\Big)(t),\qquad\zeta(t)=\theta\int_0^t\varphi_3(s)\xi(s)\,ds .

The rate function is

I_T(\xi,\zeta)=\inf_{\varphi\in\mathcal U(\xi,\zeta)}\Big\{\lambda\!\int_0^T\!\ell(\varphi_1)+\mu\!\int_0^T\!\ell(\varphi_2)+\theta\!\int_0^T\!\xi\,\ell(\varphi_3)\Big\},

equal to $\infty$ when no control is admissible. The cost of seeing $\gamma T$ reneged customers by time $T$ is

I^*_{\gamma,T}=\inf\{I_T(\xi,\zeta):\zeta(T)=\gamma T\},

with the one-sided versions $I_{\gamma,T}$ (constraint $\zeta(T)\ge\gamma T$ ) and $\tilde I_{\gamma,T}$ (constraint $\zeta(T)\le\gamma T$ ). Finally

z_\gamma=\frac{\sqrt{\gamma^2+4\lambda\mu}-\gamma}{2\mu},\qquad C(\gamma)=\lambda\big(1-z_\gamma^{-1}\big)+\mu(1-z_\gamma)-\gamma\log z_\gamma .

Formalization targets

Goal: Theorem 2.3

\lim_{T\to\infty}\frac{I^*_{\gamma,T}}{T}=C(\gamma)\ (\gamma\ge0),\qquad\lim_{T\to\infty}\frac{I_{\gamma,T}}{T}=C(\gamma)\ (\gamma\ge\lambda-\mu),\qquad\lim_{T\to\infty}\frac{\tilde I_{\gamma,T}}{T}=C(\gamma)\ (0\le\gamma\le\lambda-\mu).

The limit depends on $\lambda,\mu,\gamma$ only; $\theta$ and $x_0$ appear in the hypotheses and inside $I_T$ , never in $C$ .

Milestones

The milestones follow the paper's proof, in order:

the reduction of $I_T$ to the class $\mathcal C_T$ of absolutely continuous paths with $\xi(0)=x_0$ , $\zeta(0)=0$ , $\zeta$ nondecreasing and $\zeta'=0$ a.e. on $\{\xi=0\}$ (§4, p. 18);
the representation $I_T(\xi,\zeta)=\int_0^TL(\xi,\xi',\zeta')\,ds$ with an explicit local rate $L$ (Lemma 4.1);
convexity of $L$ and of $I_T$ on $\mathcal C_T$ (Lemma 4.4);
existence and uniqueness of the constant $A$ solving the transcendental equation (5.9), and its asymptotics (Lemma 5.2);
the explicit candidate $(\bar\xi,\bar\zeta)$ of Construction 5.3: its terminal value $\bar\zeta(T)=\gamma T$ (Lemma 5.4), positivity and membership in $\mathcal C_T$ (Lemma 5.5), its cost and $I_T(\bar\xi,\bar\zeta)/T\to C(\gamma)$ (Lemma 5.6), and its optimality for $x_0>0$ (Lemma 5.7);
convexity of $\gamma\mapsto I^*_{\gamma,T}$ and its zero at the law-of-large-numbers rate $\gamma^*_T$ (Lemma 6.1);
(6.1) and the elementary properties of $C$ ; the upper bound $\limsup I^*_{\gamma,T}/T\le C(\gamma)$ (Proposition 6.2) and the lower bounds for $\gamma>0$ (Proposition 6.3) and $\gamma=0$ (Proposition 6.4).

Significance

The theorem gives the exact long-horizon decay rate of the probability of atypical reneging in the $M/M/1+M$ queue, in closed form, together with the explicit optimal path for $x_0>0$ . It shows that the patience parameter, which governs typical reneging, is invisible in the long-run large-deviation cost of atypical reneging. The paper treats the many-server analogue $M/M/n+M$ in its §7; that part is not in this mission.

The result is proved in the paper. None of it is formalized: Mathlib has no sample-path large deviations and no Skorohod problem, and the platform has no rate function for a reflected, state-dependent jump process. This mission formalizes the deterministic, variational half (§§4–6) of the paper; the probabilistic LDP itself (Theorem 2.1, proved in §3) is not a target.

Difficulty

The variational problem has a state-dependent cost ( $\xi\,\ell(\varphi_3)$ ) and a reflection constraint, so the obvious approach of guessing a constant-rate tilt and checking it fails: the optimal path is not linear, its constants solve the transcendental equation (5.9), and the minimizer must be shown to stay in the interior $\{\xi>0\}$ for large $T$ , which happens only beyond a horizon $T_0$ that genuinely grows with the data. The case $x_0=0$ , where the explicit candidate is not shown to be optimal, and $\gamma=0$ , where the reflection at zero is active, need separate arguments (Propositions 6.3 and 6.4). The final passage from $I^*$ to the one-sided problems relies on the shape of $\gamma\mapsto I^*_{\gamma,T}$ (Lemma 6.1).

Formalization scope

All declarations live in the namespace RenegingLD.MM1, in two definition files (Model for §2, Variational for §§4–6) and one theorem file per statement. The conventions are:

lam, mu stand for $\lambda,\mu$ . The standing assumptions $\lambda,\mu,\theta>0$ , $\mu\le\lambda$ , $x_0\ge0$ and $T>0$ are explicit hypotheses of every statement that needs them.
Paths and controls are functions $\mathbb R\to\mathbb R$ of which only $[0,T]$ is used; a path is required to be continuous and nonnegative on $[0,T]$ . Infima over the paper's $\mathcal D([0,T]:\mathbb R^2_+)$ are taken over all functions, which agrees because $I_T=\infty$ off continuous paths.
Admissible controls are additionally required to make $\varphi_1$ , $\varphi_2$ and $\varphi_3\xi$ integrable on $[0,T]$ , which the page's integrals presuppose.
$I_T$ , $I^*$ , $I$ , $\tilde I$ and $L$ take values in $[0,\infty]$ . The cost is a lower Lebesgue integral of nonnegative functions. Limits, $\limsup$ and $\liminf$ of $I/T$ are taken in $[0,\infty]$ , against $C(\gamma)$ embedded there; $C(\gamma)\ge0$ , so nothing is clamped.
Derivatives are Lean's deriv, the a.e. derivative on $\mathcal C_T$ .
The root of (5.9) is never chosen by a choice function: each statement about the candidate quantifies over every $A<e^{-\theta T}$ solving (5.9), with $B=1/(1-Ae^{\theta T})$ .
Lemma 5.6 uses the closed form of display (5.15). The printed lemma has $\bar\zeta(T)$ where (5.15) has $\bar\xi(T)$ , and a numerical check confirms (5.15).

A trivializing formalization is ruled out: the costs are lower integrals, so a non-integrable control cannot have cost zero; $I_T$ is $\infty$ off continuous paths; and the goal quantifies over every path through $I^*$ , $I$ and $\tilde I$ , not over the explicit candidate, for every $x_0\ge0$ and every $\gamma$ in the paper's ranges.

A complete development needs absolutely continuous functions and the fundamental theorem of calculus for them (present in Mathlib), the one-dimensional Skorohod problem, convexity of perspective functions, and a first-variation argument for convex integral functionals. The Skorohod-map and perspective-convexity lemmas are reusable beyond this mission. Contributions of proofs of any milestone, including partial results such as the $\lambda=\mu$ or $x_0>0$ cases of the goal, are welcome.

Selected references

R. Atar, A. Budhiraja, P. Dupuis, R. Wu, Large deviations for the single server queue and the reneging paradox, Mathematics of Operations Research, 2022; preprint arXiv:1903.06870v2 (2020). https://arxiv.org/abs/1903.06870
A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4
P. Dupuis, R. S. Ellis, A Weak Convergence Approach to the Theory of Large Deviations, Wiley, 1997. https://doi.org/10.1002/9781118165904

18 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Waiting for the Payday? The Market for Startups and the Timing of Entrepreneurial Exit: Low-Capability Startups Commit Early, High-Capability Startups Commit Late, Intermediate Ones Stay FlexibleResearch Paper

Motivation

Most technology startups that exit successfully are acquired by incumbents rather than taken public. A founder therefore faces a timing question: sell early, while the company is still an invention that only a few incumbents can evaluate, or wait until the invention has been developed into an innovation that every potential buyer can value, at the risk of failing before that point. Arora, Fosfuri and Rønde (SSRN 3611808, forthcoming in Management Science, 2020) model this choice as a contest between three exit strategies: commit to an early sale, commit to a late sale, or keep both options open. The paper's first main result, Proposition 1, describes which startups choose which strategy as a function of their execution capability and of the cost of seeking early offers.

The question matters to entrepreneurship and innovation economics because the answer is not monotone: the paper finds that keeping options open is chosen by startups of intermediate capability, while both weak and strong startups prefer to commit. Commitment to an early exit can be valuable even when flexibility costs nothing, because flexibility changes how early buyers bid.

Setting

A startup has execution capability $\theta\in[0,1]$ , its probability of surviving to the late market on its own. It holds resources $R>0$ . Trying the early market costs $c\in[0,R]$ ; the remaining $R-c$ is spent developing the invention, which realizes the fraction $\phi(R-c)$ of the late-market value, where $\phi$ is strictly increasing and continuous on $[0,R]$ with $\phi(0)=0$ and $\phi(R)=1$ .

There are $m$ buyers in the early market and $n$ in the late market, with $2\le m<n$ . Buyer $i$ values the startup at $w+v_i$ : a common component $w>1$ and an idiosyncratic component $v_i$ drawn independently from the uniform law on $[-1,1]$ , with distribution function $H(x)=(x+1)/2$ . Each market is a sealed-bid second-price auction. With $z$ bidders, let $X(1,z)$ and $X(2,z)$ be the expected highest and second-highest idiosyncratic draws, computed from the order-statistic distribution functions $F(x,z)=H(x)^z$ and $G(x,z)=zH(x)^{z-1}-(z-1)H(x)^z$ and their densities $f$ and $g$ . A buyer then expects $\pi_B(z)=\frac1z[X(1,z)-X(2,z)]$ and the seller $w+X(2,z)$ .

The three exit strategies pay:

commit early: $\Pi^E=w+X(2,m)$ ;
commit late: $\Pi^L=\theta\,[w+X(2,n)]$ ;
flexibility: with $t=\phi(R-c)\,\theta$ , early buyers bid only above the cutoff $\underline v^*(t)=\max\{t(\pi_B(n)+w+X(2,n))-w,\,-1\}$ , and

\Pi^F=\int_{\underline v^*(t)}^{1}(w+x)\,g(x,m)\,dx+G(\underline v^*(t),m)\,t\,(w+X(2,n)).

The startup's choice maximizes the three profits; on ties it prefers the less time-consuming strategy, so early before late before flexible. Let $\tilde\theta$ be the type at which $\Pi^E=\Pi^L$ ; it equals $\bigl(w+\frac{m-3}{m+1}\bigr)/\bigl(w+\frac{n-3}{n+1}\bigr)$ .

Formalization targets

Goal: Proposition 1

There exist costs $0<\underline c<\bar c<R$ such that

for $0\le c<\underline c$ there is $\theta_L\in\bigl(\frac{w-1}{\phi(R-c)(w+X(1,n))},\tilde\theta\bigr)$ such that no type commits late, and a type chooses flexibility if and only if $\theta>\theta_L$ ;
for $\underline c<c<\bar c$ there are $\theta_L<\theta_H$ with $\theta_H\in(\tilde\theta,1)$ such that $\theta\ge\theta_H$ commits late, $\theta_L<\theta<\theta_H$ is flexible, and $\theta\le\theta_L$ commits early;
for $\bar c\le c\le R$ , $\theta\le\tilde\theta$ commits early and $\theta>\tilde\theta$ commits late.

All thresholds except $\tilde\theta$ are existential, as on the page, so the goal does not depend on any computed constant.

Milestones

The milestones follow the paper's own proof, Online Appendix A2:

Lemma 1 (order-statistic distributions of uniform draws) and Lemma 3 ( $X(1,z)=\frac{z-1}{z+1}$ , $X(2,z)=\frac{z-3}{z+1}$ );
eq. (3), the closed form of $\tilde\theta$ ;
for $c=0$ : Lemma A2.1 (a single-crossing inequality with threshold $\theta_0$ ), the derivative formula (A2.2), Lemma A2.2 ( $\Pi^F$ flat, then decreasing, then increasing), Lemma A2.3 ( $\Pi^F>\Pi^L$ and a smaller slope), and Lemma A2.4 ( $\Pi^F>\Pi^E$ exactly above $\theta_{FE}$ );
for $c>0$ : Lemma 5 (the same shape after rescaling by $\phi(R-c)$ ), the strict decrease of $\Pi^F-\Pi^L$ in $\theta$ for every cost, and the existence, uniqueness and order of the cost thresholds $\underline c<\bar c$ .

Significance

Proposition 1 is the paper's characterization of exit timing. It explains why some founders publicly commit to an early sale, and it is the input to the paper's welfare analysis (§4), which compares the equilibrium timing with the efficient one in the two polar cases (iii) and (i). Without it, the comparative statics of Proposition 2 and the inefficiency results of Propositions 3 and 4 have no equilibrium to refer to.

The paper proves Proposition 1 on paper only. This mission produces a machine-checked version of the model and its proof. That includes the order-statistic facts for uniform valuations, which are standard (Krishna, Auction Theory, 2010, Appendix C) but which have no closed-form statement on the platform. The appendix's argument relies on "calculations show" steps and on convexity claims stated without proof; checking them in Lean is the main work beyond the paper. The platform holds no formalization of this model or of startup exit timing.

Difficulty

The obvious argument compares three explicit profit functions, but $\Pi^F$ is not explicit: its lower integration limit $\underline v^*$ moves with $\theta$ and has a kink where it leaves $-1$ . The shape of $\Pi^F$ (flat, then strictly decreasing, then strictly increasing) depends on the sign of an inequality between the ratio $G/g$ evaluated at the moving cutoff and a linear function of $\theta$ , and the paper settles this inequality at $\theta=1$ by an unstated calculation valid for every $m$ and $n$ . The comparison $\Pi^F>\Pi^L$ at $c=0$ holds uniformly in $\theta$ , and the slope comparison must hold across the kink. Finally, the cost thresholds are defined implicitly, and their order $\underline c<\bar c$ follows only by combining the single crossing in $\theta$ with the monotonicity of $\phi$ .

A tempting shortcut is to define the choice through the thresholds; that would make the goal true by definition and is ruled out (see below).

Formalization scope

All quantities are real numbers; $m,n$ are natural numbers with $2\le m<n$ , so the paper's $n\to\infty$ branches are not formalized. $\theta$ ranges over $[0,1]$ (the paper's $b=0$ ) and $c$ over $[0,R]$ . The standing assumptions are bundled in one predicate. Three choices differ from the printed page and are disclosed in each item:

$2\le m$ is added, since $X(2,m)$ needs at least two early bidders;
$\phi'>0$ is replaced by "strictly increasing and continuous on $[0,R]$ ", a weaker hypothesis and the only property the proofs use;
part (i) of Proposition 1 is posed for $c<\underline c$ rather than $c\le\underline c$ , because at $c=\underline c$ the type $\theta=1$ ties flexibility with late commitment and the tie rule sends it late.

The tie rule early ≻ late ≻ flexible is the page's "least time consuming" convention.

$F,f,G,g$ are Lemma 1's closed forms, linked to the actual order statistics of a product of uniform laws by the theorem lemma_1. $X(1,z)$ and $X(2,z)$ are integrals, so Lemma 3 is a theorem rather than a definition. $\Pi^F$ is eq. (2) with Lemma 4's cutoff; Lemma 4 itself, the early-market bidding equilibrium, is not formalized. The choice is defined from $\Pi^E,\Pi^L,\Pi^F$ only, never from $\theta_L$ , $\theta_H$ or $\tilde\theta$ , so the goal cannot hold by unfolding a definition. Proposition 2, Lemma 6, Propositions 3–4 and the Online Appendix extensions A4–A6 are outside this mission.

Contributions are welcome at every level. Particularly reusable are:

Lemma 1 for uniform order statistics;
the interval-integral computations behind Lemma 3;
the differentiation of $\Pi^F$ under a moving integration limit (eq. (A2.2)).

Selected references

A. Arora, A. Fosfuri, T. Rønde, Waiting for the payday? The market for startups and the timing of entrepreneurial exit, Management Science (forthcoming, 2020); authors' copy SSRN 3611808. https://ssrn.com/abstract=3611808
V. Krishna, Auction Theory, 2nd ed., Academic Press, 2010, Appendix C (order statistics).

14 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Inventory Integration with Rational Consumers: Unique Correlation and Variability Thresholds Below Which the Behavioral Value of Integration Is PositiveResearch Paper

Inventory pooling when consumers wait for markdowns

Inventory integration (or pooling) serves several markets from one stock instead of one stock per market. Its classical value is statistical: when demands are not perfectly correlated, the pooled demand is relatively less variable, so less safety stock is needed for the same service level. Eppen (Management Science, 1979) quantified this for normal demand, and it is the starting point of the risk-pooling literature.

Retailers who mark down unsold stock face a second effect. Strategic consumers who expect a clearance sale may delay their purchase, and whether they wait depends on how likely they believe a unit will still be available at the low price. Integration changes that availability and therefore changes consumer behavior. Aflaki and Swinney (SSRN 2842182, 2020; Operations Research 69(4), 2021) model this interaction as a rational-expectations game between a firm and its consumers, in the line of Su and Zhang (Management Science, 2008) and Cachon and Swinney (Management Science, 2009). They split the value of integration into an operational part and a behavioral part, and characterize when the behavioral part is positive.

Setting

A firm sells one product over two periods: at full price $p$ in period 1 and at clearance price $s$ in period 2. It orders $q$ units at cost $c$ before the season, with $s<c<p$ . Market demand $D$ is normal. In the multichannel system each of two identical markets has demand $N(\mu,\sigma^2)$ and its own stock. In the integrated system one stock serves $D_1+D_2\sim N\bigl(2\mu,2(1+\rho)\sigma^2\bigr)$ , where $\rho\in(-1,1)$ is the correlation.

Consumers have valuations $v$ with density $g$ on $(v_l,v_h)$ , distribution $G$ and $\bar G=1-G$ . A unit bought in period 2 is worth $\delta v$ , with $\delta\in(0,1]$ and $\delta p>s$ , and $v_l<p<v_h$ . Consumers believe a unit is available in period 2 with probability $\tilde\xi$ . They buy in period 1 exactly when $v\ge v^*(\tilde\xi)$ , where

v^*(\tilde\xi)=\min\Bigl(v_h,\max\Bigl(\frac{p-\tilde\xi s}{1-\tilde\xi\delta},\,p\Bigr)\Bigr).\tag{1}

Given the belief $\tilde v$ about this threshold, the firm faces period-1 demand $\bar G(\tilde v)D$ and solves a newsvendor problem. Its optimal profit is $\bar G(\tilde v)\,\Pi(m,\mathrm{sd})$ , with

\Pi(m,\mathrm{sd})=(p-c)m-(p-s)\,\mathrm{sd}\,L(\hat z)-(c-s)\hat z\,\mathrm{sd},

where $\Phi(\hat z)=(p-c)/(p-s)$ and $L(\hat z)=\int_{\hat z}^\infty(t-\hat z)\phi(t)\,dt$ .

The second-period fill rate $\xi_2(q,v)$ is expected period-2 sales divided by expected period-2 demand. Period-2 demand is $(G(v)-G(s/\delta))^+D$ , and period-2 sales are the smaller of that demand and the leftover stock $(q-\bar G(v)D)^+$ .

An equilibrium (Definition 1) is a triple $(q,v,\xi)$ in which $q$ maximizes profit given $v$ , $v=v^*(\xi)$ , and $\xi=\xi_2(q,v)$ . Write $v^*_m(\sigma)$ and $v^*_I(\rho,\sigma)$ for the equilibrium thresholds of the two systems. The behavioral value of integration is the second term of the paper's decomposition (6):

\mathrm{BV}(\rho,\sigma)=\frac{G(v^*_m)-G(v^*_I)}{\bar G(v^*_m)}\times\frac{\Pi\bigl(2\mu,\sqrt{2(1+\rho)}\,\sigma\bigr)}{2\,\Pi(\mu,\sigma)}.

Formalization targets

Goal: Proposition 5 (ii)–(iii), corrected

Let $\sigma_{\max}=\mu(p-c)/\bigl((p-s)\phi(\hat z)\bigr)$ , the value of $\sigma$ at which $\Pi(\mu,\sigma)$ changes sign.

\forall\sigma>0\text{ with }\Pi(\mu,\sigma)>0:\ \exists!\,\bar\rho\in[-1,1],\ \forall\rho\in(-1,1),\ \ \mathrm{BV}(\rho,\sigma)>0\iff\rho<\bar\rho,

\forall\rho\in(-1,1):\ \exists!\,\bar\sigma\in[0,\sigma_{\max}],\ \forall\sigma\in(0,\sigma_{\max}),\ \ \mathrm{BV}(\rho,\sigma)>0\iff\sigma<\bar\sigma.

The goal asserts only the shape of the answer: the set where the behavioral value is positive is an initial segment, in correlation and in variability. It fixes no formula for the thresholds.

Milestones

Propositions 1–3 cover consumer thresholds, the newsvendor best response, and existence and uniqueness of the equilibrium with $v^*<v_h$ . Equations (8) and (14) give the fixed-point form of the equilibrium fill rate. Three further milestones are the reduction to the coefficient of variation, the deterministic endpoint ( $\xi_2=0$ , $v^*=p$ ), and Lemma 1, continuity of a unique fixed point. The last ones are Proposition 5 (i), quasiconcavity of $\xi_{I2}$ and $v^*_I$ in $\rho$ and in $\sigma$ , and the sign rule that $\mathrm{BV}>0$ when $v^*_m>v^*_I$ and $\mathrm{BV}<0$ when $v^*_m<v^*_I$ .

Significance

The result says when pooling helps through consumer behavior: when markets are not too positively correlated and not too variable. Above either threshold, integration encourages strategic waiting enough to reduce the total value of pooling below its classical operational value. A firm that ignored this effect would overrate integration in highly correlated or highly variable markets.

The formalization adds two things. It makes the equilibrium of a rational-expectations inventory game a checked object. It also records gaps in the printed statements. First, part (iii) and the sign rule on p. 13 need $\Pi(\mu,\sigma)>0$ : for $\sigma>\sigma_{\max}$ the sign of $\Pi(\mu,\sigma)$ flips the sign of $\mathrm{BV}$ . Second, footnote 4 needs $v_l<p$ . Third, under the paper's ratio fill rate with normal demand, the equilibrium fill rate can be negative, which affects (8) and (14). The result is proved on paper. To the best of current knowledge, nothing in it has been formalized.

Difficulty

The equilibrium is an implicit fixed point. The fill rate is the solution of (14), in which the demand ratio $B$ depends on the fill rate itself, through the threshold valuation. Comparing $v^*_m$ with $v^*_I$ means comparing the fixed points of two different equations, one per system.

A direct approach would show that $\mathrm{BV}$ is monotone in $\rho$ or $\sigma$ . That fails, because the equilibrium fill rate rises and then falls in variability. Only quasiconcavity holds, and the threshold structure must come from combining quasiconcavity with the behavior at the endpoints, where demand is deterministic. Quasiconcavity of an implicitly defined fixed point needs a second-order argument on (14), which involves Gaussian integrals with variable limits.

Formalization scope

Everything is real-valued. The multichannel system is formalized as one market $N(\mu,\sigma^2)$ , taken once, since the two markets are identical and the equilibrium is symmetric (Proposition 3). The integrated system is the market given by the law $N(2\mu,2(1+\rho)\sigma^2)$ , as in Proposition 2 (ii), not as a bivariate sum. The demand law with standard deviation $0$ is the Dirac mass, which is how the deterministic endpoint is stated.

The valuation density is integrable, has total mass one, vanishes off $(v_l,v_h)$ and assigns positive probability to every nonempty interior subinterval. Three conventions and additions are disclosed:

the standing hypothesis $v_l<p$ is added, and $\delta>0$ is made explicit;
$\Pi(\mu,\sigma)>0$ is added in the goal and in the sign rule (the correction);
the fill rate keeps the sign of the normal demand, exactly as in the paper's (14), so it can be negative. Eq. (8) is accordingly stated with the guard $\xi\ge0$ , and (14) evaluates $B$ at the equilibrium valuation.

The goal is stated about equilibria of Definition 1 and about the behavioral value. It is not stated about (14), an abstract function of the coefficient of variation, or the sign of $v^*_m-v^*_I$ . The thresholds range over $[-1,1]$ and $[0,\sigma_{\max}]$ , so the uniqueness claim cannot be met by an unconstrained threshold.

A complete development needs Gaussian integrals of piecewise-linear functions, the newsvendor solution for normal demand, fixed-point arguments for monotone maps, and implicit differentiation of parametric integrals. The normal newsvendor and the loss-function identity are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Proposition 5 (i) that avoid differentiability assumptions on $g$ .

Selected references

A. Aflaki and R. Swinney, Inventory Integration with Rational Consumers, SSRN preprint 2842182 (July 2020); Operations Research 69(4), 2021. https://ssrn.com/abstract=2842182
G. D. Eppen, Effects of Centralization on Expected Costs in a Multi-Location Newsboy Problem, Management Science 25(5), 498–501, 1979. https://doi.org/10.1287/mnsc.25.5.498
X. Su and F. Zhang, Strategic Consumer Behavior, Commitment, and Supply Chain Performance, Management Science 54(10), 1759–1773, 2008.
G. P. Cachon and R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, Management Science 55(3), 497–511, 2009. https://doi.org/10.1287/mnsc.1080.0948

13 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Time-Varying Semidefinite Programs: Under Strict Feasibility, Feasible Polynomial Solutions Have Objective Values Converging to the TV-SDP Optimal ValueResearch Paper

Motivation

Many planning problems ask for a decision that varies over a time horizon and must satisfy a constraint at every instant, possibly with cumulative effects of past decisions. The applications in the source paper are a maximum-flow problem with time-varying pipeline capacities, a wireless coverage problem for a moving target region, and the approximation of Pareto curves of bi-objective semidefinite programs. Ahmadi and El Khadir (arXiv:1808.03994, Mathematics of Operations Research, 2021) model these as time-varying semidefinite programs (TV-SDPs), a common generalization of semidefinite programming and of the continuous linear programs of Bellman (1953), Tyndall (1965) and Levinson (1966), which are the case of diagonal matrices.

A TV-SDP is an infinite-dimensional problem: its variable is a function. The paper's main message is that, under a strict feasibility assumption, nothing is lost by searching only over polynomial solutions, and that the best polynomial solution of a fixed degree can be computed by an ordinary SDP through sum-of-squares certificates. The first statement, Theorem 4, is what justifies the second as a convergent approximation scheme, and it is the goal of this mission.

Setting

Fix integers $n, m \ge 0$ . Let $\mathbf L^n$ be the set of measurable functions $x:[0,1]\to\mathbb R^n$ that are bounded, $\sup_{t\in[0,1]}\|x(t)\|_\infty<\infty$ . The data are polynomial: an objective $c=(c_1,\dots,c_n)$ of univariate polynomials, symmetric $m\times m$ matrices $A_0(t),\dots,A_n(t)$ with polynomial entries, and symmetric $m\times m$ kernels $D_1(t,s),\dots,D_n(t,s)$ with entries polynomial in $(t,s)$ . For $x\in\mathbf L^n$ define the matrix function

\mathcal Fx(t)=A_0(t)+\sum_{i=1}^n x_i(t)A_i(t)+\sum_{i=1}^n\int_0^t x_i(s)\,D_i(t,s)\,ds .

A function $x$ is feasible if $x\in\mathbf L^n$ and $\mathcal Fx(t)\succeq0$ for almost every $t\in[0,1]$ . The TV-SDP is

\mathrm{opt}=\sup\Bigl\{\langle c,x\rangle_{\mathbf L^n}=\int_0^1\langle c(t),x(t)\rangle\,dt \;:\; x \text{ feasible}\Bigr\}\in[-\infty,+\infty].

It is strictly feasible if some $x^s\in\mathbf L^n$ and $\varepsilon>0$ satisfy $\mathcal Fx^s(t)\succeq\varepsilon I$ for almost every $t\in[0,1]$ . A polynomial solution is $x(t)=(p_1(t),\dots,p_n(t))$ for polynomials $p_i$ .

The proof uses the mollifying operators $\mathcal M_v$ , $v\in\mathbb N$ : with the bump $J(t)=c\,e^{-1/(1-t^2)}$ for $|t|<1$ , $J(t)=0$ otherwise, normalized so that $\int_{\mathbb R}J=1$ ,

\mathcal M_vf(t)=\int_0^1 v\,J(v(t-s))\,f(s)\,ds ,

applied entrywise to vector- and matrix-valued functions. In Lean these are Ln, Sm, Data, F, Feasible, StrictlyFeasible, obj, opt, polySol, J, cJ, Mv, MvVec and MvMat in the namespace TVSDP.PolyOpt.

Formalization targets

Goal: Theorem 4 (p. 11)

If the TV-SDP is strictly feasible, there are polynomial vectors $p^k$ such that every $x^k=p^k$ is feasible and

\langle c,x^k\rangle_{\mathbf L^n}\longrightarrow\mathrm{opt}\qquad(k\to\infty),

the limit taken in the extended reals, so $\mathrm{opt}=+\infty$ is included.

Milestones

Proof of Theorem 4, p. 13. For feasible $x$ and strictly feasible $x^s$ with margin $\varepsilon$ , the combination $(1-\lambda)x+\lambda x^s$ satisfies $\mathcal F(\cdot)\succeq\lambda\varepsilon I$ a.e., and its objective tends to $\langle c,x\rangle$ as $\lambda\to0^+$ .
Proposition 1, p. 11 (first two sentences). $\mathcal M_vf$ is continuous and $\int_0^1|\mathcal M_vf-f|\to0$ for bounded measurable $f$ .
Lemma 3(a), p. 12. $M(t)\succeq0$ a.e. implies $\mathcal M_vM(t)\succeq0$ for all $t\in[0,1]$ .
Lemma 3(b), p. 12, and the explicit rate of its proof: $\sup_{t\in[0,1]}|a(t)\mathcal M_vx(t)-\mathcal M_v(a\cdot x)(t)|\le L\gamma/v\to0$ for polynomial $a$ .
Proof of Theorem 4, p. 13 (minimum-eigenvalue step). If $G(t)\succeq\beta I$ on $[0,1]$ and $\sup_t\|G(t)-H_v(t)\|\to0$ , then $H_v(t)\succeq\frac\beta2 I$ on $[0,1]$ for large $v$ .
Proof of Theorem 4, pp. 13–14. $\sup_t\|\mathcal Fx(t)-\mathcal Fy(t)\|\le C\sup_t\|x(t)-y(t)\|_\infty$ with $C=\sup_{t,s\in[0,1]}\sum_i(\|A_i(t)\|+\|D_i(t,s)\|)$ .

Significance

The result. Theorem 4 says that the supremum of a strictly feasible TV-SDP over polynomial solutions equals its supremum over all bounded measurable solutions. Combined with the paper's Theorem 6, which computes the best degree- $d$ polynomial solution by an SDP, it shows that these SDP values form a nondecreasing sequence of lower bounds converging to $\mathrm{opt}$ . Without it, the polynomial restriction could have a strictly smaller value; Example 1 of the paper shows that this happens when strict feasibility fails, where the unique feasible solution is a step function.

Formalizing it. The result is proved in the paper, not formalized anywhere. A machine-checked proof also has to repair the printed argument: the operator $\mathcal M_v$ integrates over $[0,1]$ only and is not normalized near the endpoints ( $\mathcal M_v1(0)=\tfrac12$ for $v\ge1$ ), so three auxiliary statements of §3.1 are false as printed (see Formalization scope), although Theorem 4 itself is true. Any complete proof therefore needs an argument that handles the endpoints, which the formal development would record.

Difficulty

The natural route is "perturb into the strict interior, smooth, approximate by polynomials", and each step preserves feasibility only up to a uniform error, so the margin $\varepsilon$ must survive all three. The difficulty is uniformity on the closed interval: smoothing commutes with $\mathcal F$ only approximately, the Volterra term $\int_0^t x_i(s)D_i(t,s)\,ds$ couples times, and at $t=0$ and $t=1$ the mollifier of Definition 3 loses half its mass. Applying the printed Corollary 1 directly fails at the endpoints. In Lean, a further cost is the bookkeeping between "almost every $t\in[0,1]$ " for feasibility and "every $t\in[0,1]$ " for the smoothed and polynomial solutions.

Formalization scope

Conventions committed to:

Functions are total maps on $\mathbb R$ ; only their values on $[0,1]$ matter. "Almost every $t\in[0,1]$ " is with respect to Lebesgue measure restricted to $[0,1]$ (volume.restrict (Set.Icc 0 1)), never Lebesgue measure on $\mathbb R$ .
$\mathbf L^n$ is bounded and measurable, with the sup norm on $\mathbb R^n$ ; the bold $\mathbf L^1$ of the paper is $\mathbf L^n$ with $n=1$ , not Lebesgue $L^1$ .
The data are polynomial (the paper's standing assumption, p. 3), with symmetric polynomial matrices. Theorem 4 is false for general bounded measurable data.
$\mathcal F$ is defined entrywise; the kernel term is an interval integral, with variable $0$ of $D_i$ the outer time $t$ and variable $1$ the integration variable $s$ .
$\mathrm{opt}$ is an EReal supremum; the matrix inequality $X\succeq\beta I$ is positive semidefiniteness of $X-\beta I$ .
$J(\pm1)=0$ (the page's formula is undefined there); $\mathcal M_v$ is defined for $v\in\mathbb N$ exactly as in Definition 3, without normalization.
Matrix norms are the entrywise maximum; the page allows any matrix norm.

Trivializations ruled out: feasibility is a.e. on $[0,1]$ only, solutions in $\mathbf L^n$ are bounded, $\mathrm{opt}$ is not a real sSup (which would be $0$ on an unbounded set), and polynomial solutions are genuine polynomials evaluated everywhere, not functions that agree with a polynomial almost everywhere.

Deliberately absent: the third sentence of Proposition 1 (uniform convergence $\mathcal M_vf\to f$ for continuous $f$ ), Lemma 3(c) and Corollary 1. All three are false for the operator of Definition 3 because of the endpoint effect; for example, Corollary 1 fails for $x=0$ , $A_0=I$ at $t=0$ . The printed constant $C$ on p. 14 has $D_i(s,t)$ in place of $D_i(t,s)$ , and with it the Lipschitz display fails; milestone 6 uses the corrected constant. Measurability of $M$ is added in Lemma 3(a), where the paper uses it implicitly.

Infrastructure needed: interval mollification of bounded measurable functions, uniform convergence on $[0,1]$ , the Weierstrass approximation theorem for $\mathbb R^n$ -valued functions (in Mathlib), and Loewner-order perturbation bounds. The mollifier and the Loewner perturbation lemma are reusable beyond this mission. Contributions of proofs for any milestone, of the missing endpoint-robust smoothing step, and of the paper's Example 1 are welcome.

Selected references

A. A. Ahmadi and B. El Khadir, Time-varying semidefinite programs, Mathematics of Operations Research, 2021; arXiv:1808.03994v2. https://arxiv.org/abs/1808.03994
R. Bellman, Bottleneck problems and dynamic programming, Proceedings of the National Academy of Sciences 39(9), 1953. https://doi.org/10.1073/pnas.39.9.947
W. F. Tyndall, A duality theorem for a class of continuous linear programming problems, Journal of the SIAM 13(3), 1965. https://doi.org/10.1137/0113044
N. Levinson, A class of continuous linear programming problems, Journal of Mathematical Analysis and Applications 16(1), 1966. https://doi.org/10.1016/0022-247X(66)90184-3
R. A. Adams and J. J. F. Fournier, Sobolev Spaces, 2nd ed., Academic Press, 2003 (Theorem 2.29, cited for Proposition 1).

10 thms3 active usersReviewed

Completed

Combinatorics Linear Optimization Operations Research+1·Captain: mikedeng1

Robust Optimization Approach to Process Flexibility Designs with Contribution Margin Differentials: The Alternate Long Chain Is Worst-Case Optimal Among Balanced Two-Margin Long ChainsResearch Paper

Why process flexibility matters

A factory can respond to uncertain demand by allowing a plant to make more than one product. Those extra capabilities cost money, so the design question is where to place a limited number of plant–product links. The usual measure of a flexible production system is the number of units sold. When products have different contribution margins, however, two designs with the same sales may earn different profits: capacity used for a low-margin product cannot then serve a high-margin one. Wang, Wang and Zhang study this distinction through worst-case demand and show that a particular arrangement of two product classes is optimal within the family of long chains (Wang, Wang and Zhang 2020, §§1 and 4).

The result addresses a concrete design choice. A long chain gives every plant two product capabilities and connects the system in a cycle. If half the products have high margins and half low margins, should the two classes be grouped on that cycle or spread out? The paper's answer is that alternating high- and low-margin products gives at least as good a worst-case score as every other long-chain arrangement, for a broad class of scores.

Production and uncertain demand

A flexibility design $A$ is a set of arcs $(j,i)$ from plant $j$ to product $i$ . Plant $j$ has capacity $C_j$ , product $i$ has demand $d_i$ and margin $p_i$ , and $x_{ij}$ units of product $i$ are made by plant $j$ . The maximum profit $g(A,d)$ is the optimum of the finite linear program

g(A,d)=\max_{x\ge0}\sum_{(j,i)\in A}p_i x_{ij},\qquad \sum_jx_{ij}\le d_i,\quad \sum_i x_{ij}\le C_j.

Products fall into $T$ categories with margins $P_1<\cdots<P_T$ . Write $S_t$ for the products with margin $P_t$ and $D_t(d)=\sum_{i\in S_t}d_i$ for their total demand. A deterministic score in the paper's class has the form $f(A,d)=h(g(A,d),(D_t(d))_t)$ , with $h$ strictly increasing in its profit argument when category totals are fixed. Its robust score is $R^f(A,U)=\min_{d\in U}f(A,d)$ for an uncertainty set $U$ of nonnegative demand vectors. This includes maximum profit and scores that subtract a demand-based benchmark from profit (Wang, Wang and Zhang 2020, §2.2).

A set is part-wise independently symmetric when it is a Cartesian product of its category projections and remains unchanged if products are permuted within any category. The perturbation version applies that property to $E=\{d-\mu:d\in U\}$ for a fixed centre $\mu$ . Such sets preserve the high/low distinction while treating products within each class interchangeably (Wang, Wang and Zhang 2020, Definitions 2.1–2.2).

Formalization targets

Alternate-chain optimality

In the target system there are $2k$ plants and $2k$ products, $k\ge1$ , with unit plant capacities and exactly $k$ products in each of two margin classes $0<P_L<P_H$ . A long chain places the fixed products in any cyclic order and connects each plant to two consecutive products. An alternate long chain places high- and low-margin products alternately. The goal, Theorem 3, says that for every such pair of chains, every part-wise independently symmetric $U$ , and every robust score in the class above,

R^f(\mathrm{AL},U)\ge R^f(L_{HL},U).

This is the paper's worst-case comparison, rather than a claim about a single demand instance or a single performance measure (Wang, Wang and Zhang 2020, Theorem 3, p. 21).

Margin-group comparisons

The paper defines a dual margin group index $\delta^K_\mu(A)$ by an integer program that assigns product dual values from the finite menu $\beta_{tr}=P_t-P_r$ , where $P_0=0$ . The parameter $K$ counts how many products in each category receive each nonzero menu value. Its feasible set is $Q$ . Theorem 1 expresses every robust score in terms of these indices and residual demand vectors; Theorem 2(a) says that index dominance for every $K\in Q$ implies robust-score dominance. Lemma 2 evaluates the index of an alternate chain in three cases, and Proposition 1 compares it with every long chain (Wang, Wang and Zhang 2020, pp. 17–22). These are the mission's milestones, alongside the profit LP's duality and two cyclic-window statements used in the comparison.

What the result provides

Within balanced, unit-capacity, two-margin long chains, the theorem resolves placement of the high-margin products without choosing one demand distribution or one profit-based robustness score. The dominance holds across the paper's whole class of category-symmetric uncertainty sets and scores. It gives a design rule within that family; it does not claim that an alternate chain beats every possible two-capability graph. The paper separately studies limits of that broader comparison (Wang, Wang and Zhang 2020, §4.3).

The paper proves these results on paper. This mission asks for machine-checked proofs of the stated Lean targets. Its reusable output includes the finite bipartite profit LP, its dual, category-wise demand symmetry, and the DMGI representation. None of the mission's theorems is presented here as already machine-checked.

Where the formal proof is difficult

The LP optimum must be related to a dual optimum whose product variables belong to a small, margin-dependent set. That is stronger than merely invoking an objective-value duality statement. The robust representation then has to account for both a discrete assignment of dual values and the permissible permutations of demand residuals within each product class. The last comparison is combinatorial: a general long chain can have runs of high-margin products, and its relevant cyclic windows must be compared with the alternating chain across every feasible count vector $K$ (Wang, Wang and Zhang 2020, Appendix A).

Formalization scope

The Lean development represents plants and products by finite index types, real capacities, demands and margins, and a design by a finite set of plant–product pairs. A separate general profit-LP definition is instantiated by the paper's margin-category system. Lean indices start at zero: category $t$ is the paper's category $t+1$ , and the added margin level $P_0$ is zero. The production variable is written x j i in Lean for the paper's $x_{ij}$ . Category residuals are enumerated by increasing product index; part-wise symmetry makes that choice immaterial. A long chain uses a permutation of fixed products around a cycle, so the uncertainty set stays attached to the same high- and low-margin categories.

The system requires positive numbers of plants, products and occupied margin categories, nonnegative capacities, and positive strictly increasing margins. The paper treats margins as positive profits but does not state that inequality explicitly. The model also supplies $z_j\ge0$ to the DMGI program, matching the dual program and the use of dual feasibility in the paper's proof; equations (4) and (5) omit this line. For the robust minimum, $U$ is nonempty, compact and contained in nonnegative demand, and the deterministic score is continuous there. Nonemptiness and compactness are explicit mathematical additions needed for the paper's minimum and minimizer. Every DMGI theorem restricts $K$ to $Q$ . These conditions prevent empty or unbounded real infima from supplying Lean's default zero. The $k=1$ case is included.

Contributions may establish the LP duality, dual extreme-point structure, robust representations, exact alternate-chain index, or cyclic-window comparison. The definitions use finite sums and real suprema and infima; establishing attainment is part of the theorem work.

Selected references

S. Wang, X. Wang and J. Zhang, Robust Optimization Approach to Process Flexibility Designs with Contribution Margin Differentials, Manufacturing & Service Operations Management, 2020. SSRN author version 3233721, 22 May 2020; DOI.

12 thms3 active usersReviewed

Completed

Economics Operations Research Stochastic Systems·Captain: mikedeng1

A Model of Queue-Scalping: A Single Queue-Scalper Enters the Queue if and only if the Demand Volume Is IntermediateResearch Paper

Why queue position has a price

A customer who is short of time may pay for a better place in a service queue. Unlike resale of a fixed ticket, this transaction changes the waits faced by later customers, and those customers' choices then change the value of the position being sold. Yang, Wang, and Cui study this feedback in an unobservable queue with a firm that repeatedly sells its place to arriving customers. Their single-scalper analysis identifies demand levels at which such a firm enters, rather than assuming that more customer traffic always makes entry more attractive (Yang, Wang, and Cui 2021, §§3–4).

The mission targets a precise claim about that entry decision. Low demand leaves few sales; very high demand forces more customers to balk and limits what a buyer will pay. The result is a possibly empty interval of demand volumes in which the scalper enters. The associated price and revenue results are useful milestones because they describe the economics of that interval using the same customer equilibrium as the entry theorem (Yang, Wang, and Cui 2021, Propositions 2–4).

Service system and customer equilibrium

The service system is an M/M/1 queue: potential customers arrive as a Poisson process at rate $\Lambda$ , and a single server completes service at exponential rate $\mu>0$ . Customers cannot observe the queue length or their positions. Every customer values completed service at $V$ and has a private delay cost $c$ per unit time. In this mission, $c$ is uniform on $[0,1]$ and $V>1/\mu$ . A queue-scalping firm may place one scalper in line. Under the head-queueing rule, the scalper can hold the first position without blocking service while waiting to sell it to a customer. After a sale, the scalper returns to the tail. The firm pays cost $k$ per unit time for the scalper and charges a nonnegative price $P$ per sale (Yang, Wang, and Cui 2021, pp. 5–9, Lemma 1).

Customers use two cutoffs. Customers below $\tilde c$ join without buying, customers from $\tilde c$ through $c^S$ join and buy, and customers above $c^S$ balk. The actual throughput is $\lambda=\Lambda c^S$ ; the share of joining customers who buy is $q=(c^S-\tilde c)/c^S$ . A customer with delay cost $\tilde c$ is indifferent between buying and not buying. A customer at $c^S$ can join and buy, while the corresponding utility is zero if any customers balk. These are the customer-equilibrium equations (1b)–(1d) of the paper, with $0< c^S\le1$ , $0\le\tilde c\le c^S$ , and stable throughput $\lambda<\mu$ (Yang, Wang, and Cui 2021, pp. 7–9).

Let $W^I_1(\lambda,q)$ be a buyer's expected delay and $W^I_2(\lambda,q)$ a nonbuyer's expected delay under the head-queueing rule. Their difference $D^I(q)=W^I_2-W^I_1$ is the buyer's delay saving. Optimal revenue $\Pi(\Lambda)$ is the attained maximum of $P\lambda q$ over nonnegative prices and compatible customer equilibria. If the firm stays out, its profit is zero. If it enters, its best profit is $\Pi(\Lambda)-k$ . At equality the model takes the no-entry decision, as in the proof's entry criterion $\Pi>k$ (Yang, Wang, and Cui 2021, equation (1a), Proposition 4 and its Online Appendix proof).

Formalization targets

Entry at intermediate demand

For fixed $\mu$ , $V$ , and $k>0$ , Proposition 4 asserts that thresholds $\underline\Lambda\le\overline\Lambda$ exist such that every positive demand volume has an optimal customer-equilibrium revenue and

N^*(\Lambda)=\begin{cases} 1,&\underline\Lambda<\Lambda<\overline\Lambda,\\ 0,&\text{otherwise}. \end{cases}

The interval can be empty. The thresholds depend on the system parameters, rather than on the demand volume being tested (Yang, Wang, and Cui 2021, Proposition 4, p. 12).

Price and revenue structure

Proposition 2 gives the optimal price in the all-join regime $\Lambda\le\mu-1/V$ and the balking regime $\Lambda>\mu-1/V$ , and says that this price is unimodal. Proposition 3 says that optimal revenue is also unimodal, with a unique peak $\Lambda^*\ge\mu-1/V$ . The Online Appendix identifies the cutoff $c^S$ , reduces the pricing problem to the buying cutoff $\tilde c$ , gives the revenue expression in each regime, and shows that revenue less cost approaches $-k$ at both extreme demand levels (Yang, Wang, and Cui 2021, Propositions 2–3, Online Appendix pp. 1–3).

What the result provides

The entry theorem classifies queue demand by the scalper's decision while allowing the equilibrium buying and balking rates to change with price. It explains why a queue with more arrivals can become less attractive to a scalper even though it offers more potential buyers. The price and revenue milestones also distinguish two operational regimes: one in which everyone joins, and one in which joining itself contracts as demand rises (Yang, Wang, and Cui 2021, §§4.1 and 9).

The paper proves these results mathematically; this mission asks for machine-checked proofs of the statements under an explicit model interface. The reusable output includes formulas for the two customer delay classes, a predicate for cutoff-based customer equilibrium, and an attained joint optimization predicate. A formal proof of entry must connect the closed-form revenue analysis to that optimization predicate. At the draft stage, the proposed theorem statements compile with sorry; they are not yet machine-checked proofs.

Where the difficulty lies

More arrivals directly create more opportunities to sell a place, but customer behavior also changes the number who join, the fraction who buy, and the price they will pay. Holding any one of these responses fixed gives the wrong entry question. The challenging point is to establish a single rise and fall of optimal revenue across the boundary between the all-join and balking regimes, while keeping the customer equilibrium and the price optimization tied together. The endpoint behavior matters as well: an interval theorem needs no entry at sufficiently low and sufficiently high demand, including the possibility that the entry interval is empty (Yang, Wang, and Cui 2021, Propositions 2–4 and Online Appendix A).

Formalization scope

Lean represents $\mu,V,k,\Lambda,\lambda,P,q,c^S,\tilde c$ as real numbers and the entry decision $N^*$ as either zero or one. Params.Standing records $\mu>0$ , $V>1/\mu$ , and $k\ge0$ . Proposition 4 additionally assumes $k>0$ ; the Online Appendix uses the negative limit $-k<0$ , and at zero cost the high-demand nonentry threshold need not be finite. Statements concerning demand use $\Lambda>0$ . The positive cutoff $c^S$ makes the purchase-rate quotient meaningful, and stable throughput keeps the queue-delay denominators positive.

The delay formulas of Lemma 1 are taken as the model's delays; their underlying stationary queueing-process derivation is outside this mission. The uniform CDF is the identity on $[0,1]$ . The paper's optimization is represented by an attained maximum over prices and customer equilibria, rather than by a supremum of arbitrary real values. The entry goal includes existence of an optimizer at every positive demand, so missing feasible equilibria cannot make the result vacuous. Contributions that establish equilibrium cutoff uniqueness, exact reduction of the pricing problem, price and revenue optimality, and the resulting demand shape are all within scope. The definitions of the equilibrium and optimum can be reused in further analysis of queue position sales under the same rule.

Selected references

Luyi Yang, Zhongbin Wang, and Shiliang Cui, A Model of Queue-Scalping, Management Science, 2021, authors' manuscript and Online Appendix. DOI: 10.1287/mnsc.2020.3865.

10 thms3 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Assessing Algorithmic Fairness with Unobserved Protected Class Using Data Combination: The Partial Identification Set of Demographic Disparity Is the Closed Interval with Fréchet–Hoeffding EndpointsResearch Paper

Why the disparity is uncertain

An auditor may need to measure whether a decision rule approves members of one protected group more often than members of another. The decision, the relevant outcome, and useful proxy variables may be observed in a primary dataset, while protected class and the same proxies are observed in a separate auxiliary dataset. There is no record linking the two datasets person by person. Consequently, the two observed distributions do not determine a unique joint distribution, even if they are known without sampling error. Kallus, Mao, and Zhou study what can still be said about such fairness measures from the two marginals alone (arXiv:1906.00285v2, §§2, 4–5).

The issue is relevant whenever protected labels cannot be joined to individual decisions. Proxy methods can estimate group membership, but their errors do not disappear merely because the marginal distributions are known. A set of compatible disparity values makes the uncertainty visible. This mission treats the population result in Proposition 7 of the cited preprint; estimation from finite samples and the paper's empirical case studies are separate topics.

Observed information and compatible joints

Let decision $\hat Y\in\{0,1\}$ and true outcome $Y\in\{0,1\}$ . The protected class $A\in\{a,b\}$ has two groups, with $a$ conventionally advantaged and $b$ disadvantaged. The proxy $Z$ takes values in a measurable space $\mathcal Z$ ; it may be categorical, continuous, or mixed. The primary marginal is $P(\hat Y,Y,Z)$ , and the auxiliary marginal is $P(A,Z)$ . Both share one proxy distribution $P(Z)$ , as required when they arise from a common population joint law.

For each proxy value $z$ , write $\eta_{\mathrm{aux}}(\alpha,z)=P(A=\alpha\mid Z=z)$ and $\eta_{\mathrm{priT}}(\hat y,y,z)=P(\hat Y=\hat y,Y=y\mid Z=z)$ . Their decision marginal is $\eta_{\mathrm{pri}}(\hat y,z)=\sum_y\eta_{\mathrm{priT}}(\hat y,y,z)$ . A coupling of two discrete probability vectors is a nonnegative array whose row and column sums equal those vectors. The paper's set $\mathcal P_D$ contains all measurable conditional joint arrays $\pi(\alpha,\hat y,y\mid z)$ that couple $\eta_{\mathrm{priT}}(\cdot,\cdot,z)$ and $\eta_{\mathrm{aux}}(\cdot,z)$ at each $z$ , together with the fixed $P(Z)$ . It imposes no additional assumptions on the unknown association of class and outcomes.

The demographic disparity of a compatible joint $P'$ is $\delta_{DD}(a,b;P')=P'(\hat Y=1\mid A=a)-P'(\hat Y=1\mid A=b)$ . Its partial identification set is

\Delta_{DD}(\mathcal P_D)=\{\delta_{DD}(a,b;P'):P'\in\mathcal P_D\}.

This set lists every disparity that the two observed marginals permit, rather than selecting a particular way to combine them.

Formalization targets

For a group $\alpha$ , decision $\hat y$ , and proxy value $z$ , define the Fréchet–Hoeffding weight endpoints

w^L_\alpha(\hat y,z)=\max\left\{0,1+\frac{P(A=\alpha\mid Z=z)-1}{P(\hat Y=\hat y\mid Z=z)}\right\},\qquad w^U_\alpha(\hat y,z)=\min\left\{1,\frac{P(A=\alpha\mid Z=z)}{P(\hat Y=\hat y\mid Z=z)}\right\}.

For a class weight function $w$ , let $\mu(\alpha;w)=E[w_\alpha(\hat Y,Z)\hat Y]/P(A=\alpha)$ . The goal, Proposition 7, is the equality

\Delta_{DD}(\mathcal P_D)= \left[\mu(a;w^L)-\mu(b;w^U),\;\mu(a;w^U)-\mu(b;w^L)\right].

Equality makes the interval sharp: every compatible joint produces a value inside it, and every value inside it is produced by a compatible joint. The milestones state the finite coupling bounds, the weighted description of the disparity set, the constraints on admissible weights, the numerical bounds, and attainment of both endpoint values. The source is Proposition 1, Propositions 5–7, and the proof of Proposition 7 on pp. 10 and 14–15 of the preprint (arXiv:1906.00285v2).

What the result gives

The theorem gives an exact range for the difference in group approval rates when class and decision are never observed jointly. An interval that excludes zero has an interpretation that does not depend on choosing one compatible joint law. A wide interval identifies uncertainty due to data combination itself, before finite-sample error enters. A single point signals that the observed marginals identify the demographic disparity under these conventions.

Formalizing the known result adds a reusable definition of finite couplings and a precise model of compatible conditional joints over an arbitrary measurable proxy space. The proposition is proved in the paper; the Lean goal and its milestone statements are open formalization targets. The development also records the null-cell and denominator conventions that ordinary probability notation leaves implicit. It does not claim a machine-checked proof of Proposition 7 yet.

Central difficulty

The observed data fix the class marginal and the joint decision–outcome marginal, but they do not fix their association within a proxy cell. Bounding one cell of a coupling does not by itself prove that an extreme disparity is simultaneously attainable under all marginal constraints. The true outcome $Y$ remains in the compatible-joint model even though demographic disparity uses only $\hat Y$ . When a decision cell has zero probability, a conditional class weight on that cell is undefined, so pointwise weight statements require care. A set inclusion alone would miss the sharpness claim.

Formalization scope

The Lean model uses Fin 2 for each binary outcome and a two-constructor type for protected class. It represents the two observed marginals by one probability measure on $Z$ and measurable, normalized, nonnegative conditional vectors $\eta_{\mathrm{aux}}$ and $\eta_{\mathrm{priT}}$ . The set $\mathcal P_D$ consists of measurable conditional couplings for every $z$ . Conditional probabilities in the candidate joint are ratios of integrals of that joint array. In particular, the denominator of $\delta_{DD}(a,b;P')$ is computed from $P'$ , not inserted from the auxiliary marginal.

The theorem explicitly assumes $P(A=a)>0$ and $P(A=b)>0$ , since conditioning on a group of zero probability is undefined in the paper. The paper's conditional laws are defined almost everywhere; requiring a coupling at every $z$ selects a version and does not change the attainable disparities. On a cell with $P(\hat Y=\hat y\mid Z=z)=0$ , weight identities and bounds are imposed only when that cell has positive probability; all weighted expectations multiply by the cell probability. The integrands arising from compatible joints and admissible weights are measurable and bounded on a probability space, so their real integrals are genuine expectations.

The identification set is built from compatible joint laws and their conditional disparity. Defining it directly as an interval or as the image of a chosen weight set would erase the content of the target. Finite coupling bounds and conditional-joint modeling can be reused outside demographic disparity. Contributions proving the milestone statements, handling measurable selections, and connecting coupling arrays to probability measures are within scope. Estimation, true-positive and true-negative disparities, and additional assumptions on the joint law are outside this mission.

Selected references

Nathan Kallus, Xiaojie Mao, and Angela Zhou, Assessing Algorithmic Fairness with Unobserved Protected Class Using Data Combination, Management Science 68(3), 2022; preprint arXiv:1906.00285v2, 2020. Pinned preprint.

8 thms3 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Artificial Shortage in Agricultural Supply Chains: Cash Subsidy Leaves Artificial Shortage Unchanged on a Small Budget, Mitigates It on a Moderate One, and Aggravates It on a Large OneResearch Paper

Motivation

Prices of staple vegetables in India, onions above all, rise sharply at irregular intervals. When they do, governments respond with cash transfers, subsidized sales and import programmes. A recurring explanation for these price spikes is artificial shortage: traders who control a large share of the stock withhold supply early in a season, and consumers who observe the scarcity raise the amount they are willing to spend on the commodity, so the traders sell more later at a higher price. Levi, Singhvi and Zheng (SSRN 3332493; Manufacturing & Service Operations Management) give a stylized model of this mechanism. It shows that a monopolist trader facing budget-adjusting consumers creates an artificial shortage. It then asks how three common government interventions change the shortage. This mission formalizes the paper's answer for the first intervention, a cash subsidy (CS) to the poorest consumers. The question matters for policy: the paper argues that a well-intended transfer can make the hoarding worse.

Setting

A unit mass of consumers have Period-1 budgets $b_c$ distributed uniformly on $[0,1]$ . A monopolist trader sells over two periods.

Period 1. The trader releases $q_1\in[0,1]$ , which clears at price $p_1=1-q_1$ . Consumers interpret $q_1<1$ as a shortage and scale their budgets by the updated-budget multiplier

B(q_1)=1+g(1-q_1),

where $g>0$ is the budget adjustment factor.

Period 2, no intervention. A consumer buys at price $p_2$ iff $b_cB(q_1)\ge p_2$ . The trader's total revenue is $q_1(1-q_1)+B(q_1)q_2(1-q_2)$ .
Artificial shortage (Definition 1): $q_1<q_2$ and $p_1<p_2$ , i.e. less is sold early and the later price is still higher.

Under a cash subsidy $(c,f)$ , the government gives cash $c\ge0$ to the fraction $f\in[0,1]$ of consumers with the lowest budgets, within a budget $cf\le b$ . At price $p$ :

a non-subsidized consumer ( $b_c\ge f$ ) buys iff $b_c\ge p/B(q_1)$ ;
a subsidized consumer ( $b_c<f$ ) buys iff $b_c\ge(p-c)/B(q_1)$ .

The game is solved by backward induction:

the trader sets the Period-2 price, maximizing revenue;
the government, after observing $q_1$ , chooses $(c,f)$ to maximize Period-2 consumer welfare $CW_2$ (eq. (5)) at the trader's response. $CW_2$ measures the buyers' original budgets against the price they pay, adds the cash they receive, and counts a utility $\lambda$ per buyer and $-\lambda$ per non-buyer, with $1+g<\lambda$ ;
the trader chooses $q_1$ , anticipating both.

The set of equilibrium Period-1 quantities is $\mathrm{EqQ1}(b)$ . An element is written $q^1_{CS}$ , and $q^1_\phi$ is the no-intervention quantity.

Formalization targets

Goal: Proposition 3 (p. 22)

With $\bar b=(8+4g+g^2)/32$ , there is a threshold $t_1\in(0,\bar b)$ such that

q^1_{CS}=q^1_\phi\ (b<t_1),\qquad q^1_{CS}\ge q^1_\phi\ (t_1<b\le\bar b),\qquad q^1_{CS}<q^1_\phi\ (b>\bar b),

and $q^1_{CS}$ is non-increasing in $b$ for $b>t_1$ . The equilibrium set is also nonempty for every $b\ge0$ .

Milestones

Proposition 1 (p. 10): without intervention the unique optimum is $(q_1^*,q_2^*)=(1/2-g/8,\,1/2)$ , with $p_1^*=1/2+g/8$ and $p_2^*=1/2+g/4+g^2/16$ .
Remark after Proposition 1 (p. 10): for $g>0$ this optimum is an artificial shortage.
Theorem 1 (p. 16): the government's optimal subsidy is $f^*=\min(1,b/c^*)$ , with $c^*$ given by four closed forms on four budget ranges.
Theorem 2(i)–(iii) (p. 17): $q_1^*=1/2-g/8$ for $b<t_1$ , and the roots of two explicit first-order conditions on $[t_1,\bar b)$ and $[\bar b,(4+2g+g^2)/4)$ .
Theorem 2(iv), corrected (p. 17): for $b>(4+2g+g^2)/4$ ,

q_1^*=\max\{0,(1-g)/2,1-(b-1)/g\}.

Significance

Proposition 3 is the paper's verdict on cash subsidies. A small budget is absorbed without effect on the trader's behaviour, because the trader's Period-2 revenue equals its no-intervention value. A moderate budget induces a larger Period-1 release and so mitigates the shortage. A budget above $\bar b$ makes the trader withhold more than without intervention, because subsidized consumers can pay more in Period 2. The non-monotone dependence on $b$ is the basis of the paper's policy advice against "oversubsidizing" and of its comparison with supply-allocation schemes (Proposition 4, not in this mission).

The paper prints no proofs; they are "available from the authors upon request" (p. 10). The threshold $t_1$ and the online appendix (Lemma O.1) are not in the published text. A machine-checked development would therefore be the first complete public proof of these statements. It would also settle Theorem 2(iv), whose printed form is false on a band of budgets and is posed here in corrected form. None of these results has a formal proof anywhere.

Difficulty

Every stage of the backward induction is a non-smooth optimization.

Period 2. The demand is piecewise linear with up to three pieces, so the trader's revenue is bimodal. One mode sells only to non-subsidized consumers, the other also reaches subsidized ones.
Government. It optimizes over a two-dimensional policy against this discontinuous best response. The optimum sits at the trader's point of indifference between the two modes (Theorem 1(i)), which is attained only through the trader's tie-break toward the larger quantity.
Period 1. The trader's objective inherits the bimodality and a kink at $b=B(q_1)$ . The equilibrium therefore jumps at $t_1$ , and the printed closed form fails near the kink.

The tempting route is to differentiate the Period-1 objective and solve the first-order condition. It fails twice. It misses the jump at $t_1$ , where the global maximizer switches modes, and it misses the kink above $(4+2g+g^2)/4$ , where the maximizer is not a stationary point.

Formalization scope

All quantities are real numbers. The trader's Period-2 decision is a price $p\ge0$ with quantity equal to the explicit demand, which is equivalent to the paper's quantity form. Purchases at equality count as purchases, as in the text. The commitments are:

Standing assumptions: $0<g$ and $1+g<\lambda$ (pp. 10, 13), and the added $g<4$ , which keeps $1/2-g/8$ in $[0,1]$ .
Tie-breaks: the trader picks the larger quantity among revenue maximizers (footnote 10). The government picks the least outlay $cf$ among welfare maximizers. Without the second rule, Theorem 1(iv) and Proposition 3(i)(c) are false, because for $b>B(q_1)$ every $c\in[B(q_1),b]$ ties.
Equilibrium: $\mathrm{EqQ1}(b)$ is the set of $q_1\in[0,1]$ that maximize total revenue against some selection of government choices and Period-2 best responses. Every claim about $q^1_{CS}$ is made for every element.
Existential constants: $t_1$ , $b^{CS}_1$ and $b^{CS}_2$ , whose formulas are not in the paper. Each is pinned by the clauses around it.

The goal is stated about $\mathrm{EqQ1}$ itself. A version that substituted Theorem 2's closed forms or first-order roots for $q^1_{CS}$ would assume the content of the theorem, and is ruled out.

The development needs the Period-2 best response of a piecewise-linear demand, the government's two-variable welfare problem (eq. (5) is a polynomial in the breakpoints), and a comparison of the two modes of the Period-1 objective. Lemmas on maximizers of piecewise-quadratic functions are reusable beyond this mission. Proofs of any milestone, and sanity lemmas on the tie-breaks, are welcome.

Selected references

R. Levi, S. Singhvi, Y. Zheng, Artificial Shortage in Agricultural Supply Chains, Manufacturing & Service Operations Management (forthcoming; SSRN version of 2021-04-14), 2021. https://ssrn.com/abstract=3332493 — DOI of the journal version: https://doi.org/10.1287/msom.2021.1010

7 thms3 active usersReviewed

Completed

Economics Graph Theory Operations Research+1·Captain: mikedeng1

The Value of Price Discrimination in Large Random Networks: The Expected Fractional Regret of Uniform Pricing Vanishes in Erdős–Rényi Networks of Any DensityResearch Paper

Motivation

A seller whose customers influence one another faces a choice between two pricing policies. It can collect information about the social network and charge each customer a personalised price that reflects their position in it, or it can ignore the network and charge everyone one uniform price. Personalised pricing is never worse for the seller, but collecting network data is costly and raises privacy concerns. The question is how much profit the network information is worth.

For a fixed network the answer depends on its fine structure. Candogan, Bimpikis and Ozdaglar (Operations Research 2012) showed that with linear-quadratic utilities the optimal personalised prices are expressed through Bonacich centralities, so the gain from discrimination is a difference of discounted walk counts. Huang, Mani and Wang (SSRN 3368458; published in Management Science, 2021) study this gain, the value of price discrimination, in large random networks. Their main result for random networks, Theorem 5.1, says that in directed Erdős–Rényi networks the seller who prices uniformly loses only a vanishing fraction of the optimal profit, whatever the density of the network. This mission formalizes that theorem and the results its proof rests on.

Setting

There are $n$ consumers. The network is an $n\times n$ matrix $G$ with non-negative entries, where $G_{ij}$ is the influence of consumer $j$ on consumer $i$ . For a square matrix $A$ , $\|A\|$ is its spectral norm (the $\ell^2$ operator norm); $\mathbf 1$ is the all-ones vector, and $\mathbf 1^{\mathsf T}A^k\mathbf 1$ is the total weight of walks of length $k$ in $A$ .

Consumer $i$ facing price $p_i$ chooses a consumption level $x_i$ to maximise

u_i=ax_i-x_i^2+4\rho x_i\sum_{j\ne i}\frac{G_{ij}}{\|G+G^{\mathsf T}\|}x_j-p_ix_i,

with a stand-alone utility $a>0$ and a network coefficient $\rho\in(0,1)$ . The resulting consumption equilibrium is (eq. (1))

x^*(p)=\tfrac12\Big(I-\tfrac{2\rho}{\|G+G^{\mathsf T}\|}G\Big)^{-1}(a\mathbf 1-p).

The seller has marginal cost $c<a$ and profit $\pi(p)=(p-c\mathbf 1)^{\mathsf T}x^*(p)$ . The optimal profit is $\pi^*=\max_{p\in\mathbb R^n}\pi(p)$ ; the optimal uniform price is $p_0=\frac{a+c}{2}\mathbf 1$ . The regret and fractional regret of uniform pricing are

R(p_0)=\pi^*-\pi(p_0),\qquad R_F(p_0)=1-\frac{\pi(p_0)}{\pi^*}.

A directed Erdős–Rényi network $G(n,p)$ is the random $0/1$ matrix whose off-diagonal entries are independent with $\Pr[G_{ij}=1]=p$ , and whose diagonal is zero. $\mathbb E_G$ denotes expectation over it. The constants $a,c,\rho$ are the same for every $n$ .

Formalization targets

Goal: Theorem 5.1

For every sequence of densities $(p(n))_{n\in\mathbb N}$ with values in $[0,1]$ ,

\mathbb E_{G(n,p(n))}[R(p_0)]=o(n)\qquad\text{and}\qquad\mathbb E_{G(n,p(n))}[R_F(p_0)]=o(1).

Both parts are stated. The goal fixes no rate and no density regime; the paper's Theorems 5.2–5.4 give exact rates in three regimes and are not part of this mission.

Milestones

Eq. (3): $\pi^*$ is attained and equals $\frac12(\frac{a-c}{2})^2\,\mathbf 1^{\mathsf T}(I-\frac{\rho}{\|G+G^{\mathsf T}\|}(G+G^{\mathsf T}))^{-1}\mathbf 1$ , with its walk series.
Eq. (4): $p_0$ is the optimal uniform price, and $\pi(p_0)=\frac12(\frac{a-c}{2})^2\,\mathbf 1^{\mathsf T}(I-\frac{2\rho}{\|G+G^{\mathsf T}\|}G)^{-1}\mathbf 1$ .
Lemma 5.3 (for even $t$ ): $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1\le\|G+G^{\mathsf T}\|^{k-t}\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^t\mathbf 1$ for $k\ge t$ .
Eq. (29): $\mathbb E_G[R(p_0)]\le\frac12(\frac{a-c}{2})^2\,\mathbb E_G[\frac{\rho^2}{1-\rho}\|G+G^{\mathsf T}\|^{-2}\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1]$ .
Appendix D.1, Case 1, and footnote 6: a non-empty binary network has $\|G+G^{\mathsf T}\|\ge1$ . In the footnote's words, "Therefore a non-empty network (with at lease one link) has spectral norm greater than or equal to 1."
Lemma 5.2: $\mathbb E_G[\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1]=2n(n-1)p(1-3p+2np)$ .
Lemma 5.5 (i): $\mathbb E_G[\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1]\ge2^k\mathbb E_G[\mathbf 1^{\mathsf T}G^k\mathbf 1]$ for all $k\ge0$ .
Lemma 5.5 (ii): for $1\le k<n$ and $\frac1{n-k+1}\le p<1$ , the gap in (i) is at most $(k-1)2^{k-1}P(n,k)p^{k-1}+(k-1)^k2^kP(n,k-1)p^{k-2}$ , with $P(n,k)=n!/(n-k)!$ .
Eq. (12), Rayleigh step: $\|G+G^{\mathsf T}\|\ge\mathbf 1^{\mathsf T}(G+G^{\mathsf T})\mathbf 1/\mathbf 1^{\mathsf T}\mathbf 1$ .
Eq. (9): for non-empty $G$ and $k>0$ , $0<\mathbf 1^{\mathsf T}\big((G+G^{\mathsf T})/\|G+G^{\mathsf T}\|\big)^k\mathbf 1\le n$ .
Eq. (14): $\frac n2(\frac{a-c}2)^2\le\pi^*\le\frac12(\frac{a-c}2)^2\frac n{1-\rho}$ .

The paper calls the optimal uniform price $p_0$ "under the assumption that $c<a$ , according to [12]" (p. 7); milestone 2 states that optimality as part of eq. (4).

Significance

Theorem 5.1 says that in large random networks the network information has asymptotically no value to a monopolist: the uniform price $p_0$ does not depend on the network, yet earns a fraction of the optimal profit tending to one, for sparse, critical and dense networks alike. This separates the deterministic picture, where some networks have a large value of discrimination (Theorem 4.1 of the paper characterises those with none), from the typical random one. It supplies a benchmark against which network-based pricing, and the cost of collecting network data, can be judged.

The paper proves the theorem by hand. No part of it, and no part of the model, has been machine-checked; the platform has no network pricing model and no walk-count results for directed random graphs. A complete development would make the closed forms (3) and (4), the spectral inequalities and the Erdős–Rényi walk moments reusable. The printed proof of Theorem 5.1 bounds expectations of ratios by almost-sure statements and splits the density sequence into "maximal subsequences"; a formal proof must replace these steps by quantitative ones. The printed proof of Lemma 5.5 (i) relies on a per-walk claim that fails (a closed walk $0\to1\to2\to0\to1$ in $G+G^{\mathsf T}$ can use four arcs of $G$ while it visits three ordered pairs), although the statement itself was checked by exhaustive enumeration for small $n$ ; that lemma needs a new argument.

Difficulty

The regret is a difference of two discounted walk series. Bound (29) controls it by walks of length two and the spectral norm, which suffices when the network is very sparse, but in dense networks, where $\|G+G^{\mathsf T}\|\approx2np$ and $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1\approx4n^3p^2$ , it only gives $O(n)$ . The dense case needs the cancellation between $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1$ and $2^k\mathbf 1^{\mathsf T}G^k\mathbf 1$ for each $k$ up to a slowly growing cutoff (Lemma 5.5), together with a lower bound on the spectral norm that holds with high probability. In the critical regime $np=\Theta(1)$ , neither bound applies directly, and one needs that $\|G+G^{\mathsf T}\|$ grows with $n$ in probability. The goal quantifies over all density sequences, so the argument must be uniform across these regimes; a proof for one regime does not suffice.

Formalization scope

All objects live in the namespace NetPriceDisc.Random and are defined in one file. Networks are Matrix (Fin n) (Fin n) ℝ; the spectral norm is Mathlib's $\ell^2$ operator norm (Matrix.Norms.L2Operator). The consumption equilibrium is formula (1) for every price vector, with no non-negativity constraint on consumption, as in the paper's definition of $\pi(p)$ . $\pi^*$ is defined as the supremum of $\pi$ over $\mathbb R^n$ , and $R$ , $R_F$ from $\pi^*$ and $\pi(p_0)$ ; the closed forms (3) and (4) are theorems, not definitions, so the goal cannot be discharged by unfolding formulas. Lean's convention $x/0=0$ gives the empty network no externality, hence zero regret, which is the paper's own reading of the empty network (p. 12); the empty network keeps its probability $(1-p)^{n(n-1)}$ . The Erdős–Rényi expectation is the finite sum over arc sets $S$ of off-diagonal pairs with weight $p^{|S|}(1-p)^{n(n-1)-|S|}$ ; no measure theory is used. The fractional regret's expectation is the expectation of the ratio. "Any sequence of densities" is a function $\mathbb N\to[0,1]$ , with no further restriction.

Two printed statements are corrected and disclosed: Lemma 5.3 is stated for even $t$ (as printed it fails for odd $t$ ; for the star $K_{1,3}$ with $t=1$ , $k=2$ one gets $12>6\sqrt3$ ), and Lemma 5.5 (ii) for $k\ge1$ (at $k=0$ it involves the undefined $P(n,-1)$ ). Only the deterministic Rayleigh-quotient part of eq. (12) is stated.

Useful infrastructure includes Neumann series and Rayleigh-quotient bounds for symmetric non-negative matrices, walk moments of directed Erdős–Rényi graphs, and maximum-degree or spectral lower bounds in probability. Proofs of any milestone, and alternative routes to the goal that avoid Lemma 5.5, are welcome.

Selected references

J. Huang, A. Mani, Z. Wang, The Value of Price Discrimination in Large Random Networks, SSRN 3368458 (EC '19 submission version); published as The Value of Price Discrimination in Large Social Networks, Management Science, 2021. https://ssrn.com/abstract=3368458, https://doi.org/10.1287/mnsc.2021.4108
O. Candogan, K. Bimpikis, A. Ozdaglar, Optimal Pricing in Networks with Externalities, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1066
P. Bonacich, Power and Centrality: A Family of Measures, American Journal of Sociology 92(5), 1987. https://doi.org/10.1086/228631
M. Krivelevich, B. Sudakov, The Largest Eigenvalue of Sparse Random Graphs, Combinatorics, Probability and Computing 12(1), 2003. https://doi.org/10.1017/S0963548302005424

15 thms3 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Dynamic Probabilistic Selling When Customers Have Boundedly Rational Expectations: The Optimal Two-Period Pricing and Product-Offering Policy When Each Customer Draws One AnecdoteResearch Paper

Motivation

Probabilistic selling, also called opaque selling, offers a customer a product whose exact version is revealed only after purchase: a "mystery box", an unnamed hotel on a travel site, a flight whose carrier is announced after booking. The firm controls the price and the probability with which each version is delivered. The classical analyses (Fay and Xie 2008; Jerath, Netessine and Veeraraghavan 2010) assume customers know these probabilities and form rational expectations.

Huang and Yin (SSRN 3627927; Manufacturing & Service Operations Management, 2020) drop that assumption. Customers do not observe the offering probability; they infer it from a few anecdotes, which are reports of what earlier buyers received, in the spirit of the literature on the belief in small samples (Tversky and Kahneman 1971), here as a model of boundedly rational expectations. Because today's deliveries become tomorrow's anecdotes, the firm's offering decision in one period shapes demand in the next, and probabilistic selling becomes a dynamic problem. The paper's first main result, Proposition 1, solves the two-period problem when every customer draws a single anecdote.

Setting

A firm sells two versions of a product, $H$ and $L$ , over two periods $t=1,2$ . Each period has a fresh unit mass of customers. Every customer values $H$ at $v_H$ and $L$ at $v_L$ , with $v_H>v_L$ ; unit costs are $c_H>c_L$ ; and $c_L\le v_L$ .

In period $t$ the firm posts one price $p_t$ for the opaque product and delivers $H$ with probability $\xi_t\in[0,1]$ . A customer draws one anecdote and estimates the $H$ -probability as $\tilde\xi=(\xi_0+\mathbf 1\{\text{anecdote}=H\})/2$ with prior $\xi_0=0$ , so $\tilde\xi\in\{0,\tfrac12\}$ . She buys if and only if

\tilde\xi\,v_H+(1-\tilde\xi)\,v_L\ \ge\ p_t .

A period-1 anecdote is $H$ with probability $\xi_1$ . A period-2 anecdote comes from period 1 with probability $\alpha\in[0,1]$ and from period 2 otherwise, so it is $H$ with probability $\alpha\xi_1+(1-\alpha)\xi_2$ . Writing $\gamma_t$ for the purchasing fraction, the firm's profit is

\Pi(\xi_1,\xi_2\mid p_1,p_2)=\sum_{t=1,2}\gamma_t\,[p_t-\xi_tc_H-(1-\xi_t)c_L].

The price $v_{HL}=\frac{v_H-v_L}{2}+v_L$ is what a customer with an $H$ anecdote is willing to pay; $v_L$ is what everyone pays. The alternative is transparent selling: one version $m$ at prices $q_1,q_2$ , bought in period $t$ iff $q_t\le v_m$ .

Formalization targets

Goal: Proposition 1

Let $\bar\alpha=\frac{\sqrt{17}-3}{2}$ , $r=\frac{v_{HL}-c_L}{c_H-c_L}$ and $M=\max\{v_H-c_H,v_L-c_L\}$ . Over all feasible opaque and transparent policies:

(i) if $0\le\alpha<\bar\alpha$ , $r<\frac{4-4\alpha-\alpha^2}{2-\alpha-\alpha^2}$ and $\frac{(1-\alpha)(v_{HL}-c_L)^2}{(4-4\alpha-\alpha^2)(c_H-c_L)}>M$ , the optimal policy is

p_1^*=p_2^*=v_{HL},\quad \xi_1^*=\frac{(2-\alpha-\alpha^2)(v_{HL}-c_L)}{(4-4\alpha-\alpha^2)(c_H-c_L)},\quad \xi_2^*=\frac{(2-3\alpha-\alpha^2)(v_{HL}-c_L)}{(4-4\alpha-\alpha^2)(c_H-c_L)},

with profit $\Pi^*=\frac{2(1-\alpha)(v_{HL}-c_L)^2}{(4-4\alpha-\alpha^2)(c_H-c_L)}$ ;

(ii) if $\bar\alpha\le\alpha\le1$ , $r<\frac{2}{1+\alpha}$ and $\frac{(1+\alpha)^2(v_{HL}-c_L)^2}{8(c_H-c_L)}>M$ , the optimal policy is

p_1^*=p_2^*=v_{HL},\quad \xi_1^*=\frac{(1+\alpha)(v_{HL}-c_L)}{2(c_H-c_L)},\quad \xi_2^*=0,\qquad \Pi^*=\frac{(1+\alpha)^2(v_{HL}-c_L)^2}{4(c_H-c_L)};

(iii) otherwise, transparent selling of the version with the larger margin, at its valuation in both periods, is optimal, with $\Pi^*=2M$ .

Milestones

In the order the paper's argument uses them:

Lemma 1 for one anecdote: the demands at $v_L$ and $v_{HL}$ , and the reduction of every price pair to these two candidates;
displays (3)–(6): the profit at each of the four candidate price pairs;
the §3.3 benchmark: transparent selling earns at most $2M$ ;
Lemma 2 (i) and (ii): maximizers of (3) on $[0,1]^2$ in seven regimes;
Lemma 3: maximizers of (4);
Lemma 4, in corrected form: (5) is dominated by (3) or (4);
the claim after (6): $\xi_1=\xi_2=0$ is optimal at $p_1=p_2=v_L$ ;
from the proof of Proposition 1: the price pair $(v_{HL},v_L)$ is never strictly better than the best of (3) and transparent selling;
from the same proof: in the corner regimes of Lemma 2, the policy $(v_{HL},v_{HL})$ earns at most $2M$ .

Significance

The result says when, and how, a firm should randomize its product delivery when customers learn from anecdotes. The optimal offering probability is decreasing over time, $\xi_1^*>\xi_2^*$ : the firm delivers the high version generously early, so that period-1 deliveries become favourable anecdotes for period-2 customers, and then saves cost. Probabilistic selling is optimal only when both transparent margins are low, which makes it a complement to transparent selling rather than a substitute. Corollary 2 of the paper builds on Proposition 1 to show that the dynamic policy can earn up to twice the profit of the best static one.

Proposition 1 is proved in the paper's appendix (pp. 30–31), with Lemmas 1–4 proved in an online appendix. No part of it has been machine-checked. A formalization supplies the missing lemma proofs in checked form, pins down the conventions the printed statements leave implicit (tie-breaking, the price domain, the sign of $v_L-c_L$ ), and corrects a false part of Lemma 4 as printed. The model layer, an anecdote-based demand computed from a purchase rule, is a reusable template for other sampling-based expectation models.

Difficulty

The goal is a global optimality claim over a continuum of prices and offering probabilities and a second family of transparent policies. Lemma 1 reduces prices to two candidates, but each of the four resulting objectives is a non-separable quadratic in $(\xi_1,\xi_2)$ , maximized over a box. Objective (3) has seven regimes whose boundaries depend on $\alpha$ and on the margin ratio $r$ ; the threshold $\bar\alpha$ is where the interior optimum's $\xi_2$ reaches zero. Comparing the regimes with each other and with transparent selling requires signed polynomial inequalities in $\alpha$ and $r$ across regime boundaries. Checking first-order conditions is not enough: in part (iii) the claim is that no opaque policy at any price beats transparent selling, which requires bounding the box maximum of every objective, including the corner regimes.

Formalization scope

Everything is real-valued and lives in the namespace DynOpaque.TwoPeriod. The definitions file states the model from its primitives: the anecdote estimate with $K=1$ and $\xi_0=0$ , the purchase rule (1) with equality buying, the purchasing fraction derived from them, profit (2), transparent profit from a version and two prices, the policy type with its feasibility predicate, and global optimality. The objectives (3)–(6) are separate literal definitions, so their agreement with (2) is a theorem, not a definition.

Committed conventions, each disclosed in the statements:

$c_L\le v_L$ is added to the paper's standing assumptions $v_H>v_L$ , $c_H>c_L$ , $0\le\alpha\le1$ . The paper's proof uses it (p. 30), and without it $\xi_1^*$ in (i) can be negative.
Opaque prices satisfy $p_t\le v_{HL}$ . Lemma 1 places every optimal price in $\{v_L,v_{HL}\}$ ; above $v_{HL}$ nobody buys, there are no anecdotes, and the paper's period-2 dynamics are undefined. Transparent prices are unrestricted.
"Otherwise" in (iii) is the negation of the full hypothesis lists of (i) and (ii).
Lemma 4 (i) as printed (" $\xi_1=1$ or $\xi_2=0$ is optimal") is false; the mission states the corrected claim that some optimum has $\xi_1\in\{0,1\}$ .
Lemma 2's "optimal" is a maximizer over $[0,1]^2$ , not a unique one.

A formalization that optimizes only over the candidate prices $\{v_L,v_{HL}\}$ , defines demand by the closed forms $\xi_1$ and $\alpha\xi_1+(1-\alpha)\xi_2$ , or defines the transparent value as $2M$ would make Lemma 1 or part (iii) circular; the goal quantifies over every feasible price and derives demand from the purchase rule.

The general- $K$ model (Lemma 1 with binomial sums, Proposition 3), the extensions of §5, and Corollaries 1–2 are out of scope. Proofs of any milestone are welcome, and so are reusable lemmas on maximizing quadratics over a box.

Selected references

T. Huang and Z. Yin, Dynamic Probabilistic Selling When Customers Have Boundedly Rational Expectations, Manufacturing & Service Operations Management, 2020; SSRN manuscript 3627927. https://ssrn.com/abstract=3627927 (doi:10.1287/msom.2020.0894)
S. Fay and J. Xie, Probabilistic Goods: A Creative Way of Selling Products and Services, Marketing Science 27(4), 674–690, 2008. https://doi.org/10.1287/mksc.1070.0318
K. Jerath, S. Netessine and S. K. Veeraraghavan, Revenue Management with Strategic Customers: Last-Minute Selling and Opaque Selling, Management Science 56(3), 430–448, 2010. https://doi.org/10.1287/mnsc.1090.1125
A. Tversky and D. Kahneman, Belief in the Law of Small Numbers, Psychological Bulletin 76(2), 105–110, 1971. https://doi.org/10.1037/h0031322

12 thms3 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Intertemporal Segmentation via Flexible-Duration Group Buying: Above an Explicit Batch-Size Threshold, the Optimal Uniform-Price Campaign Admits High-End Customers First and Both Segments LaterResearch Paper

Motivation

Group buying sells a product at a discount once enough customers have committed to it. Groupon's "a deal a day" campaigns ran on a fixed deadline. Group buying on Pinduoduo has no preset deadline: a customer pledges, then waits until the group is complete. Most of the operations literature studies the first, fixed-duration form, in which a campaign ends at its deadline whether or not the threshold is reached. Hu, Liu and Zhai (SSRN 3242687, Manufacturing & Service Operations Management) study the flexible-duration form: the campaign stays open until $N$ customers have signed up, a batch of $N$ premium units is produced, and a new campaign starts at once.

In this form the expected waiting time of a new customer falls as the campaign fills up. A customer arriving early faces a long wait, a customer arriving late a short one. The firm can therefore use the state of the campaign itself to separate customer segments over time, which the paper calls intertemporal segmentation: high-valuation customers sign up early, and low-valuation customers join once the remaining wait is short enough. The paper's Proposition 2 says exactly when a profit-maximizing firm chooses this.

Setting

Customers arrive as a Poisson process with rate $\lambda>0$ . A fraction $\gamma\in(0,1)$ are high-end, with valuation $H$ , and the rest are low-end, with valuation $L$ , where $H>L>0$ . The firm sells a regular product of quality $1$ at price $r$ and a group-buying premium product of quality $\theta>1$ at price $p$ . A customer who signs up for the premium product gets $\theta v - p - c\,w$ , where $v$ is her valuation, $w$ is her expected waiting time and $c>0$ is the waiting cost per unit time. Buying the regular product gives $v-r$ . Prices are fixed for the whole horizon, and the firm maximizes long-run average profit.

The pledge-to-go state $n\in\{1,\dots,N\}$ is the number of further sign-ups the campaign still needs. In the equilibria of interest, high-end customers sign up at every state and low-end customers sign up once the state has fallen to the tipping state $\bar x^G\in[0,N]$ . The three resulting scenarios are $\{H\}$ (never tip, $\bar x^G=0$ ), $\{H;H+L\}$ (intertemporal segmentation, $0<\bar x^G<N$ ) and $\{H+L\}$ (always tip, $\bar x^G=N$ ). The expected waiting time is

w^G(n)=\frac{n-1}{\lambda}\ (n\le\bar x^G),\qquad w^G(n)=\frac{\bar x^G}{\lambda}+\frac{n-\bar x^G-1}{\gamma\lambda}\ (n>\bar x^G).

The firm sets $r^G=L$ . Its premium price is the largest one that keeps high-end customers signing up at state $N$ and low-end customers at state $\bar x^G$ :

p^G=\min\{\bar p^G_1,\bar p^G_2\},\qquad \bar p^G_1=\theta L-c\,w^G(\bar x^G),\qquad \bar p^G_2=(\theta-1)H+L-c\,w^G(N).

At $\bar x^G=0$ only $\bar p^G_2$ applies. The profit $\pi^G(\bar x^G)$ is revenue per expected renewal cycle.

Formalization targets

Goal: Proposition 2

With $\bar N_1=(\theta-1)(1-\gamma)L\lambda/c+1-\gamma$ , $\bar N_2=(\theta-1)(H-L)\gamma\lambda/c+1-\gamma$ and $\bar x^G_1=N-1+\gamma-(\theta-1)(H-L)\gamma\lambda/c$ , the optimal tipping state over $[0,N]$ is

\bar x^G=\begin{cases} N & H/L\le 1/\gamma,\ N\le\bar N_1,\\ \bar x^G_1\in(0,N) & H/L\le 1/\gamma,\ N>\bar N_1,\\ 0 & H/L>1/\gamma,\ N\le\bar N_2,\\ \bar x^G_1\in(0,N) & H/L>1/\gamma,\ N>\bar N_2.\end{cases}

In each case the optimal price $p^G$ and profit $\pi^G$ also have the closed forms printed in the proof (Online Appendix pp. 4–5).

Milestones

Lemma A.1: a sign-up at state $n$ persists at every later state.
Proposition 1: for $\theta>1$ , no low-end-first campaign satisfies the IR/IC constraints.
Five displayed steps of the proof of Proposition 2:
- the price switch $\bar p^G_1<\bar p^G_2\iff\bar x^G>\bar x^G_1$ ;
- the closed form of $\pi^G$ ;
- the derivative of $\pi^G$ on each branch and its sign;
- $\bar x^G_1>0\iff N>\bar N_2$ ;
- $\bar N_2>\bar N_1\iff H/L>1/\gamma$ .

Significance

Proposition 2 is the paper's characterization of equilibrium segmentation. It shows that a flexible-duration campaign can separate customers through time alone, with one uniform price. It also shows that the separation is chosen for every large enough batch size, whatever the valuation ratio. The profit comparisons of the paper's Theorem 2, between group buying and the volume, margin and product-line strategies, are built on these closed forms.

The proof is a printed calculation on Online Appendix pp. 3–5, and no part of it has been machine-checked. A formalization checks three things: the case analysis over the whole interval $[0,N]$ , including the junction at $\bar x^G_1$ and the endpoint $\bar x^G=0$ ; the closed forms, notably $\pi^G_1$ ; and the threshold algebra.

Difficulty

The calculations are elementary, but $\pi^G$ is piecewise. The price switches branch at $\bar x^G_1$ , and at $\bar x^G=0$ it is not given by the minimum formula at all. A proof must compare the maxima of both branches with the value at $0$ . In case (ii-1) with $\bar N_1<N\le\bar N_2$ , the late branch is decreasing and its supremum is approached as $\bar x^G\to0^+$ without being attained. Only the jump of the price at $0$ makes $\bar x^G=0$ optimal there. The obvious argument, "each branch is monotone, so compare endpoints", has to handle this endpoint carefully.

Formalization scope

All quantities are real numbers, and the parameters are bundled in a structure Params with a predicate Standing ( $H>L>0$ , $0<\gamma<1$ , $\lambda>0$ , $c>0$ , $\theta>1$ ). The batch size is a natural number $N\ge1$ .
The tipping state is real, $\bar x^G\in[0,N]$ , as in the paper's appendix (footnote 1, Online Appendix p. 2). The waiting time at $n=\bar x^G$ takes the first branch.
$p^G(0)=\bar p^G_2(0)$ : no low-end customer signs up at $\bar x^G=0$ .
$\pi^G$ is defined by the renewal-cycle ratio, not by its simplified closed form.
Optimality means maximizing $\pi^G$ over all of $[0,N]$ . Uniqueness is not claimed.
The optimization is the paper's reduced problem: $r^G=L$ with ICH and ICL2 binding. The constraints IRH, IRL2 and ICL1 are not imposed, since the proof never checks them.
Proposition 1 is formalized as the infeasibility of the low-end-first constraint system, which is what its proof establishes.

Defining $p^G$ or $\pi^G$ case by case, or maximizing over $\{0,\bar x^G_1,N\}$ only, would trivialize the goal. Both are ruled out: $p^G$ is the binding-constraint minimum, and the maximum ranges over the whole interval.

Only Mathlib's real analysis (HasDerivAt, monotonicity from derivatives) is needed. Proofs of any milestone are welcome. The model definition is specific to this paper.

Selected references

M. Hu, J. Liu, X. Zhai, Intertemporal Segmentation via Flexible-Duration Group Buying, Manufacturing & Service Operations Management (forthcoming; SSRN version of 2019-12-06). https://ssrn.com/abstract=3242687 — published version DOI 10.1287/msom.2020.0869.

10 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Second-Order Optimality Conditions for Nonconvex Set-Constrained Optimization Problems: A Directional Second-Order Necessary Condition via the Lower Generalized Support FunctionResearch Paper

Motivation

Optimization problems often require a smooth objective to be minimized subject to membership in a set. When that set is convex, established second-order conditions describe how curvature of the objective and constraints limits a local solution. Complementarity constraints and related models lead to nonconvex constraint sets. The tangent sets needed for a second-order condition can then be nonconvex as well, so a condition expressed only through ordinary convex support functions does not cover the general case. Gfrerer, Ye, and Zhou study this setting and state a directional necessary condition that permits a nonconvex set and a directional form of metric subregularity. Their result is Theorem 2 of arXiv:1911.04076v2, on printed page 16.

The mission concerns the first of the paper's two approaches to second-order necessary conditions. It targets the theorem that uses a lower generalized support function. The paper also develops conditions through convex duality under a stronger directional qualification; those results have different hypotheses and are outside this mission's target. The theorem here is a proved mathematical result whose statement and supporting definitions remain to be formalized and proved in Lean.

Setting

Fix natural dimensions $n$ and $m$ . A problem $(P)$ consists of twice continuously differentiable maps $f:\mathbb R^n\to\mathbb R$ and $g:\mathbb R^n\to\mathbb R^m$ , together with a closed set $\Lambda\subseteq\mathbb R^m$ . Its feasible region is $F=\{x:g(x)\in\Lambda\}$ . A point $\bar x\in F$ is a local solution if no sufficiently nearby feasible point has a smaller value of $f$ .

For a set $S$ and a point $x\in S$ , the contingent cone $T_S(x)$ collects limits of directions of feasible displacements $x+t_kd_k\in S$ as $t_k\downarrow0$ . Given a direction $d$ , the outer second-order tangent set $T_S^2(x;d)$ collects limits of $w_k$ for displacements $x+t_kd+\tfrac12t_k^2w_k\in S$ . It can be empty and need not be convex. The regular normal cone $\widehat N_S(x)$ describes vectors whose inner product with nearby displacements into $S$ is negligible to first order. Limits of these normals form the limiting normal cone $N_S(x)$ ; restricting their approach to direction $d$ gives the directional limiting normal cone $N_S(x;d)$ .

The critical cone at $\bar x$ is $C(\bar x)=\{d:\nabla g(\bar x)d\in T_\Lambda(g(\bar x)),\;\nabla f(\bar x)d\le0\}$ . Directional metric subregularity requires an error bound near $\bar x$ within a neighborhood of the ray in direction $d$ : distance to $F$ is at most a positive constant times distance from $g(x)$ to $\Lambda$ . The neighborhood is precisely $\bar x+V_{\rho,\delta}(d)$ from Definition 6, including the zero direction.

The Lagrangian is $L(x,\lambda)=f(x)+g(x)^\top\lambda$ . A directional M-multiplier at $(\bar x,d)$ satisfies $\nabla_xL(\bar x,\lambda)=0$ and $\lambda\in N_\Lambda(g(\bar x);\nabla g(\bar x)d)$ . For a set $S$ and a subset $A$ , the lower generalized support function $\widehat\sigma_{S,A}(\lambda)$ is the lower limit, as $\widetilde\lambda\to\lambda$ , of the infimum of $\widetilde\lambda^\top u$ over $u\in A$ with $\widetilde\lambda\in N_S(u)$ . Write $\widehat\sigma_S$ when $A$ is the whole space. The paper's Definition 7 assigns $+\infty$ to the unrestricted function when $S$ is empty.

Formalization targets

Let $D=T_\Lambda^2(g(\bar x);\nabla g(\bar x)d)$ and let $A_{\mathrm{opt}}=\nabla g(\bar x)T_F^2(\bar x;d)+\nabla^2g(\bar x)(d,d)$ . The main target is Theorem 2, equations (17) and (18): if $\bar x$ is a local solution, $d\in C(\bar x)$ , directional metric subregularity holds along $d$ , and $D$ is nonempty, then one directional M-multiplier $\lambda$ works for every $A\supseteq A_{\mathrm{opt}}$ :

\widehat\sigma_{D,A}(\lambda)\le\nabla_{xx}^2L(\bar x,\lambda)(d,d).

The same multiplier gives the unrestricted conclusion $\widehat\sigma_D(\lambda)\le\nabla_{xx}^2L(\bar x,\lambda)(d,d)$ . The goal retains the order “there exists $\lambda$ such that for every $A$ .” The milestones state the paper's supporting results: the distance and outer-limit identity, the tangent and second-order tangent chain rules, their error bound and nonemptiness consequence, the primal second-order necessary condition, the critical-direction derivative condition, and the inclusion of limiting normals to a second-order tangent set.

Significance

The result supplies a directional dual necessary condition for a local minimizer without assuming that $\Lambda$ is convex. Its multiplier belongs to a directional normal cone, which can be smaller than the ordinary limiting normal cone. The set $A$ also lets the condition retain information about which second-order constraint perturbations arise from feasible displacements. The paper explains that taking $A=\mathbb R^m$ gives a more tractable but weaker condition, while $A_{\mathrm{opt}}$ gives the strongest member of this family on page 17.

A complete formalization would provide checked interfaces for second-order tangent sets, directional normals, directional metric subregularity, and lower generalized support. Those objects can be reused in later work on nonconvex constrained optimization. This mission supplies statements and definitions; the published mathematical argument still needs a Lean proof. The local draft's compilation checks statement well-formedness, not the theorems' truth.

Difficulty

At a local minimum, ordinary first-order information constrains derivatives along contingent directions. The second-order tangent set is harder: it may be empty, and even when the original set is convex it need not be convex. The usual convex-support interpretation therefore cannot simply be applied to it. In addition, the error bound for the original constraint system must remain valid in the second-order linearized setting before normal-cone information can be transferred. These are the substantive points represented by Proposition 5 and Lemma 3 in the milestone list.

Formalization scope

The Lean development uses EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), so both dimensions are finite and may be zero. The standing assumptions of $(P)$ are explicit: both maps are $C^2$ and $\Lambda$ is closed. The contingent and second-order tangent sets use positive sequences tending to zero; a monotonically decreasing sequence can be selected from one of these. Tangent sets and normal cones are empty when their base point is outside the underlying set, matching the domain stated in Definitions 1, 3 and 4. Second derivatives are Fréchet derivatives applied twice to $(d,d)$ . A local minimum is stated together with feasibility.

Distances to possibly empty second-order tangent sets or outer limits use extended nonnegative reals, with distance to the empty set equal to $+\infty$ . The lower generalized support function uses extended reals, where an empty infimum is $+\infty$ ; the goal compares its value with the real Hessian value embedded in that order. This expresses the paper's “Hessian minus support is nonnegative” without undefined extended-real subtraction. Directional metric subregularity requires positive constants and the exact neighborhood in Definition 6, including $0$ ; it cannot be satisfied by making that neighborhood empty. Likewise the lower generalized support function is computed from limiting normals and is not assigned a constant extreme value.

The paper's $t_k\downarrow0$ is represented by $t_k>0$ and $t_k\to0$ . The “modulus $\kappa$ ” in Proposition 5 is represented by an admissible constant in the defining error bound. Equations (11), (12), and Corollary 1 contain printed slips in the point or derivative notation; their Lean statements use $\bar x$ and $\nabla^2g$ as their surrounding formulas and proofs require. Equation (18) uses the same multiplier as (17), by taking $A$ to be the whole space. Contributions to the definitions, chain rules, error bound, normal-cone inclusion, and final theorem are all within scope.

Selected references

H. Gfrerer, J. J. Ye, and J. Zhou, Second-order optimality conditions for non-convex set-constrained optimization problems, arXiv:1911.04076v2, 2020; published in Mathematics of Operations Research, 2022. Pinned preprint.

11 thms3 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Fair Allocation of Indivisible Goods: Improvement and Generalization: Every Instance with Additive Valuations Admits a 3/4-MMS AllocationResearch Paper

Motivation

Dividing a set of indivisible goods among agents with different preferences is a basic problem of fair division, with applications to inheritance, course allocation and the division of shared assets. With indivisible goods, envy-freeness and proportionality cannot always be achieved: a single good and two agents already rule both out. Budish (The combinatorial assignment problem, J. Political Economy, 2011) proposed the maxmin share as a benchmark that adapts to indivisibility: each agent is guaranteed what it could secure by partitioning all goods into $n$ bundles and receiving the worst one.

Whether every agent can receive its maxmin share at once has a short history.

2014. Procaccia and Wang (Fair enough: guaranteeing approximate maximin shares, EC 2014) showed that for additive valuations an allocation giving every agent its full maxmin share need not exist, and that a $2/3$ fraction can always be guaranteed.
2015–2017. Amanatidis, Markakis, Nikzad and Saberi (ICALP 2015) gave polynomial-time $(2/3-\epsilon)$ -approximations; Kurokawa, Procaccia and Wang (J. ACM 2018) and others refined the $2/3$ analysis, and several of these arguments were tight at $2/3$ .
2017–2021. Ghodsi, Hajiaghayi, Seddighin, Seddighin and Yami (arXiv:1704.00222; Mathematics of Operations Research, 2021) proved that a $3/4$ fraction can always be guaranteed for additive valuations, and also gave guarantees for submodular, XOS and subadditive valuations.

This mission formalizes the additive $3/4$ result of the last paper.

Setting

There are $n\ge 1$ agents $a_1,\dots,a_n$ and a finite set $\mathcal M$ of $m$ goods (items) $b_1,\dots,b_m$ . Agent $a_i$ has a valuation $V_i$ on sets of goods. It is additive when

V_i(S)=\sum_{b\in S}V_i(\{b\}),\qquad V_i(S)\ge 0\qquad(S\subseteq\mathcal M).

For a set function $f$ and $r\ge 1$ , the $r$ -maxmin share of a set $\mathcal M$ is

\mathsf{MMS}^r_f(\mathcal M)=\max_{(P_1,\dots,P_r)}\ \min_{1\le j\le r} f(P_j),

the maximum over all partitions of $\mathcal M$ into $r$ disjoint parts, and $\mathsf{MMS}_i=\mathsf{MMS}^n_{V_i}(\mathcal M)$ is the maxmin share of agent $a_i$ .

An allocation gives each good to exactly one agent; $A_i$ is the set agent $a_i$ receives. It is $\alpha$ -MMS if $V_i(A_i)\ge\alpha\,\mathsf{MMS}_i$ for every agent.

The paper's proof works with instances $(\mathcal N,\mathcal M)$ , a set of agents and a set of goods. An instance is $\alpha$ -reducible (Definition 2.1) if some non-empty set $T$ of agents can be given a set $S$ of goods so that each agent of $T$ gets at least $\alpha\,\mathsf{MMS}_i$ and every other agent keeps its share in the smaller instance, $\mathsf{MMS}^{n-|T|}_{V_i}(\mathcal M\setminus S)\ge\mathsf{MMS}_i$ ; otherwise it is $\alpha$ -irreducible. The proof also uses bipartite graphs between goods and agents, maximum matchings, the set $F_H(M,\hat{\mathcal X})$ of vertices not reachable by alternating paths (Definition 3.5), maximum cardinality maximum weight matchings (MCMWM), and an envy relation among agents holding partial bundles (Definitions 3.9–3.12).

Formalization targets

Goal: Theorem 3.39, existence form

For every $n\ge 1$ and all additive valuations $V_1,\dots,V_n$ on $\mathcal M$ there is an allocation $\langle A_1,\dots,A_n\rangle$ of $\mathcal M$ with

V_i(A_i)\ \ge\ \tfrac34\,\mathsf{MMS}_i\qquad(1\le i\le n).

Table 1 of the paper (p. 5) lists this existential statement as Theorem 3.39; the sentence printed under that number on p. 30 is the claim that the paper's algorithm satisfies every agent before it stops. The goal fixes no normalization of the valuations.

Milestones

The milestones are the statements of §2 and §3.2–§3.3 that the existence proof uses, in attack order.

Observation 2.1: if every $\alpha$ -irreducible instance admits an $\alpha$ -MMS allocation, every instance does.
Lemma 3.1, inequality (16) from the proof of Lemma 3.2, Lemma 3.2 and Lemma 3.3: under $\mathsf{MMS}_i=1$ , irreducibility bounds the value of single goods ( $<\alpha$ ) and of pairs of goods ( $V_{i'}(\{b_j,b_k\})>1$ for some other agent whenever a pair is worth $3/4$ to one).
Lemma 3.20 and Corollary 3.21, in restated form: two goods each worth less than $1/2$ to everyone are together worth less than $3/4$ to everyone, so each agent values at most one such good at $3/8$ or more.
Lemmas 3.6, 3.7 and Corollary 3.8: strict Hall conditions $|N(T)|>|T|$ for the vertices outside $F_H(M,\hat{\mathcal X})$ .
Lemma 3.11 and Observation 3.1: a cycle-envy-free set has an acyclic envy graph, and in its topological order $V_i(f_j)\le 3/4-\epsilon_i$ for earlier agents $a_j$ .
Lemma 3.13: winner, loser and unsaturated-vertex properties of an MCMWM.

Significance

The result. The factor $3/4$ broke a barrier at $2/3$ that several earlier techniques could not pass. It shows that the structural properties of the maxmin share known before were not the limit of what can be guaranteed, and its reducibility argument and double-counting techniques were reused in later improvements of the constant. The value of the best possible constant remains open: Feige, Sapir and Tauber (WINE 2021) showed it is at most $39/40$ .

Formalizing it. The theorem is proved on paper, in a long case analysis spread over about forty pages of the paper and its appendices. To our knowledge no part of it has a machine-checked proof. A formal development would check the case analysis and would provide reusable statements about maxmin shares under removal of goods and agents, about alternating-path structure in bipartite matchings, and about maximum weight matchings. These are used across the fair-division literature.

Difficulty

The obvious approach is to fill bags greedily: give an agent a bag as soon as it reaches $3/4$ of its share. This works when all goods are small, but large goods break it. A bag closed by a large good can be worth far more than $3/4$ to the agent who takes it, and the goods left over may no longer be worth enough to the remaining agents. Reducibility removes the very large goods (Lemmas 3.1–3.3), but goods worth between roughly $1/4$ and $3/4$ remain. Assigning them requires clustering the agents through matchings (Lemmas 3.6–3.13) and a careful order in which the clusters are served. The final counting argument, which shows that the leftover goods suffice for the agents not yet served, is the step that depends on all the earlier structure.

Formalization scope

Agents are Fin n and goods Fin m. Valuations are v : Fin n → Finset (Fin m) → ℝ with the published LittleCharity.MMS.IsAdditive (sum of singleton values, non-negative). The paper's printed additivity identity on p. 12 contains a sign slip; the paper uses only the sum form. The maxmin share is the published LittleCharity.MMS.mms (v i) k S, a maximum over labelled, possibly empty $k$ -partitions. An allocation is a map A : Fin m → Fin n; agent $i$ receives the goods mapped to $i$ . Instances $(\mathcal N,\mathcal M)$ are pairs of finite sets of the ambient agents and goods, so sub-instances need no re-indexing.

The following conventions are added or chosen, each disclosed in the item's Formalization Note:

the set $T$ of Definition 2.1 is non-empty, and $T=\mathcal N$ is allowed;
Observation 2.1 ranges over instances with at least one agent;
the §3 normalization $\mathsf{MMS}_i=1$ (p. 14) is a hypothesis of Lemmas 3.1–3.3, (16), 3.20 and 3.21;
inequality (16) assumes at least two agents;
the sets $T$ of Lemmas 3.3, 3.6, 3.7 and 3.13 are non-empty, since the printed statements fail or are vacuous at $T=\emptyset$ ;
envy is between distinct agents;
Lemma 3.20 and Corollary 3.21 replace membership in the algorithm-built set $\mathcal X'\setminus\mathcal X'_{1/2}$ by the property their proofs use (every such good is worth less than $1/2$ to every agent);
the goal assumes $n\ge 1$ .

Bipartite graphs are two finite vertex sets with an edge set $E\subseteq\hat{\mathcal X}\times\hat{\mathcal Y}$ . Alternating-path reachability is an inductive predicate.

The goal is the unconditional existence statement. A formalization that assumes $\mathsf{MMS}_i=1$ or irreducibility in the goal, or that drops the requirement that every good be allocated, does not state the paper's theorem. Neither does one that lets the reducing set $T$ be empty, which would make every irreducibility hypothesis unsatisfiable. The paper's Algorithms 1–3, the running-time statement of Theorem 3.40, and the algorithm-state Lemmas 3.36–3.38 are not posed.

A complete development needs basic facts about maxmin shares (monotonicity in the number of parts, removal of goods), Hall's theorem and Berge's augmenting-path characterization for bipartite matchings, and the exchange arguments for MCMWMs. The matching and maxmin-share lemmas are reusable beyond this mission. Proofs of any milestone, and of auxiliary facts about mms, are welcome.

Selected references

M. Ghodsi, M. T. Hajiaghayi, M. Seddighin, S. Seddighin, H. Yami, Fair Allocation of Indivisible Goods: Improvement and Generalization, arXiv:1704.00222v3, 2017; Mathematics of Operations Research, 2021. https://arxiv.org/abs/1704.00222
A. D. Procaccia, J. Wang, Fair enough: guaranteeing approximate maximin shares, ACM EC 2014. https://doi.org/10.1145/2600057.2602835
D. Kurokawa, A. D. Procaccia, J. Wang, Fair enough: guaranteeing approximate maximin shares, J. ACM 65(2), 2018. https://doi.org/10.1145/3140756
G. Amanatidis, E. Markakis, A. Nikzad, A. Saberi, Approximation algorithms for computing maximin share allocations, ICALP 2015. https://doi.org/10.1007/978-3-662-47672-7_4
E. Budish, The combinatorial assignment problem: approximate competitive equilibrium from equal incomes, J. Political Economy 119(6), 2011. https://doi.org/10.1086/664613
U. Feige, A. Sapir, L. Tauber, A tight negative example for MMS fair allocations, WINE 2021. https://arxiv.org/abs/2104.04977

18 thms3 active usersReviewed

Completed

Operations Research Probability Reinforcement Learning+1·Captain: mikedeng1

Markovian Interference in Experiments: The Differences-In-Q’s Estimator Has Bias Second Order in the Impact of the InterventionResearch Paper

Motivation

An intervention inside a continuing system can change what happens after the moment at which it is assigned. In a search service, for example, an action shown now can alter the system state that later users encounter. A simple randomized experiment therefore mixes two effects: the immediate reward of treatment and the change in the distribution of future states. Farias, Li, Peng and Zheng model this setting as a finite Markov decision process and study how to estimate the long-run effect of always using the intervention from data collected while treatment is randomized Farias et al., 2022.

The paper calls the difference between treatment and control averages the Naive estimator. It can be biased at first order in the intervention's effect on transitions, because both averages use the state distribution generated by the randomized experiment. The differences-in-Q estimator uses state-action values instead of immediate rewards. Theorem 1 asserts that its population bias is at most second order in that transition effect under a geometric mixing assumption Farias et al., 2022, Theorem 1.

Setting

Let $S$ be a finite state space. At each time, the system takes one of two actions: $0$ is control and $1$ is intervention. An action $a$ at state $s$ earns a real reward $r(s,a)$ and moves to the next state according to the row $P_a(s,\cdot)$ of a stochastic matrix $P_a$ . The control policy always selects $0$ ; the intervention policy always selects $1$ . The experiment policy selects each action with probability one half independently at each decision, so its transition matrix and expected reward vector are

P_{1/2}=\tfrac12(P_0+P_1),\qquad r_{1/2}=\tfrac12(r_0+r_1).

Write $\rho_0$ , $\rho_1$ and $\rho_{1/2}$ for stationary probability distributions of these three matrices. The average treatment effect is the difference between the long-run average rewards under always intervening and always controlling:

\mathrm{ATE}=\rho_1^{\top}r_1-\rho_0^{\top}r_0.

For the experiment policy, $Q_{1/2}(s,a)$ is the expected excess reward when action $a$ is taken first at state $s$ and the experiment policy is followed thereafter. Excess means reward relative to the experiment's stationary average reward $\rho_{1/2}^{\top}r_{1/2}$ . The idealized differences-in-Q value is

D=\sum_{s\in S}\rho_{1/2}(s)\bigl(Q_{1/2}(s,1)-Q_{1/2}(s,0)\bigr).

This is the population quantity whose bias Theorem 1 bounds. It is distinct from the finite-sample estimator calculated from a trajectory Farias et al., 2022, §3.1–3.2.

The mixing condition, Assumption 1, says that for every state $s$ and time $k\ge0$ , the total-variation distance between the $k$ -step experiment law and its stationary law is at most $C\lambda^k$ . The intervention impact is measured by a second total-variation bound, $d_{\mathrm{TV}}(P_1(s,\cdot),P_0(s,\cdot))\le\delta$ for every $s$ Farias et al., 2022, Assumption 1 and Theorem 1.

Formalization targets

Second-order population bias

The goal is Theorem 1. With $r_{\max}=\max_{s,a}|r(s,a)|$ , it asks for one polynomial $q$ , valid uniformly over all finite models and all admissible $C$ , $\lambda$ and $\delta$ , such that

|\mathrm{ATE}-D|\le q(\log C)\left(\frac1{1-\lambda}\right)^2r_{\max}\delta^2.

This formalizes the paper's statement that the unspecified constant depends polynomially on $\log C$ . The polynomial is quantified before the state space and the model, so its coefficients cannot be chosen from a particular example.

Source milestones

Five subtargets record the paper's route to this statement: Lemma 1's stationary-distribution perturbation identity; the corrected norm bound of Appendix F, Lemma 2; the corrected average-treatment-effect expansion in Eq. (6); the identification of the experiment's relative value with a group-inverse expression; and the identity that makes $D$ the first-order truncation Farias et al., 2022, pp. 13–15, 41. The goal and these milestones concern the idealized population estimator. Asymptotic normality and finite-sample estimation from Theorem 2 are outside this mission.

Significance

The result quantifies what the DQ adjustment buys in a dynamic experiment. When action-dependent transitions differ by at most $\delta$ in total variation, the population bias scales as $\delta^2$ , with an explicit dependence on the experiment chain's mixing rate and the reward bound. This provides a statement against which variants of the estimator and sharper constants can be compared Farias et al., 2022, Theorem 1.

The theorem is proved in the cited paper; the task here is to give its claim and the supporting identities machine-checkable proofs. The finite-chain definitions, perturbation identity and group-inverse bound can be reused in other average-reward Markov-chain arguments. No machine-checked proof of this theorem or these milestones was found in the local Prove2Me catalog search for this mission.

Difficulty

The immediate-reward difference averages under $\rho_{1/2}$ , whereas the treatment effect compares rewards under $\rho_1$ and $\rho_0$ . Replacing both stationary laws by $\rho_{1/2}$ therefore loses a term of order $\delta$ in general. The relative-value and Q-function expressions account for that term, but their definitions involve infinite excess-reward series. A formal proof must establish their convergence from mixing and reconcile them with the matrix group inverse. It must also control the norm of that inverse with the paper's precise row norm; using a generic matrix norm would change the claim.

Formalization scope

The state type is finite, actions are Fin 2, and reward vectors take real values. The matrices $P_0$ and $P_1$ are row stochastic. Primitivity represents the §2 standing ergodicity convention for the control and intervention policies. A stationary distribution is a nonnegative vector summing to one, so an empty state space cannot satisfy the theorem's hypotheses. Total variation is half the rowwise $\ell_1$ distance. The paper's $\|M\|_{1,\infty}$ is the maximum absolute row sum, and $\mathbf1\rho^{\top}$ is a rank-one matrix. The group inverse is represented by $(I-P+\mathbf1\rho^{\top})^{-1}-\mathbf1\rho^{\top}$ , used under hypotheses making the inverse valid Farias et al., 2022, Appendix A.

The relative value $V_{1/2}$ and action value $Q_{1/2}$ are sums of expected excess rewards, matching the reading of the paper's expectation formulas used in §3.3. They are not defined by the group inverse: the equivalence is a milestone. The idealized DQ value averages their action difference under $\rho_{1/2}$ ; the ATE uses the stationary-distribution form stated on p. 13. The goal assumes $0<\lambda<1$ , as required by the mixing expression and the denominator. Its polynomial constant is uniform over all instances. These choices exclude an instance-dependent constant or a definition that builds the desired equality into $V$ .

The Appendix F version of Lemma 2 is corrected with $C\ge1$ : without it, the one-state case permits a negative stated upper bound. Its premise bounds the maximum row norm. The p. 14 total-variation version omits the factor of two needed to convert to that norm. Accordingly, the remainder inequality and Eq. (6) milestones use the corrected Appendix F premise; their verbatim fields preserve what the paper prints Farias et al., 2022, pp. 14, 41. Contributions that establish these identities and bounds under the stated hypotheses, including reusable finite-chain matrix results and summability facts, are within scope.

Selected references

V. F. Farias, A. A. Li, T. Peng and A. Zheng, Markovian Interference in Experiments, arXiv preprint arXiv:2206.02371v2, 2022. Preprint.

8 thms3 active usersReviewed