Reindexing the doubly-weighted sum

Read-back 2 — sum_interchange

Data and binders. Again two implicitly quantified types $I$ and $J$ in arbitrary universes, each carrying a finiteness structure, and three explicit pieces of data: a real matrix $A : I \to J \to \mathbb{R}$ with rows indexed by $I$ and columns by $J$, a vector $x : I \to \mathbb{R}$ indexed by rows, and a vector $y : J \to \mathbb{R}$ indexed by columns.

Hypotheses. There are none. Beyond the two finiteness instances on the index types, the statement carries no assumption whatsoever: no nonnegativity, no feasibility, no bounds, no nonemptiness, no relation between $A$, $x$ and $y$. Consequently the claim is asserted for arbitrary real data, including negative entries of $A$, negative $x_i$, negative $y_j$, mixed signs, and all-zero data; there is no hypothesis that could be vacuous or unsatisfiable, and no hypothesis that could be unused.

Conclusion. The asserted equality is

The two sides differ in which index of $A$ is summed inside and which outside:

• Left side: inner sum over $j$ (the second index of $A$), i.e. each row of $A$ is contracted against $y$, and the resulting row value is multiplied by $x_i$; the outer sum runs over $i$ (the first index).
• Right side: inner sum over $i$ (the first index of $A$), i.e. each column of $A$ is contracted against $x$, and the resulting column value is multiplied by $y_j$; the outer sum runs over $j$ (the second index).

In both cases the scalar factor from the outer index is written to the right of the inner sum. The relation asserted is exact equality of two real numbers, not an inequality and not an approximation.

Degenerate cases. If $I$ is empty, the left side is the empty sum $0$; on the right, each inner sum over $i$ is $0$, so the right side is $\sum_{j} 0 \cdot y_j = 0$, and the claim is $0 = 0$. Symmetrically, if $J$ is empty, the left side is $\sum_i 0 \cdot x_i = 0$ and the right side is the empty sum $0$. If both are empty, the claim is $0 = 0$. Since all sums are over finite index types, no question of convergence arises and every sum is a well-defined real number.

Not asserted. The statement asserts no inequality in either direction, no sign information about the common value, and no nonnegativity of any of $A$, $x$, $y$ or the sums. It does not mention $c$, $b$, the primal objective, the dual objective, feasibility, or optimality. It does not claim that either side equals any third expression (for instance a doubly-indexed sum over $I \times J$), only that the two displayed nestings agree. It makes no claim about the matrix having full rank, being square, or the index types having equal cardinality. The declaration's body is a placeholder, so no proof is supplied by the code.