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.
Coefficient-scaled averaging and BDDC
Definition
Use the spaces and partial Schur operator of Primal interface spaces and jump convention and Discrete harmonic extension and interface Schur complement. Let average every remaining interface degree of freedom and preserve every already-shared primal value. It is a scaled average if the weights for all copies of each such degree of freedom sum to one. Put . Then and is a projection onto .
In the PE26 two-dimensional corner-constraint branch, each non-primal node is interior to one interface edge shared by exactly two subdomains . Set
At primal nodes the copies already agree, so the average is the common value. For any finite-dimensional positive definite partial Schur operator , the BDDC preconditioner is
for the assembled interface system with operator . Its constrained partial-energy interpretation is established in BDDC is the constrained partial-energy minimizer ↗.
Depends on
Used by
- FETI-DP dual system and preconditioner Definition
- A finite-dimensional BDDC/FETI-DP spectral match Example
- Two floating Poisson subdomains and primal anchoring Example
- Complementary primal and dual projections share nonunit spectrum Lemma
- Two-dimensional scaled averaging energy bound Lemma
- BDDC is the constrained partial-energy minimizer Proposition
- Conditioning and solver work are separate claims Remark
- BDDC and FETI-DP have matching nontrivial spectra Theorem
- The two-dimensional BDDC and FETI-DP polylogarithmic bound Theorem
Dependency tree · two levels
7 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
- Olof B. Widlund, Introduction to the Design and Theory of Domain Decomposition Algorithms, DD20 Tutorial, pp. 87–90 and 96–97 (standard reference, not scraped)
- Jan Mandel and Bedřich Sousedík, BDDC and FETI-DP under Minimalist Assumptions, §§3.1–3.2 (standard reference, not scraped)