theorem Orthogonalization.FinDim.blockProj_isStarProjection {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (q : ι → H →L[ℂ] H) (hq : ∀ (i : ι), IsStarProjection (q i)) : IsStarProjection (blockProj q)

theorem Orthogonalization.FinDim.trace_blockProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (q : ι → H →L[ℂ] H) : (LinearMap.trace ℂ (BlockSpace H ι)) ↑(blockProj q) = ∑ i : ι, (LinearMap.trace ℂ H) ↑(q i)

The trace of the block projection is the sum of the traces of the blocks.

theorem Orthogonalization.FinDim.exists_isometryData {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (a q : ι → H →L[ℂ] H) (ha0 : ∀ (i : ι), 0 ≤ a i) (hq : ∀ (i : ι), IsStarProjection (q i)) (hqa : ∀ (i : ι), Commute (q i) (a i)) (htr : ∑ i : ι, (LinearMap.trace ℂ H) ↑(q i) = ↑(Module.finrank ℂ H)) : ∃ (w : ι → H →L[ℂ] H), IsometryData a q w

Step F2: the isometry data exist in finite dimension.