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.

The Galerkin coarse correction is an energy-orthogonal projector

Statement

Let $A_{h} \in R^{n \times n}$ be symmetric positive definite and let $P \in R^{n \times m}$ have full column rank, where $1 \leq m \leq n$ . Put $A_{H} = P^{T} A_{h} P$ . Then $A_{H}$ is symmetric positive definite, hence invertible, and the map $C = I_{n} - P A_{H}^{- 1} P^{T} A_{h}$ of Galerkin coarse matrices and the exact coarse-correction error map satisfies

$C^{2} = C, C P = 0, P^{T} A_{h} C = 0, C^{T} A_{h} = A_{h} C .$

Consequently $Ran (C) = Ran (P)^{⊥_{A_{h}}}$ ; $C$ is the orthogonal projector onto that complement in the energy inner product $⟨ x, y ⟩_{A_{h}} : = x^{T} A_{h} y$ .

Facts & Assumptions

Given: A symmetric positive-definite $A_{h} \in R^{n \times n}$ and a full-column-rank $P \in R^{n \times m}$ , where $1 \leq m \leq n$ .

[F1]

Galerkin coarse matrices and the exact coarse-correction error map: $A_{H} = P^{T} A_{h} P$ , and when $A_{H}$ is invertible, $C = I_{n} - P A_{H}^{- 1} P^{T} A_{h}$ .

[F2]

For Hermitian positive-definite $A$ , the exact solution of $A x = b$ is the unique minimizer of the quadratic energy: a real symmetric positive-definite matrix has a unique solution to $A_{H} z = b$ for every right-hand side $b$ , so it is invertible.

[F3]

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

[F4]

Transpose is linear and involutive, and $(A B)^{T} = B^{T} A^{T}$ : transposition is involutive and reverses matrix products, $(X Y)^{T} = Y^{T} X^{T}$ .

Proof

1.1givenF1F2F4algebra

For every nonzero $q \in R^{m}$ , full column rank gives $P q \neq 0$ , so $q^{T} A_{H} q = (P q)^{T} A_{h} (P q) > 0$ . Also $A_{H}^{T} = P^{T} A_{h}^{T} P = A_{H}$ by [F4]. Thus $A_{H}$ is symmetric positive definite and [F2] makes it invertible; [F1] therefore defines $C$ .

2.1F1step 1.1algebra

From $P^{T} A_{h} P = A_{H}$ , direct multiplication gives $C P = P - P A_{H}^{- 1} A_{H} = 0$ and $P^{T} A_{h} C = P^{T} A_{h} - A_{H} A_{H}^{- 1} P^{T} A_{h} = 0$ . Moreover, $C^{2} = I_{n} - 2 P A_{H}^{- 1} P^{T} A_{h} + P A_{H}^{- 1} (P^{T} A_{h} P) A_{H}^{- 1} P^{T} A_{h} = C .$

3.1F1F3F4step 2.1algebra

Transposing $A_{H} A_{H}^{- 1} = I = A_{H}^{- 1} A_{H}$ and using [F4] shows that $(A_{H}^{- 1})^{T}$ is an inverse of $A_{H}^{T} = A_{H}$ . If $B$ and $D$ are two-sided inverses of $A_{H}$ , then $B = B (A_{H} D) = (B A_{H}) D = D$ , so the inverse is unique and $(A_{H}^{- 1})^{T} = A_{H}^{- 1}$ . Thus [F4] yields $C^{T} A_{h} = A_{h} - A_{h} P A_{H}^{- 1} P^{T} A_{h} = A_{h} C$ , so $C$ is self-adjoint in [F3]. Also $P^{T} A_{h} C = 0$ says $Ran (C) \subseteq Ran (P)^{⊥_{A_{h}}}$ . If $w$ is in that complement, then $P^{T} A_{h} w = 0$ , so [F1] gives $C w = w$ ; therefore every such $w$ is in $Ran (C)$ and the ranges are equal.

4.1step 2.1step 3.1∎

The identities in step 2.1 and the range equality in step 3.1 prove all stated projection properties.

Depends on

Used by

Dependency tree · two levels

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