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.HilbertSpaces.FiniteTarget.Basic

The tight binding chain

i. Overview

The tight binding chain corresponds to an electron in motion in a 1d solid with the assumption the electron can sit only on the atoms of the solid.

The solid is assumed to consist of N sites with a separation of a between them

Mathematically, the tight binding chain corresponds to a QM problem located on a lattice with only self and nearest neighbour interactions, with periodic boundary conditions.

ii. Key results

    TightBindingChain : The physical parameters making up the tight binding chain.

    localizedState : The orthonormal basis of localized states.

    hamiltonian : The Hamiltonian of the tight binding chain.

    BrillouinZone : The Brillouin zone of the tight binding chain.

    QuantaWaveNumber : The quantized wavenumbers of the energy eigenstates.

    energyEigenstate : The energy eigenstates of the tight binding chain.

    energyEigenvalue : The energy eigenvalues of the tight binding chain.

    hamiltonian_energyEigenstate : The Hamiltonian acting on an energy eigenstate gives the corresponding energy eigenvalue times the energy eigenstate.

iii. Table of contents

    A. The setup

      A.1. The input data for the tight binding chain

      A.2. The Hilbert space

    B. The localized states

      B.1. The orthonormal basis of localized states

      B.2. Notation for localized states

      B.3. Orthonormality of the localized states

    C. The operator |m⟩⟨n|

      C.1. Definition of the operator |m⟩⟨n|

      C.2. Notation for the operator |m⟩⟨n|

      C.3. The operator |m⟩⟨n| applied to a localized state

    D. The Hamiltonian of the tight binding chain

      D.1. Hermiticity of the Hamiltonian

      D.2. Hamiltonian applied to a localized state

      D.3. Mean energy of a localized state

    E. The Brillouin zone and quantized wavenumbers

      E.1. The Brillouin zone

      E.2. The quantized wavenumbers of the energy eigenstates

      E.3. Wavenumbers lie in the Brillouin zone

      E.4. Expotentials related to the quantized wavenumbers

    F. The energy eigenstates and eigenvalues

      F.1. The energy eigenstates

      F.2. Orthonormality of the energy eigenstates

      F.3. The energy eigenvalues

      F.4. The time-independent Schrodinger equation

iv. References

    https://www.damtp.cam.ac.uk/user/tong/aqm/aqmtwo.pdf

@[expose] public section

A. The setup

A.1. The input data for the tight binding chain

The physical parameters making up the tight binding chain.

The number of sites, or atoms, in the chain

The distance between the sites

The energy associate with a particle sitting at a fixed site.

The hopping parameter.

structure TightBindingChain where N : Nat [N_ne_zero : NeZero N] a : a_pos : 0 < a E0 : t :
instance : NeZero T.N := T.N_ne_zero

A.2. The Hilbert space

The Hilbert space of a TightBindingchain is the N-dimensional finite dimensional Hilbert space.

abbrev HilbertSpace := QuantumMechanics.FiniteHilbertSpace (Fin T.N)

B. The localized states

Localized states correspond to the electron being located on a specific site in the chain.

B.1. The orthonormal basis of localized states

B.2. Notation for localized states

@[inherit_doc localizedState] scoped notation "|" n "⟩" => localizedState n

The inner product of two localized states.

scoped notation "⟨" m "|" n "⟩" => localizedState m, localizedState n⟫_

B.3. Orthonormality of the localized states

The localized states are normalized.

lemma localizedState_orthonormal : Orthonormal (localizedState (T := T)) := (localizedState (T := T)).orthonormal
lemma localizedState_orthonormal_eq_ite (m n : Fin T.N) : m|n = if m = n then 1 else 0 := orthonormal_iff_ite.mp T.localizedState_orthonormal _ _

C. The operator |m⟩⟨n|

C.1. Definition of the operator |m⟩⟨n|

C.2. Notation for the operator |m⟩⟨n|

@[inherit_doc localizedComp] scoped notation "|" n "⟩⟨" m "|" => localizedComp n m

C.3. The operator |m⟩⟨n| applied to a localized state

All goals completed! 🐙

The adjoint of localizedComp |m⟩⟨n| is |n⟩⟨m|.

lemma localizedComp_adjoint (m n : Fin T.N) (ψ φ : T.HilbertSpace) : |m⟩⟨n| ψ, φ⟫_ = ψ, |n⟩⟨m| φ⟫_ := T:TightBindingChainm:Fin T.Nn:Fin T.Nψ:T.HilbertSpaceφ:T.HilbertSpace|m⟩⟨n| ψ, φ⟫_ = ψ, |n⟩⟨m| φ⟫_ T:TightBindingChainm:Fin T.Nn:Fin T.Nψ:T.HilbertSpaceφ:T.HilbertSpaceψ, localizedState n⟫_ * localizedState m, φ⟫_ = localizedState m, φ⟫_ * ψ, localizedState n⟫_ All goals completed! 🐙

D. The Hamiltonian of the tight binding chain

D.1. Hermiticity of the Hamiltonian

The hamiltonian of the tight binding chain is hermitian.

lemma hamiltonian_hermitian (ψ φ : T.HilbertSpace) : T.hamiltonian ψ, φ⟫_ = ψ, T.hamiltonian φ⟫_ := T:TightBindingChainψ:T.HilbertSpaceφ:T.HilbertSpaceT.hamiltonian ψ, φ⟫_ = ψ, T.hamiltonian φ⟫_ T:TightBindingChainψ:T.HilbertSpaceφ:T.HilbertSpaceT.E0 c, |c⟩⟨c| ψ, φ⟫_ - T.t x, (|x⟩⟨x + 1| ψ + |x + 1⟩⟨x| ψ), φ⟫_ = ψ, T.E0 c, |c⟩⟨c| φ⟫_ - ψ, T.t x, (|x⟩⟨x + 1| φ + |x + 1⟩⟨x| φ)⟫_ T:TightBindingChainψ:T.HilbertSpaceφ:T.HilbertSpaceT.E0 c, |c⟩⟨c| ψ, φ⟫_ = ψ, T.E0 c, |c⟩⟨c| φ⟫_T:TightBindingChainψ:T.HilbertSpaceφ:T.HilbertSpaceT.t x, (|x⟩⟨x + 1| ψ + |x + 1⟩⟨x| ψ), φ⟫_ = ψ, T.t x, (|x⟩⟨x + 1| φ + |x + 1⟩⟨x| φ)⟫_ T:TightBindingChainψ:T.HilbertSpaceφ:T.HilbertSpaceT.E0 c, |c⟩⟨c| ψ, φ⟫_ = ψ, T.E0 c, |c⟩⟨c| φ⟫_ -- E0 term All goals completed! 🐙 T:TightBindingChainψ:T.HilbertSpaceφ:T.HilbertSpaceT.t x, (|x⟩⟨x + 1| ψ + |x + 1⟩⟨x| ψ), φ⟫_ = ψ, T.t x, (|x⟩⟨x + 1| φ + |x + 1⟩⟨x| φ)⟫_ -- t term T:TightBindingChainψ:T.HilbertSpaceφ:T.HilbertSpace x, (T.t ψ, |x + 1⟩⟨x| φ⟫_ + T.t ψ, |x⟩⟨x + 1| φ⟫_) = x, (T.t ψ, |x⟩⟨x + 1| φ⟫_ + T.t ψ, |x + 1⟩⟨x| φ⟫_) exact Finset.sum_congr rfl fun n _ => T:TightBindingChainψ:T.HilbertSpaceφ:T.HilbertSpacen:Fin T.Nx✝:n Finset.univT.t ψ, |n + 1⟩⟨n| φ⟫_ + T.t ψ, |n⟩⟨n + 1| φ⟫_ = T.t ψ, |n⟩⟨n + 1| φ⟫_ + T.t ψ, |n + 1⟩⟨n| φ⟫_ All goals completed! 🐙

D.2. Hamiltonian applied to a localized state

The Hamiltonian applied to the localized state |n⟩ gives T.E0 • |n⟩ - T.t • (|n + 1⟩ + |n - 1⟩).

lemma hamiltonian_apply_localizedState (n : Fin T.N) : T.hamiltonian |n = (T.E0 : ) |n - (T.t : ) (|n + 1 + |n - 1) := T:TightBindingChainn:Fin T.NT.hamiltonian (localizedState n) = T.E0 localizedState n - T.t (localizedState (n + 1) + localizedState (n - 1)) T:TightBindingChainn:Fin T.NT.E0 localizedState n - (T.t localizedState (n - 1) + T.t localizedState (n + 1)) = T.E0 localizedState n - (T.t localizedState (n + 1) + T.t localizedState (n - 1)) All goals completed! 🐙

D.3. Mean energy of a localized state

The energy of a localized state in the tight binding chain is E0. This lemma assumes that there is more then one site in the chain otherwise the result is not true.

T:TightBindingChainn:Fin T.Nhtn:1 < T.NlocalizedState n, T.E0 localizedState n - T.t (localizedState (n + 1) + localizedState (n - 1))⟫_ = T.E0 T:TightBindingChainn:Fin T.Nhtn:1 < T.N((if T.N = 1 then T.t else 0) + if T.N = 1 then T.t else 0) = 0 All goals completed! 🐙

E. The Brillouin zone and quantized wavenumbers

E.1. The Brillouin zone

The Brillouin zone of the tight binding model is [-π/a, π/a). This is the set in which wave functions are uniquely defined.

def BrillouinZone : Set := Set.Ico (- Real.pi / T.a) (Real.pi / T.a)

E.2. The quantized wavenumbers of the energy eigenstates

The wavenumbers associated with the energy eigenstates. This corresponds to the set 2 π / (a N) * (n - ⌊N/2⌋) for n : Fin T.N. It is defined as such so it sits in the Brillouin zone.

def QuantaWaveNumber : Set := {x | ( n : Fin T.N, 2 * Real.pi / (T.a * T.N) * ((n : ) - (T.N / 2 : )) = x)}

E.3. Wavenumbers lie in the Brillouin zone

The quantized wavenumbers form a subset of the BrillouinZone.

T:TightBindingChainx:n:Fin xhNpos:0 < xa:hT:0 < ahx:0 < xhn:n + 1 xhn0:0 nhx2:2 * (x / 2) xhx2':x 2 * (x / 2) + 12 * Real.pi * (n - (x / 2)) * a < Real.pi * (a * x) All goals completed! 🐙
T:TightBindingChainn:m:Fin T.Nhpp:T.N 0Complex.I * 2 * Real.pi / (T.a * T.N) * (m - (T.N / 2)), * n * T.N * T.a = ((m - (T.N / 2)) * n) * (2 * Real.pi * Complex.I) T:TightBindingChainn:m:Fin T.Nhpp:T.N 0hT':T.a 0Complex.I * 2 * Real.pi / (T.a * T.N) * (m - (T.N / 2)), * n * T.N * T.a = ((m - (T.N / 2)) * n) * (2 * Real.pi * Complex.I) T:TightBindingChainn:m:Fin T.Nhpp:T.N 0hT':T.a 0Complex.I * (2 * Real.pi / (T.a * T.N) * (m - (T.N / 2))) * n * T.N * T.a = (m - (T.N / 2)) * n * (2 * Real.pi * Complex.I) All goals completed! 🐙All goals completed! 🐙lemma quantaWaveNumber_exp_add_one (n : Fin T.N) (k : T.QuantaWaveNumber) : Complex.exp (Complex.I * k * (n + 1).val * T.a) = Complex.exp (Complex.I * k * n * T.a) * Complex.exp (Complex.I * k * T.a) := T:TightBindingChainn:Fin T.Nk:T.QuantaWaveNumberComplex.exp (Complex.I * k * (n + 1) * T.a) = Complex.exp (Complex.I * k * n * T.a) * Complex.exp (Complex.I * k * T.a) conv_rhs => T:TightBindingChainn:Fin T.Nk:T.QuantaWaveNumber| Complex.exp (Complex.I * k * (n + 1) * T.a) * Complex.exp (-Complex.I * k * T.a + Complex.I * k * T.a) T:TightBindingChainn:Fin T.Nk:T.QuantaWaveNumber| Complex.exp (Complex.I * k * (n + 1) * T.a)

F. The energy eigenstates and eigenvalues

F.1. The energy eigenstates

F.2. Orthonormality of the energy eigenstates

The energy eigenstates of the tight binding chain are orthogonal.

This is a fundamental quantum mechanical result: eigenstates of a Hermitian operator (the Hamiltonian) with distinct eigenvalues are orthogonal. Here we prove it directly using the periodic boundary conditions which quantize the wavenumbers.

The key physical insight is that different wavenumbers k₁ ≠ k₂ give rise to different N-th roots of unity exp(i(k₂-k₁)a), and the sum of all N-th roots of unity equals zero.

T:TightBindingChaink1:T.QuantaWaveNumberk2:T.QuantaWaveNumberhne:k1 k2ω: := Complex.exp (Complex.I * (k2 - k1) * T.a)hω_def:ω = Complex.exp (Complex.I * (k2 - k1) * T.a)hsum_eq: n, (starRingEnd ) (Complex.exp (Complex.I * k1 * n * T.a)) * Complex.exp (Complex.I * k2 * n * T.a) = i Finset.range T.N, ω ^ ihω_pow:ω ^ T.N = 1hω_ne_one:ω 1hgeom:(ω - 1) * i Finset.range T.N, ω ^ i = 0 i Finset.range T.N, ω ^ i = 0 All goals completed! 🐙

F.3. The energy eigenvalues

F.4. The time-independent Schrodinger equation

The energy eigenstates satisfy the time-independent Schrodinger equation.

T:TightBindingChaink:T.QuantaWaveNumberhp1: n, Complex.exp (Complex.I * k * n * T.a) localizedState (n + 1) = n, Complex.exp (Complex.I * k * (n - 1) * T.a) localizedState nhm1: n, Complex.exp (Complex.I * k * n * T.a) localizedState (n - 1) = n, Complex.exp (Complex.I * k * (n + 1) * T.a) localizedState nn:Fin T.Nx✝:n Finset.univ(T.E0 * Complex.exp (Complex.I * k * n * T.a) - T.t * (Complex.exp (Complex.I * k * (n - 1) * T.a) + Complex.exp (Complex.I * k * (n + 1) * T.a))) localizedState n = ((T.energyEigenvalue k) * Complex.exp (Complex.I * k * n * T.a)) localizedState n T:TightBindingChaink:T.QuantaWaveNumberhp1: n, Complex.exp (Complex.I * k * n * T.a) localizedState (n + 1) = n, Complex.exp (Complex.I * k * (n - 1) * T.a) localizedState nhm1: n, Complex.exp (Complex.I * k * n * T.a) localizedState (n - 1) = n, Complex.exp (Complex.I * k * (n + 1) * T.a) localizedState nn:Fin T.Nx✝:n Finset.univ(T.E0 * Complex.exp (Complex.I * k * n * T.a) - T.t * (Complex.exp (Complex.I * k * n * T.a) * Complex.exp (-Complex.I * k * T.a) + Complex.exp (Complex.I * k * n * T.a) * Complex.exp (Complex.I * k * T.a))) localizedState n = ((T.E0 - 2 * T.t * ((Complex.exp (k * T.a * Complex.I) + Complex.exp (-(k * T.a) * Complex.I)) / 2)) * Complex.exp (Complex.I * k * n * T.a)) localizedState n All goals completed! 🐙