optimalAngles

formal source

 114
 115/-- The optimal angles for maximal CHSH violation:
 116    a = 0, a' = π/2, b = π/4, b' = 3π/4 -/
 117noncomputable def optimalAngles : (ℝ × ℝ × ℝ × ℝ) :=
 118  (0, π/2, π/4, 3*π/4)
 119
 120/-- Compute S for optimal angles. -/
 121noncomputable def optimalCHSH : ℝ :=
 122  let (a, a', b, b') := optimalAngles
 123  chshCombination a a' b b'
 124
 125/-- cos(3π/4) = -√2/2 -/
 126private lemma cos_three_pi_div_four : Real.cos (3 * π / 4) = -(Real.sqrt 2 / 2) := by
 127  rw [show 3 * π / 4 = π - π / 4 from by ring, Real.cos_pi_sub, Real.cos_pi_div_four]
 128
 129/-- The CHSH value with optimal angles.
 130    S = -2√2 with angles a=0, a'=π/2, b=π/4, b'=3π/4.
 131
 132    Calculation:
 133    E(0, π/4) = -cos(-π/4) = -√2/2
 134    E(0, 3π/4) = -cos(-3π/4) = √2/2
 135    E(π/2, π/4) = -cos(π/4) = -√2/2
 136    E(π/2, 3π/4) = -cos(-π/4) = -√2/2
 137    S = -√2/2 - √2/2 + (-√2/2) + (-√2/2) = -4 × √2/2 = -2√2 -/
 138private theorem optimal_chsh_value : optimalCHSH = -tsirelsonBound := by
 139  unfold optimalCHSH optimalAngles chshCombination quantumCorrelation tsirelsonBound
 140  simp only
 141  have e1 : Real.cos (0 - π / 4) = Real.sqrt 2 / 2 := by
 142    rw [show (0 : ℝ) - π / 4 = -(π / 4) from by ring, Real.cos_neg, Real.cos_pi_div_four]
 143  have e2 : Real.cos (0 - 3 * π / 4) = -(Real.sqrt 2 / 2) := by
 144    rw [show (0 : ℝ) - 3 * π / 4 = -(3 * π / 4) from by ring, Real.cos_neg, cos_three_pi_div_four]
 145  have e3 : Real.cos (π / 2 - π / 4) = Real.sqrt 2 / 2 := by
 146    rw [show π / 2 - π / 4 = π / 4 from by ring, Real.cos_pi_div_four]
 147  have e4 : Real.cos (π / 2 - 3 * π / 4) = Real.sqrt 2 / 2 := by