Density Functional theory[7, 8] is a formally exact theory based on the charge density of a system. Kohn-Sham Density Functional theory 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 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 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
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.