Towards the GNS Radon-Nikodym correspondence

For a state ω with cyclic GNS representation (H, π, Ω) and a positive linear functional ψ dominated by ω (0 ≤ ψ(a* a) ≤ ω(a* a)), the classical Radon-Nikodym theorem produces a unique operator 0 ≤ T ≤ 1 in the commutant of π(A) with ψ(a) = ⟪Ω, T π(a) Ω⟫. The operator is the bounded sesquilinear form (π(a)Ω, π(b)Ω) ↦ ψ(a* b) represented via Riesz.

This file establishes the analytic crux on which that construction rests: the form is well-defined and bounded, namely

‖ψ(a* b)‖ ≤ ‖π(a)Ω‖ · ‖π(b)Ω‖,

obtained from the Cauchy-Schwarz inequality for ψ together with domination (ψ ≤ ω) and the GNS reproducing identity ω(x* x) = ‖π(x)Ω‖². As an immediate consequence the form depends only on the vectors π(a)Ω, π(b)Ω, not on the representatives a, b.

theorem Physicslib4.GNS.reproducing_norm_sq {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) (x : A) : (ω (star x * x)).re = ‖(π x) Ω‖ ^ 2

The GNS reproducing identity in real-part form: ω(x* x) = ‖π(x)Ω‖².

theorem Physicslib4.GNS.gns_form_normSq_le {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) (a b : A) : Complex.normSq (ψ (star a * b)) ≤ ‖(π a) Ω‖ ^ 2 * ‖(π b) Ω‖ ^ 2

The GNS form is bounded. For a positive functional ψ dominated by the state ω, the off-diagonal values satisfy ‖ψ(star a * b)‖² ≤ ‖π a Ω‖² · ‖π b Ω‖².

theorem Physicslib4.GNS.gns_form_norm_le {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) (a b : A) : ‖ψ (star a * b)‖ ≤ ‖(π a) Ω‖ * ‖(π b) Ω‖

The GNS form is bounded (norm form). ‖ψ(star a * b)‖ ≤ ‖π a Ω‖ · ‖π b Ω‖.

theorem Physicslib4.GNS.gns_form_well_defined {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) {a a' : A} (haa : (π a) Ω = (π a') Ω) (b : A) : ψ (star a * b) = ψ (star a' * b)

The GNS form is well-defined on vectors. If π a Ω = π a' Ω, then ψ(star a * b) = ψ(star a' * b) for every b: the form ψ(star · * ·) depends only on the GNS vectors, not on their algebra representatives.

noncomputable def Physicslib4.GNS.cycLM {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) : A →ₗ[ℂ] H

The cyclic map a ↦ π a Ω as a ℂ-linear map A →ₗ[ℂ] H.

Equations

• Physicslib4.GNS.cycLM π Ω = { toFun := fun (a : A) => (π a) Ω, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Physicslib4.GNS.cycLM_apply {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) (a : A) : (cycLM π Ω) a = (π a) Ω

theorem Physicslib4.GNS.cycLM_denseRange {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) : DenseRange ⇑(cycLM π Ω)

noncomputable def Physicslib4.GNS.rnFun {A : Type u_1} [CStarAlgebra A] (ψ : A →L[ℂ] ℂ) (b : A) : A →ₗ[ℂ] ℂ

The linear functional a ↦ conj (ψ (star a * b)) on A, linear in a.

Equations

• Physicslib4.GNS.rnFun ψ b = { toFun := fun (a : A) => (starRingEnd ℂ) (ψ (star a * b)), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Physicslib4.GNS.rnFun_apply {A : Type u_1} [CStarAlgebra A] (ψ : A →L[ℂ] ℂ) (b a : A) : (rnFun ψ b) a = (starRingEnd ℂ) (ψ (star a * b))

theorem Physicslib4.GNS.rnFun_bound {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) (b : A) : ∃ (C : ℝ), ∀ (a : A), ‖(rnFun ψ b) a‖ ≤ C * ‖(cycLM π Ω) a‖

noncomputable def Physicslib4.GNS.rnVec {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) (ψ : A →L[ℂ] ℂ) (b : A) : H

The Riesz vector representing a ↦ ψ(star a * b) on the GNS space.

Equations

• Physicslib4.GNS.rnVec π Ω ψ b = (InnerProductSpace.toDual ℂ H).symm ((Physicslib4.GNS.rnFun ψ b).extendOfNorm (Physicslib4.GNS.cycLM π Ω))

theorem Physicslib4.GNS.rnVec_inner {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) (a b : A) : inner ℂ ((π a) Ω) (rnVec π Ω ψ b) = ψ (star a * b)

The reproducing identity (dense level). ⟪π a Ω, rnVec π Ω ψ b⟫ = ψ(star a * b).

theorem Physicslib4.GNS.rnVec_norm_le {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) (b : A) : ‖rnVec π Ω ψ b‖ ≤ ‖(π b) Ω‖

The Riesz vector is bounded by the cyclic vector norm.

noncomputable def Physicslib4.GNS.rnLM {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) : A →ₗ[ℂ] H

The assignment b ↦ rnVec π Ω ψ b, bundled as a ℂ-linear map (linearity is forced by the reproducing identity and density of the cyclic vectors).

Equations

• Physicslib4.GNS.rnLM hcyc hrep hψpos hψdom = { toFun := fun (b : A) => Physicslib4.GNS.rnVec π Ω ψ b, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def Physicslib4.GNS.rnOp {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) : H →L[ℂ] H

The Radon-Nikodym operator T of a dominated functional ψ.

Equations

• Physicslib4.GNS.rnOp hcyc hrep hψpos hψdom = (Physicslib4.GNS.rnLM hcyc hrep hψpos hψdom).extendOfNorm (Physicslib4.GNS.cycLM π Ω)

theorem Physicslib4.GNS.rnOp_inner {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) (a b : A) : inner ℂ ((π a) Ω) ((rnOp hcyc hrep hψpos hψdom) ((π b) Ω)) = ψ (star a * b)

The reproducing identity for the Radon-Nikodym operator. ⟪π a Ω, T (π b Ω)⟫ = ψ(star a * b).

theorem Physicslib4.GNS.rnOp_commute {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) (c : A) : π c * rnOp hcyc hrep hψpos hψdom = rnOp hcyc hrep hψpos hψdom * π c

The Radon-Nikodym operator commutes with the representation.

theorem Physicslib4.GNS.rnOp_reproducing {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {ψ : A →L[ℂ] ℂ} (hψpos : ∀ (a : A), 0 ≤ ψ (star a * a)) (hψdom : ∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) (a : A) : ψ a = inner ℂ Ω ((rnOp hcyc hrep hψpos hψdom) ((π a) Ω))

The reproducing identity for the state. ψ(a) = ⟪Ω, T (π a Ω)⟫.

theorem Physicslib4.GNS.isPure_of_isIrreducible {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) (hirr : IsIrreducible π) : IsPure ω

Irreducible ⟹ pure. If the GNS representation of ω is irreducible, then ω is pure: every dominated positive functional is a scalar multiple of ω. The Radon-Nikodym operator of a dominated ψ commutes with π, hence is a scalar by irreducibility, and the reproducing identity makes ψ proportional to ω.

theorem Physicslib4.GNS.isPure_iff_isIrreducible {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) : IsPure ω ↔ IsIrreducible π

The full GNS purity ⟺ irreducibility equivalence. A state ω is pure if and only if its cyclic GNS representation is irreducible.

theorem Physicslib4.GNS.exists_gns_factor_of_isPure {A : Type u} [CStarAlgebra A] {ω : State A} (hpure : IsPure ω) : ∃ (H : Type u) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H), IsCyclicVector π Ω ∧ (∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) ∧ gnsVonNeumann π ∩ (gnsVonNeumann π).centralizer = {T : H →L[ℂ] H | ∃ (c : ℂ), T = c • 1}

The GNS representation of a pure state is a factor. For a pure state ω there is a cyclic GNS triple (H, π, Ω) reproducing ω whose generated von Neumann algebra π(A)'' has trivial center: the center π(A)'' ∩ (π(A)'')' equals the scalar operators. This combines the GNS construction, purity ⟹ irreducibility (isPure_iff_isIrreducible), and center_gnsVonNeumann_eq_of_isIrreducible.

theorem Physicslib4.GNS.exists_gns_generates_all_of_isPure {A : Type u} [CStarAlgebra A] {ω : State A} (hpure : IsPure ω) : ∃ (H : Type u) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H), IsCyclicVector π Ω ∧ (∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) ∧ gnsVonNeumann π = Set.univ

The GNS representation of a pure state generates all of B(H). For a pure state ω there is a cyclic GNS triple (H, π, Ω) reproducing ω whose generated von Neumann algebra is the whole of B(H): π(A)'' = B(H). This is the density (bicommutant-theorem) sharpening of exists_gns_factor_of_isPure, combining the GNS construction, purity ⟹ irreducibility (isPure_iff_isIrreducible), and the density form gnsVonNeumann_eq_univ_of_isIrreducible.