- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
For a Hermitian matrix \(\rho \in M_{D}(\mathbb {C})\) with eigenvalues \(\lambda _0,\ldots ,\lambda _{D-1}\), the von Neumann entropy is
where \(0\log 0:=0\).
Let \(K_j\) be invertible filters on nested regions \(D_j\), each commuting with the regional state of the unit vector \(\varphi \) and clipped relative to it with weight \(a_j\le \tfrac 12\). Let \(X\) be Hermitian, supported on \(S\), with \(\lVert X\rVert \le c_0\), and suppose that at most one region meets \(S\) without containing it. Then conjugation by the nested product \(K\) changes \(\Re \langle \varphi ,X\varphi \rangle \) by at most \(\sum _{j}4a_j^2d_S^2c_0\), the sum over the regions splitting \(S\).
For \(\varepsilon ,\lambda {\gt}0\), \(a\ge 0\) and positive \(p_i,p_k\), the numbers \(l_i=\max \{ \varepsilon ,p_i/\lambda \} ^{a/2}\) satisfy \(|\log (l_i/l_k)|\le \frac a2|\log (p_i/p_k)|\). If \(a\le 1/2\), \(p,q{\gt}0\) and \(|t|\le \frac a2|\log (p/q)|\), then \(\sqrt{pq}\, (\cosh t-1)\le 2a^2(p+q)\).
Let \(K=U\operatorname {diag}(x^{a/2})U^*\) with \(x\ge f{\gt}0\), \(\sum x=1\), maximize the output norm among the filters \(U\operatorname {diag}(y^{a/2})U^*\) with \(y\ge f\), \(\sum y=1\), and let the regional state of the output be \(U\operatorname {diag}(q)U^*\). Then \(q_k/x_k\le q_i/x_i\) whenever \(x_i{\gt}f\). If moreover \(\# \cdot f{\lt}1\), then \(x_i=\max \{ f,q_i/\lambda \} \) for some \(\lambda {\gt}0\), hence \(|\log (x_i/x_k)^{a/2}|\le \frac a2|\log (q_i/q_k)|\) for positive \(q_i,q_k\).
Let the marginal of \(\Theta \) be \(\operatorname {diag}(s)\) with \(\sum s=1\), let \(X=\sum _\alpha c_\alpha \otimes d_\alpha \) be Hermitian, and let \(L= \operatorname {diag}(l)\) with \(l{\gt}0\) and \(|\log (l_j/l_k)|\le \frac a2|\log (s_j/s_k)|\) for positive \(s_j,s_k\), where \(a\le 1/2\). Then \(|\operatorname {Re}(\langle \Theta ,X\Theta \rangle -\langle \Theta ,(L\otimes 1) X(L^{-1}\otimes 1)\Theta \rangle )|\le 4a^2\sum _\alpha \lVert c_\alpha \rVert \lVert d_\alpha \rVert \).
If the marginal of a unit vector is \(U\operatorname {diag}(q)U^*\) and \(L=U\operatorname {diag}(l)U^*\) has clipped eigenvalue ratios with \(a\le 1/2\), then conjugating a Hermitian \(X=\sum c_\alpha \otimes d_\alpha \) by \(L\otimes 1\) changes the real part of its expectation by at most \(4a^2\sum \lVert c_\alpha \rVert \lVert d_\alpha \rVert \). Operators supported on disjoint regions commute.
Let \(L\ge 0\) act on \(\mathcal H_B\) with \(\operatorname{Tr}L^{2/a}=1\), \(0{\lt}a{\lt}1\). For a unit vector with marginal \(\rho \), \(\lVert (L\otimes 1)\Psi \rVert ^2=\operatorname{Tr}\rho L^2\le (\operatorname{Tr}\rho ^{1/(1-a)})^{1-a}=M(-a/(1-a))^{1-a}\). Under the hypotheses of Theorem 21.3.2, if \(a\le 1/2\) and \(a/(1-a)\le 1/(32\sqrt{(1+\vartheta )\mathcal B})\), then \(\lVert (L\otimes 1)\Psi \rVert ^2\le \exp (-aS(\rho )+1024\mathrm e\vartheta \mathcal Ba^2)\).
Let \(K{\gt}0\) on a region \(D\) maximize or minimize \(\lVert A(K\otimes 1)Cw\rVert \) over its unitary orbit, where \(A\) is a product of invertible filters on regions containing \(D\), each commuting with the regional state of the output \(\psi =A(K\otimes 1)Cw\) on its region. Then \(K\) commutes with \(\rho _{\psi ,D}\).
- Entropy.re_inner_commutator_eq_zero_of_isLocalMax
- Entropy.isHermitian_of_re_trace_mul_skew_eq_zero
- Entropy.commute_of_isHermitian_inv_mul_mul
- Entropy.inner_liftProd_conj
- Entropy.commute_regionState_of_unitary_max
- Entropy.re_inner_commutator_eq_zero_of_isLocalExtr
- Entropy.commute_regionState_of_unitary_extr
- Entropy.commute_regionState_of_unitary_min
The lift \(K\mapsto K\otimes 1\) from a region \(D\) is a unital multiplicative map compatible with adjoints, and its range is the set of operators supported on \(D\). The regional pure-state matrix is Hermitian. Support is monotone in \(D\) and closed under products. For every vector \(\varphi \), \(\langle \varphi ,(K\otimes 1)\varphi \rangle = \operatorname{Tr}\rho _{\varphi ,D}K\). Consequently, if \(K\) is invertible and commutes with \(\rho _{\varphi ,D}\), then \(\langle \varphi ,(K\otimes 1)Y(K^{-1}\otimes 1)\varphi \rangle =\langle \varphi , Y\varphi \rangle \) for every \(Y\) supported on \(D\).
- Entropy.localLift
- Entropy.regionState
- Entropy.regionState_isHermitian
- Entropy.localLift_mul
- Entropy.localLift_one
- Entropy.localLift_conjTranspose
- Entropy.isSupportedOn_localLift
- Entropy.IsSupportedOn.exists_localLift
- Entropy.IsSupportedOn.mono
- Entropy.IsSupportedOn.mul
- Entropy.inner_localLift
- Entropy.inner_localLift_conj_eq
- Entropy.inner_conj_eq_of_isSupportedOn
Suppose the marginal of the ground vector \(\Psi \) is \(\operatorname {diag}(p)\). The vector \(\Theta =F\Psi /\sqrt{M(u)}\), \(F=\operatorname {diag}(p^{-u/2})\) on the support, is a unit vector with marginal proportional to \(p^{1-u}\) and \(\langle \Psi ,\Theta \rangle =M(u/2)/\sqrt{M(u)}\). At \(z_u=-u/(2(1-u))\) its modular function is \(\langle F^2\Psi ,X\Psi \rangle /M(u)\), and one-sided terms have constant modular function. For \(|u|\le 1/2\) and \(|u|\le 1/(8\log (\mathrm ed_i))\) at every crossing term, \(\langle \Theta ,(\mathsf H-E_0)\Theta \rangle \le 128\mathrm ec_0\mathcal Bu^2\), and the gap gives \((1-128\mathrm e\vartheta \mathcal Bu^2)M(u)\le M(u/2)^2\).
One has \(f(0)=\langle \Theta ,X\Theta \rangle \) and \(|f(\mathrm iy)|\le \lVert X\rVert \), and \(f(-x)=\overline{f(x)}\) for Hermitian \(X\). For \(X=c\otimes d\) and \(|\operatorname {Re}z|\le 1/2\), \(|f(z)|\le 2\lVert c\rVert \lVert d\rVert \). Consequently, if \(X\) is Hermitian, \(\lVert X\rVert \le c_0\) and \(X\) is a sum of \(N\) products with \(\lVert c_\alpha \rVert \lVert d_\alpha \rVert \le c_0\), then \(|\operatorname {Re}(f(x)-f(0))|\le 128\mathrm ec_0\ell ^2x^2\) whenever \(\ell \ge 1\), \(\log (2N)\le 2\ell \) and \(|x|\le 1/(8\ell )\).
Let \(e_L:H_L\to H_L'\) and \(e_R:H_R\to H_R'\) be bijections, and write \(Z^{e_L\otimes e_R}\) for the corresponding simultaneous relabelling of the rows and columns of \(Z\). Then
For \(0\le a\le 1\) and \(y\in \mathbb {R}\),
If \(p,q\ge 0\), \(a\le 1\), and \(|t|\le \frac a2|\log p-\log q|\) whenever \(p,q{\gt}0\), then
Suppose the physical configuration space is nonempty. An operator \(X\) supported on \(S\) has a product decomposition across \(B\sqcup B^c\) with at most \(d_{S\cap B}^2\) terms, each of product norm at most \(\lVert X\rVert \), where \(d_{S\cap B}=\prod _{v\in S\cap B}n_v\).
Let \(\psi =L_k\cdots L_0\Omega \) with \(L_k\) Hermitian, suppose the normalization of \(\psi \) has overlap at least \(s\) with \(\Omega \), and \(\lVert L_{k-1}\cdots L_0\Omega \rVert \le N\). Then \(s\lVert \psi \rVert \le \lVert L_k\Omega \rVert N\).
Under the hypotheses of Theorem 21.3.2 for the cut \(B\mid B^c\), a feasible filter \(L\) on \(B\) with positive floor and weight \(0{\lt}a\le \tfrac 12\), such that \(a/(1-a)\) is admissible for the cut, satisfies \(\lVert L\Psi \rVert ^2\le \exp \bigl(-aS(\rho _{\Psi ,B})+1024e\vartheta \mathcal B_Ba^2\bigr)\).
Let \(\varphi \) be a unit vector, \(B\) a region, and let \(L=W\operatorname {diag}(l)W^*\) and \(\rho _{\varphi ,B}=W\operatorname {diag}(q)W^*\) with \(W\) unitary, \(l{\gt}0\), and \(\lvert \log l_i-\log l_k\rvert \le \tfrac a2\lvert \log q_i-\log q_k\rvert \) for positive \(q_i,q_k\), where \(a\le \tfrac 12\). For a Hermitian operator \(X\) supported on \(S\) with \(\lVert X\rVert \le c_0\),
Let \(f\) be entire with \(f(-x)=\overline{f(x)}\) for real \(x\), \(|f(\mathrm iy)|\le c\) for real \(y\), and \(|f(z)|\le cm\) for \(|\operatorname {Re}z|\le 1/4\), where \(m\ge 1\). If \(\ell \ge 1\) and \(\log m\le 2\ell \), then \(|f(z)|\le \mathrm ec\) for \(|\operatorname {Re}z|\le 1/(8\ell )\), and \(|\operatorname {Re}(f(x)-f(0))|\le 128\mathrm ec\ell ^2x^2\) for real \(|x|\le 1/(8\ell )\).
Let \(h\) be supported on \(D\) and let \(B\sqcup B^c=V\). If \(D\subseteq B\) or \(D\subseteq B^c\), then \(h\) acts on one factor of \(\mathcal H_B\otimes \mathcal H_{B^c}\). In general \(h\) is a sum of at most \(d^2\) products \(c_\alpha \otimes d_\alpha \) with \(\lVert c_\alpha \rVert \le 1\) and \(\lVert d_\alpha \rVert \le \lVert h\rVert \), where \(d=\prod _{v\in D}n_v\).
The function \(L=\log M\) satisfies \(L(0)=0\) and \(L'(0)=S\). If \(K_0\ge 0\), \(K_0u^2\le 1/2\) and \((1-K_0u^2)M(u)\le M(u/2)^2\) for all \(|u|\le r\), then \(L(u)\le uS+4K_0u^2\) for \(|u|\le r\). If \(L(\pm r)\le \pm rS+Cr^2\) with \(r{\gt}0\), then \(\Pr \{ |K-S|{\gt}w\} \le 2\mathrm e^{Cr^2}\mathrm e^{-rw}\).
For positive semidefinite \(A,B\) with eigenvalues \(a_i,b_j\) and \(1/p+1/q=1\), \(p,q{\gt}1\), \(\operatorname {Re}\operatorname{Tr}(AB)\le (\sum _ia_i^p)^{1/p}(\sum _jb_j^q)^{1/q}\).
Let \(\rho _{\Omega ,X}=U\operatorname {diag}(p)U^*\) and let \(P_i\) be the projection onto the \(i\)-th eigenvector \(u_i\). Then \(\lVert P_i\Omega \rVert ^2=p_i\), and on every region \(T\) disjoint from \(X\) the regional state of \(\Omega \) is the sum of those of the vectors \(P_i\Omega \). For regions \(T_j\) disjoint from \(X\) and filters \(M_j\) on \(T_j\), the filters \(P_i\otimes M_j\) on \(X\cup T_j\) are nonnegative with \(\operatorname {Tr}(P_i\otimes M_j)^{2/a}=\operatorname {Tr}M_j^{2/a}\), and \(\lVert M_{m-1}\cdots M_0P_i\Omega \rVert \le \lVert (P_i\otimes M_{m-1})\cdots (P_i\otimes M_0)\Omega \rVert \).
- Entropy.localLift_apply
- Entropy.regionUnionEquiv
- Entropy.localLift_union_kronecker
- Entropy.isFeasibleFilter_union_kronecker
- Entropy.pinProj
- Entropy.pinProj_conjTranspose
- Entropy.pinProj_mul_self
- Entropy.sum_pinProj
- Entropy.eq_of_forall_trace_mul_eq
- Entropy.norm_toEuclideanLin_sq
- Entropy.norm_sq_localLift_pinProj
- Entropy.inner_localLift_eq_sum_pinProj
- Entropy.regionState_eq_sum_pinProj
- Entropy.mul_prod_map_mul_of_idempotent
- Entropy.mul_prod_eq_prod_mul
- Entropy.norm_toEuclideanLin_le_of_proj
- Entropy.norm_liftProd_trial_ge
Let \(E\) be the set of indices with \(p_i{\gt}0\) and \(|-\log p_i-S|\le w\), and let \(z=\sum _{i\in E}p_i\). Then \(z\ge 1-\Pr \{ |K-S|{\gt}w\} \), and \(\mathrm e^{-S-w}\le p_i\le \mathrm e^{-S+w}\) for \(i\in E\).
Suppose every region \(D_j\) carries at least one configuration and \(\# \cdot f_j\le 1\). Then the norm \(\lVert L_{m-1}\cdots L_0\Omega \rVert \) attains its maximum over families of feasible filters. If moreover all floors are positive and \(\Omega \ne 0\), every such product maps \(\Omega \) to a nonzero vector.
A filter on \(D\) is feasible at floor \(f{\gt}0\) and weight \(a{\gt}0\) when it is \(U\operatorname {diag}(y^{a/2})U^*\) with \(U\) unitary, \(y\ge f\) and \(\sum y=1\). Let a feasible filter \(K\) maximize the output norm of \(A(K\otimes 1)Cw\) among feasible filters, where \(A\) is a product of filters on regions containing \(D\), each commuting with its regional state of the output \(\psi \ne 0\), and let \(\# \cdot f{\lt}1\). Then \(K\) commutes with \(\rho _{\psi ,D}\), and in a common eigenbasis \(K=W\operatorname {diag}(l)W^*\), \(\rho _{\psi ,D}=W\operatorname {diag}(q)W^*\) with \(|\log (l_i/l_k)|\le \frac a2|\log (q_i/q_k)|\) for positive \(q_i,q_k\).
Under the hypotheses of Theorem 21.5.20 with \(E{\lt}\Delta \), and bounds \(\lVert L\Omega \rVert \le x_k\) for filters on \(D_k\) feasible at any positive floor, every family of \(m\) nonnegative filters \(L_j=U_j\operatorname {diag}(y_j^{a_j/2})U_j^*\) with \(y_j\ge 0\) and \(\sum y_j=1\) satisfies \(\sqrt{1-E/\Delta }^{\, m}\lVert L_{m-1}\cdots L_0\Omega \rVert \le \prod _{k{\lt}m}x_k\).
Let feasible filters \(K_j\) on nested regions \(D_0\subseteq \dots \subseteq D_{m-1}\) maximize \(\lVert L_{m-1}\cdots L_0\Omega \rVert \) over the product of the feasible sets, with nonzero output \(\psi \) and \(\# \cdot f_j{\lt}1\). Then for every \(j\), \(K_j\) commutes with \(\rho _{\psi ,D_j}\), and in a common eigenbasis its eigenvalue ratios are clipped.
Let \(X\) be a region, \(T_0\subseteq T_1\subseteq \cdots \) regions disjoint from \(X\), and \(D_j=X\cup T_j\), with weights \(0{\lt}a_j\le \tfrac 12\) of total mass \(\sum _{j{\lt}m}a_j=2\). Let \(\Omega \), \(H\) and \(\Delta \) be as in Theorem 21.5.20 for the regions \(D_j\), with energy budget at most \(E{\lt}\Delta \), and suppose every \(a_j/(1-a_j)\) is admissible for the cut \(D_j\). If every \(T_j\) lies in a region \(T\) disjoint from \(X\), then
Let feasible filters \(K_j\) on nested regions \(D_j\), with floors \(f_j{\gt}0\), \(\# \cdot f_j{\lt}1\) and weights \(0{\lt}a_j\le \tfrac 12\), maximize \(\lVert L_{m-1}\cdots L_0\Omega \rVert \), where \(\Omega \ne 0\) satisfies \(H\Omega =E_0\Omega \) for \(H=\sum _ih_i\) with \(h_i\) Hermitian, supported on \(S_i\), \(\lVert h_i\rVert \le c_0\), and every \(S_i\) split by at most one region. Then the normalized output \(\varphi =K\Omega /\lVert K\Omega \rVert \) satisfies
Let \(\rho \) be a Hermitian matrix indexed by a finite set \(J\), and let \(e : I \to J\) be a bijection from a finite set \(I\). The reindexed matrix on \(I\) with entries \(\rho _{e(i)\, e(j)}\) has the same von Neumann entropy as \(\rho \).
Let \(M_j=W_j\operatorname {diag}(l_j)W_j^*\) with \(l_j{\gt}0\) be filters on nested regions \(T_j\), let \(\xi \) be a unit vector, and suppose that every nested product of unitary conjugates \(V_j^*M_jV_j\), with \(V_j\) unitary on \(T_j\), has output norm at most \(B{\gt}0\) on \(\xi \). Then \(\lVert M_{k-1}^x\cdots M_0^x\xi \rVert \le B^x\) for \(0\le x\le 1\), and \(\sum _{j{\lt}k}\Re \langle \xi ,\log M_j\, \xi \rangle \le \log B\).
- Entropy.specPow
- Entropy.specPow_zero
- Entropy.specPow_one
- Entropy.specPow_add
- Entropy.specPow_conjTranspose
- Entropy.specPow_conjTranspose_mul_self
- Entropy.hasDerivAt_specPow
- Entropy.differentiable_specPow
- Entropy.norm_specPow_le
- Entropy.localLift_injective
- Entropy.localLiftCLM
- Entropy.chainPow
- Entropy.chainPow_zero_length
- Entropy.chainPow_succ
- Entropy.chainPow_zero
- Entropy.chainPow_conjTranspose_mul_self
- Entropy.chainPow_mul_conjTranspose_self
- Entropy.differentiable_chainPow
- Entropy.norm_chainPow_le
- Entropy.hasDerivAt_chainPow_zero
- Entropy.chainPow_eq_liftProd
- Entropy.chainPow_one_add
- Entropy.applyCLM
- Entropy.norm_toEuclideanLin_chainPow_le_rpow
- Entropy.sum_re_inner_log_le
Let \(N_k\) be the largest output norm \(\lVert L_{k-1}\cdots L_0\Omega \rVert \) over feasible filters on the first \(k\) nested regions, where the floors are positive with \(\# \cdot f_j{\lt}1\) and \(0{\lt}a_j\le \tfrac 12\). Let \(\Omega \) be a unit vector with \(H\Omega =E_0\Omega \) and \(H-E_0\ge \Delta (1-\lvert \Omega \rangle \langle \Omega \rvert )\), where \(\Delta {\gt}0\) and \(H=\sum _ih_i\) with \(h_i\) Hermitian, supported on \(S_i\), \(\lVert h_i\rVert \le c_0\), and every \(S_i\) split by at most one region. If \(\sum _{j{\lt}m}4a_j^2\sum _{i\text{ crossing }D_j}d_{S_i}^2c_0\le E\) and every feasible filter on \(D_k\) has \(\lVert L\Omega \rVert \le x_k\), then
Let \(\mathsf H=\sum _ih_i\) on \(\mathcal H_B\otimes \mathcal H_{B^c}\) with Hermitian terms, \(\lVert h_i\rVert \le c_0\), \(c_0\ge 0\), each term acting on one factor except the crossing terms \(i\in \mathcal I_\times \), each a sum of at most \(d_i^2\) products with factor norms at most \(c_0\), \(d_i\ge 1\). Let \(\Psi \) be a unit vector with \(\mathsf H\Psi =E_0\Psi \) and \(\mathsf H-E_0\ge g_0(1-|\Psi \rangle \langle \Psi |)\), \(g_0{\gt}0\). Let \(\rho \) be its marginal on \(\mathcal H_B\), \(p\) the eigenvalues of \(\rho \), \(S=S(\rho )\), \(\mathcal B=1+\sum _{i\in \mathcal I_\times }\log ^2(\mathrm ed_i)\) and \(\vartheta =c_0/g_0\). Then \(\log \mathbb E\, \mathrm e^{uK}\le uS+512\mathrm e\vartheta \mathcal Bu^2\) for \(|u|\le 1/(32\sqrt{(1+\vartheta )\mathcal B})\), and for every real \(w\)
Let \(\mathsf H=\sum _{i\in \mathcal I}h_i\) on \(\mathcal H\) with \(\mathcal I\) finite, each \(h_i\) Hermitian with \(\lVert h_i\rVert \le c_0\), \(c_0\ge 0\), and supported on a designated set \(D_i\). Let \(\Psi \) be a unit vector with \(\mathsf H\Psi =E_0\Psi \) and \(\mathsf H-E_0\ge g_0(1-|\Psi \rangle \langle \Psi |)\), \(g_0{\gt}0\). Fix \(B\sqcup B^c=V\), let \(\mathcal I_\times \) be the indices whose support meets both sides, \(\rho =\operatorname{Tr}_{B^c}|\Psi \rangle \langle \Psi |\), \(d_i=\prod _{v\in D_i}n_v\), \(\mathcal B=1+\sum _{i\in \mathcal I_\times }\log ^2(\mathrm ed_i)\) and \(\vartheta =c_0/g_0\). Then the conclusions of Theorem 21.3.2 hold: \(\log \mathbb E\, \mathrm e^{uK}\le uS+512\mathrm e\vartheta \mathcal Bu^2\) for \(|u|\le 1/(32\sqrt{(1+\vartheta )\mathcal B})\), and the stated tail bound holds for every real \(w\).
Let \(K_j\) be invertible filters on nested regions \(D_j\). Each filter commutes with the regional marginal of the same unit vector \(\phi \) and satisfies the common-basis and clipping hypotheses above, with weight \(a_j\le 1\). Suppose the support \(S\) of a Hermitian operator \(X\) is split by at most one region, and \(\lVert X\rVert \le J\). Writing \(K=K_{m-1}\cdots K_0\) for the lifted product,
In particular, an interaction with one inside endpoint of dimension \(q\) has one-term cost at most \(q^2Ja_j^2\).
Let \(\phi \) be a unit vector. Suppose the positive invertible filter \(L\) and its marginal have a common orthonormal eigenbasis, with eigenvalues \(l_i{\gt}0\) and \(p_i\ge 0\). Assume \(a\le 1\) and \(|\log l_i-\log l_k|\le \frac a2|\log p_i-\log p_k|\) whenever \(p_i,p_k{\gt}0\). For a Hermitian product sum \(X=\sum _\alpha c_\alpha \otimes d_\alpha \),
If \(X\) is supported on \(S\) and \(\lVert X\rVert \le J\), the expectation difference is at most \(a^2d_{S\cap B}^2J\), by choosing the inside-support matrix-unit decomposition.
Under the hypotheses of Theorem 21.5.1.4, let \(H=\sum _i h_i\), where each \(h_i\) is Hermitian, supported on \(S_i\), has norm at most \(J\), and is split by at most one region. If \(KHK^{-1}\phi =E_0\phi \), then
For pairwise disjoint regions \(A,B,C\), \(S(A\cup B\cup C)+S(B)\le S(A\cup B)+S(B\cup C)\). In particular \(S(X\mid T)\le S(X\mid T')\) for \(T'\subseteq T\) disjoint from \(X\).
- Entropy.regionEntropy
- Entropy.trace_regionState_submatrix_mul
- Entropy.disjoint_union_of_disjoint
- Entropy.tripleEquiv
- Entropy.tripleEquiv_apply
- Entropy.localLift_tripleEquiv_kronecker_one
- Entropy.regionState_posSemidef
- Entropy.tripleState
- Entropy.partialTraceLeft_tripleState
- Entropy.partialTraceRight_regionState_union
- Entropy.partialTraceRight_reassoc_tripleState
- Entropy.regionEntropy_ssa
- Entropy.regionEntropy_cond_anti
Let \(V,V'\) be finite sets of sites, let \(e:V\to V'\) be a bijection, and let \(n_v,n'_{v'}\) be nonnegative integer local dimensions. Write \(E_v=\{ i\in \mathbb N:i{\lt}n_v\} \) and \(E'_{v'}=\{ i\in \mathbb N:i{\lt}n'_{v'}\} \) for the local bases. Suppose that \(f_v:E_v\to E'_{e(v)}\) is a bijection for each \(v\in V\). These bijections induce a configuration bijection \(f\) and, for \(D\subseteq V\) and \(D'=e(D)\), a regional configuration bijection \(f_D\). Write \(T\Omega (\sigma ')=\Omega (f^{-1}(\sigma '))\) for the transported vector and \(U_D\) for the permutation isometry induced by \(f_D\). Then \(\rho _{T\Omega ,D'}=U_D\rho _{\Omega ,D}U_D^*\). No normalization assumption is required.