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.

Eigenvalue bounds from a left-inverse preconditioner

Statement

Let $A : V \to V^{'}$ be symmetric positive definite on a finite-dimensional real vector space, and let $L : V \to U$ , $T : U \to V$ satisfy $L T = I_{U}$ . Every eigenvalue of

$G = (L A^{- 1} L^{T}) (T^{T} A T)$

lies in $[1, ∥ T L ∥_{A}^{2}]$ , where $∥ Q ∥_{A} : = \sup_{v \neq 0} \sqrt{⟨ A Q v, Q v ⟩ / ⟨ A v, v ⟩}$ . When $V = {0}$ , set $∥ Q ∥_{A} = 0$ for its unique endomorphism. In that case $L T = I_{U}$ forces $U = {0}$ , the spectrum of $G$ is empty, and the eigenvalue assertion is vacuous.

Facts & Assumptions

Given: Finite-dimensional real spaces $V, U$ , a symmetric positive definite operator $A : V \to V^{'}$ , linear maps $L : V \to U$ and $T : U \to V$ , and $L T = I_{U}$ .

[A1]

The energy form $⟨ A v, v ⟩$ is positive for every nonzero $v \in V$ , and $L T$ is the identity on $U$ .

Proof

1.1givenA1algebra

If $V = {0}$ , the identity $L T = I_{U}$ forces $U = {0}$ and $G$ has no eigenvalues, so the assertion holds with the stated zero-space norm convention. Assume henceforth $V \neq {0}$ . Put $D = T^{T} A T$ , which is SPD because $T$ is injective (if $T u = 0$ , then $u = L T u = 0$ ), and $C = L A^{- 1} L^{T}$ , which is SPD because $L$ is onto (it has right inverse $T$ ). Hence $G = C D$ is similar to the symmetric positive definite matrix $D^{1 / 2} C D^{1 / 2}$ and has positive real eigenvalues. For an eigenvector $u \neq 0$ with eigenvalue $λ$ , let $w = A^{- 1} L^{T} D u$ , so $L w = G u = λ u$ and $∥ w ∥_{A}^{2} = ⟨ D u, G u ⟩ = λ ⟨ D u, u ⟩$ .

2.1givenA1step 1.1algebra

By [A1], $⟨ D u, u ⟩ = ⟨ D u, L T u ⟩ = ⟨ A w, T u ⟩$ . Cauchy–Schwarz in the $A$ inner product gives $⟨ D u, u ⟩^{2} \leq ∥ w ∥_{A}^{2} ∥ T u ∥_{A}^{2} = λ ⟨ D u, u ⟩^{2}$ . Dividing by the positive square gives $λ \geq 1$ .

3.1givenA1step 1.1algebra∎

Also $∥ G u ∥_{D}^{2} = ∥ T L w ∥_{A}^{2} \leq ∥ T L ∥_{A}^{2} ∥ w ∥_{A}^{2}$ . For the eigenvector, the left side is $λ^{2} ⟨ D u, u ⟩$ and step 1.1 makes the right side $∥ T L ∥_{A}^{2} λ ⟨ D u, u ⟩$ . Divide by the positive factor to obtain $λ \leq ∥ T L ∥_{A}^{2}$ .

Used by

The two-dimensional BDDC and FETI-DP polylogarithmic bound Theorem

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

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