Statistics

Motivation

Graph alignment asks for the correspondence between the vertices of two graphs that are noisy copies of each other with hidden labels. It arises in the de-anonymization of social networks, where an anonymized friendship graph is matched against a public one (Narayanan–Shmatikov 2009), and in computational biology, where protein–protein interaction networks of related species are aligned. The standard random model is the correlated Erdős–Rényi model of Pedarsani–Grossglauser 2011, for which exact recovery thresholds are known (Cullina–Kiyavash 2016) and almost-exact recovery is known to be impossible when $nqs=O(1)$ (Cullina–Kiyavash–Mittal–Poor 2018).

Hall and Massoulié (arXiv:2007.00533) study the weaker goal of partial recovery: output a permutation that agrees with the hidden one on a constant fraction $\alpha$ of the vertices. This mission formalizes their impossibility theorem; a companion mission (II) formalizes their possibility theorem.

Setting

Fix $n$ and scalars $0\le q<s\le1$. A parent graph $G\sim G(n,q/s)$ is copied twice and each copy keeps every edge independently with probability $s$, giving graphs $G_A$ and $G_{B'}$ with adjacency matrices $A$ and $B'$. Every unordered pair $\{i,j\}$ of distinct vertices independently carries the pair $(A_{ij},B'_{ij})\in\{0,1\}^2$ with law $P$ (equation (3)):

$$p_{00}=1-2q+qs,\qquad p_{01}=p_{10}=q(1-s),\qquad p_{11}=qs .$$

Two independent edges of $G(n,q)$ have law $Q$ (equation (4)):

$$q_{00}=1-2q+q^2,\qquad q_{01}=q_{10}=q(1-q),\qquad q_{11}=q^2 .$$

The Kullback–Leibler divergence is $D(P\|Q)=\sum_{x\in\{0,1\}^2}P(x)\log\frac{P(x)}{Q(x)}$.

A hidden permutation $\pi^*$ of the vertices, drawn uniformly from the $n!$ permutations, relabels $G_{B'}$ into $G_B$: $B_{\pi^*(i)\pi^*(j)}=B'_{ij}$. An algorithm sees only $(A,B)$ and returns a permutation $\hat\pi$, possibly at random. Its quality is the overlap

$$\beta(\hat\pi,\pi^*)=\frac1n\sum_{i=1}^n\mathbf 1_{\hat\pi(i)=\pi^*(i)} .$$

The mutual information $I(\pi^*;(A,B))$ is that of the joint law of $\pi^*$ and the observation, and $M_\alpha=\max_{\pi^*}|\{\pi\mid\beta(\pi,\pi^*)\ge\alpha\}|$ counts the permutations that are $\alpha$-close to a given one, out of $M=n!$.

Formalization targets

Goal: Theorem 2.1 (p. 8)

Let $\alpha_n\in(0,1)$, bounded below by a constant $c>0$ for large $n$. If

$$\frac{D(P\|Q)}{\alpha_n}=o\Big(\frac{\log n}{n}\Big),$$

then for every sequence of algorithms,

$$\mathbb P\big[\beta(\hat\pi,\pi^*)<\alpha_n\big]\to1\qquad(n\to\infty).$$

Milestones

1. Theorem 3.1 (generalized Fano inequality): $\mathbb P[d(\hat Z,Z)>d]\ge1-\frac{I(Z;\hat X)+1}{\log(M/M_d)}$ for any Markov chain $Z\to\hat X\to\hat Z$ with $Z$ uniform.
2. Corollary 3.2: $\mathbb P(\beta(\hat\pi,\pi^*)<\alpha)\ge1-\frac{I(\pi^*;(A,B))+1}{\log(M/M_\alpha)}$.
3. Proposition 3.3: $M/M_\alpha=\Omega(\lceil n\alpha\rceil!)$.
4. Inequality (8): $I(\pi^*;(A,B))\le\mathbb E_{\pi^*}\big[D(\mathbb P((A,B)=\cdot\mid\pi^*)\,\|\,\mathcal Q)\big]$, with $\mathcal Q$ the law of two independent $G(n,q)$ graphs.
5. The display after (8), p. 13: $I(\pi^*;(A,B))\le\binom n2D(P\|Q)$.

Significance

The theorem gives a sufficient condition, in terms of a single per-pair divergence, under which no algorithm (efficient or not) recovers even a fraction $\alpha$ of the alignment. Together with the companion possibility result (Theorem 2.3: partial recovery is possible when $nqs$ exceeds an explicit constant under sparsity conditions), it brackets the partial-recovery threshold; the paper's Corollary 2.2 specializes it to $nqs=o(1)$ in the regime $n^{-k}\le q=o(n^{-1/2})$.

On the formal side, the mission produces a finite, self-contained model of correlated random graphs with a planted permutation, a generalized Fano inequality for finite hypothesis classes with an arbitrary distance, and the bound of mutual information by a product divergence. The Fano inequality and the mutual-information bounds are reusable for other information-theoretic lower bounds (community detection, planted matching, testing). The paper proves the results on paper; none of them is formalized, and no Fano inequality is proved on the platform.

Difficulty

The Fano inequality (Theorem 3.1) is cited from Lemma 20 of Banerjee–Hegde–Massoulié (2012) and not proved in the paper, and the entropy calculus it rests on is not in Mathlib in a finite, real-valued form. The counting step (Proposition 3.3) concerns rencontres numbers; the paper uses the asymptotic $D_{n,k}\sim e^{-1}n!/k!$, which is valid only for fixed $k$, while the statement needs control uniform in $k$. Bounding $I(\pi^*;(A,B))$ requires relating the conditional law of the observation, a relabelled product law, to the unlabelled reference law $\mathcal Q$ on a space of $4^{n^2}$ matrix pairs, most of which have probability zero.

A natural first idea for the goal, taking $\alpha$ arbitrary as printed, fails: if $\alpha_n=1/n$, the identity algorithm succeeds whenever $\pi^*$ has a fixed point, with probability tending to $1-e^{-1}$, even when the divergence condition holds. The argument needs $\log(M/M_\alpha)$ to grow like $n\alpha_n\log n$, which needs $\alpha_n$ bounded below.

Formalization scope

Vertices are Fin n; a vertex pair is an off-diagonal element of Sym2 (Fin n); an edge state is a Bool × Bool with first coordinate $A$, second $B'$. The probability of a configuration is the product of $P$ over pairs, and $B$ is computed through $\pi^{*-1}$. Every probability is a finite sum; logarithms are natural. Standing assumptions on the parameters are $0\le q<s\le1$ (pp. 5 and 7); the remark "we assume $s<1$" of p. 6 is not used and not imposed.

Algorithms are real stochastic kernels from the observed pair $(A,B)$ to permutations, so randomized algorithms are included and deterministic ones are the 0/1 kernels. The algorithm's argument is the observation only: it does not see $\pi^*$ or $G_{B'}$. Mutual information and Kullback–Leibler divergence are defined as finite sums (Lean's $0\cdot\log 0=0$).

Hypotheses added relative to the page, each disclosed in the item's note:

• Theorem 2.1: $\alpha_n\ge c>0$ for large $n$ (the printed statement is false for $\alpha_n\to0$ fast).
• Theorem 3.1 and Corollary 3.2: $M_d<M$ (resp. $M_\alpha<n!$), without which $\log(M/M_d)=0$ and the bound is meaningless.
• Theorem 3.1: the observation space is finite; no metric axioms on $d$ are assumed.

Proposition 3.3 reads $(n\alpha)!$ as $\lceil n\alpha\rceil!$.

Trivializing formalizations are ruled out: the algorithm cannot be given $\pi^*$ (an oracle wins) or nothing (the statement becomes empty); the little-$o$ hypothesis is a limit of a ratio, not an inequality; the configuration law is built from (3) and sums to 1, not chosen by the solver.

Infrastructure a complete development needs: finite entropy and mutual information with the chain rule and data processing; Gibbs' inequality; derangement and rencontres counts (numDerangements in Mathlib); Stirling-type lower bounds on $\log k!$. Contributions are welcome on each milestone independently; the Fano inequality is the piece with the widest reuse.

The source is the arXiv preprint v5 (13 Jan 2022); its numbering is used throughout.

Selected references

• G. Hall, L. Massoulié, Partial Recovery in the Graph Alignment Problem, arXiv:2007.00533v5, 2022; Operations Research, 2023. https://arxiv.org/abs/2007.00533
• P. Pedarsani, M. Grossglauser, On the privacy of anonymized networks, KDD 2011. https://doi.org/10.1145/2020408.2020596
• D. Cullina, N. Kiyavash, Improved achievability and converse bounds for Erdős–Rényi graph matching, SIGMETRICS 2016. https://arxiv.org/abs/1602.01042
• D. Cullina, N. Kiyavash, P. Mittal, H. V. Poor, Partial recovery of Erdős–Rényi graph alignment via k-core alignment, arXiv:1809.03553, 2018. https://arxiv.org/abs/1809.03553
• S. Banerjee, N. Hegde, L. Massoulié, The price of privacy in untrusted recommendation engines, Allerton 2012, pp. 920–927 (Lemma 20: the generalized Fano inequality); cited as [3] in the paper.
• A. Narayanan, V. Shmatikov, De-anonymizing social networks, IEEE S&P 2009. https://doi.org/10.1109/SP.2009.22
• T. M. Cover, J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006. https://doi.org/10.1002/047174882X

Motivation

Ranking and selection asks which of $M$ simulated alternatives has the largest mean, when each simulation run returns one noisy sample and the simulation budget is limited. A large literature allocates the budget using the large-deviations analysis of Glynn and Juneja (2004): for a static allocation in which alternative $x$ receives a fixed fraction $\alpha_x$ of the samples, the probability of incorrect selection decays exponentially, and the allocation that maximizes the decay rate is characterized by a system of nonlinear optimality conditions. Those conditions depend on the unknown means, so practical procedures plug in estimates and solve the system repeatedly, which is costly and comes with few guarantees.

Chen and Ryzhov (Proc. 2019 Winter Simulation Conference) propose Balancing Optimal Large Deviations (BOLD), a sequential rule that never solves the optimality conditions: at each step it evaluates the two sides of one condition at plug-in estimates and samples whichever alternative appears to be falling behind. It has no tuning parameters and applies to any sampling distribution whose rate function can be evaluated. The paper states that BOLD learns the optimality conditions with probability 1; the full proofs are in the companion article (Chen and Ryzhov, Management Science, 2023).

Setting

There are $M > 2$ alternatives with distinct means $\mu_1,\dots,\mu_M$; the best is $x^* = \arg\max_x \mu_x$. Alternative $x$ produces independent samples from a law $F_x$ with mean $\mu_x$, a member of a distributional family $\{F_x(\theta)\}$ indexed by its mean $\theta$. The families may differ between alternatives.

The rate function of the member with mean $\theta$ is the Fenchel–Legendre transform of its log-moment generating function,

$$I_x(u;\theta) = \sup_{\gamma}\big(\gamma u - \log \mathbb E\,e^{\gamma W}\big),\qquad W \sim F_x(\theta),$$

with values in $[0,\infty]$, and $D_x(u;\theta) = \partial I_x(u;\theta)/\partial u$. For a normal law with variance $\lambda_x^2$, $I_x(u;\theta) = (u-\theta)^2/(2\lambda_x^2)$.

An allocation chooses alternative $x^n$ at stage $n = 0,1,\dots$. Write $N^n_x$ for the number of samples of $x$ among stages $0,\dots,n-1$ and $\theta^n_x$ for their mean (an arbitrary $\theta^0_x$ while $N^n_x = 0$). The plug-in rate is $I^n_x(\cdot) = I_x(\cdot;\theta^n_x)$, likewise $D^n_x$. For $x \ne y$, $u^n_{x,y}$ is the solution of

$$N^n_x D^n_x(u) + N^n_y D^n_y(u) = 0 \qquad (10)$$

and $\Gamma^n_{x,y} = N^n_x I^n_x(u^n_{x,y}) + N^n_y I^n_y(u^n_{x,y})$ (11).

BOLD (Figure 1 of the paper): let $x^{*,n}$ be the leader, an alternative with the largest $\theta^n_x$. If the leader is not unique, sample the tied leader with the fewest samples. Otherwise sample the leader if

$$\sum_{x\ne x^{*,n}} \frac{I^n_{x^{*,n}}(u^n_{x^{*,n},x})}{I^n_x(u^n_{x^{*,n},x})} > 1, \qquad (12)$$

and if not, sample the $x \ne x^{*,n}$ minimizing $\Gamma^n_{x^{*,n},x}$ (13). Remaining ties are broken arbitrarily.

Formalization targets

Goal: BOLD learns the optimality conditions

Under Assumptions 1–4 of the paper, with probability 1,

$$\lim_{n\to\infty}\sum_{x\ne x^*}\frac{I^n_{x^*}(u^n_{x^*,x})}{I^n_x(u^n_{x^*,x})} = 1 \quad\text{and}\quad \lim_{n\to\infty}\frac{\Gamma^n_{x^*,y}}{\Gamma^n_{x^*,z}} = 1 \ \text{ for all } y,z\ne x^*.$$

These are the plug-in forms of the total balance condition (5) and the individual balance conditions (6), which together characterize the optimal static allocation. The paper states them as Theorems 3 and 4; the goal is their conjunction.

Milestones

1. Theorem 1 (consistency). Under Assumptions 1–3, $N^n_x \to \infty$ for every $x$, almost surely.
2. Theorem 2. Under Assumptions 1–3, $\limsup_n N^n_x/N^n_y < \infty$ for all $x, y$, almost surely.
3. Theorem 3. The total balance limit above.
4. Theorem 4. The individual balance limit above.

Significance

The result. Convergence of BOLD to the optimality conditions shows that the static optimum of Glynn and Juneja can be learned by a cheap sequential rule without knowing the proportion of the budget the best alternative should receive. Top-two methods require that proportion as an input. The paper claims the guarantee for any sampling distributions satisfying four regularity assumptions, not only normal ones. As the paper notes, convergence to the static optimum does not by itself transfer the static exponential rate to the adaptive procedure; the result concerns learning the conditions.

The formalization. The WSC paper gives proof outlines only, and the complete argument lives in a long journal article. No part of it has been machine-checked. A formal proof would check a strong-law argument for an adaptive procedure with two interleaved decision criteria and would yield a reusable formal model of sequential sampling for ranking and selection with general rate functions.

Difficulty

The obvious argument is "sample means converge, hence the plug-in conditions converge". It fails because the sample means converge only if every alternative is sampled infinitely often, and BOLD gives no forced exploration: an alternative is sampled only when (12) or (13) selects it. Consistency must therefore come from the structure of the rule itself. Even with consistency, the limits in Theorems 3–4 are not continuity statements: the plug-in quantities depend on the sample sizes as well as the sample means, and they oscillate around the level 1 as (12) alternately holds and fails, so convergence requires quantitative control of how long the rule can neglect any one alternative. Discrete sampling laws add ties among sample means and a sample mean that can coincide with another alternative's true mean (Assumption 3).

Formalization scope

• Model. Alternatives are Fin M with 2 < M (indexed from 0). The family is Fam : Fin M → ℝ → Measure ℝ of probability measures, with true law Fam x (μ x). Samples form an observation array W x k (the $(k+1)$-th sample of $x$), mutually independent, with W x k ∼ Fam x (μ x); this gives the same law of the sample path as the paper's sequential sampling.
• Rate function. $I_x(u;\theta)$ is the extended-real Legendre transform of the extended-real log-MGF, from the published BellWilliams2001.ThresholdPolicy.LargeDeviation, so $+\infty$ is a genuine value. $D_x$ is the derivative of its real part. Conditions on $D_x$ are imposed on the effective domain $\mathcal D_x$, where $I_x$ is finite nearby.
• Parameter space. For each $x$ there is an open interval $\Theta_x \supseteq H_x$ that contains the samples almost surely, on which $F_x(\theta)$ has mean $\theta$ and $I_x(\cdot;\theta)$ is finite between any two parameters. The initial means lie in $\Theta_x$. These conditions are not printed, but without them the plug-in rule can starve an alternative forever: a law with $I_x(\cdot;\theta) = +\infty$ off one point gives $\Gamma = +\infty$. Bernoulli laws, whose sample means reach $0$ or $1$, fall outside this convention, although the paper says they are covered.
• Assumptions. The interval $H$ of Assumptions 1–2 is one fixed interval $H_x = [a_x,b_x]$ per alternative with $\mu_x$ in its interior. Assumption 3 is written without division. Assumption 4 is joint $C^1$ on $\mathcal D_x$.
• Algorithm. BOLD is a predicate IsBOLD on allocation sequences, so every tie-breaking rule is covered. The initial means $\theta^0$ are arbitrary. The solution of (10) is a chosen solution between the two sample means; its uniqueness is the paper's claim, not a hypothesis.
• Conventions. Ratios and $\Gamma$ are in $[0,\infty]$, with $a/0 = \infty$ for $a > 0$, so a never-sampled leader triggers (12) as in the paper. Theorem 2's limsup is taken in $[0,\infty]$. Every theorem is an almost-sure statement, with "probability 1" taken from §4.
• Ruled out. The theorems are not vacuous: a BOLD run exists on every realization (a local check proves this). The rate function is the Legendre transform of the actual family, not an unconstrained function. The family is not fixed to the normal or any single parametric case.

The development needs strong laws of large numbers along adaptively chosen sample counts, properties of Legendre transforms of log-moment generating functions (convexity, a unique zero at the mean), and law-of-the-iterated-logarithm-type rates for sample means. Lemmas on Legendre transforms of log-MGFs and the observation-array model are reusable for other large-deviations allocation rules. Contributions toward any milestone are welcome. Statements specialized to normal families are not substitutes for the general milestones.

Selected references

• Y. Chen and I. O. Ryzhov, Balancing Optimal Large Deviations in Ranking and Selection, Proc. 2019 Winter Simulation Conference, pp. 3368–3379, IEEE.
• Y. Chen and I. O. Ryzhov, Balancing Optimal Large Deviations in Sequential Selection, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4527
• P. Glynn and S. Juneja, A Large Deviations Perspective on Ordinal Optimization, Proc. 2004 Winter Simulation Conference, pp. 577–585, IEEE.
• A. Dembo and O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 2009. https://doi.org/10.1007/978-3-642-03311-7

Motivation

Model-based reinforcement learning algorithms for Markov decision processes estimate each transition distribution $P_{s,a}$ from the transitions they have observed out of the state–action pair $(s,a)$. Their regret analyses then need to know how far the empirical distribution $\hat p$ can be from the true one $p$. The standard tool is an $\ell_1$ bound on $\hat p-p$, as in UCRL2 (Jaksch, Ortner and Auer, 2010), which costs a factor of order $\sqrt S$ in the number of states $S$. What the analysis actually uses, however, is the deviation along one direction: the projection $(\hat p-p)^Th$ onto a bias (or value) vector $h$ whose entries differ by at most the MDP's diameter $D$.

S. Agrawal and R. Jia (arXiv:1705.07041v3, published in Mathematics of Operations Research, 2023, as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds) prove a worst-case regret bound of order $\tilde O(D\sqrt{SAT})$ for an optimistic variant of posterior sampling. One ingredient of that analysis is their Proposition 5.2: a Bernstein-type bound on $(\hat p-p)^Th$ whose leading term is governed by a variance of $h$ under $p$, written in stick-breaking form. This mission formalizes that proposition and the steps of its proof.

Setting

Fix a number of states $S$ and order them $1,\dots,S$. A probability vector $p\in\Delta^S$ has $p_i\ge0$ and $\sum_ip_i=1$. A multinoulli trial with parameter $p$ is a random state $X$ with $\mathbb P(X=i)=p_i$. Draw $n$ independent trials $X_1,\dots,X_n$ and let

$$\hat p_i=\frac{\#\{t: X_t=i\}}{n}$$

be the empirical probability vector, the average of the one-hot outcomes. For $p$ and a vector $h\in\mathbb R^S$ define the stick-breaking quantities

$$\gamma_i=\frac{p_i(p_{i+1}+\cdots+p_S)}{p_i+\cdots+p_S},\qquad H_{i+1}=\frac{1}{\sum_{j=i+1}^Sp_j}\sum_{j=i+1}^Sh_jp_j,\qquad c_i=h_i-H_{i+1}.$$

Thus $H_{i+1}$ is the mean of $h$ under $p$ conditioned on the states after $i$, and $c_i$ compares $h_i$ with it. The sum $\sum_{i<S}\gamma_ic_i^2$ equals the variance of $h(X)$ for $X\sim p$. In Lean these objects are gammaCoef p i, Hnext p h i, cCoef p h i, phat ω i, the law of one trial is cat p and the law of $n$ trials is trialsLaw n p, all in the namespace OptimisticPSRL.Concentration.

Formalization targets

Goal: Proposition 5.2 (p. 9)

Let $h\in\mathbb R^S$ satisfy $|h_i-h_{i'}|\le D$ for all $i,i'$, let $n\ge96$ and $\rho\in(0,1)$. Then, with probability at least $1-\rho$,

$$\big|(\hat p-p)^Th\big|\le2\sqrt{\log(n/\rho)\sum_{i<S}\frac{\gamma_ic_i^2}{n}}+3D\,\frac{\log(2/\rho)}{n}.$$

Milestones

1. Fact 1 (p. 17), a deterministic identity: for probability vectors $\tilde p,\bar p$ with stick-breaking ratios $\tilde y_i=\tilde p_i/(\tilde p_i+\cdots+\tilde p_S)$ and $\bar y_i$,

$$(\tilde p-\bar p)^Th=\sum_i(\tilde y_i-\bar y_i)(h_i-\tilde H_{i+1})(\bar p_i+\cdots+\bar p_S)=\sum_i(\tilde y_i-\bar y_i)(h_i-\bar H_{i+1})(\tilde p_i+\cdots+\tilde p_S).$$

2. The projection as a sum of martingale differences (proof, p. 21): with $Z_{t,i}=c_i\mathbb 1(X_t=i)-c_i\frac{p_i}{p_i+\cdots+p_S}\mathbb 1(X_t\ge i)$ and $Z_t=\sum_iZ_{t,i}$,

$$\frac1n\sum_{t=1}^nZ_t=(\hat p-p)^Th,$$

together with the two intermediate expressions of the page. 3. Uncorrelated coordinates (proof, p. 21): $\mathbb E[Z_{t,i}Z_{t,j}]=0$ for $i\ne j$. 4. The predictable variance (proof, p. 21): $\sum_{t=1}^n\mathbb E[Z_t^2]=\sum_ic_i^2\,n\,\gamma_i$. 5. Corollary B.1 (p. 26), Bernstein's inequality for bounded martingale differences with random predictable variance $V_n$: for $n\ge96$, $\delta\in(0,1)$, with probability greater than $1-\delta$,

$$|M_n|\le2\sqrt{V_n\ln(n/\delta)}+3K\ln(n/\delta).$$

Significance

The result. Proposition 5.2 is the concentration half of the optimism step of the paper (Lemma 5.3): combined with an anti-concentration bound for Dirichlet samples along the same direction (Proposition 5.1), it shows that some posterior sample is optimistic along $h$ with constant probability. Because the bound is stated along a single direction and is weighted by the variance of $h$ rather than by $D$ alone, it avoids the $\sqrt S$ loss that an $\ell_1$ bound would incur, which is part of how the paper's regret bound improves on UCRL2's $\tilde O(DS\sqrt{AT})$. The stick-breaking form of the variance is what lets the same quantity appear on both sides of the optimism argument, in the Dirichlet bound and in the empirical bound.

Formalizing it. The proposition and its proof steps are proved on paper; none of them has a machine-checked proof. The regret theorem of the paper (Theorem 1) is not posed: its constants are hidden in $O(\cdot)$ and its algorithm's parameters are given as $\Theta(\cdot)$. Proposition 5.2, by contrast, is fully explicit. Corollary B.1 is a reusable martingale inequality with explicit constants. The predictable-variance identity and Fact 1 are exact identities about stick-breaking coordinates that recur in analyses of Dirichlet and categorical models.

Difficulty

Two steps resist the obvious approach. First, the statement carries the variance in stick-breaking form, not as $\mathrm{Var}_p(h)$; linking the two needs the decomposition of Fact 1 and the identity for the predictable variance, which are exact algebraic identities whose bookkeeping of tails and empty tails is error-prone. Second, the paper's own route goes through Corollary B.1, a martingale Bernstein inequality with a random variance, which rests on a peeling argument over a grid of variance levels (Seldin et al., 2012); Mathlib has neither this inequality nor a Bernstein inequality with explicit constants for bounded variables.

A known subtlety: the paper's proof, through Corollary B.1, yields the second term $3D\log(n/\rho)/n$, while the statement prints the smaller $3D\log(2/\rho)/n$. The printed statement is still true for $n$ iid trials (the classical Bernstein inequality gives a bound below it), so the goal is posed as printed. The paper's own proof therefore does not establish the printed constant.

Formalization scope

• States are Fin S with its natural order, 0-based; the paper's range $i<S$ is every state but the last (belowLast S). Fact 1 holds for every ordering; the natural order covers this since states are labels.
• Probability vectors are p : Fin S → ℝ with IsProbVec p (nonnegative, summing to one). Zero entries are allowed. A ratio whose denominator is zero evaluates to $0$ (Lean's convention), which gives the values the identities need; no positivity of $p$ is assumed.
• One trial has law cat p $=\sum_ip_i\delta_i$; $n$ trials have the product law trialsLaw n p $=$ Measure.pi. The empirical vector phat ω is computed from the sample ω : Fin n → Fin S. "With probability $1-\rho$" is ENNReal.ofReal (1 - ρ) ≤ trialsLaw n p {good event}; Corollary B.1's "greater than $1-\delta$" is strict. $\log$ is Real.log.
• The proof displays (milestones 2–4) are stated in the iid reading of the proposition: the paper writes them for transitions of an MDP out of a fixed $(s,a)$, with an indicator $\mathbb 1(s_{t-1}=s,a_{t-1}=a)$ and a random count $\tau$; here the indicator is one and $\tau=n$, and the conditional expectations are expectations under one draw of law $p$. Milestone 2 assumes every drawn state has positive probability (true almost surely), which the page's intermediate sum over $i\le S-1$ needs.
• Corollary B.1 is posed for a general filtered probability space, with $Z_i$ $\mathcal F_i$-measurable, $|Z_i|\le K$ almost surely and $\mathbb E[Z_i\mid\mathcal F_{i-1}]=0$.

The goal cannot be satisfied by a degenerate reading: $\hat p$ is built from the sample, the measure is the $n$-fold product of the categorical law $p$, the event is the good event itself (not a complement bound), and the variance term is not identically zero (for $S=2$, $p=(\tfrac12,\tfrac12)$ it equals $(h_1-h_2)^2/4$).

Needed infrastructure: finite-sum manipulations over tails of Fin S; a Bernstein or Freedman inequality with explicit constants (for iid bounded variables for the goal, for martingale differences for Corollary B.1). Contributions of either inequality are reusable well beyond this mission and are welcome, as are alternative proofs of the goal that bypass Corollary B.1.

Selected references

• S. Agrawal and R. Jia, Posterior sampling for reinforcement learning: worst-case regret bounds, arXiv:1705.07041v3, 2020; published as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1705.07041
• T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/jaksch10a.html
• Y. Seldin, F. Laviolette, N. Cesa-Bianchi, J. Shawe-Taylor and P. Auer, PAC-Bayesian inequalities for martingales, IEEE Transactions on Information Theory 58(12), 2012. https://doi.org/10.1109/TIT.2012.2211334

Detecting a change in a partially observed network

Many networks are recorded as a sequence of snapshots: contact networks in epidemiology, communication graphs, brain connectivity measured over time, trade or transport links. A basic statistical question is whether the law generating the snapshots changed at some point. Two features make the question hard in practice. The networks are often sparse, so each snapshot carries little information. And links are missing: a pair of vertices is observed only with some probability, so an absent edge may mean "no link" or "not sampled".

Enikeeva and Klopp (arXiv:2106.14470, Operations Research, 2025) give minimax bounds for this testing problem. They treat both a known change time (Theorems 1 and 2) and an unknown change time (Theorem 3). This mission formalizes the unknown-time case, where the test scans a dyadic grid of candidate times. Two companion missions formalize the known-time upper bound (Theorem 1) and the lower bound (Theorem 2).

Setting

There are $n$ vertices and $T$ time points. At time $t$ the statistician observes a symmetric matrix $Y^t\in\{0,1\}^{n\times n}$ with zero diagonal, $Y^t_{ij}=\Omega^t_{ij}A^t_{ij}$. Here $A^t$ is the adjacency matrix of the network and $\Omega^t$ records which pairs were sampled. The entries $Y^t_{ij}$, $i<j$, are independent over pairs and times, and

$$Y^t_{ij}\sim\mathrm{Bernoulli}\big((\Pi\odot\Theta^t)_{ij}\big),$$

where $\Theta^t\in[0,1]^{n\times n}$ is the connection-probability matrix (symmetric, zero diagonal), $\Pi$ is the sampling matrix (symmetric, entries in $(0,1]$, unit diagonal), and $\odot$ is the entrywise product.

The sparsity level $\omega_n$ bounds the expected observed degree: $(\Theta,\Pi)\in\mathcal S_n(\omega_n)$ when $\|\Pi\odot\Theta\|_{1,\infty}=\max_j\sum_i|(\Pi\odot\Theta)_{ij}|\le\omega_n$.

Under the null hypothesis $\Theta^t=\Theta^0$ for all $t$. Under the alternative there is $\tau\in\mathcal D_T=\{1,\dots,T-1\}$ with $\Theta^t=\Theta^0$ for $t\le\tau$ and $\Theta^t=\Theta^0+\Delta\Theta^\tau$ for $t>\tau$. Both parameter pairs lie in $\mathcal S_n(\omega_n)$, and the jump has energy at least $R$:

$$q(\tau/T)\,\|\Pi\odot\Delta\Theta^\tau\|_{2\to2}\ge R,\qquad q(x)=\sqrt{x(1-x)},$$

where $\|\cdot\|_{2\to2}$ is the spectral norm. A test $\psi$ maps the data to $\{0,1\}$. Its type I error $\alpha(\psi)$ is the largest rejection probability over the null class. Its type II error $\beta(\psi,R)$ is the largest acceptance probability over all $\tau\in\mathcal D_T$ and all alternatives of energy at least $R$.

The Matrix CUSUM at time $t$ contrasts the averages before and after $t$:

$$Z_T(t)=\sqrt{\frac{t(T-t)}{T}}\Big(\frac1t\sum_{s=1}^tY^s-\frac1{T-t}\sum_{s=t+1}^TY^s\Big),\qquad1\le t\le T-1.$$

The dyadic grid is $\mathcal T=\{2^k\}\cup\{T-2^k\}$, $0\le k\le\lfloor\log_2(T/2)\rfloor$. Fix $\epsilon\in(0,1/2]$. The test (14) of the paper rejects when

$$\max_{t\in\mathcal T}\|Z_T(t)\|_{2\to2}>H_{\alpha,n,T}=2\sqrt2(1+\epsilon)\sqrt{\omega_n}+C_\epsilon\log\frac{4n\log_2(T)}{\alpha}.$$

Formalization targets

Goal: Theorem 3

For every $\epsilon\in(0,1/2]$ there are constants $C_\epsilon>0$ and $C$, depending only on $\epsilon$, such that for all $n\ge1$, $T\ge2$, $\omega_n\ge0$ and $\alpha,\beta\in(0,1)$: if

$$R\ \ge\ 4(1+\epsilon)\Big(\frac{6\omega_n}{T}\Big)^{1/2}+\frac{C}{\sqrt T}\log\Big(\frac{4n\log_2(T)}{\alpha\wedge\beta}\Big),$$

then the grid test with threshold $H_{\alpha,n,T}$ has $\alpha(\psi_{n,T})\le\alpha$ and $\beta(\psi_{n,T},R)\le\beta$.

Milestones

• the signal-plus-noise decomposition $Z_T(t)=-\mu^\tau_T(t)\,\Pi\odot\Delta\Theta^\tau+\xi(t)$ and the maximum $\mu^\tau_T(\tau)=\sqrt T\,q(\tau/T)$, display (7);
• the grid facts $\mathcal T\subseteq\mathcal D_T$ and $|\mathcal T|\le2\log_2T$;
• the grid captures signal: for every $\tau\in\mathcal D_T$ some $t\in\mathcal T$ has $\mu^\tau_T(t)\ge\sqrt T\,q(\tau/T)/\sqrt3$;
• Proposition 11, the Bandeira–van Handel bound for symmetric random matrices with independent bounded entries;
• Lemma 12, the noise bound for the CUSUM at a fixed time;
• Lemma 5 (level) and Lemma 6 (power above $4\sqrt6(1+\epsilon)(\omega_n/T)^{1/2}+\frac{\sqrt3C_\epsilon}{\sqrt T}(\log\frac{4n\log_2T}\alpha+\log\frac{2n}\beta)$).

Significance

Theorem 3 shows that not knowing the change time costs at most a constant factor and a $\log\log T$ term in the detection energy. Together with the lower bound of Theorem 2, which is of order $(\omega_n/T)^{1/2}$, this makes the grid test rate-optimal when $\omega_n$ grows at least polylogarithmically in $n$ (Remark 3 of the paper). The statistic depends on the data only through spectral norms of $O(\log T)$ CUSUM matrices, so it is cheap to compute. The threshold needs only the degree bound $\omega_n$, which can be estimated from the observed degrees.

The paper's proof is complete on paper apart from one step noted below. No part of it is machine-checked. Formalizing it produces a checked finite model of Bernoulli network data with missing links, a reusable Matrix CUSUM, and a precise statement of a Bandeira–van Handel type bound for symmetric matrices with independent bounded entries. That bound is a standard tool in random-matrix statistics and is not yet available in Mathlib or on the platform.

Difficulty

The level of the test is a union bound over the grid combined with a high-probability bound on $\|\xi(t)\|_{2\to2}$ at a fixed time. The hard part is that bound, Lemma 12. A matrix Bernstein inequality gives a leading term $\sigma\sqrt{\log(n/\delta)}$, which is too large. The statement needs the sharp form $2\sqrt2(1+\epsilon)\sigma+C_\epsilon\log(2n/\delta)$, where the variance proxy $\sigma$ enters without a logarithmic factor. Proposition 11 supplies this only for matrices whose entries are bounded by $\sigma_*$. The entries of $\xi(t)$ are sums over time and are only bounded by about $\sqrt{\log(n/\delta)}$ with high probability. The paper applies Proposition 11 "given the event" $\{\|\xi(t)\|_\infty\le\sigma_*\}$, but conditioning on that event destroys centring and independence, so a truncation argument is missing there.

The power analysis is elementary once Lemma 12 is available. Its one subtlety is that the change time ranges over all of $\mathcal D_T$, while the test inspects only the grid.

Formalization scope

• Data and probability. Only $Y$ is modelled; the latent $A^t,\Omega^t$ are integrated out. An observation is a Boolean function of a 0-based time index and of a pair $i<j$. Probabilities are finite sums of products of Bernoulli weights, so every test is measurable and no measure theory enters the model. Proposition 11 is the only measure-theoretic statement.
• Classes. The sampling class carries the paper's standing assumptions $\Pi_{ii}=1$, $\Pi_{ij}>0$. The errors are real suprema of sets of probabilities; an empty alternative has type II error $0$.
• Spectral norm. $\|\cdot\|_{2\to2}$ is the published HighDimProb.RandomMatrices.matrixOpNorm.
• Grid and test. $\lfloor\log_2(T/2)\rfloor$ is Nat.log 2 (T / 2). "$\max_{t\in\mathcal T}\|Z_T(t)\|>H$" is "$\exists t\in\mathcal T$, $\|Z_T(t)\|>H$". The threshold uses the real $\log_2T$.
• Constants. $C_\epsilon$ and $C$ are quantified existentially before $n,T,\omega_n,\alpha,\beta,R$. A version with the constants chosen after $n$ or $T$ would be trivial, because huge constants silence the test or empty the alternative. The goal does not assume Lemma 12's conclusion. Lemmas 5 and 6 take it as a hypothesis, and Lemma 12 states that it is satisfiable. The test ranges over all functions of the data, and the alternative over all $\tau\in\mathcal D_T$.
• Disclosed additions and corrections. The theorems assume $n\ge1$, $T\ge2$ and $\omega_n\ge0$, which the paper leaves implicit. Proposition 11 assumes $m\ge1$ and $c_\epsilon>0$. Independence in Proposition 11 and Lemma 12 refers to the entries with $i\le j$ ($i<j$) of a symmetric matrix. The grid statement is the inequality $|\mathcal T|\le2\log_2T$: the printed equality $|\mathcal T|=2+2\lfloor\log_2(T/2)\rfloor$ fails when the two halves overlap, as at $T=4$. Lemma 5 is stated with "$\le\alpha$", as its proof concludes, rather than the printed "less than $\alpha$". The grid-signal milestone is stated as an existence claim, because the printed choice $\tau/2\le t^*<\tau$ has no solution at $\tau=1$.

Welcome contributions: a proof of Proposition 11, or of any sharp spectral-norm bound that implies it; a rigorous proof of Lemma 12, repairing the conditioning step; and the elementary grid lemmas.

Selected references

• F. Enikeeva and O. Klopp, Change-point detection in dynamic networks with missing links, Operations Research, 2025; arXiv:2106.14470v2. https://arxiv.org/abs/2106.14470
• A. S. Bandeira and R. van Handel, Sharp nonasymptotic bounds on the norm of random matrices with independent entries, Annals of Probability 44(4), 2016. https://doi.org/10.1214/15-AOP1025
• H. Liu, C. Gao and R. J. Samworth, Minimax rates in sparse, high-dimensional change point detection, Annals of Statistics 49(2), 2021. https://doi.org/10.1214/20-AOS1994

Motivation

Online platforms run randomized experiments on subjects (users, sessions, orders) that arrive one at a time and must be assigned to a control or a treatment group on arrival, before later subjects are seen. The precision of a treatment-effect estimate depends on how similar the two groups are in their observed covariates. When the groups are badly balanced, the estimator's variance grows, and a large literature on covariate balancing (blocking, rerandomization, matched pairs) addresses this for offline experiments, where all covariates are known in advance.

J. Zhao and Z. Zhou (arXiv:2201.12936, Management Science, 2025) cast the online problem as an online matching problem. The cost of an assignment is the discrepancy, the weight of a minimum-cost perfect matching between the two groups, and they compare three designs against an oblivious adversary that fixes the covariate sequence in advance:

• the clairvoyant matched-pair design;
• the completely randomized design;
• their online pigeonhole design.

For one continuous covariate the pigeonhole design attains $O(T^{1/4}(\log T)^{1/2})$ against $\Theta(T^{1/2})$ for complete randomization. This mission concerns the multi-dimensional result, Theorem 9.

Setting

$T$ subjects arrive in order; $T$ is even. Subject $t$ carries a covariate vector $x_t$ with $q$ discrete coordinates, the $i$-th in a finite set $S_i\subseteq[0,1]$ of size $m_i$, and $p\ge2$ continuous coordinates in $[0,1]$. Distances are Euclidean in $\mathbb R^{q+p}$. An assignment puts each subject in control ($A$) or treatment ($B$).

The discrepancy of a split with $|A|=|B|$ is

$$d_{A,B}=\min_{\sigma:A\to B\text{ bijective}}\ \sum_{t\in A}\lVert x_t-x_{\sigma(t)}\rVert_2 ,$$

the value of the assignment problem (1) of the paper.

The completely randomized design picks $A$ uniformly among the $\binom{T}{T/2}$ subsets of size $T/2$; $\mathrm{ALG}^C(x)$ is the mean of $d_{A,B}$.

A pigeonhole design fixes a partition of the covariate space into pigeonholes. When subject $t$ arrives:

1. if one group already has $T/2$ subjects, $t$ joins the other group;
2. otherwise $t$ joins the group that has fewer subjects in its own pigeonhole, and on a tie a fair coin decides.

Theorem 9 uses the pigeonholes

$$\mathcal P(\mathcal S)=S_1\times\cdots\times S_q\times\Big\{[0,c^{1/p}T^{-\varphi}),\ \dots,\ [1-c^{1/p}T^{-\varphi},1]\Big\}^p ,$$

uniform cells of edge $c^{1/p}T^{-\varphi}$ on each continuous axis, for parameters $\varphi\in(0,1)$ and $c>1$. The expected discrepancy is the mean of $d_{A,B}$ over the design's coins.

Formalization targets

Goal: Theorem 9 (p. 26)

There are $C>0$ and $T_0$, depending only on $p,q,S_1,\dots,S_q,\varphi,c$, such that for every even $T\ge T_0$ and every admissible arrival sequence,

$$\mathbb E[d_{A,B}]\le C\Big(T^{1-\varphi}+T^{(p-1)\varphi}\,\lambda_p(T)\Big),\qquad \lambda_2(T)=(\log T)^{3/2},\quad \lambda_p(T)=1\ (p\ge3).$$

Milestones

1. Lemma EC.1: Hoeffding for a binomial, $\Pr(|H(n)-pn|\le\sqrt{n\log n})\ge1-2/n^2$.
2. Lemma 5, $p=2$: if $T=m^2$ and the subjects occupy each cell of the $m\times m$ grid exactly once, then $\mathrm{ALG}^C(x)=O(T^{1/2}\log T)$.
3. Lemma 5, $p\ge3$: on the full grid of $T=m^p$ cells, $\mathrm{ALG}^C(x)=O(T^{(p-1)/p})$.
4. Balance: every run of a pigeonhole design has $|A|=|B|=T/2$.
5. Component 1: the subjects paired within their pigeonhole before the stopping time $\tau$ contribute at most $\tfrac12c^{1/p}\sqrt p\,T^{1-\varphi}$, on every run.
6. Unmatched subjects: at most one unmatched subject per pigeonhole, $H^0_\tau+H^1_\tau$ at most the number of pigeonholes, and $|H^0_\tau-H^1_\tau|=T-\tau$.
7. Component 2: the remaining subjects contribute $O(T^{(p-1)\varphi}\lambda_p(T))$ in expectation.

Corollary 2 (the case $\varphi=1/p$) is an extra theorem after the goal.

Significance

At $\varphi=1/p$ Theorem 9 gives $O(T^{(p-1)/p})$ for $p\ge3$. This is the order $\Theta(T^{(p-1)/p})$ of the matched-pair design (Theorem 7), which sees all covariates in advance. An online design that commits to each assignment on arrival therefore loses at most a constant factor in dimension $p\ge3$, and at most a $(\log T)^{3/2}$ factor at $p=2$. For the completely randomized design no comparable upper bound is known for general sequences (p. 21). Lemma 5 is the paper's bound for complete randomization on the special family of full grids, and is of independent interest as a random-labelling matching estimate.

The results are proved on paper; none of them has a machine-checked proof, and the platform holds no item on them. A formalization would close the gaps of the printed argument:

• Lemma 5's induction for $p=2$ ends at $\sqrt T(\log T)^{3/2}$ rather than the stated $\sqrt T\log T$.
• Component 2 applies Lemma 5 to unmatched subjects, which occupy distinct cells but do not fill the grid.
• The case $q\ge1$ is argued per discrete support, although the balancing rule acts across supports.

Every statement in the mission is believed true.

Difficulty

The matched part (Component 1) is deterministic: paired subjects share a pigeonhole of diameter $O(T^{-\varphi})$. The difficulty lies in the subjects left over: the unmatched ones and the subjects after $\tau$. Their labels come from coins, but which subjects end up unmatched, and when $\tau$ occurs, depend on the same coins. So the leftover set is not a fixed set with independent fair labels, and the conditional binomial law used on p. ec22 does not hold literally.

A second obstacle is the random-matching estimate itself. Bounding the expected optimal matching between randomly labelled points of a grid at the rates $T^{1/2}\log T$ ($p=2$) and $T^{(p-1)/p}$ ($p\ge3$) is a multi-scale problem of Ajtai–Komlós–Tusnády type. A single-scale count of imbalances per cell gives only $T^{1/2}$ times a power of $T$ that is too large.

Formalization scope

• Subjects are indexed $0,\dots,T-1$; an assignment is a map to Bool (false = control). The covariate space is EuclideanSpace ℝ (Fin q ⊕ Fin p). Admissible sequences have discrete coordinates in $S_i$ and continuous ones in $[0,1]$, with $S_i\subseteq[0,1]$ (the paper's normalisation).
• Discrepancy: an infimum over bijections between the groups. An unbalanced split has the junk value $0$. The designs, the matched set and its complement are balanced on every run, so the junk is never reached.
• Cells: the printed edge $c^{1/p}T^{-\varphi}$ gives a partition only when $c^{-1/p}T^{\varphi}$ is an integer. The formalization uses $m=\lceil c^{-1/p}T^{\varphi}\rceil$ cells per axis of edge $1/m\le c^{1/p}T^{-\varphi}$, with the last cell closed. A pigeonhole is keyed by the exact discrete values and the cell index on each axis. The partition is the printed one, not a quantified family.
• Randomness: the pigeonhole design uses one coin per subject, consulted only on a tie. Its expected discrepancy is the average over all $2^T$ coin vectors, which is exactly the paper's law. The completely randomized design averages over all $\binom{T}{T/2}$ control sets.
• Asymptotics: $O(f(T))$ means $\exists C>0,\exists T_0,\forall T\ge T_0$ even, $\forall x$ admissible. $C$ and $T_0$ are chosen before $T$ and $x$ and depend only on the fixed parameters. $\log$ is the natural logarithm.
• Lemma 5's family $\mathcal X$: $T=m^p$ subjects in $[0,1]^p$, one per cell, stated as injectivity of the cell map.
• Stopping objects: $\tau$ is the first $n$ at which a group holds $T/2$ subjects. Within a pigeonhole the subjects before $\tau$ are paired in arrival order, and the last one is unmatched when their number is odd.
• Corrections to the page: the second cell printed as $[T^{-\varphi},2c^{1/p}T^{-\varphi})$ on p. ec21 is read as $[c^{1/p}T^{-\varphi},2c^{1/p}T^{-\varphi})$. The family's $x'_t\notin\mathbb X$ is read as $x_{t'}\notin\mathbb X$. The bound $H\le\frac1cT^{p\varphi}$ becomes $H\le(\prod_i m_i)\,m^p$ under the ceiling and the discrete supports.

The following formalizations would trivialize the mission and are ruled out:

• a bound on the discrepancy of one run, or of the best run, instead of the average over all coin vectors;
• constants that depend on $T$ or $x$;
• an unbalanced design that exploits the junk value $0$;
• an arbitrary partition in place of the printed grid.

A complete development needs a binomial Hoeffding bound and an exact analysis of the design's recursion (balance, alternation within a pigeonhole before $\tau$). It also needs a multi-scale bound on random bichromatic matchings of grid points. That bound is reusable for Lemma 5 and for matching estimators generally. Contributions on any milestone are welcome, as are proofs of Lemma 5 for arbitrary subsets of grid points, which is what Component 2 needs.

Selected references

• J. Zhao and Z. Zhou, Pigeonhole Design: Balancing Sequential Experiments from an Online Matching Perspective, Management Science, 2025; arXiv:2201.12936v6, 2024. https://arxiv.org/abs/2201.12936
• M. Ajtai, J. Komlós and G. Tusnády, On optimal matchings, Combinatorica 4 (1984) 259–264. https://doi.org/10.1007/BF02579135
• N. Fournier and A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015) 707–738. https://doi.org/10.1007/s00440-014-0583-7
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

Motivation

A forecaster who issues a probability distribution for a multivariate quantity, such as the joint demand at several locations or the joint returns of several assets, is often judged not on the whole distribution but on a region it implies: the set of outcomes whose cumulative probability, or smoothed density, exceeds a threshold. Such level sets are the multivariate counterpart of quantiles, and they are used as risk regions and as summaries of joint distributions in management science (Abbas, Budescu and Gu 2010) and in density level set estimation (Cadre 2006). To compare competing level set forecasts against realized data, one needs a consistent scoring function: a loss $l(A, y)$ of a candidate set $A$ and an outcome $y$ whose expectation under the true distribution is smallest at the true level set. For univariate quantiles the answer is classical (the quantile or pinball loss, Gneiting 2011); for general multivariate level sets, the paper notes, scores had not been studied beyond density level sets and univariate quantiles.

Meng, Taylor, Ben Taieb and Li (Operations Research, 2025) obtain such scores by decomposing their $L^2$ scoring rule for multivariate distributions into an integral, over the threshold $\alpha$, of scores for the level sets of a smoothed density. This mission formalizes that construction: Theorem 2 of the paper.

Setting

Write $\mathbb R^d$ for $d$-dimensional space with Lebesgue measure $\mathcal L^d$ and the componentwise order ($z \ge y$ means $z_j \ge y_j$ for all $j$). The unknown distribution of the observation $Y$ is a probability measure $P_Y$ on $\mathbb R^d$; the paper writes $f_Y$ for its generalized density. Fix a kernel $w : \mathbb R^d \to \mathbb R$ and a nonnegative integrable weight $h$. The smoothed density is the convolution

$$(f_Y * w)(z) = \int_{\mathbb R^d} w(z - s)\, dP_Y(s).$$

For $w = u = \mathbb 1\{\cdot \ge 0\}$ (the Heaviside function) it is the multivariate CDF $F_Y(z) = P_Y\{s \le z\}$.

The $\alpha$ level set of a function $g$ is (display (9), p. 12)

$$L(g;\alpha) = \{ z \in \mathbb R^d : g(z) \ge \alpha \}.$$

A function $l(A, y)$ of a Borel set $A \subseteq \mathbb R^d$ and a realization $y$ is a consistent scoring function for $L(f_Y * w; \alpha)$ if $\mathbb E_{P_Y}[l(A, \bullet)]$ is minimized at $A = L(f_Y * w;\alpha)$, and strictly consistent if that set is the only minimizer (p. 12). The level set score is (display (11), p. 13)

$$(S')^\Gamma(A, y; w, h, \alpha) = \int_{\mathbb R^d} \bigl(\alpha - w(z - y)\bigr)\, \mathbb 1\{z \in A\}\, h(z)\, dz,$$

and the $L^2$ scoring rule of the paper is (display (3), p. 8)

$$S'(P_X, y; w, h) = \int_{\mathbb R^d} (f_X * w)^2(z)\, h(z)\, dz - 2 \int_{\mathbb R^d} (f_X * w)(z)\, w(z - y)\, h(z)\, dz.$$

In Lean these are smooth, levelSet, scoreΓ, S', cdf and heaviside in the definition item MultivarScores.LevelSet.Setting.

Formalization targets

The paper's Theorem 2 (p. 13) reads:

Let $\mathcal V^d$, $h$, and $w$ satisfy Assumption 1 in the appendix, and $w$ is nonnegative. Let $\alpha > 0$, and let $A \subseteq \mathbb R^d$ be an arbitrary Borel set. Suppose $(S')^\Gamma(A, \bullet; w, h, \alpha)$ is finite $\mathcal L^d$-a.e. and $(S')^\Gamma(A, \bullet; w, h, \alpha) f_Y(\bullet)$ is integrable. Then the following expression defines a consistent scoring function for the $\alpha$ level set $L(f_Y * w; \alpha)$: $(S')^\Gamma(A, y; w, h, \alpha) = \int_{\mathbb R^d} (\alpha - w(z - y))\, \mathbb 1\{z \in A\}\, h(z)\, dz$. (11) If $h$ is nonzero $\mathcal L^d$-a.e. and $L(f_Y * w; \alpha)$ equals the closure of $\{f_Y * w > \alpha\}$, it is strictly consistent. Moreover, with $A = L(f_X * w; \alpha)$, the integral of (11) with respect to $\alpha$ is precisely half of the $L^2$ score in (3), i.e., $\tfrac12 S'(P_X, y; w, h) = \int_0^\infty (S')^\Gamma(L(f_X * w; \alpha), y; w, h, \alpha)\, d\alpha$.

Goal: consistency

For every Borel $A$ and every $\alpha > 0$,

$$\mathbb E_{P_Y}\bigl[(S')^\Gamma(L(f_Y * w;\alpha), \bullet; w, h, \alpha)\bigr] \le \mathbb E_{P_Y}\bigl[(S')^\Gamma(A, \bullet; w, h, \alpha)\bigr].$$

This is the part of Theorem 2 that holds exactly as printed, and it is the goal.

Strict consistency (milestone)

If moreover $h \ne 0$ a.e., $\mathcal L^d\{f_Y * w = \alpha\} = 0$, and $\mathcal L^d(A \,\triangle\, L(f_Y * w;\alpha)) \ne 0$, the inequality is strict. The null-set condition replaces the printed closure condition (see Formalization scope).

Layer-cake decomposition (milestone)

$$\tfrac12 S'(P_X, y; w, h) = \int_0^\infty (S')^\Gamma\bigl(L(f_X * w;\alpha), y; w, h, \alpha\bigr)\, d\alpha.$$

The other milestones are the steps of the paper's proof (pp. 33–34): the per-realization difference $\Delta''$ (p. 33), the expected difference (19) (p. 34), and two companions: the CDF level set score (13) is consistent for $L(F_Y;\alpha)$ (p. 16), and in dimension one it equals the quantile score up to a term depending only on $y$ (Remark 2, p. 17).

Significance

Theorem 2 supplies consistent scoring functions for a whole family of multivariate level sets at once, one for each kernel $w$: CDF level sets (from $w = u$), density level sets (from $w = \delta_0$) and lower-partial-moment level sets. It thereby gives a way to rank and compare multivariate region forecasts, and in one dimension recovers the full class of quantile scores (Remark 2). The layer-cake identity explains the relation between a distribution score and its level set scores, generalizing the classical identity $\mathrm{CRPS} = 2\int_0^1(\text{quantile score})\,d\alpha$ (display (10)); the paper relates its CDF level set score to the Vorob'ev quantile scores of Fissler, Frongillo, Hlavinová and Rudloff (2021).

The result is proved in the paper's appendix (pp. 33–34). It has no machine-checked proof that this mission is aware of. Formalizing it fixes the exact integrability conditions under which the expectations exist (the paper states them loosely in Assumption 1), and it repairs the strict consistency clause, whose printed sufficient condition does not imply what the proof uses.

Difficulty

The core of consistency is a sign argument, but every quantity in it is an integral over $\mathbb R^d$ against $h$ or against $P_Y$, and none of them is a priori finite: $w$ need not be bounded or integrable, and $(S')^\Gamma(A, y)$ must be integrable in $y$ for the true level set as well as for the candidate $A$, although the paper assumes it only for $A$. Exchanging the $y$- and $z$-integrals therefore needs a product-integrability condition, not pointwise finiteness. The layer-cake milestone requires the layer cake formula for two different measures ($h\,dz$ and $w(z-y)h(z)\,dz$), with powers $2$ and $1$, followed by an exchange that keeps the sign of the second term; a nonnegative (lower) integral cannot express the difference. The strict clause needs a measure-theoretic condition on the boundary $\{f_Y * w = \alpha\}$; a topological condition on closures, as printed, is not enough.

Formalization scope

• $\mathbb R^d$ is Fin d → ℝ with volume and the Pi order; $d$ is any natural number. A distribution is a probability measure P : Measure (E d); every integral is a Bochner integral.
• The kernel $w$ is a measurable function. The paper allows a local Borel measure, so that $w = \delta_0$ gives the density level set score (12); that case is not formalized.
• Standing assumptions. $w \ge 0$ and $\alpha > 0$ (Theorem 2), $h \ge 0$ measurable and integrable (Assumption 1(a)), $A$ Borel.
• Integrability. Assumption 1 and Theorem 2's "$(S')^\Gamma(A,\bullet)$ finite a.e. and $(S')^\Gamma(A,\bullet)f_Y$ integrable" are pinned down as the single hypothesis that $(s, z) \mapsto w(z - s)h(z)$ is integrable for $P_Y \otimes \mathcal L^d$. With $w, h \ge 0$ it covers every Borel set at once, including $L(f_Y * w;\alpha)$. The layer-cake milestone uses Assumption 1(b)/(c) for the given $y$ and the almost-everywhere integrability of $w(z - \cdot)$ under $P_X$.
• No class $\mathcal V^d$. The consistency statement is pointwise in $P_Y$; its convexity is never used.
• Strict consistency is stated under $\mathcal L^d\{f_Y * w = \alpha\} = 0$ and $h \ne 0$ a.e., and "only minimizer" is read modulo $\mathcal L^d$-null sets. The printed condition "$L(f_Y * w;\alpha)$ equals the closure of $\{f_Y * w > \alpha\}$" does not imply the null-set property the proof uses: for $d = 1$, $P_Y = \delta_0$, $w = \alpha + \mathrm{dist}(\cdot, C)$ with $C$ a fat Cantor set, the closure condition holds but $\mathbb R \setminus C$ scores as well as $L$.
• Level sets use $\ge$, as in (9). The proof's partition by $\{f_Y * w > \alpha\}$ is a printed slip; the milestones use $A \setminus L$ and $L \setminus A$.
• Ruled out. Because a Bochner integral of a non-integrable function is $0$, dropping the integrability hypotheses, letting $A$ range over non-measurable sets, or fixing particular $w$ or $h$ would trivialize or change the statements; none of these is done.
• Infrastructure: Mathlib's layer cake (MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul and relatives in Mathlib/MeasureTheory/Integral/Layercake.lean) and Fubini–Tonelli (integral_prod). A reusable lemma for $\int\!\!\int g(z) w(z - s) h(z)\,dz\,dP(s) = \int g(z)(f_P * w)(z)h(z)\,dz$ is welcome; it also serves the companion mission on the $L^2$ scoring rules.

Selected references

• X. Meng, J. W. Taylor, S. Ben Taieb, S. Li, Scores for Multivariate Distributions and Level Sets, Operations Research, 2025; preprint arXiv:2002.09578v6, 2023. https://arxiv.org/abs/2002.09578
• T. Gneiting, A. E. Raftery, Strictly Proper Scoring Rules, Prediction, and Estimation, Journal of the American Statistical Association 102(477), 359–378, 2007. https://doi.org/10.1198/016214506000001437
• T. Gneiting, Making and Evaluating Point Forecasts, Journal of the American Statistical Association 106(494), 746–762, 2011. https://doi.org/10.1198/jasa.2011.r10138
• T. Fissler, R. Frongillo, J. Hlavinová, B. Rudloff, Forecast Evaluation of Quantiles, Prediction Intervals, and Other Set-Valued Functionals, Electronic Journal of Statistics 15(1), 1034–1084, 2021. https://doi.org/10.1214/21-EJS1808
• A. E. Abbas, D. V. Budescu, Y. Gu, Assessing Joint Distributions with Isoprobability Contours, Management Science 56(6), 997–1011, 2010. https://doi.org/10.1287/mnsc.1100.1157
• E. H. Lieb, M. Loss, Analysis, 2nd ed., Graduate Studies in Mathematics 14, AMS, 2001. https://doi.org/10.1090/gsm/014