(2.15) and $\Lambda\le2\sqrt{\operatorname{rank}(\mathcal P_A(M))}\|M\|_\infty\le2\sqrt{2\operatorname{rank}(A)}\|M\|_\infty\le\sqrt{2\operatorname{rank}(A)}\lambda$

Let $A=\sum_{j=1}^r\sigma_ju_jv_j^\top$ be a singular value decomposition of a real $m_1\times m_2$ matrix with support $(S_1,S_2)$, let $M$ be any $m_1\times m_2$ matrix, and let $\mathcal P_A(M)=M-P_{S_1^\perp}MP_{S_2^\perp}$ and $\Lambda=2\|\mathcal P_A(M)\|_2$. Then

1. (2.15) $\mathcal P_A(M)=P_{S_1^\perp}MP_{S_2}+P_{S_1}M$;
2. $\Lambda\le2\sqrt{\operatorname{rank}(\mathcal P_A(M))}\,\|M\|_\infty$;
3. $2\sqrt{\operatorname{rank}(\mathcal P_A(M))}\,\|M\|_\infty\le2\sqrt{2\operatorname{rank}(A)}\,\|M\|_\infty$;
4. for every $\lambda\ge2\|M\|_\infty$, $2\sqrt{2\operatorname{rank}(A)}\,\|M\|_\infty\le\sqrt{2\operatorname{rank}(A)}\,\lambda$.

Together: $\Lambda\le2\sqrt{\operatorname{rank}(\mathcal P_A(M))}\|M\|_\infty\le2\sqrt{2\operatorname{rank}(A)}\Delta\le\sqrt{2\operatorname{rank}(A)}\lambda$ with $\Delta=\|M\|_\infty$, which is the bound on $\Lambda$ used to pass from (2.17) to (2.5).

Formalization Note $P_{S_1^\perp}MP_{S_2}$ is written as $MP_{S_2}-P_{S_1}MP_{S_2}$ (rightSingularProjection S M - twoSidedSingularProjection S M). The paper states the chain for the random matrix $\mathbf M$; it holds for every $M$ and is stated so. Rank is Mathlib's Matrix.rank.