Orthogonal countable splitting for projection-valued measures

The diagonal scalar measure records the squared norm of the projection of a Hilbert-space vector onto a measurable spectral region. For a countable measurable partition, these squared norms sum to the squared norm of the original vector. The identity applies to projection-valued measures on arbitrary measurable spaces.

Adapted from Kitware's DKPS formalization in ForTauCeti/Analysis/InnerProductSpace/ProjValMeasure/Additivity.lean.

@[simp]

theorem TauCeti.ProjValMeasure.enorm_sq_proj_apply {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (B : Set X) (hB : MeasurableSet B) (ξ : H) : ‖(P.proj B hB) ξ‖ₑ ^ 2 = (P.diag ξ) B

Squared extended norm of a spectral projection equals the diagonal mass of the corresponding measurable set.

theorem TauCeti.ProjValMeasure.tsum_enorm_sq_proj {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {ι : Type u_3} [Countable ι] (B : ι → Set X) (hB : ∀ (k : ι), MeasurableSet (B k)) (hdisj : Pairwise (Function.onFun Disjoint B)) (hcov : ⋃ (k : ι), B k = Set.univ) (ξ : H) : ∑' (k : ι), ‖(P.proj (B k) ⋯) ξ‖ₑ ^ 2 = ‖ξ‖ₑ ^ 2

For a countable measurable partition, the squared extended norms of the projected components sum to the squared extended norm of the original vector.