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.

BDDC and FETI-DP have matching nontrivial spectra

Statement

For BDDC and FETI-DP built from the same positive definite partially assembled Schur operator, primal constraints, and scaled averaging, all eigenvalues of the two preconditioned operators other than $1$ agree with multiplicity. With the multiplier space fixed as $Λ = range B$ , neither operator has a zero eigenvalue; retaining all redundant row coordinates instead would add only multiplier null modes that are removed by this convention. The multiplicity of $1$ is not asserted to agree.

Facts & Assumptions

Given: A positive definite partial Schur operator, a conforming trace subspace, a primal projection, and a jump map with multiplier space $range B$ .

[F1]

Coefficient-scaled averaging and BDDC: $E_{0} R = I_{\hat{W}}$ and $R E_{0}$ is the BDDC projection.

[F2]

FETI-DP dual system and preconditioner: $B B_{D}^{T} = I_{Λ}$ and $B_{D}^{T} B + R E_{0} = I_{\tilde{W}}$ .

[F3]

Complementary primal and dual projections share nonunit spectrum: if $L_{i} T_{i} = I$ and $T_{1} L_{1} + T_{2} L_{2} = I$ , the associated abstract products have matching nonunit eigenvalues with multiplicity.

Proof

1.1givenF1F2F3algebra

Take $V = \tilde{W}$ , $U_{1} = \hat{W}$ , $U_{2} = Λ$ , $A = \tilde{S}$ , $L_{1} = E_{0}$ , $T_{1} = R$ , $L_{2} = B$ , and $T_{2} = B_{D}^{T}$ . By [F1] and [F2], $L_{i} T_{i} = I$ and $T_{1} L_{1} + T_{2} L_{2} = I$ . The first abstract product in [F3] is $(E_{0} {\tilde{S}}^{- 1} E_{0}^{T}) (R^{T} \tilde{S} R)$ , exactly the BDDC preconditioned operator by [F1]; the second is $(B_{D} \tilde{S} B_{D}^{T}) (B {\tilde{S}}^{- 1} B^{T})$ , exactly the FETI-DP product by [F2].

2.1givenF1F2F3step 1.1algebra∎

Apply [F3] to conclude equal eigenvalues and multiplicities for every eigenvalue other than $1$ . The identities $E_{0} R = I$ and $B B_{D}^{T} = I$ make $R$ and $B_{D}^{T}$ injective and $E_{0}$ and $B$ surjective onto their ranges; since $\tilde{S}$ is positive definite, the four Gram operators in the two products are positive definite on their respective spaces. Thus both preconditioned products have positive eigenvalues. Taking $Λ = range B$ removes redundant multiplier null modes. No step determines the multiplicity of eigenvalue $1$ .

Depends on

Used by

Dependency tree · two levels

6 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

Jan Mandel and Bedřich Sousedík, BDDC and FETI-DP under Minimalist Assumptions, §4 (standard reference, not scraped)
Olof B. Widlund, Introduction to the Design and Theory of Domain Decomposition Algorithms, DD20 Tutorial, pp. 90–93 (standard reference, not scraped)