The dense analytic criterion for KMS states

The analytic KMS identity can be checked on a norm-dense invariant set of entire analytic elements. In particular, a norm-dense invariant star subalgebra of entire elements suffices; no continuity of imaginary-time evolution in the ambient norm is assumed.

The extension to arbitrary elements uses uniform convergence on the closed KMS strip. Differences of KMS functions satisfy the strip norm bound, so norm approximation of the second coefficient gives uniformly Cauchy KMS functions. Their limit retains continuity, holomorphy, boundedness, and both boundary values. This argument works for either sign of the inverse temperature, including zero, and for nonunital algebras.

The criterion follows Bratteli--Robinson, Operator Algebras and Quantum Statistical Mechanics 2, second edition, Section 5.3.

theorem TauCeti.CStarAction.isClosed_setOf_exists_isKMSFunction {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (β : ℝ) (φ : A →L[ℂ] ℂ) (a : A) : IsClosed {b : A | ∃ (F : ℂ → ℂ), α.IsKMSFunction β φ a b F}

For a fixed first coefficient, the second coefficients admitting a KMS function form a norm-closed set.

theorem TauCeti.CStarAction.exists_isKMSFunction_of_dense {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {φ : A →L[ℂ] ℂ} {a : A} {s : Set A} (hs : Dense s) (h : ∀ b ∈ s, ∃ (F : ℂ → ℂ), α.IsKMSFunction β φ a b F) (b : A) : ∃ (F : ℂ → ℂ), α.IsKMSFunction β φ a b F

It suffices to construct KMS functions for second coefficients in a dense set. The first coefficient is allowed to be arbitrary.

theorem TauCeti.CStarAction.isKMSState_iff_of_dense {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} [PartialOrder A] [StarOrderedRing A] {ω : A →P[ℂ] ℂ} {s : Set A} (hs : Dense s) (hinv : IsInvariant (fun (t : Multiplicative ℝ) (a : A) => (α t) a) s) (hentire : ∀ b ∈ s, α.IsEntireAnalytic b) : α.IsKMSState β ω ↔ ‖ω.toContinuousLinearMap‖ = 1 ∧ ∀ a ∈ s, ∀ b ∈ s, ω (a * α.entireExtension b (↑β * Complex.I)) = ω (b * a)

Dense analytic KMS criterion. A state is β-KMS if and only if the analytic KMS identity holds for pairs in a norm-dense invariant set of entire analytic elements. In particular, the set can be a norm-dense invariant star subalgebra.

theorem TauCeti.CStarAction.isKMSState_iff_forall_isEntireAnalytic {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} [PartialOrder A] [StarOrderedRing A] {ω : A →P[ℂ] ℂ} : α.IsKMSState β ω ↔ ‖ω.toContinuousLinearMap‖ = 1 ∧ ∀ (a : A), α.IsEntireAnalytic a → ∀ (b : A), α.IsEntireAnalytic b → ω (a * α.entireExtension b (↑β * Complex.I)) = ω (b * a)

A state is β-KMS exactly when it satisfies the analytic KMS identity for every pair of entire analytic elements. No assumption that all elements of the algebra are entire is needed.

theorem TauCeti.CStarAction.isKMSState_trivial_iff {A : Type u_1} [NonUnitalCStarAlgebra A] {β : ℝ} [PartialOrder A] [StarOrderedRing A] {ω : A →P[ℂ] ℂ} : trivial.IsKMSState β ω ↔ ‖ω.toContinuousLinearMap‖ = 1 ∧ ∀ (a b : A), ω (a * b) = ω (b * a)

For the trivial action the β-KMS states are the tracial states, for every β.