Physicslib4.AQFT.HaagKastler.QuasilocalObservable

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 #

Supporting lemmas #

Note on the file name, and on Axiom 4 #

Despite its name, this file does not formalise Axiom 4. The existence of a quasilocal algebra is a theorem, exists_quasilocalAlgebra (thrm:quasilocal-algebra-exists), proved by building the algebra from the net alone, so no hypothesis asserting it is needed.

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.

source
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

An operator T is a quasilocal observable in a representation π if T = π(a) with a self-adjoint.

Here π is a *-representation of the quasilocal algebra 𝔘 on a Hilbert space H, in practice the GNS representation of a state (Physicslib4.GNS.gns_construction), and a is a self-adjoint element of 𝔘. Such an operator is self-adjoint (IsQuasilocalObservable.isSelfAdjoint); conversely the quasilocal observables are exactly the self-adjoint operators in the range of π (isQuasilocalObservable_iff).

Blueprint: def:quasilocal-observable

Equations
Instances For
    source
    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.

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

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

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

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

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

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

    source
    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
    Instances For
      source
      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 π.

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

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

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