All missions

Motivation

The trade-off capacity region of a quantum channel characterizes the optimal net rates at which a sender can communicate classical, quantum, and entangled bits to a receiver by exploiting many independent uses of the channel, along with the help of the same resources. Similarly, one can consider a trade-off capacity region when the noiseless resources are public, private, and secret key bits. In [Phys. Rev. Lett. 108, 140501 (2012)], we identified these trade-off rate regions for the pure-loss bosonic channel and proved that they are optimal provided that a longstanding minimum output entropy conjecture is true. Additionally, we showed that the performance gains of a trade-off coding strategy when compared to a time-sharing strategy can be quite significant. In the present paper, we provide detailed derivations of the results announced there, and we extend the application of these ideas to thermalizing and amplifying bosonic channels. We also derive a "rule of thumb" for trade-off coding, which determines how to allocate photons in a coding strategy if a large mean photon number is available at the channel input. Our results on the amplifying bosonic channel also apply to the "Unruh channel" considered in the context of relativistic quantum information theory.

This mission is the statement-level formalization of Quantum trade-off coding for bosonic communication (arXiv:1105.0119v4). 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 Thermal entropy: convergent power series (Lemma 4: thermal entropy power series, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

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

• Theorem 3 / (1), (28)–(30): pure-loss quantum dynamic achievability: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• Proposition 1: regularized quantum dynamic formula (background reformulation): Canonical interpretation and full domain of unrestricted infinite-dimensional entropy differences (source-ambiguity)
• Proposition 2: degradable private dynamic formula (background reformulation): Canonical interpretation and full domain of unrestricted infinite-dimensional entropy differences (source-ambiguity)
• Theorem 7 / (2), (48)–(50): pure-loss private dynamic achievability: Full-Fock forward public/private/key consuming and generating block protocols, joint recovery/security, and independent asymptotic signed (R,P,S) region (hard)
• Theorem 8: unconditional entanglement-assisted quantum slice: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• Theorem 9: thermal-noise quantum dynamic achievability: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• Theorem 10: thermal-noise private dynamic achievability: Full-Fock forward public/private/key consuming and generating block protocols, joint recovery/security, and independent asymptotic signed (R,P,S) region (hard)
• Theorem 11: amplifier quantum dynamic achievability: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• Theorem 12: amplifier private dynamic achievability: Full-Fock forward public/private/key consuming and generating block protocols, joint recovery/security, and independent asymptotic signed (R,P,S) region (hard)
• §III B, (40)–(41): pure-loss classical–quantum achievable slice: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• §III B, (42)–(43): pure-loss assisted/unassisted classical achievable slice: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• §III F, (58)–(59): public/private and public/key achievable slices: Full-Fock forward public/private/key consuming and generating block protocols, joint recovery/security, and independent asymptotic signed (R,P,S) region (hard)
• §III G: conditional full quantum dynamic capacity: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• §III G.1: conditional CE and CQ capacity slices: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• §III H, (77)–(79): conditional full private dynamic capacity: Full-Fock forward public/private/key consuming and generating block protocols, joint recovery/security, and independent asymptotic signed (R,P,S) region (hard)
• §IV A, (81)–(82) and CE display: thermal-noise achievable slices: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• §VI / Figure 7: mean-photon encoding versus single-excitation Unruh encoding: Physical two-use full-Fock vacuum amplifier precomposed with the dual-rail isometry, and both of its operational CQ/CE slices (hard)

Selected references

• Quantum trade-off coding for bosonic communication, arXiv:1105.0119v4, https://arxiv.org/abs/1105.0119v4

Motivation

We present an efficient family of quantum circuits for a fundamental primitive in quantum information theory, the Schur transform. The Schur transform on n d-dimensional quantum systems is a transform between a standard computational basis to a labelling related to the representation theory of the symmetric and unitary groups. If we desire to implement the Schur transform to an accuracy of epsilon, then our circuit construction uses a number of gates which is polynomial in n, d and log(1/epsilon). The important insights we use to perform this construction are the selection of the appropriate subgroup adapted basis and the Wigner-Eckart theorem. Our efficient circuit construction renders numerous protocols in quantum information theory computationally tractable and is an important new efficient quantum circuit family which goes significantly beyond the standard paradigm of the quantum Fourier transform.

This mission is the statement-level formalization of The Quantum Schur Transform: I. Efficient Qudit Circuits (arXiv:quant-ph/0601001v1). 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 Finite Gelfand–Zetlin labels fit in binary registers (III B: finite GZ labels and binary storage, PDF p. 11). 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

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

• Abstract/I/V C: efficient qudit Schur transform: A phase-compatible GZ/YY Schur analysis map and a clean, uniform qubit compiler with charged reversible classical work. (hard)
• III B, Eq.(29): reversible YY path compression: A bit-costed clean reversible rank/unrank program for valid one-box YY paths, implementing Eq.(29). (hard)
• IV B: coherent Schur cascade and composable cost: A constructed physical-space-to-GZ/YY cascade and row-label reversible schedule, tied to local CG maps. (hard)
• V opening: direct synthesis for fixed d: A fixed-d all-label GZ CG target with a uniform circuit-construction program and controlled-label synthesis costs. (hard)
• V B, Eqs.(46)–(54), Figs.4–5: dimension-reducing CG factorization: Compatible subgroup branching coordinates and total padded reduced-Wigner blocks controlled on the retained lower output. (hard)
• V C: efficient coherent reduced Wigner synthesis: An independently defined controlled reduced-Wigner target and an executable clean synthesis of it with numerical-error accounting. (hard)
• V C, Algorithm: Clebsch–Gordan transform: A source-compatible finite GZ one-box CG analysis map, clean recursive circuit interpreter and uniform d^3 polylog cost contract. (hard)
• III B: unfulfilled optimal-width GZ compression promise: A specified optimal-width GZ rank/inverse algorithm and a pinned meaning of efficient. (source-ambiguity)

Selected references

• The Quantum Schur Transform: I. Efficient Qudit Circuits, arXiv:quant-ph/0601001v1, https://arxiv.org/abs/quant-ph/0601001v1

Motivation

Machine-learned models of molecular energies and properties are trained on the output of quantum-chemistry calculations, and a common way to make them data-efficient is to build the physical symmetries of the problem into the architecture. When the input is not a point cloud but a set of matrices expressed in an atomic-orbital basis (Fock, density, overlap and Hamiltonian matrices from a cheap mean-field calculation), the relevant symmetry is the freedom to rotate the orbital basis of each atom independently: a rotation of the molecule, or any other unitary change of the local frames, changes every matrix element but not the physics.

Qiao, Christensen, Welborn, Manby, Anandkumar and Miller (arXiv:2105.14655v4, published in PNAS 2022) introduce UNiTE (Unitary N-body Tensor Equivariant network), the architecture behind OrbNet-Equi. They state as eq. (4), p. 3, that the network must satisfy $R\cdot F(T[\Psi_0])\equiv F(R\cdot T[\Psi_0])$ for every isometric basis rotation $R$, and prove this property in Appendix S2.6 (pp. 26–28) for a generalized version of the network: tensors of any order $N$, complex scalars, and an arbitrary unitary change of basis on each atom. The empirical results of the paper (QM9, MD17, GMTKN55) rest on this design principle, but the mathematical content of the paper is the equivariance proof.

Setting

There are $d$ atoms $u$. Atom $u$ carries a finite basis $\{e_{u;v}\}_{v\in\iota_u}$, and the concatenated basis is the set of pairs $(u,v)$. An N-body tensor of order $N=n+1$ is a function $T$ of $N$ concatenated indices; its sub-tensor $T_{\vec u}$ at $\vec u=(u_1,\dots,u_N)$ collects the entries whose $j$-th index lies in atom $u_j$.

A group $K$ (the paper's $\mathrm U(n)$; $\mathrm O(3)$ in the experiments) acts through unitary representations $\pi^1_u:K\to\mathrm U(\iota_u)$, and each atom has a subgroup $G_u\le K$. An element $g=(g_u)_u$ with $g_u\in G_u$ acts on tensors by the local action (S26):

$$g\cdot T_{\vec u}=(\pi^1(g_{u_1})\otimes\pi^1(g_{u_2})\otimes\cdots\otimes\pi^1(g_{u_N}))\,T_{\vec u}.$$

The network's hidden features $h_u$ assign to each label $L$ of a unitary representation $U^L:K\to\mathrm U(\mathbb V^L)$ and each channel $c$ a vector $h_{u,L,c}\in\mathbb V^L$; $g$ acts by $h_{u,L,c}\mapsto U^L_{g_u}h_{u,L,c}$. Matching matrices $(D_u)^{L,k,M}_v=\langle e_{u;v},\pi_{u;L,k,M}\rangle$ relate the atomic basis to a basis adapted to the decomposition $V_u\simeq\bigoplus_L(\mathbb V^L)^{\oplus K_L}$.

The UNiTE network $F$ (Methods 1.1; Appendix S2.5) consists of:

• a diagonal reduction $\psi_u$ turning the diagonal block $T_u$ into the initial features $h^0_u$;
• $t_1$ full steps, each made of a block convolution (S36), message passing (S37) with scalar attention weights $\alpha$, a reverse matching layer (S45) and a point-wise interaction $\phi$ (S40)–(S42) built from EvNorm (S39) and Clebsch–Gordan-type coefficients $C$;
• then $t_2$ point-wise interaction steps.

Formalization targets

Goal: G-equivariance of UNiTE (S2.6, p. 26)

Under the hypotheses the paper's proof uses — compatibility (S35) of the matching matrices, the Clebsch–Gordan property (S33) of $C$, equivariance (S32) of the diagonal reduction, invariance $g\cdot\alpha=\alpha$ of the attention weights, and positivity of the EvNorm constants — for every $g\in\prod_u G_u$, tensor $T$ and atom $u$,

$$F(g\cdot T)_u=U(g_u)\cdot F(T)_u .$$

Milestones

The proof in S2.6 rests on three results of S2.4 and four labelled sub-proofs:

• Theorem S1 (p. 24): a tensor product of irreducible unitary representations decomposes into irreducibles, with $\sum_L\mu(L)\dim\mathbb V^L=\prod_j\dim\mathbb V^{L_j}$ (S29)–(S30);
• Corollary S2 (p. 24): an invertible equivariant linear map $\psi:V_u^{\otimes N}\to\bigoplus_L(\mathbb V^L)^{\oplus\mu(L;V_u)}$;
• Corollary S3 (p. 24): an injective equivariant reduction $\psi(T)_{\nu,L,M}=\sum_{\vec v}T(\vec v)Q^{\vec v}_{\nu,L,M}$ with $\sum_Ln_L\le\dim(V_u)^N$;
• the four building-block equivariances of S2.6, for the block convolution, message passing, EvNorm and the point-wise interaction.

Significance

The theorem is what justifies feeding UNiTE features in arbitrary local frames: the predicted invariant quantities (energies) do not depend on the choice of atomic-orbital phases or orientations. The vector-valued outputs, such as dipole moments, then transform correctly. Without it, the model would have to learn the symmetry from data or from augmentation. The same argument applies to other architectures acting on matrices in local bases, for example models of Hamiltonian or density matrices.

The result is proved in the paper, with a proof written at the level of index manipulations. To our knowledge it has no machine-checked proof. Formalizing it pins down exactly which hypotheses each layer needs: (S35) on the matching matrices, the complex conjugate in (S36), the intertwining form of (S33), and invariance of the attention weights. It also yields a reusable library of statements about tensor-product and block-diagonal actions of unitary representations. Theorem S1 for an arbitrary group with a complete catalogue of irreducibles is a statement of independent interest: finite-dimensional unitary representations are completely reducible, which Mathlib does not yet provide outside finite groups.

Difficulty

No single step is deep; the difficulty is bookkeeping across dependent index types. The local action is block-diagonal over atoms, so cross-atom terms must be shown to vanish. Sub-tensor indices are dependent on the atom sequence $\vec u$. The block convolution's cancellation $\sum_v\pi^1_{vv'}\overline{\pi^1_{vv''}}=\delta_{v'v''}$ uses unitarity and the conjugate. The reverse matching layer needs the adjoint form of (S35), which uses that $G_u$ is a subgroup (closed under inverses). The point-wise block reindexes a double sum through a Kronecker product. The full network is a two-phase recursion whose attention weights depend on the current features, so the induction must carry the equivariance of every intermediate feature. Theorem S1 needs complete reducibility of a finite-dimensional unitary representation of an arbitrary group, together with the identification of each irreducible summand with a catalogue member.

A tempting shortcut, assuming each layer equivariant and composing, proves nothing about UNiTE: the content is that these specific layers are equivariant under these specific hypotheses.

Formalization scope

All scalars are complex; the paper's real (orthogonal) case is the special case of real unitary matrices. $\mathrm U(n)$ is replaced by an abstract group $K$ ([Group K]), representations are homomorphisms K →* Matrix.unitaryGroup ι ℂ, and the catalogue of irreducibles of $\mathrm U(n)$ is a family $U^L$ with the hypothesis CatalogComplete (every irreducible unitary representation is equivalent to some $U^L$), the formal reading of the paper's "we have abstracted the labelling details … into the index L". The subgroups $G_u$ are S u : Subgroup K, and every hypothesis is assumed only for $k\in G_u$.

Committed conventions:

• the tensor has order $N=n+1$ over the concatenated basis Σ u, ι u;
• every label has the same number $n_{\max}$ of channels, as (S41) requires;
• the matching weights use the main-text shapes (16) and (28), with a multiplicity index for the copies of $\mathbb V^L$ in $V_u$; they may depend on atom and step;
• the multilayer perceptrons are arbitrary functions of the invariant features, and the EvNorm statistics $\mu,\sigma$ are fixed parameters;
• (S33) is assumed in intertwining form $C(U^{L_1}\otimes U^{L_2})=U^LC$, which follows from the printed form for co-isometric $C$;
• the diagonal reduction $\psi_u$ is any linear map satisfying (S32), and the attention weights are any functions of the step's inputs satisfying $g\cdot\alpha=\alpha$; the paper's concrete attention (18)–(21) is not instantiated;
• only part (a) of the group $G$ of S2.2 (local unitaries) is formalized; permutations (b) and translations (c) leave the symmetric, translation-invariant input unchanged and are trivial.

Trivializing formalizations are ruled out. The layers are defined concretely, not replaced by maps assumed equivariant. The action is local, one unitary per atom, not one global unitary. The complex conjugate in (S36) is kept. Irreducibility of the catalogue and its completeness are both stated in Theorem S1 and the corollaries.

The development needs one definitions module (OrbNetEqui.Equivariance.Basic) and Mathlib's matrices, unitary groups, block-diagonal and Kronecker matrices. Contributions are welcome on every milestone; the building-block lemmas (block-diagonal and Kronecker actions of unitary matrices, unitary invariance of the regularized norm) and complete reducibility of finite-dimensional unitary representations are reusable beyond this mission.

Selected references

• Z. Qiao, A. S. Christensen, M. Welborn, F. R. Manby, A. Anandkumar, T. F. Miller III, Informing Geometric Deep Learning with Electronic Interactions to Accelerate Quantum Chemistry, Proc. Natl. Acad. Sci. USA 119 (2022); preprint arXiv:2105.14655v4. https://arxiv.org/abs/2105.14655
• Z. Qiao, M. Welborn, A. Anandkumar, F. R. Manby, T. F. Miller III, OrbNet: Deep learning for quantum chemistry using symmetry-adapted atomic-orbital features, J. Chem. Phys. 153, 124111 (2020). https://doi.org/10.1063/5.0021955
• N. Thomas et al., Tensor field networks: Rotation- and translation-equivariant neural networks for 3D point clouds, arXiv:1802.08219 (2018). https://arxiv.org/abs/1802.08219

Motivation

Forecast aggregation asks how to combine several experts' probability forecasts for the same event into one forecast. The two classical answers are linear pooling (average the probability vectors) and logarithmic pooling (average the log-probabilities and renormalize). Neither is justified by the way forecasts are usually evaluated: with a proper scoring rule, a payment rule under which reporting one's true belief maximizes expected reward. Neyman and Roughgarden (arXiv:2102.07081, Operations Research 2023) tie the aggregation method to the scoring rule. For each proper scoring rule $s$ they define quasi-arithmetic (QA) pooling with respect to $s$, which recovers linear pooling for the quadratic (Brier) score and logarithmic pooling for the log score, and they justify it in several ways. This mission formalizes the first justification, the paper's Theorem 4.1: QA pooling is the unique max-min optimal way for an agent paid by $s$ to aggregate the forecasts of experts it has sub-contracted.

The result places the paper in a line of work on scoring rules and convex analysis: the Savage representation of proper scoring rules as tangent planes of a convex function (Gneiting and Raftery, JASA 2007, Theorem 2), the link between entropy maximization and worst-case expected loss (Grünwald and Dawid, Annals of Statistics 2004), and the result of Chun and Shachter (UAI 2011) that, for $n=2$ outcomes, experts rewarded with the same scoring rule cannot be prevented from colluding profitably, by all reporting what Neyman and Roughgarden call the QA pool of their reports.

Setting

There are $n$ outcomes. A forecast is a point of the standard simplex $\Delta^n=\{p\in\mathbb R^n: p_j\ge 0,\ \sum_j p_j=1\}$, and $\delta_j$ is the vertex with a $1$ in coordinate $j$. A scoring rule is a function $s:\Delta^n\times[n]\to\mathbb R\cup\{-\infty\}$: an expert who reports $p$ receives $s(p;j)$ if outcome $j$ happens. The rule is proper if for every belief $p\in\Delta^n$ and every report $x\in\Delta^n$,

$$\sum_j p_j\,s(p;j)\ \ge\ \sum_j p_j\,s(x;j),$$

with equality only when $x=p$. It is regular if $s(p;j)$ is real except possibly $s(p;j)=-\infty$ when $p_j=0$. The forecast domain $\mathcal D$ is the set of $p$ at which every $s(p;j)$ is real, and the expected reward function is $G(p)=\sum_j p_j s(p;j)$. The paper assumes throughout that each $s(\cdot\,;j)$ and $G$ are continuous on $\Delta^n$.

An exposure function $g$ of $s$ satisfies the Savage representation

$$s(p;j)=G(p)+\langle g(p),\delta_j-p\rangle\qquad(p\in\mathcal D),$$

so $g(p)$ is a subgradient of $G$ at $p$. The Bregman divergence is $D_G(p\,\|\,q)=G(p)-G(q)-\langle g(q),p-q\rangle$.

Given forecasts $p_1,\dots,p_m\in\mathcal D$ and non-negative weights $w_1,\dots,w_m$ adding to $1$, the QA pool $p^*=\bigoplus_{\mathbf g}^{i=1..m}(p_i,w_i)$ is the unique $p^*\in\Delta^n$ at which $\sum_i w_i g(p_i)$ is a subgradient of $G$. An agent paid by $s$ who pays expert $i$ the amount $w_i s(p_i;j)$ and reports $q$ earns the profit

$$u(q;j)=s(q;j)-\sum_{i=1}^m w_i\,s(p_i;j).$$

Formalization targets

Goal: Theorem 4.1

For a regular, proper, continuous scoring rule $s$ with exposure function $g$, forecasts $p_i\in\mathcal D$ and weights $w_i\ge 0$ adding to $1$:

$$\min_j u(q;j)\ <\ \min_j u(p^*;j)\quad\text{for every } q\in\Delta^n,\ q\neq p^*;$$

the minimum $\min_j u(p^*;j)$ is attained at every $j$ with $p^*_j>0$; it is non-negative; and it is positive unless all reports with positive weight are equal. All four clauses are part of the goal.

Milestones

In the order the paper's proof uses them:

1. Proposition 3.1 (only-if direction, on $\mathcal D$): $G$ is convex on $\Delta^n$, $s(p;\cdot)$ is an exposure function, and every exposure function gives subgradients of $G$ on $\mathcal D$.
2. Proposition 3.4, first bullet: $D_G(x\,\|\,q)\ge 0$, with equality only when $x=q$, for $q\in\mathcal D$.
3. Well-definedness of the QA pool (§3.2): exactly one $p^*$ exists.
4. Claim 3.10: $p^*\in\mathcal D$.
5. KKT display in the proof of Theorem 4.1: $g(p^*)=\sum_i w_i g(p_i)+\lambda\mathbf 1_n+\mu$ with $\mu\ge 0$ and $\mu_j=0$ where $p^*_j>0$.
6. Profit identity: $u(p^*;j)=\sum_i w_i D_G(p^*\,\|\,p_i)+\mu_j$.

Significance

Theorem 4.1 says that an agent who sub-contracts experts and is paid by the same proper scoring rule can guarantee itself the largest worst-case profit, uniformly over outcomes, by reporting the QA pool, and that no other report achieves this guarantee. It gives an operational reason to aggregate with the method the scoring rule induces rather than a fixed one, and the strict positivity of the guarantee unless the weighted experts agree recovers, as a special case, the two-outcome collusion result of Chun and Shachter. The same objects (QA pools, exposure functions, Bregman divergences of expected rewards) carry the paper's later results on learning expert weights online and on axiomatizing QA pooling.

The theorem is proved in the paper; none of it is machine-checked. The mission produces a Lean statement and proof of Theorem 4.1 in full generality, including boundary pools where some outcome has probability zero, together with reusable statements about proper scoring rules on the simplex that are not in Mathlib: the Savage representation, non-negativity of the expected-reward Bregman divergence, existence and uniqueness of QA pools, and first-order optimality conditions on the simplex.

Difficulty

When $p^*$ lies in the interior of $\Delta^n$ and $G$ is differentiable, first-order optimality gives $g(p^*)=\sum_i w_i g(p_i)+\lambda\mathbf 1_n$ directly, and the rest is algebra. The difficulty is the boundary. The QA pool can have $p^*_j=0$ for some $j$; $G$ need not be differentiable there; and for rules such as the logarithmic score $s(p;j)=-\infty$ at points with $p_j=0$, so $G$'s subgradients may blow up near the boundary of $\Delta^n$. Showing that the pool avoids the points where $s$ is $-\infty$ (Claim 3.10) and that the multipliers $\lambda,\mu$ exist with the right sign there requires the continuity of $s$ into the extended reals, not just convexity of $G$. Uniqueness of the maximizer also needs the strictness built into properness.

Formalization scope

Forecasts are functions Fin n → ℝ, and $\Delta^n$ is Mathlib's stdSimplex ℝ (Fin n). The scoring rule takes values in EReal; only its values on $\Delta^n$ matter, the expected score uses $0\cdot(-\infty)=0$, and inner products are finite sums. Properness is strict, belief first and report second. $G$ is the real part of the expected score and is only evaluated on $\Delta^n$. Subgradients are taken relative to $\Delta^n$, the domain of $G$. The exposure function is real-valued and constrained by the Savage representation on $\mathcal D$ only; on $\mathcal D$ it is determined up to a multiple of $\mathbf 1_n$, and no statement depends on that choice. The Bregman divergence uses the exposure function in place of a gradient, since $G$ need not be differentiable at boundary forecasts. Continuity of $s(\cdot\,;j)$ is in the order topology of the extended reals. The QA pool is a predicate (a point of $\Delta^n$ with the subgradient property), and its existence and uniqueness is a separate milestone. The profit is $-\infty$ when the agent's report scores $-\infty$, and $\min_j$ is an infimum over the outcomes.

A trivial formalization is ruled out: the QA-pool hypothesis of the goal is satisfiable (milestone 3), exposure functions exist (milestone 1), and the continuity assumptions of the paper are kept as hypotheses rather than dropped.

Not formalized: the paper's results on learning expert weights (Theorems 5.1, 5.3), its axiomatizations (Theorems 6.6, C.7), which rules have convex exposure (Appendix D), the "if" direction of Proposition 3.1, and the second bullet of Proposition 3.4. Contributions of general lemmas on convex functions on the simplex (one-sided directional derivatives, first-order conditions at boundary minimizers) are welcome alongside the milestones.

Selected references

• E. Neyman and T. Roughgarden, From Proper Scoring Rules to Max-Min Optimal Forecast Aggregation, Operations Research, 2023; arXiv:2102.07081v2. https://arxiv.org/abs/2102.07081
• T. Gneiting and A. E. Raftery, Strictly Proper Scoring Rules, Prediction, and Estimation, Journal of the American Statistical Association 102(477), 2007. https://doi.org/10.1198/016214506000001437
• P. D. Grünwald and A. P. Dawid, Game Theory, Maximum Entropy, Minimum Discrepancy and Robust Bayesian Decision Theory, Annals of Statistics 32(4), 2004. https://doi.org/10.1214/009053604000000553
• S. Chun and R. D. Shachter, Strictly Proper Mechanisms with Cooperating Players, UAI 2011, pp. 125–134. https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=2168&proceeding_id=27
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, §5.5.3. https://doi.org/10.1017/CBO9780511804441

Motivation

Many large-population systems are modelled as aggregative games: each agent's cost depends on its own decision and on an average of everybody's decisions. Examples are electric-vehicle charging and demand response, where a household's cost depends on its own consumption profile and on the aggregate load through the electricity price, and congestion and routing, where a traveller's cost depends on the total flow on the links used. In these applications individual decisions are often non-convex: a charging profile may be on/off, a route is a discrete choice, an appliance runs in fixed blocks. Without convexity, the classical existence theorems for pure Nash equilibria (Rosen 1965, Debreu–Glicksberg–Fan) do not apply, and a pure Nash equilibrium may fail to exist.

The intuition that "non-convexity averages out when many small agents are aggregated" goes back to Starr's work on markets with non-convex preferences (1969), based on the Shapley–Folkman lemma. Liu, Oudjane and Wan (arXiv:2011.12604, Mathematics of Operations Research) make it quantitative for sum-aggregative games: they show that a non-convex aggregative game with $n$ players has an approximate pure Nash equilibrium whose error decays like $n^{-\gamma}$, and they construct it from an equilibrium of a convexified game.

Setting

There are $n$ players $N=\{1,\dots,n\}$. Player $i$ chooses an action $x_i$ in a compact, nonempty, possibly non-convex set $\mathcal X_i\subset\mathbb R^d$, of diameter at most $\Delta>0$. Write $\tilde{\mathcal X}_i=\operatorname{conv}\mathcal X_i$ for its convex hull. There are $q\times d$ matrices $A_1,\dots,A_n$ with spectral norm $\|A_j\|_2\le M$, $M>0$. The cost of player $i$ at a profile $x=(x_1,\dots,x_n)$ is

$$f_i(x_i,x_{-i})=\theta_i\Big(x_i,\ \frac1n\sum_{j\in N}A_jx_j\Big),$$

where $\theta_i$ is defined on $\mathcal X_i\times\Omega$ and $\Omega\subset\mathbb R^q$ is a neighbourhood of the set of aggregates $\frac1n\sum_jA_jy_j$ with $y_j\in\tilde{\mathcal X}_j$.

Assumption 1 requires that (1) $x_i\mapsto\theta_i(x_i,y)$ is lower semicontinuous on $\mathcal X_i$ for every $y\in\Omega$, and (2) $y\mapsto\theta_i(x_i,y)$ is $(H,\gamma)$-Hölder on $\Omega$ uniformly in $x_i\in\mathcal X_i$: $|\theta_i(x_i,y')-\theta_i(x_i,y)|\le H\|y'-y\|^\gamma$, with $H,\gamma>0$.

For $\epsilon\ge0$, an $\epsilon$-pure Nash equilibrium ($\epsilon$-PNE) is a feasible profile $x$ such that no player can lower its cost by more than $\epsilon$ through a unilateral deviation: $f_i(x_i,x_{-i})\le f_i(y_i,x_{-i})+\epsilon$ for all $i$ and $y_i\in\mathcal X_i$.

The convexified game $\tilde\Gamma$ has action sets $\tilde{\mathcal X}_i$ and costs

$$\tilde f_i(x_i,x_{-i})=\inf\Big\{\sum_{k=1}^{d+1}\alpha^kf_i(z^k,x_{-i})\ \Big|\ \alpha\in\mathcal S_d,\ z^k\in\mathcal X_i,\ x_i=\sum_k\alpha^kz^k\Big\},$$

with $\mathcal S_d$ the probability simplex in $\mathbb R^{d+1}$: $\tilde f_i(\cdot,x_{-i})$ is the convex envelope of $f_i(\cdot,x_{-i})$. A generator $Z(i,x)$ is the set of points $z^k$ carrying positive weight in a minimizer of this infimum. A point $\tilde x$ satisfies the $\eta$-stability condition with respect to generators $(Z(i,\tilde x))_i$ if $\tilde f_i(x_i,\tilde x_{-i})\le\tilde f_i(\tilde x_i,\tilde x_{-i})+\eta$ for all $i$ and $x_i\in Z(i,\tilde x)$.

Formalization targets

Goal: Proposition 2.4

Under Assumption 1, with

$$\epsilon=2H\Big(\frac{(\sqrt q+1)M\Delta}{n}\Big)^\gamma,$$

the non-convex game $\Gamma$ has an $\epsilon$-PNE. More precisely, if $\tilde x$ is a pure Nash equilibrium of $\tilde\Gamma$ and $Z(i,\tilde x)$ are arbitrary generators, every profile

$$x^*\in\operatorname*{arg\,min}_{x_i\in Z(i,\tilde x),\,i\in N}\Big\|\sum_iA_i\tilde x_i-\sum_iA_ix_i\Big\|^2$$

is an $\epsilon$-PNE of $\Gamma$. Both sentences are part of the goal.

Stronger: Theorem 2.7

If $\tilde x$ is only an $\epsilon$-PNE of $\tilde\Gamma$ and satisfies the $\eta$-stability condition with respect to a generator profile, the same disaggregation is an $\tilde\epsilon$-PNE of $\Gamma$ with $\tilde\epsilon=\epsilon+\eta+2H\big(\frac{(\sqrt q+1)M\Delta}{n}\big)^\gamma$.

Milestones

In attack order: Lemma 5.1 (a fixed point of the argmin map of a function continuous in $x$, jointly lower semicontinuous and convex in $y$); Theorem 5.3 (existence of a PNE in games with convex compact action sets, convex lower semicontinuous costs and uniform equicontinuity in the other players' actions); Lemma 5.5 (1)–(2), (3) and (4) (properties of the convex envelope $\tilde f_i$ and of generators); Proposition 2.3 (the convexified game has a PNE); the Shapley–Folkman lemma (Lemma 5.4, first bullet, already proved on the platform); Starr's bound (Lemma 5.4, second bullet); Lemma 5.6 (1) ($f_i=\tilde f_i$ at generator points); Theorem 2.7.

Significance

The result. Proposition 2.4 gives existence of approximate pure equilibria in a class of games where exact pure equilibria need not exist, with an explicit error bound that vanishes as the population grows, for fixed aggregate dimension $q$. It also says how to obtain one: solve the convexified game, which is a convex game with lower semicontinuous costs, and round its equilibrium to generator points. Theorem 2.7 makes the construction robust to approximate solutions of the convexified game, which is what an iterative algorithm delivers. The paper's later sections (a randomized disaggregation and an application to flexible electricity consumption) rest on these two statements.

Formalizing it. The results are proved in the paper; none of them is formalized. The Shapley–Folkman lemma itself is proved on the platform and is reused here. The mission adds a quantitative Starr bound in Euclidean norm, an existence theorem for pure equilibria under lower semicontinuity (an extension of Rosen's theorem that the authors prove themselves because they found no reference), the basic theory of the $(d+1)$-point convex envelope, and the disaggregation argument. Formalization also checks the paper's statements: the printed definition of a generator, read literally, makes Theorem 2.7 false (see Formalization scope).

Difficulty

The disaggregation step needs more than "average over many players". The convexified equilibrium gives each player a point $\tilde x_i$ in $\operatorname{conv}\mathcal X_i$, but the deviation analysis has to happen in the original game, at points of $\mathcal X_i$. Two facts must be combined: the generator points of a best response of $\tilde\Gamma$ are best responses of $\Gamma$ against the convexified profile, and a profile of generator points can be found whose aggregate is within $O(\sqrt q\,M\Delta/n)$ of the convexified aggregate. The first fails if a generator is allowed to contain points of zero weight. The second fails with the naive bound: picking arbitrary generator points for the at most $q$ exceptional players of the Shapley–Folkman lemma gives an error of order $q$, not $\sqrt q$; the bound $\sqrt q$ requires a choice that exploits Euclidean geometry.

On the existence side, Rosen's theorem does not apply to $\tilde\Gamma$: $\tilde f_i$ is convex and lower semicontinuous in the own action, but it need not be continuous even when $f_i$ is (the paper gives a three-dimensional example on p. 5).

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) and players are Fin n. A $q\times d$ matrix is a continuous linear map from $\mathbb R^d$ to $\mathbb R^q$; its operator norm is the spectral norm $\|A\|_2$ of the paper. Deviations $(y_i,x_{-i})$ are Function.update x i y, and $f_i(z^k,x_{-i})$ inside $\tilde f_i$ is evaluated at the profile in which player $i$ plays $z^k$, so the aggregate contains $A_iz^k$. One $\epsilon$-PNE predicate, parameterized by action sets and costs, serves both $\Gamma$ and $\tilde\Gamma$. Hölder powers are real powers, and $\gamma\le1$ is not assumed. $\Omega$ is a neighbourhood of the aggregate set of $\tilde{\mathcal X}$, encoded with nhdsSet. The infimum defining $\tilde f_i$ is a real infimum; at every profile of $\tilde{\mathcal X}$ its set is nonempty and bounded below, so Lean's default value for empty or unbounded sets is never reached.

Three readings differ from the printed text, and each is the one the paper's proofs use. (i) A generator is the set of components with positive weight, as in the paper's Lemma 5.7; keeping zero-weight components makes Lemma 5.6, Theorem 2.7 and Proposition 2.4 false (a two-player example with $d=q=1$ exists). (ii) Lemma 5.5 (2), printed "for all $x_i\in\mathcal X_i$", is stated on $\tilde{\mathcal X}_i$, as its proof and Definition 2.2 require. (iii) Action sets are assumed nonempty. Lemma 5.1 is stated in any finite-dimensional real normed space; the uniform equicontinuity of Theorem 5.3 measures closeness coordinatewise, an equivalent norm. Starr's bound is stated with any upper bound $D$ on the diameters, which is equivalent to the maximal diameter.

A trivializing formalization is ruled out: $\tilde f_i$ is an infimum over representations of the player's own action, not over all points, so equilibria of $\tilde\Gamma$ are not arbitrary profiles; a sorry-free sanity check confirms that the definitions are satisfiable and agree with $f_i$ on a singleton action set.

Out of scope: Theorem 3.3, Propositions 2.8, 3.2, 3.4, Lemmas 2.6, 3.1, 5.6 (2), 5.7, 5.8, the full stability condition, mixed strategies, and the numerical study of §4. Contributions welcome: proofs of the milestones, in particular a reusable Starr bound and a reusable existence theorem for lower semicontinuous convex games.

Selected references

• K. Liu, N. Oudjane, C. Wan, Approximate Nash equilibria in large nonconvex aggregative games, Mathematics of Operations Research; arXiv:2011.12604v3, 2022. https://arxiv.org/abs/2011.12604
• R. M. Starr, Quasi-equilibria in markets with non-convex preferences, Econometrica 37(1), 25–38, 1969. https://doi.org/10.2307/1909201
• J. B. Rosen, Existence and uniqueness of equilibrium points for concave n-person games, Econometrica 33(3), 520–534, 1965. https://doi.org/10.2307/1911749
• S. Kakutani, A generalization of Brouwer's fixed point theorem, Duke Mathematical Journal 8(3), 457–459, 1941. https://doi.org/10.1215/S0012-7094-41-00838-4
• J.-B. Hiriart-Urruty, C. Lemaréchal, Convex Analysis and Minimization Algorithms I, Springer, 1993. https://doi.org/10.1007/978-3-662-02796-7

Motivation

Fast-fashion chains and flash-sale sites rotate their assortments: a product is on display for a short window and is then replaced. Retailers that do this face a choice that a classical assortment model cannot express. They can show the whole catalog at once, or they can conceal part of it and reveal products one at a time. In the classical discrete-choice models, which include multinomial logit, nested logit and Markov chain choice, each consumer buys at most one product, so the order in which products are revealed is immaterial.

Ferreira and Goh (HBS Working Paper 17-041; published in Management Science, 2021, doi:10.1287/mnsc.2020.3610) let consumers buy several products. Each additional purchase is worth less to the consumer than the previous one. This diminishing marginal utility goes back to Marshall and appears in the satiation model of Baucells and Sarin (2007). With it, the order of revelation matters, and the paper asks whether concealment pays.

Setting

A retailer has $N$ products with nonnegative prices $p_1,\dots,p_N$. A consumer has a random valuation shock $X_i$ for each product $i$. The shocks are mutually independent, continuous and integrable random variables on a probability space $(\Omega,\mathbb P)$. The quantity $X_i-p_i$ is the price-adjusted valuation of product $i$. Buying a set $S$ of products gives the consumer the utility

$$u(S)=\sum_{j\in S}(X_j-p_j)+\sum_{j=0}^{|S|-1}v(j),$$

where the marginal utility $v:\mathbb N_0\to\mathbb R$ is nonnegative and decreasing.

• Fixed assortment. The retailer offers a subset $S$ of $M\le N$ products for the whole season. The consumer sees all realized shocks and buys a utility-maximizing set. Lemma 1 shows that she buys in an order $\sigma$ of decreasing price-adjusted valuation (Definition 1), so the retailer earns

$$R^f=\sum_{i=1}^{M}p_{\sigma(i)}\,\mathbb 1\{v(i-1)+X_{\sigma(i)}-p_{\sigma(i)}\ge 0\}.$$

• Sequential assortment. The retailer shows one product per period. A consumer who has already bought $k$ items buys the current product $i$ iff $v(k)+X_i-p_i\ge 0$. With $W_{i-1}$ purchases made before period $i$, the revenue is $R^s=\sum_i p_i\,\mathbb 1\{v(W_{i-1})+X_i-p_i\ge 0\}$. The quantity $R_k(n)$ is the revenue from the last $n$ products when the consumer enters them with $k$ purchases.
• Optimized strategies. $\mathbb E[R^f_*]$ is the largest expected fixed revenue over all subsets $S$, and $\mathbb E[R^s_*]$ the largest expected sequential revenue over all orders of all $N$ products. The value of concealment is $\mathrm{VoC}=\mathbb E[R^s_*]-\mathbb E[R^f_*]$.

In Lean a product is a pair (price, realized shock). seqRev v L k is the sequential revenue of a list L for a consumer starting with k purchases, fixedRev v L' is (4) along a list L', and ERsStar, ERfStar are the two optima.

Formalization targets

Goal: Theorem 1 (p. 15)

Let $S$ be an optimized fixed assortment, and let $R$ be the revenue of the sequential assortment showing the same products in decreasing order of prices. Then

$$\text{(a)}\quad R(\omega)\ \ge\ R^f_*(\omega)\ \text{ for every outcome }\omega,\qquad\text{(b)}\quad \mathbb E[R^s_*]\ \ge\ \mathbb E[R^f_*].$$

Part (b) fixes no constants and asserts only the sign of the value of concealment, which can be zero (Theorem 2 of the paper).

Milestones

1. Lemma 1 (p. 11): buying the products $\sigma(1),\dots,\sigma(D^f)$ maximizes $u$.
2. Lemma 2 (p. 13): $R_{k+1}(n)\le R_k(n)\le \rho^*_n+R_{k+1}(n)$, with $\rho^*_n$ the highest remaining price.
3. Lemma 4 (p. 38): if the first product has the highest price and $X_1-p_1\le X_2-p_2$, interchanging products 1 and 2 does not raise the revenue.
4. Proof of Theorem 1 (p. 39): in a Definition-1 order the sequential revenue equals $R^f$.
5. Theorem 1(a) for every fixed assortment: $R\ge R^f$ pathwise.
6. Remark 1 (p. 12): appending a product never lowers $R^s$.

Significance

The result. Theorem 1 says that concealment never hurts a retailer facing multi-purchase consumers with diminishing marginal utility. Part (a) also gives a concrete policy, independent of the shock distributions: take the optimal fixed assortment and reveal its products from the most to the least expensive. The paper reads the gain as structural: the retailer learns nothing from offering products sequentially, yet it still gains from them. The rest of the paper builds on it. Theorem 2 characterizes when the value of concealment is zero, Theorem 3 gives its asymptotics, and §6 measures the decreasing-price heuristic numerically.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The mission produces a reusable model of a multi-purchase consumer under fixed and sequential presentation, together with its basic monotonicity facts (Lemma 2, Remark 1). The goal is also stated pathwise, which is stronger than the paper's "with probability 1".

Difficulty

The obvious approach compares the two strategies product by product, and it fails. Under the fixed assortment the purchase decision for a product depends on its rank among the realized price-adjusted valuations. Under the sequential assortment it depends on the number of earlier purchases, which in turn depends on every earlier shock. Neither revenue is monotone in the order of presentation. Swapping two adjacent products can raise or lower the revenue, depending on the realization and on which of the two is more expensive. Lemma 4 identifies the one swap whose sign is controlled, and Lemma 2 bounds how far an extra purchase can shift the remaining revenue. The difficulty is to arrange swaps of this kind into a sorting of the decreasing-price sequence into a Definition-1 order, and to keep the bookkeeping exact when prices or valuations tie.

Formalization scope

• Products are pairs (price, realized shock), sequences are lists, and positions are 0-based: the paper's position $i$ with $v(i-1)$ is list position $i-1$.
• The marginal utility $v$ is taken directly, nonnegative and antitone, rather than through the concave $V$ of (2).
• Prices are nonnegative. The paper leaves this implicit, and Lemma 2's lower bound needs it.
• The purchase rule is $v(k)+X-p\ge 0$ everywhere, including $R_k(n)$, for which (7) prints $>0$. The two differ only on a null event for continuous shocks.
• All "with probability 1" statements are proved for every realization. The milestones are stated for arbitrary lists, with ties in prices and in valuations allowed.
• $R^f(S)$ uses the canonical Definition-1 order, with ties broken by smaller index. Every other order gives the same revenue off the null event of a tie.
• $\mathbb E[R^s_*]$ is a maximum over the orders of all $N$ products, and $\mathbb E[R^f_*]$ a maximum over all subsets, the empty set and strict subsets included. Both maxima range over finite sets, and the revenues are bounded and measurable, so the integrals are genuine.
• Independence, continuity and integrability of the shocks are the paper's standing assumptions and stay in the goal, although the inequality does not use them.

Trivializing encodings are ruled out: $R^f$ is the positional formula (4), not the sequential revenue in $\sigma$-order. Restricting $R^s_*$ to the $M$ products of the fixed assortment, or $R^f_*$ to the full set, would change the claim and is not done.

The development needs only finite sums, lists and permutations from Mathlib, plus Bochner integrals of bounded random variables. The list-level lemmas about seqRev (Lemmas 2 and 4, Remark 1) apply to any sequential-purchase model with diminishing marginal utility. Contributions are welcome on every milestone, and on general list-sorting lemmas that carry an interchange argument from adjacent swaps to a full permutation.

Not formalized here: Lemma 3 and Corollaries 1–2 (optimal sequences under hazard-rate and IFR conditions), Theorems 2–3, the forward-looking consumer model of §5, and the numerical study of §6.

Selected references

• K. J. Ferreira and J. Goh, Assortment Rotation and the Value of Concealment, Harvard Business School Working Paper 17-041 (2020 revision); Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3610
• M. Baucells and R. K. Sarin, Satiation in discounted utility, Operations Research 55(1), 2007. https://doi.org/10.1287/opre.1060.0322
• F. Caro and V. Martínez-de-Albéniz, Product and price competition with satiation effects, Management Science 58(7), 2012. https://doi.org/10.1287/mnsc.1110.1484
• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Pricing without knowing demand

A firm launching a new product (a drug, a software package, a digital download) must choose a price before it has data on its demand curve. Classical monopoly pricing needs the whole demand curve: the optimal price balances marginal revenue against marginal cost, and both depend on the curve's shape. Cohen, Perakis and Pindyck (Management Science; accepted version SSRN 2673810) ask how well a firm can do when it knows only two numbers: its constant marginal cost $c$ and the maximum price $P_m$, the price at which consumers stop buying. Their answer is a rule that needs nothing else: charge the price that would be optimal if demand were linear through $(0, P_m)$. They give closed-form performance guarantees for this rule under several demand families. The guarantee that holds for an entire nonparametric class is the one for concave inverse demand, and that is the subject of this mission.

The setting matters in practice when the firm need not plan output in advance (zero or near-zero marginal cost, no capacity decision): then the only decision is the price, and the slope of the demand curve, which determines how much will be sold, is immaterial for choosing it.

Setting

A market consists of

• a maximum price $P_m$ and a marginal cost $c$ with $0 \le c < P_m$;
• a saturation quantity $Q_{\max} > 0$: no more than $Q_{\max}$ units can be sold, however low the price;
• the actual inverse demand $P_A(Q)$, the price at which exactly $Q$ units are demanded, defined on $[0, Q_{\max}]$, with $P_A(0) = P_m$, non-increasing and continuous.

Selling $Q$ units at the market-clearing price earns the profit $\Pi(Q) = (P_A(Q) - c)\,Q$. A firm that knew $P_A$ would choose an optimal quantity $Q^{**}$ maximizing $\Pi$ on $[0, Q_{\max}]$, charge the optimal price $P^{**} = P_A(Q^{**})$, and earn $\Pi^{**} = \Pi(Q^{**})$.

The demand at price $p$ is $Q_A(p) = \sup\{Q \in [0, Q_{\max}] : P_A(Q) \ge p\}$, the quantity sold when the firm charges $p$.

If demand were linear, $P(Q) = P_m - bQ$ with $b > 0$, the profit $(P_m - bQ - c)Q$ would be maximized at $Q^*_L = (P_m - c)/2b$, at the price

$$P^* = \frac{P_m + c}{2},$$

which does not depend on $b$. This is the linear price. The linear pricing rule charges $P^*$ whatever the true demand is, and earns $\Pi^* = (P^* - c)\,Q_A(P^*)$.

In Lean these objects are Market, Market.Standing, profit, IsOptQty, linPrice, demandAt and linProfit in the namespace LinearPriceRule.Concave.

Formalization targets

Goal: Proposition 5 (p. 13)

If $P_A$ is concave on $[0, Q_{\max}]$, then an optimal quantity exists, $\Pi^* > 0$, and every optimal quantity satisfies

$$1 \le \frac{\Pi^{**}}{\Pi^*} \le 2, \qquad 1 \le \frac{P^{**}}{P^*} \le 2 .$$

Milestones

1. Eq. (1), §1.4, p. 4. Under linear inverse demand $P_m - bQ$, the profit is uniquely maximized at $Q^*_L = (P_m - c)/2b$, and the price there is $(P_m + c)/2$.
2. Theorem 1, concave case, p. 9. If $P_A$ is concave, every optimal price satisfies $P^{**} \ge P^*$.
3. Proof of Proposition 5, p. 26. $Q_A$ is non-increasing on $(-\infty, P_m]$, and $Q_A(P^{**}) = Q^{**}$, so $\Pi^{**} = (P^{**} - c)\,Q_A(P^{**})$.
4. Theorem 1, convex case, p. 9. If $P_A$ is convex and the optimum is interior ($Q^{**} < Q_{\max}$), then $P^{**} \le P^*$.
5. Remark after Proposition 5, p. 13. For a rectangular demand ($P_A \equiv P_m$ on $[0, Q_{\max}]$), $\Pi^{**}/\Pi^* = 2$, and $P^{**}/P^* = 2$ when $c = 0$.

Significance

Proposition 5 is a distribution-free guarantee: across the whole class of concave inverse demands, which contains linear, concave quadratic and many other shapes, a rule that uses only $P_m$ and $c$ loses at most half of the optimal profit. The rectangle shows that the factor $2$ cannot be improved within the class. Theorem 1 says in which direction the rule errs, under-pricing for concave and over-pricing for convex inverse demand, so a firm with qualitative information about curvature knows which way to adjust. The paper's parametric results (quadratic, monomial, semi-log, log-log demand) and its welfare comparisons are built on the same model.

The results are proved in the paper. As far as is known, none of them has been formalized. This mission provides a machine-checked model of a monopolist facing an unknown inverse demand on a bounded quantity interval, which other robust-pricing statements can reuse, together with the paper's argument for the concave case, carried out without the differentiability its Taylor-expansion proof of Theorem 1 assumes.

Difficulty

The paper's proof of Theorem 1 writes $P_A(Q) = P_m - bQ + f(Q)$, equates marginal revenue with marginal cost, and applies a second-order Taylor expansion. None of this is available for the statement as formalized: $P_A$ is only continuous and concave, it may have kinks (the rectangle has one at $Q_{\max}$), and the optimum may sit at the corner $Q^{**} = Q_{\max}$, where the first-order condition fails. A proof must compare the profit at $Q^{**}$ with profits at other quantities using only the defining inequality of concavity.

The second subtlety is the demand $Q_A$, a supremum over a set. Identifying $\Pi^*$ with the profit of an actual quantity, and $Q_A(P^{**})$ with $Q^{**}$, needs continuity and the optimality of $Q^{**}$: a flat stretch of $P_A$ at the optimal price would otherwise let $Q_A(P^{**})$ exceed $Q^{**}$.

The convex half of Theorem 1 is false at a corner optimum. For $P_A(Q) = 5 - Q/10$ on $[0, 1]$ and $c = 1$, the optimum is $Q^{**} = 1$ with $P^{**} = 4.9 > P^* = 3$. That milestone therefore assumes $Q^{**} < Q_{\max}$.

Formalization scope

• $P_A$ is a function $\mathbb R \to \mathbb R$. Only its values on $[0, Q_{\max}]$ matter: monotonicity, continuity, concavity and convexity are assumed on $[0, Q_{\max}]$, and optimality and $Q_A$ range over $[0, Q_{\max}]$. Concavity on all of $[0, \infty)$ together with nonnegativity would force $P_A$ to be constant, so it is not used.
• The standing assumptions are $0 \le c < P_m$, $0 < Q_{\max}$, $P_A(0) = P_m$, and $P_A$ non-increasing and continuous on $[0, Q_{\max}]$. Nonnegativity of $P_A$ is not assumed. Continuity guarantees that an optimum exists and that $Q_A(P^*)$ is actually sold at $P^*$.
• "Concave demand curve" is read as concavity of the inverse demand $P_A$ in $Q$. Proposition 5's proof invokes Theorem 1, which is about $P_A$.
• The firm optimizes over quantities, and $P^{**}$ is read off as $P_A(Q^{**})$. All bounds are stated for every optimal quantity, and existence is a separate clause.
• $Q_A(p)$ is the supremum of $\{Q \in [0, Q_{\max}] : P_A(Q) \ge p\}$, and $\Pi^* = (P^* - c)\,Q_A(P^*)$ is the profit of charging $P^*$, not the profit at some quantity.
• Ratios are real divisions, and the goal asserts $\Pi^* > 0$. Without the clauses "an optimum exists" and "$\Pi^* > 0$", the goal could hold vacuously or through the convention $x/0 = 0$. These clauses are part of the statement and rule out that trivialization.
• No differentiability is assumed anywhere.

Only Mathlib's convexity and order-theoretic infrastructure (ConcaveOn, ConvexOn, AntitoneOn, sSup on ℝ, the extreme value theorem on compact intervals) is needed. Proofs of the milestones are welcome in any order. The parametric Propositions 1–4, the welfare results (Propositions 6–7) and the uncertain-$P_m$ analysis of §3 are outside this mission.

Selected references

• M. C. Cohen, G. Perakis, R. S. Pindyck, A Simple Rule for Pricing with Limited Knowledge of Demand, Management Science. https://doi.org/10.1287/mnsc.2020.3602 — accepted version: SSRN 2673810, https://ssrn.com/abstract=2673810 (the version cited by page in this mission).

Motivation

Assortment optimization asks a retailer which subset of products to offer so as to maximize expected revenue, given a model of how customers choose among what is offered. A widely used class of choice models in operations management describes customers by ranked preference lists: each customer type buys the highest-ranked product on offer, or nothing (Farias, Jagabathula & Shah 2013). These nonparametric models fit sales data well, but optimizing over them is hard: even when all customer types share one ranking and differ only in which products they are willing to consider, the problem is NP-hard to approximate within a factor $O(N^{1-\epsilon})$ (Aouad, Farias, Levi & Segev 2018).

Aouad, Farias and Levi (Management Science 2021) study consider-then-choose models, a behavioural refinement from marketing in which a customer first screens products into a consideration set and then picks her favourite among the offered products in that set. Their main algorithmic device is a dynamic program whose number of subproblems they bound by structural properties of the consideration sets. This mission formalizes the first and most general such bound, for a single common ranking, together with the lemmas it rests on. Earlier exact algorithms for special cases of ranking-based models are due to Honhon, Jonnalagedda & Pan (2012).

Setting

There are $N$ products $[N]=\{1,\dots,N\}$ with prices $P_i$, and $K$ customer types $[K]$. Type $j$ has a consideration set $C_j\subseteq[N]$ and occurs with probability $\lambda_j$, where $(\lambda_1,\dots,\lambda_K)$ is a probability vector. All types rank products by the same permutation, and products are numbered in that order: product $1$ is the most preferred. If assortment $A\subseteq[N]$ is offered, type $j$ buys the smallest-index product of $A\cap C_j$, giving revenue

$$\mathrm{Rev}(j,A)=P_{\min(A\cap C_j)}\quad\text{if }A\cap C_j\neq\emptyset,\qquad \mathrm{Rev}(j,A)=0\text{ otherwise}.$$

For $S\subseteq[N]$ and $T\subseteq[K]$ the subproblem value is

$$J(S,T)=\max_{A\subseteq S}\ \sum_{j\in T}\lambda_j\,\mathrm{Rev}(j,A),$$

and $J([N],[K])$ is the original problem. The bipartite graph $G$ has the products and types as vertices and an edge $\{i,j\}$ when $i\in C_j$; $G[S,T]$ is its subgraph induced on $S\cup T$, and $(S',T')$ is a connected component of $G[S,T]$ when $S'\cup T'$ induces a connected subgraph and no edge of $G[S,T]$ leaves it. For a product $i$, $T(i)=\{j\in T:i\in C_j\}$.

The dynamic program processes products in preference order. Its state space $\mathcal S$ is generated as follows: the components of $G[[N],[K]]$ are states; from a state $(S,T)$ with $i=\min(S)$, the components of $G[S\setminus\{i\},T\setminus T(i)]$ (product $i$ stocked) and of $G[S\setminus\{i\},T]$ (product $i$ not stocked) are states. Only components with at least one product and at least one type are states. Finally,

$$\Phi(S,T)=[\min(S)]\cap\bigcup_{u\in T}C_u,\qquad [\min(S)]=\{1,\dots,\min(S)\}.$$

Formalization targets

Goal: Theorem 1 (p. 14)

$$|\mathcal S|\ \le\ \min\big(2^N,\ N\cdot 2^K\big),$$

together with its state-space consequence: if $K\le c\log_2 N$ then $|\mathcal S|\le N^{c+1}$. The bound holds for every family of consideration sets; prices and type probabilities do not enter.

Milestones, in the paper's order

1. Lemma 1 (p. 12): $J(S,T)=\sum_{u=1}^{r}J(S_u,T_u)$ over the connected components $(S_u,T_u)$ of $G[S,T]$.
2. §3, Eq. (1) (p. 13): for connected $G[S,T]$ and $i=\min(S)$,

$$J(S,T)=\max\Big[P_i\sum_{j\in T(i)}\lambda_j+\sum_{u}J(S^+_u,T^+_u),\ \sum_{u}J(S^-_u,T^-_u)\Big],$$

over the components of the two residual graphs. 3. Claim 1 (p. 15): if two states have equal $\Phi$ and $u'\in T_2\setminus T_1$, then $C_{u'}\cap S_1=\emptyset$. 4. Lemma 2 (Central Lemma) (p. 15): $\Phi$ is injective on $\mathcal S$, so $|\mathcal S|=|\Phi\langle\mathcal S\rangle|$.

Significance

The result. A naive dynamic program over all pairs $(S,T)$ has $2^{N+K}$ states. Theorem 1 shows that the states actually generated are at most $N\cdot 2^K$, so the algorithm, which spends $O(NK)$ operations per state, runs in time quadratic in $N$ when the number of customer types is constant and polynomial when $K=O(\log N)$. This identifies a tractable regime for a problem that is inapproximable in general. Lemma 2 is the paper's main counting tool: the same injection yields its later polynomial bounds for structured consideration sets (consideration sets of bounded diameter, induced intervals, laminar and $d$-disjunctive families), which are natural follow-up missions on top of this one.

Formalizing it. The results are proved in the paper; none is formalized. The mission produces a machine-checked model of the consider-then-choose problem under a unique ranking, of its graph decomposition, and of the inductively generated state space, plus proofs of the decomposition lemma, the recursion, and the counting bound. The proof of Lemma 2 in the paper is short and relies on invariants of the generated states stated in passing; a formal proof has to establish them for every state the recursion produces.

Difficulty

The upper bound $2^N$ is not a count of subsets of products: the map $(S,T)\mapsto S$ is not injective on $\mathcal S$, and different states can share their product sets. The bound $N\cdot 2^K$ likewise is not a count of pairs $(\min S, T)$ for arbitrary connected subgraphs: for the family of all connected pairs $(S,T)$ the count exceeds both bounds (when every $C_j=[N]$, all $(2^N-1)(2^K-1)$ nonempty pairs are connected). The bounds hold only because of how the recursion generates states, processing products in the common preference order, and the injectivity of $\Phi$ has to be derived from properties of that generation process (which types survive, which products remain) rather than from the definition of a state alone. Claim 1, proved in the paper's appendix, is where this history argument happens.

Formalization scope

• Products are Fin N and types Fin K. The order on Fin N is the common ranking, so the paper's product $1$ is 0 : Fin N, and $[\min(S)]$ is the set of indices ≤ S.min' h, including $\min(S)$ itself. Prices and type probabilities are real; the standing assumption that $\lambda$ is a probability vector is defined but not needed by any statement, since Lemma 1 and recursion (1) hold for all real data and the state space depends on the consideration sets only.
• $J$ is a finite maximum over the subsets of $S$. Connectivity is Mathlib's SimpleGraph.Connected of the subgraph of the bipartite graph induced on $S\cup T$; a component is a connected, closed vertex set. In Lemma 1 and recursion (1) the sums run over all components, including isolated products and isolated types, which contribute $0$.
• The state space is an inductive predicate with three rules (root components, the stock move, the skip move), and its size is Set.ncard of a subset of a finite type. States are nontrivial components (at least one product and one type). This is the paper's own setting: the proof of Lemma 2 uses that every state has an edge, and on isolated products $\Phi$ is not injective.
• Theorem 1's second sentence is about running time; only its state-space consequence is stated. Running time itself is not formalized.
• Claim 1 is stated under the hypotheses of the paper (two generated states with equal $\Phi$, $u'\in T_2\setminus T_1$). It is a step of a proof by contradiction: by Lemma 2 these hypotheses never hold together, so the claim records the key step rather than an inhabited situation.
• A formalization in which the state space is any family other than the one generated by the recursion (all connected pairs, or a family merely closed under the two moves), in which the processed product is not $\min(S)$, or in which $\Phi$ uses indices strictly below $\min(S)$, is a different statement, and the counting bounds are false or empty for it.
• Not formalized: Corollary 1 (diameter bound), Theorems 2–6 and EC.1–EC.3 (structured consideration sets, multiple rankings), and the general-ranking dynamic program of §5. A reusable by-product is the component decomposition of an induced bipartite subgraph. Proofs of the milestones in any order are welcome, as are lemmas on the invariants of generated states.

Page numbers are those of the accepted manuscript: page $n$ of the body is PDF page $n+1$ of the deposited file, and page ec$n$ of the e-companion is PDF page $35+n$.

Selected references

• A. Aouad, V. Farias, R. Levi, Assortment Optimization Under Consider-then-Choose Choice Models, Management Science 67(6):3368–3386, 2021 (accepted manuscript, LBS Research Online eprint 1426). https://doi.org/10.1287/mnsc.2020.3681
• A. Aouad, V. Farias, R. Levi, D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6):1661–1669, 2018. https://doi.org/10.1287/opre.2018.1754
• V. Farias, S. Jagabathula, D. Shah, A Nonparametric Approach to Modeling Choice with Limited Data, Management Science 59(2):305–322, 2013. https://doi.org/10.1287/mnsc.1120.1610
• D. Honhon, S. Jonnalagedda, X. A. Pan, Optimal Algorithms for Assortment Selection Under Ranking-Based Consumer Choice Models, Manufacturing & Service Operations Management 14(2):279–289, 2012. https://doi.org/10.1287/msom.1110.0365

Motivation

Many decisions under uncertainty share one structure: a choice $b$ scales the exposure to a random quantity $\tilde X$. A portfolio share scales the excess return of a risky asset, a coinsurance rate scales an uninsured loss, an output level scales a random price or a random cost. The linear-payoff model of Dionne, Eeckhoudt and Gollier (1993) covers all of these, and the comparative-statics question it poses is old: when the risk in $\tilde X$ increases, does the decision maker take less of it?

For second-degree risk (a mean-preserving spread, Rothschild and Stiglitz 1970) the answer is classical and depends on the decision problem. Menegatti and Peter (2022, doi:10.1287/mnsc.2021.4081) ask the question for risk increases of every order $N$ in the sense of Ekern (1980): downside risk ($N=3$), outer risk ($N=4$) and beyond. Their finding is that the answer depends on whether $\tilde X$ is a risky benefit or a risky cost, and, for a risky cost, on the parity of $N$.

Timeline:

• 1970, Rothschild and Stiglitz: increases in risk ($N=2$).
• 1980, Ekern: $N$th-degree risk increases and their expected-utility characterization (Lemma 1 of the paper).
• 2008, Eeckhoudt and Schlesinger: relative $(N+1)$th-degree risk aversion and the threshold $N$ for precautionary saving.
• 2016, Nocetti: a general criterion for comparative statics of $N$th-degree risk increases, the source of the paper's Lemma 3.
• 2022, Menegatti and Peter: the benefit/cost dichotomy (Proposition 2).

Setting

The payoff of decision $b\in B$ at realization $X$ is

$$z(X,b)=f(b)\,(X-x_0)+z_0,$$

where $B\subset\mathbb R$ is compact, $f$ is continuous on $B$, and $x_0,z_0$ are constants. The random variable $\tilde X\ge 0$ takes values in $[\underline x,\bar x]$. A decision maker with increasing, sufficiently smooth utility $U$ solves $\max_{b\in B}\mathbb E\,U(z(\tilde X,b))$, with maximizer set $B^*$.

Problem classes. The problem is risk taking if $f$ is increasing and risk mitigation if $f$ is decreasing; $\tilde X$ is a risky benefit if $f\ge0$ on $B$ and a risky cost if $f\le0$ on $B$.

$N$th-degree risk increase. For a distribution function $F$ on $[\underline x,\bar x]$ put $F^{(1)}=F$ and $F^{(k+1)}(z)=\int_{\underline x}^zF^{(k)}(t)\,dt$. If $\tilde X_1,\tilde X_2$ have distribution functions $F,G$, then $\tilde X_2$ is an $N$th-degree risk increase over $\tilde X_1$ when $F^{(k)}(\bar x)=G^{(k)}(\bar x)$ for $k=1,\dots,N$ and $F^{(N)}\le G^{(N)}$ on $[\underline x,\bar x]$.

Risk attitudes. The decision maker is $N$th-degree risk averse if $(-1)^{N+1}U^{(N)}\ge0$. Where $(-1)^{N+1}U^{(N)}>0$, the relative $(N+1)$th-degree risk aversion is $r_{N+1}(z)=-zU^{(N+1)}(z)/U^{(N)}(z)$.

Strong set order. For $D,D'\subset\mathbb R$, $D\ge_S D'$ if for all $d\in D$, $d'\in D'$: $\max\{d,d'\}\in D$ and $\min\{d,d'\}\in D'$.

Formalization targets

Goal: Proposition 2

Assume the decision maker is $N$th- and $(N+1)$th-degree risk averse with $r_{N+1}<N$ on the relevant domain, and let $\tilde X_2$ be an $N$th-degree risk increase over $\tilde X_1$, with maximizer sets $B_1^*,B_2^*$. Then

$$\text{risky benefit:}\quad B_2^*\le_S B_1^*\ \text{(risk taking)},\qquad B_2^*\ge_S B_1^*\ \text{(risk mitigation)};$$ $$\text{risky cost, }N\text{ even:}\quad B_2^*\le_S B_1^*\ \text{(risk taking)},\qquad B_2^*\ge_S B_1^*\ \text{(risk mitigation)},$$

and for a risky cost with $N$ odd both orderings are reversed.

Milestones

1. Lemma 1 (Ekern), direction (i) $\Rightarrow$ (ii): an $N$th-degree risk increase lowers $\mathbb E\,u$ for every $u$ with $(-1)^{N+1}u^{(N)}\ge0$.
2. Lemma 3: if $(-1)^Nf(b)^NU^{(N)}(f(b)(X-x_0)+z_0)$, display (5), is increasing (decreasing) in $b$ for all $X$, then $B_2^*\ge_S B_1^*$ ($\le_S$).
3. Display (7): the derivative of (5), stated in the variable $\varphi=f(b)$.
4. Display (8): the bracket of (7) equals $(-1)^{N+1}U^{(N)}\,[r_{N+1}-N]-z_0(-1)^{N+2}U^{(N+1)}$ and is negative.
5. The monotonicity of (5) in $b$ in each of the four problem classes.
6. Nonemptiness of $B_i^*$.

Significance

The result. Proposition 2 shows that the familiar statement "more risk, less risk taking" is a statement about risky benefits. For a risky cost, such as an uninsured loss or a random input price, an odd-order risk increase (for example, more downside risk) leads a prudent decision maker to take more risk. The paper uses this to explain apparently conflicting results in the portfolio, coinsurance, output-choice and hedging literatures, and to show that stochastic-dominance assumptions must be chosen differently for benefits and costs (its §5–§6).

Formalizing it. The result is proved in the paper; none of it is machine-checked. A complete development produces a reusable Lean account of Ekern's $N$th-degree risk order through iterated distribution functions, the integration-by-parts identity behind Lemma 1, and a template for transferring a distributional order through Topkis's monotonicity theorem to argmax sets in the strong set order. Topkis's theorem is already proved on the platform and is included as a reference item.

Difficulty

The calculus steps (7)–(8) are short; the weight sits elsewhere. Lemma 1 is an $N$-fold integration by parts of a Lebesgue–Stieltjes integral against a distribution function with possible atoms, with boundary terms that vanish only by Definition 2(i). Lemma 3 must turn a pointwise monotonicity of (5) into increasing differences of $b\mapsto\mathbb E\,U(z(\tilde X_i,b))$ in $(b,i)$, and then into a strong-set-order comparison of possibly set-valued maximizers. A tempting shortcut, differentiating (5) in $b$, is unavailable: $f$ is only continuous. The sign conditions are then needed at payoffs lying between those of two decisions, not only at the payoffs themselves, which is why the relevant domain must be an interval.

Formalization scope

• Random variables are represented by their laws: probability measures on $\mathbb R$ concentrated on $[\underline x,\bar x]$. Distribution functions are Mathlib's right-continuous cdf. The iterated CDF is indexed from $0$: iterCDF μ xl k is the page's $F^{(k+1)}$.
• $U:\mathbb R\to\mathbb R$ is $C^{N+1}$ and increasing. The "relevant domain" is an order-connected set $D$ containing every payoff; the risk attitudes are imposed only on $D$. A $C^{N+1}$ utility on a neighbourhood of the compact payoff range extends to $\mathbb R$, so this loses nothing.
• $N$th-degree risk aversion is strict, $(-1)^{N+1}U^{(N)}>0$ on $D$, because Definition 4 defines $r_{N+1}$ only there; "below $N$" is strict.
• Added hypothesis $z_0\ge0$. The paper's sign argument for (8) marks $z_0(-1)^{N+2}U^{(N+1)}$ as non-negative, which assumes it; without it the bracket of (7) can be positive.
• "Increasing" and "decreasing" are weak. Parity is Mathlib's Even/Odd.
• The strong set order is the published Supermodularity.Lattices.InducedSetOrder; $B_2^*\le_S B_1^*$ is InducedSetOrder B₂ B₁.
• The goal does not assume that (5) is monotone, nor that $B_i^*$ is nonempty: monotonicity of (5) is a milestone derived from the risk attitudes, and nonemptiness is a separate milestone, so the strong-set-order conclusions are not vacuous on the intended instances. A formalization that put the monotonicity of (5) among the goal's hypotheses would reduce it to Lemma 3 and is excluded.
• Not formalized here: Proposition 1 ($(N+1)$th-degree risk neutrality), Lemma 2 (mirror images), the $(M/N)$ stochastic-dominance extension (Definitions 5–6, Lemma 4, Theorems 1–2) and the applications (Corollaries 1–5).

Contributions are welcome on any milestone; a proof of Lemma 1 is reusable well beyond this mission, for any statement about Ekern's risk orders.

Selected references

• M. Menegatti, R. Peter, Changes in risky benefits and in risky costs: a question of the right order, Management Science 68(5):3625–3634, 2022. https://doi.org/10.1287/mnsc.2021.4081
• S. Ekern, Increasing Nth degree risk, Economics Letters 6(4):329–333, 1980. https://doi.org/10.1016/0165-1765(80)90005-1
• L. Eeckhoudt, H. Schlesinger, Changes in risk and the demand for saving, Journal of Monetary Economics 55(7):1329–1336, 2008. https://doi.org/10.1016/j.jmoneco.2008.08.004
• D. C. Nocetti, Robust comparative statics of risk changes, Management Science 62(5):1381–1392, 2016. https://doi.org/10.1287/mnsc.2015.2190
• G. Dionne, L. Eeckhoudt, C. Gollier, Increases in risk and linear payoffs, International Economic Review 34(2):309–319, 1993.
• M. Rothschild, J. E. Stiglitz, Increasing risk: I. A definition, Journal of Economic Theory 2(3):225–243, 1970. https://doi.org/10.1016/0022-0531(70)90038-4
• D. M. Topkis, Minimizing a submodular function on a lattice, Operations Research 26(2):305–321, 1978. https://doi.org/10.1287/opre.26.2.305