An inexact FAS coarse solve contributes a bounded correction defect

Consider one two-grid FAS cycle with fixed pre-smoothing result, exact selected coarse root $v(u)$, prolongation $P$, and a post-smoother that is $L_{\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{t}}$-Lipschitz on the relevant corrected states. Suppose a coarse solver returns $\widehat{v}$ with residual $\eta =\mathrm{\parallel }{F}_H(\widehat{v})-g_H(u){\mathrm{\parallel }}_2$ and a separately verified residual-to-solution estimate $\mathrm{\parallel }\widehat{v}-v(u){\mathrm{\parallel }}_2\le M_H\eta \mathrm{.}$ Then the inexact-cycle output $\widehat{E}(u)$ and exact-cycle output $E(u)$ satisfy $\mathrm{\parallel }\widehat{E}(u)-E(u){\mathrm{\parallel }}_2\le L_{\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{t}}\mathrm{\parallel }P{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}{M}_H\eta \mathrm{.}$ If the exact cycle satisfies the root-error estimate $\mathrm{\parallel }E(u)-u_{\ast }{\mathrm{\parallel }}_2\le \kappa \mathrm{\parallel }u-u_{\ast }{\mathrm{\parallel }}_2$ on a stated invariant region, then for every iteration input $u_k$ in that region whose exact and inexact corrected states satisfy the preceding hypotheses, $\mathrm{\parallel }{u}_{k+1}-u_{\ast }{\mathrm{\parallel }}_2\le \kappa \mathrm{\parallel }{u}_k-u_{\ast }{\mathrm{\parallel }}_2+L_{\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{t}}\mathrm{\parallel }P{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}{M}_H{\eta }_k\mathrm{.}$ Invertibility of $D{F}_H$ alone is not asserted to imply the stated residual-to-solution estimate; that bound must be proved under additional coarse-operator hypotheses.