Heisenberg_uncertainty_principle.lean

import algebra
import analysis.normed_space.inner_product
import data.complex.basic
import tactic
import data.complex.is_R_or_C
import analysis.normed_space.basic
import data.real.basic

variables (F: Type) (𝕜 : Type) [is_R_or_C 𝕜] [add_comm_group F] [vector_space 𝕜 F] [c : inner_product_space.core 𝕜 F]
include c

variables {ψ : F}

--ψ is the state of the variable, most likely a particle. In Quantum Mechanics, ψ is a wave function, and the
--operators are mostly differentials. We shall not define the operator structure, we shall just consider them
--functions with specific properties. The proof shall be taken directly from Sadri Hassani's 'Mathematical Physics'.
--We shall prove that, for any two operators A and B, |⟪ψ | [A,B] | ψ⟫| ≤ 2 * Δ_A * Δ_B. In Quantum Mechanics, the
--operators A and B are the position operator X and momentul operator P, and [X,P]=iℏI, where I is the identity operator.

noncomputable theory

local notation `⟪`x`, `y`⟫` := @inner 𝕜 F _ x y
local notation `𝓚` := @is_R_or_C.of_real 𝕜 _
local notation `norm_sqK` := @is_R_or_C.norm_sq 𝕜 _
local notation `reK` := @is_R_or_C.re 𝕜 _
local notation `ext_iff` := @is_R_or_C.ext_iff 𝕜 _
local postfix `†`:90 := @is_R_or_C.conj 𝕜 _

def to_has_inner : has_inner 𝕜 F := { inner := c.inner }
local attribute [instance] to_has_inner

def norm_sq (x : F) := reK ⟪x, x⟫

local notation `norm_sqF` := @norm_sq 𝕜 F _ _ _ _

def to_has_norm : has_norm F :=
{ norm := λ x, real.sqrt (is_R_or_C.re ⟪x, x⟫) }

local attribute [instance] to_has_norm

--First, some useful general lemmas.

lemma abs_min_add: ∀ z w : 𝕜, is_R_or_C.abs(z - w) ≤ is_R_or_C.abs z + is_R_or_C.abs w:=
begin
intros z w, have fact: z - w = z + (- w), {ring,}, rw fact, rw ← is_R_or_C.abs_neg w, exact is_R_or_C.abs_add z (-w),
end

lemma sub_sub_sub: ∀ a b c d : F, a - b - (c - d) = a - b - c + d:=
begin
intros a b c d, rw sub_sub_assoc_swap, have obs: a - b + d - c = a - b + d + (-1 : 𝕜) • c, {rw neg_one_smul 𝕜 c, ring,},
rw obs, rw add_assoc, have obs2: a - b + (d + (-1 : 𝕜) • c) = a - b + ((-1 : 𝕜) • c + d), {rw ← add_comm ((-1:𝕜) • c) d,},
rw obs2, rw ← add_assoc, rw neg_one_smul 𝕜, ring,
end

lemma sub_sub_add_add: ∀ a b c d : F, a - b - c + d + b = a - c + d:=
begin
intros a b c d,
rw sub_add_eq_add_sub, rw add_comm, rw ← add_sub_assoc, rw ← add_assoc, rw add_comm b (a-b), rw sub_add_cancel a b, rw sub_add_eq_add_sub,
end

lemma op_mul (A : F → F) (ha: ∀ x y : F, ∀ a b : 𝕜, A (a • x + b • y) = a • A x + b • A y): ∀ x : F, ∀ a : 𝕜, A (a • x) = a • A x :=
begin
intros x a, have fact: a • x = a • x + (0 : F), {ring}, have fact': (0 : 𝕜) • (0 : F) = (0 : F), {exact zero_smul 𝕜 0,}, rw ← (fact') at fact,
rw fact, rw ha x 0 a 0, rw zero_smul 𝕜 (A 0), ring,
end

lemma op_same (A : F → F) (B : F → F) (a : 𝕜) (b : 𝕜) (ha1: ∀ x y : F, ∀ a b : 𝕜, A (a • x + b • y) = a • A x + b • A y) 
(ha2: ∀ x y : F, ⟪x, A y ⟫ = ⟪A x, y⟫) (hb1: ∀ x y : F, ∀ a b : 𝕜, B (a • x + b • y) = a • B x + b • B y) 
(hb2: ∀ x y : F, ⟪x, B y⟫ = ⟪B x, y⟫) (C : F → F) (hc: ∀ x : F, C x = A x - a • x) 
(D : F → F) (hd: ∀ x : F, D x = B x - b • x) : C (D ψ) - D (C ψ) = A (B ψ) - B (A ψ) :=
begin
rw hc (D ψ), rw hd (C ψ), rw hd ψ, have fact: ∀ z w : F, z - w = z + (-w), {intros z w, ring,}, rw fact (B ψ) (b • ψ),
rw hc ψ, have obs: (-1:𝕜) • (b • ψ) = - (b • ψ), {exact neg_one_smul 𝕜 (b • ψ),}, rw ← obs, have obs': (1:𝕜) • B ψ = B ψ, {exact one_smul 𝕜 (B ψ)},
rw ← obs', rw ha1 (B ψ) (b • ψ) 1 (-1), clear obs obs', rw fact (A ψ) (a • ψ), 
have obs: (-1 : 𝕜) • (a • ψ) = - (a • ψ), {exact neg_one_smul 𝕜 (a • ψ),}, rw ← obs, have obs': (1 : 𝕜) • A ψ = A ψ, {exact one_smul 𝕜 (A ψ),},
rw ← obs', rw hb1 (A ψ) (a • ψ) 1 (-1), rw one_smul 𝕜 (A (B ψ)), rw op_mul F 𝕜 A ha1, rw op_mul F 𝕜 B hb1, 
rw one_smul 𝕜 (B ψ), rw one_smul 𝕜 (A ψ), rw neg_one_smul 𝕜 (b • A ψ), rw neg_one_smul 𝕜 (b • ψ), rw one_smul 𝕜, rw neg_one_smul 𝕜,
rw neg_one_smul 𝕜 (a • ψ), ring, rw (smul_sub a (B ψ) (b • ψ)), rw smul_sub b (A ψ) (a • ψ), rw smul_smul a b ψ, rw smul_smul b a ψ,
rw mul_comm b a, rw sub_sub_assoc_swap, rw sub_sub_sub F 𝕜 (A(B ψ)) (b • A ψ) (a • B ψ) ((a * b) • ψ), rw add_sub,
rw sub_sub_sub F 𝕜, ring, rw sub_sub_add_add F 𝕜, rw add_sub_cancel, have rk1: A(B ψ) - a • B ψ - B(A ψ) + a • B ψ = A (B ψ) - a • B ψ - B (A ψ) + 0 + a • B ψ, {ring,},
rw rk1, have rk2: A (B ψ) - B (A ψ) = A (B ψ) - B (A ψ) + 0, {ring,}, rw rk2, rw sub_sub_add_add F 𝕜,
end

lemma op_linear (A : F → F) (t : 𝕜) (ha1: ∀ x y : F, ∀ a b : 𝕜, A (a • x + b • y) = a • A x + b • A y) 
(C : F → F) (hc: ∀ x : F, C x = A x - t • x) : ∀ x y : F, ∀ a b : 𝕜, C (a • x + b • y) = a • C x + b • C y :=
begin
intros x y a b, rw hc (a • x + b • y), rw hc x, rw hc y, rw smul_add, rw ha1 x y a b, rw smul_sub, rw smul_sub, 
rw add_sub, rw ← sub_sub, rw smul_comm t a, rw smul_comm t b, rw ← sub_add_eq_add_sub,
end

lemma op_hermitian (A : F → F) (t : 𝕜) (ht: is_R_or_C.conj t = t) (ha1: ∀ x y : F, ∀ a b : 𝕜, A (a • x + b • y) = a • A x + b • A y) 
(ha2: ∀ x y : F, ⟪x, A y ⟫ = ⟪A x, y⟫) (C : F → F) (hc: ∀ x : F, C x = A x - t • x) : ∀ x y : F, ⟪x, C y⟫ = ⟪C x, y⟫:=
begin
intros x y,rw hc y, rw hc x, rw inner_product_space.of_core.inner_sub_left, rw inner_product_space.of_core.inner_smul_left,
rw inner_product_space.of_core.inner_sub_right, rw inner_product_space.of_core.inner_smul_right, rw ht, rw ha2,
end

lemma average_real (A : F → F) (ha2: ∀ x y : F, ⟪x, A y⟫ = ⟪A x, y⟫) : is_R_or_C.conj ⟪ψ, A ψ⟫ = ⟪ψ, A ψ⟫ :=
begin
rw inner_product_space.of_core.inner_conj_sym (A ψ) ψ, rw ha2,
end

--In this section, we shall prove the uncertainty principle without operators. Instead, we shall mention operator
--properties as the hypothesis.

section Heisenberg_without_operators

theorem Heisenberg_a' (A : F → F) (B : F → F) (ha1: ∀ x y : F, ∀ a b : 𝕜, A (a • x + b • y) = a • A x + b • A y) 
(ha2: ∀ x y : F, ⟪x, A y ⟫ = ⟪A x, y⟫) (hb1: ∀ x y : F, ∀ a b : 𝕜, B (a • x + b • y) = a • B x + b • B y) 
(hb2: ∀ x y : F, ⟪x, B y⟫ = ⟪B x, y⟫): 
is_R_or_C.abs(⟪ψ, A (B ψ)⟫)^2 ≤ is_R_or_C.re ⟪ψ, A(A ψ)⟫ * is_R_or_C.re ⟪ψ, B(B ψ)⟫:=
begin
rw ha2 ψ (B ψ), rw ha2 ψ (A ψ), rw hb2 ψ (B ψ), 
have fact: is_R_or_C.abs⟪A ψ, B ψ⟫^2  = is_R_or_C.abs ⟪A ψ, B ψ⟫ * is_R_or_C.abs ⟪B ψ, A ψ⟫, 
{rw inner_product_space.of_core.inner_abs_conj_sym, ring,}, rw fact,
exact inner_product_space.of_core.inner_mul_inner_self_le (A ψ) (B ψ),
end

theorem Heisenberg_b' (A : F → F) (B : F → F) (ha1: ∀ x y : F, ∀ a b : 𝕜, A (a • x + b • y) = a • A x + b • A y) 
(ha2: ∀ x y : F, ⟪x, A y ⟫ = ⟪A x, y⟫) (hb1: ∀ x y : F, ∀ a b : 𝕜, B (a • x + b • y) = a • B x + b • B y) 
(hb2: ∀ x y : F, ⟪x, B y⟫ = ⟪B x, y⟫): 
is_R_or_C.abs(⟪ψ, A (B ψ) - B (A ψ)⟫)^2 ≤ 4 * is_R_or_C.re ⟪ψ, A (A ψ)⟫ * is_R_or_C.re ⟪ψ, B (B ψ)⟫:=
begin
rw inner_product_space.of_core.inner_sub_right,  
have fact: is_R_or_C.abs(⟪A ψ, B ψ⟫ - ⟪B ψ, A ψ⟫) ≤ 2 * is_R_or_C.abs ⟪ψ, A (B ψ)⟫,
{
  calc is_R_or_C.abs(⟪A ψ, B ψ⟫ - ⟪B ψ, A ψ⟫) ≤ is_R_or_C.abs ⟪A ψ, B ψ⟫ + is_R_or_C.abs ⟪B ψ, A ψ⟫: by exact abs_min_add F 𝕜 (⟪A ψ, B ψ⟫) (⟪B ψ, A ψ⟫)
  ... = is_R_or_C.abs ⟪A ψ, B ψ⟫ + is_R_or_C.abs ⟪A ψ, B ψ⟫: congr_arg (has_add.add (is_R_or_C.abs (inner (A ψ) (B ψ)))) (eq.symm (inner_product_space.of_core.inner_abs_conj_sym))
  ... = 2 * is_R_or_C.abs ⟪A ψ, B ψ⟫: by ring
  ... = 2 * is_R_or_C.abs ⟪ψ , A (B ψ)⟫: congr_arg (has_mul.mul 2) (congr_arg is_R_or_C.abs (eq.symm (ha2 ψ (B ψ)))),
},
have fact': is_R_or_C.abs(⟪A ψ, B ψ⟫ - ⟪B ψ, A ψ⟫) ^2 ≤ (2 * is_R_or_C.abs ⟪ψ, A (B ψ)⟫)^2,
{
    have obs1: 0 ≤ is_R_or_C.abs (⟪A ψ, B ψ⟫ - ⟪B ψ, A ψ⟫), {exact is_R_or_C.abs_nonneg (inner (A ψ) (B ψ) - inner (B ψ) (A ψ)),}, 
    have obs2: 0 ≤ 2 * is_R_or_C.abs(⟪ψ , A (B ψ)⟫), {linarith [has_le.le.trans_eq (is_R_or_C.abs_nonneg (inner (A ψ) (B ψ))) (congr_arg is_R_or_C.abs (eq.symm (ha2 ψ (B ψ))))],},
    exact pow_le_pow_of_le_left obs1 fact 2,
},
ring at fact', have fact1: ⟪ψ, A (B ψ)⟫ - ⟪ψ, B (A ψ)⟫ = ⟪A ψ , B ψ⟫ - ⟪B ψ, A ψ ⟫, {rw ha2 ψ (B ψ), rw hb2 ψ (A ψ),},
rw fact1,
have fact'': is_R_or_C.abs(⟪ψ, A (B ψ)⟫)^2 ≤ is_R_or_C.re ⟪ψ, A (A ψ)⟫ * is_R_or_C.re ⟪ψ, B (B ψ)⟫, {exact Heisenberg_a' F 𝕜 A B ha1 ha2 hb1 hb2,}, 
linarith,
end

theorem Heisenberg_c' (A : F → F) (B : F → F) (ha1: ∀ x y : F, ∀ a b : 𝕜, A (a • x + b • y) = a • A x + b • A y) 
(ha2: ∀ x y : F, ⟪x, A y ⟫ = ⟪A x, y⟫) (hb1: ∀ x y : F, ∀ a b : 𝕜, B (a • x + b • y) = a • B x + b • B y) 
(hb2: ∀ x y : F, ⟪x, B y⟫ = ⟪B x, y⟫) (k l : 𝕜) (hk: k = ⟪ψ, A ψ⟫) (hl: l = ⟪ψ, B ψ⟫) (Δ_A : F → F) (Δ_B : F → F)
(ha: ∀ x : F, Δ_A x = A x - k • x) (hb: ∀ x : F, Δ_B x = B x - l • x):
is_R_or_C.abs(⟪ψ, A (B ψ) - B (A ψ)⟫) ≤2 * ∥Δ_A ψ∥ * ∥Δ_B ψ∥:=
begin
have hkr: is_R_or_C.conj ⟪ψ, A ψ⟫ = ⟪ψ, A ψ⟫, {exact average_real F 𝕜 A ha2,},
have hlr: is_R_or_C.conj ⟪ψ, B ψ⟫ = ⟪ψ, B ψ⟫, {exact average_real F 𝕜 B hb2,}, rw ← hk at hkr, rw ← hl at hlr,
have ha1': ∀ x y : F, ∀ a b : 𝕜 , Δ_A (a • x + b • y) = a • Δ_A x + b • Δ_A y, {exact op_linear F 𝕜 A k ha1 Δ_A ha,},
have ha2': ∀ x y : F, ⟪x, Δ_A y ⟫ = ⟪Δ_A x, y⟫, {exact op_hermitian F 𝕜 A k hkr ha1 ha2 Δ_A ha,},
have hb1': ∀ x y : F, ∀ a b : 𝕜, Δ_B (a • x + b • y) = a • Δ_B x + b • Δ_B y, {exact op_linear F 𝕜 B l hb1 Δ_B hb,},
have hb2': ∀ x y : F, ⟪x, Δ_B y ⟫ = ⟪Δ_B x , y⟫, {exact op_hermitian F 𝕜 B l hlr hb1 hb2 Δ_B hb,},
have fact: ⟪ψ, A (B ψ) - B (A ψ)⟫ = ⟪ψ, Δ_A (Δ_B ψ) - Δ_B (Δ_A ψ)⟫, {rw ← op_same F 𝕜 A B k l ha1 ha2 hb1 hb2 Δ_A ha Δ_B hb,},
rw fact, have inequality: is_R_or_C.abs(⟪ψ, Δ_A (Δ_B ψ ) - Δ_B (Δ_A ψ)⟫)^2 ≤ 4* is_R_or_C.re ⟪ψ, Δ_A(Δ_A ψ)⟫ * is_R_or_C.re ⟪ψ, Δ_B(Δ_B ψ)⟫,
{exact Heisenberg_b' F 𝕜 Δ_A Δ_B ha1' ha2' hb1' hb2',}, 
rw ha2' ψ (Δ_A ψ) at inequality, rw hb2' ψ (Δ_B ψ) at inequality,
have sqr_a: is_R_or_C.re ⟪Δ_A ψ, Δ_A ψ⟫ = ∥Δ_A ψ∥ * ∥Δ_A ψ∥, {exact inner_product_space.of_core.inner_self_eq_norm_square (Δ_A ψ),}, ring at sqr_a,
have sqr_b: is_R_or_C.re ⟪Δ_B ψ, Δ_B ψ⟫ = ∥Δ_B ψ∥ * ∥Δ_B ψ∥, {exact inner_product_space.of_core.inner_self_eq_norm_square (Δ_B ψ),}, ring at sqr_b,
rw [sqr_a, sqr_b] at inequality, 
have facta: 0 ≤ is_R_or_C.abs ⟪ψ, Δ_A (Δ_B ψ) - Δ_B (Δ_A ψ)⟫, {exact is_R_or_C.abs_nonneg _,},
have rk1 : ∥Δ_A ψ∥ = real.sqrt (is_R_or_C.re ⟪Δ_A ψ, Δ_A ψ⟫), {refl,}, have rk2: 0 ≤ ∥Δ_A ψ∥, {rw rk1, exact real.sqrt_nonneg _,},
have rk3 : ∥Δ_B ψ∥ = real.sqrt (is_R_or_C.re ⟪Δ_B ψ, Δ_B ψ⟫), {refl,}, have rk4: 0 ≤ ∥Δ_B ψ∥, {rw rk3, exact real.sqrt_nonneg _,},
have rk5: 0 ≤ ∥Δ_A ψ∥ * ∥Δ_B ψ∥, {exact mul_nonneg rk2 rk4,},  have rk6 : 0 ≤ (2:ℝ) * ∥Δ_A ψ∥ * ∥Δ_B ψ∥, {linarith,},
have rk7: ((2:ℝ) * ∥Δ_A ψ∥ * ∥Δ_B ψ∥)^2 = 4 * ∥Δ_A ψ∥^2 * ∥Δ_B ψ∥^2 , {ring,},
have rk9: 0 ≤ is_R_or_C.abs ⟪ψ, Δ_A (Δ_B ψ) - Δ_B (Δ_A ψ)⟫ ^2, {exact pow_nonneg facta 2,},
have rk10: 0 ≤ 4 * ∥Δ_A ψ∥^2 * ∥Δ_B ψ∥^2, {linarith,},
have factb: real.sqrt (4 * ∥Δ_A ψ∥^2 * ∥Δ_B ψ∥^2) = 2 * ∥Δ_A ψ∥ * ∥Δ_B ψ∥, {exact (real.sqrt_eq_iff_sqr_eq rk10 rk6).mpr rk7,}, rw ← factb,
have rk11: (is_R_or_C.abs ⟪ψ, Δ_A (Δ_B ψ) - Δ_B (Δ_A ψ)⟫)^2 = is_R_or_C.abs ⟪ψ, Δ_A (Δ_B ψ) - Δ_B (Δ_A ψ)⟫^2, {refl,},
have factc: real.sqrt (is_R_or_C.abs ⟪ψ, Δ_A (Δ_B ψ) - Δ_B (Δ_A ψ)⟫^2) = is_R_or_C.abs ⟪ψ, Δ_A (Δ_B ψ) - Δ_B (Δ_A ψ)⟫, {exact (real.sqrt_eq_iff_sqr_eq rk9 facta).mpr rk11,}, rw ← factc,
exact (real.sqrt_le rk9 rk10).mpr inequality,
end

end Heisenberg_without_operators

structure operator := 
{operator : F → F}
{op_lin: ∀ x y : F, ∀ a b : 𝕜, operator (a • x + b • y) = a • operator x + b • operator y}
{op_her: ∀ x y : F, ⟪x, operator y⟫ = ⟪operator x, y⟫}

instance : has_coe_to_fun (operator F 𝕜) :=
⟨_, λ A, A.operator⟩

variables {A : operator F 𝕜} {B : operator F 𝕜} 

@[simp] theorem coe_to_inner_A: ∀ x : F, A x  = A.operator x:=
begin
intro x, refl, 
end

@[simp] theorem coe_to_inner_B: ∀ x : F, B x = B.operator x :=
begin
intro x, refl,
end

lemma op_lin_A: ∀ x y : F, ∀ a b : 𝕜, A (a • x + b • y) = a • A x + b • A y:=
begin
intros x y a b, rw coe_to_inner_A _, rw coe_to_inner_A _, rw coe_to_inner_A _, exact A.op_lin x y a b,
end

lemma op_her_A: ∀ x y : F, ⟪x, A y⟫ = ⟪A x, y⟫:=
begin
intros x y, rw coe_to_inner_A _, rw coe_to_inner_A _, exact A.op_her x y,
end

lemma op_lin_B : ∀ x y : F, ∀ a b : 𝕜, B (a • x + b • y) = a • B x + b • B y :=
begin
intros x y a b, rw coe_to_inner_B _, rw coe_to_inner_B _, rw coe_to_inner_B _, exact B.op_lin x y a b,
end

lemma op_her_B: ∀ x y : F, ⟪x, B y⟫ = ⟪B x, y⟫:=
begin
intros x y, rw coe_to_inner_B _, rw coe_to_inner_B _, exact B.op_her x y,
end

structure is_operator (X : F → F) : Prop :=
(is_op_lin: ∀ x y : F, ∀ a b : 𝕜, X (a • x + b • y) = a • X (x) + b • X (y))
(is_op_her: ∀ x y : F, ⟪x, X y⟫ = ⟪X x, y⟫)