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.
Shape-regular affine finite elements supply the Strang approximation term
Statement
Assume Countable Choice and let . Let be a matching shape-regular affine simplicial mesh as in Matching affine simplicial meshes and shape regularity. Set , so for an empty mesh. Let be a conforming zero-boundary P1 Lagrange subspace of a Hilbert space , with , and let be the global nodal interpolant of whose boundary nodal values vanish. Assume for . The reference nodal functionals are bounded on , and the exact/discrete variational problems satisfy the hypotheses of First Strang estimate for conforming perturbed Galerkin problems, with exact solution and discrete coercivity . Then a constant depending only on the reference P1 element and shape-regularity bound satisfies
If uniformly, the displayed approximation contribution is ; the geometry, quadrature, and load defects remain separate terms and require their own estimates.
Facts & Assumptions
Given: Countable Choice; or ; a matching shape-regular affine simplicial mesh with ; a conforming P1 Lagrange family in ; with zero boundary nodal values; a global interpolant ; and the bounded/coercive exact and discrete forms and loads of the first Strang theorem.
Matching affine simplicial meshes and shape regularity: cells are nondegenerate affine simplices, their interiors are disjoint, and intersections are whole matching faces; shape regularity bounds diameter divided by inradius.
Reference finite elements and unisolvent degrees of freedom: an unisolvent reference element defines its interpolation operator from its degrees of freedom.
Broken and conforming polynomial spaces on a matching mesh: conformity means matching polynomial traces on each interior facet, and the zero-boundary subspace has zero polynomial trace on every boundary facet.
Local interpolation estimates on shape-regular affine meshes: for the P1 Lagrange element, , , , and , uniformly on the shape-regular affine mesh.
First Strang estimate for conforming perturbed Galerkin problems: the conforming error is bounded by its best-approximation term and the actual discrete form/load defects.
Under Countable Choice, a bounded piece of an affine hyperplane is contained in the graph of an affine function over a closed nondegenerate rectangle. Such a graph has Jordan content zero (The graph of a continuous function on a closed nondegenerate rectangle in has content zero in ) and is Lebesgue measurable of measure zero (Lebesgue outer measure is at most Jordan outer content, and a bounded Jordan measurable set is Lebesgue measurable with Lebesgue measure equal to its Jordan content, Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume); its subsets are measurable null sets by completeness. Finite unions of facets are null by finite subadditivity (Finite and countable subadditivity of measures).
For every nonnegative measurable , is a measure and its integral over a null set is zero (The indefinite integral of a nonnegative measurable function is a measure, A nonnegative integral over a null set vanishes).
The global nodal interpolant has matching traces and zero boundary nodal values, and it belongs to as stipulated in the Statement.
The reference P1 nodal functionals are bounded on , as assumed in the Statement; no point-evaluation theorem or stronger choice principle is used to infer this hypothesis here.
Proof
By [A2], the reference nodal degrees of freedom are bounded on ; together with unisolvence [F2], this gives the local Lagrange interpolants required by [F4]. Unisolvence also identifies each restriction with the local interpolant . Apply [F4] with , , , and on every cell .
On a shared facet, both neighboring P1 traces are affine and have the same values at every facet vertex, so the traces agree. Every boundary facet has zero values at all its vertices, so its affine trace is zero. Thus the assembled function has the conformity and boundary traces in [F3]; its membership in is the explicit hypothesis [A1].
Let be the union of the mesh facets. Each facet lies in an affine hyperplane; choosing a coordinate with nonzero normal coefficient writes that hyperplane as the graph of an affine function over the other coordinates. A closed nondegenerate rectangle containing the facet's projection gives a bounded graph containing the facet, so [F6] makes each facet, and hence , a Lebesgue null set. By [F7], for every nonnegative measurable the integral over is the sum of its integrals over the disjoint cell interiors , since and . Applying this to the squared first derivatives of and the squared second derivatives of gives the global seminorm decompositions used next.
Square the cell estimate in [F4] and sum over the cells using step 1.3. Their interiors are disjoint and , so , hence .
Apply [F5] with and use from the stated norm bound and step 2.1. This gives the displayed error estimate without absorbing the form, geometry, quadrature, or load defects.
Depends on
- Variational-crime settings and consistency defects
- First Strang estimate for conforming perturbed Galerkin problems
- Matching affine simplicial meshes and shape regularity
- Reference finite elements and unisolvent degrees of freedom
- Broken and conforming polynomial spaces on a matching mesh
- Local interpolation estimates on shape-regular affine meshes
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Integer-order Sobolev spaces and their norms
- The graph of a continuous function on a closed nondegenerate rectangle in $\mathbb{R}^m$ has content zero in $\mathbb{R}^{m+1}$
- Lebesgue outer measure is at most Jordan outer content, and a bounded Jordan measurable set is Lebesgue measurable with Lebesgue measure equal to its Jordan content
- Assuming countable choice, $\mathcal{L}(\mathbb{R}^n)$ is a sigma-algebra containing every elementary set and $\lambda_n$ is a complete measure extending elementary volume
- Finite and countable subadditivity of measures
- The indefinite integral of a nonnegative measurable function is a measure
- A nonnegative integral over a null set vanishes
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
78 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, Chapter 11, Local interpolation on affine meshes (standard reference, not scraped)
- Joachim Schöberl, Numerical Methods for Partial Differential Equations, Chapter 4 (standard reference, not scraped)