I am interested in the backward stability of numerical algorithms for computation of the singular value decomposition (SVD). Specifically, I am interested in the following result:
Backward stabile computation of the SVD. Assume $\operatorname{poly}(n) u < 1$. There exists an algorithm which takes input $A\in\mathbb{R}^{n\times n}$ runs in $\mathcal{O}(n^3 \log^\beta (n/u))$ (for some $\beta \ge0$) floating point operations of precision $u$ that produces matrices $\hat{U},\hat{\Sigma},\hat{V}$ such that there exist $\Delta A,\Delta U,\Delta V$ for which $$A+\Delta A = (\hat{U}+\Delta U)\hat{\Sigma}(\hat{V}+\Delta V)^\top$$ is an exact singular value decomposition of $A+\Delta A$ and $\|\Delta U\|,\|\Delta V\|,\|\Delta A\|/\|A\| \le \operatorname{poly}(n)u$.
Here, I am happy for $\operatorname{poly}(n)$ to be any nonnegative polynomial function in $n$.
Is there any reference in the literature for this theorem that provides a complete proof (including references to any needed results)?
The literature contains many references to this statement being "well-known". The classic reference of Golub and van Loan states that the conclusion of this theorem "can be shown" (section 5.4.1) for the Golub–Kahan–Reinsch algorithm. I was unable to find a proof in standard books by Demmel and Trefethen and Bau and original references.
Recent work in theoretical computer science (see, e.g., this note) has brought renewed attention to the complexity of core linear algebra problems. In one of the papers in this recent effort, they state that the finite-precision analysis of shifted QR iteration (closely related to the Golub–Kahan–Reinsch algorithm) was unsolved (see section 1.2).
To be clear, my intentions are to find a reference which establishes the unassailable truth of this (purported) theorem as a statement of mathematics. I am well-aware that existing algorithms such as Golub–Kahan–Reinsch appear to obey the conditions of this theorem in practice.