Documentation

TauCeti.Analysis.InnerProductSpace.ProjValMeasure.Representation.OfRepresentation

The projection-valued measure of a representation of C(K, ℂ) #

Let π : C(K, ℂ) →⋆ₐ[ℂ] (H →L[ℂ] H) be a unital star representation on a complex Hilbert space, with K compact Hausdorff. Its Borel extension T = StarAlgHom.representationBorelOperator π is a unital star algebra homomorphism on the bounded Borel symbols of K. Applied to the indicator of a Borel set B it gives an orthogonal projection P(B) = T(𝟙_B), and multiplicativity of T gives P(B ∩ C) = P(B) P(C). With the diagonal Riesz measures μ_ξ of π, for which ⟪ξ, P(B) ξ⟫ = μ_ξ(B), these projections form the projection-valued measure ProjValMeasure.ofRepresentation π.

Integration against this measure recovers the Borel extension, and in particular π itself on continuous symbols. Its diagonal measures are regular, and it is the only projection-valued measure on K with regular diagonal measures that recovers π: the diagonal measures of such a measure are regular measures with the same continuous integrals as those of π, hence equal to them by the uniqueness in the Riesz–Markov–Kakutani theorem. The measure also has the same commutant as π.

Main declarations #

References #

source
noncomputable def TauCeti.ProjValMeasure.ofRepresentation {K : Type u_1} [TopologicalSpace K] [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) :
ProjValMeasure K H

The projection-valued measure of a representation π of C(K, ℂ): the projection of a Borel set B is the Borel extension of π applied to the indicator of B, and the diagonal measures are the Riesz measures μ_ξ of π.

Instances For
    source
    @[simp]
    theorem TauCeti.ProjValMeasure.ofRepresentation_proj {K : Type u_1} [TopologicalSpace K] [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) {B : Set K} (hB : MeasurableSet B) :
    (ofRepresentation π).proj B hB = π.representationBorelOperator ((BoundedBorelFunction.indicator B hB) 1)

    The projection of a Borel set B is the Borel extension of π at the indicator of B.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.ofRepresentation_diag {K : Type u_1} [TopologicalSpace K] [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) (ξ : H) :
    (ofRepresentation π).diag ξ = π.representationDiagMeasure ξ

    The diagonal measures are the Riesz measures of π.

    source
    instance TauCeti.ProjValMeasure.regular_diag_ofRepresentation {K : Type u_1} [TopologicalSpace K] [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) (ξ : H) :
    ((ofRepresentation π).diag ξ).Regular

    The diagonal measures of the projection-valued measure of a representation are regular.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.polarizedComplexMeasure_ofRepresentation {K : Type u_1} [TopologicalSpace K] [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) (ψ ξ : H) :
    (ofRepresentation π).polarizedComplexMeasure ψ ξ = π.representationPolarizedMeasure ψ ξ

    The polarized complex measures of the projection-valued measure of π are the polarized measures μ_(ψ,ξ) of π.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.integral_ofRepresentation {K : Type u_1} [TopologicalSpace K] [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) :
    (ofRepresentation π).integral = π.representationBorelOperator

    Integration against the projection-valued measure of π is the Borel extension of π.

    source
    theorem TauCeti.ProjValMeasure.integral_ofRepresentation_ofContinuousMap {K : Type u_1} [TopologicalSpace K] [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) (f : C(K, ℂ)) :
    (ofRepresentation π).integral (BoundedBorelFunction.ofContinuousMap f) = π f

    Recovery of the representation. Integrating a continuous function against the projection-valued measure of π gives its image under π.

    source
    theorem TauCeti.ProjValMeasure.eq_ofRepresentation_iff {K : Type u_1} [TopologicalSpace K] [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) (P : ProjValMeasure K H) (hP : ∀ (ξ : H), (P.diag ξ).Regular) :
    P = ofRepresentation π ↔ ∀ (f : C(K, ℂ)), P.integral (BoundedBorelFunction.ofContinuousMap f) = π f

    Uniqueness of the projection-valued measure of a representation. A projection-valued measure on K whose diagonal measures are regular is the projection-valued measure of π iff integrating every continuous function against it gives its image under π.

    source
    theorem TauCeti.ProjValMeasure.forall_commute_proj_ofRepresentation_iff {K : Type u_1} [TopologicalSpace K] [CompactSpace K] [T2Space K] [MeasurableSpace K] [BorelSpace K] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : C(K, ℂ) →⋆ₐ[ℂ] H →L[ℂ] H) (A : H →L[ℂ] H) :
    (∀ (B : Set K) (hB : MeasurableSet B), Commute A ((ofRepresentation π).proj B hB)) ↔ ∀ (f : C(K, ℂ)), Commute A (π f)

    Commutant of the projection-valued measure of a representation. An operator commutes with every projection of the projection-valued measure of π iff it commutes with π f for every continuous f; by forall_commute_integral_iff, equivalently with every integral against it.