SpectralTemperature.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The temperature-scaled group diagonals and the interaction energy.

theorem OAI.InvariantIsing.finiteR_scale_nonneg line 16
theorem OAI.InvariantIsing.projectedResolventDerivative_scale line 25
theorem OAI.InvariantIsing.finiteInteractionEnergy_eq_groupDiagonal line 38
Source documentation
The derivative formula for energy is exactly the weighted group-diagonal formula for the spectrum at temperature t, including zero temperature.
```
theorem finiteInteractionEnergy_eq_groupDiagonal (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) {t : ℝ} (ht : 0 ≤ t) (p : OverlapPath) :
    finiteInteractionEnergy ρ eig hρ hρsum t p =
      (1 / 2 : ℝ) * ∑ a, eig a *
        spectralGroupDiagonal ρ (fun b => t * eig b) hρ hρsum p a := by
…
```
Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.finiteInteractionEnergy, OAI.InvariantIsing.spectralGroupDiagonal