Matrix elements of the integral against a projection-valued measure

Let P be a projection-valued measure on X acting on a complex Hilbert space H. For vectors ψ ξ : H, the polarized complex measure μ_(ψ,ξ) = P.polarizedComplexMeasure ψ ξ takes the value ⟪ψ, P(B) ξ⟫ on a measurable set B, and has finite variation. This file identifies the matrix elements of the operator integral P.integral f = ∫ f dP of a bounded Borel symbol f with Mathlib's integral against this complex measure, through the multiplication pairing ℂ × ℂ → ℂ:

⟪ψ, (∫ f dP) ξ⟫ = ∫ᵛ x, f x ∂[mul ℝ ℂ; μ_(ψ,ξ)].

So the operator integral is determined by scalar integration against the polarized measures, and the scalar integration theory of complex measures applies to its matrix elements.

On the diagonal, the variation of the polarized measure μ_(ξ,ξ) is the finite positive measure P.diag ξ (variation_polarizedComplexMeasure_self), and integrating any complex function against μ_(ξ,ξ) gives the Bochner integral against P.diag ξ.

Main declarations

• ProjValMeasure.integral_polarizedComplexMeasure_eq_inner_integral: the matrix element ⟪ψ, (∫ f dP) ξ⟫ is the integral of f against μ_(ψ,ξ).
• ProjValMeasure.integral_polarizedComplexMeasure_self: integration of any f : X → ℂ against μ_(ξ,ξ) is the Bochner integral against P.diag ξ.

References

• W. Rudin, Functional Analysis, 2nd ed., McGraw–Hill, 1991, Theorem 12.21.
• K. Schmüdgen, Unbounded Self-adjoint Operators on Hilbert Space, Springer GTM 265, 2012, Section 4.2.

theorem TauCeti.ProjValMeasure.integral_polarizedComplexMeasure_eq_inner_integral {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (f : BoundedBorelFunction X) (ψ ξ : H) : ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ ℂ; P.polarizedComplexMeasure ψ ξ] = inner ℂ ψ ((P.integral f) ξ)

Matrix elements of the integral against a projection-valued measure. For a bounded Borel symbol f, ⟪ψ, (∫ f dP) ξ⟫ is the integral of f against the polarized complex measure μ_(ψ,ξ), whose value on a measurable set B is ⟪ψ, P(B) ξ⟫, through the multiplication pairing.

@[simp]

theorem TauCeti.ProjValMeasure.integral_polarizedComplexMeasure_self {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (f : X → ℂ) (ξ : H) : ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ ℂ; P.polarizedComplexMeasure ξ ξ] = ∫ (x : X), f x ∂P.diag ξ

Integration of a complex function against the diagonal polarized measure through the multiplication pairing is the Bochner integral against the diagonal measure. Both sides vanish when f is not integrable, since the variation of the polarized measure is the diagonal measure.