Averaged-operator inequality ($\Vert Tz-Tw{\Vert }^2\le \Vert z-w{\Vert }^2-\frac{1-\alpha }{\alpha }\Vert (I-T)z-(I-T)w{\Vert }^2$)

The defining averaging representation is equivalent to $\Vert Tz-Tw{\Vert }^2\le \Vert z-w{\Vert }^2-(1-\alpha )\Vert (I-T)z-(I-T)w{\Vert }^2/\alpha$. Expanding the norm of the convex combination proves both directions. Substituting a fixed point for $w$ gives Fejér monotonicity and summability of squared residuals.