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.

A separated Cauchy block has a geometric rank bound

Statement

Let $0 \leq a < b$ , $c \geq 0$ , and choose $m, n \geq 1$ points $x_{i} \in [0, a]$ and $y_{j} \in [b, b + c]$ . Put $q = a / b < 1$ and define the Cauchy block $K_{i j} = 1 / (y_{j} - x_{i})$ . For any integer $r \geq 1$ , the matrix $\tilde{K}$ with entries ${\tilde{K}}_{i j} = \sum_{ℓ = 0}^{r - 1} x_{i}^{ℓ} y_{j}^{- (ℓ + 1)}$ has rank at most $r$ and satisfies $∣ K_{i j} - {\tilde{K}}_{i j} ∣ \leq q^{r} / (b - a)$ and $∥ K - \tilde{K} ∥_{F} \leq \sqrt{m n} q^{r} / (b - a)$ . If $b - a \geq η \max (a, c)$ and the H-matrix rank cap satisfies $k \geq r$ , the sampled clusters are admissible and $\tilde{K}$ is a permitted rank-at-most- $k$ far-block representation.

Facts & Assumptions

Given: The real intervals, their sample points, and the integer truncation order $r$ .

[F1]

Finite cluster trees and geometric admissibility: admissibility requires positive distance and $dist (τ, σ) \geq η \max (diam (τ), diam (σ))$ .

[F2]

Finite tensor arrays and the Frobenius inner product: the matrix Frobenius norm is the square root of the sum of squared entry moduli, and the rank is the dimension of the column image.

[F3]

H-matrix block representation: an admissible H-matrix block is stored as $U V^{*}$ with rank at most the declared cap.

Proof

1.1givenalgebra

For $z = x / y$ one has $(1 - z) \sum_{ℓ = 0}^{r - 1} z^{ℓ} = 1 - z^{r}$ . Since $y - x > 0$ , division by $y (1 - x / y)$ gives the exact identity $\frac{1}{y - x} = \sum_{ℓ = 0}^{r - 1} \frac{x^{ℓ}}{y^{ℓ + 1}} + \frac{x^{r}}{y^{r} (y - x)}$ .

2.1F2step 1.1algebra

Because $0 \leq x_{i} / y_{j} \leq a / b = q$ and $y_{j} - x_{i} \geq b - a$ , step 1.1 gives $∣ K_{i j} - {\tilde{K}}_{i j} ∣ = x_{i}^{r} / (y_{j}^{r} (y_{j} - x_{i})) \leq q^{r} / (b - a)$ . Each summand of $\tilde{K}$ is the outer product of $(x_{i}^{ℓ})_{i = 1}^{m}$ and $(y_{j}^{- (ℓ + 1)})_{j = 1}^{n}$ , so its column image lies in the span of at most $r$ vectors and its rank is at most $r$ .

3.1F1F2F3step 2.1algebra∎

Summing the squared entrywise bound from step 2.1 over the $m n$ entries and using [F2] gives $∥ K - \tilde{K} ∥_{F} \leq \sqrt{m n} q^{r} / (b - a)$ . The sample clusters have distance at least $b - a$ and diameters at most $a$ and $c$ ; since $b - a > 0$ , the additional inequality in the Statement implies admissibility by [F1]. The rank bound in step 2.1 and $k \geq r$ then meet the far-block representation in [F3].

Depends on

Used by

A rank-one approximation of a separated Cauchy block Example

Dependency tree · two levels

4 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.2–1.3 (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.2.2.1 (standard reference, not scraped)