All missions

Motivation

Monte Carlo tree search repeatedly chooses actions using estimates built from earlier simulations. The rewards attached to an action need not form an independent, identically distributed sequence: deeper parts of the search tree change as the search proceeds. Shah, Xie and Xu isolate this difficulty in a non-stationary multi-armed bandit and study a version of upper confidence bound selection with a polynomial exploration bonus. Their bandit theorem is the concentration result used in their subsequent analysis of tree search; it is a distinct finite-sample result with explicit assumptions and constants. Shah, Xie and Xu, §5–§7

The mission concerns Theorem 3 of arXiv:1902.05213v4, including both its expected-reward bound and its two-sided concentration bound. It provides the bandit foundation for the paper's later Monte Carlo tree search statements. The latter require a separate model of the search tree and are outside this mission. Shah, Xie and Xu, Theorems 1 and 3

Setting

A reward table has $K\ge1$ arms and random variables $X_{i,t}$, where $X_{i,t}$ is the reward obtained on the $t$th play of arm $i$. Every reward lies in $[-R,R]$ for a fixed $R>0$. The arm's empirical mean after $s\ge1$ plays is $\bar X_{i,s}=s^{-1}\sum_{t=1}^{s}X_{i,t}$, and the expectations of these means converge to $\mu_i$. Rewards may depend on earlier rewards, including rewards from other arms. The model imposes no independence or identical-distribution assumption. Shah, Xie and Xu, §5, equation (12)

The per-arm concentration assumption fixes $\beta>1$, $\xi>0$, and $1/2\le\eta<1$. For every $s,z\ge1$, both tails of $s\bar X_{i,s}-s\mu_i$ beyond $s^\eta z$ have probability at most $\beta/z^\xi$. This describes each arm's complete reward sequence without specifying a filtration or a sampling law. The limiting optimal arm $i_*$ has mean $\mu_*=\mu_{i_*}$; each other arm has gap $\Delta_i=\mu_*-\mu_i>0$. Shah, Xie and Xu, §5, equation (13)

A run chooses arm $I_t$ at round $t\ge1$. Its count $T_i(t)$ records how many rounds through $t$ chose arm $i$, and its average reward is $\bar X_n=n^{-1}\sum_iT_i(n)\bar X_{i,T_i(n)}$. The polynomial UCB index is $U_{i,s,t}=\bar X_{i,s}+B_{t,s}$ for $s>0$, with $B_{t,s}=\beta^{1/\xi}t^{\alpha/\xi}/s^{1-\eta}$. At round $t$, the run maximizes the index formed using counts and bonus time $t-1$. An unplayed arm has infinite priority, and ties among eligible arms are arbitrary. Shah, Xie and Xu, §5.1–§5.2, equations (14)–(16)

Formalization targets

Expected-reward convergence

Theorem 3.A bounds the gap between expected run reward and the best limiting arm mean. With $\Delta$ a positive lower bound for every $\Delta_i$, and $\eta'=\alpha/(\xi(1-\eta))$, the target for $n\ge1$ is

$$\left|\mathbb E[\bar X_n]-\mu_*\right|\le \left|\mathbb E[\bar X_{i_*,n}]-\mu_*\right|+ \frac{2R(K-1)}{n}\left[ \left(\frac{2\beta^{1/\xi}}{\Delta}\right)^{1/(1-\eta)}n^{\eta'}+ \frac{2}{\alpha-2}+1\right].$$

The first term is the optimal arm's own finite-sample bias. The remaining term is explicit in the bandit parameters. Lemma 2 and the displayed decomposition on page 18 are the curated targets for this part. Shah, Xie and Xu, Theorem 3.A and §6

Polynomial concentration

Theorem 3.B states that one constant $\beta'>1$, depending only on $R,K,\Delta,\beta,\xi,\alpha,\eta$, bounds both tails for every admissible reward table, measurable UCB run, horizon $n\ge1$, and $z\ge1$:

$$\mathbb P(n\bar X_n-n\mu_*\ge n^{\eta'}z),\quad \mathbb P(n\bar X_n-n\mu_*\le-n^{\eta'}z) \le \frac{\beta'}{z^{\xi'}},\qquad \eta'=\frac{\alpha}{\xi(1-\eta)}\in[1/2,1),\quad \xi'=\alpha-1>0.$$

The tuning parameter satisfies $\xi\eta(1-\eta)\le\alpha<\xi(1-\eta)$ and $\alpha>2$. Lemma 1, the event inclusion (34), the play-count tail (36), and Lemma 3 are the curated targets for this part. The same theorem statement carries parts A and B. Shah, Xie and Xu, Theorem 3 and §6.1–§6.3

Significance

The expected-reward bound relates the run's finite-horizon mean to the optimal arm's own mean and to an explicit penalty for sampling other arms. The concentration bound says that the run's cumulative reward inherits polynomial two-sided tails at a derived exponent. Together these claims let the paper apply a bandit guarantee in its analysis of Monte Carlo tree search, where an action's reward process changes as the search continues. Shah, Xie and Xu, §6–§7

The result is proved in the cited paper; the mission seeks a machine-checked Lean development of that known result. Its reward-table model and finite-sample count estimates may be reused when a sequential choice rule is analyzed without independent arm rewards. The mission currently provides compiled definitions and theorem statements as proof targets, not verified proofs of those targets.

Difficulty

A standard stationary-bandit analysis would replace each arm's history by independent draws from a fixed law. Here the assumptions give only convergence of expected arm means and polynomial per-arm concentration. A run also samples arms adaptively, so the random number of observed rewards on an arm cannot simply be inserted into a fixed-sample tail inequality. The finite-sample guarantee has to retain the exact dependence on the bonus, arm gaps, pull counts, and the tuning window. The paper's intermediate results identify the required count and tail statements. Shah, Xie and Xu, §6.1–§6.3

Formalization scope

Lean uses a probability space $\Omega$, a table $X:\mathrm{Fin}(K)\to\mathbb N\to\Omega\to\mathbb R$, and a run $I:\mathbb N\to\Omega\to\mathrm{Fin}(K)$. Play numbers begin at one; index zero is unused. The model makes reward measurability, boundedness, limiting expected means, and both concentration inequalities explicit. The run requires measurable arm-selection events so that its probabilities and bounded expectations are genuine. The model does not add independence, an identical-distribution condition, or a filtration.

The real index is compared only when every arm under comparison has a positive count; a separate clause gives unplayed arms the paper's $+\infty$ priority. The time argument of the index at round $t$ is $t-1$. The thresholds $A_i(t)$ and $A(t)$ use the paper's closed ceiling formulas. The paper's $\Delta_{\min}$ is represented by a positive lower bound $\Delta$ on all suboptimality gaps; setting $\Delta=\Delta_{\min}$ recovers the printed statement when that minimum is defined. Theorem 3 explicitly requires $K\ge1$ and $n\ge1$. The existential $\beta'$ precedes the probability space, rewards, run, $n$, and $z$, so it cannot change with an instance or horizon. Both parts of Theorem 3 are present, and the model's hypotheses are satisfiable for ordinary bounded bandits.

The mission needs reusable definitions for reward tables, empirical and run averages, pull counts, measurable runs, UCB selection and polynomial play thresholds. Contributions proving the six curated milestones, connecting them to the goal, or establishing reusable measurability and finite-sum facts are in scope. The pathwise two-sided reward decomposition is also posed as a supporting theorem.

Selected references

• Devavrat Shah, Qiaomin Xie, and Zhi Xu, Non-Asymptotic Analysis of Monte Carlo Tree Search, arXiv:1902.05213v4, 2020; published in Operations Research, 2022. arXiv preprint

Why reuse matters

In reinforcement learning, each policy update may require new interaction with an environment. When interaction is costly, an optimizer can retain past trajectories and use them again, provided it corrects for the different policy that generated them. Lin, Wang, and Zhou study this idea for natural policy gradient, using importance weights to reuse earlier state-action samples. Their rate result identifies how reuse changes the covariance of the optimization error, rather than measuring progress solely by the number of iterations. The result appears as Theorem 2 of their 2025 preprint, subsequently published in Operations Research.

The question is subtle because the reused data are correlated with the sequence of policies. A fresh sample drawn at iteration $n$ has the current occupancy distribution, while an old sample was drawn under an earlier policy and receives a likelihood ratio that depends on the current iterate. The inverse Fisher-information estimate adds another random factor. The covariance therefore has separate terms for gradient sampling and for the interaction between gradient sampling and the inverse-information estimate. The paper's §4 and Theorem 2 quantify both.

The model and algorithm

A discounted Markov decision process has states $S$, actions $A$, transition probabilities $P(s'\mid s,a)$, rewards $R(s,a)$, an initial-state law $\rho_0$, and a discount factor $0<\gamma<1$. A parameter $\theta\in\Theta\subseteq\mathbb R^d$ specifies a stochastic policy $\pi_\theta(a\mid s)$. Its objective $\eta(\theta)$ is the expected sum of discounted rewards. The discounted occupancy distribution $d^{\pi_\theta}(s,a)$ is the probability of observing $(s,a)$ when the time is geometrically distributed with parameter $1-\gamma$. It is this distribution, rather than the one-step transition law, that supplies the algorithm's samples.

At each iteration, the method draws $B$ state-action pairs from $d^{\pi_{\theta_n}}$. Its gradient estimate combines the current batch with $K-1$ earlier batches. A reused pair from iteration $m$ is weighted by $d^{\pi_{\theta_n}}(s,a)/d^{\pi_{\theta_m}}(s,a)$. The preconditioner is the inverse of a regularized empirical Fisher information matrix. The iterate moves in that preconditioned gradient direction and is projected back onto the feasible set $\Theta$. The source's equations (3)–(6) and Algorithm 1 define these operations; the paper fixes reuse to the gradient estimate alone for its convergence analysis in §3, p. 7.

Write $G(\xi,\theta)$ for the single-sample policy-gradient contribution, $S(\xi,\theta)$ for the score outer product, $\bar F^{-1}(\theta)$ for the mean regularized inverse Fisher estimate, and $\Sigma_\eta(\theta)$ for the covariance of $G(\xi,\theta)$. The two matrices governing the rate are

$$\Sigma_1(\theta)=\bar F^{-1}(\theta)\Sigma_\eta(\theta)\bar F^{-1}(\theta)^T, \qquad \Sigma_2(\theta)=\Sigma'_2(\theta)-\Sigma_1(\theta),$$

where $\Sigma'_2(\theta)$ averages $\hat F^{-1}\Sigma_\eta(\hat F^{-1})^T$ over a fresh Fisher batch. All three matrices are derived from the MDP and policy; none is supplied as a free covariance parameter.

Formalization targets

Suppose the RNPG iterates converge almost surely to $\bar\theta$, the paper's regularity and step-size conditions hold, and the linearization of the mean natural-gradient field at $\bar\theta$ is a Hurwitz matrix $\mathcal G$. For the normalized error $E_n=(\theta_n-\bar\theta)/\sqrt{\alpha_n}$, the goal is the marginal central limit conclusion of Theorem 2, p. 11:

$$E_n\ \Rightarrow\ \mathcal N(0,\Sigma_\infty),\qquad \operatorname{vec}(\Sigma_\infty) =-(\mathcal G\oplus\mathcal G)^{-1} \operatorname{vec}\!\left( \frac{\Sigma_1(\bar\theta)}{B} +\frac{\Sigma_2(\bar\theta)}{KB} \right).$$

Here $\operatorname{vec}$ stacks matrix columns and $\oplus$ is the Kronecker sum. The milestone list follows Lemmas 4–8 and display (10), pp. 12–13: three conditional covariance limits for the fresh-gradient and random-preconditioner terms, their combined covariance, then two limits for the fixed-state memory process. The formulas retain the paper's factors $1/(K^2B)$, $1/(KB)$, $(K-1)/(K^2B)$, and $(K-1)/(2KB)$.

What the result supplies

The limit law gives a quantitative description of the parameter error when the step size is small: the covariance is $\alpha_n\Sigma_\infty$ to first order. In the noise matrix, the $\Sigma_2$ contribution is divided by $K$, exposing the benefit of reusing gradient samples under the paper's assumptions. It also recovers the single-batch regime at $K=1$, where the memory terms vanish. These are claims about the algorithm's asymptotic statistical behavior, not guarantees that every finite run improves.

The paper proves the theorem analytically. This mission presents Lean statements and definitions; the open task is to give machine-checked proofs of those statements. A completed development would supply reusable finite-MDP occupancy and importance-weighted sampling interfaces, plus conditional-moment tools for stochastic approximation with finite memory. The marginal convergence claim is the goal; the source's additional process-level weak convergence to a stationary stochastic differential equation remains outside this mission.

The hard point

Treating the $K$ gradient batches as independent at every iteration gives the wrong covariance. An old batch appears in several successive estimates, and each reuse weight depends on the changing policy. Even the random inverse Fisher estimate cannot simply be replaced by its mean inside a covariance. The paper distinguishes the conditional fluctuation from the term carried by the stored history; the two have different limits, and a cross term survives in the accounting. The required result is a joint limit over a late starting time and a long averaging window, not a one-step variance calculation. This dependence is the central obstacle for the milestone chain in §4 and Appendix A.7–A.11.

Formalization scope

Lean uses finite, nonempty state and action types with discrete measurable structures, real rewards and parameters in a Euclidean space of positive dimension. All state-action and batch expectations are finite weighted sums. The objective itself is the unnormalized infinite discounted return from equation (1); occupancy is normalized. The policy family is defined on all of $\mathbb R^d$, while the bounds in Assumption 1 are imposed on $\Theta$. The theorem additionally requires $\bar\theta\in\operatorname{interior}(\Theta)$: at a boundary limit a projected iterate can have a one-sided normalized error, contradicting a nondegenerate centered Gaussian. The paper discusses the interior case just below Assumption 2 on p. 10.

The run draws separate independent gradient and Fisher batches, realizing Assumption 1(A.1.7). Before $K$ batches exist, its gradient estimate averages all batches available. A general filtration records the past; conditional matrix expectations are taken entrywise. The fixed-state lemmas condition on a stored-memory process whose future batches follow the occupancy law at fixed $\bar\theta$. The finite model writes the distributional continuity of Assumption 2(A.2.4) as pointwise continuity of the finite sample functions. The complete process-level SDE claim of Theorem 2, the separate almost-sure convergence Theorem 1, and the numerical examples are not formalized here.

The covariance matrices and limit law are computed from the policy, MDP, and RNPG run. An arbitrary covariance inserted as an extra hypothesis would erase the paper's main claim. Work on the published goal and the six paper-indexed milestones is welcome, as are supporting results for occupancy positivity, score identities, conditional expectations, and finite-memory stochastic approximation.

Selected references

• Yifan Lin, Yuhao Wang, and Enlu Zhou, Reusing Historical Trajectories in Natural Policy Gradient via Importance Sampling: Convergence and Convergence Rate, arXiv:2403.00675v2, 2025; published in Operations Research, 2025. Version used for all page and theorem citations.

Motivation

Hawkes processes are point processes in which every event raises the rate of future events. They are used to model contagion in financial markets, earthquake aftershocks, the spread of posts on social networks and arrivals to service systems (Hawkes 1971; Hawkes and Oakes 1974). Hawkes and Oakes showed that a stationary Hawkes process is a Poisson stream of immigrants, each of which starts an independent cluster of descendants. Many questions about a Hawkes process therefore reduce to questions about a single cluster: how many events it contains, when they occur, and how long it lasts.

For a homogeneous Poisson process, the classical conditional uniformity property says that, given the number of points in an interval, the points are distributed as sorted i.i.d. uniforms. A. Daw, Conditional Uniformity and Hawkes Processes (arXiv:2202.05335; Mathematics of Operations Research, 2024), establishes the analogue for a Hawkes cluster. After the random time change by the compensator, the event times of a cluster of known size are uniform on a polytope. Sampling from that polytope is organized by a combinatorial object, a uniformly random parking function. This mission formalizes that result.

Setting

Let $g:\mathbb R_+\to\mathbb R_+$ be the excitation kernel, with

$$\rho=\int_0^\infty g(t)\,dt<1,\qquad G(x)=\int_0^x g(u)\,du .$$

A cluster starts with an event at $A_0=0$. Each event at time $A_i$ adds $g(t-A_i)$ to the intensity, so the intensity is $\lambda_t=\sum_{i:A_i<t}g(t-A_i)$ (eq. (3) of the paper). Since $\rho<1$, the cluster is almost surely finite. Its events are $0=A_0<A_1<\dots<A_{N-1}$, and $N$ is the cluster size.

The compensator points are

$$\Lambda_j=\sum_{i=0}^{j-1}G(A_j-A_i),\qquad j=1,\dots,N-1,$$

the values of the compensator $\int_0^t\lambda_s\,ds$ at the event times (eq. (6)). For $k\in\mathbb N$, the polytope is

$$\mathcal P_k=\{x\in\mathbb R_+^k:\ x_i<i\rho\ \ \forall i,\ \ x_1<x_2<\dots<x_k\},$$

and the unit polytope $\bar{\mathcal P}_k$ is $\mathcal P_k$ with $\rho=1$.

A parking function of length $k$ is a vector $\pi\in\{1,2,\dots\}^k$ whose increasing rearrangement satisfies $\pi_{(i)}\le i$ for every $i$ (Definition 2). $\mathsf{PF}_k$ denotes the set of parking functions of length $k$. A $k$-step Dyck path is recorded as a non-decreasing integer vector $d$ with $1\le d_i\le i$; $\mathsf D_k$ denotes the set of them. Each $d\in\mathsf D_k$ determines the region

$$\bar{\mathcal P}_{k,d}=\{x\in\mathbb R_+^k:\ d_i-1\le x_i<d_i\ \ \forall i,\ \ x_1<\dots<x_k\}$$

(eq. (10)), and $\kappa_i(d)=|\{j: d_j=i\}|$ counts the coordinates of $d$ equal to $i$.

In the Lean development these are rho, bigG, compensator, polytope, unitPolytope, parkingFunctions, dyckPaths, dyckRegion and kappa, all in the namespace HawkesParking.Spine.

Formalization targets

Goal: Theorem 1 (pp. 12–13)

Given $N=k+1$, with $\pi$ uniform on $\mathsf{PF}_k$ and $U$ uniform on $(0,1)^k$ independent of $\pi$,

$$(\Lambda_1,\dots,\Lambda_k)\ \overset{D}{=}\ \rho\cdot\big((\pi-U)_{(1)},\dots,(\pi-U)_{(k)}\big).$$

The law of the compensator points does not depend on $g$ beyond $\rho$. Their spine is a uniformly random parking function.

Milestones, in attack order

1. Lemma 1 (p. 9): $|\mathsf{PF}_k|=(k+1)^{k-1}$.
2. Proposition 1 (p. 13): $\bar{\mathcal P}_k=\bigsqcup_{d\in\mathsf D_k}\bar{\mathcal P}_{k,d}$.
3. Volume of a Dyck region (proof of Proposition 2, p. 14): $\mathrm{vol}(\bar{\mathcal P}_{k,d})=\prod_{i=1}^k 1/\kappa_i(d)!$.
4. Proposition 2 (p. 14): the order statistics of $d-U$ are $\mathrm{Uni}(\bar{\mathcal P}_{k,d})$.
5. Proposition 3 (p. 15): $P(\Lambda\in\bar{\mathcal P}_{k,d})=P(\vec\pi=d)=k!\big/\big((k+1)^{k-1}\prod_{i=1}^k\kappa_i(d)!\big)$ for $\Lambda\sim\mathrm{Uni}(\bar{\mathcal P}_k)$.
6. Change of variables (proof of Lemma 2, p. 11): the joint density of $(\Lambda_1,\dots,\Lambda_k)$ on $\{N=k+1\}$ is $e^{-(k+1)\rho}$ on $\mathcal P_k$.
7. Equation (4) (p. 7): $P(N=k+1)=e^{-\rho(k+1)}(\rho(k+1))^k/(k+1)!$, the Borel$(\rho)$ law.
8. Lemma 2 (p. 10): given $N=k+1$, the conditional density of $(\Lambda_1,\dots,\Lambda_k)$ is $(1/\rho)^k(k+1)!/(k+1)^k$ on $\mathcal P_k$, i.e. $\Lambda\mid N\sim\mathrm{Uni}(\mathcal P_{N-1})$.

Significance

The result. Theorem 1 gives an exact description of a Hawkes cluster of known size. Combined with the Borel law of $N$, it yields an exact simulation algorithm: draw $N$, draw a uniform parking function and independent uniforms, and invert the compensator. In the paper this is Algorithm 1 and Proposition 4. For the exponential kernel it also yields a representation of the cluster duration as a sum of conditionally independent exponentials (Theorem 2). The result links self-exciting point processes to the combinatorics of parking functions and Dyck paths, which count labelled trees and are enumerated by Cayley-type formulas.

Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The mission formalizes the proof chain of Theorem 1: Pollak's count of parking functions, the Dyck decomposition of the polytope, the volume of each region, the identification of region probabilities with sorted-parking-function probabilities, and the change of variables behind Lemma 2. None of these objects, and no result about them, has a machine-checked proof on Prove2Me or in Mathlib. Mathlib has neither parking functions nor this encoding of Dyck paths.

Difficulty

Every step is elementary on paper; the difficulty is in the formal measure theory and combinatorics. The change of variables of Lemma 2 maps the ordered epochs to the polytope by a triangular, non-linear map whose Jacobian is the product of the pre-event intensities. This is exactly the factor in the cluster's likelihood. For a general integrable kernel, $G$ is only absolutely continuous and may be flat on intervals, so the multivariate change-of-variables theorem for $C^1$ diffeomorphisms does not apply directly.

Proposition 3 needs the number of parking functions sorting to a given Dyck path, $k!/\prod_i\kappa_i(d)!$, and their total count $(k+1)^{k-1}$, whose standard proof is Pollak's circular argument. Proposition 2 needs the law of order statistics of shifted uniforms with repeated shifts. The goal then assembles four measure identities, including a mixture over a finite set and a disjoint decomposition up to null sets.

Formalization scope

• The cluster is modelled by its likelihood. clusterLaw g k is the measure on $\mathbb R^k$ with density

$$e^{-(k+1)\rho}\prod_{j=1}^k\Big(\sum_{i<j}g(a_j-a_i)\Big)$$

on ordered epochs $0<a_1<\dots<a_k$, with $a_0=0$. This is the Janossy density of the point process with intensity (3) on $\{N=k+1\}$, and the proof of Lemma 2 (p. 11) works from the same quantity. Mathlib has no point processes with compensators, and the step from the intensity to the likelihood is classical, not part of this paper. No intensity-based definition is formalized. The model is checked by milestone 7: its total masses are the Borel probabilities.

• The cluster is not defined in compensator coordinates. It is a measure on epochs, pushed forward by the compensator map. Defining it as a uniform or constant-density law on $\mathcal P_k$ would make Lemma 2 definitional and is ruled out. Parking functions are defined by Definition 2, not as rearrangements of Dyck paths, so the counting in Proposition 3 is a theorem.
• Added hypotheses. IsKernel g bundles $g\ge0$ on $[0,\infty)$, integrability on $(0,\infty)$ and $\rho<1$ from the page. It adds two hypotheses: $g$ is measurable, and $\rho>0$. The latter is needed because for $\rho=0$ the event $N=k+1\ge2$ is null and $1/\rho$ is undefined.
• Conventions. $G$ uses $g$ extended by zero below $0$. Vectors are 0-indexed: the paper's coordinate $i$ is i : Fin k with value $i+1$. $\mathbb R_+=[0,\infty)$. Order statistics are v ∘ Tuple.sort v. "Given $N=k+1$" is the cluster law normalized by its total mass. The law of $\rho\cdot\mathrm{sort}(\pi-U)$ is written as the uniform mixture over $\pi\in\mathsf{PF}_k$. Theorem 1 is stated for the joint law, which implies the coordinatewise eq. (8). Eq. (4) is indexed by $k+1$.
• Infrastructure. A complete development needs four pieces of general machinery: a one-dimensional change of variables for monotone absolutely continuous maps, iterated by Fubini; volumes of ordered simplices; counting of multiset permutations; and Pollak's bijection. The parking-function and Dyck-path layer and the order-statistics lemma are reusable beyond this mission. Contributions to any milestone are welcome independently.

Selected references

• A. Daw, Conditional Uniformity and Hawkes Processes, Mathematics of Operations Research, 2024; preprint arXiv:2202.05335v2. https://arxiv.org/abs/2202.05335
• A. G. Hawkes, Spectra of some self-exciting and mutually exciting point processes, Biometrika 58(1), 1971. https://doi.org/10.1093/biomet/58.1.83
• A. G. Hawkes and D. Oakes, A cluster process representation of a self-exciting process, Journal of Applied Probability 11(3), 1974. https://doi.org/10.2307/3212693
• E. N. Brown, R. Barbieri, V. Ventura, R. E. Kass, L. M. Frank, The time-rescaling theorem and its application to neural spike train data analysis, Neural Computation 14(2), 2002. https://doi.org/10.1162/08997660252741149
• A. G. Konheim and B. Weiss, An occupancy discipline and applications, SIAM Journal on Applied Mathematics 14(6), 1966. https://doi.org/10.1137/0114101

Motivation

We establish a quantum version of the classical isoperimetric inequality relating the Fisher information and the entropy power of a quantum state. The key tool is a Fisher information inequality for a state which results from a certain convolution operation: the latter maps a classical probability distribution on phase space and a quantum state to a quantum state. We show that this inequality also gives rise to several related inequalities whose counterparts are well-known in the classical setting: in particular, it implies an entropy power inequality for the mentioned convolution operation as well as the isoperimetric inequality, and establishes concavity of the entropy power along trajectories of the quantum heat diffusion semigroup. As an application, we derive a Log-Sobolev inequality for the quantum Ornstein-Uhlenbeck semigroup, and argue that it implies fast convergence towards the fixed point for a large class of initial states.

This mission is the statement-level formalization of Geometric inequalities from phase space translations (arXiv:1606.08603v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1: convolution data processing (Lemma 1, (30), PDF p. 11). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1, (35)–(36): quantum Stam inequality; abstract seed: Canonical extended displacement family with output finite second derivatives established from local input C2 (hard)
• Lemma 3, (40): inverse-Fisher sensitivity: Source-pinned general-state entropy/Fisher analytic domain (source-ambiguity)
• Theorem 2: entropy-power concavity: Source-pinned general-state entropy/Fisher analytic domain (source-ambiguity)
• Theorem 3, (44): hybrid entropy power inequality: Source-pinned general-state entropy/Fisher analytic domain; differential-entropy and heat-asymptotic moment domain for arbitrary classical densities (source-ambiguity)
• Theorem 4, (51): entropy isoperimetry: Source-pinned general-state entropy/Fisher analytic domain (source-ambiguity)
• Theorem 5: energy-constrained attenuator optimum: Extended right entropy derivative convention on the full finite-mean state/law domain, and energy-constrained attainment with that convention (source-ambiguity)
• Theorem 6: constrained quantum/classical correspondence: Extended right entropy derivative convention on the full finite-mean state/law domain, and energy-constrained attainment with that convention (source-ambiguity)
• Theorem 8: geometric pure-death optimum: Extended right entropy derivative convention on the full finite-mean state/law domain, and energy-constrained attainment with that convention (source-ambiguity)
• Lemma 8, (62): relative entropy production identity: Source-pinned general-state entropy/Fisher analytic domain; well-defined rate/energy identities without infinity cancellations (source-ambiguity)
• Example 1: large-entropy OU convergence: Exact threshold together with a source-pinned domain for entropy/relative-entropy rates (source-ambiguity)
• Unnumbered (65): entropy/Fisher log-Sobolev inequality: Source-pinned general-state entropy/Fisher analytic domain (source-ambiguity)
• Lemma 9, (66)–(67): qOU log-Sobolev inequality: Source-pinned general-state entropy/Fisher analytic domain; well-defined rate/energy identities without infinity cancellations (source-ambiguity)
• Example 2: low-energy OU convergence: Exact threshold together with a source-pinned domain for entropy/relative-entropy rates (source-ambiguity)
• Lemma 10, (72): classical OU entropy derivative: Initial-density domain justifying entropy differentiation, integrability and vanishing boundary terms for the classical OU process (source-ambiguity)

Selected references

• Geometric inequalities from phase space translations, arXiv:1606.08603v2, https://arxiv.org/abs/1606.08603v2

Motivation

Let {\rho} the density matrix of a mixed Gaussian state. Assuming that one of the Robertson--Schr"odinger uncertainty inequalities is saturated by {\rho}, e.g. ({\Delta}^{{\rho}}X_1)^2({\Delta}^{{\rho}}P_1)^2={\Delta}^{{\rho}}(X_1,P_1)^2+(1/4)\hbar^2, we show that there exists a unique pure Gaussian state whose Wigner distribution is dominated by that of {\rho} and having the same variances and covariance {\Delta}^{{\rho}}X_1,{\Delta}^{{\rho}}P_1, and {\Delta}^{{\rho}}(X_1,P_1) as {\rho}. This property can be viewed as an analytic version of Gromov's non-squeezing theorem in the linear case, which implies that the intersection of a symplectic ball by a single plane of conjugate coordinates determines the radius of this ball.

This mission is the statement-level formalization of The Unique Pure Gaussian State Determined by the Partial Saturation of the Uncertainty Relations of a Mixed Gaussian State (arXiv:1205.5222v1). 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 Saturation of one Robertson–Schrödinger inequality gives minimal symplectic capacity (Section 4, First step (continued on p.8), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1 (both clauses): A corrected uniqueness and domination statement for normalized Gaussian physical states (source-ambiguity)
• Section 4, Second step: A valid uniqueness criterion for a quantum blob contained in a minimal-capacity ellipsoid (source-ambiguity)
• Proposition 2: A valid replacement for the claimed fixed conjugate-coordinate plane section-area identity (source-ambiguity)

Selected references

• The Unique Pure Gaussian State Determined by the Partial Saturation of the Uncertainty Relations of a Mixed Gaussian State, arXiv:1205.5222v1, https://arxiv.org/abs/1205.5222v1

Motivation

We show that Araki and Masuda's weighted non-commutative vector valued $L_p$-spaces [Araki & Masuda, Publ. Res. Inst. Math. Sci., 18:339 (1982)] correspond to an algebraic generalization of the sandwiched R'enyi divergences with parameter $\alpha = \frac{p}{2}$. Using complex interpolation theory, we prove various fundamental properties of these divergences in the setup of von Neumann algebras, including a data-processing inequality and monotonicity in $\alpha$. We thereby also give new proofs for the corresponding finite-dimensional properties. We discuss the limiting cases $\alpha\to \{\frac{1}{2},1,\infty\}$ leading to minus the logarithm of Uhlmann's fidelity, Umegaki's relative entropy, and the max-relative entropy, respectively. As a contribution that might be of independent interest, we derive a Riesz-Thorin theorem for Araki-Masuda $L_p$-spaces and an Araki-Lieb-Thirring inequality for states on von Neumann algebras.

This mission is the statement-level formalization of R'enyi divergences as weighted non-commutative vector valued Lₚ-spaces (arXiv:1608.05317v2). 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 Finite-dimensional identification of Araki–Masuda and sandwiched Rényi divergences (§4.1 Eq.(39); Definition 2 and Eq.(10), p.5; Definition 7, p.8, PDF p. 9). 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:

• Lemma 1: interpolation for products of spatial derivatives: Supported spatial derivative and its domain-sensitive complex powers in arbitrary normal representations (hard)
• Lemma 3: representation independence: Representation-indexed extended Araki–Masuda vector norms and GNS implementers (hard)
• Proposition 4: norm interpolation: General Araki–Masuda norms at reciprocal exponents, including infinity (hard)
• Corollary 5: convexity of log of the p-th power: Extended logarithm of the p-th power of the general Araki–Masuda norm (hard)
• Theorem 6: Riesz–Thorin for Araki–Masuda spaces: Extended induced operator norm between general Araki–Masuda spaces (hard)
• Lemma 8, monotonicity clause: General Araki–Masuda divergence with an infinity-order endpoint (hard)
• Lemma 8, full-range continuity clause: A valid finite-domain boundary hypothesis for the printed continuity assertion (source-ambiguity)
• Lemma 9: fidelity and max-relative entropy endpoints: General AM divergence, squared intertwiner fidelity, and domination infimum (hard)
• Proposition 11: three Petz-divergence properties: Petz spectral moments, Umegaki entropy, and endpoint extensions on arbitrary W*-algebras (hard)
• Theorem 12, Eq.(57): algebraic ALT divergence comparison: Distinct general AM and Petz divergences in the common order domain (hard)
• Theorem 12, Eq.(58): vector ALT assertion as printed: Support and representative restrictions missing from Eq.(58) (source-ambiguity)
• Theorem 13: Umegaki entropy as the alpha=1 limit: General AM divergence and extended spectral Umegaki entropy (hard)
• Theorem 14, Eq.(72): data processing: Normal unital completely positive observable maps and general AM divergences (hard)
• Theorem 14, Eq.(73): Stinespring vector inequalities: A consistent p=2 definition or a corrected reversed endpoint in Eq.(73) (source-ambiguity)
• §5 Eq.(81): tensor-product additivity: Spatial von Neumann tensor powers and product normal states with AM divergences (hard)
• §5 Eq.(84): lower bound on the strong converse exponent: General tensor-product testing exponent with extended limsup/liminf and AM variational bound (hard)
• Lemma 16: general interpolation for unbounded positive operators: Supported unbounded positive self-adjoint operators with genuine complex-power domains (hard)
• Lemma 20: Jensen for unbounded operators: Domain-sensitive closed quadratic-form compression, including potentially nondense form domains, and fractional powers (hard)

Selected references

• R'enyi divergences as weighted non-commutative vector valued Lₚ-spaces, arXiv:1608.05317v2, https://arxiv.org/abs/1608.05317v2

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