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 2.3.1Gauge equivalence

Two tensors $A$ and $B$ of the same bond dimension $D$ are gauge equivalent if there exists an invertible matrix $X \in \mathrm{GL}_D(\mathbb {C})$ such that, for every $i \in \{ 0,\ldots ,d{-}1\} $,

\begin{align} B^i & = X A^i X^{-1}. \label{eq:mps_gauge_equiv} \end{align}

In tensor-network notation, (5) is represented by

$\begin{tenkz}[boundary=open] \tn[skin=ring]{X} & \tn[ports={90:physical:$i$}]{A} & \tn[skin=ring]{X^{-1}} \end{tenkz}$

where the black node denotes the tensor $A$, the upper leg is the physical index $i$, and the two red side nodes denote the gauge matrices acting on the virtual legs.

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 8.1.1.1Irreducible tensor

An MPS tensor $A$ is irreducible if it has no nontrivial invariant projection.

LaTeX Lean

Definition 5.4.1Left-canonical normalization

An MPS tensor $A=(A^i)_i$ is left-canonical when

\begin{align} \sum _i (A^i)^\dagger A^i & =\mathbb {1}. \notag \end{align}

Equivalently, its Kraus map is trace-preserving.

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

Lemma A.1.1Square-root trace-preserving gauge is a gauge equivalence

If $\sigma $ is positive definite and $B$ is defined by (1), then $A$ and $B$ are gauge equivalent.

LaTeX Lean

Theorem 4.1.2Injectivity implies irreducibility

If $A$ is an injective MPS tensor, then its transfer map $\mathcal{E}_A$ is irreducible.

LaTeX Lean

Theorem 5.4.2Left-canonical (trace-preserving) gauge

Let $\sigma $ be a fixed point of the adjoint transfer map $\sum _i (A^i)^\dagger \sigma A^i = \sigma $, and let $S$ be invertible with $S^\dagger S = \sigma $. Define $A'^i = SA^iS^{-1}$. Then $\sum _i (A'^i)^\dagger A'^i = \mathbb {1}$, i.e. the gauged Kraus map is trace-preserving. This is the left-canonical normalization.

LaTeX

Lean

Kraus.gauged_isTP_of_map_conjTranspose_fixedPoint
gauged_tracePreserving

Theorem 5.5.2Positive-definite adjoint eigenvector for irreducible tensors

Let $A$ be an irreducible MPS tensor with $D {\gt} 0$ and some $A^i \neq 0$. Then there exist a positive definite matrix $\sigma $ and a positive real $r {\gt} 0$ such that $\mathcal{E}_A^\dagger (\sigma ) = r\sigma $.

This combines the eigenvector-existence part of [ Wol12 , Theorem 6.5 ] with the irreducible upgrade to positive definiteness ( [ Wol12 , Theorem 6.3(2)–(3) ] ); the application to the adjoint transfer map follows [ CPGSV16 , Appendix A ] .

LaTeX Lean

Theorem 5.3.1Existence of PSD fixed point

Assume $D \ge 1$. Let $A$ be an MPS tensor with $\sum _i (A^i)^\dagger A^i = \mathbb {1}$, so that $\mathcal{E}_A$ is trace-preserving. Then there exists $\rho \ge 0$, $\rho \neq 0$, with $\mathcal{E}_A(\rho ) = \rho $.

LaTeX Lean

Theorem 5.1.2PSD fixed point is positive definite

Let $A$ be an injective MPS tensor and let $\rho \ge 0$, $\rho \neq 0$, be a fixed point of $\mathcal{E}_A$. Then $\rho $ is positive definite.

LaTeX Lean

Theorem 5.2.2Uniqueness of PSD fixed point

Let $A$ be an injective MPS tensor. If $\rho ,\sigma \geq 0$ are nonzero fixed points of $\mathcal{E}_A$, then $\sigma =c\rho $ for some $c\in \mathbb {C}$.

LaTeX Lean

Theorem 5.2.1Irreducible fixed-point uniqueness

Let $A$ be an MPS tensor whose transfer map is irreducible. If $\rho ,\sigma \geq 0$ are fixed points of $\mathcal{E}_A$ and $\rho \neq 0$, then $\sigma =c\rho $ for some $c\in \mathbb {C}$.

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 5.3.3Quantum Perron–Frobenius for irreducible transfer maps

Assume $D\ge 1$. Let $A$ be an MPS tensor such that its transfer map is irreducible and $\sum _i (A^i)^\dagger A^i=\mathbb {1}$, so that $\mathcal{E}_A$ is trace-preserving. Then $\mathcal{E}_A$ has a unique positive definite fixed point, up to scalar multiple.

LaTeX Lean

Theorem 5.5.3TP-gauge existence for irreducible tensors

Let $A$ be an irreducible MPS tensor with $D {\gt} 0$ and some $A^i \neq 0$. Then there exist a positive real $r$, a positive definite matrix $\sigma $, and a tensor $B$ gauge-equivalent to $r^{-1/2}A$ such that

\begin{align} B^i & = \sigma ^{1/2}(r^{-1/2}A^i)\sigma ^{-1/2}, \label{eq:qpf_irred_tp_gauge} \end{align}

and $\sum _i (B^i)^\dagger B^i = \mathbb {1}$.

This is the “spectral rescaling $+$ TP gauge” step of [ CPGSV16 , Appendix A ] . The similarity is generally non-unitary.

LaTeX Lean

Theorem 5.4.4Square-root trace-preserving gauge from an adjoint eigenvector

Let $\sigma $ be positive definite and satisfy $\sum _i (A^i)^\dagger \sigma A^i = r\sigma $ for $r{\gt}0$. Define

\begin{align} B^i & = \sigma ^{1/2}(r^{-1/2}A^i)\sigma ^{-1/2}. \label{eq:qpf_tp_gauge_eigenvector} \end{align}

Then $B$ is trace-preserving: $\sum _i (B^i)^\dagger B^i = \mathbb {1}$.

LaTeX Lean

Theorem 5.4.3Square-root trace-preserving gauge from an adjoint fixed point

Let $\sigma $ be positive definite and satisfy $\sum _i (A^i)^\dagger \sigma A^i = \sigma $. Define

\begin{align} B^i & = \sigma ^{1/2}A^i\sigma ^{-1/2}. \label{eq:qpf_tp_gauge} \end{align}

Then $B$ is trace-preserving: $\sum _i (B^i)^\dagger B^i = \mathbb {1}$.

LaTeX Lean

Theorem 4.2.6Transfer map is a channel

If $\sum _i(A^i)^\dagger A^i=\mathbb {1}$, then the transfer map $\mathcal{E}_A(X)=\sum _i A^iX(A^i)^\dagger $ is a quantum channel (CPTP).

LaTeX Lean

Theorem 4.2.1Transfer map is CP

The transfer map $\mathcal{E}_A(X)=\sum _i A^iX(A^i)^\dagger $ is completely positive.

LaTeX Lean

Theorem 5.5.1Irreducibility of the transfer map of an irreducible tensor

If an MPS tensor $A$ is irreducible, then its transfer map $\mathcal{E}_A$ is irreducible.

LaTeX Lean

Theorem 5.1.1Transfer-map PSD fixed point — irreducible version

Let $A$ be an MPS tensor whose transfer map $\mathcal{E}_A$ is irreducible. If $\rho \geq 0$, $\rho \neq 0$, and $\mathcal{E}_A(\rho )=\rho $, then $\rho $ is positive definite.

LaTeX Lean

Theorem 5.5.4Unital-gauge existence for irreducible tensors

Let $A$ be an irreducible MPS tensor with $D {\gt} 0$ and some $A^i \neq 0$. Then there exist a positive real $r$, a positive definite matrix $\rho $, and a tensor $B$ gauge-equivalent to $r^{-1/2}A$ such that

\begin{align} B^i & = r^{-1/2}\rho ^{-1/2}A^i\rho ^{1/2}, \label{eq:qpf_irred_unital_gauge} \end{align}

and $\sum _i B^i(B^i)^\dagger = \mathbb {1}$.

This is the Perron–Frobenius unital-gauge orientation used in [ PGVWC07 , Theorem 4, lines 765–770 ] , stated for one irreducible nonzero block.

LaTeX Lean

Theorem 8.8.2Unital gauge from a full-rank Perron–Frobenius eigenvector

Let $\rho $ be positive definite with $\mathcal{E}_A(\rho )=r\rho $ for some $r{\gt}0$. For $B^i:=r^{-1/2}\rho ^{-1/2}A^i\rho ^{1/2}$,

\begin{align} \sum _i B^i(B^i)^\dagger & =\mathbb {1}. \label{eq:canon_unital_gauge_identity} \end{align}

If $r=1$, then the unscaled gauge $B^i:=\rho ^{-1/2}A^i\rho ^{1/2}$ is unital and generates the same MPV family as $A$. This is the spectral-radius normalization and full-rank fixed-point gauge of [ PGVWC07 , Theorem 4 ] .

LaTeX

Lean

Kraus.spectralUnitalGauge_isUnital_of_map_eigenvector
Kraus.unitalGauge_isUnital_of_map_fixedPoint
MPSTensor.sameMPV_unitalGauge