LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge 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.

Tensor Q1 nodal interpolation has a first-order H1 error bound

Statement

Let $d \in {2, 3}$ and let the unit cube be partitioned into uniform tensor cells of side length $h = 1 / N$ . Let $g \in C^{1} ([0, 1]^{d})$ have Lipschitz gradient with constant $M_{g}$ , meaning $∣ \nabla g (x) - \nabla g (y) ∣ \leq M_{g} ∣ x - y ∣$ for all $x, y$ . Let $I_{h} g$ be the continuous tensor-product, degree-one nodal interpolant matching $g$ at every grid vertex. Then $I_{h} g$ lies in the tensor-product degree-one $C^{0}$ spline space and $∥ g - I_{h} g ∥_{H^{1} ((0, 1)^{d})} \leq C_{d} h M_{g}, C_{d} : = d + \sqrt{d} + 2^{d - 1} d \sqrt{d} .$

Facts & Assumptions

Given: The unit tensor grid, $g$ and its Lipschitz-gradient constant, and the nodal interpolant described in the Statement.

[F1]

B-spline spaces and knot conventions defines degree-one tensor spline factors, and B-spline basis properties and polynomial reproduction gives their piecewise polynomial, continuity, partition and polynomial reproduction properties. On each cell, the tensor nodal shape functions are the products of the two endpoint linear factors in each coordinate; products of the one-dimensional partition/reproduction identities give $\sum_{ν} ϕ_{ν} = 1$ and $\sum_{ν} (x_{ν})_{r} ϕ_{ν} = x_{r}$ for each coordinate $r$ . Hence they reproduce every affine function.

[F2]

For a $C^{1}$ function with $M_{g}$ -Lipschitz gradient, integration along the line segment from $x_{0}$ to $x$ gives $∣ g (x) - g (x_{0}) - \nabla g (x_{0}) \cdot (x - x_{0}) ∣ \leq \frac{1}{2} M_{g} ∣ x - x_{0} ∣^{2}, ∣ \nabla g (x) - \nabla g (x_{0}) ∣ \leq M_{g} ∣ x - x_{0} ∣ .$

Proof

1.1F1F2given

Fix a cell $K$ and one vertex $x_{0}$ . Put $ℓ (x) = g (x_{0}) + \nabla g (x_{0}) \cdot (x - x_{0})$ and $r = g - ℓ$ . The cell diameter is $\sqrt{d} h$ , so [F2] gives $∣ r (x) ∣ \leq (d / 2) h^{2} M_{g}$ on $K$ and $∣ \nabla r (x) ∣ \leq \sqrt{d} h M_{g}$ . The tensor Q1 interpolant reproduces $ℓ$ , hence $g - I_{K} g = r - I_{K} r$ .

2.1F1step 1.1algebra

Let $ϕ_{ν}$ be the $2^{d}$ tensor nodal shape functions. They satisfy $ϕ_{ν} \geq 0$ , $\sum_{ν} ϕ_{ν} = 1$ , and $∣ \nabla ϕ_{ν} ∣ \leq \sqrt{d} / h$ . Thus $∣ I_{K} r ∣ \leq (d / 2) h^{2} M_{g}$ and $∣ \nabla I_{K} r ∣ \leq \sum_{ν} ∣ r (x_{ν}) ∣ ∣ \nabla ϕ_{ν} ∣ \leq 2^{d - 1} d \sqrt{d} h M_{g} .$ Combining these with step 1.1 yields $∣ g - I_{K} g ∣ \leq d h^{2} M_{g}$ and $∣ \nabla (g - I_{K} g) ∣ \leq (\sqrt{d} + 2^{d - 1} d \sqrt{d}) h M_{g}$ .

3.1F1step 2.1givenalgebra∎

Adjacent cells use the same vertex values, so their local interpolants agree on their common faces; consequently $I_{h} g$ is continuous and belongs to the tensor degree-one spline space defined by [F1]. Square the pointwise bounds of step 2.1, integrate on each cell, and sum over the unit-volume partition. The resulting global $L^{2}$ errors are at most $d h^{2} M_{g}$ and $(\sqrt{d} + 2^{d - 1} d \sqrt{d}) h M_{g}$ for value and gradient. Since $h \leq 1$ , the Euclidean combination defining the $H^{1}$ norm is at most their sum, which is bounded by $C_{d} h M_{g}$ .

Depends on

Used by

Smooth compactly supported data have a degree-one NURBS energy rate Theorem

Dependency tree · one level

2 results within one dependency step 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

Stefan Takacs, Numerical Analysis of Isogeometric Methods, complete JKU lecture notes, 2018/19 (standard reference, not scraped)
Annalisa Buffa, Gregor Gantner, Carlotta Giannelli, Dirk Praetorius, Rafael Vázquez, Mathematical Foundations of Adaptive Isogeometric Analysis, Archives of Computational Methods in Engineering 29 (2022) (standard reference, not scraped)