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.

The complex infinity matrix norm is compatible and submultiplicative

Statement

Use $∥ A ∥_{\infty, C}$ and $∥ x ∥_{\infty}$ from The complex induced infinity matrix norm. For compatible complex matrices and vectors with every row and column dimension positive, $∥ A x ∥_{\infty} \leq ∥ A ∥_{\infty, C} ∥ x ∥_{\infty}, ∥ A B ∥_{\infty, C} \leq ∥ A ∥_{\infty, C} ∥ B ∥_{\infty, C} .$

Facts & Assumptions

Given: Complex matrices $A, B$ and vector $x$ of compatible finite dimensions.

[F1]

Complex absolute value is $∣ u + i v ∣ = \sqrt{u^{2} + v^{2}}$ (The complex induced infinity matrix norm).

[F2]

For real $x_{1}, x_{2}, y_{1}, y_{2}$ , $(x_{1} y_{1} + x_{2} y_{2})^{2} \leq (x_{1}^{2} + x_{2}^{2}) (y_{1}^{2} + y_{2}^{2})$ , since the difference is $(x_{1} y_{2} - x_{2} y_{1})^{2} \geq 0$ .

Proof

1.1F1F2algebra

If $z = x_{1} + i x_{2}$ and $w = y_{1} + i y_{2}$ , then $∣ z w ∣^{2} = (x_{1}^{2} + x_{2}^{2}) (y_{1}^{2} + y_{2}^{2})$ by expansion. Also $∣ z + w ∣^{2} = ∣ z ∣^{2} + ∣ w ∣^{2} + 2 (x_{1} y_{1} + x_{2} y_{2}) \leq (∣ z ∣ + ∣ w ∣)^{2}$ by [F2]. Nonnegativity gives $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ and $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ .

2.1givenF1step 1.1algebra

For each row $i$ , [F1] and step 1.1 give $∣ (A x)_{i} ∣ \leq \sum_{j} ∣ a_{i j} ∣ ∣ x_{j} ∣ \leq (\sum_{j} ∣ a_{i j} ∣) ∥ x ∥_{\infty}$ . Taking the maximum over $i$ proves compatibility.

3.1step 1.1algebra∎

For each row $i$ , $\sum_{j} ∣ (A B)_{i j} ∣ \leq \sum_{j} \sum_{k} ∣ a_{i k} ∣ ∣ b_{k j} ∣ = \sum_{k} ∣ a_{i k} ∣ \sum_{j} ∣ b_{k j} ∣ \leq (\sum_{k} ∣ a_{i k} ∣) ∥ B ∥_{\infty, C}$ . Taking the maximum over $i$ proves submultiplicativity.

Depends on

The complex induced infinity matrix norm

Used by

Dependency tree · two levels

2 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), §10.5 (standard reference, not scraped)
Nicholas J. Higham, Numerical Linear Algebra and Matrix Analysis, MIMS EPrint 2015.103, §5.1 (standard reference, not scraped)