Read-back: separable_apply_local_reward

What the statement asserts

Fix a natural number $N$ (implicit) and a family of types $S_0,\dots,S_{N-1}$ indexed by $i \in \mathrm{Fin}\,N = \{0,\dots,N-1\}$ (implicit), where each $S_i$ is assumed finite and to have decidable equality. Write

for the joint space, whose elements are the dependent tuples $p$ assigning to each index $j$ an element $p_j \in S_j$; $\mathcal{J}$ is again a finite type. Fix a natural number $K$ (implicit), a vector of real coefficients $x : \mathrm{Fin}\,K \to \mathbb{R}$, and a doubly-indexed family of real square matrices $P^{(k)}_j \in \mathbb{R}^{S_j \times S_j}$ for $k \in \mathrm{Fin}\,K$, $j \in \mathrm{Fin}\,N$. The hypotheses are:

• (hPj) for every $k \in \mathrm{Fin}\,K$ and every index $j \in \mathrm{Fin}\,N$, the matrix $P^{(k)}_j$ is row-stochastic in the sense of this bundle's IsTransitionMatrix, i.e. all its entries are $\ge 0$ and each of its rows sums to exactly $1$: $\sum_{t \in S_j} P^{(k)}_j(s,t) = 1$ for all $s \in S_j$;
• (hx) $\sum_{k \in \mathrm{Fin}\,K} x_k = 1$ — an affine constraint only; no sign condition is imposed on the individual $x_k$.

Finally fix an index $i \in \mathrm{Fin}\,N$, an arbitrary real-valued function $r : S_i \to \mathbb{R}$ (no nonnegativity, boundedness, or normalisation assumed), and an arbitrary joint point $p \in \mathcal{J}$.

The bundle's $N$-fold tensor product tensorProdN of a family $(P_j)_j$ is the matrix on $\mathcal{J}$ whose entry at $(p,q)$ is $\prod_{j} P_j(p_j, q_j)$. The claimed identity is then, entrywise in the real matrix $\sum_k x_k \cdot \big(\bigotimes_j P^{(k)}_j\big)$ evaluated at the row $p$:

Here the outer sum on the left ranges over the whole finite joint space, the scalar action $x_k \bullet(-)$ is ordinary real scaling of a matrix, and the sum of matrices is taken entrywise before evaluation at $(p,q)$. The equality is an exact equality of real numbers — not an inequality, not an approximation.

Quantification, satisfiability, and degenerate cases

• Every variable occurring in the conclusion is bound. $N$, $S$, $K$, $x$, $P^{(k)}_j$, $i$, $r$, $p$ are all binders of the theorem (some implicit, some explicit), universally quantified; the typeclass assumptions (finiteness and decidable equality of each $S_j$) are likewise binders. Nothing in the conclusion is free, and the identity is asserted for the single given $p$ and given $i$, universally over all choices of them.
• The hypotheses are jointly satisfiable and do not collapse the statement. For instance $K = 1$, $x_0 = 1$, and any row-stochastic $P^{(0)}_j$ (e.g. identity matrices) satisfies both hPj and hx, with any nonempty finite $S_j$'s. So the theorem is not vacuous.
• (hx) forces $K \ge 1$. If $K = 0$ the sum $\sum_k x_k$ is the empty sum $0 \ne 1$, so hx cannot hold; the $K = 0$ instance is vacuous.
• $N = 0$ makes the statement vacuous for a different reason: $\mathrm{Fin}\,0$ is empty, so no index $i$ can be supplied and no instance of the theorem exists.
• Supplying $p \in \mathcal{J}$ forces every $S_j$ to be nonempty (a dependent tuple picks out an element of each $S_j$). Hence $\mathcal{J}$ is nonempty in every instance, and the left-hand sum is over a nonempty finite set. There is therefore no "empty joint space" instance in which the left side degenerates to $0$ while the right side does not.
• The coefficients $x_k$ may be negative, so $\sum_k x_k \bigotimes_j P^{(k)}_j$ need not itself be a nonnegative matrix; only the affine condition $\sum_k x_k = 1$ is imposed. The statement is about this possibly-signed affine combination, not about a convex mixture.
• Asymmetry between the two sides. Hypothesis hPj is asserted for all $k$ and all indices $j$, including $j \ne i$; the right-hand side mentions only agent $i$'s matrices $P^{(k)}_i$ and the reward $r$ on $S_i$, while the left-hand side involves all the $P^{(k)}_j$.
• Small $K$, $N$, or singleton $S_j$ are all included: with $N = 1$ the products $\prod_j$ have a single factor and both sides read as the same sum; with $S_j$ a singleton for $j \ne i$ the left-hand sum collapses to a sum over $S_i$.