1. Physlib
  2. QuantumMechanics
  3. FiniteTarget
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 Mathlib.Analysis.InnerProductSpace.Adjoint public import Mathlib.Analysis.Normed.Algebra.Exponential public import Physlib.Meta.TODO.Basic public import Physlib.QuantumMechanics.PlanckConstant

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.

@[expose] public section

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

the Hilbert space has the provided (finite) dimension.

The Hamiltonian, written now as a continuous linear map.

The Hamiltonian is self-adjoint.

structure FiniteTarget (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H] (n : ℕ) where hdim: Module.finrank ℂ H = n Ham : H →L[ℂ] H Ham_selfAdjoint: IsSelfAdjoint Ham
TODO "Define a smooth structure on `FiniteTarget`."