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)
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
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)
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-
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
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
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)
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
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 -
let ?x = "Re(⟨ψ| A * B *⇩v ψ⟩)"
let ?y = "Im(⟨ψ| A * B *⇩v ψ⟩)"
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
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)
also have "... ≤ 4 * Re (⟨A *⇩v ψ| A *⇩v ψ⟩ * ⟨B *⇩v ψ| B *⇩v ψ⟩)"
by (smt (verit) assms Cauchy_Schwarz dim mult_mat_vec_carrier)
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)
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 -
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
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
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
also have "...= A * B - ⟪A⟫ * B - A * ⟪B⟫ + ⟪A⟫ * ⟪B⟫ - B * A + A * ⟪B⟫ + ⟪A⟫ * B - ⟪A⟫ * ⟪B⟫"
using assms by auto
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
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 -
let ?A = "C - ⟪C⟫"
let ?B = "D - ⟪D⟫"
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)
have "(norm ⟨ψ| ⟦?A, ?B⟧ *⇩v ψ⟩)^2 ≤ 4 * Re ((⟨ψ| ?A * ?A *⇩v ψ⟩) * (⟨ψ| ?B * ?B *⇩v ψ⟩))"
using commutator_ineq[OF observables_A_B] by auto
then have "(norm ⟨ψ| ⟦C, D⟧ *⇩v ψ⟩)^2 ≤ 4 * Re ((⟨ψ| ?A * ?A *⇩v ψ⟩) * (⟨ψ| ?B * ?B *⇩v ψ⟩))"
using assms by simp
then have "sqrt ((norm (⟨ψ| ⟦C, D⟧ *⇩v ψ⟩))^2) ≤ sqrt (4 * Re ((⟨ψ| ?A * ?A *⇩v ψ⟩) * (⟨ψ| ?B * ?B *⇩v ψ⟩)))"
using real_sqrt_le_mono by blast
then have "norm (⟨ψ| ⟦C, D⟧ *⇩v ψ⟩) ≤ 2 * sqrt (Re ((⟨ψ| ?A * ?A *⇩v ψ⟩) * (⟨ψ| ?B * ?B *⇩v ψ⟩)))"
by (auto cong: real_sqrt_mult)
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)
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