Density Functional theory[7, 8] is a formally exact theory based on the charge density of a system. Kohn-Sham Density Functional theory[9] is a formally exact one-electron theory. Working within the Born-Oppenheimer approximation, the many-body Schrödinger equation,

where is the many-body wavefunction, is replaced by a
set of *N* one-electron equations of the form

where is a single-electron wavefunction. These one-electron equations contain a potential produced by all the ions and the electrons. Density Functional theory properly includes all parts of the electron-electron interaction, i.e. the Hartree potential

where is the charge density of all the electrons, a potential due to exchange and correlation effects, , and the external potential due to the ions, ,

Hohenberg and Kohn[10] originally developed Density Functional theory for application to the ground state of a system of spinless fermions. In such a system the particle density is given by

with being the many-body ground state wavefunction of the system. It can be shown that the total ground state energy of the system is a functional of the density, , and that if the energy due to the electron-ion interactions is excluded the remainder of the energy is a universal functional of the density, (i.e. does not depend on the potential from the ions). The most elegant proof of Density Functional theory is due to Levy[11] and is as follows:

For a particular *N*-representable density
(i.e. any density given by an antisymmetric *N*-electron
wavefunction), a functional of the density corresponding to any
operator can be defined via

The right hand side is evaluated by searching over wavefunctions, , which give rise to the density and looking for the one which makes the expectation value of the operator a minimum.

We can define in the same way, where

and

Now let be the ground state of an *N*-electron system and
a state which yields a density and minimises
.
Then, from the definition of ,

Now is the electronic Hamiltonian, from Eq.(), and so must obey the variational principle (see section ),

Also, from the definition of , in Eq.(), we have

since is just one of the trial wavefunctions that yield . Adding to the above equation gives

which in combination with Eq.() yields the desired result

hence completing the proof.

Tue Nov 19 17:11:34 GMT 1996