Dependency graph

Legend

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

Definition 15.1.3Auxiliary-space connected correlator

The connected two-point function is

\begin{align} C(X,Y;n) & = \langle X_0Y_n\rangle - \langle X_0\rangle \langle Y_0\rangle . \notag \end{align}

LaTeX Lean

Definition 15.2.4Correlation length

For every $\lambda _2\in \mathbb {C}$, define the associated correlation-length quantity by

\begin{align} \xi & = -\frac{1}{\log |\lambda _2|}. \notag \end{align}

For a nonzero subleading eigenvalue in the physical range $0{\lt}|\lambda _2|{\lt}1$, this quantity is positive. If all subleading spectral values vanish and correlations therefore vanish after finitely many transfer steps, the total definition gives the limiting value $\xi =0$.

LaTeX Lean

Definition 15.1.4Fixed-point-centered auxiliary insertion

For a matrix $\rho \in M_{D}(\mathbb {C})$ and an auxiliary insertion $X\in M_{D}(\mathbb {C})$, define

\begin{align} Z_\rho (X) & = X\rho -\operatorname{tr}(X\rho )\rho . \label{eq:correlator_traceless_part} \end{align}

When $\operatorname{tr}(\rho )=1$, this removes the trace component of $X\rho $.

LaTeX Lean

Definition 2.4.1Injectivity

A tensor $A$ is injective if its matrices span the full matrix algebra: $\operatorname{span}_{\mathbb {C}}\{ A^i : i = 0,\ldots ,d{-}1\} = M_{D}(\mathbb {C})$.

LaTeX Lean

Definition 15.1.1Auxiliary-space one-point functional

Fix an MPS tensor and a right fixed point of its transfer map. Write the tensor as $A$ and the fixed point as $\rho ^R$. Under the hypotheses of Theorem 5.3.2, that fixed point exists and is unique up to scaling; we normalize it so that $\operatorname{tr}(\rho ^R)=1$. For an auxiliary-space insertion $X\in M_{D}(\mathbb {C})$, define

\begin{align} \langle X_0 \rangle & = \operatorname{tr}(X\rho ^R). \notag \end{align}

LaTeX Lean

Definition 2.1.8Transfer map

The transfer map associated to a tensor $A$ is the linear map $\mathcal{E}_A : M_{D}(\mathbb {C}) \to M_{D}(\mathbb {C})$ defined by

\begin{align} \mathcal{E}_A(X) & = \sum _{i=0}^{d-1} A^i X (A^i)^\dagger . \label{eq:mps_transfer_map} \end{align}

Diagrammatically, the transfer map is the double-layer contraction

$\begin{tenkz}[rows={ket,bra}, cols=1, west=open, east={cup=$X$}] \tn[label pos=n]{A} \\ \tn[label pos=s, conjugate]{\overline{A}} \end{tenkz}$

in which the upper node denotes $A$, the lower node denotes $A^\dagger $, and the physical index is summed over between them.

LaTeX Lean

Definition 15.1.2Auxiliary-space two-point functional at distance $n$

For auxiliary-space insertions $X,Y\in M_{D}(\mathbb {C})$ and $n\ge 0$, define

\begin{align} \langle X_0 Y_n \rangle & = \operatorname{tr}\! \left(Y\, \mathcal{E}_A^n(X\rho ^R)\right). \notag \end{align}

Equivalently, insert $X$ at site $0$, propagate by $\mathcal{E}_A^n$, then insert $Y$ and take the trace.

$\begin{tenkz}[rows={wire,wire}, cols=3, west={cup=$Y$}, east={cup=$X\rho^R$}] \tn[at=(1,2), skin=ring, wires=2]{\E_A^n} \end{tenkz}$

LaTeX Lean

Lemma 15.2.5Correlation length is positive

If $|\lambda _2| {\lt} 1$ and $\lambda _2 \ne 0$, then $\xi {\gt} 0$.

LaTeX Lean

Lemma 15.1.5Trace of the centered insertion

If $\operatorname{tr}(\rho )=1$, then

\begin{align} \operatorname{tr}\! \bigl(Z_\rho (X)\bigr) & =0. \end{align}

LaTeX Lean

Theorem 15.1.6Fixed-point centering identity for connected correlators

Suppose that $\rho $ is a right fixed point of the transfer map, $\mathcal{E}_A(\rho )=\rho $. Then, for every $n\geq 0$,

\begin{align} C(X,Y;n) & =\operatorname{tr}\! \left(Y\, \mathcal{E}_A^n\bigl(Z_\rho (X)\bigr)\right). \label{eq:connected_correlator_traceless_reduction} \end{align}

When moreover $\operatorname{tr}(\rho )=1$, the preceding lemma shows that $Z_\rho (X)$ is traceless. The identity isolates the fixed-point contribution before the remaining transfer iterates are analysed.

LaTeX Lean

Theorem 15.3.2Correlation length bound

For an injective trace-preserving MPS tensor, there exist $C{\gt}0$ and $\xi {\gt}0$ such that, for all $n\ge 0$ and all traceless $X\in M_{D}(\mathbb {C})$, i.e. $\operatorname{tr}(X)=0$,

\begin{align} \| \mathcal{E}_A^n(X)\| & \le C e^{-n/\xi }\| X\| . \label{eq:correlations_traceless_decay} \end{align}

Traceless matrices lie in $\ker P$, where $P$ is the fixed-point projection (8). Since $\mathcal{E}_A-P$ has spectral radius strictly less than $1$, choose any $r$ with $\rho (\mathcal{E}_A-P){\lt}r{\lt}1$. The Gelfand formula then gives exponential decay with $\xi =-1/\log r$. Choosing a rate strictly above the spectral radius is necessary in general because a Jordan block at the spectral radius can prevent a uniform bound proportional to $\rho (\mathcal{E}_A-P)^n$.

LaTeX Lean

Theorem 15.2.2Exponential decay bound (interface)

If a constant $C_{XY}\in \mathbb {R}$ and $\lambda _2\in \mathbb {C}$ satisfy, for all $n\ge 0$,

\begin{align} |C(X,Y;n)| & \le C_{XY}\, |\lambda _2|^n, \label{eq:correlations_decay_bound} \end{align}

then the connected correlator satisfies that exponential decay bound. The source [ CPGSV21 , Section II.B.3 ] obtains this by combining the sum-of-exponentials expansion with the triangle inequality, while under the primitive or injective hypotheses stated in Chapter 6, the transfer-map gap results ensure that the subleading eigenvalues lie strictly inside the unit disk.

LaTeX Lean

Theorem 15.2.1Sum of exponentials (spectral expansion interface)

If coefficients $c_j\in \mathbb {C}$ and eigenvalues $\lambda _j\in \mathbb {C}$, for $j=1,\ldots ,D^2-1$, satisfy, for all $n\ge 0$,

\begin{align} C(X,Y;n) & = \sum _{j=1}^{D^2-1} c_j\, \lambda _j^n, \label{eq:correlations_spectral_expansion} \end{align}

then the connected correlator equals the stated sum of exponentials. The source [ CPGSV21 , Section II.B.3 ] states that the connected correlator is a sum of $D^2-1$ pure exponentials, $C(X,Y;n)=\sum _{j\ge 2}^{D^2}c_{XY}(j)\lambda _j^n$. This pure-exponential representation follows when the relevant subleading spectral data of the transfer map are diagonalizable. For a non-diagonalizable transfer map, nontrivial Jordan blocks can instead produce terms of the form $n^k\lambda ^n$. Accordingly, the pure-exponential formula is retained here as an explicit interface hypothesis rather than asserted for every normal MPS.

LaTeX Lean

Theorem 15.3.1Exponential convergence of injective primitive channels

Fix an injective, trace-preserving MPS tensor $A$ with positive definite fixed point $\rho $. Let

\begin{align} P(X) & = \frac{\operatorname{tr}(X)}{\operatorname{tr}(\rho )}\rho \label{eq:correlations_fixed_point_projection} \end{align}

be the corresponding fixed-point projection. Then there exist $C {\gt} 0$ and $0 {\lt} \delta \le 1$ such that, for all $n\ge 0$ and $X\in M_{D}(\mathbb {C})$,

\begin{align} \| \mathcal{E}_A^n(X)-P(X)\| & \le C(1-\delta )^n\| X\| . \label{eq:correlations_channel_convergence} \end{align}

The transfer-map gap $\delta $ exists by primitivity (the corresponding theorem in the companion quantum-channel volume [ LTC26 , “Complementary transfer-map gap for primitive maps” ] , the complementary transfer-map gap).

LaTeX Lean

Theorem 6.10.2Self-overlap convergence from a complementary transfer-map gap

Let $A$ be a normalized MPS tensor with a nonzero PSD fixed point $\rho $ of the transfer map. If $\rho _{\operatorname{spec}}(\mathcal{E}_A-P){\lt}1$, where $P$ is the fixed-point projection, then $O_{AA}(N)\to 1$ as $N\to \infty $.

LaTeX Lean

Theorem 5.3.2Quantum Perron–Frobenius

Assume $D \ge 1$. Let $A$ be an injective MPS tensor with $\sum _i (A^i)^\dagger A^i = \mathbb {1}$. Then the transfer map $\mathcal{E}_A$ has a unique positive semidefinite fixed point $\rho $ up to scaling, and $\rho $ is positive definite.

LaTeX Lean

Theorem 15.3.3Transfer-map gap from injectivity

For an injective trace-preserving MPS tensor, there exists $\delta {\gt}0$ such that every eigenvalue $\mu \ne 1$ of the transfer map satisfies $|\mu |\le 1-\delta $.

LaTeX Lean

Theorem 6.3.6Strict transfer-operator gap

Let $A$ and $B$ be injective normalized MPS tensors that are not gauge-phase equivalent. Then $\rho _{\operatorname{spec}}(F_{AB}){\lt}1$.

LaTeX Lean