LemmaStatement: 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.

Separated Matérn sites have a positive Gram lower bound

Statement

Assume Countable Choice. Fix $d \geq 1$ , $ν > 0$ , $a > 0$ , $s = ν + d / 2$ , and the normalized Matérn kernel with spectral density $w (ξ) = A (a^{2} + 4 π^{2} ∣ ξ ∣^{2})^{- s}$ from The normalized Matérn kernel in the 2π Fourier convention. For a list of $N \geq 2$ distinct sites $X = (x_{1}, \dots, x_{N}) \subset R^{d}$ , put $q = \frac{1}{2} \min_{i \neq j} ∣ x_{i} - x_{j} ∣$ . There is $c = c (d, ν, a) > 0$ such that if $0 < q \leq 1$ , then $λ_{\min} (K_{X}) \geq c q^{2 ν}, λ_{\max} (K_{X}) \leq N, κ_{2} (K_{X}) \leq c^{- 1} N q^{- 2 ν} .$ The eigenvalues and condition number are those of the exact real symmetric positive-definite matrix. For $N = 1$ , $K_{X} = [1]$ and $κ_{2} (K_{X}) = 1$ .

Facts & Assumptions

Given: Countable Choice, fixed Matérn parameters, $N \geq 2$ distinct sites, and $0 < q \leq 1$ .

[F1]

The spectral density is positive, $w (ξ) = A (a^{2} + 4 π^{2} ∣ ξ ∣^{2})^{- s}$ , and $k (z) = \int w (ξ) e^{2 π i z \cdot ξ} d ξ$ . (The normalized Matérn kernel in the 2π Fourier convention, The Matérn spectral integral, normalization, and radial formula)

[F2]

The Matérn kernel is real and even, with $k (0) = 1$ , so its Gram matrix is real symmetric and every diagonal entry is one. (The Matérn spectral integral, normalization, and radial formula)

[F3]

Linear changes of variables scale Lebesgue measure by the absolute determinant; balls are measurable with positive finite measure, translations preserve measure, and Lebesgue measure is finitely additive on disjoint measurable sets. (A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not, Euclidean balls have positive finite Lebesgue measure, Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation, Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume)

[F4]

For a real symmetric matrix, its smallest and largest eigenvalues are the minimum and maximum Rayleigh quotients. (The smallest and largest eigenvalues of a self-adjoint endomorphism are the minimum and maximum Rayleigh quotients, Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis)

[F5]

A smooth bump can be chosen equal to one on the half-radius ball and supported in the unit ball. (A smooth bump between concentric Euclidean balls, Euclidean balls have positive finite Lebesgue measure)

[F6]

The induced matrix 2-norm of a symmetric matrix is its largest absolute eigenvalue. (A symmetric matrix operator norm is its largest absolute Rayleigh quotient, The matrix norm induced by a published vector p-norm)

[F7]

The nonnegative integral is monotone and the modulus of an integral is bounded by the integral of the modulus. (Monotonicity and nonnegative homogeneity of the nonnegative integral, The modulus of an integral is bounded by the integral of the modulus)

[F8]

Smooth compactly supported functions are Schwartz, and the negative-sign, $2 π$ -normalized Fourier transform maps Schwartz functions to Schwartz functions. (Schwartz space and its seminorms, Fourier transform acts continuously on Schwartz space)

[F9]

Euler's formula gives $∣ e^{i t} ∣ = 1$ for real $t$ and $\overline{e^{i t}} = e^{- i t}$ . ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ )

[F10]

For $s > 0$ , $r \mapsto r^{s}$ is increasing on $(0, \infty)$ by its positive derivative and the mean value theorem, so $0 < x \leq y$ implies $x^{- s} \geq y^{- s}$ ; positive-base power laws also give $(r^{- 2})^{- s} = r^{2 s}$ . (Continuity and derivatives of positive-base real powers, The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ , The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents)

[F11]

The positive p-series $\sum_{n \geq 1} n^{- p}$ converges for $p > 1$ . (The p-series for a real exponent p converges exactly when p is greater than one)

[A1]

Countable Choice is inherited from the spectral normalization, ball and Lebesgue measure, and Schwartz Fourier-transform suppliers; no choice of sites or window functions is made from an arbitrary family. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

Proof technique: localized spectral window, packing, and Rayleigh quotients.

Proof

technique · localized spectral window, packing, and Rayleigh quotients

Given: The hypotheses above.

1.1F3F5F7F9A1algebrachoose

By [F5] choose a smooth function $ρ : R^{d} \to [0, 1]$ equal to one on $\overline{B} (0, 1 / 2)$ and supported in $B (0, 1)$ . Set $η (ξ) = (ρ (ξ) + ρ (- ξ)) / 2$ . Then $η$ is smooth, even, nonnegative, at most one, still equals one on the half-radius ball, and is supported in the unit ball. Define $ψ (z) = \int η (ξ) e^{2 π i z \cdot ξ} d ξ$ . Reflection invariance of Lebesgue measure [F3] and Euler's formula [F9] make $ψ$ real and even, and monotonicity [F7] gives $ψ (0) = \int η \geq λ (B (0, 1 / 2)) > 0$ .

2.1F7F8F9step 1.1algebra

Since $η$ is smooth and compactly supported, it is Schwartz by [F8], so $\hat{η}$ is Schwartz and $ψ (z) = \hat{η} (- z)$ is Schwartz as well. For $∣ z ∣ \geq 1$ , choose a coordinate $j$ with $∣ z_{j} ∣ \geq ∣ z ∣ / \sqrt{d}$ ; the Schwartz seminorm $\sup_{ξ} ∣ ξ_{j}^{M} \hat{η} (ξ) ∣ < \infty$ gives $∣ ψ (z) ∣ \leq C_{M} ∣ z ∣^{- M}$ . For $∣ z ∣ \leq 1$ , [F7] and $∣ e^{2 π i z \cdot ξ} ∣ = 1$ from [F9] give $∣ ψ (z) ∣ \leq \int η$ . Combining the two bounds yields $∣ ψ (z) ∣ \leq C_{M}^{'} (1 + ∣ z ∣)^{- M}$ .

3.1F3F11A1step 2.1givenchoose

Fix $i$ . The open balls $B (x_{j}, q)$ are pairwise disjoint because center distances are at least $2 q$ . If $n \leq ∣ x_{i} - x_{j} ∣ / q < n + 1$ , then $B (x_{j}, q) \subset B (x_{i}, (n + 2) q)$ . Translation invariance and dilation change of variables in [F3] give $λ (B (x, r)) = r^{d} λ (B (0, 1))$ ; this unit-ball measure is finite and positive. Finite additivity on the disjoint balls therefore bounds the number of such $j$ by $(n + 2)^{d}$ . Hence, for any integer $M > d + 1$ and $T \geq 1$ , [step 2.1] yields the uniform row-sum estimate $\sum_{j \neq i} ∣ ψ ⁣ (T (x_{i} - x_{j}) / q) ∣ \leq C_{M} T^{- M} \sum_{n \geq 1} (n + 2)^{d} n^{- M} .$ For $n \geq 1$ , $(n + 2)^{d} \leq 3^{d} n^{d}$ , so this series is bounded by $3^{d} \sum_{n \geq 1} n^{- (M - d)}$ , which converges by [F11] because $M - d > 1$ . Choose one fixed $T$ large enough that this upper bound is at most $ψ (0) / 2$ .

4.1F3step 3.1algebra

For any $c \in C^{N}$ , the quadratic form of $H_{i j} = ψ (T (x_{i} - x_{j}) / q)$ satisfies $c^{*} H c \geq (ψ (0) - \max_{i} \sum_{j \neq i} ∣ H_{i j} ∣) ∥ c ∥_{2}^{2} \geq \frac{ψ (0)}{2} ∥ c ∥_{2}^{2},$ because each off-diagonal pair is bounded using $2 ∣ c_{i} ∣ ∣ c_{j} ∣ \leq ∣ c_{i} ∣^{2} + ∣ c_{j} ∣^{2}$ . By the change of variables $ζ = (q / T) ξ$ , $\int_{∣ ξ ∣ \leq T / q} {∣ \sum_{j} c_{j} e^{- 2 π i x_{j} \cdot ξ} ∣}^{2} d ξ \geq \int η (q ξ / T) {∣ \sum_{j} c_{j} e^{- 2 π i x_{j} \cdot ξ} ∣}^{2} d ξ = (T / q)^{d} c^{*} H c .$ The first inequality uses $0 \leq η \leq 1$ and support in the unit ball.

5.1F1F4F10step 4.1algebra

On $∣ ξ ∣ \leq T / q$ and $q \leq 1$ , set $B = (a^{2} + 4 π^{2} T^{2}) q^{- 2}$ . Then $a^{2} + 4 π^{2} ∣ ξ ∣^{2} \leq a^{2} + 4 π^{2} T^{2} / q^{2} \leq B$ . Monotonicity and the power laws [F10] give $w (ξ) \geq A B^{- s} = A {(a^{2} + 4 π^{2} T^{2})}^{- s} q^{2 s} .$ Using the Fourier quadratic-form identity from [F1] and step 4.1 gives $c^{*} K_{X} c \geq c_{0} q^{2 s - d} ∥ c ∥_{2}^{2} = c_{0} q^{2 ν} ∥ c ∥_{2}^{2}$ for a constant $c_{0} > 0$ independent of $X, q, N$ . Thus [F4] yields $λ_{\min} (K_{X}) \geq c_{0} q^{2 ν}$ .

6.1F2F4F6step 5.1algebra∎

By [F4], choose an orthonormal eigenbasis and write $K_{X} = Q Λ Q^{T}$ . If $Q = (q_{i j})$ , then $tr (K_{X}) = \sum_{i} (K_{X})_{i i} = \sum_{i, j} q_{i j}^{2} λ_{j} = \sum_{j} λ_{j} = N,$ since each column of $Q$ has unit norm and [F2] gives diagonal entries $k (0) = 1$ . By step 5.1 all eigenvalues are positive, so $λ_{\max} (K_{X}) \leq N$ . In this eigenbasis the induced 2-norms of $K_{X}$ and $K_{X}^{- 1}$ are $λ_{\max}$ and $1 / λ_{\min}$ , respectively, by [F6]. The definition $κ_{2} (K_{X}) = ∥ K_{X} ∥_{2} ∥ K_{X}^{- 1} ∥_{2}$ therefore gives $κ_{2} (K_{X}) \leq c^{- 1} N q^{- 2 ν}$ . The $N = 1$ case follows directly from $k (0) = 1$ and the same definition.

Depends on

Used by

Dependency tree · two levels

133 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

Narcowich, Ward, and Wendland, Sobolev bounds on functions with scattered zeros, Math. Comp. 74 (2005), §3.1 (standard reference, not scraped)
Gregory E. Fasshauer, MATH 590: Meshfree Methods, Chapter 13, pp. 34–36 (standard reference, not scraped)