import PhysicsLogic.Papers.KohnSham1965

open Matrix
open scoped BigOperators
open PhysicsLogic.Papers.KohnSham1965.Countermodels.OrbitalDiagnostics

example : Wave = (Fin 2 → Complex) := rfl
example : Operator = Matrix (Fin 2) (Fin 2) Complex := rfl
example (wave : Wave) : density wave = fun site => Complex.normSq (wave site) := rfl
example (wave : Wave) : mass wave = ∑ site, density wave site := rfl
example (wave : Wave) : NormalizedAt wave ↔ mass wave = 1 := Iff.rfl
example (hamiltonian : Operator) (wave : Wave) :
    energy hamiltonian wave = (∑ site, star (wave site) * hamiltonian.mulVec wave site).re := rfl
example (hamiltonian : Operator) (wave : Wave) (value : Real) :
    EigenvectorAt hamiltonian wave value ↔
      ∀ site, hamiltonian.mulVec wave site = (value : Complex) * wave site := Iff.rfl
example (hamiltonian : Operator) (wave : Wave) :
    MinimizesAt hamiltonian wave ↔ NormalizedAt wave ∧
      ∀ candidate, NormalizedAt candidate → energy hamiltonian wave ≤ energy hamiltonian candidate := Iff.rfl
example (first second : Real) : realWave first second = ![(first : Complex), (second : Complex)] := rfl
example : siteZero = realWave 1 0 := rfl
example : siteOne = realWave 0 1 := rfl
example : equalPhase = realWave (1 / Real.sqrt 2) (1 / Real.sqrt 2) := rfl
example : exactHamiltonian = !![0, 0; 0, 1] := rfl
example (wave direction : Wave) (parameter : Real) :
    waveVariation wave direction parameter = fun site => wave site + (parameter : Complex) * direction site := rfl
example (hamiltonian : Operator) (wave : Wave) :
    rayleighEnergy hamiltonian wave = energy hamiltonian wave / mass wave := rfl
example (hamiltonian : Operator) (wave : Wave) :
    RayleighStationaryAt hamiltonian wave ↔ ∀ direction,
      HasDerivAt (fun parameter => rayleighEnergy hamiltonian (waveVariation wave direction parameter)) 0 0 := Iff.rfl
example : interaction = !![6, 1; 1, 6] := rfl
example (charge : Fin 2 → Real) : hartreePotential charge = interaction.mulVec charge := rfl
example (charge : Fin 2 → Real) : hartreeEnergy charge = (1 / 2) * ∑ site, charge site * hartreePotential charge site := rfl
example : hartreeKinetic = !![3 / 2, -(3 / 2); -(3 / 2), 3 / 2] := rfl
example (charge : Fin 2 → Real) : hartreeHamiltonian charge =
    hartreeKinetic + diagonal (fun site => (hartreePotential charge site : Complex)) := rfl
example (wave : Wave) : totalEnergy wave = energy hartreeKinetic wave + hartreeEnergy (density wave) := rfl
example : leftHeavy = realWave (3 / Real.sqrt 10) (1 / Real.sqrt 10) := rfl
example : rightHeavy = realWave (1 / Real.sqrt 10) (3 / Real.sqrt 10) := rfl
example (wave : Wave) : SelfConsistentAt wave ↔ MinimizesAt (hartreeHamiltonian (density wave)) wave := Iff.rfl
example (step : Nat) : iteration step = if step % 2 = 0 then leftHeavy else rightHeavy := rfl