Summation of i from 1 to n of Summation of j from 1 to i

Theorem

$\ds \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^i a_{i j} = \sum_{j \mathop = 1}^n \sum_{i \mathop = j}^n a_{i j}$

Proof 1

$\ds \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^i$

can be expressed as:

$\ds \sum_{\map R i} \sum_{\map S {i, j} } a_{i j}$

where:

$\map R i$ is the propositional function $1 \le i \le n$

$\map S {i, j}$ is the propositional function $1 \le j \le i$

We wish to find a propositional function $\map {S'} j$ which is to be:

there exists an $i$ such that both $1 \le i \le n$ and $1 \le j \le i$

This is satisfied by the propositional function:

$\map {S'} j := 1 \le j \le n$

Next we wish to find a propositional function $\map {R'} {i, j}$ which is to be:

both $1 \le i \le n$ and $1 \le j \le i$

This is satisfied by the propositional function:

$\map {R'} {i, j} := j \le i \le n$

Hence the result, from Exchange of Order of Summation with Dependency on Both Indices.

$\blacksquare$

Proof 2

\(\ds \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^i a_{i j}\)

\(=\)

\(\ds \sum_{i, j \mathop \in \Z} a_{i j} \left[{1 \le i \le n}\right] \left[{1 \le j \le i}\right]\)

\(\ds \)

\(=\)

\(\ds \sum_{i, j \mathop \in \Z} a_{i j} \left[{1 \le j \le i \le n}\right]\)

\(\ds \)

\(=\)

\(\ds \sum_{i, j \mathop \in \Z} a_{i j} \left[{1 \le j \le n}\right] \left[{j \le i \le n}\right]\)

\(\ds \)

\(=\)

\(\ds \sum_{j \mathop = 1}^n \sum_{i \mathop = j}^n a_{i j}\)

$\blacksquare$

Example

Let $n = 3$.

\(\ds \sum_{i \mathop = 1}^3 \sum_{j \mathop = 1}^i a_{i j}\)

\(=\)

\(\ds \sum_{j \mathop = 1}^1 a_{1 j} + \sum_{j \mathop = 1}^2 a_{2 j} + \sum_{j \mathop = 1}^3 a_{3 j}\)

\(\ds \)

\(=\)

\(\ds \left({a_{1 1} }\right) + \left({a_{2 1} + a_{2 2} }\right) + \left({a_{3 1} + a_{3 2} + a_{3 3} }\right)\)

\(\ds \sum_{j \mathop = 1}^3 \sum_{i \mathop = j}^3 a_{i j}\)

\(=\)

\(\ds \sum_{i \mathop = 1}^3 a_{i 1} + \sum_{i \mathop = 2}^3 a_{i 2} + \sum_{i \mathop = 3}^3 a_{i 3}\)

\(\ds \)

\(=\)

\(\ds \left({a_{1 1} + a_{2 1} + a_{3 1} }\right) + \left({a_{2 2} + a_{3 2} }\right) + \left({a_{3 3} }\right)\)