Section 2, p. 4 — the orthogonal projection onto the span of independent columns is $P=A(A^*A)^{-1}A^*$

Let $n$ be a finite index set and let $a_1,\dots,a_m\in\mathbb{C}^n$ be linearly independent. Let $A$ be the $n\times m$ matrix whose $x$-th column is $a_x$, i.e. $A_{ix}=\langle e_i,a_x\rangle$, and let $A^*$ be its conjugate transpose. If $P$ is an $n\times n$ complex matrix which is selfadjoint ($P^*=P$), idempotent ($P^2=P$), and whose image is $\operatorname{span}\{a_1,\dots,a_m\}$, then

This is the matrix-analysis formula for the orthogonal projection onto the column space of $A$, the multidimensional version of the formula $vv^*/(v^*v)$ for the projection onto a line. Applied to the Haar average $P$ and a basis of the invariant tensors, it gives $P=AWA^*$ with the Weingarten matrix $W=(A^*A)^{-1}$.

Formalization Note The statement is general linear algebra over an arbitrary finite index type n; (Aᴴ * A)⁻¹ is Mathlib's matrix inverse, which is a genuine inverse here because linear independence makes the Gram matrix $A^*A$ invertible. The cases $m=0$ (both sides zero) are included.