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

Blockwise Frobenius errors propagate by disjoint block sums

Statement

For any finite matrix partition into disjoint blocks, if each local residual satisfies $∥ E_{b} ∥_{F} \leq δ_{b}$ , then the assembled residual satisfies $∥ E ∥_{F} \leq (\sum_{b} δ_{b}^{2})^{1 / 2}$ . In particular, let $A, B$ be conformable finite real or complex matrices, and let $\tilde{A}, \tilde{B}$ be approximations with $∥ A - \tilde{A} ∥_{F} \leq ϵ_{A}$ and $∥ B - \tilde{B} ∥_{F} \leq ϵ_{B}$ . If a successful block addition or block product from Tolerance-controlled H-matrix block addition or Tolerance-controlled H-matrix block product returns $\hat{S}$ or $\hat{C}$ , with disjoint output blocks $b$ and local Frobenius errors $e_{b} \leq δ_{b}$ , put $δ = (\sum_{b} δ_{b}^{2})^{1 / 2}$ . Then

$∥ A + B - \hat{S} ∥_{F} \leq ϵ_{A} + ϵ_{B} + δ,$

and

$∥ A B - \hat{C} ∥_{F} \leq ϵ_{A} ∥ B ∥_{F} + ∥ A ∥_{F} ϵ_{B} + ϵ_{A} ϵ_{B} + δ .$

Facts & Assumptions

Given: The target matrices, their H-matrix approximations, successful block-operation outputs, and local block-error budgets.

[F1]

Tolerance-controlled H-matrix block addition and Tolerance-controlled H-matrix block product: near blocks are computed exactly; on success, each far output block has a certified Frobenius error bound $e_{b}$ no larger than its allocated tolerance.

[F2]

Bottom-up factor-sum recompression has the reported rank and Frobenius error bound: for each successful factor-sum tree, the returned block approximation error is at most the sum of its nodewise core-SVD discarded-tail norms, which is bounded by the sum of its node tolerances.

[F3]

Block-cluster leaves partition the index-pair set: every recursively generated terminal block partition is pairwise disjoint and covers the output index-pair set.

[F4]

Finite tensor arrays and the Frobenius inner product: the Frobenius norm is the Euclidean norm of the finite matrix-entry list.

[F5]

Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs: the absolute inner product of two vectors is at most the product of their norms.

Proof

1.1F1F2F3F4algebra

Let $Δ_{b}$ be the actual residual in output block $b$ . For near blocks it is zero; for far blocks [F1] and [F2] give $∥ Δ_{b} ∥_{F} \leq e_{b} \leq δ_{b}$ . By [F3] their entry supports are disjoint, so [F4] gives $∥ Δ ∥_{F}^{2} = \sum_{b} ∥ Δ_{b} ∥_{F}^{2} \leq \sum_{b} δ_{b}^{2}$ . Hence $∥ Δ ∥_{F} \leq δ$ .

2.1F4F5step 1.1algebra

For addition, write $\hat{S} = \tilde{A} + \tilde{B} + Δ$ . Expanding the squared Frobenius norm as the finite entry inner product and applying [F5] gives the triangle inequality. Therefore $∥ A + B - \hat{S} ∥_{F} \leq ∥ A - \tilde{A} ∥_{F} + ∥ B - \tilde{B} ∥_{F} + ∥ Δ ∥_{F} \leq ϵ_{A} + ϵ_{B} + δ$ .

3.1F4F5step 1.1algebra∎

For multiplication, put $E_{A} = \tilde{A} - A$ and $E_{B} = \tilde{B} - B$ . Since $\hat{C} = \tilde{A} \tilde{B} + Δ$ , expansion gives $A B - \hat{C} = - (E_{A} B + A E_{B} + E_{A} E_{B} + Δ)$ . For any conformable $X, Y$ , entrywise Cauchy–Schwarz 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}$ . Thus $∥ E_{A} B ∥_{F} \leq ϵ_{A} ∥ B ∥_{F}$ , $∥ A E_{B} ∥_{F} \leq ∥ A ∥_{F} ϵ_{B}$ , and $∥ E_{A} E_{B} ∥_{F} \leq ϵ_{A} ϵ_{B}$ . The triangle inequality from [F4,F5] and step 1.1 give the stated product bound.

Depends on

Used by

Compressed block LU factors have a residual and inverse certificate Theorem

Dependency tree · two levels

20 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), §§1.6, 6.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.2–2.4.4 (standard reference, not scraped)