All missions

Motivation

Optical channels, such as fibers or free-space links, are ubiquitous in today's telecommunication networks. They rely on the electromagnetic field associated with photons to carry information from one point to another in space. As a result, a complete physical model of these channels must necessarily take quantum effects into account in order to determine their ultimate performances. Specifically, Gaussian photonic (or bosonic) quantum channels have been extensively studied over the past decades given their importance for practical purposes. In spite of this, a longstanding conjecture on the optimality of Gaussian encodings has yet prevented finding their communication capacity. Here, this conjecture is solved by proving that the vacuum state achieves the minimum output entropy of a generic Gaussian bosonic channel. This establishes the ultimate achievable bit rate under an energy constraint, as well as the long awaited proof that the single-letter classical capacity of these channels is additive. Beyond capacities, it also has broad consequences in quantum information sciences.

This mission is the statement-level formalization of Ultimate communication capacity of quantum optical channels by solving the Gaussian minimum-entropy conjecture (arXiv:1312.6225v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-energy Gaussian minimum output entropy (Eq. (2), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• Ultimate communication capacity of quantum optical channels by solving the Gaussian minimum-entropy conjecture, arXiv:1312.6225v1, https://arxiv.org/abs/1312.6225v1

Motivation

Many estimation problems in statistics, signal processing and machine learning ask for a low-rank positive semidefinite matrix: phase retrieval, matrix sensing, PCA-type problems and the Burer–Monteiro approach to semidefinite programs. A standard formulation is

$$\min_{X\in\mathbb S^{p\times p},\ X\succeq0,\ \operatorname{rank}(X)=r} f(X),\qquad 0<r\le p, \tag{1}$$

and Riemannian optimization solves it by treating the feasible set as a smooth manifold. Two geometries are in common use. In the embedded geometry the set of rank-$r$ PSD matrices is a submanifold of $\mathbb R^{p\times p}$ with the Euclidean metric. In the quotient geometry one writes $X=YY^\top$ with a full-column-rank factor $Y$ and optimizes over equivalence classes $[Y]=\{YO:O\text{ orthogonal}\}$. Algorithms built on the two geometries behave similarly in experiments, and landscape results (absence of spurious local minima, strict saddles) have been proved separately for each. Luo, Li and Zhang (arXiv:2110.12121, Mathematics of Operations Research 2024) explain this by an explicit dictionary between the Riemannian gradients and Hessians of the two geometries. This mission formalizes their first main result, Theorem 3, for the full-rank factorization of PSD matrices.

Setting

Matrices carry the Frobenius inner product $\langle A,B\rangle=\operatorname{tr}(A^\top B)$. The objective $f:\mathbb R^{p\times p}\to\mathbb R$ is twice continuously differentiable and symmetric, $f(X)=f(X^\top)$ (the paper's standing assumptions); $\nabla f$ and $\nabla^2f$ are its Euclidean gradient and Hessian.

Embedded geometry. $\mathcal M_{r+}=\{X\in\mathbb S^{p\times p}:X\succeq0,\ \operatorname{rank}X=r\}$, viewed as $\mathcal M^e_{r+}\subset\mathbb R^{p\times p}$. Its tangent space $T_X\mathcal M^e_{r+}$ is the span of the tangent cone. The Riemannian gradient $\operatorname{grad}f(X)$ is the orthogonal projection of $\nabla f(X)$ onto $T_X\mathcal M^e_{r+}$, and the Riemannian Hessian quadratic form $\operatorname{Hess}f(X)[\xi,\xi]$ is the derivative $\frac{d}{dt}\langle\operatorname{grad}f(c(t)),\xi\rangle$ at $t=0$ along any $C^1$ curve $c$ in $\mathcal M_{r+}$ with $c(0)=X$, $c'(0)=\xi$.

Quotient geometry. The total space is $\mathbb R_*^{p\times r}$, the $p\times r$ matrices of full column rank, with the objective $\bar h_{r+}(Y)=f(YY^\top)$ (18a). A weight $Y\mapsto W_Y$, smooth and symmetric positive definite, defines the metric $\bar g_Y(\eta,\theta)=\operatorname{tr}(W_Y\eta^\top\theta)$. The vertical space $\mathcal V_Y=\{Y\Omega:\Omega^\top=-\Omega\}$ is tangent to the orbit $[Y]$, and the horizontal space $\mathcal H_Y$ is its $\bar g_Y$-orthogonal complement. Tangent vectors of the quotient $\mathcal M^{q_1}_{r+}=\mathbb R_*^{p\times r}/\mathbb O_r$ are represented by horizontal vectors: $\overline{\operatorname{grad}h_{r+}([Y])}$ is the horizontal part of the total-space gradient $\nabla\bar h_{r+}(Y)W_Y^{-1}$, and $\overline{\operatorname{Hess}h_{r+}([Y])}[\theta,\theta]=\bar g_Y(\bar\nabla_\theta\operatorname{grad}\bar h,\theta)$ for horizontal $\theta$, where $\bar\nabla$ is the Levi-Civita connection of $\bar g$ (Koszul formula).

Comparison data. $\mathcal L^{r+}_Y(\theta)=Y\theta^\top+\theta Y^\top$; $U\in\mathrm{St}(r,p)$ spans the top $r$ eigenspace of $X=YY^\top$, $P=U^\top Y$, $Y^\dagger=(Y^\top Y)^{-1}Y^\top$. For a quadratic form on a $d$-dimensional space with inner product $g$, $\lambda_k$ is its $k$-th largest eigenvalue relative to $g$ ($1\le k\le d$). $\sigma_1,\sigma_r$ are the extreme singular values of an $r\times r$ matrix.

Formalization targets

Goal: Theorem 3 (p. 21)

If in addition $W_Y=OW_{YO}O^\top$ for all orthogonal $O$, then for every $Y\in\mathbb R_*^{p\times r}$ and $X=YY^\top$,

$$\operatorname{grad}f(X)=\Big(\overline{\operatorname{grad}h_{r+}([Y])}W_YY^\dagger+\big(\overline{\operatorname{grad}h_{r+}([Y])}W_YY^\dagger\big)^\top(I_p-YY^\dagger)\Big)/2,\qquad\overline{\operatorname{grad}h_{r+}([Y])}=2\operatorname{grad}f(X)YW_Y^{-1},$$

and if $[Y]$ is a Riemannian first-order stationary point of (18a),

$$\overline{\operatorname{Hess}h_{r+}([Y])}[\theta,\theta]=\operatorname{Hess}f(X)[\mathcal L^{r+}_Y(\theta),\mathcal L^{r+}_Y(\theta)]\quad\forall\theta\in\mathcal H_Y,$$

both Hessians have $d=pr-(r^2-r)/2$ eigenvalues, and $\lambda_i(\overline{\operatorname{Hess}h_{r+}([Y])})$ lies between $2\sigma_r(PW_Y^{-1}P^\top)\lambda_i(\operatorname{Hess}f(X))$ and $4\sigma_1(PW_Y^{-1}P^\top)\lambda_i(\operatorname{Hess}f(X))$.

Milestones

1. Lemma 6: $Y_1Y_1^\top=Y_2Y_2^\top$ iff $Y_2=Y_1O$; $U_1B_1U_1^\top=U_2B_2U_2^\top$ iff $U_2=U_1O$, $B_2=O^\top B_1O$; $\mathcal M_{r+}=\{YY^\top\}=\{UBU^\top\}$.
2. Lemma 3: $\mathcal M^e_{r+}$ is a smooth embedded submanifold of dimension $pr-r(r-1)/2$, with tangent space in the block form (14).
3. Lemma 4 (i): explicit $\mathcal V_Y$, $\mathcal H_Y$ and their dimensions.
4. Lemma 1 on $\mathbb R_*^{p\times r}$: the total-space gradient is already horizontal.
5. Proposition 1, embedded bullet: the formulas (19) for $\operatorname{grad}f$ and $\operatorname{Hess}f$.
6. Proposition 1, quotient bullet: the formulas (20) for the lifted gradient and Hessian.
7. Proposition 2: $\mathcal L^{r+}_Y$ is a bijection $\mathcal H_Y\to T_X\mathcal M^e_{r+}$.
8. Proposition 2, (23): $2\sigma_r(PW_Y^{-1}P^\top)\bar g_Y(\theta,\theta)\le\|\mathcal L^{r+}_Y\theta\|_F^2\le4\sigma_1(PW_Y^{-1}P^\top)\bar g_Y(\theta,\theta)$.
9. Theorem 2: the abstract sandwich inequality for spectra of two quadratic forms related by a bijection with bounded metric distortion.

Significance

Theorem 3 says that at stationary points the two geometries see the same second-order landscape: the Hessians are congruent through $\mathcal L^{r+}_Y$, so their eigenvalues have the same signs and comparable magnitudes, with explicit factors depending on $W_Y$ and the spectrum of $X$. The paper derives from it (Corollary 1) that first-order stationary points, second-order stationary points and strict saddles correspond between the embedded and quotient formulations, so a landscape result proved in one geometry transfers to the other. The choice of weight $W_Y$ (flat $I_r$, right-invariant $(Y^\top Y)^{-1}$, or $Y^\top Y$) changes the comparison constants, which is how the paper relates the conditioning of the two approaches.

The result is proved in the paper; it is not formalized anywhere. A formal development adds machine-checked Riemannian gradients and Hessians on a concrete embedded submanifold and on a concrete quotient, a checked horizontal-space computation, and a reusable abstract sandwich theorem for max–min eigenvalues. Corollary 1 and the parallel results for the polar factorization and for general rank-$r$ matrices (Theorems 4–7) are natural follow-up missions on the same definitions.

Difficulty

The identities (19), (20) and (34) are matrix calculus once the geometric objects are pinned down; the difficulty is that the definitions are intrinsic. The embedded Hessian requires differentiating the tangent projection $P_{T_X\mathcal M^e_{r+}}$ along the manifold, which produces the curvature term $2\langle\nabla f(X),U_\perp D\Sigma^{-1}D^\top U_\perp^\top\rangle$; the obvious computation that ignores the moving tangent space gives the wrong Hessian. The quotient Hessian involves the derivative of the weight $W_Y$ and needs the horizontal-space description of Lemma 4 to see that the projection in (5) can be dropped. Identifying $\operatorname{span}$ of the tangent cone with the block form (14) needs an explicit chart of the rank-$r$ PSD set. The final sandwich requires a max–min (Courant–Fischer) argument relative to two different inner products, and the order of the bounds flips for negative eigenvalues.

Formalization scope

• $\mathbb R^{a\times b}$ is EuclideanSpace ℝ (Fin a × Fin b) (Frobenius inner product) with matrix views toMat/ofMat. The weight $W$ takes values in $\mathbb R^{r\times r}$ in the same form so that $\mathrm DW_Y$ is defined.
• The embedded tangent space and Riemannian gradient are the published platform definitions ProjLikeRetr.Retractor.tangentSpace (span of the tangent cone) and ZORiem.RGD.rgrad (projected Euclidean gradient); "smooth embedded submanifold of dimension $d$" is the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold k d, for every $k$.
• The embedded Hessian is a curve-defined predicate on a quadratic form; the quotient Hessian is the Koszul-formula form $\bar g_Y(\mathrm DG[\theta],\theta)+\tfrac12\mathrm D\bar g(\theta,\theta)[G]$. Neither is defined by the paper's formulas (19), (20) or (34): those are theorems, and a formalization that defined the Hessians or gradients by them would make the mission trivial.
• $\lambda_k$ is the max–min value over $k$-dimensional subspaces (the paper's Lemma 13); "sandwiched between $a$ and $b$" means $\min(a,b)\le\mu\le\max(a,b)$; $\sigma_1,\sigma_r$ of the symmetric positive definite $PW_Y^{-1}P^\top$ are its extreme Rayleigh quotients.
• Conventions: $0<r\le p$; $f$ is $C^2$ and symmetric; $W_Y$ is positive definite on $\mathbb R_*^{p\times r}$ and $W$ is smooth there (the meaning of "Riemannian metric"); "$U$ spans the top $r$ eigenspace of $YY^\top$" is $U^\top U=I_r$, $UU^\top Y=Y$; $Y^\dagger=(Y^\top Y)^{-1}Y^\top$; $\mathcal L^{r+}_Y$ is defined as $Y\theta^\top+\theta Y^\top$ rather than by the block formula (22).
• In Theorem 2 the map $\mathcal L$ is assumed linear, as in every application in the paper, and the printed domain $\mathcal H_X$ in (12)–(13) is read as $\mathcal H_Z$.
• Not encoded: the half of Lemma 3 about general rank-$r$ matrices, Lemma 4 (ii) (no quotient-manifold structure in Mathlib), the polar factorization geometry and Theorems 4–7, Corollaries 1–2.

Useful contributions include Mathlib-level lemmas on the tangent cone of the rank-$r$ PSD set, Courant–Fischer for a form relative to a non-standard inner product, and matrix-calculus lemmas for $\mathrm D(W^{-1})$.

Selected references

• Y. Luo, X. Li, A. R. Zhang, On Geometric Connections of Embedded and Quotient Geometries in Riemannian Fixed-rank Matrix Optimization, Mathematics of Operations Research, 2024; arXiv:2110.12121v2. https://arxiv.org/abs/2110.12121
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244
• M. Journée, F. Bach, P.-A. Absil, R. Sepulchre, Low-rank optimization on the cone of positive semidefinite matrices, SIAM Journal on Optimization 20(5), 2010. https://doi.org/10.1137/080731359
• B. Vandereycken, S. Vandewalle, A Riemannian optimization approach for computing low-rank solutions of Lyapunov equations, SIAM J. Matrix Anal. Appl. 31(5), 2010. https://doi.org/10.1137/090764566
• R. Bhatia, Matrix Analysis, Springer GTM 169, 1997. https://doi.org/10.1007/978-1-4612-0653-8

Motivation

The small-step subgradient method is the basic algorithm for minimizing a nonsmooth, nonconvex, locally Lipschitz function $f:\mathbb R^n\to\mathbb R$. It is also the scheme behind stochastic gradient training of neural networks with nonsmooth activations. From a starting point $x_0$ it iterates

$$x_{i+1}=x_i-\varepsilon_i v_i,\qquad v_i\in\partial^c f(x_i),$$

with step sizes $\varepsilon_i\to0$ and $\sum_i\varepsilon_i=+\infty$. The basic question is whether a bounded run converges. For smooth $f$, and for continuous-time subgradient flows, convergence follows from a Kurdyka–Łojasiewicz (KŁ) inequality together with tame geometry such as Whitney stratifiability (Bolte, Daniilidis, Lewis, Shiota 2007; Absil, Mahony, Andrews 2005). Whether the same hypotheses suffice for the discrete nonsmooth method was open.

R. Ríos-Zertuche (arXiv:2007.11699, published in Math. Oper. Res. 2022) is a companion to the work of Bolte, Pauwels and Ríos-Zertuche on the long-term dynamics of the subgradient method for path-differentiable functions (arXiv:2006.00098). That work proves positive results, such as slowdown near limit points and convergence of the values under the weak Sard condition. The examples paper shows that these results cannot be improved to convergence of the iterates. Its first example (Section 2) lives on $\mathbb R^2$ and is the subject of this mission.

Setting

For a locally Lipschitz $f:\mathbb R^n\to\mathbb R$, the Clarke subdifferential $\partial^c f(x)$ is the convex envelope of all limits $\lim\nabla f(y_k)$ along sequences $y_k\to x$ of points where $f$ is differentiable. The critical set is $\operatorname{crit}f=\{x:0\in\partial^c f(x)\}$.

A subgradient sequence (Definition 1) is a sequence obeying the recursion above with positive steps $\varepsilon_i\to0$, $\sum\varepsilon_i=+\infty$. The function $f$ is path-differentiable (Definition 2) if for every Lipschitz curve $\gamma$ and almost every $t$, $(f\circ\gamma)'(t)=v\cdot\gamma'(t)$ for all $v\in\partial^c f(\gamma(t))$. It satisfies the weak Sard condition (Definition 3) if it is constant on each connected component of $\operatorname{crit}f$. It is Whitney $C^\infty$-stratifiable (Definition 5) if its graph in $\mathbb R^{n+1}$ is a locally finite union of disjoint connected $C^\infty$ submanifolds. These pieces must satisfy the frontier condition and Whitney's condition A: limits of tangent spaces of a stratum contain the tangent spaces of the strata in its boundary.

The example works on $\mathbb R^2$. For $i\ge2$ let

$$\vartheta_i=\sum_{k=2}^{i}\frac1{k\log k},\qquad x_i=\Bigl[1+\frac{(-1)^i}{i}\Bigr](\cos\vartheta_i,\sin\vartheta_i),$$

$\varepsilon_i=\|x_{i+1}-x_i\|$ and $v_i=-(x_{i+1}-x_i)/\varepsilon_i$. Let $\varphi(x)=|1-\|x\||$ be the distance to the unit circle $S^1$. Let $\psi$ be a smooth radial bump with values in $[0,1]$, equal to $1$ on $B_1(0)$, vanishing for $\|x\|\ge2$ and non-increasing along rays. Set $\psi_i(x)=\psi(2^i(x-x_i))$ and $V_i(x)=(x-x_i)\cdot v_i+1/i$. For $i_0\ge2$,

$$f(x)=\Bigl(1-\sum_{i\ge i_0}\psi_i(x)\Bigr)\varphi(x)+\sum_{i\ge i_0}\psi_i(x)V_i(x).\tag{4}$$

Formalization targets

Goal

There are $f:\mathbb R^2\to\mathbb R$, steps $(\varepsilon_i)$ and a sequence $(x_i)$ such that $(x_i)$ is a bounded, non-convergent subgradient sequence of $f$, and $f$ has all of the following properties:

• it is Lipschitz and path-differentiable;
• it satisfies the weak Sard condition;
• it is Whitney $C^\infty$-stratifiable;
• it is $C^\infty$ on a ball around every $x_i$;
• it satisfies

$$\|\nabla f(x)\|\ge\tfrac12\qquad\text{for all }x\notin\operatorname{crit}f.$$

This is the paper's negative answer to its question Q9, combined with its remarks in Q1 and Q12. The witness is left existential.

Milestones

The milestones are the properties of the explicit witness (4):

• the step-size estimates ($\varepsilon_i\to0$, $\sum\varepsilon_i=\infty$, $\sum\varepsilon_i^2<\infty$);
• Lemma 7: $v_i$ is close to $\pm x_i/\|x_i\|$, and radial projection is Lipschitz near $x_i$;
• Proposition 6 (i)–(vii): smoothness off $S^1\cup\{0\}$; $\nabla f=v_i$ on $B_{1/2^i}(x_i)$, so that $(x_i)$ is a subgradient sequence; $\partial^c f(p)=\{ap:a\in[-1,1]\}$ on $S^1$; $\operatorname{crit}f=S^1\cup\{0\}$; Lipschitz path-differentiability; Whitney stratifiability; and $\|\nabla f\|>1/2$ off the critical set;
• the weak Sard condition;
• $\operatorname{acc}\{x_i\}=S^1$, with boundedness and non-convergence.

Significance

The example is a counterexample: the standard toolbox of tame geometry plus a KŁ inequality does not give convergence of the discrete small-step subgradient method, even with a uniform gradient lower bound away from the critical set and the weak Sard condition. In continuous time the same hypotheses give convergence. The gap therefore comes from discretization. Any convergence proof for nonsmooth subgradient methods needs further structure, such as definability in an o-minimal structure or a stronger KŁ inequality near the critical set. Q12 adds that requiring the iterates to stay in the full-measure set of differentiability points does not help.

The result is proved in the paper; to our knowledge none of it is formalized. Formalizing it gives the first machine-checked Clarke-subdifferential, path-differentiability and Whitney-stratification counterexample. It also gives reusable estimates for an explicit sequence spiralling onto a circle.

Difficulty

Most of the steps are explicit estimates, but three of them are delicate.

• The Clarke subdifferential on $S^1$. It must be computed although infinitely many bumps accumulate there. Near each $x_i$ the gradient of $f$ contains the term $\nabla\psi_i\,(V_i-\varphi)$, where $\nabla\psi_i$ is of size $2^i$. Showing that the limiting gradients are still only $\pm p$ requires the second-order agreement of $V_i$ and $\varphi$ on $B_{1/2^{i-1}}(x_i)$, and that rests on the estimate of Lemma 7.
• Path differentiability. It does not follow from local Lipschitz continuity. A Lipschitz curve may cross the circle at uncountably many times, so the chain rule has to be checked for every element of $\partial^c f(\gamma(t))$ at almost every such time.
• Whitney's condition A. It must hold where the two-dimensional strata of the graph meet the circle stratum. That requires control of the tangent planes of the graph along sequences entering the bump regions.

Formalization scope

Everything lives in EuclideanSpace ℝ (Fin n). The definitions follow these conventions:

• $\partial^c f(x)$ is the convex hull of the published ShorNonsmooth.AlmostDiff.almostGradients, which uses cluster points of the gradients rather than limits; the two sets are the same.
• Path differentiability quantifies over every Lipschitz curve and every element of $\partial^c f(\gamma(t))$, and also asserts that $\gamma$ is differentiable at $t$, which holds almost everywhere by Rademacher's theorem.
• Strata are connected, pairwise disjoint and locally finite at the points of the graph. Each is a $C^k$ coordinate-slice submanifold (the published ProjLikeRetr.Retractor.IsSubmanifold) for every $k$. Tangent spaces are spans of tangent cones, and Grassmannian convergence is convergence of the subspace gap to $0$.
• The bump is an arbitrary BumpProfile with exactly the properties listed on p. 6, and the series in (4) are tsums. The indices $i<2$, where $1/0=0$ and $\log 1=0$ in Lean, are never used.

Four statements are adjusted, and each adjustment is disclosed in its item:

• Proposition 6 (i) is stated on $\mathbb R^2\setminus(S^1\cup\{0\})$, as in the paper's proof, because $f$ has a cone point at $0$.
• The last link "$<2/i$" of the step-size chain is false and is dropped.
• Proposition 6 (ii), (iv), (vii) and the weak Sard claim hold for $i_0$ beyond a threshold depending on the bump. For small $i_0$ the bump supports overlap.
• The KŁ clauses also assert differentiability, since Lean's gradient is $0$ at non-differentiable points.

The goal cannot be met trivially. Boundedness of the sequence and the conditions $\varepsilon_i\to0$, $\sum\varepsilon_i=\infty$ are part of it, and they rule out an affine $f$. Every regularity property is a separate conjunct. Contributions that develop the geometry of Whitney stratifications and path differentiability in Lean are reusable well beyond this example.

Selected references

• R. Ríos-Zertuche, Examples of pathological dynamics of the subgradient method for Lipschitz path-differentiable functions, arXiv:2007.11699v1, 2020; Math. Oper. Res., 2022. https://arxiv.org/abs/2007.11699
• J. Bolte, E. Pauwels, R. Ríos-Zertuche, Long term dynamics of the subgradient method for Lipschitz path differentiable functions, arXiv:2006.00098, 2020. https://arxiv.org/abs/2006.00098
• J. Bolte, A. Daniilidis, A. Lewis, M. Shiota, Clarke subgradients of stratifiable functions, SIAM J. Optim. 18 (2007). https://doi.org/10.1137/060670080
• D. Davis, D. Drusvyatskiy, S. Kakade, J. D. Lee, Stochastic subgradient method converges on tame functions, Found. Comput. Math. 20 (2020). https://arxiv.org/abs/1804.07795
• P.-A. Absil, R. Mahony, B. Andrews, Convergence of the iterates of descent methods for analytic cost functions, SIAM J. Optim. 16 (2005). https://doi.org/10.1137/040605266

Motivation

Banking and insurance regulation measures capital requirements with risk measures that look only at the tail of a loss distribution. The Basel framework moved from Value-at-Risk (VaR) to Expected Shortfall (ES) for market risk (BCBS, Minimum capital requirements for market risk, 2016), and both VaR and ES at level $p$ depend on a loss only through its distribution beyond the $p$-quantile. Liu and Wang (SSRN 2841909; Mathematics of Operations Research 46(3), 2021, doi:10.1287/moor.2020.1072) isolate this feature as a definition. A tail risk measure is any risk measure that depends only on the tail, and every such measure is generated by an ordinary law-invariant risk measure applied to the tail. The paper then asks which of the classical properties of risk measures (Artzner et al. 1999; Föllmer and Schied 2002) survive this construction.

The answer to that question is a practical design rule. A regulator or risk manager who wants a coherent tail risk measure can choose any coherent law-invariant risk measure and apply it to the tail. The theorem guarantees that the result is again coherent, and that nothing is lost by working only with generators.

Setting

Fix an atomless probability space $(\Omega,\mathcal F,\mathbb P)$: every event of positive probability contains an event of strictly smaller positive probability. A random variable $X:\Omega\to\mathbb R$ is a loss when positive and a profit when negative. Its distribution function is $F_X(x)=\mathbb P(X\le x)$. The space of risks is $\mathcal X=L^\infty$, the measurable, essentially bounded random variables. A risk measure is a real-valued functional $\rho$ on $\mathcal X$.

For $p\in(0,1)$, the $p$-tail of $X$ is a random variable $X_p$ with distribution function

$$\mathbb P(X_p\le x)=\frac{(\mathbb P(X\le x)-p)_+}{1-p},\qquad x\in\mathbb R, \tag{2}$$

the conditional law of $X$ beyond its $p$-quantile. A risk measure $\rho$ is a $p$-tail risk measure if $\rho(X)=\rho(Y)$ whenever $X_p$ and $Y_p$ have the same law. A pair $(\rho,\rho^*)$ is a $p$-tail pair if $\rho^*$ is law-invariant and

$$\rho(X)=\rho^*(X_p),\qquad X\in\mathcal X, \tag{3}$$

in which case $\rho^*$ is a $p$-generator of $\rho$. For example, $\mathrm{ES}_p(X)=\mathbb E[X_p]$ is generated by the expectation. The mixture $X^{(p)}$ has distribution function $p\,\mathbb 1_{\{x\ge\operatorname{ess\text{-}inf}X\}}+(1-p)F_X(x)$: it adds mass $p$ at the essential infimum of $X$.

The classical properties are those of Appendix A of the paper:

• (A1) monotonicity: $\rho(X)\le\rho(Y)$ when $X\le Y$ a.s.;
• (A2) translation invariance: $\rho(X-m)=\rho(X)-m$;
• (A3) convexity: $\rho(\lambda X+(1-\lambda)Y)\le\lambda\rho(X)+(1-\lambda)\rho(Y)$ for $\lambda\in[0,1]$;
• (A4) positive homogeneity: $\rho(\lambda X)=\lambda\rho(X)$ for $\lambda>0$;
• (A5) subadditivity;
• (A6) comonotonic additivity;
• (A7) $\prec_{\mathrm{cx}}$-monotonicity.

A monetary risk measure satisfies (A1)–(A2), a convex one (A1)–(A3), and a coherent one (A1)–(A4) (Definition A.1).

Formalization targets

Goal: Theorem 1 (iii)

For $p\in(0,1)$ and a $p$-tail pair $(\rho,\rho^*)$ on $L^\infty$,

$$\rho\ \text{coherent}\iff\rho^*\ \text{coherent},\qquad \rho\ \text{convex}\iff\rho^*\ \text{convex},\qquad \rho\ \text{monetary}\iff\rho^*\ \text{monetary}.$$

All three equivalences are part of the goal. No normalization such as $\rho(0)=0$ is assumed.

Milestones

• Lemma B.1 (p. 19): $(X^{(p)})_p\overset{d}{=}X$; the maps $X\mapsto X_p$ and $X\mapsto X^{(p)}$ preserve the stochastic order $\prec_{\mathrm{st}}$; and $X\prec_{\mathrm{st}}X_p$.
• Proposition 1 (p. 7): every $p$-tail risk measure has a $p$-generator, which is unique and given by $\rho^*(X)=\rho(X^{(p)})$.
• Eq. (14) (p. 20): for $B\sim\mathrm{Bern}(p)$ independent of $Z$ and $t\le\operatorname{ess\text{-}inf}Z$, $(tB+Z(1-B))_p\overset{d}{=}(\operatorname{ess\text{-}inf}(Z)B+Z(1-B))_p\overset{d}{=}Z$.
• Theorem 1 (i) (p. 9): monotonicity, translation invariance, positive homogeneity and comonotonic additivity each pass between $\rho$ and $\rho^*$ in both directions.
• Theorem 1 (ii) (p. 9): subadditivity, convexity and $\prec_{\mathrm{cx}}$-monotonicity pass from $\rho$ to $\rho^*$. The converses fail (Example 1, the tail standard deviation).
• Theorem 3 (p. 10): for a $p$-tail pair of monotone risk measures and marginals $F_1,\dots,F_n$,

$$\sup\{\rho(S):S\in\mathcal S_n(F_1,\dots,F_n)\}=\sup\{\rho^*(T):T\in\mathcal S_n(F_1^{[p]},\dots,F_n^{[p]})\},$$

where $\mathcal S_n$ is the set of sums $Y_1+\dots+Y_n$ with $Y_i\sim F_i$ (resp. $F_i^{[p]}$, the law of the $p$-tail).

Significance

The result. Theorem 1 (iii) makes the generator a complete parametrization of coherent and convex tail risk measures. Coherent tail risk measures are exactly $\rho^*(X_p)$ with $\rho^*$ coherent and law-invariant, so representation results for law-invariant coherent risk measures (Kusuoka 2001) transfer to tail risk measures. The paper uses this for dual representations (Appendix G) and for the bound $\rho\ge\mathrm{ES}_p$ of Theorem 2. Theorem 3 reduces worst-case risk aggregation for a tail risk measure to the same problem for its generator on tail marginals. It contains classical results on worst-case VaR (Bernard et al. 2014, Lemma 4.3) and the subadditivity of ES as special cases.

Formalizing it. The results are proved in the paper; none of them is machine-checked. The mission produces a Lean statement of tail risk measures and their generators that later missions on tail risk can import. It also produces formal versions of the distributional identities (Lemma B.1, eq. (14)) on which the paper's proofs rest, and a statement of worst-case aggregation in extended-real suprema. A complete development would also be the first formal proof that ES-type constructions preserve coherence through a general generator, rather than for one specific measure.

Difficulty

Several directions are routine. Monotonicity, translation invariance and positive homogeneity pass from $\rho^*$ to $\rho$ because $X\mapsto X_p$ commutes with shifts and positive scalings and preserves $\prec_{\mathrm{st}}$. The converse directions go through $X^{(p)}$.

Convexity is the obstruction. The obvious argument would compare $(\lambda X+(1-\lambda)Y)_p$ with $\lambda X_p+(1-\lambda)Y_p$, but the tail of a sum is not the sum of the tails. The event "beyond the $p$-quantile" for the sum differs from the corresponding events for $X$ and $Y$, so no pointwise or comonotone coupling identifies them. Example 1 makes this concrete: the tail standard deviation is generated by a convex measure and is not convex. Convexity of $\rho$ therefore needs monotonicity of $\rho^*$ together with the worst-case aggregation identity of Theorem 3. That identity is a statement about all dependence structures with given marginals, and it requires constructing, on an atomless space, couplings whose tails dominate a given sum.

Formalization scope

• Domain. The space of risks is $L^\infty$ (TailRiskSharing.TailConv.Linf), as the paper suggests on p. 5. Then $\mathcal X^*=\mathcal X$, every risk measure is a real-valued function on $\Omega\to\mathbb R$, and every property quantifies over $L^\infty$ only. The general cone $\mathcal X\supseteq L^\infty$ with $(-\infty,\infty]$-valued risk measures is not stated.
• Atomlessness. The probability space is atomless in the classical sense (TailRiskSharing.VaRConv.IsAtomless), not Mathlib's NoAtoms, which only says that singletons are null.
• Tails and mixtures are relations on distribution functions: "$Z$ has the law of $X_p$" is the identity (2). The generator relation (3) is required for every $Z\in L^\infty$ with that law, and no existence of such $Z$ is assumed.
• Coherence is Definition A.1: monotone, translation-invariant, convex and positively homogeneous. It uses convexity, not subadditivity, and it includes monotonicity.
• Stochastic orders compare expectations of increasing (resp. convex) test functions. Integrability of $f(X)$ and $f(Y)$ is part of the definition, as in "provided that both expectations exist".
• Theorem 3. Each marginal $F_i$ is given by a representative in $L^\infty$, and the suprema are taken in the extended reals.

A formalization in which $\rho^*$ is a fixed Classical.choose of the tail, in which coherence omits monotonicity, or in which atomlessness is replaced by NoAtoms is not this theorem.

A complete development needs the quantile transform on an atomless space, couplings with a prescribed joint law, the elementary identities of Lemma B.1 and eq. (14), and the worst-case aggregation argument of Appendix C. The distributional lemmas, quantile couplings and aggregation sets can be reused in any later mission on law-invariant risk measures. Contributions to any milestone, and to general infrastructure for quantile couplings on atomless spaces, are welcome.

Selected references

• F. Liu and R. Wang, A Theory for Measures of Tail Risk, SSRN 2841909 (journal accepted version, 2020); Mathematics of Operations Research 46(3), 2021. https://ssrn.com/abstract=2841909, https://doi.org/10.1287/moor.2020.1072
• P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9(3), 1999. https://doi.org/10.1111/1467-9965.00068
• H. Föllmer and A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4), 2002. https://doi.org/10.1007/s007800200072
• S. Kusuoka, On law invariant coherent risk measures, Advances in Mathematical Economics 3, 2001. https://doi.org/10.1007/978-4-431-67891-5_4
• C. Bernard, X. Jiang and R. Wang, Risk aggregation with dependence uncertainty, Insurance: Mathematics and Economics 54, 2014. https://doi.org/10.1016/j.insmatheco.2013.11.005
• Basel Committee on Banking Supervision, Minimum capital requirements for market risk, 2016. https://www.bis.org/bcbs/publ/d352.htm

Motivation

Exploratory data analysis often summarizes a large data set by a small number of representative regions: histogram bins, the leaves of a density estimation tree, balls around cluster centres, or the regions chosen by a covering or $k$-center optimization. Estes, Ball and Lovell (SSRN 3005997; Mathematics of Operations Research, 2021, doi:10.1287/moor.2020.1115) treat all of these as instances of one abstraction, the representative region selection (RRS) method, motivated by summarizing air-traffic ground-delay programs at Newark airport. The first half of their paper proposes axioms for the quality of such summaries. The second half (§6) asks a statistical question: when the data are an i.i.d. sample, do the summaries converge to the population they describe? This mission formalizes that convergence theory, culminating in the consistency of the density estimate that any RRS method induces.

Setting

Let $M$ be a set. An RRS method on $M$ is a pair $(\mathcal C, f)$: $\mathcal C \subseteq 2^M$ is a class of allowed regions, and $f$ maps every finite set $S \subseteq M$ to a finite set $f(S) \subseteq \mathcal C$. The coverage region is $C(S; f) = \bigcup_{A \in f(S)} A$. The method is sample-covering if $S \subseteq C(S; f)$, and sample-intersecting if every $A \in f(S)$ contains a point of $S$.

Now let $(M, d)$ be a metric space with a σ-algebra containing every closed ball, and let $X_1, X_2, \dots$ be i.i.d. $M$-valued random variables with law $P_X$. Write $S_n = \{X_1, \dots, X_n\}$, $C_n(f) = C(S_n; f)$, and $\hat P_{X,n}(T)$ for the fraction of the first $n$ observations lying in $T$. The support of $P_X$ is the set of points all of whose closed balls of positive radius have positive probability.

Regularity is imposed on the class, not on the method. A scalable class $(\mathcal C, \Theta, R)$ writes every region as $R(\theta, \lambda)$ with a shape parameter $\theta \in \Theta$ and a scale $\lambda > 0$, non-decreasing in $\lambda$. It is uniform-scale if increasing the scale by $\varepsilon$ swells every region by a closed ball of a radius $\delta(\varepsilon)$ that does not depend on the region, and uniformly continuous with respect to $P_X$ if changing the scale by $\delta(\varepsilon)$ changes the probability of every region by at most $\varepsilon$.

A family $\{(\mathcal C, f_m)\}_{m \in \mathbb N}$ is arbitrarily precise if, for every $\varepsilon > 0$, all methods far enough along the family eventually (almost surely, as $n$ grows) output regions of diameter at most $\varepsilon$. A method is uniformly positive with respect to a reference measure $\mu$ if its regions have $\mu$-measure bounded below, and has asymptotically-bounded cardinality if it eventually outputs at most $u$ regions. When $P_X$ has a density $g_X$ with respect to $\mu$, the RRS density estimate at $x$ averages $\hat P_{X,n}(A)/\mu(A)$ over the chosen regions $A$ that contain $x$:

$$\hat g_n(x; f) = \frac{1}{|c_n(x; f)|} \sum_{A \in c_n(x; f)} \frac{\hat P_{X,n}(A)}{\mu(A)}, \qquad c_n(x; f) = \{A \in f(S_n) : x \in A\},$$

and $\hat g_n(x; f) = 0$ when no chosen region covers $x$.

Formalization targets

Goal: Theorem 6.5 (p. 28)

If the support $K$ of $P_X$ is compact with $P_X(K) = 1$, $g_X$ is continuous, some closed neighbourhood of $K$ has finite $\mu$-measure, and $\{f_m\}$ is an arbitrarily precise family over a uniform-scale class that is uniformly continuous with respect to $P_X$, with each $f_m$ sample-covering, sample-intersecting, of asymptotically-bounded cardinality and uniformly positive, then almost surely

$$\lim_{m \to \infty} \limsup_{n \to \infty} \int_M \bigl|g_X - \hat g_n(\cdot\,; f_m)\bigr| \, d\mu = 0.$$

Milestones

1. Theorem 6.1 (p. 22): such a class is Glivenko–Cantelli, $\sup_{A \in \mathcal C} |\hat P_{X,n}(A) - P_X(A)| \to 0$ a.s.
2. Corollary 6.1 (p. 24): the same supremum over the chosen regions $A \in f(S_n)$.
3. Lemma 6.1 (p. 24): for a sample-covering method and compact $K$ inside the support, $\sup_{x \in K} d(x, C_n(f)) \to 0$ a.s.
4. Theorem 6.2 (p. 24): with asymptotically-bounded cardinality, $P_X(K \setminus C_n(f)) \to 0$ a.s.
5. Corollary 6.2 (p. 25): $P_X(C_n(f)) \to 1$ a.s.
6. Theorem 6.4 (p. 26): $\lim_m \limsup_n \sup_{x \in C_n(f_m)} |g_X(x) - \hat g_n(x; f_m)| = 0$ a.s.

Significance

The goal shows that one estimator, defined uniformly from any RRS method, is $L^1$-consistent under conditions that are checked once for the class of regions and once for the method. Histograms, density estimation trees, and the paper's own minimum-dominating-set and $k$-center summaries (Corollaries 7.1 and 7.2) all become consistent density estimators as soon as they satisfy those conditions. Theorem 6.1 is of independent interest: it is a Glivenko–Cantelli theorem whose hypotheses are geometric and measure-theoretic rather than combinatorial, applying to classes for which no finite VC dimension is known.

The results are proved on paper; none is machine-checked. The mission produces a formal layer for region-based empirical processes (RRS methods, uniform-scale classes, the region-average density estimate) and machine-checked versions of the convergence chain. The formal statements also repair two places where the printed hypotheses are too weak (see Formalization scope), so a completed development certifies corrected theorems, not merely transcribed ones.

Difficulty

The regions an RRS method selects depend on the sample, so the law of large numbers cannot be applied region by region: there are uncountably many candidate regions and no fixed finite family to which the strong law applies. The uniform convergence of Theorem 6.1 must instead come from a finite approximation of the whole class, combining compactness of the support with the uniform-scale and uniform-continuity hypotheses, and the approximation has to work at every scale, including scales smaller than the approximation step. The goal adds a second limit: the error splits into a part on the coverage region, governed by the uniform estimate of Theorem 6.4, and a part on the uncovered portion of the support where the estimate is zero, governed by Corollary 6.2. The two limits ($n \to \infty$ inside, $m \to \infty$ outside) and the almost-sure quantifier must be interleaved correctly, with countably many null sets collected over $m$.

Formalization scope

All statements live in the namespace RepRegion.Density, with one definitions file RepRegion.Density.Model. $M$ is a metric space with an arbitrary σ-algebra in which every closed ball is measurable (no Borel assumption); $\Omega$ is a probability space; the observations are X : ℕ → Ω → M, measurable, mutually independent (iIndepFun) and identically distributed, indexed from $0$. $P_X$ is P.map (X 0). The reference measure $\mu$ is an arbitrary measure on $M$. Regions are Set M, a method is Finset M → Finset (Set M), and the scale map is R : Θ → ℝ → Set M, read only at positive scales.

Committed conventions:

• the empirical measure counts observations with multiplicity; the paper's $|T \cap S_n|/n$ with $S_n$ a set would fail for laws with atoms;
• the terms $R(\theta, \lambda - \varepsilon)$ and $R(\theta, \lambda - \delta)$ of the uniform-scale and uniform-continuity definitions are read as $\emptyset$ when the scale is not positive. In particular, regions of scale at most $\delta(\varepsilon)$ must have probability at most $\varepsilon$; without this, Theorem 6.1 fails (a counterexample on $[0, 1]$ is recorded in its statement);
• suprema, limits superior and integrals of errors are taken in $[0, \infty]$; the integrated error is a lower Lebesgue integral, never a Bochner integral;
• diameters are stated pairwise ($d(x, y) \le L$), and probabilities of regions are compared with addition rather than truncated subtraction;
• the regions the methods output have finite $\mu$-measure, so that $\hat g$ is defined; the paper never states this;
• the goal's printed conclusion "$= \varepsilon$" (with $\varepsilon$ unbound) is stated as "$= 0$", as its proof and the paper's corollaries establish;
• the goal assumes $g_X$ continuous on $M$ (the paper: on $K$), the hypothesis of Theorem 6.4 that its proof invokes; Theorem 6.4 is stated with $g_X$ uniformly continuous, because with mere continuity it fails for reference measures that do not charge every open set.

A formalization in which the error is a Bochner integral, a supremum is a real sSup, or a diameter is Metric.diam would make the conclusions hold for junk reasons on non-integrable or unbounded inputs; those encodings are ruled out.

A complete development needs the strong law of large numbers for indicators (in Mathlib), finite nets of compact metric sets, and almost-sure hitting arguments for balls of positive probability. The region-based Glivenko–Cantelli theorem and the coverage results are reusable for any later mission on partition-based estimators. Proofs of the individual milestones, alternative arguments, and a version of the goal under continuity of $g_X$ on $K$ alone are all welcome.

Selected references

• A. S. Estes, M. O. Ball, D. J. Lovell, Data Exploration by Representative Region Selection: Axioms and Convergence, Mathematics of Operations Research, 2021. SSRN preprint 3005997: https://ssrn.com/abstract=3005997 ; journal version: https://doi.org/10.1287/moor.2020.1115
• G. R. Shorack, J. A. Wellner, Empirical Processes with Applications to Statistics, SIAM Classics in Applied Mathematics, 2009. https://doi.org/10.1137/1.9780898719017
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, in Empirical Inference, Springer, 2013 (English translation of the 1968/1971 work). https://doi.org/10.1007/978-3-642-41136-6_3

Motivation

Schur–Weyl duality says that on the tensor power $V^{\otimes N}$ of the natural representation of $\mathfrak{gl}_m(\mathbb C)$, the symmetric group $\Sigma_N$ acting by place permutations generates the full commutant of $\mathfrak{gl}_m$. It is the bridge between representations of general linear groups and of symmetric groups. Two extensions matter in representation theory and in the theory of tensor categories:

• Super Schur–Weyl duality. Replacing $\mathfrak{gl}_m$ by the general linear Lie superalgebra $\mathfrak{gl}_{m|n}(\mathbb C)$ and inserting Koszul signs, $\Sigma_N$ still generates the commutant of $V^{\otimes N}$ (Sergeev 1985; Berele and Regev 1987). The kernel is now governed by $(m,n)$-hook partitions.
• Mixed tensor space. On $V^{\otimes r} \otimes W^{\otimes s}$ with $W = V^*$, the symmetric group must be replaced by the walled Brauer algebra $B_{r,s}(\delta)$ of Turaev and Koike, which has diagrams with strands that may turn back.

Brundan and Stroppel (arXiv:1107.0999) prove the combination: mixed Schur–Weyl duality for $\mathfrak{gl}_{m|n}(\mathbb C)$. It is the first step towards their main result, a Morita equivalence between $B_{r,s}(\delta)$ and an idempotent truncation of Khovanov's generalized arc algebra $K(\delta)$, from which they derive that $B_{r,s}(\delta)$ is Koszul for $\delta \neq 0$. Comes and Wilson obtained the same duality independently (arXiv:1108.0652); Shader and Moon had a partial result earlier (Commun. Algebra 30, 2002).

Timeline:

• 1937: Brauer introduces the Brauer algebra for orthogonal and symplectic groups.
• 1985, 1987: Sergeev, and Berele–Regev, prove super Schur–Weyl duality for $\mathfrak{gl}_{m|n}$ on $V^{\otimes N}$.
• 1989–1994: Turaev and Koike introduce the walled Brauer algebra; Benkart et al. prove mixed duality for $\mathfrak{gl}_m$.
• 2011: Brundan–Stroppel (Theorem 7.8) and Comes–Wilson prove mixed duality for $\mathfrak{gl}_{m|n}$.

Setting

Fix integers $m, n \ge 0$ and put $\delta = m - n$. Let $I = \{1, \dots, m+n\}$, with parity $|i| = 0$ for $i \le m$ and $|i| = 1$ for $i > m$. Let $V$ have basis $v_1, \dots, v_{m+n}$ with $v_i$ of parity $|i|$, and $W = V^*$ the dual basis $w_1, \dots, w_{m+n}$. The Lie superalgebra $\mathfrak g = \mathfrak{gl}_{m|n}(\mathbb C)$ is $\operatorname{End}(V)$, spanned by matrix units $e_{a,b}$ of parity $|a| + |b|$, acting by

$$e_{a,b} v_k = \delta_{b,k} v_a, \qquad e_{a,b} w_k = -\delta_{a,k} (-1)^{(|a|+|b|)|a|} w_b .$$

It acts on $V^{\otimes r} \otimes W^{\otimes s}$, with basis $v_{\mathbf i^{\mathrm L}} \otimes w_{\mathbf i^{\mathrm R}}$ for $\mathbf i \in I^{r+s}$, through $\Delta(x) = x \otimes 1 + 1 \otimes x$ and the sign rule $(a \otimes b)(c \otimes d) = (-1)^{|b||c|} ac \otimes bd$. The super-commutant $\operatorname{End}_{\mathfrak g}(V^{\otimes r} \otimes W^{\otimes s})$ is the space of all linear maps $f$, not necessarily homogeneous, annihilated by the action $(xf)(u) = x(f(u)) - (-1)^{|x||f|} f(xu)$ of every $x \in \mathfrak g$.

A walled Brauer diagram pairs the $2(r+s)$ vertices on the top and bottom edges of a rectangle, with a wall after position $r$: a vertical strand joins vertices on the same side of the wall and a horizontal strand joins vertices on opposite sides. These diagrams are a basis of $B_{r,s}(\delta)$; the product $\sigma\tau$ puts $\sigma$ under $\tau$ and multiplies by $\delta^t$ for $t$ removed circles. Colouring the bottom vertices by $\mathbf i$ and the top vertices by $\mathbf j$, the weight $\mathrm{wt}({}_{\mathbf i}\sigma_{\mathbf j})$ is $0$ unless every strand has equally coloured ends, and otherwise $(-1)$ raised to the sum of $|k||l|$ over the crossings of strands of colours $k, l$ plus $|k|$ over the bottom horizontal strands of colour $k$ (7.5). The right action

$$(v_{\mathbf i^{\mathrm L}} \otimes w_{\mathbf i^{\mathrm R}}) \cdot \sigma = \sum_{\mathbf j} \mathrm{wt}({}_{\mathbf i}\sigma_{\mathbf j})\, v_{\mathbf j^{\mathrm L}} \otimes w_{\mathbf j^{\mathrm R}}$$

defines $\Psi^{m,n}_{r,s} : B_{r,s}(\delta) \to \operatorname{End}_{\mathfrak g}(V^{\otimes r} \otimes W^{\otimes s})^{\mathrm{op}}$ (7.12). For $s = 0$ the permutation diagrams give $\Phi^{m,n}_{N} : \mathbb C\Sigma_N \to \operatorname{End}_{\mathfrak g}(V^{\otimes N})^{\mathrm{op}}$ (7.11).

Formalization targets

Goal: Theorem 7.8 (p. 56)

For all $m, n, r, s \ge 0$,

$$\operatorname{im} \Psi^{m,n}_{r,s} = \operatorname{End}_{\mathfrak g}(V^{\otimes r} \otimes W^{\otimes s}), \qquad \Psi^{m,n}_{r,s} \text{ injective} \iff r + s < (m+1)(n+1).$$

Milestones, in attack order

• Lemma 7.1: $\Omega = \sum_{i,j} (-1)^{|j|} e_{i,j} \otimes e_{j,i}$ on $M \otimes N$, $M, N \in \{V, W\}$.
• Lemma 7.3: (7.6) is a right $\mathbb C\Sigma_N$-action on $V^{\otimes N}$; $(a\ b)$ acts as $\Omega_{a,b}$; the action lies in $\operatorname{End}_{\mathfrak g}$.
• Lemma 7.4: (7.7) is a right $B_{r,s}(\delta)$-action, $\Psi(\tau)\Psi(\sigma) = \delta^t \Psi(\pi)$; the signed transpositions act as $\Omega_{a,b}$; the action lies in $\operatorname{End}_{\mathfrak g}$.
• (2.1)–(2.2): $\mathrm{flip}_{r,s}$ is a bijection from $\Sigma_{r+s}$ to the walled diagrams, so $\dim B_{r,s}(\delta) = (r+s)!$.
• Theorem 7.5 (Sergeev, Berele–Regev): $\Phi^{m,n}_N$ maps onto $\operatorname{End}_{\mathfrak g}(V^{\otimes N})$, injectively iff $N < (m+1)(n+1)$.
• Lemma 7.6, as its instance (7.16): $\mathrm{flip}_{r,s} : \operatorname{End}(V^{\otimes(r+s)}) \to \operatorname{End}(V^{\otimes r} \otimes W^{\otimes s})$, $f \otimes g \mapsto f \otimes g^*$, is a $\mathfrak g$-isomorphism.
• Lemma 7.7: $\mathrm{flip}_{r,s} \circ \Phi^{m,n}_{r+s} = \Psi^{m,n}_{r,s} \circ \mathrm{flip}_{r,s}$.

Significance

Theorem 7.8 identifies $B_{r,s}(m-n)/\ker \Psi^{m,n}_{r,s}$ with the full super-commutant of mixed tensor space. Brundan and Stroppel use this to compare $B_{r,s}(\delta)$ with a graded algebra built from Khovanov's arc algebra (Corollary 8.2, Theorem 8.10), which yields a grading on $B_{r,s}(\delta)$, its Koszulity for $\delta \neq 0$, and descriptions of the indecomposable summands of $V^{\otimes r} \otimes W^{\otimes s}$. The injectivity range $r + s < (m+1)(n+1)$ says exactly when the walled Brauer algebra is faithfully realized on tensor space.

All statements are proved in the literature; none has a machine-checked proof that we are aware of. A complete formalization would need classical and super Schur–Weyl duality (Theorem 7.5 is the deep input, proved in the paper only by citation), the weight calculus of diagrams, and the sign bookkeeping of Lemma 7.7, which the authors call tricky.

Difficulty

Surjectivity onto a commutant is a double-centralizer statement, and the obvious route through semisimplicity fails: for $m, n > 0$ the tensor space $V^{\otimes N}$ is in general not semisimple as a $\mathfrak g$-supermodule. Theorem 7.5 instead rests on Berele and Regev's analysis of hook Young diagrams. Mixed tensor space adds a second obstacle: $W$ enters with signs both in its $\mathfrak g$-action and in the dualities $W^{\otimes s} \cong (V^{\otimes s})^*$, and the reduction to $V^{\otimes(r+s)}$ via $\mathrm{flip}_{r,s}$ works only when every sign convention (crossings, bottom caps, the sign rule, the dual map) is matched exactly.

Formalization scope

• Colours and positions are 0-based: colours are Fin (m + n), odd iff $\ge m$. A tensor space is given by a slot pattern Fin N → Bool (true = $V$); operators are complex matrices indexed by Fin N → Fin (m + n), with column = input basis vector.
• The $\mathfrak g$-action is the explicit iterated coproduct with Koszul signs; $\operatorname{End}_{\mathfrak g}$ is the joint kernel of the action of all matrix units $e_{a,b}$ on $\operatorname{End}$, with both the even and odd parts and the sign $(-1)^{|x||f|}$.
• Diagrams are fixed-point-free involutions of Fin N ⊕ Fin N (Sum.inl = top), reusing the published WalledBrauer.Blocks.WalledDiagram, its composition comp and its loop count loops. Crossings are counted by interleaving of endpoints along the boundary, which is the crossing set of a reduced drawing; Lemma 7.2 (isotopy invariance) is thereby absorbed.
• $\mathbb C\Sigma_N$ and $B_{r,s}(\delta)$ enter as vector spaces with their diagram bases; surjectivity and injectivity of (7.11) and (7.12) are properties of these linear maps. $\delta = m - n \in \mathbb C$.
• $\mathrm{flip}_{r,s}$ on endomorphisms is given in coordinates, derived from (7.13), (7.15) and (7.18).
• No restriction $m + n > 0$ or $r + s > 0$ is made: for $m = n = 0$ and $r + s > 0$ the space is zero and $\Psi$ is not injective, as the criterion predicts.

The following would trivialize or falsify the statement and are ruled out: a commutant of $\mathfrak{gl}_m \oplus \mathfrak{gl}_n$ only, or one that drops the odd part or the signs; an unsigned slotwise action; a range statement with only one inclusion; an injectivity statement with only one direction. Not formalized: the paper's general Lemma 7.6 for arbitrary supermodules (no supermodule category in Mathlib), and everything involving $K(\delta)$. Contributions of a reusable Lie-superalgebra tensor layer and of Berele–Regev's hook-partition theory are welcome.

Selected references

• J. Brundan, C. Stroppel, Gradings on walled Brauer algebras and Khovanov's arc algebra, Adv. Math. 231 (2012); arXiv:1107.0999v1. https://arxiv.org/abs/1107.0999
• A. Berele, A. Regev, Hook Young diagrams with applications to combinatorics and to representations of Lie superalgebras, Adv. Math. 64 (1987) 118–175. https://doi.org/10.1016/0001-8708(87)90007-7
• A. N. Sergeev, The tensor algebra of the identity representation as a module over the Lie superalgebras gl(n,m) and Q(n), Math. USSR Sbornik 51 (1985) 419–427. https://doi.org/10.1070/SM1985v051n02ABEH002867
• J. Comes, B. Wilson, Deligne's category Rep(GL_δ) and representations of general linear supergroups, Represent. Theory 16 (2012); arXiv:1108.0652. https://arxiv.org/abs/1108.0652
• G. Benkart, M. Chakrabarti, T. Halverson, R. Leduc, C. Lee, J. Stroomer, Tensor product representations of general linear groups and their connections with Brauer algebras, J. Algebra 166 (1994) 529–567. https://doi.org/10.1006/jabr.1994.1166