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 |β00⟩" 
proof -
  have "∀v w. state 1 v ⟶ state 1 w ⟶ |β00⟩ ≠ v ⨂ w"
  proof((rule allI)+,(rule impI)+, rule notI)
    fix v w
    assume a0:"state 1 v" and a1:"state 1 w" and a2:"|β00⟩ = 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 "|β00⟩ $$ (0,0) * |β00⟩ $$ (3,0) = |β00⟩ $$ (1,0) * |β00⟩ $$ (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 |β01⟩"
proof -
  have "∀v w. state 1 v ⟶ state 1 w ⟶ |β01⟩ ≠ v ⨂ w"
  proof((rule allI)+,(rule impI)+, rule notI)
    fix v w
    assume a0:"state 1 v" and a1:"state 1 w" and a2:"|β01⟩ = 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 "|β01⟩ $$ (1,0) * |β01⟩ $$ (2,0) = |β01⟩ $$ (0,0) * |β01⟩ $$ (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 |β10⟩"
proof -
  have "∀v w. state 1 v ⟶ state 1 w ⟶ |β10⟩ ≠ v ⨂ w"
  proof((rule allI)+,(rule impI)+, rule notI)
    fix v w
    assume a0:"state 1 v" and a1:"state 1 w" and a2:"|β10⟩ = 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 "|β10⟩ $$ (1,0) * |β10⟩ $$ (2,0) = |β10⟩ $$ (0,0) * |β10⟩ $$ (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 |β11⟩"
proof -
  have "∀v w. state 1 v ⟶ state 1 w ⟶ |β11⟩ ≠ v ⨂ w"
  proof((rule allI)+,(rule impI)+, rule notI)
    fix v w
    assume a0:"state 1 v" and a1:"state 1 w" and a2:"|β11⟩ = 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 "|β11⟩ $$ (1,0) * |β11⟩ $$ (2,0) = |β11⟩ $$ (0,0) * |β11⟩ $$ (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"
        by(simp add: u_def cmod_def numeral_2_eq_2)
      then have "∥Matrix.col u 0∥ = sqrt ((1/sqrt 2)2 + (1/sqrt 2)2)"
        using f by(auto simp: Matrix.col_def u_def cpx_vec_length_def)
      thus ?thesis by(simp add: power_divide)
    qed
    ultimately show ?thesis by(simp add: state_def)
  qed
  then have "state 2 (u ⨂ u)"
    using tensor_state by(metis one_add_one)
  thus ?thesis
    using entangled_def prod_state_def by(metis ‹state 1 u› one_less_numeral_iff semiring_norm(76) u_def)
qed

end