theorem Orthogonalization.orthAt_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) (ι : Type u_2) [Fintype ι] : Blocks.OrthAt M 1 ι

Theorem 1.2 for every von Neumann algebra on a finite-dimensional space, for functionals positive on M and normalized (the engine of tier T1b).

theorem Orthogonalization.povm_orthogonalization_finDim_vn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) (φ : NormalState M) {ι : Type u_2} [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 (povm_orthogonalization) for every von Neumann algebra M on a finite-dimensional space H: the instance of the signed statement delivered by tier T1b.