LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Strict column dominance gives an entrywise nonnegative inverse

Statement

Let $M = (m_{i j}) \in R^{m \times m}$ for a finite $m \geq 1$ . Suppose $m_{j j} > 0$ , $m_{i j} \leq 0$ for $i \neq j$ , and

$m_{j j} > \sum_{i \neq j} ∣ m_{i j} ∣ (j = 1, \dots, m) .$

Then $M$ is invertible and every entry of $M^{- 1}$ is nonnegative. If $b \in R^{m}$ has nonnegative coordinates, then $M^{- 1} b \geq 0$ ; if every coordinate of $b$ is positive, then every coordinate of $M^{- 1} b$ is positive.

Facts & Assumptions

Given: A finite real matrix satisfying the displayed positive-diagonal, nonpositive-off-diagonal, and strict column-dominance hypotheses.

[F1]

The hypotheses give $c_{i j} : = - m_{i j} / m_{j j} \geq 0$ for $i \neq j$ and $c_{j j} = 0$ .

Proof

1.1givenF1algebraconstruct

Let $D = diag (m_{11}, \dots, m_{m m})$ and $C = I - M D^{- 1}$ . Then $D$ is invertible, $C \geq 0$ , and for each column $j$ , $r_{j} : = \sum_{i} C_{i j} = \sum_{i \neq j} ∣ m_{i j} ∣ / m_{j j} < 1$ . Since there are finitely many columns, $r : = \max_{j} r_{j} < 1$ .

2.1step 1.1algebrainduction

For every $k \geq 0$ , $C^{k} \geq 0$ and $\sum_{i} (C^{k})_{i j} \leq r^{k}$ for every column $j$ : it holds at $k = 0$ , and multiplying by $C$ gives $\sum_{i} (C^{k + 1})_{i j} = \sum_{ℓ} (\sum_{i} C_{i ℓ}) (C^{k})_{ℓ j} \leq r \sum_{ℓ} (C^{k})_{ℓ j}$ . Thus each entry series in $S : = \sum_{k = 0}^{\infty} C^{k}$ converges and is nonnegative.

3.1step 1.1step 2.1algebra

The finite geometric identity $(I - C) \sum_{k = 0}^{N} C^{k} = \sum_{k = 0}^{N} C^{k} (I - C) = I - C^{N + 1}$ holds by cancellation of adjacent powers. Step 2.1 gives $C^{N + 1} \to 0$ entrywise, so $(I - C) S = S (I - C) = I$ . Since $M = (I - C) D$ , $M^{- 1} = D^{- 1} S \geq 0$ , proving invertibility and inverse nonnegativity.

4.1step 3.1algebra∎

If $b \geq 0$ , then $M^{- 1} b \geq 0$ by step 3.1. If $b > 0$ , then $S \geq I$ entrywise, so $D^{- 1} S b \geq D^{- 1} b > 0$ coordinatewise. This proves both vector conclusions.

Used by

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Stefan Kopecz, Ein gekoppeltes Finite-Elemente/Discontinuous-Galerkin-Verfahren zur Simulation von Strömungs-Transport-Problemen, §6.1.2 (standard reference, not scraped)
Stefan Kopecz and Andreas Meister, On order conditions for modified Patankar-Runge-Kutta schemes, Lemma 2.7 (standard reference, not scraped)