Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Woodbury inverse for a diagonal-plus-low-rank update

Statement

Let D∈CN×N be invertible, let U,V∈CN×r, and set W=Ir+V∗D−1U, where ∗ denotes conjugate transpose. Then D+UV∗ is invertible if and only if W is invertible. When these matrices are invertible,

(D+UV∗)−1=D−1−D−1UW−1V∗D−1.

Facts & Assumptions

Given: Finite integers N,r≥1, matrices D∈CN×N and U,V∈CN×r, with D invertible, and W:=Ir+V∗D−1U.

[A1]

The inverse D−1 exists, so all displayed matrix products are defined.

[A2]

W is an r×r matrix; a square linear map in finite dimension is invertible once its kernel is zero.

Proof

1.1A1algebra

Assume W is invertible and define X:=D−1−D−1UW−1V∗D−1. Expansion gives (D+UV∗)X=I+U(V∗D−1−W−1V∗D−1−V∗D−1UW−1V∗D−1)=I, because (Ir+V∗D−1U)W−1V∗D−1=WW−1V∗D−1=V∗D−1.

2.1A1step 1.1algebra

Expanding in the other order gives X(D+UV∗)=I+D−1U(V∗−W−1V∗−W−1V∗D−1UV∗)=I, because W−1(Ir+V∗D−1U)V∗=W−1WV∗=V∗. Thus X is the two-sided inverse of D+UV∗, proving this direction and the formula.

3.1A1A2step 1.1algebra∎

Conversely assume D+UV∗ is invertible and let w∈Cr satisfy Ww=0. Set x=D−1Uw. Then (D+UV∗)x=U(Ir+V∗D−1U)w=UWw=0, so invertibility gives x=0. Hence Uw=Dx=0, and therefore Ww=w+V∗D−1Uw=w. Since Ww=0, we have w=0. Thus W has zero kernel; by [A2] it is invertible.

Used by

Dependency tree · 0 levels

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

Sources