LemmaStatement: AI-adaptedProof: 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.

A complex infinity-norm defect bounds the inverse norm

Statement

Let $E \in C^{n \times n}$ , $n \geq 1$ , and $0 \leq q < 1$ satisfy $∥ E ∥_{\infty, C} \leq q$ . Then $I - E$ is invertible and

∥ (I - E)^{- 1} ∥_{\infty, C} \leq \frac{1}{1 - q} .

Facts & Assumptions

Given: $E, q, n$ as in the statement.

[F1]

The complex infinity matrix norm is submultiplicative (The complex infinity matrix norm is compatible and submultiplicative).

[F2]

Its vector norm is the maximum coordinate modulus and its matrix norm is the maximum absolute row sum; in particular $∥ I ∥_{\infty, C} = 1$ and $∣ Y_{i j} ∣ \leq ∥ Y ∥_{\infty, C} \leq n \max_{i, j} ∣ Y_{i j} ∣$ (The complex induced infinity matrix norm).

[F3]

An injective endomorphism of a finite-dimensional vector space is invertible (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

Proof

1.1givenF1F3algebra

If $(I - E) x = 0$ , then $x = E x$ . The vector compatibility bound in [F1] gives $∥ x ∥_{\infty} \leq q ∥ x ∥_{\infty}$ , so $x = 0$ because $q < 1$ . Thus $I - E$ is injective, and [F3] makes it invertible; put $T = (I - E)^{- 1}$ .

2.1givenF1F2step 1.1algebra∎

Define $S_{N} = \sum_{k = 0}^{N} E^{k}$ . By induction and [F1], $∥ E^{k} ∥_{\infty, C} \leq q^{k}$ . The row-sum definition [F2] gives $∥ I ∥_{\infty, C} = 1$ and the triangle inequality, so $∥ S_{N} ∥_{\infty, C} \leq (1 - q^{N + 1}) / (1 - q)$ . The identity $(I - E) S_{N} = I - E^{N + 1}$ , multiplied on the left by $T$ from step 1.1, gives $S_{N} = T - T E^{N + 1}$ and hence $T = S_{N} + T E^{N + 1}$ . By [F2] and submultiplicativity [F1], $(1 - q^{N + 1}) ∥ T ∥_{\infty, C} \leq ∥ S_{N} ∥_{\infty, C} \leq (1 - q^{N + 1}) / (1 - q)$ . Since $q^{N + 1} < 1$ , division proves the asserted bound.

Depends on

Used by

Dependency tree · two levels

9 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

Siegfried M. Rump, Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19 (2010), §§4.2 and 10.5 (standard reference, not scraped)
Nicholas J. Higham, Numerical Linear Algebra and Matrix Analysis, MIMS EPrint 2015.103, §1 (standard reference, not scraped)