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

FETI-DP is the exact dual Schur system

Statement

Let $f \in {\hat{W}}^{'}$ and set $\tilde{f} = E_{0}^{T} f$ . The constrained minimization problem

$\min_{w \in \tilde{W}, B w = 0} (\frac{1}{2} ⟨ \tilde{S} w, w ⟩ - ⟨ \tilde{f}, w ⟩)$

has the saddle equations $\tilde{S} w + B^{T} λ = \tilde{f}$ , $B w = 0$ . Eliminating $w$ gives the FETI-DP dual system

$B {\tilde{S}}^{- 1} B^{T} λ = B {\tilde{S}}^{- 1} E_{0}^{T} f .$

On $Λ = range B$ its matrix is positive definite, and the exact multiplier solution reconstructs the unique assembled interface solution $w \in \hat{W}$ .

Facts & Assumptions

Given: $\tilde{S}$ is positive definite on $\tilde{W}$ , $B : \tilde{W} \to Λ$ is onto with $\ker B = \hat{W}$ , and $E_{0}$ is the projection used by BDDC.

[F1]

FETI-DP dual system and preconditioner: $F = B {\tilde{S}}^{- 1} B^{T}$ and the multiplier space is $Λ = range B$ .

[F2]

Primal interface spaces and jump convention: $\ker B = \hat{W}$ and redundant multiplier rows are represented by their range.

[F3]

Primal constraints remove local floating kernels: all subdomain vertices primal and a nonempty global Dirichlet boundary suffice for positive definiteness of $\tilde{S}$ . Here positive definiteness is an explicit hypothesis, also for other primal choices.

Proof

1.1givenF1F2algebra

The Lagrangian is $L (w, λ) = \frac{1}{2} ⟨ \tilde{S} w, w ⟩ - ⟨ E_{0}^{T} f, w ⟩ + ⟨ λ, B w ⟩$ . Its derivative in arbitrary $z \in \tilde{W}$ is $⟨ \tilde{S} w + B^{T} λ - E_{0}^{T} f, z ⟩$ , and its multiplier derivative is $B w$ . Setting both derivatives to zero gives the displayed saddle equations.

2.1givenstep 1.1algebra

By the assumed positive definiteness of $\tilde{S}$ , the first equation has the unique solution $w = {\tilde{S}}^{- 1} (E_{0}^{T} f - B^{T} λ)$ . Substitution into $B w = 0$ gives the displayed dual system.

3.1F1F2F3step 2.1algebra∎

If $λ \in Λ$ and $B^{T} λ = 0$ , write $λ = B v$ using [F2]. Then $⟨ λ, λ ⟩ = ⟨ B v, λ ⟩ = ⟨ v, B^{T} λ ⟩ = 0$ , hence $λ = 0$ . Thus $B^{T}$ is injective on $Λ$ , and $⟨ F λ, λ ⟩ = ⟨ {\tilde{S}}^{- 1} B^{T} λ, B^{T} λ ⟩ > 0$ for every nonzero $λ$ . The exact solution satisfies $B w = 0$ , so by [F2] it lies in $\hat{W}$ and solves the assembled variational problem.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by FETI-DP dual system and preconditioner.

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

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