nyuuzyou/wikis huggingface dataset:
Excess Kurtosis of Hat-Check Distribution

== Theorem ==
Let $X$ be a discrete random variable with a Hat-Check distribution with parameter $n$. ($n \gt 3$)
Then the excess kurtosis $\gamma_2$ of $X$ is given by: 
:$\gamma_2 = 1$
== Proof ==
From Kurtosis in terms of Non-Central Moments, we have: 
:$\gamma_2 = \dfrac {\expect {X^4} - 4 \mu \expect {X^3} + 6 \mu^2 \expect {X^2} - 3 \mu^4} {\sigma^4} - 3$
where: 
:$\mu$ is the expectation of $X$. 
:$\sigma$ is the standard deviation of $X$.
We have, by Expectation of Hat-Check Distribution:
:$\expect X = n - 1$
By Variance of Hat-Check Distribution:
:$\var X = \sigma^2 = 1$
:$\expect {X^2} = \paren {n - 1 }^2 + 1$
By Skewness of Hat-Check Distribution:
:$\expect {X^3} = n^3 - 3n^2 + 6n - 5$
To now calculate $\gamma_2$, we must calculate $\expect {X^4}$.
To help complete the sum above, recall that:
Therefore:
So:
Category:Kurtosis
Category:Hat-Check Distribution
Excess Kurtosis of Log Normal Distribution

== Theorem == 
Let $X$ be a continuous random variable with the Log Normal distribution with $\mu \in \R, \sigma \in \R_{> 0}$.
Then the excess kurtosis $\gamma_2$ of $X$ is given by: 
:$\gamma_2 = \map \exp {4 \sigma^2} + 2 \map \exp {3 \sigma^2} + 3 \map \exp {2 \sigma^2} - 6$
== Proof == 
From Kurtosis in terms of Non-Central Moments, we have: 
:$\gamma_2 = \dfrac {\expect {X^4} - 4 \mu \expect {X^3} + 6 \mu^2 \expect {X^2} - 3 \mu^4} {\sigma^4} - 3$
where: 
:$\mu$ is the expectation of $X$. 
:$\sigma$ is the standard deviation of $X$.
By Expectation of Log Normal Distribution we have: 
:$\mu = \map \exp {\mu + \dfrac {\sigma^2} 2}$ 
By Variance of Log Normal Distribution we have: 
:$\sigma = \map \exp {\mu + \dfrac {\sigma^2} 2} \sqrt {\paren {\map \exp {\sigma^2} - 1} }$ 
From Raw Moment of Log Normal Distribution, we have:
:$\expect {X^n} = \map \exp {n \mu + \dfrac {n^2 \sigma^2} 2}$
Hence:
Category:Kurtosis
Category:Log Normal Distribution
Excess Kurtosis of Logistic Distribution

== Theorem == 
Let $X$ be a continuous random variable which satisfies the logistic distribution:
:$X \sim \map {\operatorname {Logistic} } {\mu, s}$
Then the excess kurtosis $\gamma_2$ of $X$ is equal to $\dfrac 6 5$.
== Proof == 
From Kurtosis in terms of Non-Central Moments, we have: 
:$\gamma_2 = \dfrac {\expect {X^4} - 4 \mu \expect {X^3} + 6 \mu^2 \expect {X^2} - 3 \mu^4} {\sigma^4} - 3$
where: 
:$\mu$ is the expectation of $X$. 
:$\sigma$ is the standard deviation of $X$.
By Expectation of Logistic Distribution we have: 
:$\mu = \mu$ 
By Variance of Logistic Distribution we have: 
:$\sigma = \dfrac {s \pi} {\sqrt 3}$ 
From Moment in terms of Moment Generating Function:
:$\expect {X^n} = \map { {M_X}^{\paren n} } 0$
where $M_X$ is the moment generating function of $X$.
From Derivatives of Moment Generating Function of Logistic Distribution: 
:$\ds \map { {M_X}^{\paren 4} } 0 = \mu^4 \int_{\to 0}^{\to 1} \rd u - 4 \mu^3 s \int_{\to 0}^{\to 1} \map \ln {\dfrac {1 - u} u} \rd u + 6 \mu^2 s^2 \int_{\to 0}^{\to 1} \map {\ln^2} {\dfrac {1 - u} u} \rd u - 4 \mu s^3 \int_{\to 0}^{\to 1} \map {\ln^3} {\dfrac {1 - u} u} \rd u + s^4 \int_{\to 0}^{\to 1} \map {\ln^4} {\dfrac {1 - u} u} \rd u $
Therefore:
Hence:
Category:Kurtosis
Category:Logistic Distribution
Excess Kurtosis of Pareto Distribution

== Theorem == 
Let $X$ be a continuous random variable with the Pareto distribution with $a, b \in \R_{> 0}$.
Then the excess kurtosis $\gamma_2$ of $X$ is given by: 
:$\gamma_2 = \begin {cases} \dfrac {6 \paren { a^3 + a^2 - 6 a - 2} } {a \paren {a - 3} \paren {a - 4} } & 4 < a \\ \text {does not exist} & 4 \ge a \end {cases}$
=== Lemma 1 ===
=== Lemma 2 ===
=== Lemma 3 ===
=== Lemma 4 ===
== Proof == 
From Kurtosis in terms of Non-Central Moments, we have: 
:$\gamma_2 = \dfrac {\expect {X^4} - 4 \mu \expect {X^3} + 6 \mu^2 \expect {X^2} - 3 \mu^4} {\sigma^4} - 3$
where: 
:$\mu$ is the expectation of $X$. 
:$\sigma$ is the standard deviation of $X$.
By Expectation of Pareto Distribution we have: 
:$\mu = \dfrac {a b } {\paren {a - 1} }$ 
By Variance of Pareto Distribution we have: 
:$\sigma = \dfrac {\sqrt a b } {\sqrt {\paren {a - 2} } \paren {a - 1} }$ 
From Raw Moment of Pareto Distribution, we have:
:$\ds \expect {X^n} = \begin {cases} \dfrac {a b^n} {a - n} & n < a \\ \text {does not exist} & n \ge a \end {cases}$
Hence:
Category:Kurtosis
Category:Pareto Distribution
Category:Excess Kurtosis of Pareto Distribution
Excess Kurtosis of Pareto Distribution/Lemma 1

== Lemma for Excess Kurtosis of Pareto Distribution ==
:$\paren {a - 1}^4 \paren {a - 2}^2 \paren {a - 3} = a^7 - 11 a^6 + 50 a^5 - 122 a^4 + 173 a^3 - 143 a^2 + 64 a - 12$
== Proof == 
Category:Excess Kurtosis of Pareto Distribution
Excess Kurtosis of Pareto Distribution/Lemma 2

== Lemma for Excess Kurtosis of Pareto Distribution ==
:$4 a \paren {a - 1}^3 \paren {a - 2}^2 \paren {a - 4} = 4 a^7 - 44 a^6 + 188 a^5 - 404 a^4 + 464 a^3 - 272 a^2 + 64 a$
== Proof == 
Category:Excess Kurtosis of Pareto Distribution
Excess Kurtosis of Pareto Distribution/Lemma 3

== Lemma for Excess Kurtosis of Pareto Distribution ==
:$6 a^2 \paren {a - 1}^2 \paren {a - 2} \paren {a - 3} \paren {a - 4} = 6 a^7 - 66 a^6 + 270 a^5 - 510 a^4 + 444 a^3 - 144 a^2$
== Proof == 
Category:Excess Kurtosis of Pareto Distribution
Excess Kurtosis of Pareto Distribution/Lemma 4

== Lemma for Excess Kurtosis of Pareto Distribution ==
:$3 a^3 \paren {a - 2}^2 \paren {a - 3} \paren {a - 4} = 3 a^7 - 33 a^6 + 132 a^5 - 228 a^4 + 144 a^3$
== Proof == 
Category:Excess Kurtosis of Pareto Distribution
Excess Kurtosis of Poisson Distribution

== Theorem ==
Let $X$ be a discrete random variable with a Poisson distribution with parameter $\lambda$.
Then the excess kurtosis $\gamma_2$ of $X$ is given by: 
:$\gamma_2 = \dfrac 1 \lambda$
== Proof == 
From the definition of excess kurtosis, we have: 
:$\gamma_2 = \expect {\paren {\dfrac {X - \mu} \sigma}^4} - 3$
where: 
:$\mu$ is the expectation of $X$. 
:$\sigma$ is the standard deviation of $X$.
By Expectation of Poisson Distribution, we have: 
:$\mu = \lambda$
By Variance of Poisson Distribution, we have: 
:$\sigma = \sqrt {\lambda}$ 
So: 
To calculate $\gamma_2$, we must calculate $\expect {X^4}$.
We find this using the moment generating function of $X$, $M_X$. 
By Moment Generating Function of Poisson Distribution, this is given by: 
:$\ds \map {M_X} t = e^{\lambda \paren {e^t - 1} }$
From Moment in terms of Moment Generating Function:
:$\expect {X^4} = \map {M_X'} 0$
In Skewness of Poisson Distribution, it is shown that:
So:
Setting $t = 0$:
Plugging this result back into our equation above:
Category:Kurtosis
Category:Poisson Distribution
Excess Kurtosis of Snedecor's F-Distribution

== Theorem ==
Let $n, m$ be strictly positive integers. 
Let $X \sim F_{n, m}$ where $F_{n, m}$ is Snedecor's F-distribution with $\tuple {n, m}$ degrees of freedom.
Then the excess kurtosis $\gamma_2$ of $X$ is given by: 
:$\gamma_2 = \dfrac {12 \paren {5 m n^2 - 22 n^2 + 5 m^2 n - 32 m n + 44 n + m^3 - 8 m^2 + 20 m - 16} } {n \paren {m - 6} \paren {m - 8} \paren {m + n - 2} }$
for $m > 8$, and does not exist otherwise. 
 
== Proof == 
Category:Kurtosis
Category:Snedecor's F-Distribution
Excess Kurtosis of Student's t-Distribution

== Theorem ==
Let $k$ be a strictly positive integer. 
Let $X \sim t_k$ where $t_k$ is the $t$-distribution with $k$ degrees of freedom.
Then the excess kurtosis $\gamma_2$ of $X$ is given by: 
:$\gamma_2 = \dfrac 6 {k - 4}$
for $k > 4$, and does not exist otherwise.
== Proof ==
Category:Kurtosis
Category:Student's t-Distribution
Excess Kurtosis of Weibull Distribution

== Theorem == 
Let $X$ be a continuous random variable with the Weibull distribution with $\alpha, \beta \in \R_{> 0}$.
Then the excess kurtosis $\gamma_2$ of $X$ is given by: 
:$\gamma_2 = \dfrac {\map \Gamma {1 + \dfrac 4 \alpha} - 4 \map \Gamma {1 + \dfrac 1 \alpha} \map \Gamma {1 + \dfrac 3 \alpha} + 12 \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2 \map \Gamma {1 + \dfrac 2 \alpha} - 6 \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^4 - 3 \paren {\map \Gamma {1 + \dfrac 2 \alpha} }^2 } {\paren {\map \Gamma {1 + \dfrac 2 \alpha} - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2}^2 }$
where $\Gamma$ is the Gamma function.
== Proof == 
From Kurtosis in terms of Non-Central Moments, we have: 
:$\gamma_2 = \dfrac {\expect {X^4} - 4 \mu \expect {X^3} + 6 \mu^2 \expect {X^2} - 3 \mu^4} {\sigma^4} - 3$
where: 
:$\mu$ is the expectation of $X$. 
:$\sigma$ is the standard deviation of $X$.
By Expectation of Weibull Distribution we have: 
:$\mu = \beta \, \map \Gamma {1 + \dfrac 1 \alpha}$ 
By Variance of Weibull Distribution we have: 
:$\sigma = \beta \, \paren {\map \Gamma {1 + \dfrac 2 \alpha} - \paren {\map \Gamma {1 + \dfrac 1 \alpha} }^2}^{\frac 1 2}$ 
From Raw Moment of Weibull Distribution, we have:
:$\expect {X^n} = \beta^n \map \Gamma {1 + \dfrac n \alpha}$
Hence:
Category:Kurtosis
Category:Weibull Distribution
Exchange Operation as Replacement Operations

== Example of use of Replacement Operation ==
Let $x$ and $y$ be variables whose values are to be exchanged.
The exchange operation on $x$ and $y$ can be implemented using replacement operations.
Let $t$ be a third variable which has been established for this purpose.
Then the sequence of replacement operations:
:$t \gets x$
:$x \gets y$
:$y \gets t$
performs the task.
== Proof ==
Observing the values of the variables after each replacement operation:
Operation 	$x$	$y$	$t$
$t \gets x$	$x$	$y$	$x$
$x \gets y$	$y$	$y$	$x$
$y \gets t$	$y$	$x$	$x$
Hence the result.
== Sources ==
* : $\S 1.1$: Algorithms
Category:Algorithms
Exchange of Columns as Sequence of Other Elementary Column Operations

== Theorem ==
Let $\mathbf A$ be an $m \times n$ matrix.
Let $i, j \in \closedint 1 m: i \ne j$
Let $\kappa_k$ denote the $k$th column of $\mathbf A$ for $1 \le k \le n$:
:$\kappa_k = \begin {pmatrix} a_{1 k} \\ a_{2 k} \\ \vdots \\ a_{m k} \end {pmatrix}$
Let $e$ be the elementary column operation acting on $\mathbf A$ as:
Then $e$ can be expressed as a finite sequence of exactly $4$ instances of the other two elementary column operations.
== Proof ==
In the below:
:$\kappa_i$ denotes the initial state of column $i$
:$\kappa_j$ denotes the initial state of column $j$
:$\kappa_i'$ denotes the state of column $i$ after having had the latest elementary column operation applied
:$\kappa_j'$ denotes the state of column $j$ after having had the latest elementary column operation applied.
$(1)$: Apply $\text {ECO} 2$ to column $j$ for $\lambda = 1$:
:$\kappa_j \to \kappa_j + \kappa_i$
After this operation:
$(2)$: Apply $\text {ECO} 2$ to column $i$ for $\lambda = -1$:
:$\kappa_i \to \kappa_i + \paren {-\kappa_j}$
After this operation:
$(3)$: Apply $\text {ECO} 2$ to column $j$ for $\lambda = 1$:
:$\kappa_j \to \kappa_j + \kappa_i$
After this operation:
$(4)$: Apply $\text {ECO} 1$ to column $i$ for $\lambda = -1$:
:$\kappa_i \to -\kappa_i$
After this operation:
Thus, after all the $4$ elementary column operations have been applied, we have:
Hence the result.
== Also see ==
* Exchange of Rows as Sequence of Other Elementary Row Operations
Category:Elementary Column Operations
Exchange of Order of Indexed Summations

== Theorem ==
Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $a, b, c, d \in \Z$ be integers.
Let $\closedint a b$ denote the integer interval between $a$ and $b$.
=== Rectangular Domain ===
== Also see ==
* Exchange of Order of Summations over Finite Sets
Category:Summations
Exchange of Order of Indexed Summations/Rectangular Domain

== Theorem ==
Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $a, b, c, d \in \Z$ be integers.
Let $\closedint a b$ denote the integer interval between $a$ and $b$.
Let $D = \closedint a b \times \closedint c d$ be the cartesian product.
Let $f: D \to \mathbb A$ be a mapping
Then we have an equality of indexed summations:
:$\ds \sum_{i \mathop = a}^b \sum_{j \mathop = c}^d \map f {i, j} = \sum_{j \mathop = c}^d \sum_{i \mathop = a}^b \map f {i, j}$
== Outline of Proof ==
We use induction on $d$. In the induction step, we use Indexed Summation of Sum of Mappings.
== Proof ==
The proof proceeds by induction on $d$.
=== Basis for the Induction ===
Let $d < c$.
Then the indexed summation in the is zero.
By Indexed Summation of Zero, so is the .
This is our basis for the induction.
=== Induction Step ===
Let $d \ge c$.
We have:
By the Principle of Mathematical Induction, the proof is complete.
== Also see ==
* Exchange of Order of Summations over Finite Sets
Category:Summations
Exchange of Order of Product

== Theorem ==
Let $R: \Z \to \set {\T, \F}$ and $S: \Z \to \set {\T, \F}$ be propositional functions on the set of integers.
Let $\ds \prod_{\map R i} x_i$ denote a product over $R$.
Let the fiber of truth of both $R$ and $S$ be finite.
Then:
:$\ds \prod_{\map R i} \prod_{\map S j} a_{i j} = \prod_{\map S j} \prod_{\map R i} a_{i j}$
== Proof ==
== Also known as ==
The word interchange can often be seen for exchange.
== Sources ==
* : $\S 1.2.3$: Sums and Products
Category:Continued Products
Exchange of Order of Summation

== Theorem ==
Let $R: \Z \to \set {\T, \F}$ and $S: \Z \to \set {\T, \F}$ be propositional functions on the set of integers.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of both $R$ and $S$ be finite.
Then:
:$\ds \sum_{\map R i} \sum_{\map S j} a_{i j} = \sum_{\map S j} \sum_{\map R i} a_{i j}$
=== Finite and Infinite Series ===
=== Infinite Series ===
== Proof ==
== Example ==
== Also known as ==
The word interchange can often be seen for exchange.
== Sources ==
* : $\S 1.2.3$: Sums and Products: $(7)$
Category:Summations
Exchange of Order of Summation/Example

== Theorem ==
Let $R: \Z \to \set {\T, \F}$ and $S: \Z \to \set {\T, \F}$ be propositional functions on the set of integers.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of both $R$ and $S$ be infinite.
Then it is not necessarily the case that:
:$\ds \sum_{\map R i} \sum_{\map S j} a_{i j} = \sum_{\map S j} \sum_{\map R i} a_{i j}$
== Proof ==
Proof by Counterexample:
== Sources ==
* : $\S 1.2.3$: Sums and Products: Exercise $8$
Category:Summations
Exchange of Order of Summation/Finite and Infinite Series

== Theorem ==
Let $R: \Z \to \set {\T, \F}$ and $S: \Z \to \set {\T, \F}$ be propositional functions on the set of integers.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of $R$ be infinite.
Let the fiber of truth of $S$ be finite.
For all $j$ in the fiber of truth of $S$, let $\ds \sum_{\map R i} a_{i j}$ be convergent.
Then:
:$\ds \sum_{\map R i} \sum_{\map S j} a_{i j} = \sum_{\map S j} \sum_{\map R i} a_{i j}$
== Proof ==
== Sources ==
* : $\S 1.2.3$: Sums and Products
Category:Summations
Exchange of Order of Summation/Infinite Series

== Theorem ==
Let $R: \Z \to \set {\T, \F}$ and $S: \Z \to \set {\T, \F}$ be propositional functions on the set of integers.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of both $R$ and $S$ be infinite.
Let:
:$\ds \sum_{\map R i} \sum_{\map S j} \size {a_{i j} }$
exist.
Then:
:$\ds \sum_{\map R i} \sum_{\map S j} a_{i j} = \sum_{\map S j} \sum_{\map R i} a_{i j}$
== Proof ==
== Sources ==
* : $\S 1.2.3$: Sums and Products
Category:Summations
Exchange of Order of Summation with Dependency on Both Indices

== Theorem ==
Let $R: \Z \to \set {\T, \F}$ be a propositional function on the set of integers.
Let $S: \Z \times \Z \to \set {\T, \F}$ be a propositional function on the Cartesian product of the set of integers with itself.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of both $R$ and $S$ be finite.
Then:
:$\ds \sum_{\map R i} \sum_{\map S {i, j} } a_{i j} = \sum_{\map {S'} j} \sum_{\map {R'} {i, j} } a_{i j}$
where:
:$\map {S'} j$ denotes the propositional function:
::there exists an $i$ such that both $\map R i$ and $\map S {i, j}$ hold
:$\map {R'} {i, j}$ denotes the propositional function:
::both $\map R i$ and $\map S {i, j}$ hold.
=== Infinite Series ===
== Proof ==
== Example ==
== Sources ==
* : $\S 1.2.3$: Sums and Products: $(9)$
Category:Summations
Exchange of Order of Summation with Dependency on Both Indices/Example

== Theorem ==
Let $n \in \Z$ be an integer.
Let $R: \Z \to \set {\T, \F}$ be the propositional function on the set of integers defining:
:$\forall i \in \Z: \map R 1 := \paren {n = k i \text { for some } k \in \Z}$
Let $S: \Z \times \Z \to \set {\T, \F}$ be a propositional function on the Cartesian product of the set of integers with itself defining:
:$\forall i, j \in \Z: \map S {i, j} := \paren {1 \le j < i}$
Consider the summation:
:$\ds \sum_{\map R i} \sum_{\map S {i, j} } a_{i j}$
Then:
:$\ds \sum_{\map R i} \sum_{\map S {i, j} } a_{i j} = \sum_{\map {S'} j} \sum_{\map {R'} {i, j} } a_{i j}$
where:
:$\map {S'} j$ denotes the propositional function:
::$\forall j \in \Z: \map {S'} j := \paren {1 < j \le n}$
:$\map {R'} {i, j}$ denotes the propositional function:
::$\forall i, j \in \Z: \map {R'} {i, j} := \paren {n = k i \text { for some } k \in \Z \text { and } i > j}$
== Proof ==
From Exchange of Order of Summation with Dependency on Both Indices:
:$\map {S'} j$ denotes the propositional function:
::there exists an $i$ such that both $\map R i$ and $\map S {i, j}$ hold
:$\map {R'} {i, j}$ denotes the propositional function:
::both $\map R i$ and $\map S {i, j}$ hold.
The definition of $\map {R'} {i, j}$ follows immediately:
:$\map R i := \paren {n = k i \text { for some } k \in \Z}$
and:
:$\map S {i, j} := \paren {1 \le j < i}$
Then:
By Absolute Value of Integer is not less than Divisors, it follows from $\map R i$ that $i \le n$.
That is, for $\map {S'} j$ to hold, $i \le n$.
But for all $j \in \Z$ such that $1 \le j < n$ it follows that $i = n$ fulfils the condition that $n = k i$.
Hence:
:$\map {S'} j := \paren {1 < j \le n}$
== Sources ==
* : $\S 1.2.3$: Sums and Products: Exercise $18$
Category:Summations
Exchange of Order of Summation with Dependency on Both Indices/Infinite Series

== Theorem ==
Let $R: \Z \to \set {\T, \F}$ be a propositional functions on the set of integers.
Let $S: \Z \times \Z \to \set {\T, \F}$ be a propositional functions on the Cartesian product of the set of integers with itself.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of both $R$ and $S$ be infinite.
Let:
:$\ds \sum_{\map R i} \sum_{\map S {i, j} } \size {a_{i j} }$
exist.
Then:
:$\ds \sum_{\map R i} \sum_{\map S {i, j} } a_{i j} = \sum_{\map {S'} j } \sum_{\map {R'} {i, j} } a_{i j}$
where:
:$\map {S'} j$ denotes the propositional function:
::there exists an $i$ such that both $\map R i$ and $\map S {i, j}$ hold
:$\map {R'} {i, j}$ denotes the propositional function:
::both $\map R i$ and $\map S {i, j}$ hold.
== Proof ==
== Sources ==
* : $\S 1.2.3$: Sums and Products
Category:Summations
Exchange of Order of Summations over Finite Sets

== Theorem ==
Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $S, T$ be finite sets.
Let $S \times T$ be their cartesian product.
=== Cartesian Product ===
=== Subset of Cartesian Product ===
== Also see ==
* Exchange of Order of Indexed Summations
Category:Summations
Exchange of Order of Summations over Finite Sets/Cartesian Product

== Theorem ==
Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $S, T$ be finite sets.
Let $S \times T$ be their cartesian product.
Let $f: S \times T \to \mathbb A$ be a mapping.
Then we have an equality of summations over finite sets:
:$\ds \sum_{s \mathop \in S} \sum_{t \mathop \in T} \map f {s, t} = \sum_{t \mathop \in T} \sum_{s \mathop \in S} \map f {s, t}$
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
Category:Summations
Category:Exchange of Order of Summations over Finite Sets
Exchange of Order of Summations over Finite Sets/Cartesian Product/Proof 2

== Theorem ==
== Proof ==
Let $m$ be the cardinality of $S$ and $n$ be the cardinality of $T$.
Let $\N_{< m}$ denote an initial segment of the natural numbers.
Let $\sigma: \N_{< m} \to S$ and $\tau : \N_{< n} \to T$ be bijections.
We have:
Category:Exchange of Order of Summations over Finite Sets
Exchange of Order of Summations over Finite Sets/Cartesian Product/Proof 3

== Theorem ==
== Proof ==
Let $n$ be the cardinality of $T$.
The proof goes by induction on $n$.
=== Basis for the Induction ===
Let $n = 0$.
=== Induction Step ===
Let $n > 0$.
Let $t \in T$.
Use Cardinality of Set minus Singleton
Category:Exchange of Order of Summations over Finite Sets
Exchange of Order of Summations over Finite Sets/Subset of Cartesian Product

== Theorem ==
Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $S, T$ be finite sets.
Let $S \times T$ be their cartesian product.
Let $D\subset S \times T$ be a subset.
Let $\pi_1 : D \to S$ and $\pi_2 : D \to T$ be the restrictions of the projections of $S\times T$.
Then we have an equality of summations over finite sets:
:$\ds \sum_{s \mathop \in S} \sum_{t \mathop \in \map {\pi_2} {\map {\pi_1^{-1} } s} } \map f {s, t} = \sum_{t \mathop \in T} \sum_{s \mathop \in \map {\pi_1} {\map {\pi_2^{-1} } t} } \map f {s, t}$
where $\map {\pi_1^{-1} } s$ denotes the inverse image of $s$ under $\pi_1$.
== Proof ==
Define an extension $\overline f$ of $f$ to $S \times T$ by:
:$\map {\overline f} {s, t} = \begin{cases}
\map f {s, t} & : \tuple {s, t} \in D \\
0 & : \tuple {s, t} \notin D
\end{cases}$
Then for all $s \in S$, by:
:Preimage of Disjoint Union is Disjoint Union
:Sum over Disjoint Union of Finite Sets
:Summation over Finite Set of Zero:
:$\ds \sum_{t \mathop \in \map {\pi_2} {\map {\pi_1^{-1} } s} } \map f {s, t} = \sum_{t \mathop \in T} \map {\overline f} {s, t}$
Thus:
:$\ds \sum_{s \mathop \in S} \sum_{t \mathop \in \map {\pi_2} {\map {\pi_1^{-1} } s} } \map f {s, t} = \sum_{s \mathop \in S} \sum_{t \mathop \in T} \map {\overline f} {s, t}$
Similarly:
:$\ds \sum_{t \mathop \in T} \sum_{s \mathop \in \map {\pi_1} {\map {\pi_2^{-1} } t} } \map f {s, t} = \sum_{t \mathop \in T} \sum_{s \mathop \in S} \map {\overline f} {s, t}$
By Exchange of Order of Summation over Cartesian Product of Finite Sets, the result follows.
Category:Summations
Exchange of Order of Supremum Operators

== Theorem ==
Let $\family {a_i}_{i \mathop \in I}$ be a family of elements of the non-negative real numbers $\R_{\ge 0}$ indexed by $I$.
Let $\family {b_j}_{j \mathop \in J}$ be a family of elements of the non-negative real numbers $\R_{\ge 0}$ indexed by $J$.
Let $\map R i$ and $\map S j$ be propositional functions of $i \in I$, $j \in J$.
Let $\ds \sup_{\map R i} a_i$ and $\ds \sup_{\map S j} b_j$ be the indexed suprema on $\family {a_i}$ and $\family {b_j}$ respectively.
Then:
:$\ds \sup_{\map R i} \paren {\sup_{\map S j} a_{i j} } = \sup_{\map S j} \paren {\sup_{\map R i} a_{i j} }$
== Proof ==
For any chosen $i$ and $j$, we have:
:$\ds a_{ij} \le \sup_{\map R i} a_{ij}$
Taking the supremum over $\map S j$ yields:
:$\ds \sup_{\map S j} a_{ij} \le \sup_{\map S j} \sup_{\map R i} a_{ij}$
for all $i$.
Hence the remains an upper bound after taking the supremum over $\map R i$ on the .
That is:
:$\ds \sup_{\map R i} \paren {\sup_{\map S j} a_{ij} } \le \sup_{\map S j} \paren {\sup_{\map R i} a_{ij} }$
Applying the same argument with $\ds a_{ij} \le \sup_{\map S j} a_{ij}$, we obtain the reverse inequality.
== Sources ==
* : $\S 1.2.3$: Sums and Products: Exercise $35$
Category:Suprema