LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Geometry error bounds a pulled-back boundary-lift residual

Statement

Assume Countable Choice. Let $\hat{Ω} = (- 1, 1)^{2}$ carry a finite matching affine triangular mesh $T$ as in Matching affine simplicial meshes and shape regularity. Let $Φ, Φ_{h} : \overline{\hat{Ω}} \to R^{2}$ be continuous and $C^{1}$ on each closed triangle, with matching traces on shared edges, and suppose $∥ D Φ ∥_{\infty} + ∥ D Φ_{h} ∥_{\infty} \leq M$ , $e_{0} = ∥ Φ - Φ_{h} ∥_{\infty}$ , and $e_{1} = ∥ D Φ - D Φ_{h} ∥_{L^{\infty}; o p}$ . Let $G$ be a scalar physical boundary lift on an open convex neighborhood containing both images and every segment joining corresponding image points, with $∥ D G ∥_{\infty} \leq L_{1}$ and $∥ D^{2} G ∥_{\infty} \leq L_{2}$ . Define the piecewise pullback gradients by $\nabla_{p w} (G \circ Φ) = D Φ^{T} \nabla G (Φ)$ and $\nabla_{p w} (G \circ Φ_{h}) = D Φ_{h}^{T} \nabla G (Φ_{h})$ , and set $ℓ_{\partial, h} (w) = \int_{\hat{Ω}} (\nabla_{p w} (G \circ Φ) - \nabla_{p w} (G \circ Φ_{h})) \cdot \nabla w, w \in H_{0}^{1} (\hat{Ω}) .$ With the $H^{1}$ dual norm, $∥ ℓ_{\partial, h} ∥_{(H_{0}^{1})^{*}} \leq 2 (L_{1} e_{1} + M L_{2} e_{0})$ . Thus the geometry-induced boundary-lift contribution to the Strang load defect is $O (e_{0} + e_{1})$ .

Facts & Assumptions

Given: Countable Choice; the reference square; continuous, cellwise $C^{1}$ maps with the stated derivative gap and upper bound; a $C^{2}$ lift $G$ on a convex neighborhood of both images; and $w \in H_{0}^{1} (\hat{Ω})$ .

[F1]

Curved-domain geometry approximation errors: $e_{0}$ and $e_{1}$ are the uniform value and derivative gaps between exact and approximate geometry maps.

[F2]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : $D (G \circ Φ) = D Φ^{T} (D G \circ Φ)$ wherever the cell maps are differentiable.

[F3]

Holder's inequality for integrals, including the endpoint cases: $∣ \int f \cdot g ∣ \leq ∥ f ∥_{L^{2}} ∥ g ∥_{L^{2}}$ .

[F4]

Under Countable Choice, the Lebesgue measurable sets form a sigma-algebra containing every elementary set, and Lebesgue measure agrees there with elementary volume. For the half-open box $B = (- 1, 1]^{2}$ , its elementary volume is $4$ . (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume, The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition, Half-open boxes in $R^{n}$ and their volume, Elementary sets: the finite unions of half-open boxes in $R^{n}$ )

[F5]

A measure is nonnegative and finitely additive on disjoint measurable sets; consequently it is monotone on measurable sets, since $E \subseteq B$ gives $B = E \cup (B ∖ E)$ . (Measures on sigma-algebras)

[F6]

Under Countable Choice, on each affine triangle, the Gauss--Green formula applies to a $C^{1}$ vector field on its closure, and the induced orientations on the two copies of a shared edge are opposite in a matching mesh. (Gauss–Green formula on an affine simplex, Interior facet orientations cancel in a matching mesh)

[A1]

Countable Choice is used through [F4] and the Gauss--Green supplier in [F6] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1F1F2F6givenalgebra

Because each geometry map and its traces are continuous across every interior edge, $G \circ Φ$ and $G \circ Φ_{h}$ have matching traces there. Apply [F6] on each triangle to the product of the pulled-back lift with a compactly supported smooth test function; the interior-edge fluxes cancel, and the outer boundary term vanishes. Thus the displayed piecewise gradients are the weak gradients of the pulled-back lifts. On each triangle, [F2] and the triangle inequality give $∣ \nabla_{p w} (G \circ Φ) - \nabla_{p w} (G \circ Φ_{h}) ∣ \leq L_{1} e_{1} + M L_{2} e_{0},$ using the bound on $D^{2} G$ along the joining segment.

2.1F4F5A1step 1.1givenalgebra

For $n \geq 2$ put $B_{n} = (- 1 + 1 / n, 1 - 1 / n]^{2}$ . Each $B_{n}$ is an elementary half-open box in the convention $(a, b]$ , and $(- 1, 1)^{2} = ⋃_{n \geq 2} B_{n}$ : one inclusion is immediate, and for any $x \in (- 1, 1)^{2}$ choose $n$ with $1 / n < \min_{i} {1 + x_{i}, 1 - x_{i}}$ for both coordinates. Thus [F4] makes $\hat{Ω}$ measurable. Since $\hat{Ω} \subset B = (- 1, 1]^{2}$ , [F5] and [F4] give $∣ \hat{Ω} ∣ \leq λ_{2} (B) = 4$ . Step 1.1 therefore yields $∥ \nabla_{p w} (G \circ Φ) - \nabla_{p w} (G \circ Φ_{h}) ∥_{L^{2} (\hat{Ω})} \leq 2 (L_{1} e_{1} + M L_{2} e_{0}) .$

3.1F1F3step 2.1algebra∎

Apply [F3] to the defining integral for $ℓ_{\partial, h} (w)$ and use $∥ \nabla w ∥_{L^{2}} \leq ∥ w ∥_{H^{1}}$ . Taking the supremum over unit $H_{0}^{1}$ tests proves the dual bound.

Depends on

Used by

Strang error bound for a parabolic isoparametric P1 family Theorem

Dependency tree · two levels

56 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 (standard reference, not scraped)
Gerald Dziuk and Charles M. Elliott, Finite element methods for surface PDEs, Acta Numerica 22 (2013) (standard reference, not scraped)