# Theory Entanglement

```(*
Authors:

Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk;
Yijun He, University of Cambridge, yh403@cam.ac.uk
*)

section ‹Quantum Entanglement›

theory Entanglement
imports
Quantum
More_Tensor
begin

subsection ‹The Product States and Entangled States of a 2-qubits System›

text ‹Below we add the condition that @{term v} and @{term w} are two-dimensional states, otherwise
@{term u} can always be represented by the tensor product of the 1-dimensional vector @{term 1} and
@{term u} itself.›

definition prod_state2:: "complex Matrix.mat ⇒ bool" where
"prod_state2 u ≡ if state 2 u then ∃v w. state 1 v ∧ state 1 w ∧ u = v ⨂ w else undefined"

definition entangled2:: "complex Matrix.mat ⇒ bool" where
"entangled2 u ≡ ¬ prod_state2 u"

text ‹The Bell states are entangled states.›

lemma bell00_is_entangled2 [simp]:
"entangled2 |β⇩0⇩0⟩"
proof -
have "∀v w. state 1 v ⟶ state 1 w ⟶ |β⇩0⇩0⟩ ≠ v ⨂ w"
proof((rule allI)+,(rule impI)+, rule notI)
fix v w
assume a0:"state 1 v" and a1:"state 1 w" and a2:"|β⇩0⇩0⟩ = v ⨂ w"
have "(v \$\$ (0,0) * w \$\$ (0,0)) * (v \$\$ (1,0) * w \$\$ (1,0)) =
(v \$\$ (0,0) * w \$\$ (1,0)) * (v \$\$ (1,0) * w \$\$ (0,0))" by simp
then have "(v ⨂ w) \$\$ (0,0) * (v ⨂ w) \$\$ (3,0) = (v ⨂ w) \$\$ (1,0) * (v ⨂ w) \$\$ (2,0)"
using a0 a1 by simp
then have "|β⇩0⇩0⟩ \$\$ (0,0) * |β⇩0⇩0⟩ \$\$ (3,0) = |β⇩0⇩0⟩ \$\$ (1,0) * |β⇩0⇩0⟩ \$\$ (2,0)"
using a2 by simp
then have "1/ sqrt 2 * 1/sqrt 2 = 0" by simp
thus False by simp
qed
thus ?thesis by(simp add: entangled2_def prod_state2_def)
qed

lemma bell01_is_entangled2 [simp]:
"entangled2 |β⇩0⇩1⟩"
proof -
have "∀v w. state 1 v ⟶ state 1 w ⟶ |β⇩0⇩1⟩ ≠ v ⨂ w"
proof((rule allI)+,(rule impI)+, rule notI)
fix v w
assume a0:"state 1 v" and a1:"state 1 w" and a2:"|β⇩0⇩1⟩ = v ⨂ w"
have "(v \$\$ (0,0) * w \$\$ (1,0)) * (v \$\$ (1,0) * w \$\$ (0,0)) =
(v \$\$ (0,0) * w \$\$ (0,0)) * (v \$\$ (1,0) * w \$\$ (1,0))" by simp
then have "(v ⨂ w) \$\$ (1,0) * (v ⨂ w) \$\$ (2,0) = (v ⨂ w) \$\$ (0,0) * (v ⨂ w) \$\$ (3,0)"
using a0 a1 by simp
then have "|β⇩0⇩1⟩ \$\$ (1,0) * |β⇩0⇩1⟩ \$\$ (2,0) = |β⇩0⇩1⟩ \$\$ (0,0) * |β⇩0⇩1⟩ \$\$ (3,0)"
using a2 by simp
then have "1/sqrt 2 * 1/sqrt 2 = 0"
using bell01_index by simp
thus False by simp
qed
thus ?thesis by(simp add: entangled2_def prod_state2_def)
qed

lemma bell10_is_entangled2 [simp]:
"entangled2 |β⇩1⇩0⟩"
proof -
have "∀v w. state 1 v ⟶ state 1 w ⟶ |β⇩1⇩0⟩ ≠ v ⨂ w"
proof((rule allI)+,(rule impI)+, rule notI)
fix v w
assume a0:"state 1 v" and a1:"state 1 w" and a2:"|β⇩1⇩0⟩ = v ⨂ w"
have "(v \$\$ (0,0) * w \$\$ (0,0)) * (v \$\$ (1,0) * w \$\$ (1,0)) =
(v \$\$ (0,0) * w \$\$ (1,0)) * (v \$\$ (1,0) * w \$\$ (0,0))" by simp
then have "(v ⨂ w) \$\$ (0,0) * (v ⨂ w) \$\$ (3,0) = (v ⨂ w) \$\$ (1,0) * (v ⨂ w) \$\$ (2,0)"
using a0 a1 by simp
then have "|β⇩1⇩0⟩ \$\$ (1,0) * |β⇩1⇩0⟩ \$\$ (2,0) = |β⇩1⇩0⟩ \$\$ (0,0) * |β⇩1⇩0⟩ \$\$ (3,0)"
using a2 by simp
then have "1/sqrt 2 * 1/sqrt 2 = 0" by simp
thus False by simp
qed
thus ?thesis by(simp add: entangled2_def prod_state2_def)
qed

lemma bell11_is_entangled2 [simp]:
"entangled2 |β⇩1⇩1⟩"
proof -
have "∀v w. state 1 v ⟶ state 1 w ⟶ |β⇩1⇩1⟩ ≠ v ⨂ w"
proof((rule allI)+,(rule impI)+, rule notI)
fix v w
assume a0:"state 1 v" and a1:"state 1 w" and a2:"|β⇩1⇩1⟩ = v ⨂ w"
have "(v \$\$ (0,0) * w \$\$ (1,0)) * (v \$\$ (1,0) * w \$\$ (0,0)) =
(v \$\$ (0,0) * w \$\$ (0,0)) * (v \$\$ (1,0) * w \$\$ (1,0))" by simp
then have "(v ⨂ w) \$\$ (1,0) * (v ⨂ w) \$\$ (2,0) = (v ⨂ w) \$\$ (0,0) * (v ⨂ w) \$\$ (3,0)"
using a0 a1 by simp
then have "|β⇩1⇩1⟩ \$\$ (1,0) * |β⇩1⇩1⟩ \$\$ (2,0) = |β⇩1⇩1⟩ \$\$ (0,0) * |β⇩1⇩1⟩ \$\$ (3,0)"
using a2 by simp
then have "1/sqrt 2 * 1/sqrt 2 = 0"
using bell_11_index by simp
thus False by simp
qed
thus ?thesis by(simp add: entangled2_def prod_state2_def)
qed

text ‹
An entangled state is a state that cannot be broken down as the tensor product of smaller states.
›

definition prod_state:: "nat ⇒ complex Matrix.mat ⇒ bool" where
"prod_state m u ≡ if state m u then ∃n p::nat.∃v w. state n v ∧ state p w ∧
n < m ∧ p < m ∧  u = v ⨂ w else undefined"

definition entangled:: "nat ⇒ complex Matrix.mat ⇒ bool" where
"entangled n v ≡ ¬ (prod_state n v)"

(* To do: as an exercise prove the equivalence between entangled2 and (entangled 2). *)

lemma sanity_check:
"¬(entangled 2 (mat_of_cols_list 2 [[1/sqrt(2), 1/sqrt(2)]] ⨂ mat_of_cols_list 2 [[1/sqrt(2), 1/sqrt(2)]]))"
proof -
define u where "u = mat_of_cols_list 2 [[1/sqrt(2), 1/sqrt(2)]]"
then have "state 1 u"
proof -
have "dim_col u = 1"
using u_def mat_of_cols_list_def by simp
moreover have f:"dim_row u = 2"
using u_def mat_of_cols_list_def by simp
moreover have "∥Matrix.col u 0∥ = 1"
proof -
have "(∑i<2. (cmod (u \$\$ (i, 0)))⇧2) = (1/sqrt 2)⇧2 + (1/sqrt 2)⇧2"