Boundedness of the GNS Radon-Nikodym form #
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.
The GNS reproducing identity in real-part form: ω(x* x) = ‖π(x)Ω‖².
The GNS form is bounded. For a positive functional ψ dominated by the
state ω, the off-diagonal values satisfy
‖ψ(star a * b)‖² ≤ ‖π a Ω‖² · ‖π b Ω‖².
The GNS form is bounded (norm form). ‖ψ(star a * b)‖ ≤ ‖π 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.
The cyclic map a ↦ π a Ω as a ℂ-linear map A →ₗ[ℂ] H.
Equations
- Physicslib4.GNS.cycLM π Ω = { toFun := fun (a : A) => (π a) Ω, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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' := ⋯ }
Instances For
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 π Ω))
Instances For
The reproducing identity (dense level). ⟪π a Ω, rnVec π Ω ψ b⟫ = ψ(star a * b).
The Riesz vector is bounded by the cyclic vector norm.
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' := ⋯ }
Instances For
The Radon–Nikodym operator T of a positive functional ψ dominated by ω, on the GNS space of ω.
Let (H, π, Ω) be a cyclic representation reproducing ω and let 0 ≤ ψ(a* a) ≤ ω(a* a) for all a. Then T is the bounded operator with
⟨π(a)Ω, T π(b)Ω⟩ = ψ(a* b) for all a, b ∈ A (rnOp_inner).
It commutes with every π(c) (rnOp_commute) and reproduces ψ as ψ(a) = ⟨Ω, T π(a)Ω⟩
(rnOp_reproducing), so it plays the role of a density dψ/dω inside the commutant π(A)'. This is
the step from irreducibility to purity: if π(A)' is the scalars, T = t·1 and ψ = t ω
(isPure_of_isIrreducible).
Implementation note: T π(b)Ω is the Fréchet–Riesz vector rnVec of the functional
π(a)Ω ↦ conj ψ(a* b), which is bounded by the Cauchy–Schwarz estimate gns_form_norm_le;
T extends π(b)Ω ↦ T π(b)Ω from the dense cyclic vectors (LinearMap.extendOfNorm), with
‖T π(b)Ω‖ ≤ ‖π(b)Ω‖ (rnVec_norm_le).
Blueprint: thrm:gns-radon-nikodym-operator
Equations
- Physicslib4.GNS.rnOp hcyc hrep hψpos hψdom = (Physicslib4.GNS.rnLM hcyc hrep hψpos hψdom).extendOfNorm (Physicslib4.GNS.cycLM π Ω)
Instances For
The reproducing identity for the Radon-Nikodym operator.
⟪π a Ω, T (π b Ω)⟫ = ψ(star a * b).
The Radon-Nikodym operator commutes with the representation.
The reproducing identity for the state. ψ(a) = ⟪Ω, T (π a Ω)⟫.
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 ω.
A state is pure exactly when its GNS representation is irreducible.
For any cyclic representation (H, π, Ω) reproducing ω, ω is pure if and only if every bounded
operator commuting with π(A) is a scalar. One direction uses the Radon–Nikodym operator
(rnOp): a functional dominated by ω comes from an element of π(A)'. The other decomposes an
element of π(A)' into self-adjoint parts and rescales them into functionals dominated by ω
(isIrreducible_of_isPure). Physically: a pure state, such as the vacuum of a theory with a
unique vacuum, generates an irreducible representation, a single superselection sector.
Blueprint: thrm:pure-iff-irreducible
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.
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.