All missions

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.

Motivation

We formalize the task of unitary Schur sampling -- an extension of weak Schur sampling -- which is the process of measuring the Young label and the unitary group register of an input $m$ qudit state. Intuitively, this task is equivalent to applying the Schur transform, projecting onto the isotypic subspaces of the unitary and symmetric groups indexed by the Young labels, and discarding of the permutation register. As such unitary Schur sampling is the natural task in processes such as quantum state tomography or spectrum estimation. We generalize this task to unitary mixed Schur sampling to account for the recently introduced mixed Schur-Weyl transform. We provide a streaming algorithm which achieves an exponential reduction in the memory complexity and a polynomial reduction in the gate complexity over na"ive algorithms for the task of unitary (mixed) Schur sampling. Further, we show that if the input state has limited rank, the gate and memory complexities of our streaming algorithm as well as the algorithms for the full Schur and mixed Schur transforms are further reduced. Our work generalizes and improves on the results in arXiv2309.11947.

This mission is the statement-level formalization of A memory and gate efficient algorithm for unitary mixed Schur sampling (arXiv:2410.15793v2). 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 Four properties of homogeneous Littlewood–Richardson coefficients (Lemma 11, PDF p. 32). 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

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

• Theorem 1: A source-pinned approximation metric, exact synthesis exponent, and multivariate asymptotic convention. (source-ambiguity)
• Corollary 2: A source-pinned approximation metric, exact synthesis exponent, and multivariate asymptotic convention. (source-ambiguity)
• Lemma 8: A source-pinned approximation metric, exact synthesis exponent, and multivariate asymptotic convention. (source-ambiguity)
• Lemma 9: A source-pinned approximation metric, exact synthesis exponent, and multivariate asymptotic convention. (source-ambiguity)
• Remarks 1 and 4: A source-pinned approximation metric, exact synthesis exponent, and multivariate asymptotic convention. (source-ambiguity)
• Appendix B2, (B6)–(B9): A consistent total-memory bound and a classical bit-precision/gate model. (source-ambiguity)
• Appendix B3, (B20)–(B24): A consistent distinction between per-CG and streaming gate costs, and between state and total storage. (source-ambiguity)
• Appendix B3, (B13)–(B19): Consistent valid-support indexing at every recursion depth. (source-ambiguity)
• Lemma 5, (54)–(55): Constructed GT-basis CG/dual-CG maps and compatible path co-restrictions in both signs. (hard)
• Lemma 7, (59)–(60): An actual sequential path instrument, with fixed mixed Schur coordinates, final-label marginal, and conditional retained irrep state. (hard)
• Lemma 12, (C8)–(C9): Concrete rational staircase representations and the conjugate-tensor representation equivalence with canonical multiplicities. (hard)
• Lemma 14, (C21): A concrete mixed isotypic decomposition or exact mixed sector projector tied to U tensor-power m times conjugate U tensor-power n. (hard)

Selected references

• A memory and gate efficient algorithm for unitary mixed Schur sampling, arXiv:2410.15793v2, https://arxiv.org/abs/2410.15793v2

Motivation

We study and solve the problem of distilling secret key from quantum states representing correlation between two parties (Alice and Bob) and an eavesdropper (Eve) via one-way public discussion: we prove a coding theorem to achieve the "wire-tapper" bound, the difference of the mutual information Alice-Bob and that of Alice-Eve, for so-called cqq-correlations, via one-way public communication. This result yields information--theoretic formulas for the distillable secret key, giving ``ultimate'' key rate bounds if Eve is assumed to possess a purification of Alice and Bob's joint state. Specialising our protocol somewhat and making it coherent leads us to a protocol of entanglement distillation via one-way LOCC (local operations and classical communication) which is asymptotically optimal: in fact we prove the so-called "hashing inequality" which says that the coherent information (i.e., the negative conditional von Neumann entropy) is an achievable EPR rate. This result is well--known to imply a whole set of distillation and capacity formulas which we briefly review.

This mission is the statement-level formalization of Distillation of secret key and entanglement from quantum states (arXiv:quant-ph/0306078v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: one-way secret-key coding theorem (Theorem 1, 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.

Selected references

• Distillation of secret key and entanglement from quantum states, arXiv:quant-ph/0306078v1, https://arxiv.org/abs/quant-ph/0306078v1

Motivation

We characterize the bath resources needed to supply repeated uses of a fixed finite-dimensional quantum channel in a closed device. For each horizon $T$, one bath, one initial state and one repeated unitary are fixed before the user. Each output is returned before the next input arrives; no reset, discard, fresh ancilla or uncounted controller is available. Approximation error must vanish against arbitrary adaptive users with quantum memory and references. Writing $r=\lim \log_2(R_T)/T$ for the bath dimension rate and $s=\lim S(ω_T)/T$ for the actual initial entropy rate, we prove that the achievable region is exactly $s\ge 0$, $r+s\ge h$ and $r-s\geκ$. Here $h$ is maximum entropy exchange and $κ$ is a smoothed independent-reference extension cost, with the zero-error limit taken before the supremum over full-rank inputs. Its exact fixed-input form is an affine transform of the zero-leakage quantum privacy funnel. The minimum dimension rate is $(h+κ)/2$. The proof combines entropy converses, a bath-dimension-independent support repair, and a closed adaptive implementation of encoder-only fully quantum Slepian--Wolf recycling. All seeds, clocks, workspace and retained residues are counted. Worked examples include dephasing, pure replacement and a qubit channel with $0<κ<h$. No computability of $κ$ or efficient circuit synthesis is claimed. △ Less

This mission is the statement-level formalization of Bath dimension and initial entropy for closed repeated use of a quantum channel (arXiv:2609.18267v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.1: uniform collision gain (Theorem 3.1, 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

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

• Theorem 2.1 (seed paper result): exact bath-dimension/initial-entropy rate region: Closed all-horizon causal device and complete adaptive process metric, actual rate-limit region, counted padding/internal-purification transformations (hard)
• Theorem 2.2: same-spectrum converse: Same actual initializer in two complete adaptive tester experiments and all-integer liminf resource rates (hard)
• Theorem 5.1: causal balancing for any fixed finite exact witness: Causal block compiler with actual flat initializer, repeated-unitary semantics and separately converging seed/data rates (hard)
• Proposition 7.1: unitary channels: Complete all-horizon memory rate c_seq and bath-free repeated-unitary realization (hard)
• Proposition 7.2: qubit dephasing and exact streaming corner: Counted exact streaming process from independent Pauli generators, ordered history words and one clocked unitary (hard)
• Proposition 7.3: pure replacement: Pure-replacer complete operating memory rate and counted preallocated-cell/clock process (hard)
• Proposition 8.1: shared-seed marginal/complete separation: Shared-bit repeated controlled-Z process, product-marginal repeatability and supremum complete adaptive error (hard)
• Section 8, unnumbered: zero memory rate iff unitary: Zero complete operating memory rate as an asymptotic repeated-service property (hard)
• Lemma A.1: fixed adaptive spectral concentration projector: Reachable states of adaptive controllers with fresh comparison channels and untouched spent Lambda outputs (hard)
• Lemma A.2: simultaneous bath/exterior/source support and spectral-cap cuts: Exact comparison block and pure complete exterior, including future-accessed spectators and their purifiers (hard)
• Lemma A.4: exact integer wires and reversible flat-stock preparation: Reversible flat-stock preparation and permanent wire/tranche allocation with immediate collision service (hard)
• Proposition A.5: joint recycling, every prefix, and one repeated unitary: Joint comparison boundary invariant, actual block composition, every prefix and counted repeated-unitary clock (hard)
• Proposition A.6: exact actual spectrum and every-horizon limits: Every-integer-horizon compiled family with actual flat spectrum, exact physical counts and separate seed/data limits (hard)

Selected references

• Bath dimension and initial entropy for closed repeated use of a quantum channel, arXiv:2609.18267v1, https://arxiv.org/abs/2609.18267v1

Motivation

In this paper we fill the gap in previous works by proving the formula for entanglement-assisted capacity of quantum channel with additive constraint (such as bosonic Gaussian channel). The main tools are the coding theorem for classical-quantum constrained channels and a finite dimensional approximation of the input density operators for entanglement-assisted capacity. The new version contains improved formulation of sufficient conditions under which suprema in the capacity formulas are attained.

This mission is the statement-level formalization of Entanglement-assisted capacity of constrained quantum channel (arXiv:quant-ph/0211170v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Trace-norm compactness of an energy sublevel (§3, unnumbered Lemma (proof on PDF p.11), PDF p. 10). 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:

• §1, Proposition 1: An operational constrained c-q coding model on arbitrary input alphabets and general trace-class output states, with genuine product outputs, bounded POVMs, maximal message error, and a liminf achievable-rate capacity. (hard)
• §1, Proposition 2 (conclusion on p.3): Borel-probability barycenters and integrated entropy for trace-norm state-valued maps, coupled to a genuine bounded-below unbounded selfadjoint observable with Gibbs trace. (hard)
• §2, Proposition 3, (19)--(20): Parallel general trace-class CPTP channel powers, constrained block codes and two separately defined information optimizations with different feasible sets. (hard)
• §3, Proposition 4, (30): Energy-constrained operational entanglement-assisted block capacity on arbitrary Hilbert spaces, plus actual purification/reference extension and the finite-entropy mutual-information interface. (hard)
• §3, (31)--(32): The special locally encoded common-resource assisted ensemble class and its block Holevo optimum, distinct from operational assisted codes. (hard)
• §3, assertion before (33): Constrained channel mutual information for arbitrary entangled block states, with actual reference purifications and additive energy expectation. (hard)
• §3, finite-rank approximation and (35) on p.10: Constructed positive-eigenvalue spectral truncations, their normalized purifications, and channel mutual information in one compatible operator model. (hard)
• §3, Proposition 5, (37): Actual dual-channel domination for bounded-below unbounded output observables, Gibbs trace, and an operational assisted capacity attaining state. (hard)
• Closing paragraph; (30) with (36): Extended-valued relative-entropy channel mutual information coupled to operational assisted capacity without either entropy restriction. (hard)

Selected references

• Entanglement-assisted capacity of constrained quantum channel, arXiv:quant-ph/0211170v2, https://arxiv.org/abs/quant-ph/0211170v2

Motivation

The Schur transform, which block-diagonalizes the tensor representation $U^{\otimes n}$ of the unitary group $\mathbf{U}_d$ on $n$ qudits, is an important primitive in quantum information and theoretical physics. We give a generalization of its quantum circuit implementation due to Bacon, Chuang, and Harrow (SODA 2007) to the case of mixed tensor $U^{\otimes n} \otimes \bar{U}^{\otimes m}$, where $\bar{U}$ is the dual representation. This representation is the symmetry of unitary-equivariant channels, which find various applications in quantum majority vote, multiport-based teleportation, asymmetric state cloning, black-box unitary transformations, etc. The "mixed" Schur transform contains several natural extensions of the representation theory used in the Schur transform, in which the main ingredient is a duality between the mixed tensor representations and the walled Brauer algebra. Another element is an efficient implementation of a "dual" Clebsch-Gordan transform for $\bar{U}$. The overall circuit has complexity $\widetilde{O} ((n+m)d^4)$. Finally, we show how the mixed Schur transform enables efficient implementation of unitary-equivariant channels in various settings and discuss other potential applications, including an extension of permutational quantum computing that includes partial transposes.

This mission is the statement-level formalization of The mixed Schur transform: efficient quantum circuit and applications (arXiv:2310.01613v1). 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 Two-input conclusive teleportation: exact success and corrected output (Section 5.1.1: two-input conclusive teleportation success, PDF p. 29). 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

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

• Main result / Corollary 4.12: efficient mixed Schur isometry: Concrete signed-staircase rational irreps with orthonormal GT and dimension-truncated path coordinates, their fixed mixed Schur isometry, and its binary channel/resource semantics. (hard)
• Section 3.3 and Remark 3.1: cascade correctness and factor-order flexibility: Ordinary and dual CG maps on the concrete signed GT sectors, path extension/reindexing and canonical permutations for factor type words. (hard)
• Theorem 4.5: multiplicity-free dual Wigner–Eckart: Concrete rational-irrep actions in GT bases and the actual multiplicity-free dual CG matrix. (hard)
• Proposition 4.6: dual CG coefficient tensor operators: The source dual CG coefficient blocks and their concrete irrep actions. (hard)
• Lemma 4.7: restriction of the coefficient tensor operators: Compatible GT restriction inclusions between U(d) and U(d-1) and actual coefficient tensor blocks. (hard)
• Proposition 4.8: reduced Wigner coefficient recursion: The constructed restriction blocks and reduced coefficients relative to the lower-dimensional source dual CG transform. (hard)
• Section 4.3 Eqs.(69)–(71): recursive factorization: The modified lower dual transform and reduced Wigner rotation on valid dependent label sectors. (hard)
• Remark 4.10: coherent reduced Wigner operator synthesis: A concrete reduced-Wigner target in the source GT conventions and its uniform reversible finite-precision coefficient/synthesis computation. (hard)
• Corollary 4.11: efficient dual Clebsch–Gordan transform: The actual coherent dual CG transform over bounded staircase labels and its encoded circuit/workspace interface. (hard)
• Remark 4.13: extensions to elementary and symmetric-power input irreps: Remark 4.13: extensions to elementary and symmetric-power input irreps (source-ambiguity)
• Proposition 5.2: deterministic one-input teleportation implementation: Proposition 5.2: deterministic one-input teleportation implementation (source-ambiguity)
• Section 5.1.1: random symmetric unitaries and random equivariant channels: Section 5.1.1: random symmetric unitaries and random equivariant channels (source-ambiguity)
• Proposition 5.5: Choi-only average-case observable prediction: A Choi-measurement training law, actual learned estimator function and cost-bearing classical learner implementing the HCP adaptation. (hard)
• Lemma 5.10: Schur-sparse Choi and square-root block encodings: Valid Schur-label encodings of the actual fixed transform and two-sided sparse row/column/value oracle programs with gate/query accounting. (hard)
• Proposition 5.11: output expectation estimation from a Choi square root: Proposition 5.11: output expectation estimation from a Choi square root (source-ambiguity)
• Section 5.1.3: combined diagonal/sparse estimation bounds: Section 5.1.3: combined diagonal/sparse estimation bounds (source-ambiguity)
• Section 5.1.3: composition by square-root Choi block encodings: Section 5.1.3: composition by square-root Choi block encodings (source-ambiguity)
• Section 5.2: partially transposed permutational quantum computing: Section 5.2: partially transposed permutational quantum computing (source-ambiguity)

Selected references

• The mixed Schur transform: efficient quantum circuit and applications, arXiv:2310.01613v1, https://arxiv.org/abs/2310.01613v1

Motivation

The maximum rates for reliably transmitting classical information over Bosonic multiple-access channels (MACs) are derived when the transmitters are restricted to coherent-state encodings. Inner and outer bounds for the ultimate capacity region of the Bosonic MAC are also presented. It is shown that the sum-rate upper bound is achievable with a coherent-state encoding and that the entire region is asymptotically achievable in the limit of large mean input photon numbers.

This mission is the statement-level formalization of Multiple-Access Bosonic Communications (arXiv:quant-ph/0506171v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Operational homodyne and heterodyne coherent-state MAC regions (§II.B, (5)–(8): single-mode homodyne/heterodyne capacity regions, 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

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

• §II.B,(9)–(11): Normalized coherent-state Fock ensembles and collective-receiver product-code MAC capacity (hard)
• §II.B,(12): Additive random-displacement Fock channel and operational product-code capacity (hard)
• §II.C,(23)–(27): Collective-receiver wideband bosonic coding and Gaussian ensemble entropy (hard)
• §III.A,(35)–(40),(50)–(58): Physical Gaussian displaced-state mixtures, raw second moments, and infinite-dimensional entropy (hard)
• §III.A,(48)–(49): Individual Holevo maximization over physical displacement laws (hard)
• §III.A,(57)–(58): Joint Holevo sum functional for independent physical displacement laws (hard)
• §III.A,(31)–(34),(59): Operational HSH two-sender capacity with physical Gaussian seed (hard)
• §III.B,(60)–(65): Fixed-seed Gaussian beam-splitter MAC and photon-budget accounting (hard)
• §III.B,(66),Fig.5: Operational fixed-seed Gaussian region realizing the explicit strict extension (hard)
• §IV,Theorem 1,(67)–(74): Anisotropic attenuator, thermal entropy conjecture, squeeze whitening, and ordinary classical capacity (hard)
• §IV,(75)–(76): Physical displaced squeezed-seed coding and unconditional anisotropic-channel capacity lower bound (hard)
• §IV,(77): Thermal attenuator capacity and conditional specialization (hard)
• §IV,(78)–(79): Pure squeezed-environment attenuator capacity and equal-energy thermal comparison (hard)
• §V,(80) and individual bounds: Ultimate independent-sender bosonic capacity allowing across-use entanglement (hard)
• §V, coherent-state sum achievement: Physical coherent encoding attaining the ultimate MAC sum capacity (hard)
• §V, Gaussian sum achievement: Pure one-port Gaussian seed output and above-threshold physical sum code (hard)
• Appendix,(A.1): Photon-support-constrained operational quantum MAC regions and their closed limit (hard)
• Abstract; §V,PDF pp.9–10: Unspecified whole-region high-energy convergence notion (source-ambiguity)

Selected references

• Multiple-Access Bosonic Communications, arXiv:quant-ph/0506171v2, https://arxiv.org/abs/quant-ph/0506171v2