Quasilocal observables

This file formalises the blueprint declaration def:quasilocal-observable and develops the elementary API of the quasilocal observables of a representation.

Main definitions

• Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable: a Prop-valued predicate (blueprint def:quasilocal-observable) saying a bounded operator on the GNS Hilbert space is the image π a of a self-adjoint element a of the quasilocal algebra under a GNS *-representation π.
• Physicslib4.AQFT.HaagKastler.quasilocalObservables: the set of those operators, shown to be exactly the self-adjoint elements in the range of π.

Note on the file name, and on Axiom 4

This file no longer defines a QuasilocalCompleteness predicate, and despite its name it does not formalise Axiom 4. The predicate that used to live here was Nonempty (QuasilocalAlgebra U i) — a mathematical existence claim about the net wearing Axiom 4's name. That claim is now a theorem, exists_quasilocalAlgebra (thrm:quasilocal-algebra-exists), proved by building the quasilocal algebra from the net alone, so a hypothesis asserting it would be vacuous and is gone.

Axiom 4 proper (def:quasilocal-completeness) is a bridge principle relating physical observables to the formalism. It is encoded in Physicslib4/AQFT/HaagKastler/ObservableBridge.lean and has no mathematical consumers, which is why nothing here depends on it.

def Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable {U : LocalNet} {i : Isotony U} (Q : QuasilocalAlgebra U i) {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (T : H →L[ℂ] H) : Prop

Quasilocal Observable (blueprint label def:quasilocal-observable).

Fix a quasilocal algebra Q for a local net U and a GNS *-representation π : Q.carrier →⋆ₐ[ℂ] (H →L[ℂ] H) of the quasilocal algebra 𝔘 = Q.carrier on a complex Hilbert space H (in practice obtained from Physicslib4.GNS.gns_construction applied to a state ω on Q.carrier). A bounded operator T : H →L[ℂ] H is a quasilocal observable if it is the image T = π a of some self-adjoint element a of the quasilocal algebra.

By IsQuasilocalObservable.isSelfAdjoint, every quasilocal observable is self-adjoint, matching the blueprint's "the image π_ω(a) of a self-adjoint member a of the quasilocal algebra 𝔘 ... is self-adjoint and thus corresponds to an observable".

Blueprint reference: def:quasilocal-observable.

Equations

• Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable Q π T = ∃ (a : Q.carrier), IsSelfAdjoint a ∧ T = π a

theorem Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable.isSelfAdjoint {U : LocalNet} {i : Isotony U} {Q : QuasilocalAlgebra U i} {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} {T : H →L[ℂ] H} (hT : IsQuasilocalObservable Q π T) : IsSelfAdjoint T

Every quasilocal observable is self-adjoint: it is the image of a self-adjoint element of the quasilocal algebra under a *-homomorphism. This is the self-adjointness clause of def:quasilocal-observable.

theorem Physicslib4.AQFT.HaagKastler.exists_isQuasilocalObservable {U : LocalNet} {i : Isotony U} (Q : QuasilocalAlgebra U i) (ω : GNS.State Q.carrier) {a : Q.carrier} (ha : IsSelfAdjoint a) : ∃ (H : Type u) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H), IsQuasilocalObservable Q π (π a) ∧ IsSelfAdjoint (π a)

For any state ω on the quasilocal algebra and any self-adjoint element a of it, the GNS construction provides a *-representation in which π a is a quasilocal observable (and is self-adjoint). This is the existence content of def:quasilocal-observable, tying together thrm:gns-construction-theorem and def:state.

theorem Physicslib4.AQFT.HaagKastler.isQuasilocalObservable_one {U : LocalNet} {i : Isotony U} {Q : QuasilocalAlgebra U i} {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} : IsQuasilocalObservable Q π 1

The identity operator on the GNS Hilbert space is a quasilocal observable: it is the image π 1 of the (self-adjoint) unit of the quasilocal algebra.

theorem Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable.add {U : LocalNet} {i : Isotony U} {Q : QuasilocalAlgebra U i} {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} {S T : H →L[ℂ] H} (hS : IsQuasilocalObservable Q π S) (hT : IsQuasilocalObservable Q π T) : IsQuasilocalObservable Q π (S + T)

Quasilocal observables are closed under addition: the sum of the images of two self-adjoint elements is the image of their (self-adjoint) sum.

theorem Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable.smul {U : LocalNet} {i : Isotony U} {Q : QuasilocalAlgebra U i} {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} {c : ℂ} {T : H →L[ℂ] H} (hT : IsQuasilocalObservable Q π T) (hc : IsSelfAdjoint c) : IsQuasilocalObservable Q π (c • T)

Quasilocal observables are closed under scaling by a self-adjoint complex scalar (equivalently, a real scalar): self-adjointness of c • a requires star c = c.

theorem Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable.smul_add_smul {U : LocalNet} {i : Isotony U} {Q : QuasilocalAlgebra U i} {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} {c d : ℂ} {S T : H →L[ℂ] H} (hc : IsSelfAdjoint c) (hd : IsSelfAdjoint d) (hS : IsQuasilocalObservable Q π S) (hT : IsQuasilocalObservable Q π T) : IsQuasilocalObservable Q π (c • S + d • T)

Real-linear combinations of quasilocal observables are quasilocal observables. The scalars are taken self-adjoint in ℂ, i.e. real, which is exactly the condition under which the combination stays self-adjoint.

theorem Physicslib4.AQFT.HaagKastler.isQuasilocalObservable_iff {U : LocalNet} {i : Isotony U} {Q : QuasilocalAlgebra U i} {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} {T : H →L[ℂ] H} : IsQuasilocalObservable Q π T ↔ IsSelfAdjoint T ∧ T ∈ Set.range ⇑π

Characterisation of quasilocal observables. An operator T on the GNS Hilbert space is a quasilocal observable precisely when it is self-adjoint and lies in the range of the representation π. The forward direction is IsQuasilocalObservable.isSelfAdjoint; the converse holds even when π is not injective, by replacing a preimage b with its self-adjoint part 2⁻¹ • (b + star b), which π still sends to T.

def Physicslib4.AQFT.HaagKastler.quasilocalObservables {U : LocalNet} {i : Isotony U} (Q : QuasilocalAlgebra U i) {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) : Set (H →L[ℂ] H)

The set of quasilocal observables on the GNS Hilbert space H for the representation π: all bounded operators of the form π a with a a self-adjoint element of the quasilocal algebra.

Equations

• Physicslib4.AQFT.HaagKastler.quasilocalObservables Q π = {T : H →L[ℂ] H | Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable Q π T}

theorem Physicslib4.AQFT.HaagKastler.quasilocalObservables_eq {U : LocalNet} {i : Isotony U} (Q : QuasilocalAlgebra U i) {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) : quasilocalObservables Q π = ↑(selfAdjoint (H →L[ℂ] H)) ∩ Set.range ⇑π

The quasilocal observables are exactly the self-adjoint elements lying in the range of the representation π.

theorem Physicslib4.AQFT.HaagKastler.one_mem_quasilocalObservables {U : LocalNet} {i : Isotony U} (Q : QuasilocalAlgebra U i) {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) : 1 ∈ quasilocalObservables Q π

The identity operator is a quasilocal observable.

theorem Physicslib4.AQFT.HaagKastler.add_mem_quasilocalObservables {U : LocalNet} {i : Isotony U} (Q : QuasilocalAlgebra U i) {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) {S T : H →L[ℂ] H} (hS : S ∈ quasilocalObservables Q π) (hT : T ∈ quasilocalObservables Q π) : S + T ∈ quasilocalObservables Q π

The quasilocal observables are closed under addition.

theorem Physicslib4.AQFT.HaagKastler.smul_mem_quasilocalObservables {U : LocalNet} {i : Isotony U} (Q : QuasilocalAlgebra U i) {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) {c : ℂ} {T : H →L[ℂ] H} (hT : T ∈ quasilocalObservables Q π) (hc : IsSelfAdjoint c) : c • T ∈ quasilocalObservables Q π

The quasilocal observables are closed under scaling by a self-adjoint (i.e. real) complex scalar.