Finite target quantum mechanics

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

Physical examples of such systems include:

• Spin systems.
• Tight binding chains.

structure QuantumMechanics.FiniteTarget (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H] (n : ℕ) : Type u_1

A FiniteTarget structure that is basis independent, i.e. use a linear map for the hamiltonian instead of a matrix."

• hdim : Module.finrank ℂ H = n

  the Hilbert space has the provided (finite) dimension.

• Ham : H →L[ℂ] H

  The Hamiltonian, written now as a continuous linear map.

• Ham_selfAdjoint : IsSelfAdjoint self.Ham

  The Hamiltonian is self-adjoint.

noncomputable def QuantumMechanics.FiniteTarget.timeEvolution {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H] {n : ℕ} (A : FiniteTarget H n) (t : ℝ) : H →L[ℂ] H

Given a finite target QM system A, the time evolution operator for a t : ℝ, A.timeEvolution t is defined as exp(- I t /ℏ * A.Ham). Still a map.

Equations

• A.timeEvolution t = NormedSpace.exp ℂ (-(Complex.I * ↑t / ↑↑Constants.ℏ) • A.Ham)

noncomputable def QuantumMechanics.FiniteTarget.timeEvolutionMatrix {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H] {n : ℕ} (A : FiniteTarget H n) (t : ℝ) (b : Module.Basis (Fin n) ℂ H) : Matrix (Fin n) (Fin n) ℂ

The matrix representation of the time evolution operator in a given basis. Given a Planck constant ℏ, the matrix is a self-adjoint n × n matrix describing the timeEvolution.

Equations

• A.timeEvolutionMatrix t b = (LinearMap.toMatrix b b) ↑(A.timeEvolution t)

noncomputable def QuantumMechanics.FiniteTarget.timeEvolutionMatrixStandard {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H] {n : ℕ} (A : FiniteTarget H n) (t : ℝ) : Matrix (Fin n) (Fin n) ℂ

An instance of timeEvolutionmatrix over the standard basis.

Equations

• A.timeEvolutionMatrixStandard t = A.timeEvolutionMatrix t (Module.finBasisOfFinrankEq ℂ H ⋯)