TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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 joint smoothing-correction estimate gives symmetric two-grid energy contraction

Statement

Let $A_{h}$ , $C$ , $S$ , and $E = S^{*_{A_{h}}} C S$ be as in The symmetric two-grid error map from a pre-smoother and Galerkin correction. Suppose $0 \leq ρ < 1$ and

$∥ C S x ∥_{A_{h}}^{2} \leq ρ ∥ x ∥_{A_{h}}^{2} for every x \in R^{n} .$

Then $E$ is self-adjoint and nonnegative in the $A_{h}$ inner product, and its operator norm induced by $∥ \cdot ∥_{A_{h}}$ satisfies $∥ E ∥_{A_{h}} \leq ρ$ . A rate derived from separate smoothing and approximation inequalities requires a proof that those inequalities imply this joint estimate.

Facts & Assumptions

Given: The fine-grid SPD matrix, exact Galerkin correction $C$ , linear pre-smoother $S$ , and $0 \leq ρ < 1$ satisfying the displayed joint estimate.

[F1]

The symmetric two-grid error map from a pre-smoother and Galerkin correction: $S^{*_{A_{h}}}$ is the adjoint in the $A_{h}$ inner product and $E = S^{*_{A_{h}}} C S$ .

[F2]

The Galerkin coarse correction is an energy-orthogonal projector: $C^{2} = C$ and $C$ is self-adjoint in the energy inner product.

[F3]

The energy inner product $⟨ u, v ⟩_{A} = ⟨ A u, v ⟩$ and energy norm $∥ u ∥_{A}$ for a Hermitian positive-definite matrix: the $A_{h}$ energy inner product is a finite-dimensional real inner product and $∥ x ∥_{A_{h}}^{2} = ⟨ x, x ⟩_{A_{h}}$ .

[F4]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: $∥ E ∥_{A_{h}} = \max_{∥ x ∥_{A_{h}} = 1} ∥ E x ∥_{A_{h}}$ .

[F5]

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis: every self-adjoint endomorphism on a finite-dimensional real inner-product space has an orthonormal eigenbasis.

[F6]

The operator norm is 0 on the zero domain and otherwise equals the largest singular value, attained at a right-singular vector: on a nonzero finite-dimensional real inner-product space, the operator-norm maximum in [F4] exists and is attained.

Proof

1.1F1F2F3algebra

Put $u = S x$ . Since $C^{2} = C$ and $C$ is $A_{h}$ -self-adjoint, $C (I - C) = 0$ and $⟨ C u, (I - C) u ⟩_{A_{h}} = ⟨ u, C (I - C) u ⟩_{A_{h}} = 0$ . Thus [F1] gives $⟨ E x, x ⟩_{A_{h}} = ⟨ C S x, S x ⟩_{A_{h}} = ⟨ C S x, C S x ⟩_{A_{h}} = ∥ C S x ∥_{A_{h}}^{2} \geq 0.$

1.2F1F2algebra

For all $x, y$ , the adjoint identity in [F1] and self-adjointness of $C$ in [F2] give $⟨ E x, y ⟩_{A_{h}} = ⟨ C S x, S y ⟩_{A_{h}} = ⟨ S x, C S y ⟩_{A_{h}} = ⟨ x, E y ⟩_{A_{h}} .$ Hence $E$ is self-adjoint.

2.1F1F4F5F6step 1.1step 1.2algebra∎

By [F5], choose an $A_{h}$ -orthonormal eigenbasis $v_{1}, \dots, v_{n}$ for the self-adjoint map $E$ , with eigenvalues $λ_{j}$ . Step 1.1 gives $λ_{j} = ⟨ E v_{j}, v_{j} ⟩_{A_{h}} \geq 0$ ; the joint hypothesis gives $λ_{j} = ∥ C S v_{j} ∥_{A_{h}}^{2} \leq ρ$ . For $x = \sum_{j} c_{j} v_{j}$ , orthonormality yields $∥ E x ∥_{A_{h}}^{2} = \sum_{j} λ_{j}^{2} c_{j}^{2} \leq ρ^{2} \sum_{j} c_{j}^{2} = ρ^{2} ∥ x ∥_{A_{h}}^{2} .$ The nonzero finite-dimensional domain has an attained operator-norm maximum by [F6], so taking the maximum over unit $x$ in [F4] proves $∥ E ∥_{A_{h}} \leq ρ$ . Since $ρ < 1$ , the two-grid error map is a strict energy contraction.

Depends on

Used by

The symmetric 1D Poisson two-grid cycle is uniformly contractive Theorem

Dependency tree · two levels

18 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

Susanne C. Brenner and L. Ridgway Scott, The Mathematical Theory of Finite Element Methods, 3rd ed., Chapter 6 (standard reference, not scraped)
Numerical Methods II, University of Heidelberg lecture notes, Chapter 10 (standard reference, not scraped)