Problem

Solve a consistent system $Ax=b$, with $A\in\mathbb{C}^{m\times n}$ of full rank and $m\ge n\ge 1$. Kaczmarz's method (1937) projects the current iterate onto the solution hyperplane of one equation at a time. The cyclic version converges, but its rate depends on the order of the rows and has no clean bound in terms of a condition number.

Strohmer and Vershynin (2009) pick row $i$ at random with probability $\|a_i\|_2^2/\|A\|_F^2$ and prove

$$\mathbb{E}\,\|x_k-x\|_2^2 \le \bigl(1-\kappa(A)^{-2}\bigr)^k\,\|x_0-x\|_2^2,\qquad \kappa(A)=\frac{\|A\|_F}{\sigma_{\min}(A)}.$$

The rate does not depend on the number of equations $m$.

Setting

• Rows. $a_i\in\mathbb{C}^n$ is the conjugate of row $i$, so equation $i$ reads $\langle a_i,x\rangle=b_i$.
• Condition number. $\sigma_{\min}(A)=\inf_{\|z\|_2=1}\|Az\|_2$ and $\kappa(A)=\|A\|_F/\sigma_{\min}(A)$ (Demmel). It satisfies $\sqrt n\le\kappa(A)\le\sqrt n\,\|A\|_2/\sigma_{\min}(A)$.
• Algorithm 1. From any $x_0$, draw row $r$ independently with probability $p_r=\|a_r\|_2^2/\|A\|_F^2$ and set

$$x_{k+1}=x_k+\frac{b_r-\langle a_r,x_k\rangle}{\|a_r\|_2^2}\,a_r .$$

• Expectation. $\mathbb{E}\|x_k-x\|_2^2$ is a finite sum over the $m^k$ possible row sequences.

Targets

• Theorem 2 (goal): the bound above, for every $x_0$ and $k$.
• Theorem 3: some $x_0\ne x$ has $\mathbb{E}\|x_k-x\|_2^2\ge(1-2k/\kappa(A)^2)\|x_0-x\|_2^2$ for all $k\ge1$, so $\kappa(A)^{-2}$ is sharp up to a constant. Caveat: the source's proof only reaches the unsquared bound $\mathbb{E}\|x_k-x\|_2\ge\dots$ and then cites Jensen, which goes the wrong way. Its estimates give the squared bound with $4$ in place of $2$. Both forms are milestones.
• Sharpness (§3.2): Theorem 2 is an equality when $\kappa(A)=\sqrt n$.
• Iteration count (§2.1): $k\ge 2\log\varepsilon/\log(1-\kappa(A)^{-2})$ steps give $\mathbb{E}\|x_k-x\|_2^2\le\varepsilon^2\|x_0-x\|_2^2$.

Proof idea

A single projection can barely reduce the error, when the error is almost orthogonal to the chosen row. On average it always does. If $Z=a_j/\|a_j\|_2$ is drawn with probability $p_j$, then

$$\mathbb{E}\,|\langle z,Z\rangle|^2=\frac{\|Az\|_2^2}{\|A\|_F^2}\ge\kappa(A)^{-2}\|z\|_2^2 .$$

Pythagoras for one projection then gives $\mathbb{E}\|x_{k+1}-x\|_2^2\le(1-\kappa(A)^{-2})\,\|x_k-x\|_2^2$; induct on $k$.

Formalization

• Vectors live in EuclideanSpace ℂ (Fin n) and matrices in Matrix (Fin m) (Fin n) ℂ. Mathlib's inner product is conjugate-linear in its first argument, which is why $a_i$ is a conjugated row.
• Full rank is stated as injectivity of $z\mapsto Az$.
• The expectation expErrSq is an explicit finite sum, so no measure theory is needed. The tower identity is a milestone.
• A zero row makes the step the identity (Lean's division by zero) and has probability $0$, so it is harmless.
• Mathlib has no Kaczmarz iteration, scaled condition number or $\sigma_{\min}$ lower bound; the mission builds them.

History

• 1937: Kaczmarz introduces the cyclic method and proves convergence, with no rate.
• 1970: Gordon, Bender and Herman rediscover it as ART for tomography.
• 2009: Strohmer and Vershynin give the first rate in terms of a condition number.
• 2010 onward: extensions to noisy systems, block methods, SGD and sketch-and-project (Needell; Needell–Tropp; Needell–Srebro–Ward; Gower–Richtárik).

References

• S. Kaczmarz, Angenäherte Auflösung von Systemen linearer Gleichungen, Bull. Int. Acad. Polon. Sci. Lett. A 35 (1937), 355–357.
• T. Strohmer and R. Vershynin, A randomized Kaczmarz algorithm with exponential convergence, J. Fourier Anal. Appl. 15 (2009), 262–278. arXiv:math/0702226
• J. Demmel, The probability that a numerical analysis problem is difficult, Math. Comp. 50 (1988), 449–480. DOI
• D. Needell, Randomized Kaczmarz solver for noisy linear systems, BIT Numer. Math. 50 (2010), 395–403. arXiv:0902.0958
• D. Needell, N. Srebro and R. Ward, Stochastic gradient descent, weighted sampling, and the randomized Kaczmarz algorithm, Math. Program. 155 (2016), 549–573. arXiv:1310.5715
• R. M. Gower and P. Richtárik, Randomized iterative methods for linear systems, SIAM J. Matrix Anal. Appl. 36 (2015), 1660–1690. arXiv:1506.03296