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.

Compressed block LU factors have a residual and inverse certificate

Statement

Let $A \in F^{n \times n}$ be invertible over $F \in {R, C}$ , $n \geq 1$ , and let $A = L U$ be an exact block lower-upper factorization. Suppose Compress exact block LU factors with local tolerances returns $\hat{L}, \hat{U}$ and exact local discarded-tail errors $e_{b}^{L}, e_{c}^{U}$ . All operations and norms in this theorem are exact. Put $ϵ_{L} = (\sum_{b} (e_{b}^{L})^{2})^{1 / 2}$ , $ϵ_{U} = (\sum_{c} (e_{c}^{U})^{2})^{1 / 2}$ , $\hat{A} = \hat{L} \hat{U}$ , and $η = ϵ_{L} ∥ U ∥_{F} + ∥ \hat{L} ∥_{F} ϵ_{U}$ . Then

$∥ A - \hat{A} ∥_{F} \leq η and ∥ A - \hat{A} ∥_{2} \leq η .$

If $q = ∥ A^{- 1} ∥_{2} η < 1$ , then $\hat{A}$ is invertible and

$∥ {\hat{A}}^{- 1} - A^{- 1} ∥_{2} \leq \frac{∥ A^{- 1} ∥_{2}^{2} η}{1 - q} .$

Facts & Assumptions

Given: The exact factorization $A = L U$ , a successful blockwise compression of $L, U$ , and the finite-dimensional real or complex matrix norms.

[F1]

Compress exact block LU factors with local tolerances: near and diagonal blocks are copied exactly; each admissible factor block is replaced by the factors returned by core-SVD recompression with its local error certificate.

[F2]

Core-SVD recompression is best at the declared Frobenius tolerance: each returned recompression has Frobenius residual exactly its reported discarded singular-value tail.

[F3]

Blockwise Frobenius errors propagate by disjoint block sums: on a disjoint block partition, local Frobenius residual bounds combine by the root sum of their squares.

[F4]

Finite tensor arrays and the Frobenius inner product: the Frobenius norm is the Euclidean norm of the finite entry list and $M^{*}$ is conjugate transpose.

[F5]

Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ in every real or complex inner-product space.

[F6]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: $∥ T ∥_{2}$ is the maximum of $∥ T x ∥_{2}$ over unit vectors.

[F7]

The operator norm is 0 on the zero domain and otherwise equals the largest singular value, attained at a right-singular vector: $∥ T ∥_{2}$ is the largest singular value of a finite-dimensional operator.

[F8]

Best rank-k matrix approximation in Frobenius norm: the Frobenius norm squared is the sum of squared singular values, by taking rank cap zero in the stated truncation formula.

[F9]

Rank-nullity: $\dim_{F} V = nullity T + rank T$ : for a linear map with finite-dimensional domain, dimension equals nullity plus rank.

[F10]

If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ : a subspace of an $n$ -dimensional space with dimension $n$ is the whole space.

[F11]

A square matrix is invertible exactly when its multiplication map is a linear isomorphism; matrices preserve inverses of linear isomorphisms: a square matrix is invertible exactly when its multiplication map is a linear isomorphism.

Proof

1.1F1F2F3

The factor compression in [F1] copies every near and diagonal block and gives local discarded-tail errors on the disjoint admissible blocks. By [F2] these are the actual local Frobenius residuals, so [F3] gives $∥ L - \hat{L} ∥_{F} \leq ϵ_{L}$ and $∥ U - \hat{U} ∥_{F} \leq ϵ_{U}$ .

2.1F4F5step 1.1algebra

Write $A - \hat{A} = L U - \hat{L} \hat{U} = (L - \hat{L}) U + \hat{L} (U - \hat{U})$ . For conformable $X, Y$ , entrywise Cauchy–Schwarz [F5] gives $∣ (X Y)_{i j} ∣^{2} \leq (\sum_{ℓ} ∣ X_{i ℓ} ∣^{2}) (\sum_{ℓ} ∣ Y_{ℓ j} ∣^{2})$ ; summing over $i, j$ gives $∥ X Y ∥_{F}^{2} \leq ∥ X ∥_{F}^{2} ∥ Y ∥_{F}^{2}$ . Also $∥ X + Y ∥_{F}^{2} = ∥ X ∥_{F}^{2} + ∥ Y ∥_{F}^{2} + 2 Re ⟨ X, Y ⟩_{F} \leq (∥ X ∥_{F} + ∥ Y ∥_{F})^{2}$ by [F4,F5], so the Frobenius triangle inequality follows. Together with step 1.1 this yields $∥ A - \hat{A} ∥_{F} \leq ϵ_{L} ∥ U ∥_{F} + ∥ \hat{L} ∥_{F} ϵ_{U} = η$ .

3.1F7F8step 2.1algebra

For any matrix $R$ , [F7] gives $∥ R ∥_{2} = σ_{1} (R)$ , while [F8] at rank cap zero gives $∥ R ∥_{F} = (\sum_{j} σ_{j} (R)^{2})^{1 / 2}$ . Hence $∥ R ∥_{2} \leq ∥ R ∥_{F}$ . Applying this to $R = A - \hat{A}$ and using step 2.1 proves $∥ A - \hat{A} ∥_{2} \leq η$ .

4.1F6F9F10F11step 3.1algebra

Let $E = \hat{A} - A$ and $q = ∥ A^{- 1} ∥_{2} η < 1$ . For every $x$ , the operator-norm definition [F6] gives $∥ A^{- 1} E x ∥_{2} \leq ∥ A^{- 1} ∥_{2} ∥ E ∥_{2} ∥ x ∥_{2} \leq q ∥ x ∥_{2}$ by step 3.1. If $\hat{A} x = 0$ , then $x = - A^{- 1} E x$ , so $∥ x ∥_{2} \leq q ∥ x ∥_{2}$ and therefore $x = 0$ . Thus $\hat{A}$ is injective. By [F9], its image has dimension $n$ ; [F10] makes that image all of $F^{n}$ , so its multiplication map is an isomorphism and [F11] gives invertibility.

5.1F5F6step 4.1algebra∎

Set $F = A^{- 1} E$ . The definition [F6] gives $∥ F ∥_{2} \leq q$ by the same estimate as in step 4.1. Since $\hat{A} = A (I + F)$ is invertible, so is $I + F$ . For $z = (I + F)^{- 1} y$ , the vector triangle inequality from [F5] gives $∥ z ∥_{2} \leq ∥ y ∥_{2} + ∥ F z ∥_{2} \leq ∥ y ∥_{2} + q ∥ z ∥_{2}$ , hence $∥ (I + F)^{- 1} ∥_{2} \leq (1 - q)^{- 1}$ . Since ${\hat{A}}^{- 1} = (I + F)^{- 1} A^{- 1}$ and $(I + F)^{- 1} - I = - (I + F)^{- 1} F$ , operator-norm submultiplicativity follows from [F6] and gives $∥ {\hat{A}}^{- 1} - A^{- 1} ∥_{2} \leq q ∥ A^{- 1} ∥_{2} / (1 - q) = ∥ A^{- 1} ∥_{2}^{2} η / (1 - q)$ .

Remarks

The certificate is conditional on exact factor compression and exact norm values. No finite-precision residual enclosure or method for constructing the initial exact $L, U$ is asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 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

Steffen Börm, Lars Grasedyck, and Wolfgang Hackbusch, Hierarchical Matrices, MiS Lecture Note 21 (2003; revised June 2006), §§6.2, 7.2 (standard reference, not scraped)
Ralf Hiptmair, AdvNumCSE Lecture Document, Chapter 2, “Local Low-Rank Compression of Non-Local Operators” (ETH Zürich, AT’23), §2.4.5 (standard reference, not scraped)