theorem Orthogonalization.MvN.orthAtN_of_isFiniteProj {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (hS : MvNStructureTheory) (M : VonNeumannAlgebra H) {p : H →L[ℂ] H} (hp : IsFiniteProj M p) (ι : Type u_1) [Fintype ι] : OrthAtN M p ι

Theorem 1.2 at a finite projection for the functionals normal on M, any finite output set, under the interface.

theorem Orthogonalization.MvN.orthAtN_of_isSemifiniteAt {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (hS : MvNStructureTheory) (M : VonNeumannAlgebra H) {z : H →L[ℂ] H} (hz : Blocks.IsCentralProj M z) (hsf : IsSemifiniteAt M z) (ι : Type u_1) [Fintype ι] : OrthAtN M z ι

Step S: Theorem 1.2 at a semifinite central projection z, from the increasing net of finite projections converging to z (interface field H2, Takesaki V.1.37) and the semifinite reduction.

theorem Orthogonalization.MvN.orthAtN_one_of_structure {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (hS : MvNStructureTheory) (M : VonNeumannAlgebra H) (ι : Type u_1) [Fintype ι] : OrthAtN M 1 ι

Theorem 1.2 for the functionals normal on M, under the interface: the type decomposition 1 = z + (1 − z) (H1) into a semifinite and a type III summand, each handled by its case, and the gluing of Blocks/Glue.lean.

theorem Orthogonalization.povm_orthogonalization_of_structure (hS : MvNStructureTheory) {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (φ : NormalState M) {ι : Type u_1} [Fintype ι] (a : ι → H →L[ℂ] H) (ha : IsPOVM M a) (ε : ℝ) (hε : 1 - ε < (φ.toLinearMap (∑ i : ι, a i * a i)).re) : ∃ (p : ι → H →L[ℂ] H), IsPVM M p ∧ (φ.toLinearMap (∑ i : ι, star (a i - p i) * (a i - p i))).re < 9 * ε

Theorem 1.2, conditional form (thm:orthonormalization; tier T3): the statement of povm_orthogonalization for every von Neumann algebra, under the structure-theory interface MvNStructureTheory (PLAN.md §9).