Theory Quantum_Prisoners_Dilemma
section ‹Quantum Prisoner's Dilemma›
theory Quantum_Prisoners_Dilemma
imports
More_Tensor
Measurement
Basics
begin
text ‹
In the 2-parameter strategic space of Eisert, Wilkens and Lewenstein [EWL], Prisoner's Dilemma
ceases to pose a dilemma if quantum strategies are allowed for. Indeed, Alice and Bob both choosing
to defect is no longer a Nash equilibrium. However, a new Nash equilibrium appears which is at the
same time Pareto optimal. Moreover, there exists a quantum strategy which always gives reward if
played against any classical strategy.
Below the parameter @{text "γ"} can be seen as a measure of the game's entanglement. The game behaves
classically if @{text "γ"} = 0, and for the maximally entangled case (@{text "γ"} = 2*$\pi$) the dilemma disappears
as pointed out above.
›
subsection ‹The Set-Up›
locale prisoner =
fixes γ:: "real"
assumes "γ ≤ pi/2" and "γ ≥ 0"
abbreviation (in prisoner) J :: "complex Matrix.mat" where
"J ≡ mat_of_cols_list 4 [[cos(γ/2), 0, 0, 𝗂*sin(γ/2)],
[0, cos(γ/2), -𝗂*sin(γ/2), 0],
[0, -𝗂*sin(γ/2), cos(γ/2), 0],
[𝗂*sin(γ/2), 0, 0, cos(γ/2)]]"
abbreviation (in prisoner) ψ⇩1 :: "complex Matrix.mat" where
"ψ⇩1 ≡ mat_of_cols_list 4 [[cos(γ/2), 0, 0, 𝗂*sin(γ/2)]]"
lemma (in prisoner) psi_one:
shows "J * |unit_vec 4 0⟩ = ψ⇩1"
proof
fix i j assume a0:"i < dim_row ψ⇩1" and a1:"j < dim_col ψ⇩1"
then have "(J * |unit_vec 4 0⟩) $$ (i,j) = (∑k<4. (J $$ (i,k)) * ( |unit_vec 4 0⟩ $$ (k,j)))"
using mat_of_cols_list_def ket_vec_def by auto
also have "... = (∑k∈{0,1,2,3}. (J $$ (i,k)) * ( |unit_vec 4 0⟩ $$ (k,j)))"
using set_4 atLeast0LessThan by simp
also have "... = ψ⇩1 $$ (i,j)"
proof-
have "i∈{0,1,2,3} ∧ j=0"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def by auto
qed
finally show "(J * |unit_vec 4 0⟩) $$ (i,j) = ψ⇩1 $$ (i,j)" by simp
next
show "dim_row (J * |unit_vec 4 0⟩) = dim_row ψ⇩1"
using mat_of_cols_list_def by simp
next
show "dim_col (J*|unit_vec 4 0⟩) = dim_col ψ⇩1"
using mat_of_cols_list_def by (simp add: ket_vec_def)
qed
locale strategic_space_2p = prisoner +
fixes θ⇩A:: "real"
and φ⇩A:: "real"
and θ⇩B:: "real"
and φ⇩B:: "real"
assumes "0 ≤ θ⇩A ∧ θ⇩A ≤ pi"
and "0 ≤ φ⇩A ∧ φ⇩A ≤ pi/2"
and "0 ≤ θ⇩B ∧ θ⇩B ≤ pi"
and "0 ≤ φ⇩B ∧ φ⇩B ≤ pi/2"
abbreviation (in strategic_space_2p) U⇩A :: "complex Matrix.mat" where
"U⇩A ≡ mat_of_cols_list 2 [[exp(𝗂*φ⇩A)*cos(θ⇩A/2), -sin(θ⇩A/2)],
[sin(θ⇩A/2), exp(-𝗂*φ⇩A)*cos(θ⇩A/2)]]"
abbreviation (in strategic_space_2p) U⇩B :: "complex Matrix.mat" where
"U⇩B ≡ mat_of_cols_list 2 [[exp(𝗂*φ⇩B)*cos(θ⇩B/2), -sin(θ⇩B/2)],
[sin(θ⇩B/2), exp(-𝗂*φ⇩B)*cos(θ⇩B/2)]]"
abbreviation (in strategic_space_2p) ψ⇩2 :: "complex Matrix.mat" where
"ψ⇩2 ≡
mat_of_cols_list 4 [[exp(𝗂*φ⇩A)*cos(θ⇩A/2) * exp(𝗂*φ⇩B)*cos(θ⇩B/2) * cos(γ/2) + sin(θ⇩A/2) * sin(θ⇩B/2) * 𝗂*sin(γ/2),
exp(𝗂*φ⇩A)*cos(θ⇩A/2) * -sin(θ⇩B/2) * cos(γ/2) + sin(θ⇩A/2) * exp(-𝗂*φ⇩B)*cos(θ⇩B/2) * 𝗂*sin(γ/2),
-sin(θ⇩A/2) * exp(𝗂*φ⇩B)*cos(θ⇩B/2) * cos(γ/2) + exp(-𝗂*φ⇩A)*cos(θ⇩A/2) * sin(θ⇩B/2) * 𝗂*sin(γ/2),
sin(θ⇩A/2) * sin(θ⇩B/2) * cos(γ/2) + exp(-𝗂*φ⇩A)*cos(θ⇩A/2) * exp(-𝗂*φ⇩B)*cos(θ⇩B/2) * 𝗂*sin(γ/2)]]"
abbreviation (in strategic_space_2p) U⇩A⇩B :: "complex Matrix.mat" where
"U⇩A⇩B ≡
mat_of_cols_list 4 [[exp(𝗂*φ⇩A)*cos(θ⇩A/2) * exp(𝗂*φ⇩B)*cos(θ⇩B/2), exp(𝗂*φ⇩A)*cos(θ⇩A/2) * -sin(θ⇩B/2),
-sin(θ⇩A/2) * exp(𝗂*φ⇩B)*cos(θ⇩B/2), -sin(θ⇩A/2) * -sin(θ⇩B/2)],
[exp(𝗂*φ⇩A)*cos(θ⇩A/2) * sin(θ⇩B/2), exp(𝗂*φ⇩A)*cos(θ⇩A/2) * exp(-𝗂*φ⇩B)*cos(θ⇩B/2),
-sin(θ⇩A/2) * sin(θ⇩B/2), -sin(θ⇩A/2) * exp(-𝗂*φ⇩B)*cos(θ⇩B/2)],
[sin(θ⇩A/2) * exp(𝗂*φ⇩B)*cos(θ⇩B/2), -sin(θ⇩A/2) * sin(θ⇩B/2),
exp(-𝗂*φ⇩A)*cos(θ⇩A/2) * exp (𝗂*φ⇩B)*cos(θ⇩B/2), exp(-𝗂*φ⇩A)*cos(θ⇩A/2) * -sin(θ⇩B/2)],
[sin(θ⇩A/2) * sin(θ⇩B/2), sin(θ⇩A/2) * exp(-𝗂*φ⇩B)*cos(θ⇩B/2),
exp(-𝗂*φ⇩A)*cos(θ⇩A/2) * sin(θ⇩B/2), exp (-𝗂*φ⇩A)*cos(θ⇩A/2) * exp(-𝗂*φ⇩B)*cos(θ⇩B/2)]]"
lemma (in strategic_space_2p) U⇩A_tensor_U⇩B:
shows "(U⇩A ⨂ U⇩B) = U⇩A⇩B"
proof
fix i j assume a0: "i<dim_row U⇩A⇩B" and a1: "j<dim_col U⇩A⇩B"
then have "i∈{0,1,2,3} ∧ j∈{0,1,2,3}"
using mat_of_cols_list_def by auto
then show "(U⇩A ⨂ U⇩B) $$ (i,j) = U⇩A⇩B $$ (i,j)"
using mat_of_cols_list_def by auto
next
show "dim_row (U⇩A ⨂ U⇩B) = dim_row U⇩A⇩B"
using mat_of_cols_list_def by simp
next
show "dim_col (U⇩A ⨂ U⇩B) = dim_col U⇩A⇩B"
using mat_of_cols_list_def by simp
qed
lemma (in strategic_space_2p) psi_two:
shows "(U⇩A ⨂ U⇩B) * ψ⇩1 = ψ⇩2"
proof
fix i j
assume a0:"i < dim_row ψ⇩2" and a1:"j < dim_col ψ⇩2"
then show "((U⇩A ⨂ U⇩B) * ψ⇩1) $$ (i,j) = ψ⇩2 $$ (i,j)"
proof-
have "i∈{0,1,2,3} ∧ j=0"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def U⇩A_tensor_U⇩B set_4 by auto
qed
next
show "dim_row ((U⇩A ⨂ U⇩B)*ψ⇩1) = dim_row ψ⇩2"
using mat_of_cols_list_def by simp
next
show "dim_col ((U⇩A ⨂ U⇩B)*ψ⇩1) = dim_col ψ⇩2"
using mat_of_cols_list_def by simp
qed
abbreviation (in prisoner) J_cnj :: "complex Matrix.mat" where
"J_cnj ≡ mat_of_cols_list 4 [[cos(γ/2), 0, 0, -𝗂*sin(γ/2)],
[0, cos(γ/2), 𝗂*sin(γ/2), 0],
[0, 𝗂*sin(γ/2), cos(γ/2), 0],
[-𝗂*sin(γ/2), 0, 0, cos(γ/2)]]"
lemma (in prisoner) hermite_cnj_of_J [simp]:
shows "J⇧† = J_cnj"
proof
fix i j assume a0:"i < dim_row J_cnj" and a1:"j < dim_col J_cnj"
then show "J⇧† $$ (i,j) = J_cnj $$ (i,j)"
proof-
have "i∈{0,1,2,3} ∧ j∈{0,1,2,3}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def dagger_def by auto
qed
next
show "dim_row (J⇧†) = dim_row J_cnj"
using mat_of_cols_list_def by simp
next
show "dim_col (J⇧†) = dim_col J_cnj"
using mat_of_cols_list_def by simp
qed
abbreviation (in strategic_space_2p) ψ⇩f :: "complex Matrix.mat" where
"ψ⇩f ≡ mat_of_cols_list 4 [[
cos(γ/2) * (exp(𝗂*φ⇩A)*cos(θ⇩A/2) * exp(𝗂*φ⇩B)*cos(θ⇩B/2) * cos(γ/2) + sin(θ⇩A/2) * sin(θ⇩B/2) * 𝗂*sin(γ/2))
+ (-𝗂*sin(γ/2)) * (sin(θ⇩A/2) * sin(θ⇩B/2) * cos(γ/2) + exp(-𝗂*φ⇩A)*cos(θ⇩A/2) * exp(-𝗂*φ⇩B)*cos(θ⇩B/2) * 𝗂*sin(γ/2)),
cos(γ/2) * (exp(𝗂*φ⇩A)*cos(θ⇩A/2) * -sin(θ⇩B/2) * cos(γ/2) + sin(θ⇩A/2) * exp(-𝗂*φ⇩B)*cos(θ⇩B/2) * 𝗂*sin(γ/2))
+ (𝗂*sin(γ/2)) * (-sin(θ⇩A/2) * exp(𝗂*φ⇩B)*cos(θ⇩B/2) * cos(γ/2) + exp(-𝗂*φ⇩A)*cos(θ⇩A/2) * sin(θ⇩B/2) * 𝗂*sin(γ/2)),
(𝗂*sin(γ/2)) * (exp(𝗂*φ⇩A)*cos(θ⇩A/2) * -sin(θ⇩B/2) * cos(γ/2) + sin(θ⇩A/2) * exp(-𝗂*φ⇩B)*cos(θ⇩B/2) * 𝗂*sin(γ/2))
+ cos(γ/2) * (-sin(θ⇩A/2) * exp(𝗂*φ⇩B)*cos(θ⇩B/2) * cos(γ/2) + exp(-𝗂*φ⇩A)*cos(θ⇩A/2) * sin(θ⇩B/2) * 𝗂*sin(γ/2)),
(-𝗂*sin(γ/2)) * (exp(𝗂*φ⇩A)*cos(θ⇩A/2) * exp(𝗂*φ⇩B)*cos(θ⇩B/2) * cos(γ/2) + sin(θ⇩A/2) * sin(θ⇩B/2) * 𝗂*sin(γ/2))
+ cos(γ/2) * (sin(θ⇩A/2) * sin(θ⇩B/2) * cos(γ/2) + exp(-𝗂*φ⇩A)*cos(θ⇩A/2) * exp(-𝗂*φ⇩B)*cos(θ⇩B/2) * 𝗂*sin(γ/2))
]]"
lemma (in strategic_space_2p) psi_f:
shows "(J⇧†) * ψ⇩2 = ψ⇩f"
proof
fix i j assume a0:"i < dim_row ψ⇩f" and a1:"j < dim_col ψ⇩f"
then show "((J⇧†) * ψ⇩2) $$ (i,j) = ψ⇩f $$ (i,j)"
proof-
have "i∈{0,1,2,3} ∧ j=0"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def set_4 hermite_cnj_of_J by auto
qed
next
show "dim_row ((J⇧†) * ψ⇩2) = dim_row ψ⇩f"
using mat_of_cols_list_def by simp
next
show "dim_col ((J⇧†) * ψ⇩2) = dim_col ψ⇩f"
using mat_of_cols_list_def by simp
qed
lemma (in prisoner) unit_vec_4_0_ket_is_state:
shows "state 2 |unit_vec 4 0⟩"
using state_def cpx_vec_length_def ket_vec_def unit_vec_def by (auto simp add: set_4)
lemma cos_sin_squared_add_cpx:
"complex_of_real (cos (γ/2)) * complex_of_real (cos (γ/2)) -
𝗂*complex_of_real (sin (γ/2)) * (𝗂*complex_of_real (sin (γ/2))) = 1"
apply (auto simp add: algebra_simps)
by (metis of_real_add of_real_hom.hom_one of_real_mult sin_cos_squared_add3)
lemma sin_cos_squared_add_cpx:
"𝗂*complex_of_real (sin (γ/2)) * (𝗂*complex_of_real (sin (γ/2))) -
complex_of_real (cos (γ/2)) * complex_of_real (cos (γ/2)) = -1"
apply (auto simp add: algebra_simps)
by (metis of_real_add of_real_hom.hom_one of_real_mult sin_cos_squared_add3)
lemma (in prisoner) J_cnj_times_J:
shows "J⇧† * J = 1⇩m 4"
proof
fix i j assume a0:"i < dim_row (1⇩m 4)" and a1:"j < dim_col (1⇩m 4)"
then show "(J⇧† * J) $$ (i,j) = 1⇩m 4 $$ (i,j)"
proof-
have "i∈{0,1,2,3} ∧ j∈{0,1,2,3}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def hermite_cnj_of_J set_4 cos_sin_squared_add_cpx by auto
qed
next
show "dim_row (J⇧† * J) = dim_row (1⇩m 4)"
using mat_of_cols_list_def by simp
next
show "dim_col (J⇧† * J) = dim_col (1⇩m 4)"
using mat_of_cols_list_def by simp
qed
lemma (in prisoner) J_times_J_cnj:
shows "J * (J⇧†) = 1⇩m 4"
proof
fix i j assume a0:"i < dim_row (1⇩m 4)" and a1:"j < dim_col (1⇩m 4)"
then show "(J * (J⇧†)) $$ (i,j) = 1⇩m 4 $$ (i,j)"
proof-
have "i∈{0,1,2,3} ∧ j∈{0,1,2,3}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def hermite_cnj_of_J set_4 cos_sin_squared_add_cpx by auto
qed
next
show "dim_row (J * (J⇧†)) = dim_row (1⇩m 4)"
using mat_of_cols_list_def by simp
next
show "dim_col (J * (J⇧†)) = dim_col (1⇩m 4)"
using mat_of_cols_list_def by simp
qed
lemma (in prisoner) J_is_gate:
shows "gate 2 J"
proof
show "dim_row J = 2⇧2"
using mat_of_cols_list_def by simp
moreover show "square_mat J"
using mat_of_cols_list_def by simp
ultimately show "unitary J"
using mat_of_cols_list_def unitary_def J_cnj_times_J J_times_J_cnj by auto
qed
lemma (in strategic_space_2p) psi_one_is_state:
shows "state 2 ψ⇩1"
proof-
have "state 2 (J * |unit_vec 4 0⟩)"
using unit_vec_4_0_ket_is_state J_is_gate by auto
then show ?thesis
using psi_one by simp
qed
abbreviation (in strategic_space_2p) U⇩A_cnj :: "complex Matrix.mat" where
"U⇩A_cnj ≡ mat_of_cols_list 2 [[(exp(-𝗂*φ⇩A))*cos(θ⇩A/2), sin(θ⇩A/2)],
[-sin(θ⇩A/2), (exp (𝗂*φ⇩A))*cos(θ⇩A/2)]]"
abbreviation (in strategic_space_2p) U⇩B_cnj :: "complex Matrix.mat" where
"U⇩B_cnj ≡ mat_of_cols_list 2 [[(exp(-𝗂*φ⇩B))*cos(θ⇩B/2), sin(θ⇩B/2)],
[-sin(θ⇩B/2), (exp(𝗂*φ⇩B))*cos(θ⇩B/2)]]"
lemma (in strategic_space_2p) hermite_cnj_of_U⇩A:
shows "U⇩A⇧† = U⇩A_cnj"
proof
fix i j assume a0:"i < dim_row U⇩A_cnj" and a1:"j < dim_col U⇩A_cnj"
then show "U⇩A⇧† $$ (i,j) = U⇩A_cnj $$ (i,j)"
proof-
have "i∈{0,1} ∧ j∈{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def dagger_def exp_of_real_cnj exp_of_real_cnj2 by auto
qed
next
show "dim_row (U⇩A⇧†) = dim_row U⇩A_cnj"
using mat_of_cols_list_def by simp
next
show "dim_col (U⇩A⇧†) = dim_col U⇩A_cnj"
using mat_of_cols_list_def by simp
qed
lemma (in strategic_space_2p) hermite_cnj_of_U⇩B:
shows "U⇩B⇧† = U⇩B_cnj"
proof
fix i j assume a0:"i < dim_row U⇩B_cnj" and a1:"j < dim_col U⇩B_cnj"
then show "U⇩B⇧† $$ (i,j) = U⇩B_cnj $$ (i,j)"
proof-
have "i∈{0,1} ∧ j∈{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def dagger_def exp_of_real_cnj exp_of_real_cnj2 by auto
qed
next
show "dim_row (U⇩B⇧†) = dim_row U⇩B_cnj"
using mat_of_cols_list_def by simp
next
show "dim_col (U⇩B⇧†) = dim_col U⇩B_cnj"
using mat_of_cols_list_def by simp
qed
lemma exp_sin_cos_squared_add:
fixes x y :: real
shows "exp (- (𝗂 * x)) * cos (y) * (exp (𝗂 * x) * cos (y)) + sin(y) * sin(y) = 1"
proof-
have "exp (- (𝗂 * x)) * cos (y) * (exp (𝗂 * x) * cos (y)) = cos(y) * cos(y)"
using exp_minus_inverse by (auto simp add: algebra_simps)
then show ?thesis
by (metis of_real_add of_real_hom.hom_one sin_cos_squared_add3)
qed
lemma (in strategic_space_2p) U⇩A_cnj_times_U⇩A:
shows "U⇩A⇧† * U⇩A = 1⇩m 2"
proof
fix i j assume a0:"i < dim_row (1⇩m 2)" and a1:"j < dim_col (1⇩m 2)"
then show "(U⇩A⇧† * U⇩A) $$ (i,j) = 1⇩m 2 $$ (i,j)"
proof-
have "i∈{0,1} ∧ j∈{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def cos_sin_squared_add_cpx hermite_cnj_of_U⇩A exp_sin_cos_squared_add[of "φ⇩A" "θ⇩A / 2"]
by (auto simp add: set_2 algebra_simps)
qed
next
show "dim_row (U⇩A⇧† * U⇩A) = dim_row (1⇩m 2)"
using mat_of_cols_list_def by simp
next
show "dim_col (U⇩A⇧† * U⇩A) = dim_col (1⇩m 2)"
using mat_of_cols_list_def by simp
qed
lemma (in strategic_space_2p) U⇩A_times_U⇩A_cnj:
shows "U⇩A * (U⇩A⇧†) = 1⇩m 2"
proof
fix i j assume a0:"i < dim_row (1⇩m 2)" and a1:"j < dim_col (1⇩m 2)"
then show "(U⇩A * (U⇩A⇧†)) $$ (i,j) = 1⇩m 2 $$ (i,j)"
proof-
have "i∈{0,1} ∧ j∈{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def cos_sin_squared_add_cpx hermite_cnj_of_U⇩A exp_sin_cos_squared_add[of "φ⇩A" "θ⇩A / 2"]
by (auto simp add: set_2 algebra_simps)
qed
next
show "dim_row (U⇩A * (U⇩A⇧†)) = dim_row (1⇩m 2)"
using mat_of_cols_list_def by simp
next
show "dim_col (U⇩A * (U⇩A⇧†)) = dim_col (1⇩m 2)"
using mat_of_cols_list_def by simp
qed
lemma (in strategic_space_2p) U⇩B_cnj_times_U⇩B:
shows "U⇩B⇧† * U⇩B = 1⇩m 2"
proof
fix i j assume a0:"i < dim_row (1⇩m 2)" and a1:"j < dim_col (1⇩m 2)"
then show "(U⇩B⇧† * U⇩B) $$ (i,j) = 1⇩m 2 $$ (i,j)"
proof-
have "i∈{0,1} ∧ j∈{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def cos_sin_squared_add_cpx hermite_cnj_of_U⇩B exp_sin_cos_squared_add[of "φ⇩B" "θ⇩B / 2"]
by (auto simp add: set_2 algebra_simps)
qed
next
show "dim_row (U⇩B⇧† * U⇩B) = dim_row (1⇩m 2)"
using mat_of_cols_list_def by simp
next
show "dim_col (U⇩B⇧† * U⇩B) = dim_col (1⇩m 2)"
using mat_of_cols_list_def by simp
qed
lemma (in strategic_space_2p) U⇩B_times_U⇩B_cnj:
shows "U⇩B * (U⇩B⇧†) = 1⇩m 2"
proof
fix i j assume a0:"i < dim_row (1⇩m 2)" and a1:"j < dim_col (1⇩m 2)"
then show "(U⇩B * (U⇩B⇧†)) $$ (i,j) = 1⇩m 2 $$ (i,j)"
proof-
have "i∈{0,1} ∧ j∈{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def cos_sin_squared_add_cpx hermite_cnj_of_U⇩B exp_sin_cos_squared_add[of "φ⇩B" "θ⇩B / 2"]
by (auto simp add: set_2 algebra_simps)
qed
next
show "dim_row (U⇩B * (U⇩B⇧†)) = dim_row (1⇩m 2)"
using mat_of_cols_list_def by simp
next
show "dim_col (U⇩B * (U⇩B⇧†)) = dim_col (1⇩m 2)"
using mat_of_cols_list_def by simp
qed
lemma (in strategic_space_2p) U⇩A⇩_is_gate:
shows "gate 1 U⇩A"
proof
show "dim_row U⇩A = 2^1"
using mat_of_cols_list_def by simp
moreover show "square_mat U⇩A"
using mat_of_cols_list_def by simp
ultimately show "unitary U⇩A"
using mat_of_cols_list_def unitary_def U⇩A_cnj_times_U⇩A U⇩A_times_U⇩A_cnj by auto
qed
lemma (in strategic_space_2p) U⇩B_is_gate:
shows "gate 1 U⇩B"
proof
show "dim_row U⇩B = 2^1"
using mat_of_cols_list_def by simp
moreover show "square_mat U⇩B"
using mat_of_cols_list_def by simp
ultimately show "unitary U⇩B"
using mat_of_cols_list_def unitary_def U⇩B_cnj_times_U⇩B U⇩B_times_U⇩B_cnj by auto
qed
lemma (in strategic_space_2p) U⇩A⇩B_is_gate:
shows "gate 2 (U⇩A ⨂ U⇩B)"
proof-
have "gate (1+1) (U⇩A ⨂ U⇩B)"
using U⇩A⇩_is_gate U⇩B_is_gate tensor_gate[of "1" "U⇩A" "1" "U⇩B"] by auto
then show ?thesis
by (auto simp add: numeral_2_eq_2)
qed
lemma (in strategic_space_2p) psi_two_is_state:
shows "state 2 ψ⇩2"
proof-
have "state 2 ((U⇩A ⨂ U⇩B) * ψ⇩1)"
using psi_one_is_state U⇩A⇩B_is_gate by auto
then show ?thesis
using psi_two by simp
qed
lemma (in strategic_space_2p) J_cnj_is_gate:
shows "gate 2 (J⇧†)"
proof
show "dim_row (J⇧†) = 2⇧2"
using mat_of_cols_list_def by simp
moreover show "square_mat (J⇧†)"
using mat_of_cols_list_def by simp
moreover have "(J⇧†)⇧† = J"
using dagger_of_dagger_is_id by auto
ultimately show "unitary (J⇧†)"
using mat_of_cols_list_def unitary_def J_cnj_times_J J_times_J_cnj by auto
qed
lemma (in strategic_space_2p) psi_f_is_state:
shows "state 2 ψ⇩f"
proof-
have "state 2 ((J⇧†) * ψ⇩2)"
using psi_two_is_state J_cnj_is_gate by auto
then show ?thesis
using psi_f by simp
qed
lemma (in strategic_space_2p) equation_one:
shows "(J⇧†) * ((U⇩A ⨂ U⇩B) * (J * |unit_vec 4 0⟩)) = ψ⇩f"
using psi_one psi_two psi_f by auto
abbreviation (in strategic_space_2p) prob00 :: "complex Matrix.mat ⇒ real" where
"prob00 v ≡ if state 2 v then (cmod (v $$ (0,0)))⇧2 else undefined"
abbreviation (in strategic_space_2p) prob01 :: "complex Matrix.mat ⇒ real" where
"prob01 v ≡ if state 2 v then (cmod (v $$ (1,0)))⇧2 else undefined"
abbreviation (in strategic_space_2p) prob10 :: "complex Matrix.mat ⇒ real" where
"prob10 v ≡ if state 2 v then (cmod (v $$ (2,0)))⇧2 else undefined"
abbreviation (in strategic_space_2p) prob11 :: "complex Matrix.mat ⇒ real" where
"prob11 v ≡ if state 2 v then (cmod (v $$ (3,0)))⇧2 else undefined"
definition (in strategic_space_2p) alice_payoff :: "real" where
"alice_payoff ≡ 3 * (prob00 ψ⇩f) + 1 * (prob11 ψ⇩f) + 0 * (prob01 ψ⇩f) + 5 * (prob10 ψ⇩f)"
definition (in strategic_space_2p) bob_payoff :: "real" where
"bob_payoff ≡ 3 * (prob00 ψ⇩f) + 1 * (prob11 ψ⇩f) + 5 * (prob01 ψ⇩f) + 0 * (prob10 ψ⇩f)"
definition (in strategic_space_2p) is_nash_eq :: "bool" where
"is_nash_eq ≡
(∀tA pA. strategic_space_2p γ tA pA θ⇩B φ⇩B ⟶
alice_payoff ≥ strategic_space_2p.alice_payoff γ tA pA θ⇩B φ⇩B)
∧
(∀tB pB. strategic_space_2p γ θ⇩A φ⇩A tB pB ⟶
bob_payoff ≥ strategic_space_2p.bob_payoff γ θ⇩A φ⇩A tB pB)"
definition (in strategic_space_2p) is_pareto_opt :: "bool" where
"is_pareto_opt ≡ ∀tA pA tB pB. strategic_space_2p γ tA pA tB pB ⟶
((strategic_space_2p.alice_payoff γ tA pA tB pB > alice_payoff ⟶
strategic_space_2p.bob_payoff γ tA pA tB pB < bob_payoff) ∧
(strategic_space_2p.bob_payoff γ tA pA tB pB > bob_payoff ⟶
strategic_space_2p.alice_payoff γ tA pA tB pB < alice_payoff))"
lemma (in strategic_space_2p) sum_of_prob:
fixes v :: "complex Matrix.mat"
assumes "state 2 v"
shows "(prob00 v) + (prob11 v) + (prob01 v) + (prob10 v) = 1"
proof-
have "(prob00 v) + (prob11 v) + (prob01 v) + (prob10 v) =
(cmod (v $$ (0,0)))⇧2 + (cmod (v $$ (1,0)))⇧2 + (cmod (v $$ (2,0)))⇧2 + (cmod (v $$ (3,0)))⇧2"
using assms by auto
then show ?thesis
using state_def assms cpx_vec_length_def by (auto simp add: set_4)
qed
lemma (in strategic_space_2p) sum_payoff_le_6:
fixes tA pA tB pB :: real
shows "alice_payoff + bob_payoff ≤ 6"
proof-
have "alice_payoff + bob_payoff = 6 * (prob00 ψ⇩f) + 2 * (prob11 ψ⇩f) + 5 * (prob01 ψ⇩f) + 5 * (prob10 ψ⇩f)"
using alice_payoff_def bob_payoff_def psi_f_is_state by auto
then have "alice_payoff + bob_payoff ≤ 6 * ((prob00 ψ⇩f) + (prob11 ψ⇩f) + (prob01 ψ⇩f) + (prob10 ψ⇩f))"
using psi_f_is_state by (auto simp add: algebra_simps)
moreover have "(prob00 ψ⇩f) + (prob11 ψ⇩f) + (prob01 ψ⇩f) + (prob10 ψ⇩f) = 1"
using sum_of_prob[of "ψ⇩f"] psi_f_is_state by auto
ultimately show ?thesis
by auto
qed
lemma (in strategic_space_2p) coop_is_pareto_opt:
assumes "alice_payoff = 3 ∧ bob_payoff = 3"
shows "is_pareto_opt"
using is_pareto_opt_def strategic_space_2p.sum_payoff_le_6 assms by fastforce
subsection ‹The Separable Case›
lemma (in strategic_space_2p) separable_case_CC:
assumes "γ = 0"
shows "φ⇩A = 0 ∧ θ⇩A = 0 ∧ φ⇩B = 0 ∧ θ⇩B = 0 ⟶ alice_payoff = 3 ∧ bob_payoff = 3"
using alice_payoff_def bob_payoff_def cos_sin_squared_add_cpx psi_f_is_state by auto
lemma (in strategic_space_2p) separable_case_DD:
assumes "γ = 0"
shows "φ⇩A = 0 ∧ θ⇩A = pi ∧ φ⇩B = 0 ∧ θ⇩B = pi ⟶ alice_payoff = 1 ∧ bob_payoff = 1"
using alice_payoff_def bob_payoff_def cos_sin_squared_add_cpx psi_f_is_state by auto
lemma (in strategic_space_2p) separable_case_DC:
assumes "γ = 0"
shows "φ⇩A = 0 ∧ θ⇩A = pi ∧ φ⇩B = 0 ∧ θ⇩B = 0 ⟶ alice_payoff = 5 ∧ bob_payoff = 0"
using alice_payoff_def bob_payoff_def sin_cos_squared_add_cpx psi_f_is_state by auto
lemma (in strategic_space_2p) separable_alice_payoff_D⇩B:
assumes "γ = 0" and "φ⇩B = 0 ∧ θ⇩B = pi"
shows "alice_payoff ≤ 1"
using alice_payoff_def assms sin_squared_le_one psi_f_is_state by auto
lemma (in strategic_space_2p) separable_bob_payoff_D⇩A:
assumes "γ = 0" and "φ⇩A = 0 ∧ θ⇩A = pi"
shows "bob_payoff ≤ 1"
using bob_payoff_def assms sin_squared_le_one psi_f_is_state by auto
lemma (in strategic_space_2p) separable_case_DD_alice_opt:
assumes "γ = 0" and "φ⇩A = 0 ∧ θ⇩A = pi ∧ φ⇩B = 0 ∧ θ⇩B = pi"
shows "⋀tA pA. strategic_space_2p γ tA pA θ⇩B φ⇩B ⟶ strategic_space_2p.alice_payoff γ tA pA θ⇩B φ⇩B ≤ alice_payoff"
proof
fix tA pA assume "strategic_space_2p γ tA pA θ⇩B φ⇩B"
then show "strategic_space_2p.alice_payoff γ tA pA θ⇩B φ⇩B ≤ alice_payoff"
using separable_case_DD strategic_space_2p.separable_alice_payoff_D⇩B assms by auto
qed
lemma (in strategic_space_2p) separable_case_DD_bob_opt:
assumes "γ = 0" and "φ⇩A = 0 ∧ θ⇩A = pi ∧ φ⇩B = 0 ∧ θ⇩B = pi"
shows "⋀tB pB. strategic_space_2p γ θ⇩A φ⇩A tB pB ⟶ strategic_space_2p.bob_payoff γ θ⇩A φ⇩A tB pB ≤ bob_payoff"
proof
fix tB pB assume "strategic_space_2p γ θ⇩A φ⇩A tB pB"
then show "strategic_space_2p.bob_payoff γ θ⇩A φ⇩A tB pB ≤ bob_payoff"
using separable_case_DD strategic_space_2p.separable_bob_payoff_D⇩A assms by auto
qed
lemma (in strategic_space_2p) separable_case_DD_is_nash_eq:
assumes "γ = 0"
shows "φ⇩A = 0 ∧ θ⇩A = pi ∧ φ⇩B = 0 ∧ θ⇩B = pi ⟶ is_nash_eq"
using is_nash_eq_def separable_case_DD_alice_opt separable_case_DD_bob_opt assms by auto
lemma (in strategic_space_2p) separable_case_CC_is_not_nash_eq:
assumes "γ = 0"
shows "φ⇩A = 0 ∧ θ⇩A = 0 ∧ φ⇩B = 0 ∧ θ⇩B = 0 ⟶ ¬ is_nash_eq"
proof
assume asm:"φ⇩A = 0 ∧ θ⇩A = 0 ∧ φ⇩B = 0 ∧ θ⇩B = 0"
then have f0:"strategic_space_2p γ pi 0 θ⇩B φ⇩B"
using strategic_space_2p_def strategic_space_2p_axioms_def prisoner_def asm by (simp add: assms)
then have "strategic_space_2p.alice_payoff γ pi 0 θ⇩B φ⇩B = 5"
using strategic_space_2p.separable_case_DC assms asm by blast
moreover have "alice_payoff = 3"
using separable_case_CC assms asm by blast
ultimately have "strategic_space_2p γ pi 0 θ⇩B φ⇩B ∧ strategic_space_2p.alice_payoff γ pi 0 θ⇩B φ⇩B > alice_payoff"
using f0 by simp
then show "¬is_nash_eq"
using is_nash_eq_def by fastforce
qed
lemma (in strategic_space_2p) separable_case_CC_is_pareto_optimal:
assumes "γ = 0"
shows "φ⇩A = 0 ∧ θ⇩A = 0 ∧ φ⇩B = 0 ∧ θ⇩B = 0 ⟶ is_pareto_opt"
using coop_is_pareto_opt separable_case_CC assms by auto
subsection ‹The Maximally Entangled Case›
lemma exp_to_sin:
fixes x:: real
shows "exp (𝗂 * x) - exp (-(𝗂 * x)) = 2 * 𝗂 * (sin x)"
using exp_of_real exp_of_real_inv by simp
lemma exp_to_cos:
fixes x:: real
shows "exp (𝗂 * x) + exp (-(𝗂 * x)) = 2 * (cos x)"
using exp_of_real exp_of_real_inv by simp
lemma cmod_real_prod_squared:
fixes x y:: real
shows "(cmod (complex_of_real x * complex_of_real y))⇧2 = x⇧2 * y⇧2"
by (simp add: norm_mult power_mult_distrib)
lemma quantum_payoff_simp:
fixes x y:: real
shows "3 * (cmod (complex_of_real (sin x) * complex_of_real (cos y)))⇧2 +
(cmod (complex_of_real (cos x) * complex_of_real (cos y)))⇧2 =
2 * (sin x)⇧2 * (cos y)⇧2 + (cos y)⇧2"
proof-
have "3 * (sin x)⇧2 * (cos y)⇧2 + (cos x)⇧2 * (cos y)⇧2 =
(2 * (sin x)⇧2 * (cos y)⇧2) + ((sin x)⇧2 + (cos x)⇧2) * (cos y)⇧2"
by (auto simp add: algebra_simps simp del: sin_cos_squared_add2)
then show ?thesis
by (simp add: cmod_real_prod_squared power_mult_distrib)
qed
lemma quantum_payoff_le_3:
fixes x y:: real
shows "2 * (sin x)⇧2 * (cos y)⇧2 + (cos y)⇧2 ≤ 3"
proof-
have "(sin x)⇧2 * (cos y)⇧2 ≤ 1" by (simp add: sin_squared_le_one cos_squared_le_one mult_le_one)
then have "2 * (sin x)⇧2 * (cos y)⇧2 ≤ 2" by simp
moreover have "(cos y)⇧2 ≤ 1"
using cos_squared_le_one[of "y"] by simp
ultimately show ?thesis by simp
qed
lemma sqrt_two_squared_cpx: "complex_of_real (sqrt 2) * complex_of_real (sqrt 2) = 2"
by (metis mult_2_right numeral_Bit0 of_real_mult of_real_numeral real_sqrt_four real_sqrt_mult)
lemma hidden_sqrt_two_squared_cpx: "complex_of_real (sqrt 2) * (complex_of_real (sqrt 2) * x) / 4 = x/2"
using sqrt_two_squared_cpx by (auto simp add: algebra_simps)
lemma (in strategic_space_2p) max_entangled_DD:
assumes "γ = pi/2"
shows "φ⇩A = 0 ∧ θ⇩A = pi ∧ φ⇩B = 0 ∧ θ⇩B = pi ⟶ alice_payoff = 1 ∧ bob_payoff = 1"
using alice_payoff_def bob_payoff_def cos_sin_squared_add_cpx psi_f_is_state
by auto
lemma (in strategic_space_2p) max_entangled_QQ:
assumes "γ = pi/2"
shows "φ⇩A = pi/2 ∧ θ⇩A = 0 ∧ φ⇩B = pi/2 ∧ θ⇩B = 0 ⟶ alice_payoff = 3 ∧ bob_payoff = 3"
using alice_payoff_def bob_payoff_def sin_cos_squared_add_cpx exp_of_half_pi exp_of_minus_half_pi psi_f_is_state
by auto
lemma (in strategic_space_2p) max_entangled_QD:
assumes "γ = pi/2"
shows "φ⇩A = pi/2 ∧ θ⇩A = 0 ∧ φ⇩B = 0 ∧ θ⇩B = pi ⟶ alice_payoff = 5 ∧ bob_payoff = 0"
using alice_payoff_def bob_payoff_def cos_sin_squared_add_cpx exp_of_half_pi exp_of_minus_half_pi
psi_f_is_state sqrt_two_squared_cpx
by (auto simp add: assms algebra_simps sin_45 cos_45)
lemma (in strategic_space_2p) max_entangled_alice_payoff_Q⇩B:
assumes "γ = pi/2"
shows "φ⇩B = pi/2 ∧ θ⇩B = 0 ⟶ alice_payoff ≤ 3"
proof
assume asm:"φ⇩B = pi/2 ∧ θ⇩B = 0"
have "ψ⇩f $$ (0,0) = -(sin φ⇩A) * (cos (θ⇩A/2))"
proof-
have "ψ⇩f $$ (0,0) = 𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θ⇩A/2)) * exp (𝗂 * φ⇩A) +
𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θ⇩A/2)) * -exp (-(𝗂 * φ⇩A))"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
then have "ψ⇩f $$ (0,0) = 𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θ⇩A/2)) * (exp (𝗂 * φ⇩A) - exp (-(𝗂 * φ⇩A)))"
by (auto simp add: algebra_simps)
then have "ψ⇩f $$ (0,0) = 𝗂 * (cos (θ⇩A/2)) * (1/2) * (exp (𝗂 * φ⇩A) - exp (-(𝗂 * φ⇩A)))"
using sqrt_two_squared_cpx by (auto simp add: algebra_simps)
then show ?thesis
using exp_to_sin by (simp add: algebra_simps)
qed
moreover have "ψ⇩f $$ (1,0) = sin (θ⇩A/2)"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi sqrt_two_squared_cpx
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"])
moreover have "ψ⇩f $$ (2,0) = 0"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi sqrt_two_squared_cpx
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
moreover have "ψ⇩f $$ (3,0) = (cos φ⇩A) * (cos (θ⇩A/2))"
proof-
have "ψ⇩f $$ (3,0) = exp (𝗂 * φ⇩A) * (cos (θ⇩A/2)) * (sqrt 2/2) * (sqrt 2/2) +
exp (- (𝗂 * φ⇩A)) * (cos (θ⇩A/2)) * (sqrt 2/2) * (sqrt 2/2)"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
then have "ψ⇩f $$ (3,0) = (exp (𝗂 * φ⇩A) + exp (-(𝗂 * φ⇩A))) * (cos (θ⇩A/2)) * (sqrt 2/2) * (sqrt 2/2)"
by (auto simp add: algebra_simps)
then have "ψ⇩f $$ (3,0) = (exp (𝗂 * φ⇩A) + exp (-(𝗂 * φ⇩A))) * (cos (θ⇩A/2)) * (1/2)"
using sqrt_two_squared_cpx hidden_sqrt_two_squared_cpx by (auto simp add: algebra_simps)
then show ?thesis
using exp_to_cos by (simp add: algebra_simps)
qed
ultimately show "alice_payoff ≤ 3"
using alice_payoff_def psi_f_is_state quantum_payoff_simp quantum_payoff_le_3
by auto
qed
lemma (in strategic_space_2p) max_entangled_bob_payoff_Q⇩A:
assumes "γ = pi/2"
shows "φ⇩A = pi/2 ∧ θ⇩A = 0 ⟶ bob_payoff ≤ 3"
proof
assume asm:"φ⇩A = pi/2 ∧ θ⇩A = 0"
have "ψ⇩f $$ (0,0) = -(sin φ⇩B) * (cos (θ⇩B/2))"
proof-
have "ψ⇩f $$ (0,0) = 𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θ⇩B/2)) * exp (𝗂 * φ⇩B) +
𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θ⇩B/2)) * -exp (-(𝗂 * φ⇩B))"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
then have "ψ⇩f $$ (0,0) = 𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θ⇩B/2)) * (exp (𝗂 * φ⇩B) - exp (-(𝗂 * φ⇩B)))"
by (auto simp add: algebra_simps)
then have "ψ⇩f $$ (0,0) = 𝗂 * (cos (θ⇩B/2)) * (1/2) * (exp (𝗂 * φ⇩B) - exp (-(𝗂 * φ⇩B)))"
using sqrt_two_squared_cpx by (auto simp add: algebra_simps)
then show ?thesis
using exp_to_sin by (simp add: algebra_simps)
qed
moreover have "ψ⇩f $$ (1,0) = 0"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi sqrt_two_squared_cpx
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
moreover have "ψ⇩f $$ (2,0) = sin (θ⇩B/2)"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi sqrt_two_squared_cpx
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
moreover have "ψ⇩f $$ (3,0) = (cos φ⇩B) * (cos (θ⇩B/2))"
proof-
have "ψ⇩f $$ (3,0) = exp (𝗂 * φ⇩B) * (cos (θ⇩B/2)) * (sqrt 2/2) * (sqrt 2/2) +
exp (- (𝗂 * φ⇩B)) * (cos (θ⇩B/2)) * (sqrt 2/2) * (sqrt 2/2)"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
then have "ψ⇩f $$ (3,0) = (exp (𝗂 * φ⇩B) + exp (-(𝗂 * φ⇩B))) * (cos (θ⇩B/2)) * (sqrt 2/2) * (sqrt 2/2)"
by (auto simp add: algebra_simps)
then have "ψ⇩f $$ (3,0) = (exp (𝗂 * φ⇩B) + exp (-(𝗂 * φ⇩B))) * (cos (θ⇩B/2)) * (1/2)"
using sqrt_two_squared_cpx hidden_sqrt_two_squared_cpx by (auto simp add: algebra_simps)
then show ?thesis
using exp_to_cos by (simp add: algebra_simps)
qed
ultimately show "bob_payoff ≤ 3"
using bob_payoff_def psi_f_is_state quantum_payoff_simp quantum_payoff_le_3
by auto
qed
lemma (in strategic_space_2p) max_entangled_DD_is_not_nash_eq:
assumes "γ = pi/2"
shows "φ⇩A = 0 ∧ θ⇩A = pi ∧ φ⇩B = 0 ∧ θ⇩B = pi ⟶ ¬is_nash_eq"
proof
assume asm:"φ⇩A = 0 ∧ θ⇩A = pi ∧ φ⇩B = 0 ∧ θ⇩B = pi"
then have f0:"strategic_space_2p γ 0 (pi/2) θ⇩B φ⇩B"
using strategic_space_2p_def strategic_space_2p_axioms_def prisoner_def asm by (simp add: assms)
then have "strategic_space_2p.alice_payoff γ 0 (pi/2) θ⇩B φ⇩B = 5"
using strategic_space_2p.max_entangled_QD assms asm by blast
moreover have "alice_payoff = 1"
using max_entangled_DD assms asm by blast
ultimately have "strategic_space_2p γ 0 (pi/2) θ⇩B φ⇩B ∧ strategic_space_2p.alice_payoff γ 0 (pi/2) θ⇩B φ⇩B > alice_payoff"
using f0 by simp
then show "¬is_nash_eq"
using is_nash_eq_def by fastforce
qed
lemma (in strategic_space_2p) max_entangled_alice_opt:
assumes "γ = pi/2" and "φ⇩A = pi/2 ∧ θ⇩A = 0 ∧ φ⇩B = pi/2 ∧ θ⇩B = 0"
shows "⋀tA pA. strategic_space_2p γ tA pA θ⇩B φ⇩B ⟶ strategic_space_2p.alice_payoff γ tA pA θ⇩B φ⇩B ≤ alice_payoff"
proof
fix tA pA assume "strategic_space_2p γ tA pA θ⇩B φ⇩B"
then have "strategic_space_2p.alice_payoff γ tA pA θ⇩B φ⇩B ≤ 3"
using strategic_space_2p.max_entangled_alice_payoff_Q⇩B assms by blast
moreover have "alice_payoff = 3"
using max_entangled_QQ assms by blast
ultimately show "strategic_space_2p.alice_payoff γ tA pA θ⇩B φ⇩B ≤ alice_payoff"
by simp
qed
lemma (in strategic_space_2p) max_entangled_bob_opt:
assumes "γ = pi/2" and "φ⇩A = pi/2 ∧ θ⇩A = 0 ∧ φ⇩B = pi/2 ∧ θ⇩B = 0"
shows "⋀tB pB. strategic_space_2p γ θ⇩A φ⇩A tB pB ⟶ strategic_space_2p.bob_payoff γ θ⇩A φ⇩A tB pB ≤ bob_payoff"
proof
fix tB pB assume "strategic_space_2p γ θ⇩A φ⇩A tB pB"
then have "strategic_space_2p.bob_payoff γ θ⇩A φ⇩A tB pB ≤ 3"
using strategic_space_2p.max_entangled_bob_payoff_Q⇩A assms by blast
moreover have "bob_payoff = 3"
using max_entangled_QQ assms by blast
ultimately show "strategic_space_2p.bob_payoff γ θ⇩A φ⇩A tB pB ≤ bob_payoff"
by simp
qed
lemma (in strategic_space_2p) max_entangled_QQ_is_nash_eq:
assumes "γ = pi/2"
shows "φ⇩A = pi/2 ∧ θ⇩A = 0 ∧ φ⇩B = pi/2 ∧ θ⇩B = 0 ⟶ is_nash_eq"
using max_entangled_alice_opt max_entangled_bob_opt is_nash_eq_def assms by blast
lemma (in strategic_space_2p) max_entangled_QQ_is_pareto_optimal:
assumes "γ = pi/2"
shows "φ⇩A = pi/2 ∧ θ⇩A = 0 ∧ φ⇩B = pi/2 ∧ θ⇩B = 0 ⟶ is_pareto_opt"
using coop_is_pareto_opt max_entangled_QQ assms by blast
subsection ‹The Unfair Strategy Case›
lemma half_sqrt_two_squared: "2 * (sqrt 2 / 2)⇧2 = 1"
by (auto simp add: power2_eq_square)
lemma (in strategic_space_2p) max_entangled_MD:
assumes "γ = pi/2"
shows "φ⇩A = pi/2 ∧ θ⇩A = pi/2 ∧ φ⇩B = 0 ∧ θ⇩B = pi ⟶ alice_payoff = 3 ∧ bob_payoff = 1/2"
proof
assume asm:"φ⇩A = pi/2 ∧ θ⇩A = pi/2 ∧ φ⇩B = 0 ∧ θ⇩B = pi"
show "alice_payoff = 3 ∧ bob_payoff = 1/2"
using alice_payoff_def bob_payoff_def sqrt_two_squared_cpx half_sqrt_two_squared
exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"] psi_f_is_state
by (auto simp add: asm assms sin_45 cos_45 algebra_simps)
qed
lemma (in strategic_space_2p) max_entangled_MC:
assumes "γ = pi/2"
shows "φ⇩A = pi/2 ∧ θ⇩A = pi/2 ∧ φ⇩B = 0 ∧ θ⇩B = 0 ⟶ alice_payoff = 3 ∧ bob_payoff = 1/2"
proof
assume asm:"φ⇩A = pi/2 ∧ θ⇩A = pi/2 ∧ φ⇩B = 0 ∧ θ⇩B = 0"
show "alice_payoff = 3 ∧ bob_payoff = 1/2"
using alice_payoff_def bob_payoff_def sqrt_two_squared_cpx half_sqrt_two_squared
exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"] psi_f_is_state
by (auto simp add: asm assms sin_45 cos_45 algebra_simps)
qed
lemma (in strategic_space_2p) max_entangled_MH:
assumes "γ = pi/2"
shows "φ⇩A = pi/2 ∧ θ⇩A = pi/2 ∧ φ⇩B = 0 ∧ θ⇩B = pi/2 ⟶ alice_payoff = 1 ∧ bob_payoff = 1"
proof
assume asm:"φ⇩A = pi/2 ∧ θ⇩A = pi/2 ∧ φ⇩B = 0 ∧ θ⇩B = pi/2"
show "alice_payoff = 1 ∧ bob_payoff = 1"
using alice_payoff_def bob_payoff_def sqrt_two_squared_cpx half_sqrt_two_squared
exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"] psi_f_is_state
by (auto simp add: asm assms sin_45 cos_45 algebra_simps)
qed
abbreviation M :: "complex Matrix.mat" where
"M ≡ mat_of_cols_list 2 [[𝗂 * sqrt(2)/2, -1 * sqrt(2)/2],
[1 * sqrt(2)/2, -𝗂 * sqrt(2)/2]]"
lemma (in strategic_space_2p) M_correct:
assumes "φ⇩A = pi/2 ∧ θ⇩A = pi/2"
shows "U⇩A = M"
proof
show "dim_row U⇩A = dim_row M" using mat_of_cols_list_def by simp
show "dim_col U⇩A = dim_col M" using mat_of_cols_list_def by simp
fix i j assume a0:"i < dim_row M" and a1:"j < dim_col M"
then show "U⇩A $$ (i,j) = M $$ (i,j)"
proof-
have "i∈{0,1} ∧ j∈{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"]
by (auto simp add: assms sin_45 cos_45)
qed
qed
lemma hidden_sqrt_two_squared_cpx2:
fixes x y :: complex
shows "(sqrt 2) * ((sqrt 2) * (x * y)) / 2 = x * y"
using sqrt_two_squared_cpx by auto
lemma (in strategic_space_2p) unfair_strategy_no_benefit:
assumes "γ = pi/2"
shows "φ⇩A = pi/2 ∧ φ⇩B = 0 ∧ θ⇩A = θ⇩B ⟶ alice_payoff = 1 ∧ bob_payoff = 1"
proof
assume asm:"φ⇩A = pi/2 ∧ φ⇩B = 0 ∧ θ⇩A = θ⇩B"
have "ψ⇩f $$ (0,0) = 0"
using exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"]
by (auto simp add: asm assms sin_45 cos_45 algebra_simps)
moreover have "ψ⇩f $$ (1,0) = 0"
using exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"]
by (auto simp add: asm assms sin_45 cos_45 algebra_simps)
moreover have "ψ⇩f $$ (2,0) = 0"
using exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"]
by (auto simp add: asm assms sin_45 cos_45 hidden_sqrt_two_squared_cpx2 algebra_simps)
moreover have "ψ⇩f $$ (3,0) = 1"
using exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"] cos_sin_squared_add_cpx
by (auto simp add: asm assms sin_45 cos_45 hidden_sqrt_two_squared_cpx2 algebra_simps)
ultimately show "alice_payoff = 1 ∧ bob_payoff = 1"
using alice_payoff_def bob_payoff_def psi_f_is_state
by auto
qed
end