Documentation

TauCeti.Analysis.InnerProductSpace.ProjValMeasure.Integral

Integration of bounded Borel symbols against a projection-valued measure #

For a projection-valued measure P on X acting on a complex Hilbert space H, this file constructs the operator integral P.integral f = ∫ f dP of a bounded Borel symbol f : BoundedBorelFunction X as a unital star algebra homomorphism BoundedBorelFunction X →⋆ₐ[ℂ] (H →L[ℂ] H).

On a simple symbol taking the value c on the measurable fibre s ⁻¹' {c}, the integral is the finite sum ∑ c • P(s ⁻¹' {c}). Because the fibres are disjoint, the projections P(s ⁻¹' {c}) are mutually orthogonal, and the diagonal matrix element of this sum against ξ is the integral of s against the diagonal measure P.diag ξ. This gives the contraction bound ‖∫ s dP‖ ≤ ‖s‖ for the supremum norm. Simple symbols are dense among bounded Borel symbols, so the integral extends uniquely by continuity; in particular it does not depend on the choice of partition or of uniformly approximating simple symbols. The algebraic laws pass to the limit.

The vector measure B ↦ P(B) ξ need not have finite variation, so this integral is not an instance of integration against a vector measure; the construction instead uses Mathlib's extension of additive set functions to simple functions, SimpleFunc.setToSimpleFunc, and the continuous extension LinearMap.extendOfNorm.

Main declarations #

References #

Simple symbols #

The integral of a bounded Borel symbol #

source
noncomputable def TauCeti.ProjValMeasure.integral {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) :
BoundedBorelFunction X →⋆ₐ[ℂ] H →L[ℂ] H

The integral of a bounded Borel symbol against a projection-valued measure P, P.integral f = ∫ f dP, as a unital star algebra homomorphism. It is characterised by integral_ofSimpleFunc on simple symbols and its continuity (continuous_integral); see eq_integral_of_continuous.

Instances For
    source
    theorem TauCeti.ProjValMeasure.continuous_integral {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) :
    Continuous ⇑P.integral

    The integral against P is continuous for the supremum norm on symbols, so uniform limits of symbols have the limiting integral.

    source
    theorem TauCeti.ProjValMeasure.eq_integral_of_continuous {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {Φ : BoundedBorelFunction X → H →L[ℂ] H} (hΦ : Continuous Φ) (h : ∀ (s : MeasureTheory.SimpleFunc X ℂ), Φ (BoundedBorelFunction.ofSimpleFunc s) = P.integral (BoundedBorelFunction.ofSimpleFunc s)) :
    Φ = ⇑P.integral

    A continuous map on bounded Borel symbols that agrees with P.integral on simple symbols is P.integral, since simple symbols are dense.

    source
    theorem TauCeti.ProjValMeasure.integral_ofSimpleFunc {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (s : MeasureTheory.SimpleFunc X ℂ) :
    P.integral (BoundedBorelFunction.ofSimpleFunc s) = ∑ c ∈ s.range, c • P.proj (⇑s ⁻¹' {c}) ⋯

    The integral of a simple symbol s is ∑ c • P(s ⁻¹' {c}), the sum running over the values of s.

    source
    @[simp]
    theorem TauCeti.ProjValMeasure.integral_indicator {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {B : Set X} (hB : MeasurableSet B) :
    P.integral ((BoundedBorelFunction.indicator B hB) 1) = P.proj B hB

    The integral of the indicator of a measurable set B is the projection P(B).

    source
    theorem TauCeti.ProjValMeasure.forall_commute_integral_iff {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (A : H →L[ℂ] H) :
    (∀ (f : BoundedBorelFunction X), Commute A (P.integral f)) ↔ ∀ (B : Set X) (hB : MeasurableSet B), Commute A (P.proj B hB)

    An operator commutes with the integral of every bounded Borel symbol iff it commutes with the projection of every measurable set: integrals of simple symbols are linear combinations of projections, and simple symbols are dense.

    source
    theorem TauCeti.ProjValMeasure.integral_diag_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 ∂P.diag ξ = inner ℂ ξ ((P.integral f) ξ)

    Diagonal matrix elements of the integral are integrals against the diagonal measures: ∫ f d(P.diag ξ) = ⟪ξ, (∫ f dP) ξ⟫.

    source
    theorem TauCeti.ProjValMeasure.norm_integral_le {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {f : BoundedBorelFunction X} {M : ℝ} (hM : 0 ≤ M) (hf : ∀ (x : X), ‖f x‖ ≤ M) :
    ‖P.integral f‖ ≤ M

    A pointwise bound ‖f x‖ ≤ M on a symbol bounds the operator norm of its integral. This includes an empty space, where every symbol and every operator integral has norm zero.

    source
    theorem TauCeti.ProjValMeasure.norm_sq_integral_apply {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (f : BoundedBorelFunction X) (ξ : H) :
    ‖(P.integral f) ξ‖ ^ 2 = ∫ (x : X), ‖f x‖ ^ 2 ∂P.diag ξ

    Vector norm identity for the integral against a projection-valued measure: ‖(∫ f dP) ξ‖ ^ 2 = ∫ ‖f x‖ ^ 2 d(P.diag ξ)(x).

    source
    theorem TauCeti.ProjValMeasure.integral_apply_eq_zero_iff {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (f : BoundedBorelFunction X) (ξ : H) :
    (P.integral f) ξ = 0 ↔ ⇑f =ᵐ[P.diag ξ] 0

    The integral of f vanishes on ξ exactly when f vanishes almost everywhere for the diagonal measure P.diag ξ.