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

Inverse positivity of discounted finite-state policy matrices

Statement

For every policy $π$ in Finite-state discounted generator Bellman system, the matrix $A^{π} = c I - Q^{π}$ is nonsingular, $(A^{π})^{- 1}$ is entrywise nonnegative, and each diagonal entry of $(A^{π})^{- 1}$ is strictly positive.

Facts & Assumptions

Given: A finite state set, $c > 0$ , and policy generator coefficients with $q_{i j} \geq 0$ for $i \neq j$ and $\sum_{j} q_{i j} = 0$ .

[F1]

For the policy generator, $q_{i j} \geq 0$ off the diagonal, $\sum_{j} q_{i j} = 0$ , and $A = c I - Q$ (Finite-state discounted generator Bellman system).

[F2]

A real square matrix with trivial kernel is invertible (Invertible matrix theorem: invertibility, full pivot rank, RREF $I$ , trivial nullspace and unique solvability are equivalent).

[F3]

Every nonempty finite set of real numbers attains its maximum and minimum (Every nonempty finite set of reals has a maximum and a minimum).

Proof

1.1F1F2F3choosealgebra

Nonsingularity. Suppose $A z = 0$ for a nonzero real vector $z$ . The finite set ${∣ z_{j} ∣ : 1 \leq j \leq n}$ has a maximum by [F3]; choose an index $i$ attaining it, so $∣ z_{i} ∣ = \max_{j} ∣ z_{j} ∣ > 0$ . By the zero row sum, $(A z)_{i} = c z_{i} + \sum_{j \neq i} q_{i j} (z_{i} - z_{j})$ . If $z_{i} > 0$ , every term in the sum is nonnegative and $c z_{i} > 0$ , contradicting $(A z)_{i} = 0$ . If $z_{i} < 0$ , every sum term is nonpositive and $c z_{i} < 0$ , again a contradiction. Thus the kernel is zero, and [F2] makes the square matrix nonsingular.

2.1F1F3step 1.1choosealgebra

Inverse positivity. Let $y \geq 0$ and let $z = A^{- 1} y$ , which exists by step 1.1. If $z_{i} < 0$ at an index where $z$ is minimal, then $(A z)_{i} = c z_{i} + \sum_{j \neq i} q_{i j} (z_{i} - z_{j}) < 0$ , contradicting $y_{i} \geq 0$ . The finite set of coordinates of $z$ attains its minimum by [F3], so this argument proves $A^{- 1} y = z \geq 0$ for every $y \geq 0$ . Applying it to each standard basis vector shows that every entry of $A^{- 1}$ is nonnegative.

3.1F1step 2.1algebra∎

Positive diagonal. Fix $i$ and set $z = A^{- 1} e_{i} \geq 0$ by step 2.1. If $z_{i} = 0$ , then $(A z)_{i} = \sum_{j \neq i} q_{i j} (0 - z_{j}) \leq 0$ , while $(A z)_{i} = (e_{i})_{i} = 1$ . Hence $z_{i} = (A^{- 1})_{i i} > 0$ . This proves the claim.

Depends on

Used by

Dependency tree · two levels

18 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

Wang He, Reinforcement Learning: A Mathematical Introduction, Chapter 10, Policy Improvement and Policy Iteration (standard reference, not scraped)