All missions

Motivation

Quantum error correction protects quantum information from noise by storing it in a code and undoing the damage with a recovery operation. The textbook theory, the Knill–Laflamme conditions, characterizes codes that can be corrected perfectly. Real noise rarely admits perfect correction, and codes that are only approximately correctable can perform better than perfect ones: they can use fewer physical resources for a given target fidelity. Approximate quantum error correction (AQEC) asks for algebraic conditions that tell, from the noise and the code alone, how well a code can be corrected.

Mandayam and Ng (arXiv:1202.5139, Phys. Rev. A 2012) extend an earlier AQEC framework for subspace codes (Ng and Mandayam, arXiv:0909.0931, 2010) to subsystem codes, where information is stored in one tensor factor $A$ of a subspace $\mathcal H_A\otimes\mathcal H_B$ and the factor $B$ is a gauge whose state does not matter. Subsystem codes include noiseless subsystems and the Bacon–Shor family, and they are the natural setting for operator quantum error correction (Kribs, Laflamme and Poulin, arXiv:quant-ph/0412076, 2005).

Setting

The system space is $\mathcal H=\mathcal H_A\otimes\mathcal H_B\oplus\mathcal K$, with $\mathcal H_A$, $\mathcal H_B$ finite dimensional; $P$ is the projector onto $\mathcal H_{AB}=\mathcal H_A\otimes\mathcal H_B$ and $P_A,P_B$ the identities of the factors. The code $\mathcal C$ is the set of all product states $\rho_A\otimes\rho_B$, with $\rho_A,\rho_B$ density operators.

The noise $\mathcal E$ is a completely positive, trace-preserving (CPTP) map with Kraus operators $E_1,\dots,E_N:\mathcal H_{AB}\to\mathcal H$:

$$\mathcal E(\rho)=\sum_iE_i\rho E_i^\dagger,\qquad \sum_iE_i^\dagger E_i=P .$$

Write $\mathcal P_{\mathcal E}$ for the support of $\mathcal E(P)=\sum_iE_iE_i^\dagger$. A recovery is a CP map $\mathcal R:\mathcal B(\mathcal P_{\mathcal E})\to\mathcal B(\mathcal H_{AB})$ that is trace preserving on $\mathcal P_{\mathcal E}$.

The fidelity of states is $F(\rho,\sigma)=\mathrm{tr}\sqrt{\rho^{1/2}\sigma\rho^{1/2}}$. The fidelity loss of the code state $\rho$ under $\mathcal E$ and $\mathcal R$ compares the information in $A$ before and after:

$$\eta_{\mathcal R}\{\rho\}=1-F^2\big(\mathrm{tr}_B\,\rho,\ \mathrm{tr}_B[(\mathcal R\circ\mathcal E)(\rho)]\big).$$

The code is $\epsilon$-correctable on $A$ under $\mathcal E$ when some recovery has $\eta_{\mathcal R}\{\rho\}\le\epsilon$ for every $\rho\in\mathcal C$.

The transpose channel $\mathcal R_P$ is the recovery with Kraus operators

$$R^P_i=P\,E_i^\dagger\,\mathcal E(P)^{-1/2},$$

the inverse square root being taken on the support of $\mathcal E(P)$.

Formalization targets

Goal: Corollary 3

Suppose that, for all $i,j$,

$$PE_i^\dagger\mathcal E(P)^{-1/2}E_jP=P_A\otimes B_{ij}+\Delta_{ij}\qquad(12)$$

with $B_{ij}$ operators on $\mathcal H_B$ and $\Delta_{ij}$ operators on $\mathcal H_{AB}$. Then the transpose channel is a recovery, and for every $\rho\in\mathcal C$

$$\eta_{\mathcal R_P}\{\rho\}\le\Big\|\sum_{ij}\Delta_{ij}^\dagger\Delta_{ij}\Big\|,$$

so $\mathcal C$ is $\epsilon$-correctable on $A$ whenever $\epsilon\ge\|\sum_{ij}\Delta_{ij}^\dagger\Delta_{ij}\|$ (operator norm). The statement holds for every choice of the operators $B_{ij}$; each choice determines $\Delta_{ij}$ and gives a bound.

Theorem 2

Under (12), $\mathcal C$ is $\epsilon$-correctable on $A$ for every $\epsilon\ge\eta_P$, where

$$\eta_P=\max_{|\psi_A,\phi_B\rangle}\langle\phi_B|\sum_{ij}\Big[\langle\psi_A|\Delta^\dagger_{ij}\Delta_{ij}|\psi_A\rangle-\langle\psi_A|\Delta^\dagger_{ij}|\psi_A\rangle\langle\psi_A|\Delta_{ij}|\psi_A\rangle\Big]|\phi_B\rangle$$

is the fidelity loss of the transpose channel. Theorem 2 is sharper than Corollary 3; the corollary trades sharpness for a quantity that is easy to compute.

Milestones

The milestones follow the paper's own steps: the pure-state form (5) of the fidelity; the reduction of the worst case over $\mathcal C$ to pure product states; trace preservation of $\mathcal R_P$ on $\mathcal P_{\mathcal E}$; the trace-preservation identity of $\mathcal R_P\circ\mathcal E$ in terms of $B_{ij},\Delta_{ij}$; the fidelity formula (14) on pure product states; Theorem 2; and the bound of the expression (13) by the operator norm.

Significance

When all $\Delta_{ij}$ vanish, (12) is the paper's perfect-correction condition (Theorem 1), and the transpose channel is a perfect recovery. Corollary 3 quantifies the robustness of that statement: a perturbation of size $\|\sum\Delta^\dagger\Delta\|$ costs at most that much fidelity loss, with an explicit recovery. This turns the search for approximate subsystem codes into a check of a matrix inequality, and it supplies the sufficient half of a characterization whose necessary half (near-optimality of the transpose channel) the paper establishes only in restricted scenarios.

Status: the results are proved in the paper, not formalized. Prove2Me's catalog has no statement of Theorem 2, Corollary 3, or of perfect-correction conditions for subsystem codes. This mission states the subsystem-code model in Lean, with mixed code states and a possibly singular $\mathcal E(P)$, and poses each step of the paper's proof as a target. The reduction to pure states needs the joint concavity of the fidelity, which Mathlib does not have; a proof of it is reusable across quantum information theory.

Difficulty

Two steps resist a direct computation. First, the code contains mixed product states, while the fidelity formula (14) is available only for pure ones; the passage from one to the other is the joint concavity of $F$, a consequence of Uhlmann's theorem, not a linear-algebra identity. Second, $\mathcal E(P)$ need not be invertible: $\mathcal E(P)^{-1/2}$ is a pseudo-inverse, the transpose channel is trace preserving only on $\mathcal P_{\mathcal E}$, and the trace-preservation identity of $\mathcal R_P\circ\mathcal E$ needs that each $E_j$ maps into $\mathcal P_{\mathcal E}$. Arguments that treat $\mathcal E(P)^{-1/2}$ as an inverse are wrong in general.

Formalization scope

• $\mathcal H_{AB}$ is indexed by a × b with $A$ first, matching ⊗ₖ and the published partial trace; $\mathcal H$ is a separate finite type o. The noise's Kraus operators are rectangular matrices Matrix o (a × b) ℂ, so $P$, $P_A$, $P_B$ are identity matrices and $P_A\otimes B_{ij}$ is 1 ⊗ₖ B i j.
• Vectors are a → ℂ, unit when star ψ ⬝ᵥ ψ = 1; $|\psi\rangle\langle\psi|$ is vecMulVec ψ (star ψ).
• Published definitions are reused: the fidelity (WildeQIT.fidelity $=F^2$, rootFidelity $=F$), the partial trace WildeQIT.partialTraceRight, the channel action PeresTerno.krausUpdate, density matrices PeresTerno.IsDensityMatrix, and the support inverse square root and support projector QReversal.NearOpt.invSqrt, supportProj.
• A recovery is any finite Kraus family $R_k$ from o to a × b with $\mathcal P_{\mathcal E}(\sum_kR_k^\dagger R_k)\mathcal P_{\mathcal E}=\mathcal P_{\mathcal E}$. Full support of $\mathcal E(P)$ is not assumed.
• $\epsilon$-correctability is the existence of a recovery with fidelity loss at most $\epsilon$ on every code state; it is equivalent to the paper's $\epsilon\ge\eta_{\mathrm{op}}$ because the minimum defining $\eta_{\mathrm{op}}$ is attained. "$\epsilon\ge\eta_P$" is stated as a bound on the expression (13) at every pair of unit vectors, with no supremum.
• The norm in (15) is the operator norm, Mathlib's Matrix.Norms.L2Operator; neither the entrywise sup norm nor the Frobenius norm.

The statements carry no smallness hypothesis on $\Delta_{ij}$, quantify over all code states including mixed ones rather than over pure states only, and admit only recoveries that are trace preserving on $\mathcal P_{\mathcal E}$; each of these restrictions would make the goal weaker or trivial.

Needed infrastructure: the continuous functional calculus identities for $X^{-1/2}XX^{-1/2}$ and for range inclusions of $\sum_iE_iE_i^\dagger$, Kronecker-product algebra, and joint concavity (or Uhlmann's theorem) for the fidelity. Proofs of any milestone, and general fidelity lemmas usable beyond this mission, are welcome.

Selected references

• P. Mandayam and H. K. Ng, Towards a unified framework for approximate quantum error correction, Phys. Rev. A 86, 012335 (2012). arXiv:1202.5139 (version v2 is the one formalized).
• H. K. Ng and P. Mandayam, Simple approach to approximate quantum error correction based on the transpose channel, Phys. Rev. A 81, 062342 (2010). arXiv:0909.0931
• D. Kribs, R. Laflamme and D. Poulin, Unified and generalized approach to quantum error correction, Phys. Rev. Lett. 94, 180501 (2005). arXiv:quant-ph/0412076
• E. Knill and R. Laflamme, Theory of quantum error-correcting codes, Phys. Rev. A 55, 900 (1997). arXiv:quant-ph/9604034
• H. Barnum and E. Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, J. Math. Phys. 43, 2097 (2002). arXiv:quant-ph/0004088

Motivation

Given an unknown quantum state distributed over two systems, we determine how much quantum communication is needed to transfer the full state to one system. This communication measures the "partial information" one system needs conditioned on it's prior information. It turns out to be given by an extremely simple formula, the conditional entropy. In the classical case, partial information must always be positive, but we find that in the quantum world this physical quantity can be negative. If the partial information is positive, its sender needs to communicate this number of quantum bits to the receiver; if it is negative, the sender and receiver instead gain the corresponding potential for future quantum communication. We introduce a primitive "quantum state merging" which optimally transfers partial information. We show how it enables a systematic understanding of quantum network theory, and discuss several important applications including distributed compression, multiple access channels and multipartite assisted entanglement distillation (localizable entanglement). Negative channel capacities also receive a natural interpretation.

This mission is the statement-level formalization of Quantum information can be negative (arXiv:quant-ph/0505062v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal state merging has signed cost S(A|B) (Unnumbered main result: optimal quantum state merging and negative information, 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

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

• Application 1; Figure 2 and all-subset inequalities: An independently operational signed m-sender compression rate region with one decoder, local encoders, free classical messages, separate Bell input/output resources for every sender, and full purifying-reference reconstruction. (hard)
• Application 2: noiseless coding with side information: A source-consistent definition of E_p(AU:R), including the correct purification/environment channel and one-copy versus regularized rate convention for the asserted one-way iff region. (source-ambiguity)
• Application 3, equation (2): A two-coordinate signed quantum MAC transmission code with independent reference inputs, individually local encoders, one joint memoryless channel/decoder, explicitly charged sender-decoder Bell resources and the allowed classical messages. (hard)
• Application 4, equation (3): An arbitrary-number-of-individually-local-helpers i.i.d. EPR-distillation protocol and its asymptotic rate threshold, without initial shared assistance or quantum helper collaboration. (hard)

Selected references

• Quantum information can be negative, arXiv:quant-ph/0505062v1, https://arxiv.org/abs/quant-ph/0505062v1

Motivation

A necessary condition for reversibility (sufficiency) of a quantum channel with respect to complete families of states with bounded rank is obtained. A full description (up to isometrical equivalence) of all quantum channels reversible with respect to orthogonal and nonorthogonal complete families of pure states is given. Some applications in quantum information theory are considered. The main results can be formulated in terms of the operator algebras theory (as conditions for reversibility of channels between algebras of all bounded operators).

This mission is the statement-level formalization of Reversibility conditions for quantum channels and their applications (arXiv:1203.0262v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3 (seed paper result): bounded-rank reversibility and the pure-state normal form (Theorem 3 (seed paper result): bounded-rank reversibility and the pure-state normal form, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 5 (entire printed quantitative statement): The binder or definition of n in the quantitative Kraus-count bound for a general Borel ensemble. (source-ambiguity)
• Theorem 2 [13], cited background: Separate scope/provenance handling of the cited complete countable-family Petz criterion, without entropy-finiteness assumptions. (hard)

Selected references

• Reversibility conditions for quantum channels and their applications, arXiv:1203.0262v3, https://arxiv.org/abs/1203.0262v3

Motivation

It is proven that recently introduced states with perfectly secure bits of cryptographic key (private states representing secure bit) [K. Horodecki et al., Phys. Rev. Lett. 94, 160502 (2005)] as well as its multipartite and higher dimension generalizations always represent distillable entanglement. The corresponding lower bounds on distillable entanglement are provided. We also present a simple alternative proof that for any bipartite quantum state entanglement cost is an upper bound on distillable cryptographic key in bipartite scenario.

This mission is the statement-level formalization of Quantum states representing perfectly secure bits are always distillable (arXiv:quant-ph/0602176v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Every exact nontrivial private state has positive GHZ distillable entanglement (Abstract; II.A–B, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• II.B, last paragraph, suggested POVM extension: A complete multi-outcome locally orthogonal filtering instrument, with specified support notion, failure completion, admissible key-pair family and exact efficiency conclusion. (source-ambiguity)

Selected references

• Quantum states representing perfectly secure bits are always distillable, arXiv:quant-ph/0602176v2, https://arxiv.org/abs/quant-ph/0602176v2

Motivation

Consider many instances of an arbitrary quadripartite pure state of four quantum systems ABCD. Alice holds the AC part of each state, Bob holds B, while D represents all other parties correlated with ABC. Alice is required to redistribute the C systems to Bob while asymptotically preserving the overall purity. We prove that this is possible using Q qubits of communication and E ebits of shared entanglement between Alice and Bob, provided that Q geq I(C;D|B)/2 and Q+E geq H(C|B), proving the optimality of the Luo-Devetak outer bound. The optimal qubit rate provides the first known operational interpretation of quantum conditional mutual information. We also show how our protocol leads to a fully operational proof of strong subadditivity and uncover a general organizing principle, in analogy to thermodynamics, that underlies the optimal rates.

This mission is the statement-level formalization of Optimal quantum source coding with quantum information at the encoder and decoder (arXiv:0706.2907v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 (Method of types): all simultaneous typical-projection bounds (Theorem 5 (Method of types): all simultaneous typical-projection bounds, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1 (seed): exact quantum state-redistribution rate region: Source-preserving signed quantum/ebit redistribution achievability and exact operational region (hard)
• Theorem 2: redistribution with generated qubits and ebits: Redistribution with separately generated forward identity channels and ebits (hard)
• Theorem 3: redistribution with coherent communication: Redistribution with a coherently generated cobit channel (hard)
• Theorem 4: robust one-shot redistribution protocol — source dimension defect: A uniquely specified normalized CPTP repair of the dimension-defective encoder in Theorem 4 (source-ambiguity)
• Lemma 1 (Composition lemma [18]): Operational simulation of arbitrary finite resource bundles and their asymptotic composition (hard)
• Lemma 2 (Cancellation lemma [18]): Operational resource addition/scaling and sublinear catalytic input (hard)
• §V, unnumbered: optimal classical communication cost: Classical-only redistribution protocols with a finite entanglement trade (hard)
• §I/§V, unnumbered: optimal successive redistribution: Composable two-step source-preserving redistribution and computed step costs (hard)
• §V, unnumbered: pure bipartite source redistribution: Zero-rate redistribution with permitted sublinear communication (hard)
• §V, unnumbered: flagged conditionally decoupled source cost: Flagged conditionally decoupled source construction and its operational cost (hard)
• §V, unnumbered: redistribution with separate consumed and generated ebits: Source-preserving redistribution with distinct initial and final Bell resources (hard)

Selected references

• Optimal quantum source coding with quantum information at the encoder and decoder, arXiv:0706.2907v2, https://arxiv.org/abs/0706.2907v2

Motivation

In this paper, we present a new entanglement monotone for bipartite quantum states. Its definition is inspired by the so-called intrinsic information of classical cryptography and is given by the halved minimum quantum conditional mutual information over all tripartite state extensions. We derive certain properties of the new measure which we call "squashed entanglement": it is a lower bound on entanglement of formation and an upper bound on distillable entanglement. Furthermore, it is convex, additive on tensor products, and superadditive in general. Continuity in the state is the only property of our entanglement measure which we cannot provide a proof for. We present some evidence, however, that our quantity has this property, the strongest indication being a conjectured Fannes type inequality for the conditional von Neumann entropy. This inequality is proved in the classical case.

This mission is the statement-level formalization of "Squashed Entanglement" - An Additive Entanglement Measure (arXiv:quant-ph/0308088v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Superadditivity and tensor-product additivity (§II, Proposition 4 (p.1 seed), PDF p. 3). 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.

Selected references

• "Squashed Entanglement" - An Additive Entanglement Measure, arXiv:quant-ph/0308088v3, https://arxiv.org/abs/quant-ph/0308088v3

Motivation

Interior-point methods minimize a linear function over a convex set $K\subseteq\mathbb R^n$ by following the minimizers of $t\,c^{\mathsf T}x+\varphi(x)$, where $\varphi$ is a self-concordant barrier for $K$. The number of Newton steps the path-following method needs to reach accuracy $\epsilon$ is $O(\sqrt{\nu}\log(1/\epsilon))$, where $\nu$ is the barrier's self-concordance parameter. A smaller $\nu$ is a better iteration bound, and the question of the smallest $\nu$ achievable for an arbitrary convex domain is a basic question of the theory.

• 1994: Nesterov and Nemirovski introduced the universal barrier, defined for every convex domain without lines, and proved it is $O(n)$-self-concordant (Interior-Point Polynomial Algorithms in Convex Programming, SIAM, Theorem 2.5.1). They also showed that no barrier for the simplex or the cube has parameter below $n$.
• 2015: Bubeck and Eldan introduced the entropic barrier, proved it is $(1+o(1))n$-self-concordant, and showed that on convex cones both the universal and the entropic barrier are $n$-self-concordant (arXiv:1412.1587).
• 2021: Lee and Yue proved that the universal barrier is $n$-self-concordant on every proper convex domain in $\mathbb R^n$, $n\ge1$ (arXiv:1809.03011, Mathematics of Operations Research). This mission formalizes that result.

Setting

A convex domain is a convex set $K\subseteq\mathbb R^n$ with non-empty interior; it is proper if it contains no line $\{x+tv:t\in\mathbb R\}$ with $v\neq0$. $K$ need not be closed or bounded. For $x\in\operatorname{int}(K)$ the polar set of $K$ with respect to $x$ is

$$K^\circ(x)=\{y\in\mathbb R^n:\ y^{\mathsf T}(z-x)\le1\ \text{ for all } z\in K\},$$

a convex body, and the universal barrier is $\varphi(x)=\log\mathrm{Vol}_n(K^\circ(x))$.

A function $\varphi$ on $\operatorname{int}(K)$ is a barrier if $\varphi(x)\to+\infty$ as $x\to\partial K$. A convex, three times continuously differentiable $\varphi$ is self-concordant if, for all $x\in\operatorname{int}(K)$ and $h\in\mathbb R^n$,

$$|D^3\varphi(x)[h,h,h]|\le2\,(D^2\varphi(x)[h,h])^{3/2},\tag{1}$$

and $\nu$-self-concordant if moreover $|D\varphi(x)[h]|\le(\nu\,D^2\varphi(x)[h,h])^{1/2}$ (2).

The proof works with one-dimensional laws. For a convex body $L$ and $h\neq0$, the marginal density $p(L,h;\cdot)$ is the density of $y^{\mathsf T}h$ for $y$ uniform on $L$. For a density $p$ on $\mathbb R$, $\mu_1(p)$ is its mean, $\mu_2^2(p)$ its variance and $\mu_3^3(p)$ its third central moment; $\mu_2^3(p)=(\mu_2^2(p))^{3/2}$. A density is $\tfrac1m$-concave if $p^{1/m}$ is concave on its support (for $m=0$: $p$ is constant on its support, up to endpoints).

Formalization targets

Goal: Theorem 2

$$\text{For } n\ge1 \text{ and every proper convex domain } K\subseteq\mathbb R^n,\ \ \varphi(x)=\log\mathrm{Vol}_n(K^\circ(x)) \text{ is an } n\text{-self-concordant barrier for } K.$$

The parameter $n$ is exact, so the goal carries no constant to improve.

Milestones

1. The barrier property of $\varphi$.
2. Brunn's concavity principle for hyperplane sections (Theorem 1 with $F=h^\perp$): $p(L,h;\cdot)$ is $\tfrac1{n-1}$-concave.
3. Lemma 2: a non-increasing density on $[0,1]$ has mean at most $\tfrac12$.
4. The polynomial inequality $f_0(\gamma)\ge0$ for $\gamma\ge1$ (§4.1.7).
5. Proposition 1, inequality (5): for a $\tfrac1{k-1}$-concave density with $0\in\operatorname{Supp}(p)$, $\mu_1^2(p)\le k(k+2)\mu_2^2(p)$.
6. Lemma 3: affine invariance of the family $\mathcal Q$ and of $\Xi(p)=|\mu_3^3(p)/\mu_2^3(p)|$.
7. Lemma 4: the polynomial inequality $g(\gamma,k)\ge0$ for $\gamma\ge1$, $k\ge2$.
8. Proposition 1, inequality (4): for a $\tfrac1{k-1}$-concave density,

$$|\mu_3^3(p)|\le2\sqrt{\tfrac{k+2}{k}}\,\tfrac{k-1}{k+3}\,\mu_2^3(p).$$

9. Lemma 1: $D\varphi$, $D^2\varphi$, $D^3\varphi$ at $x$ along $h$ as polynomials in the moments of $p(K^\circ(x),h;\cdot)$.
10. Inequality (9): $\ell(t)=(2t^3+6t+4c_n)/(1+t^2)^{3/2}\le2\sqrt{n+1}$, with $c_n=(n-1)/(2\sqrt n)$.

Significance

The theorem settles the self-concordance parameter of the universal barrier for every proper convex domain: it is $n$, and by the lower bound of Nesterov and Nemirovski no barrier does better in general. It implies the $n$-self-concordance results for cones as special cases, and it gives a canonical barrier attaining the optimal iteration bound $O(\sqrt n\log(1/\epsilon))$ on any domain. Proposition 1, a pair of sharp moment inequalities for $s$-concave distributions, is of independent interest; it extends the third-moment bound for log-concave laws used by Bubeck and Eldan.

The result is proved on paper; none of it is formalized. A complete development would give machine-checked statements of the universal barrier, its derivative formulas, Brunn's principle for hyperplane sections, and the moment inequalities, all of which are reusable for other barrier constructions (the entropic barrier missions on the platform use the same definitions of barrier and self-concordance). The two polynomial inequalities (milestones 4 and 7) are self-contained and the appendix proof of Lemma 4 is long elementary calculus, a natural target for automation.

Difficulty

The derivative formulas reduce $n$-self-concordance to moment inequalities for the marginal of the polar body. The obvious argument uses only log-concavity of marginals (Prékopa–Leindler) and the log-concave third-moment bound; it yields $\nu=O(n)$ and loses a constant. Exactness requires the stronger $\tfrac1{n-1}$-concavity and moment bounds that are sharp for every $k$, attained by $k\,t^{k-1}$ on $[0,1]$. Proposition 1 is an extremal problem over an infinite-dimensional class of densities, and the sharp constants surface only as polynomial inequalities in a parameter $\gamma\ge1$ whose degree grows with $k$ (milestones 4 and 7); Lemma 4 must hold uniformly in the integer $k\ge2$, and small $k$ behave differently. The localization lemma the paper cites for the reduction is not in Mathlib. On the analytic side, Lemma 1 requires differentiating $\log\mathrm{Vol}_n(K^\circ(x))$ three times under the integral for a possibly unbounded $K$.

Formalization scope

The space is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume. The goal's conclusion is the published predicate EntropicBarrier.Universal.IsNuSelfConcordantBarrier K φ n: barrier limits at every frontier point within $\operatorname{int}(K)$; convexity, $C^3$ and inequality (1) on $\operatorname{int}(K)$ through the published line-restriction form ConvexOptimization.IsSelfConcordantOn; and (2) in one-sided form, equivalent to the two-sided one. Lemma 1 uses Fréchet derivatives iteratedFDeriv. The universal barrier is a total function; its values off $\operatorname{int}(K)$ are junk and never read. All of $K$'s standing assumptions (convex, non-empty interior, no line) are bundled in IsProperConvexDomain, together with $n\ge1$.

Three conventions correct slips of the page and are disclosed in each item:

• $s$-concavity is quantified over support points. Definition 5 read literally (for all $t_1,t_2\in\mathbb R$) is satisfied by no probability density, which would make Proposition 1 vacuously true and Brunn's principle false. The formalization uses the paper's own usage, "on its support". This trivializing reading is ruled out by design, and a sanity check exhibits a density satisfying every hypothesis of Proposition 1.
• Marginals are normalized by their own integral, since $\mathrm{Vol}_{n-1}(\text{slice})/\mathrm{Vol}_n(L)$ integrates to $1/\|h\|$; the published section measure is an unnormalized Hausdorff measure, and the normalization removes its constant. Milestones 2 and 9 assume $h\neq0$.
• The family $\mathcal Q$ requires $a<b$; the degenerate case is the Dirac case the paper treats separately.

Densities are non-negative functions with integral $1$, and moments are Bochner integrals; a $\tfrac1{k-1}$-concave density has bounded support, so they are genuine. Not formalized: Brunn's principle for general $k$, the localization lemma (Theorem 3) and its corollaries, the limiting reductions of §4.1.1–§4.1.5 and §4.2.1, and the internals of Appendix A. Contributions of any of these as supporting lemmas, of Brunn–Minkowski-type tools for sections, and of differentiation-under-the-integral results for polar volumes are welcome.

Selected references

• Y. T. Lee and M.-C. Yue, Universal Barrier is n-Self-Concordant, Mathematics of Operations Research 46(3), 2021; arXiv:1809.03011v4. https://arxiv.org/abs/1809.03011
• Yu. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• S. Bubeck and R. Eldan, The entropic barrier: a simple and optimal universal self-concordant barrier, COLT 2015; arXiv:1412.1587. https://arxiv.org/abs/1412.1587
• M. Fradelizi and O. Guédon, The extreme points of subsets of s-concave probabilities and a geometric localization theorem, Discrete & Computational Geometry 31(2), 2004. https://doi.org/10.1007/s00454-003-2868-y
• S. Brazitikos, A. Giannopoulos, P. Valettas and B.-H. Vritsiou, Geometry of Isotropic Convex Bodies, AMS, 2014. https://doi.org/10.1090/surv/196

Learning which products to offer

A retailer that sells $N$ substitutable products must decide, for each arriving customer, which subset of products to display. Customer preferences are unknown at the start and have to be learned from purchases, while every suboptimal display costs revenue. This is dynamic assortment planning, a standard problem of revenue management in e-commerce and online advertising, and its learning version is a bandit problem whose arms are the $2^N$ subsets of products.

Under the multinomial logit (MNL) choice model the problem has been studied through the regret of a policy over $T$ customers (Chen, Wang and Zhou, §2 and Table 1):

• Rusmevichientong, Shen and Shmoys (2010) analysed the same revenue potential as this paper with a golden-ratio search; their bound involves $\log N$ and needs a separability (gap) assumption between candidate assortments.
• Sauré and Zeevi (2013) also cast MNL assortment learning as regret minimization.
• Agrawal, Avadhanula, Goyal and Zeevi gave UCB and Thompson-sampling policies with regret $\tilde O(\sqrt{NT} + N)$ for assortments of capacity $K$.
• Chen and Wang (2018) proved an $\Omega(\sqrt{NT})$ lower bound in the capacitated model when $K \le N/4$.

In the capacitated model the regret must grow with $N$. Chen, Wang and Zhou (arXiv:1805.04785v2, Mathematics of Operations Research 2021) show that without a capacity constraint it need not: a trisection policy achieves regret $C_1\sqrt T$ with a universal constant, and $\sqrt T/384$ is a lower bound. This mission formalizes the upper bound.

Setting

There are $N$ items with known revenues $r_1,\dots,r_N \in [0,1]$ and unknown utilities $v_1,\dots,v_N \ge 0$; the no-purchase option has utility $v_0 = 1$. In each period $t = 1,\dots,T$ the retailer offers an assortment $S_t \subseteq [N]$, and the customer buys $j \in S_t$ with probability $v_j/(1+\sum_{i\in S_t} v_i)$ or buys nothing with probability $1/(1+\sum_{i\in S_t} v_i)$, independently of the past. The expected revenue of $S$ is

$$R(S) = \frac{\sum_{j\in S} r_j v_j}{1 + \sum_{j\in S} v_j},$$

and the regret of a policy is $\mathrm{Regret} = \mathbb E\sum_{t=1}^T R(S^*) - R(S_t)$, where $S^*$ maximizes $R$ over all $2^N$ subsets.

The policy rests on two objects. The level set $\mathcal L_\theta = \{i : r_i \ge \theta\}$ collects the items whose revenue is at least $\theta$. The revenue potential $F(\theta) = R(\mathcal L_\theta)$ is a piecewise-constant function of one real variable. Its maximum is $F^* = \sup_{\theta \ge 0} F(\theta)$, its right limit is $F(\theta^+)$, and $\theta^*$ denotes the fixed point $\theta^* = F(\theta^*) = F^*$.

The adaptive-confidence trisection policy keeps an interval $[a_\tau, b_\tau]$, starting from $[0,1]$. In epoch $\tau$ it forms the points $x_\tau = \tfrac23 a_\tau + \tfrac13 b_\tau$ and $y_\tau = \tfrac13 a_\tau + \tfrac23 b_\tau$, at distance $\varepsilon_\tau = y_\tau - x_\tau = \tfrac13(\tfrac23)^\tau$, and runs $n_\tau = 8\lceil\varepsilon_\tau^{-2}\ln(8T\varepsilon_\tau^2)\rceil$ inner iterations. Each inner iteration does two things:

• while $y_\tau$ lies inside the current confidence interval $[\ell, u]$ for $F(y_\tau)$, it explores: it offers $\mathcal L_{y_\tau}$, adds the revenue to the running sum $\rho_t$, and sets $[\ell_t, u_t] = \rho_t/t \pm \sqrt{2\ln(8T/t)/t}$;
• it then exploits by offering $\mathcal L_{a_\tau}$.

At the end of the epoch the policy sets $b_{\tau+1} = y_\tau$ if $u < y_\tau$, and $a_{\tau+1} = x_\tau$ otherwise. The policy knows $r$ and $T$ but never $v$.

Formalization targets

Goal: Theorem 3

There is a universal constant $C_1 > 0$ such that for every $N$, every horizon $T$, all $v_i \ge 0$ and all $r_i \in [0,1]$, the adaptive-confidence trisection policy satisfies

$$\mathbb E\sum_{t=1}^T R(S^*) - R(S_t) \le C_1\sqrt T.$$

No gap condition and no bound on $v$ is assumed. The constant is left unspecified, as in the paper.

Milestones

• Structure of $F$. Lemma 1 (revenue-ordered optimality), Corollary 1 ($F^* = R(S^*)$), Lemma 2 (the fixed point, under $F^* > 0$), the jump identity (S4)/(S8), and Lemmas 3–4 ($F$ is below the diagonal to the right of $\theta^*$ and above it to the left).
• Concentration. Hoeffding's inequality (Lemma 15, already proved on the platform), the uniform inequality with growing confidence levels (Lemma 8, (11)), and the two tail bounds (S32) and (S33) used in the proof of Lemma 10.
• Recursion. With $\psi^\omega_\tau(\alpha,\beta)$ the expected regret of epochs $\tau,\dots,\tau_0$ conditioned on the relative position of $a_\tau$, $b_\tau$ and $\theta^*$ ((14)): Lemma 11 (Case 3, $\psi^3_\tau \le \alpha T$), Lemma 9 (Case 1) and Lemma 10 (Case 2).

Significance

Theorem 3, together with the lower bound of Theorem 4, settles the minimax regret of uncapacitated MNL assortment learning at $\Theta(\sqrt T)$, independent of the number of products. The policy uses no estimate of the individual utilities, and its cost per period is one level-set offer, so it applies to catalogues where $N$ is large compared with $T$. The structural lemmas on the revenue potential (Lemmas 1–4) are standard tools for MNL assortment problems and are reusable by other missions on static and dynamic assortment optimization. Lemma 8 is a MOSS-style concentration inequality whose confidence level grows with the sample size; it is the device that removes the $\sqrt{\log T}$ factor of the paper's baseline bound (Theorem 2).

The result is proved in the paper and is not presented as open; no machine-checked proof of any part of it is known. The platform has the MNL model, the UCB policy of Agrawal et al. (whose bound depends on $N$) and Hoeffding's inequality, but no level-set or trisection analysis. A formal proof would also check the paper's argument, whose printed slips are recorded in the scope section.

Difficulty

The regret concerns a stateful algorithm whose epochs end at random times: an inner iteration takes two periods while exploration is active and one afterwards, and the policy's internal state must be recomputed from the purchase history alone. The obvious argument fixes a confidence level $1/T^2$, bounds each epoch's regret on the event that all confidence intervals hold, and sums a geometric series. That argument loses a $\sqrt{\log T}$ factor, and it is the paper's own Theorem 2. Removing the factor needs confidence levels that weaken as data accumulate. A failure is then no longer rare enough to be ignored, so the analysis has to track its cost. This is done by a recursion on conditional expected regrets across three cases (interval to the right of, containing, or to the left of $\theta^*$), in which a wrong decision in one epoch passes to another case with controlled probability. Within an epoch, the purchases made while exploring a level set must be shown to behave like i.i.d. samples with mean $F(y_\tau)$, although the number of explorations is itself random.

Formalization scope

• Model. The model is the published MNLBandit.UCB.Setting with every subset admissible: histories are sequences of choices in Option (Fin N) (none = no purchase), policies are deterministic functions of the past choices, and expectations are finite sums over histories. Items and periods are 0-based in Lean; epochs and inner iterations are as on the page.
• Policy. The policy is defined exactly. Confidence radius $\sqrt{2\ln(8T/t)/t}$ (δ = 1/T in (12)); $n_\tau = \max(1, 8\lceil(y_\tau-x_\tau)^{-2}\ln(8T(y_\tau-x_\tau)^2)\rceil)$; trisection weights $2/3, 1/3$; the update $b \leftarrow y_\tau$ if and only if $u < y_\tau$; exploitation of $\mathcal L_{a_\tau}$ in every inner iteration; exploration only while $\ell \le y_\tau \le u$.
• Conventions.
  • The $\max(1,\cdot)$ matters only for tiny $T$, where the printed $n_\tau$ is $0$.
  • The empty assortment is allowed (§3 asks $S_t \neq \varnothing$; $R(\varnothing) = 0$).
  • §3's $r_i > 0$ is relaxed to Theorem 3's $r_i \in [0,1]$.
  • $F$ is defined on all of $\mathbb R$, and $F(\theta^+)$ is Mathlib's Function.rightLim.
  • $\theta^*$ is defined as $F^*$.
  • $\psi$ is a ratio of finite sums and is $0$ on a conditioning event of probability $0$.
  • Every $O(\cdot)$ and $\lesssim$ is an existential constant chosen before all other quantities.
• Added hypotheses. Lemma 2 assumes $F^* > 0$, which its proof uses. Lemmas 9 and 10 and (S33) assume $T \ge 25$ and that epoch $\tau$ can start ($\sum_{\tau'<\tau} n_{\tau'} < T$); without these, $\log(T\varepsilon^2)$ can be negative.
• Repairs. Two printed statements are repaired.
  • (S32) is stated with $\exp\{-n_\tau\Delta^2/2\}$, which its printed justification gives; the printed $\exp\{-n_\tau\Delta^2\}$ fails on an explicit instance.
  • Lemma 9 sums from $\tau' = \tau$, as its proof does, with exponent $n_{\tau'}$ and the deterministic last epoch $\bar\tau(T)$ as upper limit.
• Ruled out. Three formalizations would make the goal trivial, and none is admissible: a policy that receives $v$ (it could offer $S^*$ in every period); a constant $C_1$ that depends on $T$, $N$ or the instance (the regret is at most $T$); and an abstract "trisection oracle" with assumed guarantees in place of the algorithm above.
• Not included. Theorem 4 (the $\sqrt T/384$ lower bound) and its Lemmas 12–14 are not part of the mission, and neither are Theorem 2 and its Lemmas 5–7 (the baseline policy) or Proposition 1.
• Contributions welcome. Lemmas 1–4 need only finite sums; Lemma 8 and (S32)/(S33) need Hoeffding's inequality and a union bound over sample sizes; the reduction of exploration purchases to i.i.d. samples is reusable for other level-set policies.

Selected references

• X. Chen, Y. Wang, Y. Zhou, An Optimal Policy for Dynamic Assortment Planning Under Uncapacitated Multinomial Logit Models, arXiv:1805.04785v2, 2019; Mathematics of Operations Research 46(4), 2021. https://arxiv.org/abs/1805.04785
• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5), 2019. https://arxiv.org/abs/1706.03880
• X. Chen, Y. Wang, A note on tight lower bound for MNL-bandit assortment selection models, Operations Research Letters 46(5), 534–537, 2018.
• P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic Assortment Optimization with a Multinomial Logit Choice Model and Capacity Constraint, Operations Research 58(6), 2010. https://doi.org/10.1287/opre.1100.0866
• D. Sauré, A. Zeevi, Optimal Dynamic Assortment Planning with Demand Learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.2013.0429
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• J.-Y. Audibert, S. Bubeck, Minimax Policies for Adversarial and Stochastic Bandits, COLT 2009.

Pricing from censored sales data

A retailer who sets a price for a product with limited inventory usually learns about demand from past sales. When the shelf runs empty, sales record the inventory level rather than the demand. Demand above the stock is lost and never observed. This demand censoring is pervasive in retail and inventory data, and it biases naive estimators of demand curves (Besbes and Muharremoglu, Management Science 2013; Ban, Operations Research 2020). Bu, Simchi-Levi and Wang (SSRN 3619625; Management Science, doi:10.1287/mnsc.2022.4382) ask a basic question about offline (historical) data. The retailer has censored sales at a few past prices and must choose a single new price. When can it, with enough data, guarantee near-optimal revenue no matter what the unobserved part of the demand distribution looks like? The paper answers this exactly, and gives an algorithm that achieves the guarantee whenever it is achievable.

Setting

The retailer has $y \ge 0$ units of inventory and chooses a price $p$ in a known interval $[\underline p, \bar p] \subset (0,\infty)$. Demand is linear: $D(p) = \xi - bp$, where the base demand $\xi$ is random with c.d.f. $F_\xi$, and the price sensitivity $b$ lies in a known interval $[\underline b, \bar b] \subset (0,\infty)$. Demand is nonnegative almost surely at every feasible price. Sales are $\min\{D(p), y\}$, and under a c.d.f. $F$ of $\xi$ the expected revenue is $R_F(p) = p\,\mathbb E_F[\min\{\xi - bp, y\}]$.

Offline data. $K \ge 2$ different historical prices $p_i \in [\underline p, \bar p]$ were used with inventories $y_i$. At pair $i$ there are $N_i$ independent censored sales $S^j_i = \min\{\xi^j_i - bp_i,\ y_i\}$. The data size is $N = \min_i N_i$. A value of $\xi$ is observable only below the observable boundary $\lambda = \max_i\{y_i + bp_i\}$. Write $\gamma = \mathbb P[\xi < \lambda]$, which is assumed positive. Assumption 1 asks that, below $\lambda$, $\xi$ is either discrete with finitely many atoms or has a density, with a slope or density lower bound $\underline g > 0$.

Ambiguity set. No amount of censored data reveals $F_\xi$ on $[\lambda,\infty)$. The set of distributions consistent with the data is $\mathcal F = \{F : F(x) = F_\xi(x)\ \forall x < \lambda\}$. The optimistic and pessimistic revenues are $R_{\max}(p) = \max_{F\in\mathcal F} R_F(p)$ and $R_{\min}(p) = \min_{F\in\mathcal F} R_F(p)$. Their largest maximizers on $[\underline p,\bar p]$ are the optimistic price $p^*_{\max}$ and the pessimistic price $p^*_{\min}$. With $p^*_F$ the largest maximizer of $R_F$, the worst-case revenue loss of a price $p$ is $\max_{F\in\mathcal F}\{R_F(p^*_F) - R_F(p)\}$.

Identifiability. A data-driven algorithm maps the censored data and the public inputs ($y$, the two intervals, the pairs $(p_i, y_i)$) to a feasible price $p^{\mathcal A}$. The problem is identifiable (Definition 1) if some algorithm satisfies $\lim_{N\to\infty}\mathbb P[\max_{F\in\mathcal F}\{R_F(p^*_F) - R_F(p^{\mathcal A})\} < \varepsilon] = 1$ for every $\varepsilon > 0$.

Formalization targets

Goal: Theorem 1

The problem is identifiable if and only if

$$p^*_{\max} = p^*_{\min}.$$

The Lean goal states this in three parts, for every instance satisfying the standing assumptions:

1. the paper's algorithm D2ACD (Algorithm 1) always prices in $[\underline p,\bar p]$, and if $p^*_{\max} = p^*_{\min}$ it satisfies the near-optimality limit;
2. if $p^*_{\max} \ne p^*_{\min}$, every feasible price has worst-case loss at least

$$\frac{\gamma b}{(\sqrt\gamma+1)^2}\,(p^*_{\max} - p^*_{\min})^2 > 0;$$

3. identifiable $\iff p^*_{\max} = p^*_{\min}$.

Milestones

• Structure of the robust revenues. Concavity and projection (Proposition 1); closed forms of $R_{\max}$, $R_{\min}$ with the extremal distributions (Proposition 2); $p^*_{\min} \le p^*_F \le p^*_{\max}$ (Proposition 3); the worst-case loss equals $\max\{R_{\max}(p^*_{\max}) - R_{\max}(p),\ R_{\min}(p^*_{\min}) - R_{\min}(p)\}$ (Proposition 7); the lower bound on the minimax loss $\Delta$ (Proposition 6).
• Concentration. Hoeffding (Lemma A.1, already proved on the platform), Dvoretzky–Kiefer–Wolfowitz for an arbitrary c.d.f. (Lemma A.2), and a uniform deviation bound for bounded monotone functions (Lemma A.3).
• Analysis of D2ACD. Consistency of the sensitivity estimate $\hat b$ (Lemma 1), of the empirical revenue (Lemma D.1) and of the empirical uncensored fraction (Lemma D.2). Uniform convergence of the empirical robust revenues (Lemma 2). The sample-complexity bound $N(\varepsilon,\delta) = C\varepsilon^{-2}\log(8K/\delta)$ with the paper's explicit constant $C$ (Theorem 2).

Significance

Theorem 1 separates censored-data pricing problems into two classes. In identifiable ones, more data eventually yields near-optimal prices. In the others, a positive loss persists however large the sample, and the right benchmark is the minimax loss $\Delta$. The criterion is checkable in terms of two robust optimization problems, the maximax and the maximin. The constructive half comes with an algorithm that uses only observable data and has sample complexity $O(\varepsilon^{-2}\log(1/\delta))$, matching data-driven newsvendor results without censoring (Levi, Perakis and Uichanco, Operations Research 2015).

The results are proved in the paper. None of them, and none of the model, is formalized. The mission formalizes the model, the ambiguity set, the algorithm and the full chain of the proof. It includes two concentration inequalities not yet available in Lean in the needed form: DKW with Massart's constant for distributions with atoms, and a uniform bound over monotone function classes.

Difficulty

The algorithm sees only the censored data. A proof that silently uses $b$ or $F_\xi$ to pick the price does not establish the theorem. The obvious estimator of $b$, least squares on observed sales, is biased by censoring. D2ACD instead regresses empirical quantiles at the level $\hat\gamma_{\min}$, below which the data are uncensored. Its analysis needs a lower bound on the slope of the c.d.f. (Assumption 1), and a uniform-in-price comparison of piecewise empirical revenues whose breakpoint $\hat{\tilde p}$ is itself random. On the other side, the lower bound requires the exact extremal distributions in $\mathcal F$. The optimistic one sends the unobserved mass beyond every relevant demand level. The pessimistic one puts it at the boundary $\lambda$.

Formalization scope

Representation. c.d.f.s are probability measures on $\mathbb R$. $F \in \mathcal F$ means agreement with $F_\xi$ on every half-line $(-\infty, x]$, $x < \lambda$, so an atom at $\lambda$ is allowed. $R_{\max}$, $R_{\min}$, the worst-case loss and $\Delta$ are defined as suprema and infima. Their attainment is part of the milestones, so no statement is true through a junk value. "$\max\{\arg\max\}$" is the supremum of the set of maximizers. The data are base-demand samples $\xi^j_i$ under the product law, mapped to censored sales. An algorithm is a function of the sample sizes and the censored sales for fixed public inputs. Failure probabilities are outer measures. The limit $N \to \infty$ is over all sample-size vectors with $\min_i N_i \to \infty$.

Standing assumptions and disclosed choices. The data equation is $S^j_i = \min\{\xi^j_i - bp_i, y_i\}$; the page drops $b$ once. The continuous branch of Assumption 1 bounds the density on $[\ell, \lambda)$, with $\ell$ a lower bound of the support. The printed $[0,\lambda)$ contradicts nonnegative demand together with $\gamma > 0$. The historical prices are pairwise different, as the text says. The finite-sample statements (Lemmas 1, 2, Theorem 2) are made on the data assumption $\hat\gamma_i > 0$ for all $i$, as on p. 10; the goal is not. In D2ACD, $\hat b$ is the clamp of the least-squares slope to $[\underline b, \bar b]$, which is the arg min of line 9. Ties go to the largest price and the least index. The output is $\underline p$ when some sample is empty.

Trivializing readings ruled out. Definition 1 fixes the instance before asking for an algorithm, so a constant algorithm returning $p^*_{\max}$ witnesses the bare equivalence. For that reason the goal names D2ACD, a definition taking only the public inputs and the censored sales, and states the quantitative lower bound for the other direction. Two sanity instances, one discrete and one uniform, satisfy every standing assumption, so the hypotheses are not vacuous.

Contributions welcome. Proofs of any milestone. The concentration lemmas A.2 and A.3 are reusable well beyond this mission. Propositions 1–3, 6 and 7 are deterministic convex-analysis arguments about the two robust revenue curves and are a natural starting point.

Selected references

• J. Bu, D. Simchi-Levi, L. Wang, Offline Pricing and Demand Learning with Censored Data, Management Science, 2022 (SSRN 3619625, PDF of 2021-08-23). https://ssrn.com/abstract=3619625, https://doi.org/10.1287/mnsc.2022.4382
• P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Annals of Probability 18(3), 1990. https://doi.org/10.1214/aop/1176990746
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58, 1963. https://doi.org/10.1080/01621459.1963.10500830
• O. Besbes, A. Muharremoglu, On implications of demand censoring in the newsvendor problem, Management Science 59(6), 1407–1424, 2013.
• G.-Y. Ban, Confidence intervals for data-driven inventory policies with demand censoring, Operations Research 68(2), 309–326, 2020.
• R. Levi, G. Perakis, J. Uichanco, The data-driven newsvendor problem: new bounds and insights, Operations Research 63(6), 2015.

Motivation

Models of Bayesian social learning describe agents in a network who each receive a private signal about an unknown state of the world, observe the actions of their neighbours over time, and act optimally given everything they have seen. They are used in economics, operations research and the study of collective decision making to ask whether groups aggregate dispersed information, and they presuppose that every agent can carry out the Bayesian update. Hązła, Jadbabaie, Mossel and Rahimian (arXiv:1705.04770, Operations Research 2021) show that this presupposition fails in general: already at the second round of interaction, computing a Bayesian agent's action is NP-hard (their Theorem 1). The proof is a reduction from approximate VERTEX-COVER. This mission formalizes the mathematical core of that reduction: in the network built from a graph, the belief of one designated agent at time two is pushed to opposite extremes by graphs with small vertex covers and by graphs whose vertex covers are all large.

Setting

A finite set of agents is given, and every agent $i$ has a neighbourhood $\mathcal N_i$ of agents whose actions she observes, with $i \in \mathcal N_i$. The state is $\theta \in \{0,1\}$, drawn from the uniform prior $\nu(0) = \nu(1) = \tfrac12$. Agent $i$ receives a private signal $s_i \in \{0,1\}$ with law $\mathbb P_{i,\theta}$; conditionally on $\theta$ the signals are independent, so a signal profile $s$ has probability $\mathbb P_\theta(s) = \prod_i \mathbb P_{i,\theta}(s_i)$.

At every time $t = 0, 1, 2, \dots$ agent $i$ knows her own signal and the actions $a_{j,\tau}$ of all $j \in \mathcal N_i$ at times $\tau < t$. Her information set $\mathcal I_{i,t}(s)$ is the set of profiles $s'$ that agree with $s$ in $s_i$ and in all those actions. Her belief is the posterior (4)

$$\mu_{i,t}(\theta) = \frac{\nu(\theta)\sum_{s' \in \mathcal I_{i,t}} \mathbb P_\theta(s')}{\sum_{\theta'} \nu(\theta')\sum_{s' \in \mathcal I_{i,t}} \mathbb P_{\theta'}(s')},$$

and in the binary action model (utility $\mathbf 1(a = \theta)$) her action $a_{i,t}$ is the more likely state, with ties broken towards $0$. Actions at time $t$ depend on information sets at time $t$, which depend on actions at earlier times, so all of these are defined together by recursion on $t$. The log-belief ratio is $\phi_{i,t} = \log(\mu_{i,t}(1)/\mu_{i,t}(0))$.

The reduction network for a simple graph $G$ with $n$ vertices and $m$ edges has $n + m + 2$ agents: a vertex agent $\tau_v$ for each vertex, observing only herself, with $\mathbb P_{\tau,1}(1) = \bar p = 0.4$ and $\mathbb P_{\tau,0}(1) = \underline p = 0.3$; an edge agent $\varepsilon_e$ for each edge $e = \{u,w\}$, observing $\tau_u$, $\tau_w$ and herself, with an uninformative signal; an agent $\kappa$ observing only herself; and the agent $i$, with an uninformative signal, observing $\kappa$ and all edge agents. With $\bar q(\alpha) = \bar p^\alpha(1-\bar p)^{1-\alpha}$, $\underline q(\alpha) = \underline p^\alpha(1-\underline p)^{1-\alpha}$ and $\tilde q(\alpha) = \log(\bar q(\alpha)/\underline q(\alpha))$, agent $\kappa$'s signal is chosen so that

$$\lambda_\kappa(0) = \log\frac{\mathbb P_{\kappa,1}(0)}{\mathbb P_{\kappa,0}(0)} = -\frac n2\bigl(\tilde q(0.998) + \tilde q(0.999)\bigr).$$

Agent $i$'s observed history is: every edge agent announces $a_{\varepsilon,1} = 1$, and $\kappa$ announces $a_{\kappa,0} = 0$.

Formalization targets

Goal: Theorem 6, belief clauses (p. 27)

There are $c > 0$ and $N$ such that for every $n \ge N$, every graph $G$ on $n$ vertices, every admissible signal structure of $\kappa$, and every signal profile producing the observed history:

$$G \text{ has a vertex cover of size} \le 0.85n \implies \mu_{i,2}(1) < e^{-cn},$$ $$\text{every vertex cover of } G \text{ has size} \ge 0.999n \implies \mu_{i,2}(0) < e^{-cn}.$$

The constant $c$ is not fixed: the paper writes $\exp(-\Omega(n))$.

Milestones

1. Example 1, (3), p. 8: time-zero actions reveal informative signals, and $\phi_{i,1} = \sum_{j \in \mathcal N_i}\lambda_j$.
2. Fact 1, p. 28: $a_{\varepsilon,1} = 1$ iff one of the edge's endpoints has signal $1$.
3. Fact 2, p. 28: the vertices with signal $1$ form a vertex cover iff all edge agents announce $1$.
4. (12), p. 29: $\phi_{i,2}$ is the log-ratio of $\sum_{\hat\Sigma}\bar p^{|\hat\Sigma|}(1-\bar p)^{n-|\hat\Sigma|}$ and $\sum_{\hat\Sigma}\underline p^{|\hat\Sigma|}(1-\underline p)^{n-|\hat\Sigma|}$ over vertex covers $\hat\Sigma$, plus $\lambda_\kappa(0)$.
5. (13), p. 29: in the NO case, $\phi_{i,2} > \frac n2(\tilde q(0.999) - \tilde q(0.998))$.
6. Theorem 7, pp. 29–30: $\Pr\{\sum_k s_k \ge \alpha n\} \le \exp(-nD_{KL}(\alpha\|p))$ for i.i.d. Bernoulli($p$) and $p \le \alpha \le 1$.
7. (16), p. 30: $\mathbb P_1\{|\Sigma| > 0.998n\} \le \exp(-nD_{KL}(0.998\|0.4)) < 0.41^n$.
8. (17), p. 30: a set of at most $0.85n$ vertices has $\mathbb P_1$-probability at least $\bar q(0.85)^n > 0.42^n$.
9. (18), p. 30: in the YES case, $\phi_{i,2} < n\tilde q(0.998) + \log(1 + (0.41/0.42)^n) - \frac n2(\tilde q(0.999) + \tilde q(0.998))$.

Significance

Theorem 6 is the step that turns a statement about vertex covers into a statement about beliefs. Together with the NP-hardness of distinguishing graphs with a vertex cover of size $0.85n$ from graphs with no vertex cover smaller than $0.999n$ (Theorem 5, from Khot, Minzer and Safra's proof of the 2-to-2 games theorem), it shows that no polynomial-time algorithm computes the time-two action of a Bayesian agent unless P = NP, and that even approximating the belief is hard, since the two cases differ by exponentially small versus exponentially close to one. This sets a limit on rational-agent models of social learning as descriptions of behaviour and motivates bounded-rationality alternatives.

The result is proved in the paper; to the best of current knowledge it has not been formalized. The mission produces a machine-checked model of Bayesian group decision making on a network, with information sets defined by recursion on time, reusable for other results about Bayesian learning on graphs, and a finite Chernoff bound in Kullback–Leibler form. The NP-hardness itself is not part of the mission: it needs a model of computation and inherits its hardness from a cited theorem.

Difficulty

The model's information sets are defined by a recursion in which every agent simulates what every neighbour could have seen. The first obstacle is to compute the time-two information set of agent $i$ in closed form: one must check that the actions of agent $i$ and $\kappa$ at earlier times, and of the edge agents at time zero, carry no additional information, and that the edge agents' time-one actions reveal exactly whether the vertex signals form a vertex cover. Then the posterior becomes a ratio of two weighted counts of vertex covers. A naive bound comparing the two sums term by term does not separate the YES and NO cases, because the sums are dominated by different covers; in the YES case the large covers must be discarded using a tail bound whose exponent beats the likelihood of a single small cover, which is where the constants $0.41 < 0.42$ enter.

Formalization scope

States, signals and actions are Bool (false = 0). A network is BinNet (neighbourhoods with $i \in \mathcal N_i$, and $\mathbb P_{i,\theta}(1)$); post, mapAct, infoSet, act, logBelief are (4), the MAP action with ties to $0$, $\mathcal I_{i,t}$, $a_{i,t}$ and $\phi_{i,t}$. Information sets contain the conjunct $s'_i = s_i$ from the history of (1). The reduction network is vcNet G k₀ k₁ for G : SimpleGraph (Fin n), on the agent type Agent n G (vertex agents, edge agents indexed by G.edgeSet, iAg, kap), with $k_\theta = \mathbb P_{\kappa,\theta}(0)$ quantified over all pairs in $(0,1)$ with $\log(k_1/k_0) = \lambda_\kappa(0)$. Vertex covers are Mathlib's SimpleGraph.IsVertexCover. Decimals are exact rationals; $0.85n$, $0.998n$, $0.999n$ are compared as real numbers. Probabilities of events on the vertex signals are written as finite sums of $p^{|C|}(1-p)^{n-|C|}$ over subsets $C$. $D_{KL}$ is the published bernoulliRelativeEntropy. $n$ is the number of graph vertices, not of agents.

The goal is about the model's own posterior on the model's own information set, for every profile on which the model's actions produce the history; it is not stated about a hand-written ratio of sums, which would skip the model. The constants $c$ and $N$ are quantified before the graph and before $\kappa$'s parameters, so they cannot depend on the instance. The complexity clauses of Theorem 6 (a polynomial-time reduction, the bounds (9)) and Theorem 1's NP-hardness are not formalized.

Contributions welcome: closed-form computations of early information sets in the model, the finite Chernoff bound (Theorem 7; the published Proved MassartDKW.Binom.comment_3 is the strict-tail Cramér–Chernoff bound for binomial n p), and the numerical inequalities of (16) and (17).

Selected references

• J. Hązła, A. Jadbabaie, E. Mossel, M. A. Rahimian, Bayesian Decision Making in Groups is Hard, arXiv:1705.04770v4, 2019; Operations Research 69(2), 2021. https://arxiv.org/abs/1705.04770
• S. Khot, D. Minzer, M. Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, FOCS 2018. https://doi.org/10.1109/FOCS.2018.00062
• P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Annals of Probability 18(3), 1990. https://doi.org/10.1214/aop/1176990746

Motivation

Selecting a valuable subset subject to several simultaneous restrictions is a common combinatorial optimization problem. A facility may contribute less after nearby facilities have already been selected; a collection of observations may provide overlapping information. Such diminishing returns are captured by submodular objectives. Matroid constraints describe families of admissible selections that are closed under deletion and satisfy an exchange rule. Requiring a selection to satisfy several matroids permits overlapping restrictions on the same elements.

Lee, Sviridenko and Vondrák study this model with access to objective values and independence tests through oracles. Their main monotone guarantee is a polynomial approximation factor of $1/(k+\delta)$ for any fixed number $k\ge2$ of matroids and fixed $\delta>0$. The source compares this with the earlier $1/(k+1)$ greedy guarantee. This mission formalizes the published monotone result and its supporting exchange statements, with the constants and algorithmic quantifiers intact (Introduction and Theorem 3.1).

Setting

The ground set is a finite set $N$ of $n$ elements. A submodular function assigns a real number $f(S)$ to every subset $S\subseteq N$ and satisfies

$$f(A\cup B)+f(A\cap B)\le f(A)+f(B).$$

All objective values in the faithful source statements are nonnegative. For the headline theorem the function is also nondecreasing: $A\subseteq B$ implies $f(A)\le f(B)$. The empty set need not have value zero.

A matroid on $N$ is a family of independent sets containing the empty set, closed under taking subsets, and satisfying augmentation: a smaller independent set can gain an element from a larger independent set while remaining independent. There are $k$ such matroids, all on the same ground set. A set is common independent, or feasible, when it is independent in every one of them. The quantity $\mathrm{OPT}$ is the maximum of $f$ over feasible subsets. This maximum exists even when $N$ is empty, since there are finitely many subsets and the empty set is feasible.

An algorithm receives a value oracle for $f$ and one independence oracle for each matroid. A value query specifies a subset and returns its value; an independence query specifies a matroid and a subset and returns a yes-or-no answer. Real arithmetic and comparisons use the unit-cost oracle convention. No table of all objective values is supplied (Introduction, p. 795).

Formalization targets

The goal is the first sentence of Theorem 3.1. For each fixed $k\ge2$ and $\delta>0$, there must exist one finite oracle program and polynomial constants, depending only on those fixed parameters, such that on every instance it halts and returns a feasible set $S$ with

$$f(S)\ge\frac{\mathrm{OPT}}{k+\delta}.$$

The time bound includes initialization, oracle queries, subset processing, unsuccessful searches, and output. It is not merely a bound on the number of improving moves (Theorem 3.1, p. 803).

The eleven supporting milestones follow the source's numbered statements. They cover perfect matching for equal-size independent sets; irreducible cycle covers; the independence consequence of a unique perfect matching; feasibility of irreducible cycles; feasible path and cycle covers; exact-cover addition; generalized Rota exchange; bounded-multiplicity exchange for independent sets; exact-cover removal; and exact and approximate local-search inequalities. The order follows the dependencies identified in §§1–3. The exact local-search bound is

$$\left(k+\frac1p\right)f(S)\ge f(S\cup C)+\left(k-1+\frac1p\right)f(S\cap C),$$

with a factor $1+\varepsilon$ on the left in the approximate version. Here $p\ge1$ is an integer, $C$ is any feasible set, and the objective may be nonmonotone (Lemmas 3.1–3.2).

Significance

The approximation theorem gives a quantitative guarantee for general matroid intersections with a submodular objective. Restricting the constraints to partition matroids, or proving that a good set exists without a polynomial computation, would lose part of the result. The supporting exchange statements also describe how independent sets can be related when individual exchanges cannot simply be combined across constraints (§§2–3).

The mathematics is a published result; this mission asks for machine-checked proofs of its formal statements. The submodularity predicate is reused from an existing published definition. Lemma 2.1 is anchored to an existing Open bijective exchange theorem through a contraction and graph interpretation, rather than posed again. Open means that its proof remains a target. The remaining statements and the operational oracle model are local drafts, and compiling their statements does not prove them.

Difficulty

A chain of individually feasible swaps need not give a feasible simultaneous exchange. The source's distinction between an arbitrary directed cycle and an irreducible one therefore matters. Feasibility of a path or cycle also includes every eligible subpath, not just the whole vertex-set swap. Losing either distinction changes the supporting exchange results (Definitions 2.1–2.2).

Polynomial computation is a separate obligation from local-optimum quality. Literal Figure 1 admits infeasible singleton initialization when loops are present and nontermination at zero value under its non-strict update test. These issues are recorded as findings about the displayed routine, while the existential headline retains all inputs. Two further findings identify missing witness properties and an invalid intermediate path-count estimate in the printed analysis; they do not establish falsity of the numbered local-search inequalities. Proofs must resolve those obligations without importing them as assumptions (pp. 802–803).

Formalization scope

Lean represents $N$ by Fin n, subsets by finite sets, objective values by real numbers, and matroids by Mathlib matroids with ground set equal to the whole finite type. Indexed families preserve repeated sets and repeated paths or cycles. Paths may consist of one vertex, cycles may have two vertices, and the cover multiplicity is $2^s$, including $s=0$. There is no looplessness, normalization, positive-optimum, or equal-cardinality restriction on the headline inputs.

The algorithmic goal uses a finite register-machine language whose only input-dependent operations are the two types of oracle queries. An explicit halt and a bound on the full execution cost are conclusions. Definitions contain neither an approximation guarantee nor an assumed polynomial stopping bound. The terminal predicate for Figure 1 uses strict inequality because the printed update uses greater-than-or-equal. Empty and zero-value inputs belong to the headline theorem even though the literal terminal predicate need not describe them.

The stronger linear-objective sentence of Theorem 3.1, the nonmonotone algorithm of Theorem 4.1, and the tightness examples in §5 are outside this mission. No optional variants are posed. Contributions needed here include the source theorem proofs, the exchange adapter, and the operational algorithm witness and its accounting.

Selected references

• Jon Lee, Maxim Sviridenko and Jan Vondrák, Submodular Maximization over Multiple Matroids via Generalized Exchange Properties, Mathematics of Operations Research 35(4), 795–806, 2010. Published journal article. All result numbering and page references use this artifact; PDF pages 1–12 correspond to printed pages 795–806.