All missions

Motivation

A strong converse theorem for the classical capacity of a quantum channel states that the probability of correctly decoding a classical message converges exponentially fast to zero in the limit of many channel uses if the rate of communication exceeds the classical capacity of the channel. Along with a corresponding achievability statement for rates below the capacity, such a strong converse theorem enhances our understanding of the capacity as a very sharp dividing line between achievable and unachievable rates of communication. Here, we show that such a strong converse theorem holds for the classical capacity of all entanglement-breaking channels and all Hadamard channels (the complementary channels of the former). These results follow by bounding the success probability in terms of a "sandwiched" Renyi relative entropy, by showing that this quantity is subadditive for all entanglement-breaking and Hadamard channels, and by relating this quantity to the Holevo capacity. Prior results regarding strong converse theorems for particular covariant channels emerge as a special case of our results.

This mission is the statement-level formalization of Strong converse for the classical capacity of entanglement-breaking and Hadamard channels via a sandwiched Renyi relative entropy (arXiv:1306.1586v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exponential strong converse for entanglement-breaking and Hadamard channels (seed, 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.

Selected references

• Strong converse for the classical capacity of entanglement-breaking and Hadamard channels via a sandwiched Renyi relative entropy, arXiv:1306.1586v4, https://arxiv.org/abs/1306.1586v4

Motivation

The one-shot classical capacity of a quantum channel quantifies the amount of classical information that can be transmitted through a single use of the channel such that the error probability is below a certain threshold. In this work, we show that this capacity is well approximated by a relative-entropy-type measure defined via hypothesis testing. Combined with a quantum version of Stein's lemma, our results give a conceptually simple proof of the well-known Holevo-Schumacher-Westmoreland theorem for the capacity of memoryless channels. More generally, we obtain tight capacity formulas for arbitrary (not necessarily memoryless) channels.

This mission is the statement-level formalization of One-Shot Classical-Quantum Capacity and Hypothesis Testing (arXiv:1007.5456v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-sided one-shot classical-quantum capacity bounds (Theorem 1, (3): two-sided epsilon-one-shot classical-quantum capacity bounds, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Unnumbered strengthened achievability, (7): A meaningful finite-code attainment formulation for (7) on arbitrary unbounded channels, and the positive logarithm denominator domain. (source-ambiguity)
• Computational assertion after (1): Finite-dimensional numerical input encoding, precision objective, and complexity guarantee for the sentence after (1). (source-ambiguity)

Selected references

• One-Shot Classical-Quantum Capacity and Hypothesis Testing, arXiv:1007.5456v3, https://arxiv.org/abs/1007.5456v3

Motivation

The quantum relative entropy is frequently used as a distance measure between two quantum states, and inequalities relating it to other distance measures are important mathematical tools in many areas of quantum information theory. We have derived many such inequalities in our previous work (K.M.R. Audenaert and J. Eisert, J. Math. Phys. 46, 102104 (2005)). The present paper is a follow-up on this, and provides sharp upper bounds on the relative entropy in terms of the trace norm distance and of the smallest eigenvalues of both states concerned. The results obtained here are more general than the corresponding one from our previous work, and also corrects a mistake in one of its proofs. As a by-product, we obtain a sharp upper bound on the regularised relative entropy introduced by Lendi, Farhadmotamed and van Wonderen.

This mission is the statement-level formalization of Continuity bounds on the quantum relative entropy - II (arXiv:1105.2656v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Relative entropy bound using both smallest eigenvalues (Theorem 1: upper bound with both minimum eigenvalues (17)–(18), 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:

• Lemma 1, arbitrary path, (11): A specified integral convention or regularity class making the arbitrary-path fundamental-theorem step valid. (source-ambiguity)
• Remark following Theorem 1: A correct intended quantifier for the asserted dimension-three necessity. (source-ambiguity)

Selected references

• Continuity bounds on the quantum relative entropy - II, arXiv:1105.2656v3, https://arxiv.org/abs/1105.2656v3

Motivation

Quantum f-divergences are a quantum generalization of the classical notion of f-divergences, and are a special case of Petz' quasi-entropies. Many well known distinguishability measures of quantum states are given by, or derived from, f-divergences; special examples include the quantum relative entropy, the Renyi relative entropies, and the Chernoff and Hoeffding measures. Here we show that the quantum f-divergences are monotonic under the dual of Schwarz maps whenever the defining function is operator convex. This extends and unifies all previously known monotonicity results. We also analyze the case where the monotonicity inequality holds with equality, and extend Petz' reversibility theorem for a large class of f-divergences and other distinguishability measures. We apply our findings to the problem of quantum error correction, and show that if a stochastic map preserves the pairwise distinguishability on a set of states, as measured by a suitable f-divergence, then its action can be reversed on that set by another stochastic map that can be constructed from the original one in a canonical way. We also provide an integral representation for operator convex functions on the positive half-line, which is the main ingredient in extending previously known results on the monotonicity inequality and the case of equality. We also consider some special cases where the convexity of f is sufficient for the monotonicity, and obtain the inverse Holder inequality for operators as an application. The presentation is completely self-contained and requires only standard knowledge of matrix analysis.

This mission is the statement-level formalization of Quantum f-divergences and error correction (arXiv:1008.2529v6). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

53 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract main result (p.1), pinned to Theorem 7.1 (Theorem 7.1 (abstract main result), PDF p. 33). 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

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

• Corollary 5.3: A corrected statement with the missing hypothesis or corrected formula, retaining the printed scope. (source-ambiguity)
• Remark 6.2, endpoint derivative identities 6.2-derivatives: A corrected statement with the missing hypothesis or corrected formula, retaining the printed scope. (source-ambiguity)
• Remark 6.11: A corrected statement with the missing hypothesis or corrected formula, retaining the printed scope. (source-ambiguity)
• Proposition 7.3: A corrected statement with the missing hypothesis or corrected formula, retaining the printed scope. (source-ambiguity)
• Theorem 7.7: Separate background provenance and exact full-scope reuse certification. (hard)
• Theorem 7.8: Separate background provenance and exact full-scope reuse certification. (hard)
• Lemma A.1: Separate background provenance and exact full-scope reuse certification. (hard)
• Lemma A.2: Separate background provenance and exact full-scope reuse certification. (hard)
• Proposition A.3: A corrected statement with the missing hypothesis or corrected formula, retaining the printed scope. (source-ambiguity)

Selected references

• Quantum f-divergences and error correction, arXiv:1008.2529v6, https://arxiv.org/abs/1008.2529v6

Motivation

We prove a lower bound on the relative entropy between two finite-dimensional states in terms of their entropy difference and the dimension of the underlying space. The inequality is tight in the sense that equality can be attained for any prescribed value of the entropy difference, both for quantum and classical systems. We outline implications for information theory and thermodynamics, such as a necessary condition for a process to be close to thermodynamic reversibility, or an easily computable lower bound on the classical channel capacity. Furthermore, we derive a tight upper bound, uniform for all states of a given dimension, on the variance of the surprisal, whose thermodynamic meaning is that of heat capacity.

This mission is the statement-level formalization of Tight bound on relative entropy by entropy difference (arXiv:1304.0036v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

25 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Tight relative entropy bound and explicit equality witnesses (theorem1, 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

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

• Eq. (33): Definition of W_waste and admissible cyclic completions for unequal bath temperatures (source-ambiguity)
• Conjecture 12: Established proof status for the asymmetry assertion in Conjecture 12 (hard)

Selected references

• Tight bound on relative entropy by entropy difference, arXiv:1304.0036v3, https://arxiv.org/abs/1304.0036v3

Motivation

We derive one-shot upper bounds for quantum noisy channel codes. We do so by regarding a channel code as a bipartite operation with an encoder belonging to the sender and a decoder belonging to the receiver, and imposing constraints on the bipartite operation. We investigate the power of codes whose bipartite operation is non-signalling from Alice to Bob, positive-partial transpose (PPT) preserving, or both, and derive a simple semidefinite program for the achievable entanglement fidelity. Using the semidefinite program, we show that the non-signalling assisted quantum capacity for memoryless channels is equal to the entanglement-assisted capacity. We also relate our PPT-preserving codes and the PPT-preserving entanglement distillation protocols studied by Rains. Applying these results to a concrete example, the 3-dimensional Werner-Holevo channel, we find that codes that are non-signalling and PPT-preserving can be strictly less powerful than codes satisfying either one of the constraints, and therefore provide a tighter bound for unassisted codes. Furthermore, PPT-preserving non-signalling codes can send one qubit perfectly over two uses of the channel, which has no quantum capacity. We discuss whether this can be interpreted as a form of superactivation of quantum capacity.

This mission is the statement-level formalization of On the power of PPT-preserving and non-signalling codes (arXiv:1406.7142v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract main result; §V (49): non-signalling and entanglement-assisted quantum capacities coincide (Abstract main result; §V (49): non-signalling and entanglement-assisted quantum capacities coincide, 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

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

• Proposition 5: compact dual with absolute operator: Proposition 5: compact dual with absolute operator (source-ambiguity)
• §V (46), literal arbitrary-superclass generalization: §V (46), literal arbitrary-superclass generalization (source-ambiguity)
• §VII.A, Fig.5: fixed-rate numerical separation discussion: §VII.A, Fig.5: fixed-rate numerical separation discussion (source-ambiguity)
• Appendix B (B1): literal arbitrary-channel permutation twirl claim: Appendix B (B1): literal arbitrary-channel permutation twirl claim (source-ambiguity)

Selected references

• On the power of PPT-preserving and non-signalling codes, arXiv:1406.7142v2, https://arxiv.org/abs/1406.7142v2

Motivation

We study a protocol in which many parties use quantum communication to transfer a shared state to a receiver without communicating with each other. This protocol is a multiparty version of the fully quantum Slepian-Wolf protocol for two senders and arises through the repeated application of the two-sender protocol. We describe bounds on the achievable rate region for the distributed compression problem. The inner bound arises by expressing the achievable rate region for our protocol in terms of its vertices and extreme rays and, equivalently, in terms of facet inequalities. We also prove an outer bound on all possible rates for distributed compression based on the multiparty squashed entanglement, a measure of multiparty entanglement.

This mission is the statement-level formalization of Distributed Compression and Multiparty Squashed Entanglement (arXiv:0707.2792v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem II.1: multiparty distributed compression inner bound (seed paper result) (Theorem II.1: multiparty distributed compression inner bound (seed paper result), PDF p. 5). 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

• Distributed Compression and Multiparty Squashed Entanglement, arXiv:0707.2792v2, https://arxiv.org/abs/0707.2792v2

Motivation

The quantum capacity of a memoryless channel is often used as a single figure of merit to characterize its ability to transmit quantum information coherently. The capacity determines the maximal rate at which we can code reliably over asymptotically many uses of the channel. We argue that this asymptotic treatment is insufficient to the point of being irrelevant in the quantum setting where decoherence severely limits our ability to manipulate large quantum systems in the encoder and decoder. For all practical purposes we should instead focus on the trade-off between three parameters: the rate of the code, the number of coherent uses of the channel, and the fidelity of the transmission. The aim is then to specify the region determined by allowed combinations of these parameters. Towards this goal, we find approximate and exact characterizations of the region of allowed triplets for the qubit dephasing channel and for the erasure channel with classical post-processing assistance. In each case the region is parametrized by a second channel parameter, the quantum channel dispersion. In the process we also develop several general inner (achievable) and outer (converse) bounds on the coding region that are valid for all finite-dimensional quantum channels and can be computed efficiently. Applied to the depolarizing channel, this allows us to determine a lower bound on the number of coherent uses of the channel necessary to witness super-additivity of the coherent information.

This mission is the statement-level formalization of Quantum Coding with Finite Resources (arXiv:1504.04617v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Qubit dephasing: third-order boundary (Result 1, Eq. (6), 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

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

• Result 1: printed zero-dispersion cases: A corrected third-order operational expansion at gamma=0,1/2,1. (source-ambiguity)
• Result 3, Eq. (12): printed depolarizing/dephasing boundary comparison: A proof or operational conversion establishing the exact depolarizing/dephasing rate-boundary comparison, with assistance specified. (source-ambiguity)
• Lemma 4 [24, Proposition 20], Eq. (45): cited one-shot achievability: An audited integer-message entanglement-generation-to-transmission and purified-distance-to-squared-fidelity one-shot conversion. (source-ambiguity)
• Unnumbered §V.A, Eqs. (53)–(56): matching covariant generalized-dephasing bounds: A specified covariance/input-twirling representation and quantified maximally correlated support condition for the general class. (source-ambiguity)
• Unnumbered §II.A: claimed equivalence of complete BSC and dephasing regions: A code conversion in both directions identifying exact optimal BSC and dephasing message sizes at every block length and error. (source-ambiguity)
• Unnumbered conclusion Eq. (74): entanglement-assisted expansion: A complete paper-local entanglement-assisted quantum code boundary, its link to the classical boundary at integer dimensions, and the optimizer-based mutual-information variance. (hard)
• Unnumbered conclusion Eq. (75): printed assisted dephasing specialization: A complete paper-local entanglement-assisted quantum code boundary, its link to the classical boundary at integer dimensions, and the optimizer-based mutual-information variance. (hard)

Selected references

• Quantum Coding with Finite Resources, arXiv:1504.04617v2, https://arxiv.org/abs/1504.04617v2

Motivation

Determining the ultimate classical information carrying capacity of electromagnetic waves requires quantum-mechanical analysis to properly account for the bosonic nature of these waves. Recent work has established capacity theorems for bosonic single-user and broadcast channels, under the presumption of two minimum output entropy conjectures. Despite considerable accumulated evidence that supports the validity of these conjectures, they have yet to be proven. In this paper, it is shown that the second conjecture suffices to prove the classical capacity of the bosonic wiretap channel, which in turn would also prove the quantum capacity of the lossy bosonic channel. The preceding minimum output entropy conjectures are then shown to be simple consequences of an Entropy Photon-Number Inequality (EPnI), which is a conjectured quantum-mechanical analog of the Entropy Power Inequality (EPI) form classical information theory.

This mission is the statement-level formalization of Capacity of the Bosonic Wiretap Channel and the Entropy Photon-Number Inequality (arXiv:0801.0841v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Conditional bosonic private capacity, additivity and Gaussian coherent achievability (§III, unnumbered Theorem, (10): conditional bosonic wiretap privacy capacity, additivity and coherent-state achievability, 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.

Deferred results

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

• §IV.B, (22)–(23): the EPnI conjecture itself: An unconditional proof of EPnI, explicitly conjectural in this source. (hard)
• Abstract and §VI: ultimate quantum-capacity interpretation: The source choice of energy-constrained operational quantum encoders, error and energy convention. (source-ambiguity)
• §VI final sentence: coherent-state encoding for both capacities: An actual quantum transmission encoder on arbitrary unknown inputs corresponding to the final coherent-state wording. (source-ambiguity)
• §I, (1): Shannon complex AWGN capacity: A source-matched operational complex AWGN coding theorem with mean-square input constraint. (hard)
• §I, (2)–(3): ideal homodyne and heterodyne capacities: Noisy single-user ideal homodyne/heterodyne instruments and operational coding theorem over all source eta,N,Nbar. (hard)
• §I: cited exact classical pure-loss capacity: The cited operational classical loss-channel capacity theorem, fully matched in nats and average energy. (hard)
• §I: thermal-channel lower bound and conditional equality: The cited thermal-channel operational lower bound and conditional equality theorem. (hard)
• §I and §V: cited conditional bosonic broadcast capacity region: The cited full rate-region inequalities and broadcast coding assumptions. (hard)
• §I: cited Gaussian restrictions of both entropy conjectures: Exact Gaussian input classes in both cited entropy-conjecture restrictions and their equivalence. (source-ambiguity)
• §II historical paragraph: Wyner and Csiszar–Korner coding theorems: Both historical rate-equivocation region formulas, domains, auxiliary alphabets and Markov conditions. (hard)
• §II, (6)–(7): finite-dimensional quantum private-capacity formulas: The complete cited finite-dimensional private-capacity model, including the unprinted auxiliary constraint and correct message secrecy. (source-ambiguity)
• §II, (5) and adjacent definition: Holevo information and accessible leakage: A valid relation replacing the literal accessible-secrecy/Holevo-secrecy equivalence and message/random-index confusion. (source-ambiguity)
• §III, (11): cited additivity and single-letter private/quantum equality: The original complementary degradable-channel theorem with its actual dimension and energy domain. (hard)
• §III: cited independently obtained unconstrained quantum-capacity limit: The cited unconditional operational bosonic quantum-capacity theorem and exact coding conventions. (hard)
• §IV.A, (13)–(17): classical EPI and its purported equivalent forms: A consistent real-vector entropy-power normalization and a complete differential-entropy domain. (source-ambiguity)

Selected references

• Capacity of the Bosonic Wiretap Channel and the Entropy Photon-Number Inequality, arXiv:0801.0841v1, https://arxiv.org/abs/0801.0841v1

Production decisions under financial risk

A firm that commits to a production quantity $Q$ before demand is known faces the classical newsvendor trade-off between overstock and lost sales. When demand moves with the price of a traded asset, such as farm-equipment sales with corn futures or car sales with a stock index, part of the demand risk can be hedged in the financial market. Wang and Yao (SSRN 3875464, April 2020; published in Operations Research, 2023, doi:10.1287/opre.2022.2423) solve the problem of choosing the production quantity and a dynamic hedge together. They measure risk by the conditional value-at-risk (CVaR) of terminal wealth and cap hedging losses by a budget.

CVaR is the standard coherent risk measure in operations and finance. Its convex representation by Rockafellar and Uryasev (2000) turns CVaR maximization into a joint optimization over a decision and a target level $m$, with the shortfall $\mathsf E[(m-\text{wealth})^+]$ as the inner cost. Minimizing a shortfall by hedging is the problem studied by Föllmer and Leukert (2000) with the convex duality method of Cvitanić and Karatzas (1999). This mission formalizes the paper's closed-form joint optimum.

Setting

Fix a horizon $T>0$. The asset price follows a geometric Brownian motion driven by a Brownian motion $B$, with market price of risk $\eta\neq0$. The density of the martingale measure is

$$Z_T=\frac{d\mathsf P^M}{d\mathsf P}=e^{-\eta B_T-\eta^2T/2},\qquad \mathsf E^M[Y]=\mathsf E[Z_TY].$$

Terminal demand is $D_T=A_T+\tilde\sigma\sqrt T\,\xi$. Here $A_T\ge0$ is driven by the asset, $\tilde\sigma>0$, and $\xi\sim N(0,1)$ is independent of the hedger's information $\mathcal G=\sigma(A_T,X_T)$. With unit profit $p>0$ and net unit cost $c>0$, the production payoff is

$$H_T(Q)=pQ-(p+c)(Q-D_T^+)^+.$$

A terminal hedging payoff $V$ is feasible if it is $\mathcal G$-measurable, $V\ge-C$ for a budget $C>0$, and $\mathsf E^M[V]\le0$. These are the terminal values reachable by self-financing strategies whose losses never exceed $C$. For a target $m$ and quantity $Q$ the static hedging problem (28) is

$$s(m,Q)=\inf_{V\text{ feasible}}\mathsf E\big[(m-H_T(Q)-V)^+\big].$$

Write $\Phi$ for the standard normal CDF and, for a multiplier $\lambda\ge0$, set $\hat D_T(\lambda)=A_T+\tilde\sigma\sqrt T\,\Phi^{-1}(\lambda Z_T)$, with $\hat D_T=+\infty$ when $\lambda Z_T\ge1$. Further, $\Delta(Q)=\Phi\big((Q-A_T)/(\tilde\sigma\sqrt T)\big)$ and $\beta(\lambda)=\mathsf E[(1-\lambda Z_T)^+]$. For $\alpha\in(0,1)$, the joint problem (36) is

$$\mathrm{CVaR}^*_\alpha=\max_{m\ge0,\;Q\ge0}\Big\{m-\frac{s(m,Q)}{1-\alpha}\Big\}\quad\text{s.t. } m-pQ+C\ge0.$$

Formalization targets

Goal: Theorem 2 (p. 20)

The equations

$$\beta(\lambda)=\alpha,\qquad (p+c)\,\mathsf E[(\lambda Z_T)\wedge\Delta(Q)]=p(1-\alpha)\qquad(45)$$

have a unique solution $(\lambda^\circ,Q^\circ)$. Let

$$C^\circ=(p+c)\,\mathsf E^M[(Q^\circ-\hat D_T^+(\lambda^\circ))^+],\qquad m^\circ=p(Q^\circ)^+-C+\frac{C-C^\circ}{\mathsf P^M(\lambda^\circ Z_T\le1)}.$$

• If $C\ge C^\circ$, the unique optimum of (36) is $(m^\circ,(Q^\circ)^+)$, and $\lambda^\circ$ is a multiplier of (35) there (the only one when $C>C^\circ$).
• If $C\le C^\circ$, replace the first equation of (45) by $(p+c)\,\mathsf E^M[(Q-\hat D_T^+(\lambda))^+]=C$ (53). The new system has a unique solution $(\lambda^*,Q^*)$, the unique optimum of (36) is $(pQ^*-C,Q^*)$, and $\lambda^*\ge\lambda^\circ$, $Q^*\le Q^\circ$.
• In both cases, $Q^*\ge(C\wedge C^\circ)/p$.

The goal asserts existence and uniqueness of the optimum, not only a description of an assumed optimizer.

Milestones

1. Theorem 1 (p. 15). The optimal payoff of (28) is

$$V_T^*=(p+c)\big[(K-Q)\mathbf 1\{\lambda Z_T\le1\}+(Q-\hat D_T^+)^+\big]-C,\qquad K=\frac{m+C+cQ}{p+c},$$

almost surely unique. The multiplier $\lambda$ solves (35), and $s(m,Q)$ has the closed form (34). The root of (35) is unique when $m-pQ+C>0$; on the boundary $m=pQ-C$ it can fail to be unique, and the conclusions hold for every root. 2. Proposition 4. $s$ is jointly convex, so (36) is a concave program. 3. Lemma 5. The identities (38) and (39). 4. (42). An expression for $s$ in terms of $\beta$, $\Delta$ and the event $\mathcal D=\{D_T\le Q\wedge\hat D_T\}$. 5. (43). The partial derivatives of $s$. 6. (45). Existence and uniqueness of $\lambda^\circ$ and $Q^\circ$. 7. (49). $1-\alpha\le\lambda^\circ$. 8. (47)–(48). $C^\circ\le p(Q^\circ)^+$. 9. (50). $m^\circ\ge0$. 10. Binding budget. The budget constraint binds when $C<C^\circ$. 11. (53). Unique solvability of the case-(ii) system.

Significance

The theorem gives the jointly optimal capacity, CVaR target and, through Theorem 1, the hedge: a short cash position, a digital option and a put on a demand surrogate $\hat D_T$ that uses only market information. Two regimes appear. With a large budget the hedge is unconstrained and the capacity is $(Q^\circ)^+$, independent of $C$. With a small budget the budget binds and the capacity shrinks. The paper's later results start from this solution: the formula (55) for $\mathrm{CVaR}^*_\alpha$, its concavity in $C$ (Proposition 6), and the dominance over the unhedged newsvendor (Propositions 8–10).

The result is proved in the paper (§5 and Appendix §9.1, §9.3) and has no machine-checked proof. Formalizing it makes three things precise:

• the Lagrangian solution of a shortfall problem under partial information;
• the envelope argument behind (43), where the multiplier depends on $(m,Q)$;
• the case split at $C^\circ$, including uniqueness of the optimum, which the paper asserts but argues only through first-order conditions.

The formalization also repairs one slip. Theorem 1 states the multiplier equation under the physical expectation, $\mathsf E[V_T^*]=0$, whereas the explicit equation (35) and Proposition 2 use $\mathsf E^M$, and only the latter makes $V_T^*$ optimal.

Difficulty

The obvious route, solving the first-order conditions of (36) with the closed form (34), fails at the first step: $s$ is the value of an infinite-dimensional problem. Its closed form involves a multiplier $\lambda(m,Q)$ defined only implicitly by (35), so differentiating (34) term by term with $\lambda$ frozen does not give the derivative of $s$. That (43) is nevertheless correct is an envelope theorem for the dual of (28), and it needs uniqueness of $\lambda$ and continuity of every term in $(m,Q)$.

The partial-information constraint is the second obstacle. $V$ may depend on $A_T$ and $B_T$ but not on $\xi$, so the pointwise Lagrangian minimization is a conditional problem in $\xi$. Its solution goes through the Gaussian conditional laws behind Lemma 5.

Uniqueness claims add a third layer. Strict monotonicity of the equations in (45) rests on $Z_T$ being lognormal with full support. The left side of (53) is only weakly monotone for some admissible $A_T$, so uniqueness for (53) is stated directly. Uniqueness of the optimum of (36) needs more than concavity, because the objective is not strictly concave in $m$.

Formalization scope

Lean representation. Lean works with terminal values only. A probability space carries a sub-σ-algebra $\mathcal G$, $\mathcal G$-measurable $A\ge0$ and $W=B_T\sim N(0,T)$, and $\xi\sim N(0,1)$ independent of $\mathcal G$. Every object is a definition built from these. The paper's $\mathcal G=\sigma(A_T,X_T)$ is one instance; any $\mathcal G$ with these properties is allowed.

Parameters. $p,c,\tilde\sigma,T,C>0$ and $\eta\ne0$.

Committed conventions.

• $\Phi$ is the published BlackScholesModel.stdNormalCDF, and $\Phi^{-1}$ is its order inverse.
• $\hat D_T$ takes values in the extended reals, with $\pm\infty$ at $\lambda Z_T\ge1$ and $\lambda Z_T\le0$.
• $\mathsf E^M$ and $\mathsf P^M$ are $\mathsf E[Z_T\,\cdot\,]$.
• A feasible $V$ satisfies $V\ge-C$ everywhere and has $Z_TV$ integrable.
• "The optimal solution" is encoded as "the set of optimal points of (36) is a singleton", and the multiplier $\lambda^*_\alpha$ as a $\lambda\ge0$ solving (35) at the optimum. That root is unique when $C>C^\circ$, but not in general when the budget binds, so uniqueness is claimed only there.
• Derivatives in (43) are taken at every point of Theorem 1's domain off the line $m-pQ+C=0$: two-sided where $m>0$ (resp. $Q>0$), from the right at $m=0$ (resp. $Q=0$).

No trivializing definition. $s(m,Q)$ is defined as the infimum of the shortfall over feasible payoffs, never by the closed form (34). With (34) as the definition, Theorem 1 would be empty and the goal would lose its meaning.

Not formalized.

• Proposition 2, that the dynamic problem (22) has the same value as (28). It needs stochastic integrals against the asset and the martingale representation theorem.
• Proposition 3, the explicit strategy.
• The CVaR formula (55) and §6.

Contributions needed. A complete development needs:

• Gaussian conditional probabilities given an independent σ-algebra;
• the Lagrangian sufficiency theorem for a linear constraint on a convex functional of a random variable;
• an envelope theorem for parametric convex programs;
• monotonicity and continuity of expectations of lognormal truncations.

The first three are reusable well beyond this paper: in shortfall hedging, in Neyman–Pearson-type problems and in CVaR optimization. Proofs of individual milestones are welcome independently.

Selected references

• L. Wang, D. D. Yao, Production Planning with Risk Hedging under a CVaR Objective, SSRN 3875464, April 2020. https://ssrn.com/abstract=3875464 — published as Production Planning with Risk Hedging Under a Conditional Value at Risk Objective, Operations Research 71 (2023) 1055–1072. https://doi.org/10.1287/opre.2022.2423
• R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2 (2000) 21–41. https://doi.org/10.21314/JOR.2000.038
• H. Föllmer, P. Leukert, Efficient hedging: cost versus shortfall risk, Finance and Stochastics 4 (2000) 117–146. https://doi.org/10.1007/s007800050008
• J. Cvitanić, I. Karatzas, On dynamic measures of risk, Finance and Stochastics 3 (1999) 451–482. https://doi.org/10.1007/s007800050071

Motivation

Bike-sharing operators periodically move docks between stations: a station that often runs out of bikes or of open docks frustrates users, but every moved dock costs money. Freund, Henderson and Shmoys modelled this dock re-allocation problem as a separable nonlinear integer program with a budget on the number of moved docks (Freund–Henderson–Shmoys, IPCO 2017). Shioura observed that, after a change of variables, the objective is an M-convex function and the budget is an $\ell_1$-ball around the current allocation, and studied the resulting problem in general (Shioura, arXiv:1809.03126).

M-convex functions are the discrete analogue of convex functions on the integer points of a hyperplane, introduced by Murota (Murota, Adv. Math. 1996; Murota, Discrete Convex Analysis, SIAM 2003). Their unconstrained minimization is well understood: a local minimum with respect to single exchanges $x \mapsto x + \chi_i - \chi_j$ is global, and steepest descent converges. Adding an $\ell_1$-distance constraint breaks the M-convex structure of the feasible region, and whether the exchange method survives such a constraint is the question this mission formalizes.

Setting

Let $V$ be a finite set (the stations), and write $x(V) = \sum_{v \in V} x(v)$ for $x \in \mathbb Z^V$, $\chi_i$ for the $i$-th unit vector, $\chi_0 = \mathbf 0$, $\mathrm{supp}^+(z) = \{v \mid z(v) > 0\}$, $\mathrm{supp}^-(z) = \{v \mid z(v) < 0\}$ and $\|z\|_1 = \sum_v |z(v)|$. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$, the effective domain is $\operatorname{dom} f = \{x \mid f(x) < +\infty\}$. The function $f$ is M$^\natural$-convex if

$$\forall x, y \in \operatorname{dom} f,\ \forall i \in \mathrm{supp}^+(x - y),\ \exists j \in \mathrm{supp}^-(x - y) \cup \{0\}:\ f(x) + f(y) \ge f(x - \chi_i + \chi_j) + f(y + \chi_i - \chi_j),$$

and M-convex if, in addition, $\operatorname{dom} f \subseteq \{x \mid x(V) = \theta\}$ for some $\theta \in \mathbb Z$.

Fix an M-convex $f$ with bounded $\operatorname{dom} f$ and a center $x_c$ with $x_c(V) = \theta$; the center need not lie in $\operatorname{dom} f$. For $k \in \mathbb Z_+$ the problem

$$(\mathrm{MML1}(k))\qquad \min\{ f(x) \mid x \in \operatorname{dom} f,\ \|x - x_c\|_1 \le 2k \}$$

has optimal set $M_k$. Put $2\sigma = \min\{\|x - x_c\|_1 \mid x \in \operatorname{dom} f\}$ (the radius at which the problem becomes feasible) and $2\tau = \min\{\|x - x_c\|_1 \mid x \in \arg\min f\}$ (the radius at which the constraint stops binding). For a budget $\gamma \ge \sigma$, the problem (MML1) is (MML1($\gamma$)).

Algorithm SteepestDescentMML1 (p. 8): choose $x_\sigma \in M_\sigma$; for $k = \sigma + 1, \dots, \gamma$ set $x_k = x_{k-1} + \chi_{i_k} - \chi_{j_k}$, where $(i_k, j_k) \in V \times V$ minimizes $f(x_{k-1} + \chi_i - \chi_j)$ over all pairs; output $x_\gamma$.

Formalization targets

Goal: Theorem 4.2

Every run of SteepestDescentMML1, with any choice in Step 0 and any tie-breaking, satisfies

$$x_k \in M_k \quad (\sigma \le k \le \gamma), \qquad\text{in particular } x_\gamma \in M_\gamma .$$

The goal fixes no constant and covers every M-convex $f$ with bounded domain, every center on the hyperplane, and every budget $\gamma \ge \sigma$.

Milestones

1. (M-EXC) (§2.1, p. 4): $f$ is M-convex if and only if $\forall x, y \in \operatorname{dom} f,\ \forall i \in \mathrm{supp}^+(x - y),\ \exists j \in \mathrm{supp}^-(x - y)$ with the exchange inequality.
2. Lemma A.1 (p. 16): if $y \ne \tilde y$, $y(V) = \tilde y(V)$ and $\|y - x_c\|_1 \le \|\tilde y - x_c\|_1$, then $\tilde y$ exceeds $x_c$ somewhere on $\mathrm{supp}^+(\tilde y - y)$ or falls below it somewhere on $\mathrm{supp}^-(\tilde y - y)$.
3. Lemma A.2 (p. 16): $\|x - z\|_1 + \|y - z\|_1 \ge \|(x - \chi_i + \chi_j) - z\|_1 + \|(y + \chi_i - \chi_j) - z\|_1$ for $i \in \mathrm{supp}^+(x - y)$, $j \in \mathrm{supp}^-(x - y)$.
4. Lemma A.3 (p. 17): from $y \in \operatorname{dom} f$ with $\|y - x_c\|_1 < 2\tau$ there is a monotone sequence with strictly decreasing values to the point of $M_\tau$ nearest to $y$.
5. Theorem 4.1 (p. 8): (i) $\mu_\sigma > \mu_{\sigma+1} > \cdots > \mu_\tau$ and $M_k \subseteq \{\|x - x_c\|_1 = 2k\}$ for $k \in [\sigma, \tau]$; (ii) every $y \in M_k$ has a neighbour $y + \chi_i - \chi_j \in M_{k+1}$ with $i \notin \mathrm{supp}^-(y - x_c)$, $j \notin \mathrm{supp}^+(y - x_c)$; (iii) every $y \in M_{k+1}$ has a neighbour $y - \chi_i + \chi_j \in M_k$ with $i \in \mathrm{supp}^+(y - x_c)$, $j \in \mathrm{supp}^-(y - x_c)$, for $k \in [\sigma, \tau - 1]$.

Significance

Theorem 4.2 gives a pseudo-polynomial algorithm for (MML1): after the initial point, it needs $\gamma - \sigma$ rounds of $|V|^2$ function evaluations. It is also a structural statement: the greedy path from the center passes through an optimum at every radius simultaneously, so a single run answers the whole family of budget questions $k = \sigma, \dots, \gamma$, which is what an operator comparing budgets needs. Theorem 4.1 underlies the paper's polynomial-time proximity and scaling algorithms (§5) and its fast algorithm for dock re-allocation (§6).

The result is proved in the paper; nothing here is open mathematics. No part of it is formalized: the platform has M-convex vocabulary and unconstrained steepest descent bounds from Murota's book, but nothing about $\ell_1$-constrained minimization, the sets $M_k$, or steepest descent under a distance constraint. The mission produces a machine-checked proof of the algorithm's correctness, including the case of an infeasible center and budgets beyond $\tau$, which the printed theorem sets aside.

Difficulty

The feasible region of (MML1($k$)) is not M-convex, so the classical optimality criterion for M-convex functions does not apply to it directly, and a local optimum of the constrained problem need not be global. The obvious induction, "a steepest step from an optimum at radius $2k$ lands at an optimum at radius $2(k+1)$", requires knowing that some optimum at radius $2(k+1)$ is a single exchange away and that its exchange moves away from the center; that is Theorem 4.1 (ii), whose proof rests on the strict monotonicity of the optimal values and on the tightness of the constraint (Theorem 4.1 (i)), which in turn rests on constructing strictly decreasing exchange paths towards a nearest minimizer (Lemma A.3). The bookkeeping of $\ell_1$ distances along such paths, which change by $-2$, $0$ or $+2$ per step, is the delicate part.

Formalization scope

Vectors are V → ℤ over a finite type V with decidable equality (no lower bound on $|V|$); values are WithTop ℝ, with $+\infty = \top$; $\|x - y\|_1$ is the natural number L1Dist x y. M-convexity is the paper's definition, (M$^\natural$-EXC) plus the hyperplane condition, using the published MNatExchangeAxiom; it is not defined through (M-EXC), whose equivalence is a milestone. The hyperplane condition through the center is the hypothesis $\forall x \in \operatorname{dom} f,\ x(V) = x_c(V)$; $x_c \in \operatorname{dom} f$ is not assumed. $\sigma$ and $\tau$ are natural numbers given by IsLeast hypotheses on the doubled minima. $M_k$ is a set defined from $f$, $x_c$ and $k$, and the optimal value $\mu_k$ is never a separate real number: Theorem 4.1 (i) asserts $M_k \ne \emptyset$ and compares values of $f$ on consecutive sets. A run is a sequence x : ℕ → V → ℤ satisfying Step 0 and Steps 2–3, with all pairs $(i, j)$, $i = j$ included, admissible in Step 2.

The goal is not vacuous: the run hypothesis is satisfiable whenever $\operatorname{dom} f \ne \emptyset$ (the minima over the finite sets $V \times V$ exist and $M_\sigma \ne \emptyset$), and a sanity file exhibits an instance with an explicit run. The paper's standing assumption $\tau > \gamma$ is dropped; the goal therefore also covers budgets past the nearest minimizer.

A complete development needs the M-convex exchange calculus (the (M-EXC) equivalence and its use with $\ell_1$ distances), which is reusable for any M-convex problem with a distance or budget constraint. Proofs of the milestones in any order are welcome, as are alternative proofs of Theorem 4.1.

Selected references

• A. Shioura, M-convex Function Minimization Under L1-Distance Constraint (published as M-Convex Function Minimization Under L1-Distance Constraint and Its Application to Dock Reallocation in Bike-Sharing System, Mathematics of Operations Research, 2022), arXiv:1809.03126v3, 2018. https://arxiv.org/abs/1809.03126
• D. Freund, S. G. Henderson, D. B. Shmoys, Minimizing multimodular functions and allocating capacity in bike-sharing systems, Proc. 19th IPCO, LNCS 10328, 2017. https://arxiv.org/abs/1611.09304
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124:272–311, 1996. https://doi.org/10.1006/aima.1996.0084
• K. Murota, On steepest descent algorithms for discrete convex functions, SIAM Journal on Optimization 14:699–707, 2003. https://doi.org/10.1137/S1052623402419005

Motivation

Many performance measures of stochastic models in operations research are expectations computed along a Markov chain until a random time. Examples are the expected discounted cost until a queue empties, the expected reward until a system enters a failure set, and the price of a claim that pays at a hitting time. When the transition law depends on a parameter $\theta$ (an arrival rate, a service-time parameter, a short rate in the discount factor), sensitivity analysis asks whether the measure is differentiable in $\theta$ and what the derivative is. Derivative formulas underlie gradient-based simulation optimization, likelihood-ratio and infinitesimal-perturbation estimators, and the "greeks" of financial models.

The classical answer for finite state spaces is a matrix calculation: invert $I-K(\theta_0)$ and differentiate the linear system the measure satisfies. On general state spaces, and when the horizon $T$ has no moment bounds, that calculation needs a substitute for the inverse. C.-H. Rhee and P. W. Glynn (arXiv:1707.03870; Mathematics of Operations Research, 2022) give conditions in terms of stochastic Lyapunov functions: inequalities that involve only the one-step transition kernel and can be checked directly from the model.

Setting

Let $S$ be a measurable state space and $\Lambda=(a,b)$ an open interval containing $\theta_0$. For each $\theta$, $P(\theta)=(P(\theta,x,dy))$ is a one-step Markov transition kernel on $S$. Let $f,g:S\to\mathbb R$ be measurable, and let $\emptyset\neq C\subseteq S$ be measurable. The chain $X=(X_n)_{n\ge0}$ is driven by $P(\theta)$, and

$$T=\inf\{n\ge0:X_n\in C^c\}$$

is its exit time from $C$. $T=\infty$ is allowed, including the case $C^c=\emptyset$. The quantity of interest is

$$u^*(\theta,x)=\mathbf E^\theta_x\Big[\sum_{j=0}^{T-1}e^{\sum_{k<j}g(X_k)}f(X_j)+e^{\sum_{k<T}g(X_k)}f(X_T)\Big],\qquad x\in C .$$

The discounted kernel is $K(\theta,x,dy)=e^{g(x)}P(\theta,x,dy)$. Its restriction to $y\in C$ is a non-negative kernel $K(\theta)$ on $C$, with powers $K^n(\theta)$. The potential kernel is $G(\theta)=\sum_{n\ge0}K^n(\theta)$, and $G(\theta,x,\cdot)$ may be an infinite measure. The one-step reward with exit is $\tilde f(\theta,x)=f(x)+\int_{C^c}K(\theta,x,dy)f(y)$. Then

$$u^*(\theta)=\sum_{n\ge0}K^n(\theta)\tilde f(\theta)=G(\theta)\tilde f(\theta),$$

and $u^*(\theta)=\tilde f(\theta)+K(\theta)u^*(\theta)$ on $C$. Write $K=K(\theta_0)$ and $G=G(\theta_0)$.

The parameter enters through a density: $K(\theta,x,dy)=k(\theta,x,y)K(x,dy)$ for $x\in C$ (assumptions A1 and A3). Here $k(\cdot,x,y)$ is continuously differentiable on $[\theta_0-\varepsilon,\theta_0+\varepsilon]$ with derivative $k'$ (A2, A3). Put $\omega_\varepsilon(x,y)=\sup_{|\theta-\theta_0|<\varepsilon}|k'(\theta,x,y)|$, $k'(x,y)=k'(\theta_0,x,y)$, and $\tilde r_\varepsilon(x)=\int_{C^c}\omega_\varepsilon(x,y)|f(y)|K(x,dy)$, which A3 assumes finite.

Formalization targets

Goal: Theorem 3.1 (p. 11)

Assume A1–A3, and let $v_0,v_1\ge0$ be finite functions on $C$ such that

$$K(\theta)v_0\le v_0-|\tilde f(\theta)|\ \ (|\theta-\theta_0|<\varepsilon),\qquad Kv_1\le v_1-\int_C\omega_\varepsilon(\cdot,y)v_0(y)K(\cdot,dy)-\tilde r_\varepsilon .$$

Then for every $x\in C$, $u^*(\cdot,x)$ is differentiable at $\theta_0$ with

$$u^{*\prime}(\theta_0,x)=\int_CG(x,dy)\int_Ck'(y,z)u^*(\theta_0,z)K(y,dz)+\int_CG(x,dy)\int_{C^c}k'(y,z)f(z)K(y,dz).$$

Assume further that $\int_C\omega_\varepsilon(x,y)v_1(y)K(x,dy)<\infty$ and that the second Lyapunov inequality holds with $K(\theta)$ for every $\theta\in[\theta_0-\varepsilon,\theta_0+\varepsilon]$ (3.12′). Then $u^*(\cdot,x)$ is continuously differentiable on $[\theta_0-\varepsilon,\theta_0+\varepsilon]$.

The derivative formula is the proof's (3.25). The printed (3.13) omits a term and fails on a two-state example. The second clause is stated with one-sided derivatives at $\theta_0\pm\varepsilon$, because with two-sided derivatives it fails at the endpoints.

Milestones

1. (3.8), p. 9: for $f\ge0$, the path expectation equals $\sum_jK^j(\theta)\tilde f(\theta)$.
2. Proposition 3.1, p. 11: $Qv\le v-f$ with $f\ge0$ and $v$ finite implies $\sum_nQ^nf\le v$.
3. Proof of Theorem 3.1, p. 12: $\sum_nK^n(\theta)|\tilde f(\theta)|\le v_0$, $|u^*(\theta)|\le v_0$, and $u^*(\theta)=\tilde f(\theta)+K(\theta)u^*(\theta)$.
4. Proof of Theorem 3.1, p. 12: the $G$-integrated Lipschitz bound $\le|h|v_1(x)$ and continuity at $\theta_0$.
5. (3.24), p. 13: the dominating function for the derivative has finite $G$-integral.
6. Proof of Theorem 3.1, p. 13: $u^{*\prime}(\theta)=\tilde f'(\theta)+K'(\theta)u^*(\theta)+K(\theta)u^{*\prime}(\theta)$ on the closed interval.

Significance

The theorem gives a derivative formula for random-horizon discounted expectations on general state spaces. It needs no moment or tail condition on $T$, no bound on $f$, and no sign condition on $g$. Positive $g$ (growth instead of discounting) is allowed. The hypotheses are one-step drift inequalities, the same kind of condition used for stability of Markov chains, so they are often checkable in queueing and storage models. Because $g$ may depend on $\theta$ through the kernel $K(\theta)$, the result also covers derivatives with respect to discount-rate parameters ("rho" in finance). The formula $G K' G\tilde f+GK'_{C^c}f$ is also the form an unbiased derivative estimator takes.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission asks for a Lean statement of Theorem 3.1 with the two corrections above and machine-checked proofs of it, of the comparison bound (Proposition 3.1), of the series representation of the path expectation, and of each analytic step of the proof. Proposition 3.1 and the potential-kernel machinery are reusable for any drift-condition argument about Markov kernels.

Difficulty

The obvious argument differentiates $u^*=\tilde f+K(\theta)u^*$ and inverts $I-K(\theta_0)$. On a general state space $I-K$ need not be invertible on any fixed function space, and $G$ need not be a finite kernel. Any rigorous version must work with $G$, which may be an infinite measure, so every subtraction and every exchange of limit and integral has to be justified for non-negative quantities first. The difference quotients of $k$ are dominated only by the supremum $\omega_\varepsilon$, whose measurability and integrability (once against $K$ and once against $G$) are themselves part of the work. Continuity of $u^{*\prime}$ on the interval requires the same control at every $\theta$, with $K(\theta)$ in place of $K$.

Formalization scope

• State space and kernels. $S$ is an arbitrary measurable space, with no topology or countability. $P(\theta)$ is a Mathlib Kernel S S with IsMarkovKernel, given for every real $\theta$ but constrained only on $\Lambda$. $K(\theta)$ is Kernel.withDensity of $P(\theta)$ by $e^{g}$; integrals over $C$ and $C^c$ are set integrals.
• Powers and potential. $K^0=\mathrm{id}$, $K^{n+1}=K\circ_kK^n$, and $G(\theta,x,\cdot)$ is Measure.sum of the powers.
• The reading of $u^*$. $u^*$ is defined as $\int\tilde f(\theta)\,dG(\theta,x,\cdot)$, the series representation the proof uses. For signed $f$ the path expectation can be undefined while every hypothesis holds; milestone (3.8) identifies the two for $f\ge0$.
• Values. $\omega_\varepsilon$, $\tilde r_\varepsilon$ and the Lyapunov inequalities live in $[0,\infty]$, the inequalities written additively. $k'$ is the derivative within $[\theta_0-\varepsilon,\theta_0+\varepsilon]$.
• Added hypotheses. One $\varepsilon$ serves A2, A3 and the theorem, as in the paper's proof. $[\theta_0-\varepsilon,\theta_0+\varepsilon]\subseteq\Lambda$. $f$ is integrable on $C^c$, the presupposition that $\tilde f$ is a number. The density is a.e. non-negative, and every function that is integrated is measurable.
• No trivializing reading. The statement is not made vacuous or easy by junk values. The derivative formula carries an integrability clause, so it cannot hold through a Bochner integral defaulting to $0$. The supremum $\omega_\varepsilon$ is $[0,\infty]$-valued, so an unbounded derivative cannot weaken (3.12). $u^*$ is built from $P$ and $g$, never "some solution of $u=\tilde f+Ku$".

Not formalized: Theorem 4.1 (stationary expectations, which rests on external Harris-chain results), the operator-theoretic Theorems 2.1–2.3, the higher-order Theorem 3.2 (proof omitted in the paper), and the G/G/1 example. Contributions that build general potential-kernel and drift-inequality lemmas for Mathlib kernels are especially welcome.

Selected references

• C.-H. Rhee, P. W. Glynn, Lyapunov Conditions for Differentiability of Markov Chain Expectations: the Absolutely Continuous Case, arXiv:1707.03870v1, 2017; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1707.03870v1
• S. P. Meyn, R. L. Tweedie, Markov Chains and Stochastic Stability, Springer, 1993. https://doi.org/10.1007/978-1-4471-3267-7

Motivation

Many control problems in operations research have no natural horizon and no natural discount rate: a queue, an inventory system or a communication network runs indefinitely, and what matters is the cost it incurs per period in the long run. The average-reward Markov decision process (AMDP) is the standard model for these problems (Puterman, 2014, Ch. 8). Policy-gradient methods, and in particular policy mirror descent, have well-developed convergence theory in the discounted setting (Lan, 2022), where the discount factor makes the Bellman operator a contraction. In the average-reward setting that contraction is absent, and the analysis has to rely on the mixing of the Markov chains the policies induce.

Li, Wu and Lan (arXiv:2205.05800v6) study an actor–critic method for AMDPs, stochastic policy mirror descent (SPMD): the actor takes a KL-proximal step on the policy at every state, and the critic supplies an estimate of the differential Q-function whose bias and second moment are controlled. Their first convergence result, Theorem 1, bounds the expected optimality gap of the actor for unregularized AMDPs in terms of the two critic constants only. This mission formalizes that theorem and the lemmas its proof rests on.

Setting

An AMDP $\mathcal M=(\mathcal S,\mathcal A,\mathsf P,c)$ has a finite state space $\mathcal S$, a finite action space $\mathcal A$, a transition kernel $\mathsf P(s'\mid s,a)$ and a real cost $c(s,a)$. A policy $\pi$ assigns to every state a distribution $\pi(\cdot\mid s)$ on actions. It induces the state transition matrix $P_\pi(s,s')=\sum_a\pi(a\mid s)\mathsf P(s'\mid s,a)$, the state–action matrix $P^\pi((s,a),(s',a'))=\mathsf P(s'\mid s,a)\pi(a'\mid s')$, and the expected cost $c^\pi(s)=\sum_a c(s,a)\pi(a\mid s)$.

The average cost of $\pi$ from state $s$ is

$$\rho^\pi(s)=\lim_{T\to\infty}\frac1T\sum_{t=0}^{T-1}\mathbb E_\pi[c(s_t,a_t)\mid s_0=s].$$

The AMDP is mixing (Assumption 1) if there is a finite $t_{\mathrm{mix}}$ such that every policy $\pi$ has a stationary distribution $\nu^\pi$ and $\max_{q}\|((P_\pi)^t)^\top q-\nu^\pi\|_1\le\frac12$ for some $1\le t\le t_{\mathrm{mix}}$. Then $\rho^\pi(s)=\langle\nu^\pi,c^\pi\rangle$ does not depend on $s$ and is written $\rho(\pi)$. The basic differential Q-function is $\bar Q^\pi(s,a)=\sum_{t\ge0}\big(\mathbb E_\pi[c(s_t,a_t)\mid s_0=s,a_0=a]-\rho(\pi)\big)$.

Write $D^p_q=\sum_a p(a)\log\frac{p(a)}{q(a)}$ for the KL divergence and $\|x\|_{\mathrm{sp}}=\max_ix_i-\min_ix_i$ for the span seminorm. SPMD starts from the uniform policy $\pi_0(a\mid s)=1/|\mathcal A|$. At step $k$ a critic returns a random estimate $\bar{\mathcal Q}^{\pi_k,\zeta_k}$ of $\bar Q^{\pi_k}$, and the actor sets, at every state,

$$\pi_{k+1}(\cdot\mid s)\in\operatorname*{arg\,min}_{p\in\Delta_{|\mathcal A|}}\Big\{\lambda_k\langle\bar{\mathcal Q}^{\pi_k,\zeta_k}(s,\cdot),p\rangle+D^p_{\pi_k}(s)\Big\}.$$

Assumption 3 asks for constants $\varsigma,\kappa\ge0$ such that, conditionally on the past, the mean $\tilde{\mathcal Q}^{\pi_k}$ of the estimate satisfies $\|\tilde{\mathcal Q}^{\pi_k}-\bar Q^{\pi_k}\|_{\mathrm{sp}}\le\varsigma$ (bias) and $\mathbb E\|\bar{\mathcal Q}^{\pi_k,\zeta_k}\|^2_{\mathrm{sp}}\le\kappa^2$ (second moment). The paper's general form adds a convex regularizer $h^\pi(s)$ with KL modulus $\omega\ge0$ to the cost, and the lemmas below are stated with it.

Formalization targets

Goal: Theorem 1 (p. 11)

Let $\pi^*$ be any policy, $K\ge1$, and $\lambda_k=\lambda=2\sqrt{\log|\mathcal A|}/(\kappa\sqrt K)$. Then

$$\mathbb E\Big[\sum_{k=0}^{K-1}\big(\rho(\pi_k)-\rho(\pi^*)\big)\Big]\le\kappa\sqrt{K\log|\mathcal A|}+K\varsigma,$$

and, for an index $r$ drawn uniformly from $\{0,\dots,K-1\}$ independently of the run,

$$\mathbb E\big[\rho(\pi_r)-\rho(\pi^*)\big]\le\frac{\kappa\sqrt{\log|\mathcal A|}}{\sqrt K}+\varsigma .$$

Milestones

1. On a mixing AMDP, $\rho^\pi(s)=\langle\nu^\pi,c^\pi+h^\pi\rangle$ for every $s$ (p. 6).
2. The solution sets of the Bellman equations (2.3) and (2.4) are $\{\bar V^\pi+b\mathbf 1\}$ and $\{\bar Q^\pi+b\mathbf 1\}$ (p. 6).
3. Lemma 2, the performance difference identity $\rho(\pi')-\rho(\pi)=\mathbb E_{s\sim\nu^{\pi'}}[\langle\bar Q^\pi(s,\cdot),\pi'(\cdot\mid s)-\pi(\cdot\mid s)\rangle+h^{\pi'}(s)-h^\pi(s)]$ (p. 7).
4. The three-point inequality (3.13) for the KL prox step with a regularizer (p. 10).
5. Lemma 4, the one-step inequality $\mathbb E[\lambda_k(\rho(\pi_k)-\rho(\pi^*))+(1+\lambda_k\omega)D(\pi_{k+1},\pi^*)]\le\mathbb E[D(\pi_k,\pi^*)]+\lambda_k\varsigma+\lambda_k^2(\kappa^2/4+L^2)$ (p. 10), with $D(\pi,\pi')=\mathbb E_{s\sim\nu^*}[D^{\pi'}_\pi(s)]$.
6. $D(\pi_0,\pi^*)\le\log|\mathcal A|$ for the uniform $\pi_0$ (p. 12).

Lemma 4 is posed in the form its proof derives. As printed, the stepsize $\lambda_k$ also multiplies the distance term, and that form is false: one state, two actions, costs $(0,0.01)$, an exact critic and $\lambda_0=100$ give a left side of $31.83$ against a right side of $0.943$.

Significance

Theorem 1 separates the two sources of error in an actor–critic method. The bias $\varsigma$ enters additively and is not amplified over the iterations, while the noise enters only through the second moment $\kappa^2$ and is averaged out at rate $1/\sqrt K$. This separation is what lets the paper combine the actor with critics of different accuracy, including linear function approximation, whose bias cannot be driven to zero (§3.2). The same one-step inequality (Lemma 4) also yields the $\mathcal O(1/K)$ rate for strongly convex regularizers (Theorem 2).

The result is proved in the paper. As far as the platform's catalog shows, none of it is formalized: there is no machine-checked average-reward performance difference lemma, no Bellman solution-set characterization for a mixing chain, and no KL-prox three-point inequality on the simplex with a non-smooth regularizer. Machine-checked proofs of Theorem 1 and its milestones are the work this mission asks for.

Difficulty

The obvious argument copies the discounted analysis and runs into two places where the discount factor did the work. First, the existence and state-independence of $\rho^\pi$ and the convergence of the series defining $\bar Q^\pi$ need the mixing assumption to be turned into geometric convergence of $P_\pi^t$ to $\mathbf 1(\nu^\pi)^\top$. The policy-evaluation equations then have a one-dimensional family of solutions rather than a unique fixed point. Second, the stochastic step needs both the bias and the conditional second moment. Taking expectations of the per-state inequality requires the iterates to be measurable with respect to the past, and the critic's mean, a conditional expectation, has to be compared with the exact $\bar Q^{\pi_k}$ of a random policy. Only the span of the error enters, because the update ignores constant shifts of $\bar{\mathcal Q}$.

Formalization scope

Finite state and action types; policies are real functions $\pi(s)(a)$ with the published IsPolicy; transitions use the published IsTransitionKernel, InducedTransition, InducedReward and MarkovMixing.IsStationary. Expectations along the chain are matrix powers. $\rho$ is the limit of the Cesàro means, and $\bar V^\pi,\bar Q^\pi$ are series of expectations (the pathwise series need not converge). Regularized costs are passed as the cost argument. $D^p_q$ uses Real.log; every iterate is strictly positive, so the KL divergences that occur are the true ones, and (2.2) is required at strictly positive points only. Assumption 3 lives on a probability space with a filtration whose $k$-th σ-algebra plays the paper's $\mathcal F_{k-1}$. Every expectation the assumption writes carries its integrability: without it the conditional expectation would default to $0$ and (3.9) would hold for any critic, a trivialization the statements rule out. The variance condition (3.8) is not assumed, since no target uses it. The comparator $\pi^*$ is any policy, not only an optimal one; the proofs never use optimality. Theorem 1 has no regularizer: $L=0$ forces $h^\pi(s)$ to be independent of $\pi$, so it is absorbed into the cost.

A complete development needs geometric ergodicity of finite mixing chains, Cesàro limits and absolutely convergent series of matrix powers, the KL prox step on the simplex (strict positivity of the minimizer, its optimality condition, the three-point identity, Pinsker's inequality), and conditional expectations against a filtration. The mixing-chain and KL-prox parts are reusable well beyond this mission, for discounted and average-reward policy optimization alike. Proofs of any milestone are welcome, as are general lemmas on finite Markov chains and KL geometry that the milestones use.

Selected references

• T. Li, F. Wu, G. Lan, Stochastic First-Order Methods for Average-Reward Markov Decision Processes, Mathematics of Operations Research, 2025; cited here in the version arXiv:2205.05800v6, 2024. https://arxiv.org/abs/2205.05800
• G. Lan, Policy mirror descent for reinforcement learning: linear convergence, new sampling complexity, and generalized problem classes, Mathematical Programming, 2023. https://arxiv.org/abs/2102.00135
• G. Lan, First-order and Stochastic Optimization Methods for Machine Learning, Springer, 2020. https://doi.org/10.1007/978-3-030-39568-1
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 2014 (first ed. 1994). https://doi.org/10.1002/9780470316887
• S. Kakade, J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• Y. Zhang, K. Ross, On-policy deep reinforcement learning for the average-reward criterion, ICML 2021. https://arxiv.org/abs/2106.07329

Motivation

A bipartite quantum state $\rho$ shared by Alice and Bob is $(n_A,n_B)$-extendible if there is a state on $n_A$ copies of Alice's system and $n_B$ copies of Bob's system whose reduced state on every pair (one Alice copy, one Bob copy) is $\rho$. Extendibility (also called shareability) measures how much the correlations of $\rho$ can be shared among many parties. Only separable states are extendible for all $n_A,n_B$, so the extendibility numbers of an entangled state quantify its entanglement. The notion appears in the characterization of entanglement and non-locality, in quantum de Finetti theorems, in quantum key distribution, and in entanglement measures such as the squashed entanglement, for which it gives lower bounds (Doherty, Parrilo, Spedalieri 2004; Brandão, Christandl, Yard 2011).

Computing extendibility is in general a semidefinite program whose size grows exponentially, and analytic answers are known only for a few families. Werner states, the states invariant under all $U\otimes U$, are the standard test family. The one-sided case $(1,n)$ was solved earlier; for the two-sided case only a few extension sizes were known (Johnson, Viola 2013). D. Jakab, A. Solymos and Z. Zimborás (arXiv:2208.13743v2, 2022) map the two-sided problem for Werner states to the ground state problem of a permutation-symmetric $SU(d)$ spin Hamiltonian and solve it with the representation theory of $SU(d)$.

Setting

Fix a local dimension $d\ge2$ and extension sizes $n_A,n_B\ge1$. Let $F$ be the flip on $\mathbb C^d\otimes\mathbb C^d$, $F|a\rangle|b\rangle=|b\rangle|a\rangle$. For $\alpha\in[-1,1]$ the Werner state is

$$\rho^W(\alpha)=\frac{d}{d^2-1}\left[(d-\alpha)\frac{\mathbb 1}{d^2}+\left(\alpha-\frac1d\right)\frac{F}{d}\right],$$

the unique $U\otimes U$-invariant state with $\operatorname{Tr}(\rho^W(\alpha)F)=\alpha$. A state $\hat\rho$ on $(\mathbb C^d)^{\otimes n_A}\otimes(\mathbb C^d)^{\otimes n_B}$ is an $(n_A,n_B)$-extension of $\rho$ if its partial trace onto Alice's $i$-th and Bob's $j$-th copy equals $\rho$ for every $i$ and $j$. The extendible Werner parameters form an interval $[\alpha_{n_A,n_B},1]$.

A $d$-partition $\lambda\vdash_d n$ is a sequence $\lambda_1\ge\dots\ge\lambda_d\ge0$ of integers with sum $n$ (a Young diagram with $n$ boxes and at most $d$ rows). Dominance order is $\lambda\trianglerighteq\mu$ iff $\lambda_1+\dots+\lambda_k\ge\mu_1+\dots+\mu_k$ for every $k$. The Casimir value is

$$c(\lambda)=\sum_{i=1}^d\left[\left(\lambda_i-\frac nd\right)^2+2(d-i)\left(\lambda_i-\frac nd\right)\right],\qquad n=\sum_i\lambda_i .$$

For $\lambda^{(A)}\vdash_dn_A$ and $\lambda^{(B)}\vdash_dn_B$, the minimum product diagram is $\hat\lambda^{(AB)}=\operatorname{sort}\{\lambda^{(A)}_i+\lambda^{(B)}_{d-i+1}\}_{i=1}^d$, the rows of $\lambda^{(B)}$ reversed, added to those of $\lambda^{(A)}$ and sorted decreasingly. The energy of the pair is

$$E^W(\lambda^{(A)},\lambda^{(B)})=\frac{1}{2n_An_B}\left[c(\hat\lambda^{(AB)})-c(\lambda^{(A)})-c(\lambda^{(B)})\right]+\frac1d .$$

The Hamiltonian $H^W=\frac{1}{n_An_B}\sum_{i,j}F_{ij}$ sums the flips of every Alice copy $i$ with every Bob copy $j$.

Formalization targets

Goal: the extremal parameter is a minimum of $E^W$

$$\rho^W(\alpha)\ \text{is }(n_A,n_B)\text{-extendible}\iff\alpha\ \ge\ \min_{\lambda^{(A)}\vdash_dn_A,\ \lambda^{(B)}\vdash_dn_B}E^W(\lambda^{(A)},\lambda^{(B)}),$$

for every $d\ge2$, $n_A,n_B\ge1$ and $\alpha\in[-1,1]$. This is the characterization the paper derives in Eq. (12) and the first expression of Eq. (13). It fixes no closed form for the minimum.

Milestones, in proof order

1. The flip in $\mathfrak{su}(d)$ generators (SM Eq. (6)) and $H^W=\frac{1}{2n_An_B}(C_{AB}-C_A-C_B)+\frac{\mathbb 1}{d}$ (Eq. (5)).
2. Symmetric extensions, the trace identity $\operatorname{Tr}(\hat\rho H^W)=\alpha$, and the ground state reduction $\alpha_{n_A,n_B}=\min\operatorname{Spect}(H^W)$ (p. 2).
3. The Casimir acts on the $\lambda$-isotypic component as $c(\lambda)$ (Eq. (9)); the spectrum of $H^W$ is labelled by Littlewood–Richardson-compatible triples (p. 3).
4. $c$ refines dominance order (Eq. (10)); Azenhas's difference theorem, the dual symmetry of multiplicities and duals preserving dominance (SM Eqs. (11), (13), (14)); $\hat\lambda^{(AB)}$ is the dominance minimum of $\lambda^{(A)}\otimes\lambda^{(B)}$ (Eq. (11)) and so minimizes $c$ (p. 3).

Significance

The goal reduces a semidefinite feasibility problem on a space of dimension $d^{n_A+n_B}$ to a minimization over pairs of Young diagrams, a finite set of size polynomial in $n_A,n_B$ for fixed $d$. It decides the two-sided extendibility of every Werner state, for every local dimension and every pair of extension sizes, and shows a non-trivial trade-off between $n_A$ and $n_B$. The milestones on the minimum product diagram are statements about Littlewood–Richardson coefficients of independent interest in algebraic combinatorics.

Status. The paper also states a closed formula, Eq. (16), and it is false as printed. Eq. (15) has a sign slip: at $d=4$, $n_A=n_B=3$ exact diagonalization of $H^W$ gives $\alpha=-5/9$ while Eq. (16) gives $-1/3$. Eq. (13)'s claim that a minimizing pair can be taken of a special non-overlapping shape is also false: at $d=5$, $n_A=n_B=5$ the pair $\lambda^{(A)}=\lambda^{(B)}=(2,2,1,0,0)$ gives $E^W=-11/25$ (confirmed by Lanczos diagonalization), below the best special pair, $-2/5$. The mission therefore poses the characterization by the minimum over all pairs, which every check confirms, and no closed form. The printed middle equalities of Eq. (10) are also off: for a box moved from row $k$ to row $i<k$ the difference is $2[(k-i)+(\mu_i-\mu_k)+1]$; the inequality and the refinement claim of Eq. (10) are true. None of these results has a machine-checked proof.

Difficulty

The reduction to $H^W$ is elementary; the obstacle is the spectrum. $C_A$, $C_B$, $C_{AB}$ commute, so the eigenvalues of $H^W$ are labelled by triples $(\lambda^{(A)},\lambda^{(B)},\lambda^{(AB)})$, but only the triples with $\lambda^{(AB)}$ inside $\lambda^{(A)}\otimes\lambda^{(B)}$ occur. Minimizing $c(\lambda^{(AB)})$ over this Littlewood–Richardson support is not a local computation: the obvious candidate, adding the rows of $\lambda^{(A)}$ and $\lambda^{(B)}$ in the same order, gives the dominance-maximal constituent and the largest Casimir value. The paper's answer goes through a theorem of Azenhas on skew Littlewood–Richardson tableaux and a duality of multiplicities. On the analytic side, Schur–Weyl duality and the Casimir value on each isotypic component are needed, neither of which is in Mathlib in this form. Finally, the minimum of $E^W$ itself has no known closed form; the natural guess of non-overlapping shapes fails.

Formalization scope

All objects are explicit finite matrices over $\mathbb C$. The joint system is indexed by (Fin nA → Fin d) × (Fin nB → Fin d); sites and rows are 0-based. Extendibility requires a positive semidefinite, trace-one extension whose marginal on every pair $(A_i,B_j)$ is the given state, and the marginal sums each traced configuration exactly once. $d$-partitions are weakly decreasing maps Fin d → ℕ with the right sum, so rows of length zero are allowed and there are at most $d$ rows. The Casimir value keeps its $n/d$ shift, since $E^W$ compares $c$ at three sizes. "$\alpha\ge\min$" is written as the existence of an eigenvalue, or of a pair, below $\alpha$; the sets are finite and nonempty. Standing hypotheses: $d\ge2$, $n_A,n_B\ge1$, $\alpha\in[-1,1]$ (for $\alpha>1$, $\rho^W(\alpha)$ is not a state).

Restricting the marginal condition to some pairs, dropping positivity or the trace, rescaling the marginal, or bounding the number of rows differently would each change the theorem; the definitions exclude all of these. The goal is not trivially true at the edges: for $d=2$, $n_A=n_B=1$ it says that every Werner state is $(1,1)$-extendible, and the minimum of $E^W$ is $-1$.

The development reuses two published definitions: the $S_n$-isotypic projector on $(\mathbb C^d)^{\otimes n}$ (QAlgorithms.Schur.isotypicProjector) and the polynomial Littlewood–Richardson coefficient counted by LR tableaux (lrCoefficient). Needed infrastructure: Schur–Weyl duality for the isotypic projectors, the Casimir eigenvalue on each component, the Littlewood–Richardson rule for the tensor product of two Schur modules, and Azenhas's theorem. Proofs of the combinatorial milestones (dominance, duals, Azenhas, the minimum product diagram) are reusable in algebraic combinatorics; the Casimir and Schur–Weyl results are reusable in quantum information. Contributions to any milestone, or alternative proofs of the minimum product diagram, are welcome.

Selected references

• D. Jakab, A. Solymos, Z. Zimborás, Extendibility of Werner States, arXiv:2208.13743v2, 2022. https://arxiv.org/abs/2208.13743v2
• O. Azenhas, The admissible interval for the invariant factors of a product of matrices, Linear and Multilinear Algebra 46 (1999) 51–99. https://doi.org/10.1080/03081089908818603
• A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Complete family of separability criteria, Phys. Rev. A 69, 022308, 2004. https://doi.org/10.1103/PhysRevA.69.022308
• F. G. S. L. Brandão, M. Christandl, J. Yard, Faithful squashed entanglement, Commun. Math. Phys. 306 (2011) 805–830. https://arxiv.org/abs/1010.1750
• P. D. Johnson, L. Viola, Compatible quantum correlations: Extension problems for Werner and isotropic states, Phys. Rev. A 88, 032323, 2013. https://doi.org/10.1103/PhysRevA.88.032323
• R. F. Werner, Quantum states with Einstein–Podolsky–Rosen correlations admitting a hidden-variable model, Phys. Rev. A 40, 4277, 1989. https://doi.org/10.1103/PhysRevA.40.4277