The tight binding chain

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.

Refs.

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

structure CondensedMatter.TightBindingChain : Type

The physical parameters making up the tight binding chain.

• N : ℕ

  The number of sites, or atoms, in the chain

• N_ne_zero : NeZero self.N
• a : ℝ

  The distance between the sites

• a_pos : 0 < self.a
• E0 : ℝ

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

• t : ℝ

  The hopping parameter.

@[reducible, inline]

abbrev CondensedMatter.TightBindingChain.HilbertSpace (T : TightBindingChain) : Type

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

Equations

• T.HilbertSpace = QuantumMechanics.FiniteHilbertSpace T.N

instance CondensedMatter.TightBindingChain.instNeZeroNatN (T : TightBindingChain) : NeZero T.N

noncomputable def CondensedMatter.TightBindingChain.localizedState {T : TightBindingChain} : OrthonormalBasis (Fin T.N) ℂ T.HilbertSpace

The eigenstate corresponding to the particle been located on the nth site.

Equations

• CondensedMatter.TightBindingChain.localizedState = EuclideanSpace.basisFun (Fin T.N) ℂ

def CondensedMatter.TightBindingChain.«term|_⟩» : Lean.ParserDescr

The eigenstate corresponding to the particle been located on the nth site.

Equations

• One or more equations did not get rendered due to their size.

def CondensedMatter.TightBindingChain.«term⟨_|_⟩» : Lean.ParserDescr

The inner product of two localized states.

Equations

• One or more equations did not get rendered due to their size.

theorem CondensedMatter.TightBindingChain.localizedState_orthonormal (T : TightBindingChain) : Orthonormal ℂ ⇑localizedState

The localized states are normalized.

theorem CondensedMatter.TightBindingChain.localizedState_orthonormal_eq_ite (T : TightBindingChain) (m n : Fin T.N) : inner ℂ (localizedState m) (localizedState n) = if m = n then 1 else 0

noncomputable def CondensedMatter.TightBindingChain.localizedComp {T : TightBindingChain} (m n : Fin T.N) : T.HilbertSpace →ₗ[ℂ] T.HilbertSpace

The linear map |m⟩⟨n| for ⟨n| localized states.

Equations

• One or more equations did not get rendered due to their size.

def CondensedMatter.TightBindingChain.«term|_⟩⟨_|» : Lean.ParserDescr

The linear map |m⟩⟨n| for ⟨n| localized states.

Equations

• One or more equations did not get rendered due to their size.

theorem CondensedMatter.TightBindingChain.localizedComp_apply_localizedState (T : TightBindingChain) (m n p : Fin T.N) : (localizedComp m n) (localizedState p) = if n = p then localizedState m else 0

noncomputable def CondensedMatter.TightBindingChain.hamiltonian (T : TightBindingChain) : T.HilbertSpace →ₗ[ℂ] T.HilbertSpace

The Hamiltonian of the tight binding chain with periodic boundary conditions is given by E₀ ∑ n, |n⟩⟨n| - t ∑ n, (|n⟩⟨n + 1| + |n + 1⟩⟨n|). The periodic boundary conditions is manifested by the + in n + 1 being within Fin T.N (that is modulo T.N).

Equations

• One or more equations did not get rendered due to their size.

theorem CondensedMatter.TightBindingChain.hamiltonian_hermitian (T : TightBindingChain) (ψ φ : T.HilbertSpace) : inner ℂ (T.hamiltonian ψ) φ = inner ℂ ψ (T.hamiltonian φ)

The hamiltonian of the tight binding chain is hermitian.

theorem CondensedMatter.TightBindingChain.hamiltonian_apply_localizedState (T : TightBindingChain) (n : Fin T.N) : T.hamiltonian (localizedState n) = ↑T.E0 • localizedState n - ↑T.t • (localizedState (n + 1) + localizedState (n - 1))

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

theorem CondensedMatter.TightBindingChain.energy_localizedState (T : TightBindingChain) (n : Fin T.N) (htn : 1 < T.N) : inner ℂ (localizedState n) (T.hamiltonian (localizedState n)) = ↑T.E0

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.

def CondensedMatter.TightBindingChain.BrillouinZone (T : TightBindingChain) : Set ℝ

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

Equations

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

def CondensedMatter.TightBindingChain.QuantaWaveNumber (T : TightBindingChain) : Set ℝ

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.

Equations

• T.QuantaWaveNumber = {x : ℝ | ∃ (n : Fin T.N), 2 * Real.pi / (T.a * ↑T.N) * (↑↑n - ↑(T.N / 2)) = x}

theorem CondensedMatter.TightBindingChain.quantaWaveNumber_subset_brillouinZone (T : TightBindingChain) : T.QuantaWaveNumber ⊆ T.BrillouinZone

The quantized wavenumbers form a subset of the BrillouinZone.

theorem CondensedMatter.TightBindingChain.quantaWaveNumber_exp_N (T : TightBindingChain) (n : ℕ) (k : ↑T.QuantaWaveNumber) : Complex.exp (Complex.I * ↑↑k * ↑n * ↑T.N * ↑T.a) = 1

theorem CondensedMatter.TightBindingChain.quantaWaveNumber_exp_sub_one (T : TightBindingChain) (n : Fin T.N) (k : ↑T.QuantaWaveNumber) : Complex.exp (Complex.I * ↑↑k * ↑↑(n - 1) * ↑T.a) = Complex.exp (Complex.I * ↑↑k * ↑↑n * ↑T.a) * Complex.exp (-Complex.I * ↑↑k * ↑T.a)

theorem CondensedMatter.TightBindingChain.quantaWaveNumber_exp_add_one (T : TightBindingChain) (n : Fin T.N) (k : ↑T.QuantaWaveNumber) : Complex.exp (Complex.I * ↑↑k * ↑↑(n + 1) * ↑T.a) = Complex.exp (Complex.I * ↑↑k * ↑↑n * ↑T.a) * Complex.exp (Complex.I * ↑↑k * ↑T.a)

noncomputable def CondensedMatter.TightBindingChain.energyEigenstate (T : TightBindingChain) (k : ↑T.QuantaWaveNumber) : T.HilbertSpace

The energy eigenstates of the tight binding chain They are given by ∑ n, exp (I * k * n * T.a) • |n⟩.

Equations

• T.energyEigenstate k = ∑ n : Fin T.N, Complex.exp (Complex.I * ↑↑k * ↑↑n * ↑T.a) • CondensedMatter.TightBindingChain.localizedState n

theorem CondensedMatter.TightBindingChain.energyEigenstate_orthogonal (T : TightBindingChain) : Pairwise fun (k1 k2 : ↑T.QuantaWaveNumber) => inner ℂ (T.energyEigenstate k1) (T.energyEigenstate k2) = 0

The energy eigenstates of the tight binding chain are orthogonal.

noncomputable def CondensedMatter.TightBindingChain.energyEigenvalue (T : TightBindingChain) (k : ↑T.QuantaWaveNumber) : ℝ

The energy eigenvalue of the tight binding chain for a k in QuantaWaveNumber is E0 - 2 * t * Real.cos (k * T.a).

Equations

• T.energyEigenvalue k = T.E0 - 2 * T.t * Real.cos (↑k * T.a)

theorem CondensedMatter.TightBindingChain.hamiltonian_energyEigenstate (T : TightBindingChain) (k : ↑T.QuantaWaveNumber) : T.hamiltonian (T.energyEigenstate k) = T.energyEigenvalue k • T.energyEigenstate k

The energy eigenstates satisfy the time-independent Schrodinger equation.