structure Orthogonalization.IsometryData {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (a q w : ι → H →L[ℂ] H) : Prop

The block-wise partial isometry of Lemma 3.2 / the proof of Theorem 1.2 in the finite case: (W1) ∑ wᵢ* wᵢ = 1, (W2) wᵢ wⱼ* = δᵢⱼ qᵢ, (W3) wᵢ √(∑ qⱼ aⱼ) = qᵢ √aᵢ.

• sum_star_mul : ∑ i : ι, star (w i) * w i = 1
• mul_star (i j : ι) : w i * star (w j) = if i = j then q i else 0
• mul_sqrt (i : ι) : w i * CFC.sqrt (∑ j : ι, q j * a j) = q i * CFC.sqrt (a i)