LemmaStatement: 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.

Derivative of the exact-branch FAS two-grid cycle

Statement

Consider one exact-branch two-grid cycle from Finite-budget nonlinear FAS two-grid cycle. Let $F_{h} : U_{h} \to R^{n_{h}}$ and $F_{H} : U_{H} \to R^{n_{H}}$ be $C^{1}$ on open sets, let $I, R, P$ be linear, and suppose $F_{h} (u_{*}) = f_{h}$ and $I u_{*} \in U_{H}$ . Assume the exact coarse solver selects the local root branch through $I u_{*}$ and $D F_{H} (I u_{*})$ is invertible. Suppose the pre/post smoothing maps are $C^{1}$ and fix $u_{*}$ . The selected coarse root $v (u)$ is locally $C^{1}$ , and the derivative of the actual FAS cycle $E$ at $u_{*}$ is $D E (u_{*}) = D S^{p o s t} (u_{*}) [I_{n_{h}} - P D F_{H} (I u_{*})^{- 1} R D F_{h} (u_{*})] D S^{p r e} (u_{*}) .$

No identity between $R$ and $I$ , or between the coarse operator and a rediscretized fine operator, is assumed in this derivative formula.

Facts & Assumptions

Given: The finite-dimensional maps, linear transfers, fine root, selected exact coarse branch, invertible coarse Jacobian, and $C^{1}$ pre/post smoothers in the statement.

[F1]

Finite-budget nonlinear FAS two-grid cycle: after pre-smoothing at $u$ , the coarse target is $g_{H} (u) = F_{H} (I u) + R (f_{h} - F_{h} (u))$ , and an exact coarse solve returns $v (u)$ before the correction $u + P (v (u) - I u)$ .

[F2]

The Euclidean implicit function theorem with derivative formula: for a $C^{1}$ map $G (u, v)$ with $G (u_{*}, v_{*}) = 0$ and invertible partial derivative $D_{v} G (u_{*}, v_{*})$ , there is a local $C^{1}$ root branch $v (u)$ and $D v (u_{*}) = - D_{v} G (u_{*}, v_{*})^{- 1} D_{u} G (u_{*}, v_{*})$ .

[F3]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : for totally differentiable Euclidean maps, $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ .

Proof

1.1givenF1constructalgebra

Define $G (u, v) : = F_{H} (v) - F_{H} (I u) - R (f_{h} - F_{h} (u))$ on the open product domain where its terms are defined. The given fine root gives $G (u_{*}, I u_{*}) = 0$ . Since $I$ and $R$ are linear and $F_{h}, F_{H}$ are $C^{1}$ , $G$ is $C^{1}$ ; its partial derivatives at $(u_{*}, I u_{*})$ are $D_{v} G = D F_{H} (I u_{*})$ and $D_{u} G = - D F_{H} (I u_{*}) I + R D F_{h} (u_{*})$ . The first is invertible by hypothesis.

2.1F2step 1.1algebra

Apply [F2] to $G$ . Its selected local branch satisfies $D v (u_{*}) = - D F_{H} (I u_{*})^{- 1} (- D F_{H} (I u_{*}) I + R D F_{h} (u_{*})) = I - D F_{H} (I u_{*})^{- 1} R D F_{h} (u_{*}) .$

3.1F1step 2.1algebra

The coarse correction map is $C (u) = u + P (v (u) - I u)$ by [F1]. Differentiating and using step 2.1 gives $D C (u_{*}) = I_{n_{h}} + P (D v (u_{*}) - I) = I_{n_{h}} - P D F_{H} (I u_{*})^{- 1} R D F_{h} (u_{*})$ .

4.1givenF3step 3.1algebra∎

The whole cycle is $E = S^{p o s t} \circ C \circ S^{p r e}$ . The pre-smoother fixes $u_{*}$ , and the stated smoother maps are $C^{1}$ , so [F3] and step 3.1 give the displayed formula for $D E (u_{*})$ .

Depends on

Used by

Dependency tree · two levels

11 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)