import PhysicsLogic.Papers.HohenbergKohn1964.GroundStateQuotient

set_option autoImplicit false
noncomputable section
open PhysicsLogic.Papers.HohenbergKohn1964
open GroundStateQuotient
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) (r : Setoid S)

example : Invariant f r ↔ ∀ left right, r.r left right →
    f.densityOf left = f.densityOf right ∧ f.kineticEnergy left = f.kineticEnergy right ∧
      f.coulombRepulsionEnergy left = f.coulombRepulsionEnergy right ∧
        ∀ potential, (f.groundStateFor left potential ↔ f.groundStateFor right potential) ∧
          (f.nondegenerateGroundStateFor left potential ↔ f.nondegenerateGroundStateFor right potential) := Iff.rfl

example : StrictVariationUpTo f r ↔ ∀ correct candidate potential,
    f.groundStateFor correct potential → f.nondegenerateGroundStateFor correct potential →
      f.particleNumber (f.densityOf correct) = f.particleNumber (f.densityOf candidate) →
        ¬r.r correct candidate → f.groundEnergy potential < f.StateEnergyUnder potential candidate := Iff.rfl

example : NonconstantSeparationUpTo f r ↔ ∀ left right leftPotential rightPotential,
    f.groundStateFor left leftPotential → f.groundStateFor right rightPotential →
      ¬f.potentialsDifferOnlyByConstant leftPotential rightPotential → ¬r.r left right := Iff.rfl

example : NondegenerateUniquenessUpTo f r ↔ ∀ correct candidate potential,
    f.groundStateFor correct potential → f.nondegenerateGroundStateFor correct potential →
      f.groundStateFor candidate potential → r.r correct candidate := Iff.rfl

variable (h : Invariant f r) (state : S) (potential : P)

example : (onClasses f r h).densityOf (Quotient.mk r state) = f.densityOf state := rfl
example : (onClasses f r h).kineticEnergy (Quotient.mk r state) = f.kineticEnergy state := rfl
example : (onClasses f r h).coulombRepulsionEnergy (Quotient.mk r state) = f.coulombRepulsionEnergy state := rfl
example : (onClasses f r h).groundStateFor (Quotient.mk r state) potential ↔ f.groundStateFor state potential := Iff.rfl
example : (onClasses f r h).nondegenerateGroundStateFor (Quotient.mk r state) potential ↔ f.nondegenerateGroundStateFor state potential := Iff.rfl
example : (onClasses f r h).particleNumber = f.particleNumber := rfl
example : (onClasses f r h).groundEnergy = f.groundEnergy := rfl
example : (onClasses f r h).potentialEnergy = f.potentialEnergy := rfl
example : (onClasses f r h).potentialDifferenceIntegral = f.potentialDifferenceIntegral := rfl
example : (onClasses f r h).universalFunctional = f.universalFunctional := rfl
example : (onClasses f r h).hartreeEnergy = f.hartreeEnergy := rfl
example : (onClasses f r h).residualFunctional = f.residualFunctional := rfl
example : (onClasses f r h).nearlyUniformExpansionValue = f.nearlyUniformExpansionValue := rfl
example : (onClasses f r h).slowlyVaryingGradientExpansionValue = f.slowlyVaryingGradientExpansionValue := rfl
example : (onClasses f r h).gradientSeriesAt = f.gradientSeriesAt := rfl
example : (onClasses f r h).gradientExpansionScale = f.gradientExpansionScale := rfl
example : (onClasses f r h).gradientDensityFamily = f.gradientDensityFamily := rfl
example : (onClasses f r h).equationSixtyThree = f.equationSixtyThree := rfl
example : (onClasses f r h).partialSummationValue = f.partialSummationValue := rfl
example : (onClasses f r h).equationEightyThree = f.equationEightyThree := rfl
example : (onClasses f r h).responseAsymptotics = f.responseAsymptotics := rfl
example : (onClasses f r h).fermiMomentum = f.fermiMomentum := rfl
example : (onClasses f r h).densityGradientOverDensityWavenumber = f.densityGradientOverDensityWavenumber := rfl
example : (onClasses f r h).densityCurvatureOverGradientWavenumber = f.densityCurvatureOverGradientWavenumber := rfl
example : (onClasses f r h).parametricallySmallerThan = f.parametricallySmallerThan := rfl
example : (onClasses f r h).parametricallySmallerThanImpliesStrictOrder = f.parametricallySmallerThanImpliesStrictOrder := rfl
example : (onClasses f r h).electronicPolarizability = f.electronicPolarizability := rfl
example : (onClasses f r h).exactMomentumKernel = f.exactMomentumKernel := rfl
example : (onClasses f r h).exactPositionKernel = f.exactPositionKernel := rfl
example : (onClasses f r h).finiteGradientMomentumKernel = f.finiteGradientMomentumKernel := rfl
example : (onClasses f r h).finiteGradientPositionKernel = f.finiteGradientPositionKernel := rfl
example : (onClasses f r h).potentialsDifferOnlyByConstant = f.potentialsDifferOnlyByConstant := rfl
example : (onClasses f r h).positiveNormalizedDensity = f.positiveNormalizedDensity := rfl
example : (onClasses f r h).firstOrderPerturbationOfNormalizedUniformDensityAt = f.firstOrderPerturbationOfNormalizedUniformDensityAt := rfl
example : (onClasses f r h).externallyRealizableToFirstOrderAt = f.externallyRealizableToFirstOrderAt := rfl
example : (onClasses f r h).nonpathologicalDensity = f.nonpathologicalDensity := rfl
example : (onClasses f r h).nearlyUniformDensity = f.nearlyUniformDensity := rfl
example : (onClasses f r h).zeroMeanDensityPerturbation = f.zeroMeanDensityPerturbation := rfl
example : (onClasses f r h).exactUniformGasResponseData = f.exactUniformGasResponseData := rfl
example : (onClasses f r h).finiteGradientApproximation = f.finiteGradientApproximation := rfl
example : (onClasses f r h).slowlyVaryingDensity = f.slowlyVaryingDensity := rfl
example : (onClasses f r h).allowsSubstantialDensityVariation = f.allowsSubstantialDensityVariation := rfl
example : (onClasses f r h).gradientExpansionAssumed = f.gradientExpansionAssumed := rfl
example : (onClasses f r h).rotationallyInvariantEnergyDensity = f.rotationallyInvariantEnergyDensity := rfl
example : (onClasses f r h).divergenceEquivalentEnergyDensities = f.divergenceEquivalentEnergyDensities := rfl
example : (onClasses f r h).uniformLinearAndNonlinearResponseData = f.uniformLinearAndNonlinearResponseData := rfl
example : (onClasses f r h).gradientCoefficientsDeterminedByResponses = f.gradientCoefficientsDeterminedByResponses := rfl
example : (onClasses f r h).partialSummation = f.partialSummation := rfl
example : (onClasses f r h).testedOnActualPhysicalSystems = f.testedOnActualPhysicalSystems := rfl
example : (onClasses f r h).predictsFiniteNuclearDensity = f.predictsFiniteNuclearDensity := rfl
example : (onClasses f r h).predictsAtomicShellOscillations = f.predictsAtomicShellOscillations := rfl