Probability

Motivation

Many optimization problems in statistics and machine learning constrain the variable to a smooth manifold: orthonormal frames in sparse PCA and dictionary learning (the Stiefel manifold), unit vectors in phase retrieval (the sphere), fixed-rank matrices in matrix completion. Riemannian optimization handles these problems directly on the manifold. A step is taken in the tangent space and mapped back to the manifold by a retraction.

In several applications the objective can be evaluated but not differentiated: black-box adversarial attacks, simulation-based models, and hyperparameter or policy tuning. Zeroth-order (derivative-free) methods replace the gradient by an estimator built from function values. In Euclidean space the standard construction is Gaussian smoothing, analysed by Nesterov and Spokoiny (2017) and Ghadimi and Lan (2013). Li, Balasubramanian and Ma (arXiv:2003.11238; Mathematics of Operations Research, 2023) carry the construction over to embedded submanifolds. They sample a Gaussian vector, project it onto the tangent space, and use the retraction in place of the straight line $x+\mu u$. This mission formalizes their first optimization guarantee: the convergence rate of zeroth-order Riemannian gradient descent (ZO-RGD).

Setting

Let $E$ be a finite-dimensional real inner product space (the ambient $\mathbb R^n$). Let $M\subseteq E$ be a $C^1$ embedded submanifold of dimension $d$. At each $x\in M$ the tangent space $T_xM$ is a $d$-dimensional linear subspace of $E$; let $P_x$ denote the orthogonal projection onto it. $M$ carries the metric induced by the inner product of $E$.

A retraction is a map $(x,\eta)\mapsto R_x(\eta)$ such that, for every $x\in M$, $R_x$ is smooth on $T_xM$, maps $T_xM$ into $M$, satisfies $R_x(0)=x$, and has the identity as its differential at $0$. In this mission $R_x$ is defined on all of $T_xM$.

For a differentiable $f:E\to\mathbb R$ the Riemannian gradient is $\operatorname{grad} f(x)=P_x\nabla f(x)$. Assumption 2.1 (retraction smoothness) asks for a constant $L\ge0$ such that

$$\big|f(R_x(\eta))-f(x)-\langle \operatorname{grad} f(x),\eta\rangle\big|\le \tfrac L2\|\eta\|^2\qquad(x\in M,\ \eta\in T_xM).$$

Given $\mu>0$ and a standard Gaussian vector $u_0\sim N(0,I_n)$ of $E$, set $u=P_xu_0$. The zeroth-order Riemannian gradient estimator is

$$g_\mu(x)=\frac{f(R_x(\mu u))-f(x)}{\mu}\,u .$$

ZO-RGD (Algorithm 1) starts at $x_0\in M$, draws independent Gaussian vectors $u_0^0,u_0^1,\dots$, and sets $x_{k+1}=R_{x_k}(-\hat\eta\, g_\mu(x_k))$, where $g_\mu(x_k)$ uses $u_k=P_{x_k}u_0^k$. The step size is $\hat\eta=1/(2(d+4)L)$. Let $x^*\in M$ be a minimizer of $f$ over $M$.

Formalization targets

Goal: Theorem 3.1

For every $N\ge0$,

$$\frac1{N+1}\sum_{k=0}^{N}\mathbb E\,\|\operatorname{grad} f(x_k)\|^2\le\frac4{\hat\eta}\left(\frac{f(x_0)-f(x^*)}{N+1}+C(\mu)\right),$$

where $4/\hat\eta=8(d+4)L$ and

$$C(\mu)=\frac{\mu^2L}{16}\frac{(d+3)^3}{d+4}+\frac{\mu^2L}{16}\frac{(d+6)^3}{d+4}+\frac{\mu^2L}{16}\frac{(d+6)^3}{(d+4)^2}.$$

Milestones

These are the paper's own intermediate results (§2.2, p. 8):

1. Lemma 2.1. For a subspace $\mathcal X$ with projection $P$, $u=Pu_0$ and $x\in\mathcal X$: $\mathbb E\langle x,u\rangle u=x$ and $\mathbb E\langle x,u\rangle^2=\|x\|^2$.
2. Lemma 2.2 (Nesterov–Spokoiny). $\mathbb E\|u\|^p\le(n+p)^{p/2}$ for $p\ge2$. This result is already on the platform as a proved theorem and is referenced.
3. Corollary 2.1. If $\dim\mathcal X=d$, then $\mathbb E\|Pu_0\|^p\le(d+p)^{p/2}$.
4. Proposition 2.1(a). $\|\mathbb E g_\mu(x)-\operatorname{grad} f(x)\|\le\frac{\mu L}{2}(d+3)^{3/2}$.
5. Proposition 2.1(b). $\|\operatorname{grad} f(x)\|^2\le2\|\mathbb E g_\mu(x)\|^2+\frac{\mu^2}{2}L^2(d+6)^3$.
6. Proposition 2.1(c). $\mathbb E\|g_\mu(x)\|^2\le\frac{\mu^2}{2}L^2(d+6)^3+2(d+4)\|\operatorname{grad} f(x)\|^2$.

Significance

Theorem 3.1 shows that ZO-RGD reaches an $\epsilon$-stationary point in expectation using $O(d/\epsilon^2)$ function evaluations, provided the smoothing parameter is of order $\epsilon/d^{3/2}$. The dimension that enters is the intrinsic dimension $d$ of the manifold, not the ambient dimension $n$. For the Stiefel manifold of $n\times p$ orthonormal frames this is the difference between $np-p(p+1)/2$ and $np$, and for the sphere between $n-1$ and $n$. More importantly, the estimator never explores normal directions. The three estimates of Proposition 2.1 are the toolkit that the paper reuses for its stochastic (ZO-RSGD), proximal (ZO-ManPG) and second-order variants.

The paper proves these results on paper; none of them has a machine-checked proof. The mission adds three things. It gives a precise model of a random iterate sequence on a submanifold, driven by the infinite product of Gaussian draws. It formalizes the projected-Gaussian identities, which are reusable for any method that samples in tangent spaces. And it pins down the constants. In checking the constants, the printed Proposition 2.1(b) turned out to be false for large $L$ (its proof yields $L^2$, not $L$), and the middle term of the printed $C(\mu)$ inherits that slip. The statements here carry the constants the proofs actually give.

Difficulty

In Euclidean space, $\mathbb E\,g_\mu(x)$ is exactly the gradient of the Gaussian-smoothed function $f_\mu(x)=\mathbb E f(x+\mu u)$, and the analysis runs on $f_\mu$. Once a retraction replaces $x+\mu u$, no smoothed function has $\mathbb E g_\mu$ as its gradient. The bias must be estimated directly from Assumption 2.1, which controls $f\circ R_x$ only along the tangent space. The moment bounds must then be taken for a Gaussian projected onto a subspace that changes with $x$.

In the descent argument, the direction $u_k$ is sampled in $T_{x_k}M$, which depends on all earlier draws. The expectation of step $k$ is therefore conditional on the past. Summing the one-step inequality requires conditional expectations on the product space, together with measurability of the iterate map. Finiteness of $\mathbb E f(x_k)$ is not given and must be handled as well.

Formalization scope

• Space. The ambient space is a finite-dimensional real inner product space $E$. The standard Gaussian is Mathlib's stdGaussian E, so $\kappa^{-1}\int\cdots e^{-\|u_0\|^2/2}du_0$ becomes integration against it.
• Manifold and tangent spaces. The manifold is given by the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold 1 d M, which ties $d$ to $M$. The tangent space is the published ProjLikeRetr.Retractor.tangentSpace M x, the span of Mathlib's tangent cone. Neither $d$ nor the tangent spaces are free parameters.
• Retraction. The retraction is global: Assumption 2.1 is required for every $\eta\in T_xM$ (the paper's "$\rho_x=\infty$"). "Smooth" means $C^\infty$, not analytic.
• Regularity of $f$. $f$ is assumed differentiable on $E$, which is what the definition $\operatorname{grad} f=P_x\nabla f$ needs. This is weaker than the paper's "smooth".
• Constants. The goal takes $L>0$, because the step size divides by $L$. The milestones take $L\ge0$ and $\mu>0$.
• Draws and iterates. The draws live on $E^{\mathbb N}$ with the infinite product of standard Gaussian measures. The iterates are defined for every $k$: the algorithm runs without a stopping time, so the sum over $k=0,\dots,N$ is meaningful.
• Minimizer. $x^*$ is an attained minimizer over $M$.
• Measurability. The goal adds two measurability hypotheses that make the iterates random variables: $(x,\eta)\mapsto R_x(\eta)$ is measurable and $x\mapsto P_x$ is measurable. Both hold for closed manifolds such as spheres and Stiefel manifolds.
• Corrected constants. Proposition 2.1(b) carries $L^2$, and the middle term of $C(\mu)$ carries $L$. The milestone texts keep the printed forms. Proposition 2.1(a) and (c) are as printed.
• Not formalized. The parameter choices $\mu=O(\epsilon/d^{3/2})$, $N=O(d/\epsilon^2)$ in the theorem's second sentence are an $O(\cdot)$ statement.

Several trivializing formalizations are ruled out. A Bochner integral of a non-integrable function is $0$, so every expectation in a conclusion is either a lower Lebesgue integral compared with a finite bound or paired with an integrability conjunct. The dimension $d$ comes from the manifold, not from a free natural number. The projection is onto $M$'s own tangent space, never onto an arbitrary subspace field.

A complete development needs the following infrastructure:

• the law of $P u_0$ (a standard Gaussian on the subspace);
• Gaussian moment bounds;
• conditional expectation along the product filtration;
• measurability of the iterate map.

The projected-Gaussian lemmas and the iterate model are reusable for the stochastic variant (ZO-RSGD) in the companion mission. Contributions of proofs for any milestone, and of general lemmas about Gaussian measures restricted to subspaces, are welcome.

Selected references

• J. Li, K. Balasubramanian, S. Ma, Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization, Mathematics of Operations Research, 2023; preprint arXiv:2003.11238v3, 2021. https://arxiv.org/abs/2003.11238
• Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17 (2017) 527–566. https://doi.org/10.1007/s10208-015-9296-2
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23 (2013) 2341–2368. https://doi.org/10.1137/120880811
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244

Motivation

In the classical secretary problem, candidates arrive one at a time in uniformly random order, and a decision maker must accept or reject each one irrevocably. The decision maker sees exact scores, or at least a total ranking of the candidates seen so far. In hiring, admissions and procurement the observed scores are often biased: evaluations of candidates from different groups, or produced by different evaluators, cannot be compared reliably, even when comparisons inside a group can. Salem and Gupta (SSRN 3444283; Management Science, 2023, doi:10.1287/mnsc.2023.4926) model this by giving the algorithm only the comparisons it can trust. These form a partial order on the candidates, and the true scores remain hidden.

The question is how much is lost when only partial ordinal information is available. The paper's answer is governed by the width of the partial order, the largest number of mutually incomparable candidates. Width 1 is the classical totally ordered problem. Width $N$ means that no comparison is available at all. This mission formalizes the paper's first positive result with explicit constants: an algorithm, ProxyLabel, whose competitive ratio grows linearly in a known estimate of the width.

Setting

A finite set $C$ of $N$ elements carries a partial order $\preceq$. Each element $a$ has a hidden true score $w(a) \ge 0$. The scores are pairwise distinct and consistent with the order: $a \prec b$ implies $w(a) < w(b)$. The width $\omega$ of $(C, \preceq)$ is the largest size of an antichain, a set of pairwise incomparable elements.

The elements arrive in a uniformly random order. The algorithm knows $N$ and a selection capacity $k \ge 1$. At each time it sees the comparisons of $\preceq$ among the elements that have arrived. It may select at most $k$ elements, and every decision is irrevocable. The offline optimum $\mathrm{OPT}$ is the largest total score of at most $k$ elements. An algorithm is $\rho$-competitive if, on every instance,

$$\mathbb E\Big[\frac{w(\mathrm{Alg})}{\mathrm{OPT}}\Big] \ge \frac1\rho,$$

where $w(\mathrm{Alg})$ is the total score of the selected elements and the expectation is over the arrival order and the algorithm's randomness.

ProxyLabel (Algorithm 1 of the paper) takes a width estimate $\omega' \in \mathbb N$. It works as follows.

1. Each element receives a label $\ell(a) \in \{1, \dots, k\}$, uniformly and independently.
2. It draws $m \sim \mathrm{Bin}(N, \omega'/(\omega'+1))$ and lets the sample $S$ be the first $m$ arrivals. Sampled elements are never selected.
3. A later element $a$ is selected if it is maximal among all previously seen elements with its label, sampled or not, and no element with its label has been selected yet.

Each label class therefore contributes at most one element: the first non-sampled one that beats everything of its label seen before.

Formalization targets

Goal: Proposition 5.2

If $\omega' \ge \omega / c$ for some $c \ge 1$, then ProxyLabel has competitive ratio at most

$$\rho = \frac{e^{c}(\omega'+1)}{\big(1 - \frac1k\big)^{k-1}} \ \le\ e^{c+1}(\omega'+1),$$

with the convention $0^0 = 1$. That is, $\mathbb E[w(\mathrm{Alg})] \ge \mathrm{OPT}/\rho$.

Milestones, from the proof (pp. 16–17)

1. Under uniform labels, the $j$-th best element is the maximum of its label class with probability $(1 - 1/k)^{j-1} \ge (1 - 1/k)^{k-1} \ge 1/e$.
2. Display (3): conditional on that event, it is selected with probability at least $\frac{1}{\omega'+1}\big(1 - \frac{1}{\omega'+1}\big)^{\omega}$.
3. If $\omega/c \le \omega'$ with $c \ge 1$, this quantity is at least $1/(e^{c}(\omega'+1))$.
4. Hence each of the top $k$ elements is selected with probability at least $(1 - 1/k)^{k-1}/(e^{c}(\omega'+1))$.
5. $\mathbb E[w(\mathrm{Alg})] \ge \sum_{i=1}^k \mathbb P(a_i \in \mathrm{Alg})\, w(a_i)$ over the top $k$ elements $a_1, \dots, a_k$.

Companion: Corollary 5.1

With the exact width $\omega' = \omega$, the ratio is at most $e(\omega+1)/(1 - 1/k)^{k-1} \le e^2(\omega+1)$, and it is $e(\omega+1)$ for $k = 1$.

Significance

Proposition 5.2 shows that partial ordinal information costs at most a factor linear in the width, provided a width estimate within a constant factor is available. Proposition 5.1 of the same paper shows that no algorithm beats ratio $\omega$, so the bound is order-optimal. ProxyLabel is also the building block of the paper's width-free algorithm PosetLabel (§5.4), which estimates the width from a first sample and then runs ProxyLabel's selection phase.

The result is proved in the paper and has not been machine-checked. A complete development would give a formal model of online selection on a poset under random arrival, with an explicit selection rule and exact finite averages for probabilities. It would also contain a formal use of Dilworth's theorem inside a probabilistic argument, and the elementary inequalities $(1 - 1/k)^{k-1} \ge 1/e$ and $(1 - 1/(\omega'+1))^{\omega} \ge e^{-c}$ in the form the proof needs.

Difficulty

The events of the algorithm are tangled. The sample is a prefix of a random order with a random length. Whether an element is selected depends on everything that arrived before it, on the labels, and on whether an earlier element of the same label was already selected. The bound must be proved for every finite poset and every consistent scoring, with exact constants, on the finite probability space of arrival orders, labellings and sample sizes. The width enters only through the structure of a single label class, a subposet whose width is at most $\omega$, so the argument has to pass from the global width to an arbitrary random subposet.

A tempting simplification lets every passing unsampled element be selected. That algorithm can select several elements of one label, so its expected score is larger and the bound becomes easier. It is not ProxyLabel.

Formalization scope

• Elements are a finite type α with a PartialOrder, so $N$ is Fintype.card α. The width $\omega$ is the published definition AppliedComb.Posets.width α, the maximum size of an antichain. Dilworth's theorem is the published, proved theorem AppliedComb.Posets.dilworth.
• A consistent scoring is $w : \alpha \to \mathbb R$ with $w \ge 0$, $w$ injective, and $a < b \Rightarrow w(a) < w(b)$. These three conditions are the paper's standing assumptions (§3.1, §3.3), not additions.
• Arrival orders are bijections α ≃ Fin N, and labellings are functions α → Fin k. Labels are independent of the order, which is the same distribution as assigning labels on arrival.
• Probabilities and expectations are explicit finite averages with weights $1/N!$, $1/k^N$ and the binomial weights $\binom{N}{m}p^m(1-p)^{N-m}$ with $p = \omega'/(\omega'+1)$.
• The selection rule is encoded exactly. An element is selected iff it is unsampled, no earlier element of its label (sampled or not) is above it, and no earlier unsampled element of its label passed the same test.
• OPT is the maximum of $\sum_{a \in s} w(a)$ over sets with $|s| \le k$, so it is the total score when $k \ge N$.
• The competitive ratio is stated as $\mathrm{OPT}/\rho \le \mathbb E[w(\mathrm{Alg})]$. This agrees with Definition 3.4 when $\mathrm{OPT} > 0$; the page's ratio is undefined when $\mathrm{OPT} = 0$.
• $(1 - 1/k)^{k-1}$ has a natural exponent, so $k = 1$ gives $0^0 = 1$. The width estimate $\omega'$ is a natural number.
• The proposition's "interval order" is a slip of the page: the algorithm and the proof concern arbitrary posets, and the goal is stated for every finite poset.
• The order-optimality clause of Corollary 5.1 refers to Proposition 5.1, the subject of mission II of this series, and is not stated here.
• The goal is a statement about the full expectation of the selected score over arrival order, labels and sample size. It is not the conditional bound (3). A formalization in which several elements per label can be selected, or in which "previously seen" excludes the sample, proves a statement about a different algorithm.

Contributions are welcome on every milestone. The prefix-of-a-random-order lemma (a binomially sized prefix is an i.i.d. Bernoulli sample) is reusable well beyond this mission.

Selected references

• J. Salem and S. Gupta, Secretary Problems with Biased Evaluations Using Partial Ordinal Information, SSRN 3444283 (version of 2022-04-17); Management Science, 2023. https://ssrn.com/abstract=3444283, https://doi.org/10.1287/mnsc.2023.4926
• R. P. Dilworth, A Decomposition Theorem for Partially Ordered Sets, Annals of Mathematics 51(1), 1950, 161–166. https://doi.org/10.2307/1969503
• R. Kleinberg, A Multiple-Choice Secretary Algorithm with Applications to Online Auctions, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070519

Payment channels and the cost of locked capital

Blockchains such as Bitcoin settle every transaction on a public ledger. Each on-chain transaction pays a fee and waits for confirmation, so frequent small payments are expensive. The Lightning Network moves such payments off-chain: two parties lock funds in a shared payment channel and pay each other by updating the channel's balance, touching the blockchain only to open, close or re-fund it. A channel is not free either. The locked funds cannot be used elsewhere, and once one side's balance is exhausted the channel has to be reset on-chain.

Guasoni, Huberman and Shikhelman (Lightning Network Economics: Channels, Management Science, 2023) quantify this trade-off in a stochastic model and compare three ways of settling two opposite streams of payments: on-chain transactions, unidirectional channels, and one bidirectional channel. Their comparisons all rest on a single computation, the expected discounted cost of a channel in closed form (Theorem 1). This mission formalizes that computation.

The model

Two nodes exchange unit payments. Node 1 pays node 2 one unit at each jump of a Poisson process $N^{\lambda_1}_t$ with rate $\lambda_1$; node 2 pays node 1 one unit at each jump of an independent Poisson process $N^{\lambda_2}_t$ with rate $\lambda_2$. The paper normalizes $\lambda_1\le\lambda_2$. The net balance of node 1 is

$$X_t=N^{\lambda_2}_t-N^{\lambda_1}_t,\qquad X_0=0 .$$

In a bidirectional channel node 1 commits $l_1$ units and node 2 commits $l_2$ units. The money is the channel's capacity: the channel works as long as $-l_1<X_t<l_2$. Locked capital has an opportunity cost of $r(l_1+l_2)$ per unit of time, where $r>0$ is the continuously compounded interest rate, and all costs are discounted at rate $r$. When the balance reaches $-l_1$ (node 1 is exhausted) or $+l_2$ (node 2 is exhausted), the channel is reset at cost $B$ and the balance restarts at $0$ with the same commitments.

Let $J(n)$ be the expected total future cost when the balance equals $n$. Conditioning on the first payment, which arrives after an exponential time with rate $\lambda_1+\lambda_2$, gives the first-step equation (15)

$$J(n)=(l_1+l_2)\frac{r}{r+\lambda_2+\lambda_1}+J(n+1)\frac{\lambda_2}{r+\lambda_2+\lambda_1}+J(n-1)\frac{\lambda_1}{r+\lambda_2+\lambda_1},\qquad -l_1<n<l_2,$$

with the reset conditions $J(-l_1)=J(0)+B$ and $J(+l_2)=J(0)+B$. The cost of the channel is $c^{l_1,l_2}(\lambda_1,\lambda_2)=J(0)$.

In a unidirectional channel only node 2 pays (rate $\lambda_2$) and only node 2 commits capital ($l_2$ units). The cost satisfies $J(n)=l_2\frac{r}{r+\lambda_2}+J(n+1)\frac{\lambda_2}{r+\lambda_2}$ for $0\le n<l_2$ with $J(l_2)=J(0)+B$, and $c^{0,l_2}(0,\lambda_2)=J(0)$.

The roots of the characteristic equation $\lambda_2\alpha^2-(\lambda_1+\lambda_2+r)\alpha+\lambda_1=0$ are

$$\alpha_\pm=\frac{\lambda_1+\lambda_2+r\pm\sqrt{(\lambda_2-\lambda_1)^2+r^2+2r(\lambda_2+\lambda_1)}}{2\lambda_2}. \tag{4}$$

Formalization targets

Goal: Theorem 1 (ii)

For $0<\lambda_1\le\lambda_2$, $r>0$, any $B$ and natural commitments $l_1,l_2\ge1$, the bidirectional cost system has a solution, and every solution satisfies

$$c^{l_1,l_2}(\lambda_1,\lambda_2)=l_1+l_2-B\,\frac{\alpha_-^{l_1}(1-\alpha_+^{l_1+l_2})-\alpha_+^{l_1}(1-\alpha_-^{l_1+l_2})}{\alpha_-^{l_1}(1-\alpha_+^{l_1+l_2})-\alpha_+^{l_1}(1-\alpha_-^{l_1+l_2})+\alpha_+^{l_1+l_2}-\alpha_-^{l_1+l_2}}. \tag{3}$$

Milestones

1. Competing exponential clocks (proof of Theorem 1, p. 10): the minimum $\tau$ of independent exponential times with rates $\lambda_2,\lambda_1$ is exponential with rate $\lambda_2+\lambda_1$, and $\tau^{\lambda_2}$ rings first with probability $\lambda_2/(\lambda_2+\lambda_1)$. This is a published, proved platform theorem, reused as is.
2. The first term (p. 10): $E[e^{-r\tau}]=(\lambda_2+\lambda_1)/(\lambda_2+\lambda_1+r)$ and $E[\int_0^\tau e^{-rs}r(l_1+l_2)\,ds]=(l_1+l_2)\,r/(r+\lambda_2+\lambda_1)$.
3. The last term (p. 10): $E[e^{-r\tau}J(X_{t+\tau})\mid X_t=n]=J(n+1)\frac{\lambda_2}{r+\lambda_2+\lambda_1}+J(n-1)\frac{\lambda_1}{r+\lambda_2+\lambda_1}$.
4. General solution of (15) (§5.1): on the lattice $-l_1\le n\le l_2$, (15) holds at the interior points if and only if $J(n)=l_1+l_2+k_1\alpha_-^n+k_2\alpha_+^n$ for constants $k_1,k_2$.
5. The cost function (§5.1): the closed form of $J(n)$ at every balance $n$, which gives (3) at $n=0$.
6. Theorem 1 (i), (1): $c^{0,l_2}(0,\lambda_2)=l_2+B\big(((r+\lambda_2)/\lambda_2)^{l_2}-1\big)^{-1}$.
7. Theorem 1 (i), (2): with $k=B\log(1+r/\lambda_2)$ and $B>0$, the minimum of (1) over real sizes is $\frac{B}{2k}\big(-k+\sqrt{k(k+4)}+2\log(\tfrac12(k+\sqrt{k(k+4)}+2))\big)$, attained at $l_2=\frac Bk\log(\tfrac12(k+\sqrt{k(k+4)}+2))$.

What the closed form gives

Formula (3) is what the rest of the paper works with. Lemma 1 prices on-chain settlement of a stream of rate $\lambda$ at $C\lambda/r$. Comparing that price with (1) and (3) yields the paper's thresholds on the on-chain fee below which no channel pays off (Theorem 2), the small-interest-rate asymptotics of the optimal symmetric channel, whose minimal cost scales like $3(2B\lambda/r)^{1/3}$ (Theorem 3), and the long-run number of channel payments per on-chain transaction (Proposition 2). Without an exact expression for the cost these comparisons would rest on simulation.

The paper proves Theorem 1 by a first-step argument and the solution of a linear difference equation. No part of it has been machine-checked. A formal proof would supply what the published argument passes over: that the first-step equation (15) and the reset conditions together have a unique solution on the lattice, that the denominator of (3) does not vanish, and the measure-theoretic computation of the coefficients of (15) from the exponential clocks. The later missions of this series (rate bounds, small-rate asymptotics, the balance walk) build on the same model.

Where the difficulty lies

The algebra of solving a second-order linear recurrence is routine. Two points are not. First, the solution has to be shown to exist and to be unique for every admissible set of parameters. This requires $\alpha_-\ne\alpha_+$ and a non-singular $2\times 2$ system for $k_1,k_2$, whose determinant is the denominator of (3), and the paper does not discuss when that determinant vanishes. Second, the coefficients of (15) come from expectations over exponential times: the joint expectation of the discount factor $e^{-r\tau}$ and the indicator of which clock rang first. The paper factors it as $E[e^{-r\tau}]\,P(\tau=\tau^{\lambda_2})$, which uses that the minimum is independent of the identity of the first clock, a fact it does not state.

Formalization scope

• The rates are written lam₁, lam₂; the sizes $l_1,l_2$ are natural numbers with $l_1,l_2\ge1$, because payments are of one unit and the balance lives on the lattice $\{-l_1,\dots,l_2\}$. The cost function is a map $J:\mathbb Z\to\mathbb R$ whose values off the lattice are unconstrained.
• The cost is defined by its equations, (15) with the reset conditions (IsBiCostFn) and the §5.2 system (IsUniCostFn), never by (3) or (1). Every statement about "the cost" asserts both that a solution exists and that every solution takes the stated value, so it is neither vacuous nor dependent on a choice of solution.
• The unidirectional system is a separate definition: the bidirectional one at $l_1=0$ would force $B=0$. For the same reason the Remark after Theorem 1 ("(1) follows from (3) by substituting $\lambda_1=l_1=0$") is not posed: with $\alpha_-=0$ and $l_1=0$ the denominator of (3) vanishes.
• Powers are natural powers in (1) and (3), integer powers (zpow) in the general solution and in $J(n)$, and real powers (Real.rpow) in the minimization (2), which is over real sizes $m>0$ as in the paper's proof.
• The paper prints the exponent in the numerator of the $J(n)$ display as $l+n$; the statement uses $l_1+n$, which is what the derivation gives and what reduces to (3) at $n=0$.
• The probabilistic milestones use Mathlib's expMeasure for the laws (through push-forward measures of measurable random variables) and IndepFun. Integrability is part of what is to be proved.
• The hypothesis $\lambda_1\le\lambda_2$ is kept in the goal as printed. No sign of $B$ is assumed except $B>0$ in (2), without which the infimum is not attained.
• Ruled out as trivializing: defining the cost as its closed form (which turns the goal into a definitional equality), fixing numerical parameters, restricting to $\lambda_1=\lambda_2$, and treating the sizes as real numbers in the cost system.

Contributions welcome: proofs of the milestones in any order, and reusable lemmas on linear difference equations with constant coefficients and on Laplace transforms of exponential laws, neither of which Mathlib currently has in this form.

Selected references

• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, Management Science, Articles in Advance, 2023. https://doi.org/10.1287/mnsc.2022.01664
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, technical report, 2015 (as cited by Guasoni et al.). https://lightning.network/lightning-network-paper.pdf

Motivation

Quantum state tomography reconstructs an unknown $d$-dimensional quantum state from measurements on many copies of it. For $n$ qubits, $d = 2^n$, so the number of copies a tomography procedure needs grows exponentially in $n$, and lower bounds on that number decide how far experiments can scale. In many experiments the only measurements available are Pauli measurements: each qubit is measured in the eigenbasis of one of $\sigma_x, \sigma_y, \sigma_z$.

Flammia and Liu, Direct fidelity estimation from few Pauli measurements (arXiv:1104.4695, Phys. Rev. Lett. 106, 230501, 2011), show that the fidelity of an experimental state with a target pure state can be estimated with far fewer copies than full tomography needs. To make the comparison meaningful they also prove that full tomography of a pure state with Pauli measurements requires $\Omega(d^2/\log d)$ copies. That lower bound has two steps. The first builds a large family of nearly orthogonal pure states whose Pauli expectation values are all small, so that Pauli measurements extract little information about which state is present. Its engine is Lemma 1 of the paper (p. 7), the subject of this mission. The second step, an information-theoretic argument over a noisy classical channel, is not in scope.

Setting

Fix $n \ge 1$ qubits and put $d = 2^n$. States are unit vectors $\psi \in \mathbb C^d$, $\|\psi\|_2 = 1$; the overlap $\langle\varphi|\psi\rangle = \sum_x \overline{\varphi_x}\psi_x$ is conjugate-linear in $\varphi$.

The single-qubit Pauli matrices are $I$, $\sigma_x$, $\sigma_y$, $\sigma_z$. A Pauli label $k \in \{0,1,2,3\}^n$ determines the $n$-qubit Pauli operator $W_k = \sigma_{k_1}\otimes\cdots\otimes\sigma_{k_n}$ (with $\sigma_0 = I$). There are $d^2$ labels; the all-zero label gives $W_k = I$. Every $W_k$ is Hermitian and unitary, so the Pauli expectation $\langle\psi|W_k|\psi\rangle$ is a real number in $[-1, 1]$.

A Haar-random state is a vector $\psi$ drawn from the uniform (rotation-invariant) probability measure on the unit sphere of $\mathbb C^d$, a real sphere of dimension $2d - 1$. The constants of the lemma are

$$\varepsilon = \sqrt{9\pi^3(\log 2)\,c},\qquad \tau = \sqrt{72\pi^3},\qquad C_1 = \frac{2}{9\pi^3},$$

with $\log$ the natural logarithm and $c > 0$ a parameter.

Formalization targets

Goal: Lemma 1

Let $\varphi_1, \dots, \varphi_s \in \mathbb C^d$ be states with $s \le 2^{cd}$. Then there is a state $\psi \in \mathbb C^d$ with

$$|\langle\varphi_i|\psi\rangle| \le \varepsilon \quad (1 \le i \le s), \qquad |\langle\psi|W_k|\psi\rangle| \le \tau\sqrt{\log d}/\sqrt d \quad (W_k \ne I).$$

These are (31) and (32) of the paper. The goal is an existence statement with no measure in it.

Milestones (all p. 7)

1. (33): for a state $\varphi$, $|\langle\varphi|\psi\rangle - \langle\varphi|\psi'\rangle| \le \|\psi - \psi'\|_2$.
2. $\mathbb E\langle\varphi|\psi\rangle = 0$ for Haar-random $\psi$.
3. (34): $\Pr[|\langle\varphi|\psi\rangle| \ge \varepsilon] \le 4\exp(-C_1 d\varepsilon^2/\eta^2)$ with $\eta = 1$.
4. (35): $\Pr[(31)\text{ fails for some } i] \le 4\exp(cd\log 2 - C_1 d\varepsilon^2) = 4\cdot 2^{-cd}$.
5. (36): on unit vectors, $|\langle\psi|W_k|\psi\rangle - \langle\psi'|W_k|\psi'\rangle| \le 2\|\psi - \psi'\|_2$.
6. $\mathbb E\langle\psi|W_k|\psi\rangle = 0$ for $W_k \ne I$.
7. (37): $\Pr[|\langle\psi|W_k|\psi\rangle| \ge \tau\sqrt{\log d}/\sqrt d] \le 4\exp(-C_1\tau^2(\log d)/\eta^2)$ with $\eta = 2$.
8. (38): $\Pr[(32)\text{ fails for some } k] \le 4\exp(2\log d - C_1\tau^2(\log d)/4) = 4/d^2$.

Every constant is the paper's; none is replaced by an unspecified absolute constant.

Significance

The result. Lemma 1 is a packing statement: applied repeatedly, it yields $2^{\Omega(d)}$ states that are pairwise almost orthogonal and whose non-identity Pauli expectations are all $O(\sqrt{\log d/d})$. Such states are hard to tell apart with Pauli measurements, since each measurement outcome is nearly unbiased. The paper converts this into the $\Omega(d^2/\log d)$ copy lower bound for full tomography with Pauli measurements (pp. 3, 7–8). Since direct fidelity estimation of an arbitrary pure state uses $O(d)$ copies (for fixed accuracy and failure probability), the lower bound is what shows that the scheme beats tomography followed by a fidelity computation by a factor of about $d$.

Formalizing it. The lemma and its proof are published, but none of it is machine-checked: Mathlib has no Pauli operators, no concentration of measure on spheres with explicit constants, and no Levy lemma. A formal proof needs a concentration inequality on the complex unit sphere with the explicit constant $C_1 = 2/(9\pi^3)$ (or any sharper one), the vanishing of the means by symmetry, and the union bounds. Each milestone is a reusable fact about Haar-random states.

Difficulty

The two union bounds (35) and (38) and the Lipschitz estimates (33) and (36) are elementary. The central difficulty is the tail bounds (34) and (37). The paper obtains them from Levy's lemma, which it cites (P. Lévy, 1951) and does not prove; Levy's lemma rests on the isoperimetric inequality on the sphere, which Mathlib does not have, and (37) concerns a quadratic form of $\psi$ rather than a linear one. Both tail bounds also need a working theory of the uniform measure on the complex unit sphere (rotation invariance, the distribution of a coordinate), little of which exists in Lean today.

A second difficulty is that the printed proof does not cover every parameter. The union bound produces a good $\psi$ only when $4\cdot 2^{-cd} + 4/d^2 < 1$. For small $d$, or small $c$ with few given states, the goal is still true, but a complete proof must handle those cases separately; they are not in the paper.

Formalization scope

• Representation. Basis labels are Q n = Fin n → Fin 2, Pauli labels P n = Fin n → Fin 4, states live in EuclideanSpace ℂ (Q n), and $W_k$ is the entrywise product of single-qubit Pauli matrices (the Kronecker product). $d$ is the real number $2^n$; $\log$ is Real.log; ⟨φ|ψ⟩ is Mathlib's inner ℂ φ ψ.
• Measure. The uniform measure on the sphere is Mathlib's Measure.toSphere of an additive Haar measure on $\mathbb C^d$ (as a real vector space), normalised to total mass one. The paper's "Haar-random vector in $S^{d-1}$" is read as this measure on the unit sphere of $\mathbb C^d$.
• Added hypotheses, all disclosed. The goal assumes $n \ge 1$: at $n = 0$ ($d = 1$) and small $c$ the lemma is false, since every unit vector of $\mathbb C^1$ has overlap $1$ with $\varphi_1$. It assumes $c > 0$, under which $\varepsilon$ is defined. "States" means unit vectors, for the given $\varphi_i$ and for the produced $\psi$. The mean-zero statement for Pauli operators assumes $W_k \ne I$ (for $W_k = I$ the mean is $1$); the paper's "for each $k$" refers to the non-identity labels of (32). "$W_k \ne I$" is formalized as "the label $k$ is not all zeros".
• Non-trivialization. The produced $\psi$ must be a unit vector, so $\psi = 0$ does not satisfy the goal; the given states are unit vectors, so (31) is not trivially false; and the mean-zero milestones assert integrability together with the value of the integral, so they cannot hold merely because a non-integrable integral is $0$.
• Infrastructure needed. Facts about $n$-qubit Pauli operators (Hermitian, unitary, traceless for $W_k \ne I$); rotation invariance of the normalised sphere measure; a concentration inequality for Lipschitz functions on the complex unit sphere with an explicit constant. The concentration inequality and the sphere-measure facts are reusable well beyond this mission and are welcome as separate contributions.

Selected references

• S. T. Flammia and Y.-K. Liu, Direct fidelity estimation from few Pauli measurements, Phys. Rev. Lett. 106, 230501 (2011); arXiv:1104.4695v3. https://arxiv.org/abs/1104.4695
• P. Lévy, Problèmes concrets d'analyse fonctionnelle, Gauthier-Villars, Paris, 1951 (reference [10] of the paper; no stable online link).
• M. Ledoux, The Concentration of Measure Phenomenon, Mathematical Surveys and Monographs 89, AMS, 2001. https://doi.org/10.1090/surv/089
• P. Hayden, D. W. Leung and A. Winter, Aspects of generic entanglement, Comm. Math. Phys. 265, 95–117 (2006); arXiv:quant-ph/0407049. https://arxiv.org/abs/quant-ph/0407049

Certifying a prepared quantum state

Experiments that prepare many-body entangled states (GHZ, W, stabilizer, cluster and matrix product states) need a way to check that the device produced the intended state. Full quantum state tomography answers the question but its cost grows with the dimension $d = 2^n$ of an $n$-qubit system: a reconstruction needs on the order of $d^2$ measurement settings. Entanglement witnesses are cheap but exist only for special states.

Direct fidelity estimation (S. T. Flammia and Y.-K. Liu, arXiv:1104.4695, Phys. Rev. Lett. 106, 230501, 2011; the same idea appears in M. P. da Silva, O. Landon-Cardinal and D. Poulin, arXiv:1104.3835) estimates only the one number the experimentalist needs, the fidelity of the prepared state $\sigma$ to the target pure state $\rho$. It measures a constant number of randomly chosen Pauli observables, independent of $n$, and needs only single-qubit measurements. The method has since become a standard benchmarking tool in experimental quantum information.

Setting

Consider $n$ qubits, $d = 2^n$. Let $W_k$, $k$ ranging over the $d^2 = 4^n$ labels in $\{0,1,2,3\}^n$, be the $n$-fold tensor products of the single-qubit matrices $I, \sigma_x, \sigma_y, \sigma_z$. The characteristic function of a $d\times d$ matrix $\rho$ is

$$\chi_\rho(k) = \mathrm{tr}(\rho W_k/\sqrt d).$$

The target $\rho$ is a pure state, $\rho = |\psi\rangle\langle\psi|$ with $\|\psi\| = 1$; the prepared $\sigma$ is an arbitrary state (positive semidefinite, trace one). For pure $\rho$ the fidelity is $F(\rho,\sigma) = \mathrm{tr}(\rho\sigma)$, and $\mathrm{tr}(\rho\sigma) = \sum_k\chi_\rho(k)\chi_\sigma(k)$.

Given an additive error $\varepsilon>0$ and a failure probability $\delta>0$, the protocol runs in two stages.

1. Importance sampling. Draw $\ell = \lceil 1/(\varepsilon^2\delta)\rceil$ labels $k_1,\dots,k_\ell$ independently with probability $\Pr(k) = \chi_\rho(k)^2$. The ideal estimator is $Y = \frac1\ell\sum_i X_i$, $X_i = \chi_\sigma(k_i)/\chi_\rho(k_i)$.
2. Finite precision. For each $i$, measure the observable $W_{k_i}$ on

$$m_i = \Big\lceil\frac{2}{d\,\chi_\rho(k_i)^2\,\ell\,\varepsilon^2}\log(2/\delta)\Big\rceil$$

copies of $\sigma$. Each measurement gives an outcome $A_{ij}\in\{1,-1\}$ with mean $\mathrm{tr}(\sigma W_{k_i}) = \sqrt d\,\chi_\sigma(k_i)$, independently. The output is

$$\tilde Y = \frac1\ell\sum_{i=1}^\ell\tilde X_i,\qquad \tilde X_i = \frac{1}{m_i\sqrt d\,\chi_\rho(k_i)}\sum_{j=1}^{m_i}A_{ij}.$$

Formalization targets

Goal: the direct-fidelity-estimation guarantee (p. 2)

For every $n$, every pure $\rho$, every state $\sigma$ and every $\varepsilon,\delta>0$,

$$\Pr\Big[\,\mathrm{tr}(\rho\sigma)\in[\tilde Y-2\varepsilon,\ \tilde Y+2\varepsilon]\,\Big]\ \ge\ 1-2\delta ,$$

the probability being over both stages of the protocol.

Milestones

• the fidelity formula (1) and the Pauli expansion (2) (p. 1), and the normalization of (3) (footnote [6], p. 4);
• unbiasedness $\mathbb E X = \mathrm{tr}(\rho\sigma)$ and the variance bound $\mathrm{Var}(X)\le\mathrm{tr}(\sigma^2)-[\mathrm{tr}(\rho\sigma)]^2\le1$ ((12)–(14), p. 6);
• the ideal-estimator bound (5), $\Pr[|Y-\mathrm{tr}(\rho\sigma)|\ge\varepsilon]\le\delta$;
• Hoeffding's bound (16)–(17), $\Pr[|\tilde Y - Y|\ge t]\le 2\exp(-2t^2/C)$, the computation (18), $C\le2\varepsilon^2/\log(2/\delta)$, and the finite-precision bound (8), $\Pr[|\tilde Y - Y|\ge\varepsilon]\le\delta$ for every fixed $k_1,\dots,k_\ell$;
• the resource bounds (9)–(10) on the expected number of copies and the deterministic bound $m_i\le1+2\log(2/\delta)/(\alpha^2\ell\varepsilon^2)$ for well-conditioned states.

Significance

The guarantee says that $\ell = \lceil1/(\varepsilon^2\delta)\rceil$ Pauli settings suffice to estimate the fidelity of any $n$-qubit state to any pure target, whatever $n$. The number of copies of $\sigma$ is $O(d)$ in expectation in the worst case and constant for stabilizer states, while the paper's lower bounds show that full tomography with Pauli measurements needs a number of copies polynomial in $d$. The same scheme, applied to the Choi state, certifies unitary channels and Clifford circuits.

The result is proved on paper but has not been machine-checked. A formal proof requires the Pauli-basis machinery (orthogonality and completeness of the $n$-qubit Pauli operators), the Born-rule model of repeated Pauli measurements, and the combination of a second-moment bound with a sub-Gaussian bound through a two-stage union bound. The formalization also corrects a printed slip: the paper's equality (13) holds only as an inequality (see the milestone's note), which does not affect the result.

Difficulty

Each individual step is classical: Chebyshev's inequality for the first stage, Hoeffding's inequality for the second. The difficulty lies in the bookkeeping that the informal proof leaves implicit. The first-stage estimator involves $1/\chi_\rho(k)$, which is undefined at labels the sampling never produces, so every probability must be weighted by $\Pr(k)$. The second-stage bound holds conditionally on the labels, and its sample sizes $m_i$ depend on them, so the two stages cannot be treated as one product of independent variables. The constant in Hoeffding's bound must be tracked through the $\sqrt d$ factors of $\chi$ and of $\mathbb E A_{ij}$, and through the ceiling in $m_i$. Finally, the Pauli expansion (2) requires the trace orthogonality $\mathrm{tr}(W_kW_{k'}) = d\,\delta_{kk'}$ of $n$-fold tensor products, which is not in Mathlib.

Formalization scope

• Basis labels are Q n := Fin n → Fin 2, Pauli labels P n := Fin n → Fin 4; matrices are Matrix (Q n) (Q n) ℂ, and $W_k$ is the entrywise product $\prod_i(P_{k_i})_{x_iy_i}$. $d$ is the real number $2^n$.
• Traces are real parts of complex traces (real on Hermitian matrices); $\chi_\rho(k)$ is real-valued.
• States are WildeQIT.IsDensityOperator (positive semidefinite, trace one), referenced from the platform; purity is $\rho = \psi\psi^\dagger$ with $\psi^\dagger\psi = 1$.
• $\lceil\cdot\rceil$ is Nat.ceil, $\log$ the natural logarithm.
• The first stage is a finite sum over label tuples weighted by $\prod_i\chi_\rho(k_i)^2$. The second stage is an explicit product measure: each $A_{ij}$ is $+1$ with probability $(1+\mathrm{tr}(\sigma W_{k_i}))/2$ and $-1$ otherwise. This Born-rule law is the unique $\pm1$ law with the page's mean $\sqrt d\,\chi_\sigma(k_i)$. The outcomes are not arbitrary random variables with hypothesised means, which would make the goal vacuous or false.
• Statements that divide by $\chi_\rho(k_i)$ either weight by $\Pr(k_i)$ or assume $\chi_\rho(k_i)\neq0$; none quantifies over all labels without weights.
• (9), (10), (18) and the well-conditioned bound assume $\delta<1$, so that $\log(2/\delta)>0$; the goal, (5) and (8) carry no such hypothesis.
• The goal does not mention variances, Chebyshev, Hoeffding's constant or (15), and it quantifies over every $n$, pure $\rho$, state $\sigma$ and $\varepsilon,\delta>0$. It cannot be discharged by a special case or a degenerate measure.

A complete development needs the Pauli-basis lemmas (Hermiticity, $W_k^2 = I$, trace orthogonality and the expansion of a matrix in the Pauli basis), a Born-rule lemma for $\pm1$ observables, and Hoeffding and Chebyshev bounds specialised to finite product measures. The Pauli-basis lemmas are reusable well beyond this mission (stabilizer formalism, shadow tomography, randomized benchmarking). Proofs of any milestone, and of auxiliary Pauli-basis facts, are welcome.

Selected references

• S. T. Flammia and Y.-K. Liu, Direct fidelity estimation from few Pauli measurements, Phys. Rev. Lett. 106, 230501 (2011); arXiv:1104.4695v3. https://arxiv.org/abs/1104.4695
• M. P. da Silva, O. Landon-Cardinal and D. Poulin, Practical characterization of quantum devices without tomography, Phys. Rev. Lett. 107, 210404 (2011). https://arxiv.org/abs/1104.3835
• R. Jozsa, Fidelity for mixed quantum states, J. Mod. Opt. 41, 2315 (1994). https://doi.org/10.1080/09500349414552171
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 13–30 (1963). https://doi.org/10.1080/01621459.1963.10500830