TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A smooth FAS cycle converges locally under its actual derivative bounds

Statement

Let $E : U \to R^{n}$ be the actual exact-branch error map of one fixed FAS two-grid or recursive V/W cycle, with $U \subseteq R^{n}$ open. Let $u_{*} \in U$ be a fine root for which the selected smoothers and coarse branches fix $u_{*}$ , so $E (u_{*}) = u_{*}$ . Assume $E$ is $C^{1}$ on a neighborhood of the closed Euclidean ball $K = {\overline{B}}_{2} (u_{*}, r) \subset U$ . Put $q = ∥ D E (u_{*}) ∥_{o p}$ , where for a linear map $T$ the induced Euclidean operator norm is $∥ T ∥_{o p} : = \sup_{∥ v ∥_{2} = 1} ∥ T v ∥_{2}$ . Suppose $q < 1$ and $∥ D E (x) - D E (y) ∥_{o p} \leq L ∥ x - y ∥_{2} (x, y \in K)$ for some $L \geq 0$ . If $q + L r / 2 < 1$ , then $E (K) \subseteq K$ and every iteration $u_{k + 1} = E (u_{k})$ starting in $K$ satisfies $∥ u_{k} - u_{*} ∥_{2} \leq (q + L r / 2)^{k} ∥ u_{0} - u_{*} ∥_{2} .$ This is a local result for the derivative of the actual cycle; it supplies no global-start or mesh-independent rate unless $q, L, r$ are verified uniformly.

Facts & Assumptions

Given: The exact-branch FAS cycle map $E$ , an exact root $u_{*}$ fixed by the cycle, a closed convex ball $K \subset U$ , $q = ∥ D E (u_{*}) ∥_{o p} < 1$ , and the stated Lipschitz bound for $D E$ .

[F1]

An exact fine root is fixed by the FAS V/W cycle: when the smoothers fix exact roots and the coarse solver selects the restricted root at zero defect, the exact-branch V/W FAS cycle fixes the fine root.

[F2]

Derivative of the exact-branch FAS two-grid cycle: for a C1 two-grid exact branch with invertible coarse Jacobian, the actual cycle derivative includes the pre-smoother, $I - P D F_{H} (I u_{*})^{- 1} R D F_{h} (u_{*})$ , and the post-smoother.

[F3]

Vector Newton remainder under a Lipschitz Jacobian: for a C1 map on a convex set with $L$ -Lipschitz derivative, the endpoint Taylor remainder is bounded by $L ∥ x - x_{*} ∥_{2}^{2} / 2$ .

Proof

technique · contraction

1.1F1F2given

In the two-grid case, [F2] identifies $D E (u_{*})$ as the derivative of the actual pre-smoother, implicit coarse-branch correction, and post-smoother composition. For a recursive V/W cycle, $q$ in the hypotheses is the derivative norm of that full composed map.

1.2givenF1F3algebra

Fix $x \in K$ and put $e = x - u_{*}$ . Apply [F3] with its variables $x = u_{*}$ and $x_{*} = x$ . Reversing the resulting difference and using $E (u_{*}) = u_{*}$ gives $∥ E (x) - u_{*} - D E (u_{*}) e ∥_{2} \leq \frac{L}{2} ∥ e ∥_{2}^{2} .$ Thus, since $∥ D E (u_{*}) ∥_{o p} = q$ and $∥ e ∥_{2} \leq r$ , $∥ E (x) - u_{*} ∥_{2} \leq q ∥ e ∥_{2} + \frac{L}{2} ∥ e ∥_{2}^{2} \leq κ ∥ e ∥_{2}, κ : = q + L r / 2 < 1.$

2.1step 1.2algebra

For $x \in K$ , step 1.2 gives $∥ E (x) - u_{*} ∥_{2} \leq κ ∥ x - u_{*} ∥_{2} \leq κ r < r$ , so $E (x) \in K$ . This proves invariance of the stated ball.

3.1step 1.2step 2.1algebra∎

For an iterate starting at $u_{0} \in K$ , invariance keeps every $u_{k}$ in $K$ and step 1.2 gives $∥ u_{k + 1} - u_{*} ∥_{2} \leq κ ∥ u_{k} - u_{*} ∥_{2}$ . Induction yields $∥ u_{k} - u_{*} ∥_{2} \leq κ^{k} ∥ u_{0} - u_{*} ∥_{2}$ ; because $0 \leq κ < 1$ , the right side tends to zero.

Remarks

For the two-grid exact-branch cycle, Derivative of the exact-branch FAS two-grid cycle gives the derivative to be checked. For a recursive V/W cycle, the bound must be checked for the complete composed cycle. The one-sided estimate toward $u_{*}$ does not assert a Banach contraction bound between every pair of points in $K$ .

Depends on

Used by

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

William L. Briggs, Van Emden Henson, and Steve F. McCormick, A Multigrid Tutorial, 2nd ed., Chapter 6 (standard reference, not scraped)
Harald van Brummelen, Basics of Multigrid Methods, SINTEF winter-school lecture notes (standard reference, not scraped)
Van Emden Henson, Multigrid Methods for Nonlinear Problems: An Overview, UCRL-JC-150259 (standard reference, not scraped)