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

Finite-node Nyström equations are equivalent to their reconstructed equations

Statement

Let $X : = C ([0, 1], R)$ (The space $C (K, R)$ of continuous real-valued functions on a nonempty compact metric space), let $m \geq 1$ , let $y_{1}, \dots, y_{m} \in [0, 1]$ , and let $ψ_{1}, \dots, ψ_{m} \in X$ . Define the finite-rank linear map $(F u) (x) : = \sum_{j = 1}^{m} ψ_{j} (x) u (y_{j})$ and, for $f \in X$ , define the square matrix and vector $M_{i j} : = δ_{i j} - ψ_{j} (y_{i}), b_{i} : = f (y_{i}), 1 \leq i, j \leq m .$ Then the solutions of $(I - F) u = f$ are in bijection with the solutions $c \in R^{m}$ of $M c = b$ , via $u (x) = f (x) + \sum_{j = 1}^{m} ψ_{j} (x) c_{j}, c_{i} = u (y_{i}) .$ The nullspaces of $I - F$ and $M$ are linearly isomorphic by $c \mapsto \sum_{j} ψ_{j} c_{j}$ . In particular, $I - F$ is bijective if and only if $M$ is nonsingular.

Facts & Assumptions

Given: The space $X$ , nodes $y_{i}$ , continuous coefficient functions $ψ_{i}$ , and $f \in X$ as in the Statement.

[F1]

The space $C (K, R)$ of continuous real-valued functions on a nonempty compact metric space: members of $X$ are continuous real-valued functions on $[0, 1]$ , so finite linear combinations of the $ψ_{j}$ and $f$ lie in $X$ .

[F2]

Rank-nullity: $\dim_{F} V = nullity T + rank T$ : a linear map on the finite-dimensional space $R^{m}$ is injective if and only if it is surjective, hence a square matrix is nonsingular exactly when its kernel is zero.

Proof

Given: The data in the Statement, the operator $F$ , the matrix $M$ , and the vector $b$ .

1.1givenF1algebra

If $u$ solves $(I - F) u = f$ , put $c_{i} : = u (y_{i})$ . Evaluating $u (x) - \sum_{j} ψ_{j} (x) u (y_{j}) = f (x)$ at $x = y_{i}$ gives $c_{i} - \sum_{j} ψ_{j} (y_{i}) c_{j} = f (y_{i})$ for every $i$ , which is exactly $M c = b$ .

2.1givenF1step 1.1algebraconstruct

Conversely, if $M c = b$ , define $u (x) : = f (x) + \sum_{j} ψ_{j} (x) c_{j}$ . By [F1] this lies in $X$ . The matrix equation gives $u (y_{i}) = f (y_{i}) + \sum_{j} ψ_{j} (y_{i}) c_{j} = c_{i}$ for each $i$ , so $u = f + F u$ and it solves $(I - F) u = f$ . These constructions are inverse because each reconstructed function has the prescribed grid values.

3.1givenF2step 2.1algebra∎

If $M c = 0$ and $c \neq 0$ , set $v (x) : = \sum_{j} ψ_{j} (x) c_{j}$ . The homogeneous matrix equations imply $v (y_{i}) = c_{i}$ ; hence $v \neq 0$ and $F v = v$ . Thus a nonzero matrix kernel gives a nonzero kernel of $I - F$ . Conversely, if $(I - F) v = 0$ and $v \neq 0$ , then $c_{i} : = v (y_{i})$ satisfies $M c = 0$ ; if $c = 0$ , the formula $v = F v = \sum_{j} ψ_{j} v (y_{j})$ would give $v = 0$ , a contradiction. Therefore the two kernels are simultaneously trivial. By [F2] this is equivalent to $M$ being nonsingular; [step 2.1] then gives bijective solvability of the reconstructed equation exactly when the matrix is nonsingular.

Depends on

Used by

Dependency tree · two levels

14 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

Andreas Neubauer and Ronny Ramlau, Lecture Notes: Integral Equations and Boundary Value Problems, §3.3 (standard reference, not scraped)
Habib Ammari, Brian Fitzpatrick, and Sanghyeon Yu, Mathematical and Computational Methods in Photonics: Tutorial Notes, §1.4.1 (standard reference, not scraped)