Tensor products of vectors, states, operators, and gates

Raw tensor products are defined at the StateVector and HilbertOperator layers. PureState.tensor and Gate.tensor wrap these raw tensors with the normalization/unitarity proofs needed to stay in their semantic types.

noncomputable def QuantumAlg.StateVector.tensor {m n : ℕ} (ψ : StateVector m) (φ : StateVector n) : StateVector (m + n)

Tensor product of raw Hilbert-space vectors.

Equations

• ψ.tensor φ = WithLp.toLp 2 fun (i : Fin (2 ^ (m + n))) => ψ.ofLp (QuantumAlg.prodEquiv.symm i).1 * φ.ofLp (QuantumAlg.prodEquiv.symm i).2

@[simp]

theorem QuantumAlg.StateVector.tensor_apply {m n : ℕ} (ψ : StateVector m) (φ : StateVector n) (i : Fin (2 ^ (m + n))) : (ψ.tensor φ).ofLp i = ψ.ofLp (prodEquiv.symm i).1 * φ.ofLp (prodEquiv.symm i).2

theorem QuantumAlg.StateVector.tensor_apply_prod {m n : ℕ} (ψ : StateVector m) (φ : StateVector n) (x : Fin (2 ^ m)) (y : Fin (2 ^ n)) : (ψ.tensor φ).ofLp (prodEquiv (x, y)) = ψ.ofLp x * φ.ofLp y

@[simp]

theorem QuantumAlg.StateVector.add_tensor {m n : ℕ} (ψ ψ' : StateVector m) (φ : StateVector n) : (ψ + ψ').tensor φ = ψ.tensor φ + ψ'.tensor φ

@[simp]

theorem QuantumAlg.StateVector.sub_tensor {m n : ℕ} (ψ ψ' : StateVector m) (φ : StateVector n) : (ψ - ψ').tensor φ = ψ.tensor φ - ψ'.tensor φ

@[simp]

theorem QuantumAlg.StateVector.smul_tensor {m n : ℕ} (c : ℂ) (ψ : StateVector m) (φ : StateVector n) : (c • ψ).tensor φ = c • ψ.tensor φ

@[simp]

theorem QuantumAlg.StateVector.tensor_add {m n : ℕ} (ψ : StateVector m) (φ φ' : StateVector n) : ψ.tensor (φ + φ') = ψ.tensor φ + ψ.tensor φ'

@[simp]

theorem QuantumAlg.StateVector.tensor_sub {m n : ℕ} (ψ : StateVector m) (φ φ' : StateVector n) : ψ.tensor (φ - φ') = ψ.tensor φ - ψ.tensor φ'

@[simp]

theorem QuantumAlg.StateVector.tensor_smul {m n : ℕ} (c : ℂ) (ψ : StateVector m) (φ : StateVector n) : ψ.tensor (c • φ) = c • ψ.tensor φ

@[simp]

theorem QuantumAlg.StateVector.neg_tensor {m n : ℕ} (ψ : StateVector m) (φ : StateVector n) : (-ψ).tensor φ = -ψ.tensor φ

@[simp]

theorem QuantumAlg.StateVector.tensor_neg {m n : ℕ} (ψ : StateVector m) (φ : StateVector n) : ψ.tensor (-φ) = -ψ.tensor φ

@[simp]

theorem QuantumAlg.StateVector.zero_tensor {m n : ℕ} (φ : StateVector n) : tensor 0 φ = 0

@[simp]

theorem QuantumAlg.StateVector.tensor_zero {m n : ℕ} (ψ : StateVector m) : ψ.tensor 0 = 0

theorem QuantumAlg.StateVector.norm_tensor {m n : ℕ} (ψ : StateVector m) (φ : StateVector n) : ‖ψ.tensor φ‖ = ‖ψ‖ * ‖φ‖

The norm is multiplicative under tensor products.

theorem QuantumAlg.StateVector.inner_tensor_tensor {m n : ℕ} (ψ ψ' : StateVector m) (φ φ' : StateVector n) : inner ℂ (ψ.tensor φ) (ψ'.tensor φ') = inner ℂ ψ ψ' * inner ℂ φ φ'

The inner product factors over tensor products.

noncomputable def QuantumAlg.PureState.tensor {m n : ℕ} (ψ : PureState m) (φ : PureState n) : PureState (m + n)

Tensor product of pure states.

Equations

• ψ.tensor φ = QuantumAlg.PureState.ofVec (ψ.vec.tensor φ.vec) ⋯

@[simp]

theorem QuantumAlg.PureState.tensor_apply {m n : ℕ} (ψ : PureState m) (φ : PureState n) (i : Fin (2 ^ (m + n))) : (ψ.tensor φ).vec.ofLp i = ψ.vec.ofLp (prodEquiv.symm i).1 * φ.vec.ofLp (prodEquiv.symm i).2

theorem QuantumAlg.PureState.tensor_apply_prod {m n : ℕ} (ψ : PureState m) (φ : PureState n) (x : Fin (2 ^ m)) (y : Fin (2 ^ n)) : (ψ.tensor φ).vec.ofLp (prodEquiv (x, y)) = ψ.vec.ofLp x * φ.vec.ofLp y

theorem QuantumAlg.PureState.add_tensor {m n : ℕ} (ψ ψ' : StateVector m) (φ : StateVector n) : (ψ + ψ').tensor φ = ψ.tensor φ + ψ'.tensor φ

theorem QuantumAlg.PureState.sub_tensor {m n : ℕ} (ψ ψ' : StateVector m) (φ : StateVector n) : (ψ - ψ').tensor φ = ψ.tensor φ - ψ'.tensor φ

theorem QuantumAlg.PureState.smul_tensor {m n : ℕ} (c : ℂ) (ψ : StateVector m) (φ : StateVector n) : (c • ψ).tensor φ = c • ψ.tensor φ

theorem QuantumAlg.PureState.tensor_add {m n : ℕ} (ψ : StateVector m) (φ φ' : StateVector n) : ψ.tensor (φ + φ') = ψ.tensor φ + ψ.tensor φ'

theorem QuantumAlg.PureState.tensor_sub {m n : ℕ} (ψ : StateVector m) (φ φ' : StateVector n) : ψ.tensor (φ - φ') = ψ.tensor φ - ψ.tensor φ'

theorem QuantumAlg.PureState.tensor_smul {m n : ℕ} (c : ℂ) (ψ : StateVector m) (φ : StateVector n) : ψ.tensor (c • φ) = c • ψ.tensor φ

theorem QuantumAlg.PureState.neg_tensor {m n : ℕ} (ψ : StateVector m) (φ : StateVector n) : (-ψ).tensor φ = -ψ.tensor φ

theorem QuantumAlg.PureState.tensor_neg {m n : ℕ} (ψ : StateVector m) (φ : StateVector n) : ψ.tensor (-φ) = -ψ.tensor φ

theorem QuantumAlg.PureState.zero_tensor {m n : ℕ} (φ : StateVector n) : StateVector.tensor 0 φ = 0

theorem QuantumAlg.PureState.tensor_zero {m n : ℕ} (ψ : StateVector m) : ψ.tensor 0 = 0

theorem QuantumAlg.PureState.tensor_ket {m n : ℕ} (x : Fin (2 ^ m)) (y : Fin (2 ^ n)) : (ket x).tensor (ket y) = ket (prodEquiv (x, y))

Basis kets tensor to basis kets: |x⟩ ⊗ |y⟩ = |xy⟩.

theorem QuantumAlg.PureState.norm_tensor {m n : ℕ} (ψ : PureState m) (φ : PureState n) : ‖ψ.tensor φ‖ = ‖ψ‖ * ‖φ‖

theorem QuantumAlg.PureState.inner_tensor_tensor {m n : ℕ} (ψ ψ' : PureState m) (φ φ' : PureState n) : inner ℂ (ψ.tensor φ) (ψ'.tensor φ') = inner ℂ ψ ψ' * inner ℂ φ φ'

noncomputable def QuantumAlg.HilbertOperator.tensor {m n : ℕ} (G : HilbertOperator m) (K : HilbertOperator n) : HilbertOperator (m + n)

Tensor product of Hilbert-space operators.

Equations

• G.tensor K = (Matrix.reindex QuantumAlg.prodEquiv QuantumAlg.prodEquiv) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) G K)

@[simp]

theorem QuantumAlg.HilbertOperator.tensor_apply {m n : ℕ} (G : HilbertOperator m) (K : HilbertOperator n) (i j : Fin (2 ^ (m + n))) : G.tensor K i j = G (prodEquiv.symm i).1 (prodEquiv.symm j).1 * K (prodEquiv.symm i).2 (prodEquiv.symm j).2

@[simp]

theorem QuantumAlg.HilbertOperator.zero_tensor {m n : ℕ} (K : HilbertOperator n) : tensor 0 K = 0

@[simp]

theorem QuantumAlg.HilbertOperator.tensor_zero {m n : ℕ} (G : HilbertOperator m) : G.tensor 0 = 0

theorem QuantumAlg.HilbertOperator.add_tensor {m n : ℕ} (G G' : HilbertOperator m) (K : HilbertOperator n) : (G + G').tensor K = G.tensor K + G'.tensor K

theorem QuantumAlg.HilbertOperator.tensor_add {m n : ℕ} (G : HilbertOperator m) (K K' : HilbertOperator n) : G.tensor (K + K') = G.tensor K + G.tensor K'

theorem QuantumAlg.HilbertOperator.tensor_mul_tensor {m n : ℕ} (G G' : HilbertOperator m) (K K' : HilbertOperator n) : G.tensor K * G'.tensor K' = tensor (G * G') (K * K')

theorem QuantumAlg.HilbertOperator.conjTranspose_tensor {m n : ℕ} (G : HilbertOperator m) (K : HilbertOperator n) : Matrix.conjTranspose (G.tensor K) = tensor (Matrix.conjTranspose G) (Matrix.conjTranspose K)

@[simp]

theorem QuantumAlg.HilbertOperator.one_tensor_one {m n : ℕ} : tensor 1 1 = 1

theorem QuantumAlg.HilbertOperator.tensor_mem_unitaryGroup {m n : ℕ} {G : HilbertOperator m} {K : HilbertOperator n} (hG : G ∈ Matrix.unitaryGroup (Fin (2 ^ m)) ℂ) (hK : K ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ) : G.tensor K ∈ Matrix.unitaryGroup (Fin (2 ^ (m + n))) ℂ

theorem QuantumAlg.HilbertOperator.tensor_applyVec_tensor {m n : ℕ} (G : HilbertOperator m) (K : HilbertOperator n) (ψ : StateVector m) (φ : StateVector n) : (G.tensor K).applyVec (ψ.tensor φ) = (G.applyVec ψ).tensor (K.applyVec φ)

noncomputable def QuantumAlg.Gate.tensor {m n : ℕ} (G : Gate m) (K : Gate n) : Gate (m + n)

Tensor product of unitary gates.

Equations

• G.tensor K = QuantumAlg.Gate.ofUnitary (G.op.tensor K.op) ⋯

@[simp]

theorem QuantumAlg.Gate.tensor_apply {m n : ℕ} (G : Gate m) (K : Gate n) (i j : Fin (2 ^ (m + n))) : (G.tensor K).op i j = G.op (prodEquiv.symm i).1 (prodEquiv.symm j).1 * K.op (prodEquiv.symm i).2 (prodEquiv.symm j).2

theorem QuantumAlg.Gate.tensor_mul_tensor {m n : ℕ} (G G' : Gate m) (K K' : Gate n) : G.tensor K * G'.tensor K' = (G * G').tensor (K * K')

theorem QuantumAlg.Gate.conjTranspose_tensor {m n : ℕ} (G : Gate m) (K : Gate n) : (G.tensor K).conjTranspose = G.conjTranspose.tensor K.conjTranspose

@[simp]

theorem QuantumAlg.Gate.one_tensor_one {m n : ℕ} : tensor 1 1 = 1

theorem QuantumAlg.Gate.tensor_mem_unitaryGroup {m n : ℕ} {G : Gate m} {K : Gate n} (_hG : G.op ∈ Matrix.unitaryGroup (Fin (2 ^ m)) ℂ) (_hK : K.op ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ) : (G.tensor K).op ∈ Matrix.unitaryGroup (Fin (2 ^ (m + n))) ℂ

theorem QuantumAlg.Gate.tensor_apply_tensor {m n : ℕ} (G : Gate m) (K : Gate n) (ψ : PureState m) (φ : PureState n) : (G.tensor K).apply (ψ.tensor φ) = (G.apply ψ).tensor (K.apply φ)

theorem QuantumAlg.Gate.tensor_applyVec_tensor {m n : ℕ} (G : Gate m) (K : Gate n) (ψ : StateVector m) (φ : StateVector n) : (G.tensor K).applyVec (ψ.tensor φ) = (G.applyVec ψ).tensor (K.applyVec φ)