LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

The conforming energy projection is the best approximation

Statement

Assume Countable Choice. Let $V$ be a Hilbert space, let $a$ be a bounded, Hermitian coercive form on $V$ , and let $V_{h} \subseteq V$ be finite-dimensional. Write $∥ v ∥_{a} : = \sqrt{a (v, v)}$ for the induced energy norm. For each $v \in V$ , let $P_{h} v \in V_{h}$ be the unique solution of $a (P_{h} v, w_{h}) = a (v, w_{h}) (w_{h} \in V_{h}) .$ Then $P_{h} : V \to V_{h}$ is linear, $a (v - P_{h} v, w_{h}) = 0$ for all $w_{h} \in V_{h}$ , and $∥ v - P_{h} v ∥_{a} = \inf_{w_{h} \in V_{h}} ∥ v - w_{h} ∥_{a} .$ If $E \subseteq V$ is a nonzero finite-dimensional subspace and $δ_{a} (E, V_{h}) < 1$ , then $P_{h} ∣_{E}$ is injective.

Facts & Assumptions

Given: Countable Choice, the bounded Hermitian coercive form, the finite-dimensional conforming subspace $V_{h}$ , and a finite-dimensional $E \subseteq V$ .

[F1]

Céa's theorem gives unique continuous and discrete solutions for a bounded coercive form and bounded data (Céa quasi-optimality for coercive conforming Galerkin problems).

[F2]

The continuous and discrete variational equations imply $a (u - u_{h}, w_{h}) = 0$ for every $w_{h} \in V_{h}$ (Galerkin orthogonality for conforming approximations).

[F3]

For a Hermitian form, the Galerkin solution is exactly the best approximation in the energy norm (Hermitian Galerkin solutions are best in the energy norm).

[F4]

The directed eigenspace best-approximation gap is $δ_{a} (E, V_{h}) = \sup_{v \in E, ∥ v ∥_{a} = 1} \inf_{w_{h} \in V_{h}} ∥ v - w_{h} ∥_{a}$ (Best-approximation gap of a finite-dimensional eigenspace).

Proof

technique · direct

Given: $v \in V$ , the form $a$ , the subspace $V_{h}$ , and the subspace $E$ .

1.1F1givenconstruct

For fixed $v$ , the functional $w \mapsto a (v, w)$ is bounded and conjugate-linear. Apply [F1] to the continuous datum $F (w) = a (v, w)$ ; its continuous solution is $v$ , and the resulting discrete solution is the unique $P_{h} v \in V_{h}$ in the statement. If $v_{1}, v_{2} \in V$ and $c_{1}, c_{2} \in K$ , then $c_{1} P_{h} v_{1} + c_{2} P_{h} v_{2}$ satisfies the defining equation for $P_{h} (c_{1} v_{1} + c_{2} v_{2})$ , so uniqueness proves linearity.

2.1F2step 1.1given

The continuous equation for $v$ and the defining discrete equation for $P_{h} v$ agree on each $w_{h} \in V_{h}$ . By [F2], $a (v - P_{h} v, w_{h}) = 0$ .

3.1F2F3step 1.1step 2.1givenalgebra

Fix any $w_{h} \in V_{h}$ . Since $v - w_{h} = (v - P_{h} v) + (P_{h} v - w_{h})$ and $P_{h} v - w_{h} \in V_{h}$ , step 2.1 and Hermitian symmetry eliminate both cross terms in the squared energy norm. Therefore $∥ v - w_{h} ∥_{a}^{2} = ∥ v - P_{h} v ∥_{a}^{2} + ∥ P_{h} v - w_{h} ∥_{a}^{2} \geq ∥ v - P_{h} v ∥_{a}^{2} .$ The choice $w_{h} = P_{h} v$ attains equality, proving the best-approximation identity (the exact supplier interface [F3]).

4.1F3F4step 3.1algebra∎

If $v \in E$ is nonzero, put $\hat{v} = v / ∥ v ∥_{a}$ . By linearity in step 1.1 and the definition [F4], $∥ v - P_{h} v ∥_{a} = ∥ v ∥_{a} ∥ \hat{v} - P_{h} \hat{v} ∥_{a} \leq δ_{a} (E, V_{h}) ∥ v ∥_{a}$ ; the same inequality is immediate for $v = 0$ . If $P_{h} v = 0$ , step 3.1 makes the left side $∥ v ∥_{a}$ . Since $δ_{a} (E, V_{h}) < 1$ , this forces $v = 0$ . Thus $P_{h} ∣_{E}$ is injective.

Depends on

Used by

Dependency tree · two levels

19 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

Jean-Luc Guermond, MATH 661 Finite Element Methods, Fall 2025, Chapter 47 (standard reference, not scraped)
Bertrand Mercier, Topics in Finite Element Solution of Elliptic Problems, Chapter 8 (standard reference, not scraped)