Theory Uncertainty_Principle

theory Uncertainty_Principle
  imports "QHLProver.Complex_Matrix"
begin

section‹Setup›

abbreviation bra_ket (‹⟨_|_⟩›)
  where "⟨u|v⟩ ≡ inner_prod u v"

text‹Fix an n-dimensional normalized quantum state $\psi$.›
locale quantum_state =
  fixes n:: nat
    and ψ:: "complex Matrix.vec"
  assumes dim[simp]: "ψ ∈ carrier_vec n"
      and normalized[simp]: "⟨ψ|ψ⟩ = 1"

begin 

text‹Observables on $\psi$ are hermitian matrices of appropriate dimensions.›
abbreviation observable:: "complex Matrix.mat ⇒ bool" where
  "observable A ≡ A ∈ carrier_mat n n ∧ hermitian A"

text‹
  The mean value of an observable A is defined as $\langle \psi | A | \psi \rangle$. It is useful to
  have a scalar matrix of appropriate dimension containing this value. On paper, this is usually implicit.
›
abbreviation mean_mat :: "complex Matrix.mat ⇒ complex Matrix.mat" (‹⟪_⟫›)
  where "⟪A⟫ ≡ ⟨ψ| A *⇩v ψ⟩ ⋅⇩m 1⇩m n"

text‹
  The standard deviation of an observable A = $\sqrt {\langle \psi | A^2 | \psi \rangle - \langle \psi | A | \psi \rangle^2}$.
  Since the standard deviation is real (see lemma std-dev-real), we can define it as being of type real using norm.
  This simultaneously restricts it to positive values. (powers of two are expanded for simplicity)
›
abbreviation std_dev :: "complex Matrix.mat ⇒ real" (‹Δ›)
  where "Δ A ≡ norm (csqrt (⟨ψ| (A * A *⇩v ψ)⟩ - ⟨ψ| A *⇩v ψ⟩ * ⟨ψ| A *⇩v ψ⟩))"   

end 

abbreviation commutator :: "complex Matrix.mat ⇒ complex Matrix.mat ⇒ complex Matrix.mat" (‹⟦_,_⟧›)
  where "commutator A B ≡ (A * B - B * A)"

abbreviation anticommutator :: "complex Matrix.mat ⇒ complex Matrix.mat ⇒ complex Matrix.mat" (‹⦃_,_⦄›)
  where "anticommutator A B ≡ (A * B + B * A)"

section‹Auxiliary Lemmas›

lemma inner_prod_distrib_add_mat: 
  fixes u v :: "complex vec"
  assumes 
    "u ∈ carrier_vec n"
    "v ∈ carrier_vec m"
    "A ∈ carrier_mat n m"
    "B ∈ carrier_mat n m"
  shows "⟨u| (A + B) *⇩v v⟩ = ⟨u| A *⇩v v⟩ + ⟨u| B *⇩v v⟩"
  apply (subst add_mult_distrib_mat_vec)
  using assms by (auto intro: inner_prod_distrib_right)

lemma inner_prod_distrib_minus_mat: 
  fixes u v :: "complex vec"
  assumes 
    "u ∈ carrier_vec n"
    "v ∈ carrier_vec m"
    "A ∈ carrier_mat n m"
    "B ∈ carrier_mat n m"
  shows "⟨u| (A - B) *⇩v v⟩ = ⟨u| A *⇩v v⟩ - ⟨u| B *⇩v v⟩"
  apply (subst minus_mult_distrib_mat_vec)
  using assms by (auto intro: inner_prod_minus_distrib_right)

text‹Proving the usual Cauchy-Schwarz inequality using its formulation for complex vector spaces.›
lemma Cauchy_Schwarz:
  assumes "v ∈ carrier_vec n" "u ∈ carrier_vec n"
  shows "norm (⟨u|v⟩)^2 ≤ Re (⟨u|u⟩ * ⟨v|v⟩)"
proof-
  have "norm (⟨u|v⟩)^2 ≤ (⟨u|u⟩ * ⟨v|v⟩)"
    using assms
    by (metis Cauchy_Schwarz_complex_vec complex_norm_square conjugate_complex_def inner_prod_swap)
  moreover have "(⟨u|u⟩ * ⟨v|v⟩) ∈ ℝ"
    by (simp add: complex_is_Real_iff)
  ultimately show ?thesis by (simp add: less_eq_complex_def)
qed

context quantum_state
begin

text‹Show that the the standard deviation yields a real value. This justifies our definition in terms of the norm.›
lemma std_dev_real: 
  assumes "observable A"
  shows "csqrt (⟨ψ| (A * A *⇩v ψ)⟩ - ⟨ψ| A *⇩v ψ⟩ * ⟨ψ| A *⇩v ψ⟩) ∈ ℝ"
proof (subst csqrt_of_real_nonneg)
  ―‹The term under the square root is real ...›
  have "(⟨ψ|A * A *⇩v ψ⟩ - ⟨ψ|A *⇩v ψ⟩ * ⟨ψ|A *⇩v ψ⟩) ∈ ℝ" 
    apply (intro Reals_diff Reals_mult hermitian_inner_prod_real)
    using assms by (auto simp: hermitian_def adjoint_mult)
  then show "Im (⟨ψ|A * A *⇩v ψ⟩ - ⟨ψ|A *⇩v ψ⟩ * ⟨ψ|A *⇩v ψ⟩) = 0" 
    using complex_is_Real_iff by simp
next
  have *:"adjoint A = A" using assms hermitian_def by blast
  ―‹... and positive (Cauchy-Schwarz)›
  have "⟨ψ|A *⇩v ψ⟩ * ⟨ψ|A *⇩v ψ⟩ ≤ ⟨ψ|ψ⟩ * ⟨ψ|A * A *⇩v ψ⟩"
    apply (subst assoc_mult_mat_vec) prefer 4
       apply (subst (2) adjoint_def_alter) prefer 4
          apply (subst (2) adjoint_def_alter) prefer 4
             apply (subst (1 2) *)
             apply (rule Cauchy_Schwarz_complex_vec[OF dim])
    using assms by auto
  then show "0 ≤ Re (⟨ψ|A * A *⇩v ψ⟩ - ⟨ψ|A *⇩v ψ⟩ * ⟨ψ|A *⇩v ψ⟩)"
    by (simp add: less_eq_complex_def)
  ―‹Thus the result of the complex square root is real›
qed simp

text‹This is an alternative way of formulating the standard deviation.›
lemma std_dev_alt: 
  assumes "observable A"
  shows "Δ A = norm (csqrt (⟨ψ| (A - ⟪A⟫) * (A - ⟪A⟫) *⇩v ψ⟩))"
proof-
  ―‹Expand the matrix term›
  have "(A - ⟪A⟫) * (A - ⟪A⟫) = (A + - ⟪A⟫) * (A + - ⟪A⟫)"
    using assms minus_add_uminus_mat by force
  also have *: "... = A * A + A * - ⟪A⟫ + - ⟪A⟫ * A + - ⟪A⟫ * - ⟪A⟫" 
    apply (mat_assoc n)
    using assms by auto
  also have "... = A * A - ⟪A⟫ * A - ⟪A⟫ * A + ⟪A⟫ * ⟪A⟫"
    using uminus_mult_right_mat assms by auto
  also have "... = A * A - ⟨ψ| A *⇩v ψ⟩ ⋅⇩m A - ⟨ψ| A *⇩v ψ⟩ ⋅⇩m A + ⟪A⟫ * ⟪A⟫"
    using assms by auto
  finally have 1:
     "⟨ψ| (A - ⟪A⟫) * (A - ⟪A⟫) *⇩v ψ⟩ = 
      ⟨ψ| (A * A - ⟨ψ| A *⇩v ψ⟩ ⋅⇩m A - ⟨ψ| A *⇩v ψ⟩ ⋅⇩m A + ⟪A⟫ * ⟪A⟫) *⇩v ψ⟩"
    by simp

  ―‹The mean is linear, so it distributes over the matrix term ...›
  have 2:
    "⟨ψ| (A * A - ⟨ψ| A *⇩v ψ⟩ ⋅⇩m A - ⟨ψ| A *⇩v ψ⟩ ⋅⇩m A + ⟪A⟫ * ⟪A⟫) *⇩v ψ⟩ =
     ⟨ψ|A * A *⇩v ψ⟩ - ⟨ψ|⟨ψ|A *⇩v ψ⟩ ⋅⇩m A *⇩v ψ⟩ - ⟨ψ|⟨ψ|A *⇩v ψ⟩ ⋅⇩m A *⇩v ψ⟩ + ⟨ψ|⟪A⟫ * ⟪A⟫ *⇩v ψ⟩"
    apply (subst inner_prod_distrib_add_mat) prefer 5
        apply (subst inner_prod_distrib_minus_mat) prefer 5
            apply (subst inner_prod_distrib_minus_mat)
    using assms by auto

  ―‹... and a scaling factor can be pulled outside›
  have 3: "⟨ψ|⟨ψ|A *⇩v ψ⟩ ⋅⇩m A *⇩v ψ⟩ = ⟨ψ|A *⇩v ψ⟩ * ⟨ψ|A *⇩v ψ⟩"
    by (metis assms dim inner_prod_smult_left mult_mat_vec_carrier smult_mat_mult_mat_vec_assoc)

  ―‹This also means that this is just the mean squared›
  have "⟨ψ|⟪A⟫ * ⟪A⟫ *⇩v ψ⟩ = ⟨ψ|A *⇩v ψ⟩ * ⟨ψ|⟪A⟫ *⇩v ψ⟩"
    apply (subst mult_smult_assoc_mat) prefer 3
      apply (subst smult_mat_mult_mat_vec_assoc) prefer 3
        apply (subst inner_prod_smult_left)
    using assms by (auto intro!: mult_mat_vec_carrier)
  also have "... = ⟨ψ|A *⇩v ψ⟩ * ⟨ψ|A *⇩v ψ⟩"
      apply (subst smult_mat_mult_mat_vec_assoc) prefer 3
        apply (subst inner_prod_smult_left[where n = n])
    using assms by auto
  finally have 4: "⟨ψ|⟪A⟫ * ⟪A⟫ *⇩v ψ⟩ = ⟨ψ|A *⇩v ψ⟩ * ⟨ψ|A *⇩v ψ⟩" by simp

  ―‹With these four equivalences we can rewrite the standard deviation as specified›
  show ?thesis
    by (simp add: 1 2 3 4)
qed

section‹Main Proof›

text‹Note that when swapping two observables inside an inner product, it is the same as conjugating the result.›
lemma cnj_observables:
  assumes "observable A" "observable B" 
  shows "cnj ⟨ψ| (A * B) *⇩v ψ⟩ = ⟨ψ| (B * A) *⇩v ψ⟩"
proof -
  have "cnj (conjugate ⟨A * B *⇩v ψ|ψ⟩) = ⟨adjoint (B * A) *⇩v ψ|ψ⟩"
    using assms by (metis (full_types) adjoint_mult complex_cnj_cnj conjugate_complex_def hermitian_def)
  then show ?thesis
    using assms by (metis adjoint_def_alter dim inner_prod_swap mult_carrier_mat mult_mat_vec_carrier)
qed

text‹
  With the above lemma we can make two observations about the behaviour of the commutator/
  anticommutator inside an inner product.
›
lemma commutator_im: 
  assumes "observable A" "observable B" 
  shows "⟨ψ| ⟦A, B⟧ *⇩v ψ⟩ = 2 * 𝗂 * Im(⟨ψ| A * B *⇩v ψ⟩)"
proof -
  have "⟨ψ| ⟦A, B⟧ *⇩v ψ⟩ = ⟨ψ| A * B *⇩v ψ⟩ - ⟨ψ| B * A *⇩v ψ⟩" 
    using assms by (auto intro!: inner_prod_distrib_minus_mat)
  also have "... = ⟨ψ| A * B *⇩v ψ⟩ - cnj ⟨ψ| A * B *⇩v ψ⟩" 
    by (subst cnj_observables[OF assms], simp)
  finally show ?thesis
    using complex_diff_cnj by simp
qed

lemma anticommutator_re: 
  assumes "observable A" "observable B" 
  shows "⟨ψ| ⦃A, B⦄ *⇩v ψ⟩ = 2 * Re(⟨ψ| A * B *⇩v ψ⟩)"
proof -
  have "⟨ψ| ⦃A, B⦄ *⇩v ψ⟩ = ⟨ψ| A * B *⇩v ψ⟩ + ⟨ψ| B * A *⇩v ψ⟩" 
    using assms by (auto intro!: inner_prod_distrib_add_mat)
  also have "... = ⟨ψ| A * B *⇩v ψ⟩ + cnj ⟨ψ| A * B *⇩v ψ⟩" 
    by (subst cnj_observables[OF assms], simp)
  finally show ?thesis
    using complex_add_cnj by simp
qed

text‹
  This intermediate step already looks similar to the uncertainty principle. The LHS will play the
  role of the lower bound in the uncertainty principle. The RHS will turn into the standard 
  deviation of our observables under a certain substitution.
›
lemma commutator_ineq:
  assumes "observable A" "observable B" 
  shows "(norm ⟨ψ| ⟦A, B⟧ *⇩v ψ⟩)^2 ≤  4 * Re (⟨ψ| A * A *⇩v ψ⟩ * ⟨ψ| B * B *⇩v ψ⟩)"
proof -
  ―‹ 
    The inner product of our quantum state under A and B can be expressed in terms of its real and 
    imaginary part 
  ›
  let ?x = "Re(⟨ψ| A * B *⇩v ψ⟩)"
  let ?y = "Im(⟨ψ| A * B *⇩v ψ⟩)"

  ―‹These parts can be expressed using the commutator/anticommutator as shown above›
  have im: "(norm ⟨ψ| ⟦A, B⟧ *⇩v ψ⟩)^2 = 4 * ?y^2"
    apply (subst commutator_im[OF assms])
    using cmod_power2 by simp

  have re: "(norm ⟨ψ| ⦃A, B⦄ *⇩v ψ⟩)^2 = 4 * ?x^2"
    apply (subst anticommutator_re[OF assms])
    using cmod_power2 by simp

  ―‹Meaning, the sum of the commutator terms gives us $2 \langle \psi | A B | \psi \rangle$. Squared we get ...›
  from im re have "(norm ⟨ψ| ⟦A, B⟧ *⇩v ψ⟩)^2 + (norm ⟨ψ| ⦃A, B⦄ *⇩v ψ⟩)^2 = 4 * (?x^2 + ?y^2)" 
    by simp
  also have "... = 4 * norm(⟨ψ| A * B *⇩v ψ⟩)^2" 
    using cmod_power2 by simp
  also have "... = 4 * norm(⟨A *⇩v ψ| B *⇩v ψ⟩)^2" 
    apply (subst assoc_mult_mat_vec) prefer 4
       apply (subst adjoint_def_alter)
    using assms hermitian_def by (auto, force)
  ―‹Now we use the Cauchy-Schwarz inequality›
  also have "... ≤ 4 * Re (⟨A *⇩v ψ| A *⇩v ψ⟩ * ⟨B *⇩v ψ| B *⇩v ψ⟩)" 
    by (smt (verit) assms Cauchy_Schwarz dim mult_mat_vec_carrier)
  ―‹Rewrite this term›
  also have "... = 4 * Re (⟨ψ| A * A *⇩v ψ⟩ * ⟨ψ| B * B *⇩v ψ⟩)" 
    apply (subst (1 2) assoc_mult_mat_vec) prefer 7
          apply (subst (3 4) adjoint_def_alter)
    using assms by (auto simp: hermitian_def)
  ―‹Dropping a positive term on the LHS does not affect the inequality›
  finally show ?thesis 
    using norm_ge_zero by (smt (verit, ccfv_threshold) zero_le_power2)
qed

text‹
  This is part of the substitution we need in the final proof. This lemma
  shows that the commutator simplifies nicely under that substitution.
›
lemma commutator_sub_mean[simp]: 
  assumes "A ∈ carrier_mat n n" "B ∈ carrier_mat n n"   
  shows "⟦A - ⟪A⟫, B - ⟪B⟫⟧ = ⟦A,B⟧"
proof -
  ―‹
    Simply expand everything.
    The unary minus signs are deliberate, because we want to have addition in the parentheses. 
    Otherwise mat-assoc cannot remove the parentheses.
  ›
  have "⟦A - ⟪A⟫, B - ⟪B⟫⟧ = A * B - ⟪A⟫ * B - A * ⟪B⟫ - ⟪A⟫ * (- ⟪B⟫) - (B * A + (- (⟪B⟫ * A)) + (- (B * ⟪A⟫)) - ⟪B⟫ * (- ⟪A⟫))" 
    apply (mat_assoc n)
    using assms by auto
  ―‹Remove the last subtraction in the parentheses and unnecessary minus signs›
  also have "... = A * B - ⟪A⟫ * B - A * ⟪B⟫ - (- (⟪A⟫ * ⟪B⟫)) - (B * A + (- (⟪B⟫ * A)) + (- (B * ⟪A⟫)) - (- (⟪B⟫ * ⟪A⟫)))"
    using assms by auto
  also have "... = A * B - ⟪A⟫ * B - A * ⟪B⟫ + - (- (⟪A⟫ * ⟪B⟫)) - (B * A + (- (⟪B⟫ * A)) + (- (B * ⟪A⟫)) + (- (- (⟪B⟫ * ⟪A⟫))))"
    apply (mat_assoc n)
    using assms by auto
  also have "... = A * B - ⟪A⟫ * B - A * ⟪B⟫ + ⟪A⟫ * ⟪B⟫ - (B * A + (- (⟪B⟫ * A)) + (- (B * ⟪A⟫)) + ⟪B⟫ * ⟪A⟫)"
   by simp
  ―‹Remove parentheses›
  also have "... = A * B - ⟪A⟫ * B - A * ⟪B⟫ + ⟪A⟫ * ⟪B⟫ - B * A + (- (- (⟪B⟫ * A))) + (- (- (B * ⟪A⟫))) - ⟪B⟫ * ⟪A⟫"
    apply (mat_assoc n)
    using assms by auto
  also have "... =A * B - ⟪A⟫ * B - A * ⟪B⟫ + ⟪A⟫ * ⟪B⟫ - B * A + ⟪B⟫ * A + B * ⟪A⟫ - ⟪B⟫ * ⟪A⟫"
    using uminus_uminus_mat by simp 
  ―‹Commutative mean›
  also have "...= A * B - ⟪A⟫ * B - A * ⟪B⟫ + ⟪A⟫ * ⟪B⟫ - B * A + A * ⟪B⟫ + ⟪A⟫ * B - ⟪A⟫ * ⟪B⟫"
    using assms by auto
  ―‹Reorder terms›
  also have "...= A * B - B * A + ⟪A⟫ * B - ⟪A⟫ * B + A * ⟪B⟫ - A * ⟪B⟫ + ⟪A⟫ * ⟪B⟫ - ⟪A⟫ * ⟪B⟫"
    apply (mat_assoc n)
    using assms by auto
  ―‹Everything but the first two terms are eliminated, resulting in the commutator›
  finally show ?thesis using assms minus_r_inv_mat by auto
qed


theorem uncertainty_principle: 
  assumes "observable C" "observable D"
  shows "Δ C * Δ D ≥  norm ⟨ψ|⟦C,D⟧ *⇩v ψ⟩ / 2"
proof -
  ―‹Perform the substitution›
  let ?A = "C - ⟪C⟫"
  let ?B = "D - ⟪D⟫"

  ―‹These matrices are valid observables›
  from assms have observables_A_B: "observable ?A" "observable ?B"
    using hermitian_inner_prod_real assms Reals_cnj_iff 
    by (auto simp: hermitian_def adjoint_minus adjoint_one adjoint_scale)

  ―‹Start with commutator-ineq›
  have "(norm ⟨ψ| ⟦?A, ?B⟧ *⇩v ψ⟩)^2 ≤ 4 * Re ((⟨ψ| ?A * ?A *⇩v ψ⟩) * (⟨ψ| ?B * ?B *⇩v ψ⟩))"
    using commutator_ineq[OF observables_A_B] by auto
  ―‹Simplify the commutator›
  then have "(norm ⟨ψ| ⟦C, D⟧ *⇩v ψ⟩)^2 ≤ 4 * Re ((⟨ψ| ?A * ?A *⇩v ψ⟩) * (⟨ψ| ?B * ?B *⇩v ψ⟩))"
    using assms by simp
  ―‹Apply sqrt to both sides›
  then have "sqrt ((norm (⟨ψ| ⟦C, D⟧ *⇩v ψ⟩))^2) ≤ sqrt (4 * Re ((⟨ψ| ?A * ?A *⇩v ψ⟩) * (⟨ψ| ?B * ?B *⇩v ψ⟩)))"
    using real_sqrt_le_mono by blast
  ―‹Simplify›
  then have "norm (⟨ψ| ⟦C, D⟧ *⇩v ψ⟩) ≤ 2 * sqrt (Re ((⟨ψ| ?A * ?A *⇩v ψ⟩) * (⟨ψ| ?B * ?B *⇩v ψ⟩)))"
    by (auto cong: real_sqrt_mult)
  ―‹Because these inner products are positive and real, norm = Re›
  then have "norm (⟨ψ| ⟦C, D⟧ *⇩v ψ⟩) ≤ 2 * sqrt ( ¦Re ((⟨ψ| ?A * ?A *⇩v ψ⟩) * (⟨ψ| ?B * ?B *⇩v ψ⟩))¦)"
    by (smt (verit, ccfv_SIG) real_sqrt_le_iff)
  then have "norm (⟨ψ| ⟦C, D⟧ *⇩v ψ⟩) ≤ 2 * sqrt (norm ((⟨ψ| ?A * ?A *⇩v ψ⟩) * (⟨ψ| ?B * ?B *⇩v ψ⟩)))"
    by (auto simp: in_Reals_norm Reals_cnj_iff cnj_observables observables_A_B)
  ―‹Rewrite term to recover the standard deviation (As formulated in std-dev-alt)›
  then have "norm (⟨ψ| ⟦C, D⟧ *⇩v ψ⟩) ≤ 2 * norm (csqrt (⟨ψ| ?A * ?A *⇩v ψ⟩)) * norm (csqrt (⟨ψ| ?B * ?B *⇩v ψ⟩))"
    by (simp add: norm_mult real_sqrt_mult)
  then show "Δ C * Δ D ≥ norm ⟨ψ|⟦C, D⟧ *⇩v ψ⟩ / 2" 
    using assms by (auto cong: std_dev_alt)
qed

end

end