Almost-everywhere invariance and dominated convergence for projection-valued integrals

Let P be a projection-valued measure on X acting on a complex Hilbert space H, with diagonal measures P.diag ξ. The operator integral P.integral f = ∫ f dP of a bounded Borel symbol f satisfies the vector norm identity ProjValMeasure.norm_sq_integral_apply, ‖(∫ f dP) ξ‖ ^ 2 = ∫ ‖f x‖ ^ 2 d(P.diag ξ)(x). It identifies the map f ↦ (∫ f dP) ξ as an isometry from the symbols, with the L² norm of P.diag ξ, into H, and transfers scalar integration theory to the operator integral:

• the integral only sees the symbol P-almost everywhere, and in fact two symbols have the same integral exactly when they agree P-almost everywhere;
• uniformly bounded symbols converging P-almost everywhere have integrals converging strongly, that is on every vector, by Lebesgue's dominated convergence theorem.

Strong convergence is the right conclusion here: the indicators of (0, 1 / (n + 1)) converge pointwise to 0 on ℝ, but the norm of their integral is 1 against any projection-valued measure that charges every such interval.

Main declarations

• ProjValMeasure.integral_eq_integral_iff: ∫ f dP = ∫ g dP iff f = g P-almost everywhere.
• ProjValMeasure.integral_congr_ae: symbols equal P-almost everywhere have equal integrals.
• ProjValMeasure.tendsto_integral_apply_filter_of_dominated_convergence: bounded P-almost everywhere convergence of symbols gives strong convergence of their integrals.

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_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) : P.integral f = 0 ↔ ⇑f =ᶠ[P.ae] 0

The integral of f against P vanishes exactly when f vanishes P-almost everywhere.

theorem TauCeti.ProjValMeasure.integral_eq_integral_iff {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (f g : BoundedBorelFunction X) : P.integral f = P.integral g ↔ ⇑f =ᶠ[P.ae] ⇑g

Two bounded Borel symbols have the same integral against P exactly when they agree P-almost everywhere.

theorem TauCeti.ProjValMeasure.integral_congr_ae {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {f g : BoundedBorelFunction X} (h : ⇑f =ᶠ[P.ae] ⇑g) : P.integral f = P.integral g

Bounded Borel symbols that agree P-almost everywhere have the same integral against P.

theorem TauCeti.ProjValMeasure.tendsto_integral_apply_filter_of_dominated_convergence {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {ι : Type u_3} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → BoundedBorelFunction X} {f : BoundedBorelFunction X} {M : ℝ} (h_bound : ∀ᶠ (n : ι) in l, ∀ᶠ (x : X) in P.ae, ‖(F n) x‖ ≤ M) (h_lim : ∀ᶠ (x : X) in P.ae, Filter.Tendsto (fun (n : ι) => (F n) x) l (nhds (f x))) (ξ : H) : Filter.Tendsto (fun (n : ι) => (P.integral (F n)) ξ) l (nhds ((P.integral f) ξ))

Dominated convergence for the integral against a projection-valued measure: if bounded Borel symbols F n are eventually bounded by a common constant P-almost everywhere and converge to f P-almost everywhere, then their integrals converge to the integral of f strongly, that is on every vector.