import PhysicsLogic.Papers.WittenIndex1982

open PhysicsLogic.Papers.WittenIndex1982
open PhysicsLogic.Framework.SupersymmetricOperator
open scoped BigOperators

variable {L H : Type} [NormedAddCommGroup H] [InnerProductSpace Complex H]
variable (d : PairedSpectralData L) (beta : Real)

example : d.Label = ((Fin d.bosonicZeros ⊕ Fin d.fermionicZeros) ⊕ (L ⊕ L)) := by rfl
example : d.energy = (fun label => match label with
    | .inl _ => 0 | .inr (.inl level) => d.pairEnergy level
    | .inr (.inr level) => d.pairEnergy level) := by rfl
example : d.parity = (fun label => match label with
    | .inl (.inl _) => 1 | .inl (.inr _) => -1
    | .inr (.inl _) => 1 | .inr (.inr _) => -1) := by rfl
example : d.pairWeight beta = fun level => Real.exp (-beta * d.pairEnergy level) := by rfl
example : d.heatWeight beta = fun label => Real.exp (-beta * d.energy label) := by rfl
example : d.gradedWeight beta = fun label => d.parity label * d.heatWeight beta label := by rfl
example : d.heatTrace beta = ∑' label, d.heatWeight beta label := by rfl
example : d.supertrace beta = ∑' label, d.gradedWeight beta label := by rfl
example : d.index = Int.ofNat d.bosonicZeros - Int.ofNat d.fermionicZeros := by rfl
example : d.PositivePairsAt ↔ ∀ level, 0 < d.pairEnergy level := by rfl
example : d.FiniteEnergySublevelsAt ↔ ∀ cutoff : Real,
    Set.Finite {level | d.pairEnergy level ≤ cutoff} := by rfl
example : d.HeatTraceDefinedAt beta ↔ 0 < beta ∧ Summable (d.heatWeight beta) := by rfl
example : d.AllPositiveBetaTracesDefinedAt ↔
    ∀ b : Real, 0 < b → d.HeatTraceDefinedAt b := by rfl
example : d.BetaIndependentRegularizationAt ↔ d.AllPositiveBetaTracesDefinedAt ∧
    ∀ b c : Real, 0 < b → 0 < c → d.supertrace b = d.supertrace c := by rfl
example : d.normalizedThermalParity beta = d.supertrace beta / d.heatTrace beta := by rfl

variable (r : SpectralOperatorData d H)
example : r.RepresentsSpectrumAt ↔ d.PositivePairsAt ∧ r.operators.AlgebraAt ∧
    (∀ label, (r.state label : H) = r.basis label) ∧
    (∀ label, r.operators.HasEnergyAt (d.energy label) (r.state label)) ∧
    (∀ label, r.operators.grading (r.state label) =
      (d.parity label : Complex) • r.state label) := by rfl