LeanPool.SingleCopyStabilizer.CNOTAction

Arbitrary-qubit simultaneous CNOT action and its exact Pauli covariance. The basis permutation is x ↦ x - xᵢ w, with wᵢ=0; over F₂ this is the product of CNOTs controlled by i and targeted at the support of w.

source

def LeanPool.SingleCopyStabilizer.CNOTAction.basisShear {ι : Type u_1} (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) :

Measurement.Bits ι ≃ₗ[ZMod 2] Measurement.Bits ι

The invertible coordinate shear underlying simultaneous controlled-NOT gates.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def LeanPool.SingleCopyStabilizer.CNOTAction.applyCNOTs {ι : Type u_1} (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) (ψ : Measurement.Amplitude ι) :

Measurement.Amplitude ι

Pull amplitudes back along the inverse controlled shear.

Equations

LeanPool.SingleCopyStabilizer.CNOTAction.applyCNOTs i w hw ψ x = ψ ((LeanPool.SingleCopyStabilizer.CNOTAction.basisShear i w hw).symm x)

Instances For

source

theorem LeanPool.SingleCopyStabilizer.CNOTAction.norm_preserved {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) (ψ : Measurement.Amplitude ι) :

∑ x : Measurement.Bits ι, Measurement.bornWeight (applyCNOTs i w hw ψ) x = ∑ x : Measurement.Bits ι, Measurement.bornWeight ψ x

source

theorem LeanPool.SingleCopyStabilizer.CNOTAction.normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) (ψ : Measurement.Amplitude ι) (hψ : Measurement.IsNormalized ψ) :

Measurement.IsNormalized (applyCNOTs i w hw ψ)

source

theorem LeanPool.SingleCopyStabilizer.CNOTAction.inverse_pairing {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) (v x : Measurement.Bits ι) :

shearZ i w v ⬝ᵥ x = v ⬝ᵥ (basisShear i w hw).symm x

source

theorem LeanPool.SingleCopyStabilizer.CNOTAction.pauli_covariance {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) (u v : Measurement.Bits ι) (ψ : Measurement.Amplitude ι) :

Measurement.pauliAction (shearX i w u) (shearZ i w v) (applyCNOTs i w hw ψ) = applyCNOTs i w hw (Measurement.pauliAction u v ψ)

Exact covariance of the concrete basis-permutation action.

source

theorem LeanPool.SingleCopyStabilizer.CNOTAction.transports_eigenvector {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) (ψ : Measurement.Amplitude ι) (u v : Measurement.Bits ι) (ζ : ℂ) (heig : Measurement.IsPauliEigenvector ψ u v ζ) :

Measurement.IsPauliEigenvector (applyCNOTs i w hw ψ) (shearX i w u) (shearZ i w v) ζ

Every Pauli eigenlabel is transported by the shear used in the paper.

source

theorem LeanPool.SingleCopyStabilizer.CNOTAction.inverse_action {ι : Type u_1} (i : ι) (w : Measurement.Bits ι) (hw : w i = 0) (ψ : Measurement.Amplitude ι) :

(fun (x : Measurement.Bits ι) => applyCNOTs i w hw ψ ((basisShear i w hw) x)) = ψ

Explicit two-sided inverse, needed when the learned circuit is undone.