CorollaryStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pendingjudge 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.

Perturbed conforming solves are controlled by the exact Galerkin baseline

Statement

Assume Countable Choice and the exact conforming Galerkin hypotheses of Hermitian Galerkin solutions are best in the energy norm, with Hermitian form $a$ bounded by $M$ in $∥ \cdot ∥_{V}$ . Let $u_{h}^{G}$ be the exact Galerkin solution. Let $a_{h}$ be a bounded discrete form on the same $V_{h}$ , coercive in $∥ \cdot ∥_{V}$ with constant $α_{h} > 0$ , and let $F_{h}$ be a bounded discrete load with the matching test-linearity. Its unique perturbed solution ${\tilde{u}}_{h}$ satisfies

$∥ u - {\tilde{u}}_{h} ∥_{a} \leq \inf_{v_{h} \in V_{h}} ∥ u - v_{h} ∥_{a} + \frac{\sqrt{M}}{α_{h}} ρ_{h},$

where $ρ_{h} : = \sup_{w_{h} \neq 0} ∣ F_{h} (w_{h}) - a_{h} (u_{h}^{G}, w_{h}) ∣ / ∥ w_{h} ∥_{V}$ , defined as zero if $V_{h} = {0}$ . This uses the exact Galerkin solution as a baseline; $ρ_{h}$ must be bounded from the actual form and load defects.

Facts & Assumptions

Given: The Countable-Choice bounded coercive Hermitian Galerkin setting, its exact Galerkin solution $u_{h}^{G}$ , and a bounded coercive perturbed form/load with the stated residual $ρ_{h}$ , including its zero-space convention.

[F1]

Hermitian Galerkin solutions are best in the energy norm: $∥ u - u_{h}^{G} ∥_{a} = \inf_{v_{h} \in V_{h}} ∥ u - v_{h} ∥_{a}$ .

[F2]

The Lax--Milgram theorem under The Axiom of Countable Choice ( ${A C}_{ω}$ ): the perturbed bounded coercive form on the finite-dimensional Hilbert space has a unique solution ${\tilde{u}}_{h}$ .

[F3]

Bounded, coercive and symmetric sesquilinear forms: boundedness gives $∥ z ∥_{a}^{2} = a (z, z) \leq M ∥ z ∥_{V}^{2}$ and discrete coercivity gives $Re a_{h} (z, z) \geq α_{h} ∥ z ∥_{V}^{2}$ .

[A1]

$ρ_{h}$ is the residual supremum in the Statement, with the stated value zero when $V_{h} = {0}$ .

Proof

1.1F2given

The perturbed form and load are bounded and coercive on $V_{h}$ , so [F2] gives a unique ${\tilde{u}}_{h} \in V_{h}$ satisfying $a_{h} ({\tilde{u}}_{h}, w_{h}) = F_{h} (w_{h})$ for all $w_{h} \in V_{h}$ .

2.1F3A1step 1.1algebra

Put $e_{h} : = {\tilde{u}}_{h} - u_{h}^{G}$ . Use the discrete equation with test $e_{h}$ and the residual definition [A1] to obtain $α_{h} ∥ e_{h} ∥_{V}^{2} \leq Re a_{h} (e_{h}, e_{h}) = Re (F_{h} (e_{h}) - a_{h} (u_{h}^{G}, e_{h})) \leq ρ_{h} ∥ e_{h} ∥_{V}$ .

3.1F3step 2.1algebra

If $e_{h} = 0$ the claim is immediate; otherwise divide step 2.1 by $α_{h} ∥ e_{h} ∥_{V}$ and use [F3] to get $∥ e_{h} ∥_{a} \leq \sqrt{M} ρ_{h} / α_{h}$ .

4.1F1step 3.1algebra∎

The triangle inequality and [F1] now give $∥ u - {\tilde{u}}_{h} ∥_{a} \leq ∥ u - u_{h}^{G} ∥_{a} + ∥ e_{h} ∥_{a} \leq \inf_{v_{h} \in V_{h}} ∥ u - v_{h} ∥_{a} + \sqrt{M} ρ_{h} / α_{h}$ , as required.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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 Fall 2025, Part VI, Chapter 27, Error analysis with variational crimes (standard reference, not scraped)
Joachim Schöberl, Numerical Methods for Partial Differential Equations, Chapter 25, Non-conforming Finite Element Methods (standard reference, not scraped)