Operator-algebra dynamics, crossed products, and equilibrium

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremDense 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.

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

Formalized in Tau Ceti as TauCeti.CStarAction.isKMSState_iff_of_dense.

Sources
LeanTauCeti.CStarAction.isKMSState_iff_of_dense
Uses 1 · Used by 3
Proof usesSchwarz reflection principle (real axis)
Used byConvexity of K_β · Pointwise limits of KMS states · Weak-* compactness of K_β

TheoremKMS states are invariant#

For β ≠ 0, every β-KMS state ω is invariant under the dynamics: ω (α_t(a)) = ω a. At β = 0 the KMS states are the tracial states, which need not be invariant.

TauCeti.CStarAction.IsKMSState.apply_action.{u_1} {A : Type u_1} [NonUnitalCStarAlgebra A]
  {α : TauCeti.CStarAction (Multiplicative ℝ) A} {β : ℝ} [PartialOrder A] [StarOrderedRing A]
  {ω : A →P[ℂ] ℂ} (hω : α.IsKMSState β ω) (hβ : β ≠ 0) (t : Multiplicative ℝ) (a : A) :
  ω ((α t) a) = ω a
Lean

Formalized in Tau Ceti as TauCeti.CStarAction.IsKMSState.apply_action.

Sources
LeanTauCeti.CStarAction.IsKMSState.apply_action
Uses 3
Proof usesDensity of entire analytic elements · Schwarz reflection principle (real axis) · TauCeti.CStarAction.entireAnalytic

TheoremConvexity of K_β#

Convex combinations of β-KMS states are β-KMS states.

TauCeti.CStarAction.convex_kmsStates.{u_1} {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A]
  [StarOrderedRing A] {α : TauCeti.CStarAction (Multiplicative ℝ) A} {β : ℝ} :
  Convex ℝ (α.kmsStates β)
Lean

Formalized in Tau Ceti as TauCeti.CStarAction.convex_kmsStates.

Sources
LeanTauCeti.CStarAction.convex_kmsStates
Uses 3
Proof usesDense analytic KMS criterion · Density of entire analytic elements · TauCeti.CStarAction.entireAnalytic

TheoremWeak-* compactness of K_β#

For unital B, the set of β-KMS states is weak-* compact.

TauCeti.CStarAction.isCompact_kmsStates.{u_2} {B : Type u_2} [CStarAlgebra B] [PartialOrder B]
  [StarOrderedRing B] {α : TauCeti.CStarAction (Multiplicative ℝ) B} {β : ℝ} :
  IsCompact (α.kmsStates β)
Lean

Formalized in Tau Ceti as TauCeti.CStarAction.isCompact_kmsStates.

Sources
LeanTauCeti.CStarAction.isCompact_kmsStates
Uses 3
Proof usesDense analytic KMS criterion · Density of entire analytic elements · TauCeti.CStarAction.entireAnalytic

TheoremPointwise limits of KMS states#

If β-KMS states converge pointwise to a positive functional of norm one, then the limit is a β-KMS state.

TauCeti.CStarAction.IsKMSState.of_tendsto.{u_1, u_2} {A : Type u_1} [NonUnitalCStarAlgebra A]
  [PartialOrder A] [StarOrderedRing A] {α : TauCeti.CStarAction (Multiplicative ℝ) A} {β : ℝ}
  {ω : A →P[ℂ] ℂ} {ι : Type u_2} {l : Filter ι} [l.NeBot] {ω' : ι → A →P[ℂ] ℂ}
  (hω' : ∀ᶠ (i : ι) in l, α.IsKMSState β (ω' i))
  (hlim : ∀ (a : A), Filter.Tendsto (fun i => (ω' i) a) l (nhds (ω a)))
  (hnorm : ‖ω.toContinuousLinearMap‖ = 1) : α.IsKMSState β ω
Lean

Formalized in Tau Ceti as TauCeti.CStarAction.IsKMSState.of_tendsto.

Sources
LeanTauCeti.CStarAction.IsKMSState.of_tendsto
Uses 4
Proof usesDense analytic KMS criterion · Density of entire analytic elements · Schwarz reflection principle (real axis) · TauCeti.CStarAction.entireAnalytic

TheoremTauCeti.CStarAction.CovariantRepresentation.integratedOperator_convolution#

The integrated form of a covariant pair is multiplicative for twisted convolution with respect to a left-invariant measure: (π ⋊ U) (f ⋆ g) = (π ⋊ U) f * (π ⋊ U) g.

TauCeti.CStarAction.CovariantRepresentation.integratedOperator_convolution.{u_1, u_2, u_3}
  {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G]
  [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {α : TauCeti.CStarAction G A} (P : α.CovariantRepresentation H)
  (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [IsTopologicalGroup G]
  [MeasurableMul G] [μ.IsMulLeftInvariant] (f g : CompactlySupportedContinuousMap G A) :
  (P.integratedOperator μ) (((α.convolution μ) f) g) =
    (P.integratedOperator μ) f * (P.integratedOperator μ) g
Lean

Formalized in Tau Ceti as TauCeti.CStarAction.CovariantRepresentation.integratedOperator_convolution.

Sources
LeanTauCeti.CStarAction.CovariantRepresentation.integratedOperator_convolution

TheoremTauCeti.CStarAction.CovariantRepresentation.norm_integratedOperator_le#

The integrated form is bounded by the coefficient function's L¹ norm.

TauCeti.CStarAction.CovariantRepresentation.norm_integratedOperator_le.{u_1, u_2, u_3}
  {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G]
  [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {α : TauCeti.CStarAction G A} (P : α.CovariantRepresentation H)
  (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  (f : CompactlySupportedContinuousMap G A) : ‖(P.integratedOperator μ) f‖ ≤ ∫ (g : G), ‖f g‖ ∂μ
Lean

Formalized in Tau Ceti as TauCeti.CStarAction.CovariantRepresentation.norm_integratedOperator_le.

Sources
LeanTauCeti.CStarAction.CovariantRepresentation.norm_integratedOperator_le

StructureTauCeti.CStarAction.ConvolutionAlgebra#

The convolution ⋆-algebra of the C⋆-dynamical system (A, G, α) with respect to μ: the compactly supported continuous functions G → A, with twisted convolution as product and the twisted involution as star. Use ConvolutionAlgebra.toConv and ConvolutionAlgebra.ofConv to pass to and from C_c(G, A), whose own product and star are pointwise.

TauCeti.CStarAction.ConvolutionAlgebra.{u_1, u_2} {G : Type u_1} {A : Type u_2} [Group G]
  [TopologicalSpace G] [NonUnitalCStarAlgebra A] [MeasurableSpace G] (α : TauCeti.CStarAction G A)
  (μ : MeasureTheory.Measure G) : Type (max u_1 u_2)
Lean

Formalized in Tau Ceti as TauCeti.CStarAction.ConvolutionAlgebra.

Sources
LeanTauCeti.CStarAction.ConvolutionAlgebra

DefinitionTauCeti.CStarAction.CovariantRepresentation.regular#

The regular covariant representation on L²(G, H) induced by a representation ρ of A on H: a acts by ξ ↦ (r ↦ ρ (α_{r⁻¹}(a)) (ξ r)) and s by left translation ξ ↦ (r ↦ ξ (s⁻¹ r)).

TauCeti.CStarAction.CovariantRepresentation.regular.{u_1, u_2, u_3} {G : Type u_1} {A : Type u_2}
  {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [IsTopologicalGroup G] [MeasurableSpace G]
  [BorelSpace G] (α : TauCeti.CStarAction G A) (ρ : A →⋆ₙₐ[ℂ] H →L[ℂ] H)
  (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop]
  [MeasureTheory.IsLocallyFiniteMeasure μ] : α.CovariantRepresentation ↥(MeasureTheory.Lp H 2 μ)
Lean

Formalized in Tau Ceti as TauCeti.CStarAction.CovariantRepresentation.regular.

Sources
LeanTauCeti.CStarAction.CovariantRepresentation.regular

DefinitionTauCeti.CStarAction.entireAnalytic#

The entire analytic elements of a real action, as a nonunital star subalgebra.

TauCeti.CStarAction.entireAnalytic.{u_1} {A : Type u_1} [NonUnitalCStarAlgebra A]
  (α : TauCeti.CStarAction (Multiplicative ℝ) A) : NonUnitalStarSubalgebra ℂ A
Lean

Formalized in Tau Ceti as TauCeti.CStarAction.entireAnalytic.

Sources
LeanTauCeti.CStarAction.entireAnalytic
Used by 5
Used byConvexity of K_β · Density of entire analytic elements · KMS states are invariant · Pointwise limits of KMS states · Weak-* compactness of K_β

TheoremDensity of entire analytic elements#

The entire analytic elements of a point-norm continuous real action are dense, since every element is a limit of its Gaussian smearings.

TauCeti.CStarAction.dense_entireAnalytic.{u_1} {A : Type u_1} [NonUnitalCStarAlgebra A]
  (α : TauCeti.CStarAction (Multiplicative ℝ) A) : Dense ↑α.entireAnalytic
Lean

Formalized in Tau Ceti as TauCeti.CStarAction.dense_entireAnalytic.

Sources
LeanTauCeti.CStarAction.dense_entireAnalytic
Uses 1 · Used by 4
Statement usesTauCeti.CStarAction.entireAnalytic
Used byConvexity of K_β · KMS states are invariant · Pointwise limits of KMS states · Weak-* compactness of K_β

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.