Bounded Borel symbols acting through a continuous-function representation

Let π : C(K, ℂ) →⋆ₐ[ℂ] (H →L[ℂ] H) be a unital star representation on a complex Hilbert space, with K compact Hausdorff, and let μ_(ψ,ξ) be its polarized complex measures (StarAlgHom.representationPolarizedMeasure), with ∫ g dμ_(ψ,ξ) = ⟪ψ, π g ξ⟫ for continuous g. A bounded Borel symbol f on K defines the sesquilinear form

(ψ, ξ) ↦ ∫ f dμ_(ψ,ξ),

bounded by 2 ‖f‖ ‖ψ‖ ‖ξ‖ because the total variation of μ_(ψ,ξ) is at most 2 ‖ψ‖ ‖ξ‖. By the Riesz representation of bounded sesquilinear forms (InnerProductSpace.continuousLinearMapOfBilin) and the adjoint, it is the form of a unique bounded operator T_f with

⟪ψ, T_f ξ⟫ = ∫ f dμ_(ψ,ξ).

The assignment f ↦ T_f extends π: T_f = π f for continuous f. It is a unital star algebra homomorphism, hence contractive (NonUnitalStarAlgHom.norm_apply_le). Multiplicativity and star preservation hold for continuous symbols because π is a star homomorphism, and pass to bounded Borel symbols by approximation in L¹ of the variations of the polarized measures (TauCeti.BoundedBorelFunction.eq_of_forall_ofContinuousMap_eq): matrix elements of T_f depend Lipschitz-continuously on f for these L¹ distances. Multiplicativity is first proved when one factor is continuous, then in general. So a representation of C(K, ℂ) extends to a representation of the bounded Borel symbols; its values on indicators of Borel sets are the projections of the representation's projection-valued measure.

Main declarations

• StarAlgHom.representationBorelOperator π: the star algebra homomorphism f ↦ T_f.
• StarAlgHom.inner_representationBorelOperator: the matrix elements of T_f.
• StarAlgHom.representationBorelOperator_ofContinuousMap: T_f = π f for continuous f.
• StarAlgHom.integral_representationPolarizedMeasure_representationBorelOperator: the weighted matrix-element identity ∫ f dμ_(ψ, T_g ξ) = ∫ f g dμ_(ψ,ξ).
• StarAlgHom.commute_representationBorelOperator: an operator commuting with π commutes with every T_g.
• StarAlgHom.norm_integral_representationPolarizedMeasure_le: the bound on the sesquilinear form.

References

• J. B. Conway, A Course in Functional Analysis, 2nd ed., Springer (1990), §IX.1.

theorem StarAlgHom.norm_integral_representationPolarizedMeasure_le {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 : TauCeti.BoundedBorelFunction K) (ψ ξ : H) : ‖∫ᵛ (x : K), f x ∂[ContinuousLinearMap.mul ℝ ℂ; π.representationPolarizedMeasure ψ ξ]‖ ≤ 2 * ‖f‖ * ‖ψ‖ * ‖ξ‖

The integral of a bounded Borel symbol f against the polarized measure μ_(ψ,ξ) is at most 2 ‖f‖ ‖ψ‖ ‖ξ‖ in norm.

noncomputable def StarAlgHom.representationBorelOperator {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) : TauCeti.BoundedBorelFunction K →⋆ₐ[ℂ] H →L[ℂ] H

The Borel extension of a representation π of C(K, ℂ): the bounded operator T_f assigned to a bounded Borel symbol f, determined by its matrix elements ⟪ψ, T_f ξ⟫ = ∫ f dμ_(ψ,ξ) against the polarized measures (inner_representationBorelOperator). It is a unital star algebra homomorphism that agrees with π on continuous symbols (representationBorelOperator_ofContinuousMap).

theorem StarAlgHom.inner_representationBorelOperator {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 : TauCeti.BoundedBorelFunction K) (ψ ξ : H) : inner ℂ ψ ((π.representationBorelOperator f) ξ) = ∫ᵛ (x : K), f x ∂[ContinuousLinearMap.mul ℝ ℂ; π.representationPolarizedMeasure ψ ξ]

Matrix elements of the Borel extension. ⟪ψ, T_f ξ⟫ = ∫ f dμ_(ψ,ξ).

@[simp]

theorem StarAlgHom.representationBorelOperator_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) (g : C(K, ℂ)) : π.representationBorelOperator (TauCeti.BoundedBorelFunction.ofContinuousMap g) = π g

The Borel extension of π agrees with π on continuous symbols.

theorem StarAlgHom.integral_representationPolarizedMeasure_representationBorelOperator {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 g : TauCeti.BoundedBorelFunction K) (ψ ξ : H) : ∫ᵛ (x : K), f x ∂[ContinuousLinearMap.mul ℝ ℂ; π.representationPolarizedMeasure ψ ((π.representationBorelOperator g) ξ)] = ∫ᵛ (x : K), f x * g x ∂[ContinuousLinearMap.mul ℝ ℂ; π.representationPolarizedMeasure ψ ξ]

Weighted matrix elements. Integrating f against the polarized measure μ_(ψ, T_g ξ) is integrating f g against μ_(ψ,ξ), since both are ⟪ψ, T_f T_g ξ⟫. This is the integrated form of the identity μ_(ψ, T_g ξ) = g · μ_(ψ,ξ).

theorem StarAlgHom.commute_representationBorelOperator {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} (hA : ∀ (f : C(K, ℂ)), Commute A (π f)) (g : TauCeti.BoundedBorelFunction K) : Commute A (π.representationBorelOperator g)

Commutant of the Borel extension. An operator commuting with π f for every continuous f commutes with T_g for every bounded Borel symbol g: the matrix elements ⟪A† ψ, T_g ξ⟫ and ⟪ψ, T_g (A ξ)⟫ are Lipschitz in g for L¹ distances and agree on continuous symbols.