Physlib.QuantumMechanics.Operators.OneDimension.Commutation

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QuantumMechanics.Operators.OneDimension.Position
public import Physlib.QuantumMechanics.Operators.OneDimension.Momentum

Commutation relations

The commutation relations between different operators.

@[expose] public section

Commutation relation between position and momentum operators

              

lemma positionOperatorSchwartz_commutation_momentumOperatorSchwartz
    (ψ : 𝓢(ℝ, ℂ)) : positionOperatorSchwartz (momentumOperatorSchwartz ψ)
    - momentumOperatorSchwartz (positionOperatorSchwartz ψ)
    = (Complex.I * ℏ) • ψ := byψ:𝓢(ℝ, ℂ)⊢ positionOperatorSchwartz (momentumOperatorSchwartz ψ) - momentumOperatorSchwartz (positionOperatorSchwartz ψ) =
  (Complex.I * ↑↑ℏ) • ψ
  ext xψ:𝓢(ℝ, ℂ)x:ℝ⊢ (positionOperatorSchwartz (momentumOperatorSchwartz ψ) - momentumOperatorSchwartz (positionOperatorSchwartz ψ)) x =
  ((Complex.I * ↑↑ℏ) • ψ) x
  simp [momentumOperatorSchwartz_apply, positionOperatorSchwartz_apply,
    positionOperatorSchwartz_apply_fun]ψ:𝓢(ℝ, ℂ)x:ℝ⊢ -(↑x * (Complex.I * ↑↑ℏ * deriv (⇑ψ) x)) + Complex.I * ↑↑ℏ * deriv (fun x => ↑x * ψ x) x = Complex.I * ↑↑ℏ * ψ x
  have h1 : deriv Complex.ofReal x = 1 := Complex.ofRealCLM.deriv.trans (byψ:𝓢(ℝ, ℂ)x:ℝ⊢ Complex.ofRealCLM 1 = 1ψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ -(↑x * (Complex.I * ↑↑ℏ * deriv (⇑ψ) x)) + Complex.I * ↑↑ℏ * deriv (fun x => ↑x * ψ x) x = Complex.I * ↑↑ℏ * ψ x simpAll goals completed! 🐙ψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ -(↑x * (Complex.I * ↑↑ℏ * deriv (⇑ψ) x)) + Complex.I * ↑↑ℏ * deriv (fun x => ↑x * ψ x) x = Complex.I * ↑↑ℏ * ψ x)ψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ -(↑x * (Complex.I * ↑↑ℏ * deriv (⇑ψ) x)) + Complex.I * ↑↑ℏ * deriv (fun x => ↑x * ψ x) x = Complex.I * ↑↑ℏ * ψ x
  rw [deriv_fun_mul,ψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ -(↑x * (Complex.I * ↑↑ℏ * deriv (⇑ψ) x)) + Complex.I * ↑↑ℏ * (deriv Complex.ofReal x * ψ x + ↑x * deriv (⇑ψ) x) =
  Complex.I * ↑↑ℏ * ψ xhcψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ Complex.ofReal xhdψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ (⇑ψ) xψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ -(↑x * (Complex.I * ↑↑ℏ * deriv (⇑ψ) x)) + Complex.I * ↑↑ℏ * (1 * ψ x + ↑x * deriv (⇑ψ) x) = Complex.I * ↑↑ℏ * ψ xhcψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ Complex.ofReal xhdψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ (⇑ψ) x h1ψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ -(↑x * (Complex.I * ↑↑ℏ * deriv (⇑ψ) x)) + Complex.I * ↑↑ℏ * (1 * ψ x + ↑x * deriv (⇑ψ) x) = Complex.I * ↑↑ℏ * ψ xhcψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ Complex.ofReal xhdψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ (⇑ψ) xψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ -(↑x * (Complex.I * ↑↑ℏ * deriv (⇑ψ) x)) + Complex.I * ↑↑ℏ * (1 * ψ x + ↑x * deriv (⇑ψ) x) = Complex.I * ↑↑ℏ * ψ xhcψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ Complex.ofReal xhdψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ (⇑ψ) x]ψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ -(↑x * (Complex.I * ↑↑ℏ * deriv (⇑ψ) x)) + Complex.I * ↑↑ℏ * (1 * ψ x + ↑x * deriv (⇑ψ) x) = Complex.I * ↑↑ℏ * ψ xhcψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ Complex.ofReal xhdψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ (⇑ψ) x
  ringhcψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ Complex.ofReal xhdψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ (⇑ψ) x
  ·hcψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ Complex.ofReal x exact Complex.ofRealCLM.differentiableAtAll goals completed! 🐙
  ·hdψ:𝓢(ℝ, ℂ)x:ℝh1:deriv Complex.ofReal x = 1⊢ DifferentiableAt ℝ (⇑ψ) x exact ψ.differentiableAtAll goals completed! 🐙lemma positionOperatorSchwartz_momentumOperatorSchwartz_eq (ψ : 𝓢(ℝ, ℂ)) :
    positionOperatorSchwartz (momentumOperatorSchwartz ψ)
    = momentumOperatorSchwartz (positionOperatorSchwartz ψ)
    + (Complex.I * ℏ) • ψ :=
  sub_eq_iff_eq_add'.mp (positionOperatorSchwartz_commutation_momentumOperatorSchwartz ψ)lemma momentumOperatorSchwartz_positionOperatorSchwartz_eq (ψ : 𝓢(ℝ, ℂ)) :
    momentumOperatorSchwartz (positionOperatorSchwartz ψ)
    = positionOperatorSchwartz (momentumOperatorSchwartz ψ)
    - (Complex.I * ℏ) • ψ := byψ:𝓢(ℝ, ℂ)⊢ momentumOperatorSchwartz (positionOperatorSchwartz ψ) =
  positionOperatorSchwartz (momentumOperatorSchwartz ψ) - (Complex.I * ↑↑ℏ) • ψ
  simp [← positionOperatorSchwartz_commutation_momentumOperatorSchwartz ψ]All goals completed! 🐙