Finite target quantum mechanics

The phrase 'finite target' is used to describe quantum mechanical systems where the Hilbert space is finite.

structure QuantumMechanics.FiniteTarget (n : ℕ) {ℏ : ℝ} (hℏ : 0 < ℏ) : Type

A finite target quantum mechanical system with hilbert-space of dimension n and Plank constant ℏ is described by a self-adjoint n × n matrix.

• H : Matrix (Fin n) (Fin n) ℂ

  The Hamiltonian, written with respect to the standard basis on Fin n → ℂ.

• H_selfAdjoint : self.H.IsHermitian

@[reducible, inline]

abbrev QuantumMechanics.FiniteTarget.V {n : ℕ} {ℏ : ℝ} {hℏ : 0 < ℏ} : FiniteTarget n hℏ → Type

The Hilbert space associated with a finite target theory A.

Equations

• x✝.V = (Fin n → ℂ)

noncomputable def QuantumMechanics.FiniteTarget.timeEvolutionMatrix {n : ℕ} {ℏ : ℝ} {hℏ : 0 < ℏ} (A : FiniteTarget n hℏ) (t : ℝ) : Matrix (Fin n) (Fin n) ℂ

Given a finite target QM system A, the time evolution matrix for a t : ℝ, A.timeEvolutionMatrix t is defined as e ^ (- I t /ℏ * A.H).

Equations

• A.timeEvolutionMatrix t = NormedSpace.exp ℂ (-(Complex.I * ↑t / ↑ℏ) • A.H)

noncomputable def QuantumMechanics.FiniteTarget.timeEvolution {n : ℕ} {ℏ : ℝ} {hℏ : 0 < ℏ} (A : FiniteTarget n hℏ) (t : ℝ) : A.V →ₗ[ℂ] A.V

Given a finite target QM system A, timeEvolution is the linear map from A.V to A.V obtained by multiplication with timeEvolutionMatrix.

Equations

• A.timeEvolution t = (LinearMap.toMatrix (Pi.basisFun ℂ (Fin n)) (Pi.basisFun ℂ (Fin n))).symm (A.timeEvolutionMatrix t)