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

Theorem 1.4.10Example: First moment of Pauli-Z operator

Consider \(O = \sigma _{z}\), the Pauli-Z operator. We show that

\begin{equation} \mathbb {E}_{U \sim \mu _{2}} [U\sigma _{z}U^{\dagger }] = \frac{\text{Tr}(\sigma _{z})}{2} I. \end{equation}

LaTeX

Theorem 1.4.13Commutant of first order unitaries is a scalar multiple of the identity

Given the identity \(\mathbb {I} \in \mathcal{U}(2)\),

\begin{equation} \{ M : M U = U M, \forall U \in \mathcal{U}(2) \} = \{ \lambda \mathbb {I} : \lambda \in \mathbb {C} \} . \end{equation}

LaTeX

Theorem 1.4.15Using Schur-Weyl Duality for Commutants

Given the identity \(\mathbb {I} \in \mathcal{U}(2)\),

\begin{equation} \{ M : M U = U M, \forall U \in \mathcal{U}(2) \} = \{ \lambda \mathbb {I} : \lambda \in \mathbb {C} \} . \end{equation}

We prove this statement now using the abstract Schur-Weyl duality.

LaTeX

Theorem 1.4.16

Consider the set of \(\mathcal{U}(2)^{\otimes k}\) defined over \(\mathbb {C}\). We show that

\begin{equation} \{ M : M U^{\otimes k} = U^{\otimes k} M, \forall U \in \mathcal{U}(2) \} = \text{Span}\{ V_{d}(\pi ) : \pi \in S_{2} \} . \end{equation}

LaTeX

Definition 1.1.3Diagonal operators

An operator \(X \in \mathcal{L}(\mathcal{X})\) is a diagonal operator if \(X_{a, b} = 0\) for all \(a, b \in [d]\) where \(a \neq b\). For a given vector \(u \in \mathcal{X}\), we can define a diagonal operator \(\text{Diag}(u) \in \mathcal{L}(\mathcal{X})\) to denote the diagonal operator whose diagonal entries are given by the entries of \(u\). That is, we have

\begin{equation} \text{Diag}(u)_{a, b} = \begin{cases} u_a & \text{if } a = b \\ 0 & \text{if } a \neq b \end{cases} \end{equation}

LaTeX

Definition 1.4.1Group average

Let \(G\) be a group of order \(N\) and \(R\) a representation of the group. Define the group average to be

\begin{equation} \langle X \rangle _{G} = \frac{1}{N} \sum _{g} R(g) X R(g)^{\dagger }. \end{equation}

LaTeX

Definition 1.2.4Operator-vector correspondence

The operator-vector correspondence is a bijective mapping between the set of linear operators \(\mathcal{L}(\mathcal{X})\) and the tensor product space \(\mathcal{X} \otimes \mathcal{X}\) defined as

\begin{equation} \text{vec} : \mathcal{L}(\mathcal{X}) \to \mathcal{X} \otimes \mathcal{X}, \quad E_{i, j} \mapsto |i\rangle \otimes |j\rangle \text{ for all } i, j \in [d]. \end{equation}

One relevant identity we use is that for \(A_0, A_1, B \in \mathcal{L}(\mathcal{X})\),

\begin{equation} \label{eq:OperatorVectorDistribution} (A_0 \otimes A_1) \text{vec}(B) = \text{vec}(A_0 B A_1^{\mathrm{T}}). \end{equation}

LaTeX

Definition 1.4.8Parameterized single-qubit Haar measure

Let \(\mu _{2}\) denote the Haar measure on a single qubit, represented with vectors in \(\mathbb {C}^{2}\). Define the single-qubit Haar measure in terms of the parameters given in Remark 1.4.7, where

\begin{equation} d\mu _{2} = \sin {\theta } d\theta \cdot d\omega \cdot d\phi \end{equation}

is the unnormalized Haar measure. The normalized computation of moments using the Haar measure is given by

\begin{equation} \label{eq:NormalizedHaarMeas} \mathbb {E}_{U \sim \mu _{2}} [U O U^{\dagger }] = \frac{1}{8\pi ^2} \int _{\phi = 0}^{2\pi } \int _{\omega = 0}^{2\pi } \int _{\theta = 0}^{\pi } U O U^{\dagger } \sin {\theta } d\theta d\omega d\phi , \end{equation}

where the factor of \(\frac{1}{8\pi ^2}\) can be found by computing the integral and setting \(UOU^{\dagger } =1\).

LaTeX

Definition 1.2.3Standard computational basis of linear operators

The standard computational basis of linear operators \(\{ E_{i, j}\} _{i, j \in [d]}\) is defined as the set of \(d^2\) operators in \(\mathcal{L}(\mathcal{X})\) such that

\begin{equation} E_{i, j} = |i \rangle \langle j| \end{equation}

for all \(i, j \in [d]\), where \(\{ |i\rangle \} _{i \in [d]}\) is the standard computational basis of \(\mathcal{X}\).

LaTeX

Definition 1.2.1Symmetric subspace of linear operators

The symmetric subspace of linear operators \(\mathcal{L}(\mathcal{X})^{\mathbin {\bigcirc \mkern -15mu\vee }k}\) is the set of all operators \(X \in \mathcal{L}(\mathcal{X}^{\otimes k})\) that remain unchanged (invariant) under the permutation \(W_{\pi }\). That is,

\begin{equation} \label{eq:SymmetricLinearOperator} \mathcal{L}(\mathcal{X})^{\mathbin {\bigcirc \mkern -15mu\vee }k} = \{ X \in \mathcal{L}(\mathcal{X}^{\otimes k}) : X = W_{\pi } X W_{\pi }^{*} \text{ for all } \pi \in S_{k} \} . \end{equation}

LaTeX

Lemma 1.3.4Invariant subspace lemma

Let \(\mathcal{X}\) be a complex Euclidean space, let \(\mathcal{V} \subseteq \mathcal{X}\) be a subspace, and let \(A \in \mathcal{L}(\mathcal{X})\) be an operator. The following statements are equivalent:

It holds that both \(A\mathcal{V} \subseteq \mathcal{V}\) and \(A^{*}\mathcal{V} \subseteq \mathcal{V}\).
It holds that \([A, \Pi _{\mathcal{V}}] = 0\).

LaTeX

Lemma 1.4.14Span of 1D permutations is the span of \(\mathbb {I}\)

Let \(d \in \mathbb {N}\) and \(k = 1\). Then

\begin{equation} \text{Span}\{ V_{d}(\pi ) : \pi \in S_{k} \} = \text{Span}(\mathbb {I}). \end{equation}

LaTeX

Proposition 1.4.12

Let \(v, w \in \mathbb {C}^2\) be unit vectors (i.e., \(|v| = |w| = 1\)). Then there exists a unitary matrix \(U \in U(2)\) such that \(Uv = w\).

LaTeX

Proposition 1.3.2Symmetric subspace and span of tensor product space

Let \(\mathcal{X}\) be a complex Euclidean space and \(k\) be a positive integer. Then the following statements are equivalent:

\(X \in \mathcal{L}(\mathcal{X})^{\mathbin {\bigcirc \mkern -15mu\vee }k}\).
For \(V \in U(\mathcal{X}^{\otimes k} \otimes \mathcal{X}^{\otimes k}, (\mathcal{X} \otimes \mathcal{X})^{\otimes k})\) being the isometry defined by

\begin{equation} V \text{vec}(Y_1 \otimes \dots \otimes Y_k) = \text{vec}(Y_1) \otimes \dots \text{vec}(Y_n) \end{equation}
14

holding for all \(Y_1, \dots , Y_k \in \mathcal{L}(\mathcal{X})\), one has that

\begin{equation} V \text{vec}(X) \in (\mathcal{X} \otimes \mathcal{X})^{\mathbin {\bigcirc \mkern -15mu\vee }k}. \end{equation}
15
\(X \in \text{Span}\{ Y^{\otimes k} : Y \in \mathcal{L}(\mathcal{X})\} \)

LaTeX

Definition 1.4.4Bloch vectors

For any single-qubit quantum state \(\rho \), we can write it in terms of its Bloch vector,

\begin{equation} \rho = \frac{1}{2} (I + r \cdot \sigma ), \end{equation}

where \(r = (r_x, r_y, r_z) \in \mathbb {R}^3\) is the coordinate of the quantum state on the Bloch sphere and \(\sigma = (\sigma _x, \sigma _y, \sigma _z)\) is a three-tuple of the Pauli operators.

LaTeX Lean

Theorem 1.3.5Double Commutant Theorem

Let \(\mathcal{A}\) be a self-adjoint, unital subalgebra of \(\mathcal{L}(\mathcal{X})\). Then the double commutant of \(\mathcal{A}\) is equal to \(\mathcal{A}\), i.e.,

\begin{equation} \text{Comm}(\text{Comm}(\mathcal{A})) = \mathcal{A}. \end{equation}

LaTeX

Theorem 1.3.3Equivalence of symmetric subspace and unitary tensor span

Let \(\mathcal{X}\) be a complex Euclidean space and \(k\) be a positive integer. Then the symmetric subspace of linear operators is equivalent to the span of the unitary tensor products, i.e.,

\begin{equation} \mathcal{L}(\mathcal{X})^{\mathbin {\bigcirc \mkern -15mu\vee }k} = \text{Span}\{ U^{\otimes k} : U \in \mathcal{U}(\mathcal{X})\} . \end{equation}

LaTeX

Theorem 1.3.6Schur-Weyl duality

Let \(\mathcal{X}\) be a complex Euclidean space, \(k\) be a positive integer, and \(X \in \mathcal{L}(\mathcal{X}^{\otimes k})\) be an operator. Then the set of all commutators of the unitary group is equivalent to the span of the permutation operators, i.e.,

\begin{equation} \text{Comm}(\mathcal{U}(\mathcal{X}), k) = \text{Span}\{ W_{\pi } : \pi \in S_k \} \end{equation}

LaTeX

Theorem 1.3.1Tensor power span theorem

Let \(k\) be a positive integer, and let \(X \in \mathbb {C}^[d]\). For any set \(\mathcal{A} \subseteq \mathbb {C}\) satisfying \(|\mathcal{A}| \geq k + 1\), it holds that

\begin{equation} \text{Span}\{ v^{\otimes k} : v \in \mathcal{A}^{[d]}\} =\mathcal{X}^{\mathbin {\bigcirc \mkern -15mu\vee }k}. \end{equation}

LaTeX

Theorem 1.4.6Pauli twirling of a single qubit

For an arbitrary single-qubit state \(\rho \),

\begin{equation} \langle \rho \rangle _{G} = \frac{1}{N} \sum _{g} R(g) X R(g)^{\dagger } = \frac{I}{2}, \end{equation}

the maximally mixed state (since it is proportional to the identity matrix).

LaTeX Lean