Polarized complex measures of a continuous-function representation

Let π : C(K, ℂ) →⋆ₐ[ℂ] (H →L[ℂ] H) be a unital star representation on a complex Hilbert space, with K compact Hausdorff. Each vector ξ has a finite regular diagonal measure μ_ξ, with ∫ f dμ_ξ = ⟪ξ, π f ξ⟫ for continuous f (StarAlgHom.representationDiagMeasure). Complex polarization of these diagonal measures gives, for every pair of vectors, a complex measure

μ_(ψ,ξ) = ¼ (μ_(ξ+ψ) + i μ_(ξ+iψ) - μ_(ξ-ψ) - i μ_(ξ-iψ))

with ∫ f dμ_(ψ,ξ) = ⟪ψ, π f ξ⟫ for every continuous f, the integral being taken through the multiplication pairing ℂ × ℂ → ℂ. Its variation is dominated by the average of the four diagonal measures, so it is finite and regular. By the uniqueness theorem for scalar measures of regular variation on a compact Hausdorff space (MeasureTheory.VectorMeasure.ext_of_integral_eq_on_continuousMap), μ_(ψ,ξ) is the only such measure. Uniqueness gives its algebraic laws: it is conjugate-linear in ψ, linear in ξ, conjugate-symmetric, and on the diagonal it is μ_ξ regarded as a complex measure.

Integrating a bounded Borel symbol f against these measures defines the matrix elements ⟪ψ, T_f ξ⟫ = ∫ f dμ_(ψ,ξ) of an operator T_f that extends π from continuous to bounded Borel symbols (StarAlgHom.representationBorelOperator). The total variation bound |μ_(ψ,ξ)|(K) ≤ 2 ‖ψ‖ ‖ξ‖ makes this sesquilinear form bounded.

Main declarations

• StarAlgHom.representationPolarizedMeasure π ψ ξ: the polarized complex measure μ_(ψ,ξ).
• StarAlgHom.integral_representationPolarizedMeasure: ∫ f dμ_(ψ,ξ) = ⟪ψ, π f ξ⟫ for continuous f.
• StarAlgHom.eq_representationPolarizedMeasure_iff: characterization among complex measures of regular variation.
• StarAlgHom.variation_representationPolarizedMeasure_le: domination of the variation by the diagonal measures, with the instance of regular variation.
• StarAlgHom.variation_representationPolarizedMeasure_univ_le: the total variation is at most 2 ‖ψ‖ ‖ξ‖.
• StarAlgHom.representationPolarizedMeasure_self: the diagonal case.
• StarAlgHom.representationPolarizedMeasure_add_left and its companions: sesquilinearity.
• StarAlgHom.representationPolarizedMeasure_swap_apply: conjugate symmetry.

References

• W. Rudin, Real and Complex Analysis, 3rd ed., McGraw-Hill (1987), Theorem 6.19.
• J. B. Conway, A Course in Functional Analysis, 2nd ed., Springer (1990), §IX.1.

noncomputable def StarAlgHom.representationPolarizedMeasure {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) : MeasureTheory.ComplexMeasure K

The polarized complex measure μ_(ψ,ξ) of a representation of C(K, ℂ), the complex polarization ¼ (μ_(ξ+ψ) + i μ_(ξ+iψ) - μ_(ξ-ψ) - i μ_(ξ-iψ)) of the diagonal measures. It is the unique complex measure of regular variation with ∫ f dμ_(ψ,ξ) = ⟪ψ, π f ξ⟫ for every continuous f (eq_representationPolarizedMeasure_iff). It is conjugate-linear in ψ and linear in ξ.

theorem StarAlgHom.representationPolarizedMeasure_apply {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) {B : Set K} (hB : MeasurableSet B) : (π.representationPolarizedMeasure ψ ξ) B = 1 / 4 * (↑((π.representationDiagMeasure (ξ + ψ)).real B) + Complex.I * ↑((π.representationDiagMeasure (ξ + Complex.I • ψ)).real B) - ↑((π.representationDiagMeasure (ξ - ψ)).real B) - Complex.I * ↑((π.representationDiagMeasure (ξ - Complex.I • ψ)).real B))

The value of the polarized measure on a measurable set, by the polarization formula.

theorem StarAlgHom.variation_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) (ψ ξ : H) : MeasureTheory.VectorMeasure.variation (π.representationPolarizedMeasure ψ ξ) ≤ 4⁻¹ • (π.representationDiagMeasure (ξ + ψ) + π.representationDiagMeasure (ξ + Complex.I • ψ) + π.representationDiagMeasure (ξ - ψ) + π.representationDiagMeasure (ξ - Complex.I • ψ))

The variation of the polarized measure is dominated by the average of the four diagonal measures in the polarization formula.

instance StarAlgHom.regular_variation_representationPolarizedMeasure {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) : (MeasureTheory.VectorMeasure.variation (π.representationPolarizedMeasure ψ ξ)).Regular

The polarized measure has regular variation.

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

Integrating a continuous function against the polarized measure gives the matrix coefficient ⟪ψ, π f ξ⟫.

theorem StarAlgHom.eq_representationPolarizedMeasure_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) (ψ ξ : H) (μ : MeasureTheory.ComplexMeasure K) [(MeasureTheory.VectorMeasure.variation μ).Regular] : μ = π.representationPolarizedMeasure ψ ξ ↔ ∀ (f : C(K, ℂ)), ∫ᵛ (x : K), f x ∂[ContinuousLinearMap.mul ℝ ℂ; μ] = inner ℂ ψ ((π f) ξ)

A complex measure of regular variation equals the polarized measure μ_(ψ,ξ) iff its integral of every continuous f is ⟪ψ, π f ξ⟫.

theorem StarAlgHom.representationPolarizedMeasure_self {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) : π.representationPolarizedMeasure ξ ξ = (π.representationDiagMeasure ξ).withDensityᵥ fun (x : K) => 1

On the diagonal, the polarized measure is the diagonal measure μ_ξ regarded as a complex measure, that is, with constant complex density 1.

theorem StarAlgHom.representationPolarizedMeasure_self_apply {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) {B : Set K} (hB : MeasurableSet B) : (π.representationPolarizedMeasure ξ ξ) B = ↑((π.representationDiagMeasure ξ).real B)

On the diagonal, the polarized measure takes the real values of the diagonal measure.

@[simp]

theorem StarAlgHom.variation_representationPolarizedMeasure_self {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) : MeasureTheory.VectorMeasure.variation (π.representationPolarizedMeasure ξ ξ) = π.representationDiagMeasure ξ

On the diagonal, the variation of the polarized measure is the diagonal measure.

theorem StarAlgHom.representationPolarizedMeasure_add_left {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) : π.representationPolarizedMeasure (ψ + ψ') ξ = π.representationPolarizedMeasure ψ ξ + π.representationPolarizedMeasure ψ' ξ

The polarized measure is additive in its first argument.

theorem StarAlgHom.representationPolarizedMeasure_add_right {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) : π.representationPolarizedMeasure ψ (ξ + ξ') = π.representationPolarizedMeasure ψ ξ + π.representationPolarizedMeasure ψ ξ'

The polarized measure is additive in its second argument.

theorem StarAlgHom.representationPolarizedMeasure_smul_left {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) (c : ℂ) (ψ ξ : H) : π.representationPolarizedMeasure (c • ψ) ξ = star c • π.representationPolarizedMeasure ψ ξ

The polarized measure is conjugate-homogeneous in its first argument.

theorem StarAlgHom.representationPolarizedMeasure_smul_right {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) (c : ℂ) (ψ ξ : H) : π.representationPolarizedMeasure ψ (c • ξ) = c • π.representationPolarizedMeasure ψ ξ

The polarized measure is homogeneous in its second argument.

@[simp]

theorem StarAlgHom.representationPolarizedMeasure_zero_left {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) : π.representationPolarizedMeasure 0 ξ = 0

The polarized measure vanishes when its first argument is zero.

@[simp]

theorem StarAlgHom.representationPolarizedMeasure_zero_right {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) : π.representationPolarizedMeasure ψ 0 = 0

The polarized measure vanishes when its second argument is zero.

theorem StarAlgHom.variation_representationPolarizedMeasure_univ_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) (ψ ξ : H) : (MeasureTheory.VectorMeasure.variation (π.representationPolarizedMeasure ψ ξ)) Set.univ ≤ ENNReal.ofReal (2 * ‖ψ‖ * ‖ξ‖)

The total variation of the polarized measure μ_(ψ,ξ) is at most 2 ‖ψ‖ ‖ξ‖. This follows from the domination by the diagonal measures, after rescaling ψ and ξ by reciprocal positive factors, which does not change μ_(ψ,ξ).

theorem StarAlgHom.representationPolarizedMeasure_swap_apply {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) (B : Set K) : (π.representationPolarizedMeasure ξ ψ) B = (starRingEnd ℂ) ((π.representationPolarizedMeasure ψ ξ) B)

Conjugate symmetry. Exchanging the two vectors conjugates the polarized measure.