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.
One-level point-patch Schwarz loses uniformity on 1D Poisson
Example
For the uniform -interval P1 discretization of the Dirichlet Poisson problem on , one-level exact point-patch additive Schwarz has The patches are the supports of the interior nodal hats; they overlap with their neighbors and have bounded multiplicity. Nevertheless the condition number diverges with the number of local spaces.
Facts & Assumptions
Given: An integer , , the fine-grid P1 basis with , and the explicitly defined Dirichlet matrix , whose diagonal entries are and whose first off-diagonal entries are .
Finite-dimensional Schwarz subspace-correction data: for injections and SPD local matrices , the exact one-level additive preconditioner is .
Verification
Direct expansion gives with . It is positive for every nonzero vector because vanishing of all successive differences and forces every . For the point-patch injection , the local matrix is . Thus [F1] gives . Each corresponding nodal hat is supported on two adjacent mesh intervals, so neighboring local supports overlap and at most three closed supports meet at a point.
For , set for . The endpoints vanish. With , the identity gives These eigenvalues are distinct because cosine is strictly decreasing on . Since is symmetric, eigenvectors for distinct eigenvalues are orthogonal: for , . The vectors are nonzero, so the orthogonal vectors form a basis of . Multiplication by gives eigenvalues for .
The smallest and largest values occur at and , respectively. Therefore As the numerator tends to and the positive denominator tends to , so the condition numbers diverge.
Depends on
Used by
Nothing in the library uses this result yet.
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
- Jinchao Xu, Iterative Methods by Space Decomposition and Subspace Correction, SIAM Review 34(4) (1992) (standard reference, not scraped)
- Peter Bastian, Lecture Notes on Parallel Solution of Large Sparse Linear Systems, University of Heidelberg (2015) (standard reference, not scraped)