import PhysicsLogic.Papers.HohenbergKohn1964

set_option autoImplicit false
noncomputable section
open PhysicsLogic.Papers.HohenbergKohn1964
universe u v w z
variable {P : Type u} {S : Type v} {D : Type w} {A : Type z}
variable (f : DensityFunctionalFramework P S D A)

example : f.toGroundStateComparison.densityOf = f.densityOf := rfl
example : f.toGroundStateComparison.particleNumber = f.particleNumber := rfl
example : f.toGroundStateComparison.groundEnergy = f.groundEnergy := rfl
example : f.toGroundStateComparison.kineticEnergy = f.kineticEnergy := rfl
example : f.toGroundStateComparison.coulombRepulsionEnergy = f.coulombRepulsionEnergy := rfl
example : f.toGroundStateComparison.potentialEnergy = f.potentialEnergy := rfl
example : f.toGroundStateComparison.potentialDifferenceIntegral = f.potentialDifferenceIntegral := rfl
example : f.toGroundStateComparison.groundStateFor = f.groundStateFor := rfl
example : f.toGroundStateComparison.nondegenerateGroundStateFor = f.nondegenerateGroundStateFor := rfl
example : f.toGroundStateComparison.potentialsDifferOnlyByConstant = f.potentialsDifferOnlyByConstant := rfl

example : (∀ potential state, f.toGroundStateComparison.StateEnergyUnder potential state = f.StateEnergyUnder potential state) ∧
    (f.toGroundStateComparison.GroundStateEnergyEquation ↔ f.GroundStateEnergyEquation) ∧
    (f.toGroundStateComparison.PotentialEnergyDifferenceEquation ↔ f.PotentialEnergyDifferenceEquation) ∧
    (f.toGroundStateComparison.StrictNondegenerateVariationalPrinciple ↔ f.StrictNondegenerateVariationalPrinciple) ∧
    (f.toGroundStateComparison.NonconstantPotentialsGiveDistinctGroundStates ↔ f.NonconstantPotentialsGiveDistinctGroundStates) ∧
    (f.toGroundStateComparison.ConstantShiftPreservesGroundStates ↔ f.ConstantShiftPreservesGroundStates) ∧
    (f.toGroundStateComparison.NondegenerateGroundStateUniqueness ↔ f.NondegenerateGroundStateUniqueness) ∧
    (∀ state number, f.toGroundStateComparison.NondegenerateGroundStateAtParticleNumber state number ↔
      f.NondegenerateGroundStateAtParticleNumber state number) :=
  f.comparison_core_preserves_exact_source_conditions