TheoremStatement: Literature-sourcedProof: 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.

Augmented RBF-FD weights reproduce polynomials and obey a local Taylor bound

Statement

Let $p \geq 0$ be an integer, let $Y = (y_{1}, \dots, y_{N})$ be distinct and $(p + 1)$ -unisolvent for $Π_{p} (R^{d})$ , and let $K$ be a real strictly conditionally positive-definite kernel of order $p + 1$ . Fix a center $x$ , an ordered basis $p_{1}, \dots, p_{J}$ of $Π_{p}$ , and a homogeneous constant-coefficient differential functional $L$ of order $t \leq p$ for which all section derivatives in Exact augmented RBF-FD weights for a local differential functional exist. Let $(w, v)$ be the exact output of that procedure and put $r_{Y} = \max_{i} ∣ y_{i} - x ∣$ . Then the procedure returns success, and for every $q \in Π_{p}$ , $\sum_{i = 1}^{N} w_{i} q (y_{i}) = L q (x) .$ If $f \in C^{p + 1} (U)$ on an open convex set $U$ containing the compact convex hull $H = conv {x, y_{1}, \dots, y_{N}}$ , then $∣ \sum_{i} w_{i} f (y_{i}) - L f (x) ∣ \leq C_{d, p} (\sum_{i} ∣ w_{i} ∣) r_{Y}^{p + 1} \max_{∣ α ∣ = p + 1} \sup_{z \in H} ∣ D^{α} f (z) ∣ .$ Consequently, when $r_{Y} > 0$ , a separately proved bound $\sum_{i} ∣ w_{i} ∣ \leq C_{w} r_{Y}^{- t}$ yields the order $C_{d, p} C_{w} r_{Y}^{p + 1 - t}$ truncation bound. Unisolvence alone is not asserted to provide this weight-norm bound.

Facts & Assumptions

Given: The sites, kernel, polynomial basis, center, functional, and function hypotheses in the Statement.

[F1]

The exact algorithm forms the augmented matrix with blocks $K_{Y}, P, P^{T}, 0$ , right side $(b, ℓ)$ , and applies deterministic Gaussian elimination with row pivoting; the lower block of any solution is $P^{T} w = ℓ$ . (Exact augmented RBF-FD weights for a local differential functional)

[F2]

Under strict conditional positive definiteness of order $p + 1$ and $(p + 1)$ -unisolvence, the augmented matrix is invertible for every right-hand side. (Strict positive and conditionally positive augmented interpolation systems are invertible, Radial kernels, polynomial augmentation, and site geometry)

[F3]

Taylor's theorem gives a degree- $p$ polynomial $T_{p} f$ at $x$ whose value remainder at $y$ is bounded by $C_{d, p} ∣ y - x ∣^{p + 1}$ times the supremum of all order- $(p + 1)$ partial derivatives on the segment. (Multivariable Taylor formula with a Lagrange remainder along a line segment)

Proof

technique · exact elimination, moment equations, and Taylor cancellation

Given: The hypotheses above. All linear algebra and arithmetic in the algorithm are exact.

1.1F1F2inductionalgebra

Let $M$ be the augmented matrix and $g$ its right side in [F1]. It is square and invertible by [F2]. Initially the leading $0 \times 0$ pivot block is invertible. Inductively suppose the first $k - 1$ pivots have been nonzero. After their row swaps and elimination, the row-equivalent matrix has block form $[\begin{array}{cc} U & B \\ 0 & S \end{array}]$ with $U$ invertible and $S$ the remaining Schur complement. The block matrix is invertible, so $S$ is invertible: if $S z = 0$ , then $(- U^{- 1} B z, z)$ would be a nonzero vector in its kernel. If the first column of $S$ were zero, its first coordinate vector would be a nonzero kernel vector. Thus the finite set of remaining entries in column $k$ contains a nonzero entry, and the algorithm's least-index rule finds a nonzero pivot. Row swaps and adding multiples of pivot rows are invertible elementary row operations, so they preserve the solution set. After $N + J$ pivots the matrix is upper triangular with nonzero diagonal, and descending substitution returns the unique solution. Therefore the singular-system status is unreachable under the hypotheses.

2.1F1step 1.1algebra

Writing the returned vector as $(w, v)$ , its lower block equation is $P^{T} w = ℓ$ . For each basis polynomial $p_{j}$ , this says $\sum_{i} w_{i} p_{j} (y_{i}) = L p_{j} (x)$ . Every $q \in Π_{p}$ is a linear combination $q = \sum_{j} a_{j} p_{j}$ , so multiplying these identities by $a_{j}$ and summing, using linearity of $L$ , gives $\sum_{i} w_{i} q (y_{i}) = L q (x)$ .

3.1F3step 2.1algebra

Let $T_{p} f$ be the Taylor polynomial of $f$ at $x$ of total degree at most $p$ . Since $t \leq p$ , its derivatives at $x$ through order $t$ agree with those of $f$ , so $L T_{p} f (x) = L f (x)$ . Applying step 2.1 to $T_{p} f$ gives $\sum_{i} w_{i} T_{p} f (y_{i}) = L f (x)$ .

4.1F3step 3.1algebra∎

Subtract the identity in step 3.1 from the sampled sum for $f$ . For every $i$ , [F3] bounds $∣ f (y_{i}) - T_{p} f (y_{i}) ∣$ by $C_{d, p} ∣ y_{i} - x ∣^{p + 1}$ times the derivative supremum on $H$ , since each segment lies in the convex hull $H$ . The triangle inequality and $∣ y_{i} - x ∣ \leq r_{Y}$ now give the stated truncation estimate. When $r_{Y} > 0$ , the additional weight bound yields the final conditional rate.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Exact augmented RBF-FD weights for a local differential functional.

Dependency tree · two levels

11 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

Accelerated Training of Physics-Informed Neural Networks (PINNs) using Meshless Discretizations (standard reference, not scraped)
Narcowich, Ward, and Wendland, Sobolev bounds on functions with scattered zeros, Math. Comp. 74 (2005), §3.1 (standard reference, not scraped)