All missions

Motivation

The Littlewood-Richardson coefficients $c^{\lambda}_{\mu\nu}$ give the multiplicity of an irreducible polynomial ${\rm GL}_n$-representation $F^{\lambda}_n$ in the tensor product of polynomial representations $F^{\mu}_n\otimes F^{\nu}_n$. In this paper, we generalize these coefficients to an $r$-fold tensor product of rational representations, and give a new method for computing them using an analogue of statistical contingency tables. We demonstrate special cases in which our method reduces to counting statistical contingency tables with prescribed margins. Finally, we extend our result from the general linear group to both the orthogonal and symplectic groups.

This mission is the statement-level formalization of Contingency tables and the generalized Littlewood-Richardson coefficients (arXiv:2012.06928v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Stable rational GL multiplicities as weighted hollow LR tables (Theorem 3, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• Contingency tables and the generalized Littlewood-Richardson coefficients, arXiv:2012.06928v1, https://arxiv.org/abs/2012.06928v1

Motivation

This article provides an elementary introduction to Gaussian channels and their capacities. We review results on the classical, quantum, and entanglement assisted capacities and discuss related entropic quantities as well as additivity issues. Some of the known results are extended. In particular, it is shown that the quantum conditional entropy is maximized by Gaussian states and that some implications for additivity problems can be extended to the Gaussian setting.

This mission is the statement-level formalization of Gaussian quantum channels (arXiv:quant-ph/0505151v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Gaussian states maximize quantum conditional entropy at fixed moments (§3.3, Eq. (23): Gaussian conditional-entropy extremality (abstract seed), 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:

• Section 3.3, Eqs. (24)--(25): Operational distillable entanglement on arbitrary finite-mode bipartite trace-class states, with genuine LOCC protocols on tensor powers and asymptotic EPR yield in nats. (hard)
• Section 5.4, Eqs. (54)--(55); independent capacity definition on p.15: A Gaussian-displacement ensemble interface in the accepted full trace-class model: centered Gaussian trace-class realization for every physical covariance, finite-dimensional Gaussian probability laws including singular laws, measurable displaced-state preparation in trace norm, its trace-norm barycenter, and the independently optimized Gaussian Holevo objective with exact average-state constraints. (hard)
• Section 5.4, Eq. (58) implies (I)--(IV); proof continues p.17: A Gaussian-displacement ensemble interface in the accepted full trace-class model: centered Gaussian trace-class realization for every physical covariance, finite-dimensional Gaussian probability laws including singular laws, measurable displaced-state preparation in trace norm, its trace-norm barycenter, and the independently optimized Gaussian Holevo objective with exact average-state constraints. Also needed: compatible tensor-product channels and marginal constraint sets for the capacity-additivity clause. (hard)
• Section 5.4, final consequence after Eq. (61): An unrestricted infinite-dimensional entanglement-of-formation functional and its global tensor-additivity property, with the ensemble convention and finite-marginal-entropy domain needed by the background implications. (hard)

Selected references

• Gaussian quantum channels, arXiv:quant-ph/0505151v1, https://arxiv.org/abs/quant-ph/0505151v1

Motivation

We prove that it is impossible to distill more entanglement from a single copy of a two-mode bipartite entangled Gaussian state via LOCC Gaussian operations. More generally, we show that any hypothetical distillation protocol for Gaussian states involving only Gaussian operations would be a deterministic protocol. Finally, we argue that the protocol considered by Eisert et al. [quant-ph/0204052] is the optimum Gaussian distillation protocol for two copies of entangled Gaussian states.

This mission is the statement-level formalization of Gaussian transformations and distillation of entangled Gaussian states (arXiv:quant-ph/0204069v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite Gaussian contraction and normalized covariance update (Eqs.(1),(3)–(7), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Single-copy nondistillation paragraph: Full Gaussian LOCC instruments and deterministic-LOCC entanglement monotonicity on actual conditional states (hard)
• Eq.(8), Bell measurement and Fig.1: Trace-preserving Bell quadrature spectral instrument and outcome-dependent local displacement feedback (hard)
• Fixed-input deterministic realization, continued pp.2–3: Universal fixed-input deterministic Gaussian LOCC replacement including ideal homodyne operations (hard)
• Finite-squeezing sentence continued on p.3: Topology and domain of the claimed approximation to an infinitely squeezed resource/transformation (source-ambiguity)
• Eqs.(9),(10): Actual Gaussian separability-to-product-resource decomposition and normalized possibly degenerate posterior displacement law (hard)
• Pure-resource optimum paragraph: Operational pure-resource protocol family including ideal resources and deterministic displacement-mixture degradation (hard)
• Fig.2 and optimum protocol paragraph: Full operational Fig.2 family and entanglement-dominating reduction from arbitrary Gaussian LOCC protocols (hard)

Selected references

• Gaussian transformations and distillation of entangled Gaussian states, arXiv:quant-ph/0204069v2, https://arxiv.org/abs/quant-ph/0204069v2

Motivation

We develop an approximation approach to infinite dimensional quantum channels based on detailed investigation of the continuity properties of entropic characteristics of quantum channels and operations (trace-nonincreasing completely positive maps) as functions of a pair ``channel, input state''. The obtained results are then applied to the following problems: continuity of the $\chi$-capacity as function of a channel; strong additivity of the $\chi$-capacity for infinite dimensional channels; the analytical expression for the convex closure of the output entropy of arbitrary quantum channel.

This mission is the statement-level formalization of On approximation of quantum channels (arXiv:0711.2245v1). 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 Strong topology of quantum operations is metrizable (§3, unnumbered: metrizability of the operation topology, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

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

• §2, Proposition 1: entropy functionals of measures: Bochner barycenter and spectral entropy/relative entropy functionals for arbitrary Borel state measures (hard)
• §2, Corollary 1: continuity on entropy-continuous barycenters: Finite-valued entropy continuity on barycenter images and the three measure functionals (hard)
• §2, Proposition 2(A–C): convex closures and attainment: Genuine real locally convex trace-class domain, two spectral entropies, closed convex envelopes and pure measure attainment (hard)
• §2, equation (7): finite versus general-measure χ optimization: Finite-ensemble and general-measure Holevo optimization on fixed Bochner barycenter fibers (hard)
• §2, equation (8): finite-output-entropy χ identity: Unnormalized spectral S and both convex envelopes in the finite-output-entropy Holevo identity (hard)
• §3, Remark 1: compact-uniform versus strong topology: Genuine bounded complex-linear trace-class maps with their Banach operator norm and compact-uniform topology (hard)
• §3, Proposition 3: generalized Choi–Jamiolkowski isomorphism: Source-ambiguity / missing hypothesis: full rank of TrH |Ω⟩⟨Ω| does not imply full rank of TrK |Ω⟩⟨Ω|. With H=C², K=C, Ω=e0⊗1, identity and dephasing channels on C² have identical Y images. The proof assumes a complete Schmidt basis of H. Faithful input marginal or restriction to its support is required. (source-ambiguity)
• §3, proof of Proposition 3: faithful canonical purification: Canonical faithful purification and typed tensor amplification Choi homeomorphisms (hard)
• §3, unnumbered: channels with two fixed marginals: Canonical Choi map in input-reference/output order for channels with two fixed marginals (hard)
• §3, Corollary 2(1–2): compactness criterion as printed: Printed (1) is false without strong closedness of F0. On C² with σ=I/2, the unitary conjugations diag(1,e^{it}) for 0<t<1 have singleton evaluation image {σ}, yet the channel set is nonclosed and noncompact. The proof establishes relative compactness, not compactness of every subset. (source-ambiguity)
• §3, Example 1: negative compactness observations: Unpinned hypotheses: finite-dimensional operation fibers are uniformly compact, and for faithful σ and A=0 the positive-map fiber is just the zero map, compact in both topologies. The source’s universal-sounding negative claims require an existential example or restrictions it does not specify. (source-ambiguity)
• §4, Proposition 4: joint lower semicontinuity: Joint extended Holevo function and closed convex output-entropy envelope (hard)
• §4, Lemma 1: joint lower semicontinuity for measures: Joint extended H-integral on operations times weak Borel probability measures (hard)
• §4, Corollary 3: convexity/concavity in the operation: Extended convexity and concavity in operations of chi and closed convex output entropy (hard)
• §4, unnumbered: entropy minimum at an extreme channel: Closed convex output entropy, convex operation sets and their actual extreme points (hard)
• §4, unnumbered: minimal-noise channel with fixed input/output: CCoOE and canonical inverse-Choi extreme coupling minimizers (hard)
• §4, Proposition 5: entropy-controlled convergence of characteristics: Joint spectral H convergence and three extended characteristic limits (hard)
• §4, application after Proposition 5: energy-constrained joint continuity: Finite real-valued spectral entropy and characteristic functions on the energy-bounded product (hard)
• §4, Proposition 6(A–B): approximation without finite output entropy: Both extended entropy envelopes and chi under compression or domination approximation (hard)
• §4, Lemma 2: order bound for finite-ensemble Holevo quantities: Subnormalized infinite-dimensional relative entropy and its finite-ensemble order comparison (hard)
• §4, Remark 3: continuous bounded approximation of χ and CCoOE: Spectral chi and CCoOE plus increasing bounded continuous concave/convex function approximations (hard)
• §5.1, unnumbered equation (18): lower semicontinuity of constrained χ-capacity: Constrained single-use chi-capacity on arbitrary state subsets (hard)
• §5.1, equations (19) and postprocessing example: Extended constrained capacity and typed postprocessing composition (hard)
• §5.1, Proposition 7: capacity continuity on compact constraints: Spectral H continuous convergence on compact input constraints and chi-capacity (hard)
• §5.1, Corollary 4: energy-constrained capacity continuity: Finite real constrained capacity and output partition-function condition (hard)
• §5.1, Proposition 8: stability of output optimal average: Uniquely specified output optimal average as a capacity-approaching-ensemble limit (hard)
• §5.2, Proposition 9: strong χ-capacity additivity for complementary-EB channels: Actual Stinespring complementary channels, tensor products and extended chi-capacity (hard)
• §5.2, Example 3: the externally defined Φap channel: The named channel Φap is specified only by a reference to the example in [18] (quant-ph/0608090); the allowed local paper does not define its action, input/output spaces or full a,p domain. The claimed operational classical capacity also needs the external constrained coding model. Proposition 9 itself is retained without this unresolved example. (source-ambiguity)
• §5.3, unnumbered: atomic roof equality iff lower semicontinuity: Separate countable-pure and general-measure entropy roofs on trace-norm states (hard)
• §5.3, Proposition 10: increasing continuous bounded convex approximation of CCoOE: Ordered output eigenvalues with zero padding, unnormalized truncated spectral entropy and countable pure roofs (hard)
• §5.3, Corollary 5: uniform convergence on entropy-continuous compact sets: Spectral truncated pure roofs and real uniform convergence on entropy-continuous compact sets (hard)
• §5.3, unnumbered Gaussian energy application: Unpinned source interface: the Gaussian-channel and energy convention are delegated to [8]; this paper supplies no number of modes, canonical Hamiltonian, or parameter/access specification for that application. Corollary 5 and the explicit partition-function energy results remain state targets. (source-ambiguity)
• §5.3, unnumbered EoF limit representation: Actual partial-trace entropy channel, general-measure EoF and truncated atomic pure roofs (hard)
• §5.3, unnumbered EoF class-membership conclusion: The function class hat P is not defined in the supplied paper; [17] is referenced for its definition. A precise class-membership proposition cannot be invented merely from the letter P. The actual displayed EoF approximation theorem is separately retained. (source-ambiguity)
• §5.3, unnumbered uniform EoF approximation under energy bound: Missing energy assumptions: no composite Hamiltonian or spectral/partition-function hypothesis is specified for this sentence. Bounded mean energy alone need not give compactness or entropy continuity. Supplying an arbitrary Hamiltonian would make the claim false; the precise sufficient conditions are preserved in Corollary 5. (source-ambiguity)
• §6, unnumbered Corollary: two-marginal compactness as printed: Printed necessity is false: on l²(N), A={|n⟩⟨n|:n∈N} is noncompact and B={0} is compact. Every joint positive operator has equal traces of its two marginals, so A⊗B is empty and compact. Nonempty counterexamples also arise from unused trace sectors. Continuous partial traces only prove compactness of their actual images, not arbitrary supersets A,B. (source-ambiguity)

Selected references

• On approximation of quantum channels, arXiv:0711.2245v1, https://arxiv.org/abs/0711.2245v1

Motivation

We address the problem of learning an unknown unitary transformation from a finite number of examples. The problem consists in finding the learning machine that optimally emulates the examples, thus reproducing the unknown unitary maximum fidelity. Learning a unitary is equivalent to storing it in the state of a quantum memory (the memory of the learning machine), and subsequently retrieving it. We prove that, whenever the unknown unitary is drawn from a group, the optimal strategy consists in a parallel call of the available uses followed by a "measure-and-rotate" retrieving. Differing from the case of quantum cloning, where the incoherent "measure-and-prepare" strategies are typically suboptimal, in the case of learning the "measure-and-rotate" strategy is optimal even when the learning machine is asked to reproduce a single copy of the unknown unitary. We finally address the problem of the optimal inversion of an unknown unitary evolution, showing also in this case the optimality of the "measure-and-rotate" strategies and applying our result to the optimal approximate realignment of reference frames for quantum communication.

This mission is the statement-level formalization of Optimal quantum learning of a unitary transformation (arXiv:0903.0543v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Covariance without loss for a delayed learning comb (§III A, Eq.(9): covariance without loss for a learning comb, 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

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

• Abstract and §III A: optimal N-to-1 unitary learning: Canonical memory, its normalized covariant POVM and the actual integral measure-and-rotate retrieval channel. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• Lemma 2 (Optimal states for storage): Canonical irrep memory and an isometric embedding into H_o tensor H_i tied to the actual U^N decomposition. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §III A, Eq.(14): covariance without loss for retrieval: Two independent group actions on the actual reduced irrep memory. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §III A, Eqs.(19)-(25): sharp fixed-storage retrieval bound: Common-irrep coupling maps for U tensor conjugate(U_j), actual m_K^(j), occurrence sets P_KL, and transported retrieval blocks. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• Theorem 1 (Optimal retrieving strategy): Actual eta_h memory coordinates and their integrated retrieval Choi matrix. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §III B.1: multiple outputs with optimal single-copy fidelities: Canonical measure-and-rotate optimum plus local input insertion and output marginal maps for arbitrary joint Sigma. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §III B.2: optimal N-to-M learning for global fidelity: Canonical storage and an integral conditional tensor-target retrieval with M-dependent optimized weights. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• Remark: generalization to nonidentical group representations: Heterogeneous example/target tensor representations with actual based decomposition and common coupling data. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §IV: optimal inversion learning: Canonical integral estimator/conditional inverse channel and the normalized inverse global objective. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §IV: optimal approximate reference-frame realignment: Canonical token orbit and decoder on the Haar-correlated token/message state. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §IV: fidelity-optimal versus maximum-likelihood token states: Actual SU(2) and U(1) tensor-power irrep families and their optimized-token versus likelihood-token fidelity sequences. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)

Selected references

• Optimal quantum learning of a unitary transformation, arXiv:0903.0543v2, https://arxiv.org/abs/0903.0543v2

Motivation

The coding theorem for the entanglement-assisted communication via infinite-dimensional quantum channel with linear constraint is extended to a natural degree of generality. Relations between the entanglement-assisted classical capacity and the $\chi$-capacity of constrained channels are obtained and conditions for their coincidence are given. Sufficient conditions for continuity of the entanglement-assisted classical capacity as a function of a channel are obtained. Some applications of the obtained results to analysis of Gaussian channels are considered. A general (continuous) version of the fundamental relation between the coherent information and the measure of privacy of classical information transmission by infinite-dimensional quantum channel is proved.

This mission is the statement-level formalization of On the entanglement-assisted classical capacity of infinite-dimensional quantum channels (arXiv:1210.6926v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1, (14): general constrained entanglement-assisted coding theorem (Theorem 1, (14): general constrained entanglement-assisted coding theorem, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Proposition 2 [7]: existence of a generalized optimal ensemble (cited): Nonempty feasible set and finite-valued entropy continuity (source-ambiguity)
• Corollary 1, both sufficient alternatives: Meaning of nontrivial subchannel and non-pure optimal support in alternative 2 (source-ambiguity)
• Unnumbered Gaussian strictness application, both alternatives: Energy above the pure ground-state boundary in the full-row-rank alternative (source-ambiguity)
• Section 5 Gaussian continuity application: Many-mode regular irreducible Weyl system, canonical unbounded quadratures, oscillator closed form, and actual Gaussian channel action compatible with the trace-class channel (hard)
• Appendix Proposition 5(1): Gaussian c-q characterization: Many-mode Gaussian dual action on bounded Weyl observables, full normal dual, and general commuting-range c-q predicate (hard)
• Appendix Proposition 5(2): full-rank Gaussian subchannel claim: Many-mode Gaussian interface and subspace restriction compatible with the full-rank Weyl action (hard)

Selected references

• On the entanglement-assisted classical capacity of infinite-dimensional quantum channels, arXiv:1210.6926v2, https://arxiv.org/abs/1210.6926v2

Motivation

A polynomial that is positive away from the origin can be certified by writing it as a sum of squares after multiplication by a suitable power of the squared Euclidean norm. This is the uniform denominator theorem of Reznick (1995). In polynomial optimization, the size of a sum of squares certificate is governed by the number of variables in each square. A dense certificate can therefore lose the computational advantage of a polynomial whose terms involve only small groups of variables. Mai, Magron and Lasserre establish a version of Reznick’s result in which every numerator retains its own variable block. The question addressed here is the exact algebraic statement of that certificate, including its denominators and degree bounds.

Setting

A form of degree $2d$ is a homogeneous polynomial $f$ in real variables $x_1,\ldots,x_n$; it is positive definite when $f(x)>0$ for every $x\ne0$. The variables are covered by nonempty blocks $I_1,\ldots,I_p$, with $p\ge2$. Write $x(I_l)$ for the coordinates in block $I_l$ and $\|x(T)\|_2^2=\sum_{i\in T}x_i^2$ for any coordinate set $T$. A sparse form has a decomposition $f=\sum_l f_l$, where each $f_l$ is a degree-$2d$ form in $x(I_l)$. Individual $f_l$ need not be positive.

The running intersection property assigns every block $l>1$ an earlier parent $s_l<l$. Its overlap with preceding blocks, $\widehat I_l=I_l\cap\bigcup_{j<l}I_j$, must be contained in $I_{s_l}$. This condition lets the certificate keep each numerator in one block. The paper defines a polynomial $\Phi_l$ by multiplying squared norms of $\widehat I_l$ (except at the first block) and of later overlaps whose parent is $l$. It then sets $H_l=\|x(I_l)\|_2^2\Phi_l$. The set $\Sigma[x(I_l)]_t$ consists of finite sums of squares of polynomials in the variables $x(I_l)$ with total degree at most $2t$.

A second class of objects appears in the supporting results. A continuous rational form is a continuous, homogeneous function represented by a quotient of polynomials wherever the denominator is nonzero. It is positive definite on a block when it is positive wherever the coordinates of that block are not all zero. This block condition is weaker than positivity at every nonzero point of the full ambient space, since the form ignores coordinates outside its block.

Formalization targets

Sparse positive definite forms

The goal is Corollary 2.1 of the pinned preprint. For a positive definite form $f=\sum_{l=1}^p f_l$ of degree $2d$, with $d>0$ and each $f_l$ supported on $I_l$, it asserts the existence of a single $k\in\mathbb N$ and blockwise sums of squares $\sigma_l$ such that

$$f=\sum_{l=1}^p\frac{\sigma_l}{H_l^k}, \qquad \sigma_l\in\Sigma[x(I_l)]_{d+k(1+\deg(\Phi_l)/2)}.$$

This is an identity of rational functions, evaluated where its denominators are nonzero. The degree index is part of the target: leaving it free would discard the quantitative certificate. In the formal statement, every overlap $\widehat I_l$ with $l>1$ is assumed nonempty so that the printed $H_l$ is a nonzero polynomial.

Rational-form generalization

Theorem 2.1 is the last milestone. It begins with a positive definite rational form $f=\sum_l p_l/\|x(I_l)\|_2^{2k_l}$, in which $p_l$ is homogeneous of degree $2(d+k_l)$, and yields the same blockwise degree bound with a common exponent $k$. The polynomial goal follows by taking every $k_l=0$. Earlier milestones state the paper’s continuity, approximation, block-splitting, and uniform denominator results.

Significance

The result supplies a certificate whose numerator for block $I_l$ uses only variables in that block. That is the structural property needed when a polynomial optimization problem is represented by smaller semidefinite constraints instead of one dense constraint. The running intersection hypothesis is explicit, so the theorem also records when that sparsity claim applies. The common exponent and exact bound on each numerator make the certificate suitable for a hierarchy indexed by degree, as described in the source paper.

The 2020 preprint proves these mathematical results; this mission asks for machine-checked proofs of the statements in Lean. The definitions of sparse sums of squares, rational forms on blocks, and running intersection data are reusable in other polynomial optimization formalizations. No proof of the target is claimed by the draft statements themselves.

Difficulty

A dense Reznick certificate does not identify numerators in individual blocks. Even if the sum $f$ is positive definite, a summand $f_l$ can be negative, so a separate application of a positivity theorem to each $f_l$ cannot establish the target. The supporting statements must express how positivity is recovered on each block while preserving both the rational representation and variable support. The denominator factors also overlap: their degree contribution depends on the parent map $s_l$, so the final bound must track each factor rather than only a global degree.

Formalization scope

Lean uses MvPolynomial (Fin n) ℝ, with blocks as finite sets of coordinate indices and a zero-based Fin p block index. The paper’s first block is index zero in Lean. The standing condition $n>0$ from page 3 is explicit in supporting lemmas that do not assume the running intersection property; that property already implies it for the other results. Its squared Euclidean norm is the polynomial $\sum_{i\in T}X_i^2$; the function norm on Fin n → ℝ is not used for this purpose. A sparse sum of squares is represented explicitly as a finite sum of squares whose bases lie in Mathlib’s supported subalgebra. The paper’s $\deg(\Phi_l)$ is encoded by its combinatorial formula, which is even under the nonempty-overlap assumption. Lemma 3.3 requires the approximating polynomials to have exact total degree $2k$, as printed.

The printed formulas divide by $\Phi_l$, although the stated running intersection property allows an empty overlap and then makes that polynomial zero. The goal and Theorem 2.1 add nonempty overlaps for later blocks; Lemma 3.6 similarly requires every denominator block to be nonempty. Lemma 3.5 adds $d>0$, used by its cited continuity result. These are disclosed restrictions to the printed statements, rather than conclusions hidden in definitions. Rational identities are pointwise on the set where every displayed denominator is nonzero; at a zero denominator, Lean’s total division returns zero. The quotient $q/\|x(T)\|_2^{2k}$ in the continuity lemma takes that zero value at the origin.

The supporting statements retain the restriction that every $\sigma_l$ is a sum of squares in $x(I_l)$, the fixed degree bound, and positivity on each block’s own nonzero inputs. The nonempty-overlap conditions ensure the rational identity has points where all denominators are nonzero. Work on the algebraic preordering and real spectrum, homogeneous polynomial approximation, continuous rational forms, and degree control is within scope. The paper’s other main result, its sparse Putinar–Vasilescu certificate, is a separate target and is not stated here.

Selected references

• N. H. A. Mai, V. Magron and J.-B. Lasserre, A Sparse Version of Reznick’s Positivstellensatz, arXiv:2002.05101v2, 2020. https://arxiv.org/abs/2002.05101
• B. Reznick, Uniform denominators in Hilbert’s seventeenth problem, Mathematische Zeitschrift 220, 1995, 75–97. https://doi.org/10.1007/BF02572604
• M. Schweighofer, Iterated rings of bounded elements and generalizations of Schmüdgen’s Positivstellensatz, Journal für die reine und angewandte Mathematik 554, 2003, 19–45. https://doi.org/10.1515/crll.2003.004

Motivation

In a contextual bandit a decision maker repeatedly observes a context $X_t$, chooses one of two actions, and sees the reward of that action only. Personalised medicine, dynamic pricing and online advertising have this structure: the reward of the action not taken is never observed, so learning and earning must be balanced. Performance is measured by the regret, the expected reward lost against the oracle that knows which action is better at every context.

Two regimes were well understood before this paper. When the mean rewards are linear (parametric) in the context, the regret is of order $\log T$ (up to dimension factors) under a sharp margin condition (Bastani and Bayati 2020, doi:10.1287/opre.2019.1902). When they are only Lipschitz or Hölder with exponent at most one (non-differentiable), the optimal regret is $T^{1-(1+\alpha)\beta/(2\beta+d)}$ (Rigollet and Zeevi 2010, arXiv:1003.1630; Perchet and Rigollet 2013, arXiv:1110.6084). Hu, Kallus and Mao (arXiv:1909.02553, Operations Research 2022) treat mean rewards with $\beta \ge 1$ derivatives' worth of smoothness and obtain a rate that moves continuously from the non-differentiable rate at $\beta = 1$ to the parametric rate as $\beta \to \infty$.

Setting

The context $X$ takes values in a compact set $\mathcal X \subseteq [0,1]^d$ and has a Lebesgue density between $\mu_{\min} > 0$ and $\mu_{\max}$ on $\mathcal X$. At each round $t = 1, \dots, T$, nature draws $(X_t, Y_t(1), Y_t(-1))$ i.i.d., with rewards $Y_t(\pm1) \in [0,1]$; the decision maker sees $X_t$, pulls an arm $A_t \in \{-1, 1\}$ using the history, and receives $Y_t(A_t)$. Write $\eta_{\pm1}(x) = E[Y(\pm1) \mid X = x]$, the conditional average treatment effect $\tau = \eta_1 - \eta_{-1}$, the oracle policy $\pi^*(x) = +1$ if $\tau(x) \ge 0$ and $-1$ otherwise, and the regret

$$R_T(\pi) = E\Big[\sum_{t=1}^T \big(Y_t(\pi^*(X_t)) - Y_t(A_t)\big)\Big].$$

For $\beta > 0$ let $\mathfrak b(\beta)$ be the largest integer strictly below $\beta$. A function is $(\beta, L, \mathcal X)$-Hölder if it is $\mathfrak b(\beta)$-times continuously differentiable and its Taylor polynomial of order $\mathfrak b(\beta)$ at $x$ approximates it at $x'$ within $L\|x' - x\|^\beta$. A Lebesgue-measurable set $S$ is weakly $(c, r)$-regular at $x \in S$ if $\mathrm{Leb}[S \cap \mathcal B(x, r)] \ge c\,\mathrm{Leb}[\mathcal B(x, r)]$ for the closed ball $\mathcal B(x, r)$, and a $(c_0, r_0)$-regular set if this holds at each of its points for all $0 \le r \le r_0$. The class $\mathcal P$ consists of the instances with:

1. $\eta_{\pm1}$ both $(\beta, L, \mathcal X)$-Hölder and $L_1$-Lipschitz, with $\beta \ge 1$;
2. the optimal regions $\mathcal Q_a = \{x \in \mathcal X : a\tau(x) \ge 0\}$ non-empty and $(c_0, r_0)$-regular;
3. the density condition above;
4. the margin condition $P(0 < |\tau(X)| \le t) \le \gamma t^\alpha$ for all $t > 0$.

The algorithm, SmoothBandit (Algorithm 1), partitions $[0,1]^d$ into cubes of side $\delta = T^{-\beta/(2\beta+d)}(\log T)^{-1}$ and runs in epochs of geometrically growing length $n_k$, with error tolerance $\epsilon_k = 2^{-k}$. Each cube is assigned to an exploitation region $\mathcal E_{\pm1}$ (always pull that arm) or to the randomisation region $\mathcal R_k$ (toss a fair coin). After each epoch it estimates $\eta_{\pm1}$ at the cube centres by local polynomial regression of degree $\mathfrak b(\beta)$ with bandwidth $H_{a,k} = N_{a,k}^{-1/(2\beta+d)}$, using data from inside and outside each cube. It moves a cube to $\mathcal E_a$ when the estimated effect exceeds $\epsilon_k$ in favour of arm $a$, and hands to the other arm the cubes where the data of arm $a$ are too sparse to estimate (the inestimable regions $\mathcal D_{a,k}$).

Formalization targets

Goal: Theorem 2 (p. 25)

With $e = (\beta + d - \alpha\beta)/(2\beta + d)$, uniformly over the class $\mathcal P$ (constants depending only on the parameters):

$$R_T(\hat\pi) \le C\big(T^{e}\log^{1+\frac d{2\beta}}T + \log^2 T\big) \quad (\alpha\beta < \beta + d,\ \text{or}\ \alpha\beta > \beta + d \text{ and } d \le 2\beta), \qquad R_T(\hat\pi) \le C\,(T^{e} + 1)\log^m T \quad (\text{all } \alpha \ge 0),$$

for all $T \ge T_0$, where $\hat\pi$ is Algorithm 1 run with horizon $T$.

Milestones

In the order the proof uses them:

1. Lemma 1: each arm is optimal with probability at least $p = \mu_{\min}c_0r_0^dv_d$.
2. Lemma 2: the number of epochs is at most $\lceil \beta\log T/((2\beta+d)\log 2)\rceil$.
3. Lemma 3: the bandwidths are at least $\sqrt d\,\delta$.
4. Lemma 14: inestimable cubes are cubes where the data support is not regular.
5. Lemma 5: on the good events the regions behave as intended.
6. The regret decomposition (13):

$$R_T(\hat\pi) \le \sum_{k=1}^K \gamma 2^{1+\alpha}\epsilon_{k-1}^{1+\alpha}n_k + \sum_{k=1}^K n_k P(\bar{\mathcal G}^C_{k-1} \cup \bar{\mathcal M}^C_{k-1}).$$

7. Lemma 16: uniform concentration of the local polynomial estimates.
8. Theorem 1: $P(\bar{\mathcal G}^C_k \cup \bar{\mathcal M}^C_k) \le (10 + 4M_\beta^2)k/T$.

Significance

Together with the paper's lower bound (Theorem 3, not part of this mission), Theorem 2 identifies the minimax regret of smooth contextual bandits as $T^{(\beta+d-\alpha\beta)/(2\beta+d)}$ up to logarithmic factors when $\alpha\beta \le d$. The two known regimes are endpoints of this rate: $\beta = 1$ recovers the non-differentiable rate $T^{1-(1+\alpha)/(2+d)}$, and as $\beta \to \infty$ the exponent tends to the parametric value $(1-\alpha)/2$, which is $\sqrt T$ without a margin condition ($\alpha = 0$) and polylogarithmic under a sharp margin ($\alpha = 1$). The result says how much the smoothness of the reward functions is worth in a sequential decision problem, and its algorithm shows that local polynomial estimators, which use data outside each cube, are needed to get there.

The theorem is proved in the paper; no machine-checked proof of it, or of any smooth ($\beta > 1$) nonparametric bandit bound, is known. A formal proof would also check the paper's analysis, which has gaps recorded in this mission: Theorem 2's $O$-form fails for $\alpha\beta > \beta + d$ when $d > 2\beta$ and its explicit constant needs $\alpha\beta < \beta + d$, Lemma 5's fourth statement needs the sample-size event of the current epoch, and a display of Lemma 3 is misprinted. The definitions layer (the Hölder class with derivatives, regular sets, the local polynomial estimator, an epoch-based algorithm on a probability space with coins) is reusable for other nonparametric bandit and estimation results.

Difficulty

The goal's own proof is short once its ingredients are available: the decomposition (13), Theorem 1 and Lemma 2, then a geometric sum. The weight is in Theorem 1 and Lemma 16. The samples of each epoch are collected adaptively: which contexts are sampled for arm $a$ depends on regions computed from earlier data, so the samples are i.i.d. only conditionally on the past, with a conditional density that vanishes on the other arm's exploitation region. The classical analysis of local polynomial regression assumes a design density bounded below on a neighbourhood of every point and so does not apply. The paper restores a usable condition through the regularity of the regions $\mathcal Q_a$ (Assumption 2) and the screening rule (6); making this rigorous requires conditioning on events of the past epochs, a lower bound on the smallest eigenvalue of the local Gram matrices uniformly over the grid, and a union bound over $\delta^{-d}$ cubes. Bounding the estimation error at one point is not enough: the accuracy event $\mathcal G_k$ is a supremum over a region that is itself random.

Formalization scope

Contexts live in EuclideanSpace ℝ (Fin d) with $d \ge 1$; arms are Bool (true is $+1$); Lean rounds start at $0$. An instance is a structure on a probability space $\Omega$ that carries the contexts, the potential rewards of both arms, i.i.d. fair coins independent of the data, the support $\mathcal X$ and the mean rewards $\eta_{\pm1}$. Its laws are stated through iIndepFun, identical distributions and the integral form of $E[Y(a) \mid X] = \eta_a(X)$. The Hölder condition uses $C^{\mathfrak b(\beta)}$ on an open neighbourhood of $\mathcal X$ and iteratedFDeriv. The density condition is stated on measurable subsets of $\mathcal X$. All standing parameter conditions are explicit ($\beta \ge 1$, $L, L_1 > 0$, $0 < c_0 \le 1$, $r_0 > 0$, $0 < \mu_{\min} \le \mu_{\max}$, $\gamma > 0$, $\alpha \ge 0$).

Algorithm 1 is a concrete, total function of the contexts, the coins and the rewards of the pulled arms, with the paper's constants $p$, $\lambda_0$, $C_0$, the epoch lengths (10) and every tie-break as printed. Its conventions:

• regions are finite sets of grid cells;
• the bandwidth uses $\max(N, 1)$;
• $G$ uses Lebesgue volume (equivalent under Assumption 3);
• the local polynomial estimate is $0$ exactly when the least-squares minimiser is not unique.

The goal must be proved for this algorithm. A statement for an abstract policy assumed to satisfy Lemma 5, or with regions or good events taken as hypotheses, would reduce Theorem 2 to the decomposition (13) and is not the theorem. The constants $C$, $T_0$ and $m$ are chosen before the instance. The $O$-form clause excludes only the parameters where it fails as printed ($\alpha\beta > \beta + d$ with $d > 2\beta$) and the boundary $\alpha\beta = \beta + d$.

Welcome contributions: proofs of the milestones; the conditional i.i.d. structure (Lemma 6) and the Gram-matrix bound (Lemma 7), which are used inside Lemma 16 but not stated here; and general lemmas on local polynomial regression and on regular sets.

Selected references

• Y. Hu, N. Kallus, X. Mao, Smooth Contextual Bandits: Bridging the Parametric and Non-differentiable Regret Regimes, Operations Research 70(6), 2022; arXiv:1909.02553v4 (2020). https://arxiv.org/abs/1909.02553
• P. Rigollet, A. Zeevi, Nonparametric Bandits with Covariates, COLT 2010. https://arxiv.org/abs/1003.1630
• V. Perchet, P. Rigollet, The Multi-Armed Bandit Problem with Covariates, Annals of Statistics 41(2), 2013. https://arxiv.org/abs/1110.6084
• H. Bastani, M. Bayati, Online Decision Making with High-Dimensional Covariates, Operations Research 68(1), 2020. https://doi.org/10.1287/opre.2019.1902
• C. J. Stone, Optimal Global Rates of Convergence for Nonparametric Regression, Annals of Statistics 10(4), 1982. https://doi.org/10.1214/aos/1176345969

Motivation

Optimal transport asks how cheaply several prescribed probability distributions can be coupled. Adding a divergence penalty relative to their independent product makes the problem amenable to numerical methods, but changes its value. A quantitative bound on that change tells users of regularized transport how much bias a chosen regularization parameter can introduce. Eckstein and Nutz study this question through quantization of an optimal plan. Their Theorem 3.8 gives an entropic bound and a bound for a broader family of divergence penalties when the cost has a bounded second derivative. The result concerns the value of the transport problem; it does not assert convergence of optimal couplings or dual potentials.

Setting

There are $N\ge1$ marginals. For $i=1,\ldots,N$, $X_i$ is a closed convex subset of a Euclidean space and $\mu_i$ is a probability measure on $X_i$ with finite second moment. Their product $X=X_1\times\cdots\times X_N$ has the Euclidean product metric. A coupling $\pi\in\Pi(\mu_1,\ldots,\mu_N)$ is a probability measure on $X$ whose $i$th marginal is $\mu_i$. The reference measure $P=\mu_1\otimes\cdots\otimes\mu_N$ makes the coordinates independent.

The transport value $\mathrm{OT}$ is the infimum of $\int c\,d\pi$ over these couplings. The cost $c$ is continuous and has growth of order two, so its integral and the value are finite in this setting. For a strictly convex, lower bounded generator $f:[0,\infty)\to\mathbb R$ with $f(1)=0$ and $f(t)/t\to\infty$, the $f$-divergence $D_f(\pi,P)$ integrates $f(d\pi/dP)$ against $P$ when $\pi\ll P$; it is $+\infty$ otherwise. The regularized value is

$$\mathrm{OT}_{f,\varepsilon}=\inf_{\pi\in\Pi(\mu_1,\ldots,\mu_N)}\left(\int c\,d\pi+\varepsilon D_f(\pi,P)\right),\qquad \varepsilon>0.$$

Entropic regularization has $f(t)=t\log t$, with $f(0)=0$. A law belongs to $\mathcal P^n(X)$ when it is supported on at most $n$ points of $X$. An optimal plan $\pi^*$ has quantization rate $\operatorname{quant}_2(C,\alpha)$ when, for each $n\ge1$, some $\nu_n\in\mathcal P^n(X)$ satisfies $W_2(\nu_n,\pi^*)\le Cn^{-\alpha}$. Here $W_2$ is the Wasserstein distance for the Euclidean product norm. The rate hypothesis is on the joint optimal plan, not merely on its individual marginals.

Formalization targets

The goal is the corrected form of Theorem 3.8. Assume $c$ is twice continuously differentiable on a neighborhood of $X$, $B\ge0$, $C>0$, $0<\alpha\le1$, and $\pi^*$ is an optimal plan with $\operatorname{quant}_2(C,\alpha)$. The Hessian bound is two-sided and holds for every direction $w$ in the ambient product space:

$$|D^2c(x)[w,w]|\le B\|w\|^2\qquad(x\in X).$$

For entropy and $0<\varepsilon\le1$, the first target is

$$\mathrm{OT}_{f,\varepsilon}-\mathrm{OT} \le \frac{N-1}{2\alpha}\,\varepsilon\log(1/\varepsilon) +8BC^2\varepsilon.$$

For two marginals, suppose $f(t)=t\varphi(t)$ on $t>0$, where $\varphi$ is nondecreasing and concave there. Write $\beta=1/(2\alpha)$ and $\widetilde f(t)=t\varphi(t^\beta)$. If $\widetilde f$ is strictly increasing on $[x_0,\infty)$, $x_0\ge0$, put $S_\varepsilon=\widetilde f^{-1}(1/\varepsilon)$. The second target includes $S_\varepsilon\to\infty$ and $\varepsilon S_\varepsilon\to0$ as $\varepsilon\downarrow0$ and, when $0<\varepsilon$, $\varepsilon x_0\le1$, and $S_\varepsilon\ge1$,

$$\mathrm{OT}_{f,\varepsilon}-\mathrm{OT} \le \frac{8BC^2+1}{S_\varepsilon}.$$

The source prints $8BC$ in both bounds and a one-sided condition in (3.4). The squared quantization estimate requires $C^2$, and the Hessian condition must control both signs in every ambient direction. The mission records these corrections explicitly rather than changing the quantization hypothesis.

Significance

The first estimate controls entropic bias at order $\varepsilon\log(1/\varepsilon)$ when an optimal joint plan admits the stated $W_2$ quantization rate. The second expresses a rate for other divergence generators through an inverse function determined by $f$. These are established analytical results in the cited paper, though the corrected formulation is needed for the stated constants and hypotheses. The formalization target is a machine-checked statement of those rates and their supporting cost and divergence bounds. No completed machine-checked proof of this mission's goal is claimed here.

Difficulty

A finite approximation of the optimal plan need not retain the prescribed marginals. Restoring them can increase cost and divergence. A direct first-order cost estimate also misses the improvement sought here: the result uses cancellation associated with martingale quantization, while the remaining cost change is quadratic in the Wasserstein error. The requested infrastructure therefore includes a transport model with actual probability couplings, finite-support quantizers on the joint space, and a divergence that keeps its infinite value outside absolute continuity.

Formalization scope

Lean represents each marginal space by EuclideanSpace ℝ (Fin (d i)) and the product by PiLp 2, whose norm is the paper's Euclidean product metric. The paper's marginal $\mu_{i+1}$ is Lean's index i : Fin N. The formal statement requires $N>0$, closed convex supports, probability marginals concentrated on those supports with finite second moments, growth of order two for $c$, and $C^2$ regularity on an open neighborhood. The real value OTval is used only under those conditions; OTreg and fDiv use extended real values, so an infinite divergence cannot silently become zero. The divergence definition assigns $+\infty$ when its density integrand is not integrable, consistent with a lower-bounded generator under a probability reference measure. The condition $\varepsilon x_0\le1$ covers $x_0=0$ without division by zero. The function $\varphi$ is constrained only on $(0,\infty)$, allowing generators with a nonzero value at zero.

The development reuses the published WassersteinDRO.Duality.wassersteinDistance for $W_2$. Its new definitions of couplings, product reference law, divergence, quantization, and martingale coupling are reusable for related finite-dimensional transport results. The milestones isolate the Taylor estimate, the marginal-restoring coupling and its data-processing bound, the corrected cost estimate, and the entropic discrete-marginal bound of Lemma 2.3(iii). Lemma 2.3(i) is not posed here because the proposed positive-argument interpretation of $f(t)=t\varphi(t)$ does not control $f(0)$, and its stated divergence bound then has a two-point counterexample. A valid closure must use joint-plan quantization and a two-sided Hessian bound; replacing the regularized infimum by a default real value, restricting the Hessian to directions inside $X$, or quantizing only the marginals would change the result.

Selected references

• Stephan Eckstein and Marcel Nutz, Convergence Rates for Regularized Optimal Transport via Quantization, Mathematics of Operations Research, 2024; arXiv:2208.14391v3, pp. 5–8, 14–17. This mission cites the held arXiv version's pagination and labels.

Motivation

In information design (Bayesian persuasion), a designer commits to a signal about an unknown state, and every signal induces a distribution over the receiver's posterior beliefs. Kamenica and Gentzkow (2011) showed that the distributions a signal can induce are exactly the Bayes-plausible ones, those whose mean posterior is the prior, and that the designer's optimal value is the concave hull (concavification) of the designer's objective, evaluated at the prior. This reduces the design problem to a computation in convex analysis, and it is the basic tool of the information design literature.

Many applications add constraints on the distribution of posteriors: a capacity or cost constraint on information (rational inattention), participation or incentive constraints when the designer is a mechanism designer with limited commitment, or a bound on the probability of a given action. Le Treust and Tomala (2019) treated one inequality constraint for finitely supported distributions. Doval and Skreta (arXiv:1811.03588v3, Mathematics of Operations Research, 2024) allow any finite number of inequality and equality constraints, and an arbitrary Borel distribution over posteriors. Their first main result, Theorem 3.1, shows that the value is still a concave hull, of a function of more variables.

Setting

Let $\Omega = \{\omega_1, \dots, \omega_N\}$ be a finite set of states and $\Delta(\Omega) \subseteq \mathbb R^N$ the simplex of beliefs. The data are measurable functions on $\Delta(\Omega)$: an objective $f$, $I$ inequality constraint functions $\bar g_I = (\bar g_1, \dots, \bar g_I)$ and $E$ equality constraint functions $\bar g_E = (\bar g_{I+1}, \dots, \bar g_{I+E})$, with $I, E \ge 0$.

For a prior $\mu_0$, $\Delta_{\mu_0}(\Delta(\Omega))$ is the set of Borel probability measures $\tau$ on $\Delta(\Omega)$ with mean $\mu_0$. The constrained information design problem (CID) at a parameter $(\mu_0, \gamma) \in \mathbb R^{N+I+E}$, $\gamma = (\gamma_I, \gamma_E)$, is

$$V(\mu_0, \gamma) = \sup_{\tau \in \Delta_{\mu_0}(\Delta(\Omega))} \mathbb E_\tau[f(\mu)] \quad\text{s.t.}\quad \mathbb E_\tau[\bar g_I(\mu)] \ge \gamma_I,\ \ \mathbb E_\tau[\bar g_E(\mu)] = \gamma_E,$$

component-wise, with $V = -\infty$ when no $\tau$ is feasible. The feasibility set $\mathcal F$ (Definition 2.2) is the set of $(\mu, \tilde\gamma)$ at which (CID) is feasible.

The pointwise set $C = \{(\mu, \tilde\gamma) \in \Delta(\Omega) \times \mathbb R^{I+E} : \bar g_I(\mu) \ge \tilde\gamma_I,\ \bar g_E(\mu) = \tilde\gamma_E\}$ collects the parameters at which the constraints hold for the degenerate distribution at $\mu$. The modified objective (3.1) is

$$f^{\bar g}(\mu, \tilde\gamma) = f(\mu) - \delta(\mu, \tilde\gamma \mid C),$$

equal to $f(\mu)$ on $C$ and $-\infty$ off $C$. For a function $h$ on $\mathbb R^D$, the hypograph is $\operatorname{hypo} h = \{(x, y) \in \mathbb R^{D+1} : y \le h(x)\}$ and the concave hull (Definition 2.1) is

$$(\operatorname{cav} h)(x) = \sup\{y \in \mathbb R : (x, y) \in \operatorname{conv}(\operatorname{hypo} h)\}.$$

In the Lean development these are IsBayesPlausible, IsConstraintFeasible, value, feasibleSet, pointwiseSet, modObj, hypo and cav, in the namespace ConstrInfoDesign.Cav.

Formalization targets

Goal: Theorem 3.1 (p. 7)

For every $(\mu_0, \gamma) \in \mathbb R^{N+I+E}$,

$$V(\mu_0, \gamma) = \operatorname{cav} f^{\bar g}(\mu_0, \gamma). \tag{3.2}$$

The statement fixes no constants and assumes nothing beyond measurability; it covers infeasible parameters, where both sides are $-\infty$, and unbounded objectives, where both sides may be $+\infty$.

Milestones (Appendix A, pp. 24–25)

1. Rubin–Wesler step (proof of Proposition A.1): for $\tau \in \Delta_{\mu_0}(\Delta(\Omega))$ with $f, \bar g$ integrable, $(\mu_0, \mathbb E_\tau f, \mathbb E_\tau \bar g) \in \operatorname{conv}\{(\mu, f(\mu), \bar g(\mu)) : \mu \in \operatorname{supp}\tau\}$.
2. Proposition A.1: every feasible $\tau$ can be replaced by a finitely supported $\tau^\star$ with the same mean and the same expectations of $(f, \bar g)$.
3. Lemma A.1: $\mathcal F = \operatorname{conv} C$.
4. Proof of Theorem 3.1, first step: off $\mathcal F$, $\operatorname{cav} f^{\bar g} = V = -\infty$.
5. Proposition A.2 (Rockafellar, Corollary 17.1.5): $(\operatorname{cav} h)(x) = \sup\{\sum_{m \le M} \lambda_m h(x_m) : x_m \in \operatorname{dom} h,\ \lambda \in \Delta_x,\ M \le D + 1\}$.

Significance

Theorem 3.1 gives the value function of (CID) in closed form as a single concave hull. Its consequences in the paper are a bound $N + I + E$ on the number of posteriors an optimal design needs (Corollary 3.1), a refinement to $N + B + E$ with $B$ binding constraints (Corollary 3.2), and, combined with Lagrangian duality, the characterization of optimal designs in applications such as mechanism design with limited commitment and persuasion of a privately informed receiver. The result also explains when the feasibility set is the convex hull of the pointwise set (Lemma A.1), which is the geometric reason the constrained problem behaves like an unconstrained one in $N + I + E$ coordinates.

The result is proved in the paper; to the best of current knowledge none of it is formalized. Mathlib has convex hulls, Carathéodory's theorem, measures, supports and Bochner integrals, but neither the concavification theorem of Kamenica and Gentzkow nor the Rubin–Wesler theorem that the mean of an integrable random vector lies in the convex hull (not only its closure) of a set carrying it. A complete development would give machine-checked versions of both, reusable by any formalization of Bayesian persuasion with finitely many states.

Difficulty

The obvious argument for $V \le \operatorname{cav} f^{\bar g}$ says that the mean of the vector $(\mu, f(\mu), \bar g(\mu))$ under $\tau$ lies in the convex hull of its range. Mathlib's tools (Convex.integral_mem) only give membership in a closed convex set, and the range of an integrable, possibly unbounded and discontinuous $f$ is not closed; the closure gives the concave closure of $f^{\bar g}$, which differs from the concave hull on the boundary of its domain (Example D.1 of the paper). The Rubin–Wesler theorem closes this gap, but it needs its own argument by induction on dimension.

In Proposition A.2, Carathéodory's theorem in $\mathbb R^{D+1}$ gives $D + 2$ points of the hypograph; the claimed bound $D + 1$ needs the extra observation that a point of the hypograph can be moved up to the graph. The remaining steps are bookkeeping in the extended reals: shifting thresholds so that each point of a convex combination lies in $C$, and approximation arguments when the suprema are infinite.

Formalization scope

States are Fin N; beliefs are points of Fin N → ℝ and $\Delta(\Omega)$ is stdSimplex ℝ (Fin N). The parameter space $\mathbb R^{N+I+E}$ is the product (Fin N → ℝ) × ((Fin I → ℝ) × (Fin E → ℝ)). The functions $f$, $\bar g_k$ are total on Fin N → ℝ; their values off the simplex never matter. A distribution over posteriors is a Borel probability measure on Fin N → ℝ that gives the complement of the simplex measure zero, and its mean is the Bochner integral of the identity.

Conventions committed to:

• $V$, $f^{\bar g}$ and cav take values in EReal; suprema are sSup in EReal, so the empty supremum is $-\infty$.
• The choice set of (CID) is all such measures, not only finitely supported ones.
• Every admissible $\tau$ must make $f$ and each $\bar g_k$ integrable. The paper leaves this implicit; it is needed because Lean's integral of a non-integrable function is $0$. Theorem 3.1 holds unchanged with this convention.
• Proposition A.1 states the mean $\mu_0$ of $\tau^\star$ explicitly (the page leaves it implicit).
• Proposition A.2 is stated for $h$ valued in $[-\infty, +\infty)$ on any finite-dimensional real vector space of dimension $D$, because the paper applies it to $f^{\bar g}$, which takes the value $-\infty$.
• No upper semicontinuity is assumed: Theorem 3.1 does not use the paper's Assumptions $f$ and $\bar g$.

Trivializing formalizations are ruled out: $V$ is not taken over finitely supported distributions only (which would make Proposition A.1 empty), cav is Definition 2.1 and not the sum formula of Proposition A.2, $\mathcal F$ is Definition 2.2 and not $\operatorname{conv} C$, integrals of non-integrable maps are excluded rather than counted as $0$, and no supremum is taken in $\mathbb R$.

The development needs the Rubin–Wesler theorem in finite dimensions, a Carathéodory variant for hypographs, and the finite-dimensional facts that a measure on a second-countable space is carried by its support and that finite sums of Dirac masses are probability measures with the expected integrals. The Rubin–Wesler theorem and Proposition A.2 are reusable beyond this mission. Proofs of the milestones and of the goal, and alternative arguments, are welcome.

Selected references

• L. Doval and V. Skreta, Constrained Information Design, Mathematics of Operations Research, 2024; held as arXiv:1811.03588v3, 2022. https://arxiv.org/abs/1811.03588
• E. Kamenica and M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• M. Le Treust and T. Tomala, Persuasion with limited communication capacity, Journal of Economic Theory 184, 104940, 2019. https://doi.org/10.1016/j.jet.2019.104940
• H. Rubin and O. Wesler, A note on convexity in Euclidean n-space, Proceedings of the American Mathematical Society 9, 522–523, 1958. https://www.ams.org/journals/proc/1958-009-04/
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Passive funds hold a market index rather than selecting individual stocks. In the model of Baruch and Zhang (2022), this difference matters for what prices reveal. An investor who studies individual stocks can bring information about their payoffs into trading; an investor restricted to the market portfolio cannot make the same stock-by-stock trades. The paper asks how the mix of these investors changes the information about future asset payoffs that can be inferred from market prices. Its answer separates the market portfolio from every other stock portfolio: indexing preserves the former's price efficiency while reducing the latter's, at an increasing rate. This mission targets that price-efficiency result, Theorem 3 on p. 6226.

The question matters to asset-pricing models that use prices as information. A price can be informative even when it is affected by many other forces; here the paper gives a controlled Gaussian economy in which the effect of replacing active investors with indexers can be isolated. The target is a theorem about conditional variances, not an empirical estimate of the effect of real index funds. The equilibrium interpretation comes from the paper's earlier price construction; the formal statements here use the public statistic that the paper proves equivalent for this purpose (15)–(16), p. 6224.

Setting

There are $n$ risky assets and $m$ investors. The random payoff vector is $v\in\mathbb R^n$, with multivariate normal law $N(\mu_v,\Sigma_{vv})$. Investor $k$ sees a private signal $s_k=v+\varepsilon_k$, where $\varepsilon_k\sim N(0,\Sigma_{\varepsilon\varepsilon})$. The payoff and all noise vectors are mutually independent, and the two covariance matrices are positive definite. A stock portfolio $x\in\mathbb R^n$ pays $x'v$. The all-ones vector $\mathbf1$ is the market portfolio. These are the assumptions and terms introduced in §2, p. 6221.

The investors are partitioned into indexers $I$, who hold the market portfolio, and nonindexers $NI$. Both kinds are present: $1\le |NI|<m$, with $|I|=m-|NI|$ p. 6222. Equation (3) sets $g=(m\Sigma_{vv}+\Sigma_{\varepsilon\varepsilon})^{-1}\Sigma_{vv}\mathbf1$. Equation (4) combines the nonindexers' average signal and a scalar statistic of all signals into the public statistic

$$y_{NI}=\left(\frac1{|NI|}\sum_{k\in NI}s_k,\quad g'\sum_{k=1}^{m}s_k\right).$$

The first component has $n$ coordinates; the second has one. The paper identifies the conditional variance given this statistic with the variance given equilibrium prices (16), p. 6224. In this mission, $V_x(NI)$ means the conditional variance of $x'v$ given $\sigma(y_{NI})$. It is initially a random variable, and equation (20) asserts that it is almost surely a deterministic matrix expression under the Gaussian model.

Formalization targets

The goal is Theorem 3, p. 6226, stated for all admissible nonindexer sets on the same probability space. For any real $c$, market-portfolio multiples have unchanged conditional variance:

$$x=c\mathbf1\quad\Longrightarrow\quad V_x(NI)=V_x(NI')\quad\text{almost surely}.$$

For every other portfolio, fewer nonindexers, equivalently more indexers, strictly raise conditional variance. The rate also grows: whenever $|NI_1|=|NI_2|+1$ and $|NI_2|=|NI_3|+1$,

$$V_x(NI_1)<V_x(NI_2)<V_x(NI_3),\qquad V_x(NI_2)-V_x(NI_1)<V_x(NI_3)-V_x(NI_2) \quad\text{almost surely}.$$

The six milestones are the identities and statements used in the paper's development: the cross-covariance $\Sigma_{vy}$ in (7), the covariance $\Sigma_{yy}$ of $y$ in (8), Gaussian conditioning in (20), the characterization of market portfolios in Lemma 2, the first derivative in (21), and the second-derivative conclusion in §6.1, p. 6227. They make the model-to-goal path explicit without changing the goal's three clauses.

Significance

The result specifies which price information survives a shift toward passive investing in this economy. It says that market-portfolio payoff information is preserved while information about every portfolio outside the span of $\mathbf1$ is lost, with an accelerating loss across successive increases in indexer count. The distinction is used later in the paper to discuss asset-price comovement and a conditional CAPM measure §6.2–6.3, pp. 6227–6228.

Baruch and Zhang proved the theorem in 2022. The formalization work is to represent their Gaussian model, its public statistic, the conditional-variance identity, and the comparative-statics claims in Lean, then supply machine-checked proofs. The current proposal contains checked statements and definitions with open theorem proofs; it does not claim that those proofs already exist. The model interface and covariance identities could also support later formalizations of the paper's price and comovement results.

Difficulty

The target compares conditional variances arising from different information sets. Their equality or ordering cannot be read directly from the definitions of conditional expectation. The Gaussian assumption turns the conditional variance into a matrix expression, but the derivation must preserve the dependence structure of all $m$ signals and the special scalar coordinate of $y$. The boundary $|NI|=m$ makes $y$ redundant and its covariance singular, so the inverse formula requires the paper's standing condition that both investor types are present.

The rate claim requires more than the sign of the first derivative. The printed second-derivative argument on p. 6227 omits the minus sign in the derivative of a matrix inverse; the nonnegativity conclusion survives, but its formal statement records the corrected derivative value. The strict increasing-rate clause in the goal is stronger than the non-strict inequality displayed in that proof. These distinctions must be established for every portfolio outside the market span, including edge dimensions, rather than inferred from a numerical example.

Formalization scope

Assets are indexed by Fin n and investors by Fin m, both starting at zero. The final coordinate of $y$ is represented by the Unit side of Fin n ⊕ Unit. Mathlib's multivariate Gaussian law lives on a Euclidean space; a SignalModel bundles the Gaussian laws, positive definiteness, mutual independence, and measurability of payoffs and noises. Joint normality follows from these model assumptions. The measurability fields ensure that $\sigma(y)$ is a sub-σ-algebra of the ambient one.

The conditional variance in the goal is Mathlib's conditional variance of $x'v$ given $\sigma(y)$, compared almost surely across choices of $NI$. It is not defined by the Schur-complement formula: milestone (20) asserts that identity. The matrix $\Sigma_{yy}(N)$ and the coefficients in (19) use a real variable $N\in(0,m)$ in the derivative milestones, extending the integer count $|NI|$ used by the economy. Positive definiteness and $1\le |NI|<m$ rule out the junk inverse and zero-denominator cases. The strict discrete-increment statement expresses “increasing rate” in the goal.

The equilibrium prices and their equivalence with $y$ in (16), Theorems 1–2, and the later comovement and CAPM results are outside this mission. Contributions are welcome on Gaussian conditioning, covariance identities, matrix inverse differentiation, and the comparison of successive portfolio variances. General Gaussian and matrix lemmas can be reused beyond this paper.

Selected references

• Shmuel Baruch and Xiaodi Zhang, The Distortion in Prices Due to Passive Investing, Management Science 68(8), 6219–6234, 2022. doi:10.1287/mnsc.2021.4114.

Motivation

A neural network can change its behavior substantially when both its width and its training duration grow. For a network with two hidden layers, the parameters of the layers interact during training, so a large-width description must account for the output of the actual optimization algorithm. Sirignano and Spiliopoulos study this question for online stochastic gradient descent (SGD) under a mean-field normalization. Their Theorem 2.3 identifies the limit of the trained network when the first hidden layer grows, followed by the second, and gives a rate for the intermediate second-layer approximation. The result concerns a trained network: all three families of weights evolve at every SGD step.

The normalization matters. Each hidden layer contributes an average, with factors $1/N_1$ and $1/N_2$ for the first and second widths. The learning rates depend on those widths, so the output can continue changing on the time scale of $N_1$ SGD steps. The paper notes that a different scaling may lead to a different limiting equation or to no nontrivial training behavior at large width. A precise statement therefore needs the finite network and its SGD updates alongside the limiting equations, not merely a claim about an abstract mean-field flow.

Setting

Let $d$ be an input dimension and $x\in\mathbb R^d$ an input. A two-hidden-layer network has $N_1$ first-layer units and $N_2$ second-layer units. Its parameters are output weights $C^i$, first-layer vectors $W^{1,j}$, and second-layer weights $W^{2,i,j}$. With an activation $\sigma:\mathbb R\to\mathbb R$, its output is

$$g_\theta^{N_1,N_2}(x)=\frac1{N_2}\sum_{i=1}^{N_2}C^i\sigma\left(\frac1{N_1}\sum_{j=1}^{N_1}W^{2,i,j}\sigma(W^{1,j}\cdot x)\right).$$

Training samples $(x_k,y_k)$ are independent draws from a probability law $\pi$ supported on a compact product $X\times Y$. The three initial weight families are mutually independent and identically distributed within each family, with laws $\mu_c$, $\mu_{W^1}$, and $\mu_{W^2}$. Each law has a continuous density and compact support. The activation is twice continuously differentiable and, as the paper's $C_b^2$ notation requires, it and its first two derivatives are bounded. These are the standing conditions of Assumption 2.1.

At each step, SGD updates all parameters from the same previous parameter state and the same sample. The learning rates in equation (2.1) are $\alpha_C=N_2/N_1$, $\alpha_{W,1}=1$, and $\alpha_{W,2}=N_2$, applied with the step-size denominators in equation (1.4). The output at time $t$ is the output after $\lfloor N_1t\rfloor$ updates. For fixed $N_2$, the first-width limit is described by an $N_2$-particle system. Its first-layer particle retains both its initial first-layer vector and the full vector of its $N_2$ second-layer initial weights, because its dynamics depend on all of them. The second-width limit is a limiting integro-differential system for representative paths $\widetilde C_t^c$, $\widetilde W_t^{1,w}$, and $\widetilde W_t^{2,c,w,u}$.

Formalization targets

The main limit

For $t\in[0,1]$ and $x\in X$, the target is the existence and uniqueness of the limiting system (2.6), together with

$$\lim_{N_2\to\infty}\lim_{N_1\to\infty}g_t^{N_1,N_2}(x)=g_t(x) \quad\text{in probability}, \qquad g_t(x)=\int \widetilde C_t^c\,\sigma(\widetilde Z_t^c(x))\,\mu_c(dc).$$

The order is fixed: $N_1$ grows first while $N_2$ is held fixed. The goal states the entire Theorem 2.3, including the existence clause; without existence, convergence quantified only over solutions would have no content.

Quantitative intermediate limit

For the particle output $g_t^{N_2}$, the same theorem gives a constant $K<\infty$ such that

$$\sup_{x\in X}\mathbb E\bigl[|g_t^{N_2}(x)-g_t(x)|\bigr] \le \frac K{\sqrt{N_2}}.$$

The attack path records the finite-particle well-posedness of Lemma A.5; the first-width output limit stated after Lemma 2.2; the uniform particle bound (5.5); the sampling-variance estimate (5.9); the mean squared particle-error estimate (5.15); the output rate from Section 5.8; and uniqueness from Lemma 6.1. Each is a stated result or displayed assertion in the source. The rate and uniqueness milestones are also conclusions of the goal theorem.

Significance

The theorem specifies what the output of this trained network approaches, rather than only describing the parameters of a network at initialization. It connects the discrete SGD recursion to a finite particle system and then to a deterministic output from a limiting system. The $N_2^{-1/2}$ bound makes the second-width approximation quantitative, while uniqueness makes the limiting output independent of the choice of representative solution. These claims provide the basis for the paper's later discussion of global convergence under stronger assumptions; they do not themselves assert that training reaches a global minimum.

The paper proves the first-width and error estimates and gives a uniqueness argument for the limiting system. It asserts existence of a solution to (2.6) in Theorem 2.3, although a separate existence proof is not supplied there. A complete machine-checked development must account for that clause as well as the known arguments. No proof of this mission's goal or milestones is currently included in the draft Lean statements; they are targets for solvers. The network model, initialization law, and particle equations can also serve as reusable interfaces for further formal work on trained wide networks.

Difficulty

A direct large-width argument cannot treat the two widths as one undifferentiated limit. With $N_2$ fixed, the shared first-layer weights couple all second-layer units. The first limit is a stochastic statement about the SGD iterates and a particle system whose state includes a vector of initial second-layer weights. Only after that limit can the $N_2$ fluctuations be controlled. The second stage must bound both the sampling fluctuation of the representative output and the discrepancy between the particle paths and the limiting paths. The source's existence assertion also needs a mathematical justification in the specified continuous-solution class. Simply taking a pointwise limit of the network formula leaves all of these issues unresolved.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) for inputs, Fin N_1 and Fin N_2 for neuron indices, and Measure.pi or Measure.infinitePi for independent initial weights and data. The arrays of all widths live on one probability space with the stated product law. The SGD recursion is the simultaneous update (1.4), with the exact factors from (2.1), and time uses $\lfloor N_1t\rfloor$. The representative and particle systems are written in integral form. Solutions are jointly continuous on $[0,1]$ times the compact supports of their initial states; this supplies the regularity needed for the integrals and matches the class used in Lemma 6.1. No nonempty-input-set assumption or monotonicity assumption on $\sigma$ is added.

The inner probability limit in the goal uses a limsup in $N_1$. Footnote 2 writes an inner limit but does not assert its existence at every probability threshold; the limsup version implies its claim whenever that inner limit exists. A single rate constant works for all $t\in[0,1]$, all positive $N_2$, and all $x\in X$. The particle state includes the full vector of initial $W^2$ values, and the conditional expectation defining its second-layer preactivation is an integral over their product law at fixed initial $C$ values. The finite network, particle system, and limiting system must be connected by the stated results; an arbitrary output function with the desired limit would not formalize this theorem.

A complete development needs probability measures on product spaces, integrals of continuous functions on compact supports, convergence in measure, finite-sample variance estimates, and existence and uniqueness theory for the coupled integral systems. Contributions to these pieces and to the stated milestone theorems are within scope. The measure-valued Skorokhod-space statement of Lemma 2.2, numerical experiments, and the paper's separate global-convergence theorem are outside this mission.

Selected references

• Justin Sirignano and Konstantinos Spiliopoulos, Mean Field Analysis of Deep Neural Networks, Mathematics of Operations Research, 2022; arXiv:1903.04440v5 preprint, 2021. This mission uses the preprint's page and equation numbering.