OAI/Probability/InvariantIsing/Spectral/SpectralEnergyPrimitive.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The temperature primitive of the finite-spectrum interaction energy.

  1. theorem OAI.InvariantIsing.integral_finiteSpectralSlope_temperature line 16
  2. theorem OAI.InvariantIsing.integral_finiteInteractionEnergy line 38

    Source documentation

    Equation up:primitive, for the actual finite atomic spectral transform.

    theorem integral_finiteInteractionEnergy (ρ eig : ι → ℝ) (hρ : ∀ a, 0 < ρ a)
    (hρsum : ∑ a, ρ a = 1) {t : ℝ} (ht : 0 ≤ t) (p : OverlapPath) :
    (∫ u in 0..t, finiteInteractionEnergy ρ eig hρ hρsum u p) =
      spectralFunctional (fun x => t * finiteR ρ eig hρ hρsum (t * x)) p := by
…

    Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.finiteInteractionEnergy, OAI.InvariantIsing.spectralFunctional, OAI.InvariantIsing.finiteR