Angle between column types, row types and a global signed type on a punctured rectangle

This is the angle estimate between prescribed column types, prescribed row types and a prescribed global signed type on a rectangle with marked cells removed.

Throughout, $S_p$ acts on the word space $W_p=\ell^2\big((C\sqcup C)^p\big)$, with $C=\{1,\dots,q\}$ two-coloured into even and odd letters, by the signed action $(\rho(g)f)(w)=\varepsilon(g,w)\,f(w\circ g)$, where $\varepsilon(g,w)$ is the sign of the permutation $g$ induces between the odd positions of $w$. For $u+v=p$ and partitions $\alpha\vdash u$, $\beta\vdash v$, the operator $P_{\alpha,\beta}$ is the sum, over the placements of $u$ even sites among the $p$ sites, of the tensor product of the orthogonal projections onto the $S^\alpha$-isotypic part of the $u$ even sites and the $S^\beta$-isotypic part of the $v$ odd sites. Its entropy is $F(\alpha,\beta)=\sum_{a\in\alpha\cup\beta}a\log\frac{u+v}{a}$, and a local type on $k$ sites is such a pair of total size $k$. For an enumeration $e$ of the $p$ sites by blocks $j\in J$ with $k_j$ sites each and local types $t=(t_j)_j$, $P^{e}_{t}$ is the corresponding tensor product of local type projections, with $F(t)=\sum_jF(t_j)$. For a coefficient function $f:G\to\mathbb{C}$ on a finite group and a representation $\pi$, $\pi(f)=\sum_gf(g)\pi(g)$.

Let $A,B$ be finite with $B$ nonempty, let $e:\{1,\dots,n\}\to A\times B$ be a bijection, and let $p+l=n$. Fix an injection $z$ of $l$ marks into the $n$ positions, and let $x\mapsto\iota(x)$ enumerate the remaining $p$ positions. Let $e_H$ enumerate these $p$ sites by column, with $k^H_j\le s$ sites in column $j\in B$, and let $e_K$ enumerate them by row, with $k^K_i\le m$ sites in row $i\in A$, compatibly with $e$ and $\iota$. Let $H=(H_j)$ and $K=(K_i)$ be local types on these blocks. Let $u+v=p$ with $\alpha\vdash u$, $\beta\vdash v$ having at most $q\ge1$ rows, and let $R\ge\max(s,m)+1$. Then

The estimate converts the entropies of line types into the global entropy; the removed cells cost only the factor $e^l$, with no assumption on their arrangement.

Formalization Note The norm is the operator norm on $W_p$. The upstream statement is reproduced verbatim from BlockAngle.lean.