avewright/proofwiki-math huggingface dataset:
Theorem: Raw Moment of Pareto Distribution

Let $X$ be a continuous random variable with the Pareto distribution with $a, b \in \R_{> 0}$.
Let $n$ be a strictly positive integer. 
Then the $n$th raw moment $\expect {X^n}$ of $X$ is given by: 
:$\expect {X^n} = \begin {cases} \dfrac {a b^n} {a - n} & n < a \\ \text {does not exist} & n \ge a \end {cases}$

Proof:
From the definition of the Pareto distribution, $X$ has probability density function:
:$\map {f_X} x = \dfrac {a b^a} {x^{a + 1} }$
Where $\Img X \in \hointr b \infty$.
From the definition of the expected value of a continuous random variable: 
:$\ds \expect {X^n} = \int_b^\infty x^n \map {f_X} x \rd x$
First take $a > n$. 
{{begin-eqn}}
{{eqn | l = \expect {X^n}
      | r = a b^a \int_b^\infty x^{n - a - 1} \rd x
}}
{{eqn | r = a b^a \bigintlimits {\dfrac {x^{n - a} } {n - a} } b \infty
      | c = Primitive of Power
}}
{{eqn | r =  \dfrac {a b^a} {n - a} \paren {\lim_{x \mathop \to \infty} x^{n - a} - b^{n - a} }
}}
{{eqn | r = a b^a \paren {0 - \dfrac {b^{n - a} } {n - a} }
      | c = for $n - a < 0$, $x^{n - a} \mathop \to 0$ as $x \mathop \to \infty$
}}
{{eqn	| r = \dfrac {a b^n} {a - n}
        | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Now take $a = n$.
{{begin-eqn}}
{{eqn | l = \expect {X^n}
      | r = a b^a \int_b^\infty x^{a - a - 1} \rd x
}}
{{eqn | r = a b^a \bigintlimits {\ln x } b \infty
      | c = Primitive of Reciprocal
}}
{{eqn | r =  a b^a \paren {\lim_{x \mathop \to \infty} \ln x - \ln b }
}}
{{eqn | o = \to
      | r = \infty
      | c = Logarithm Tends to Infinity
}}
{{end-eqn}}
{{qed|lemma}}
Finally, take $a < n$. 
{{begin-eqn}}
{{eqn | l = \expect {X^n}
      | r = a b^a \int_b^\infty x^{n - a - 1} \rd x
}}
{{eqn | r = a b^a \bigintlimits {\dfrac {x^{n - a} } {n - a} } b \infty
      | c = Primitive of Power
}}
{{eqn | r = \dfrac {a b^a} {n - a} \paren {\lim_{x \mathop \to \infty} x^{n - a} - b^{n - a} }
}}
{{eqn | o = \to
      | r = \infty
      | c = for $n - a > 0$, $x^{n - a}$ increases without bound as $x \mathop \to \infty$
}}
{{end-eqn}}
{{qed}}
Category:Pareto Distribution
Category:Raw Moments
2dgcfjawstxkjkxk9m7lswt6xbj78yz
Theorem: Expectation of Pareto Distribution

Let $X$ be a continuous random variable with the Pareto distribution with $a, b \in \R_{> 0}$.
The expectation of $X$ is given by:
:$\expect X = \begin {cases} \dfrac {a b} {a - 1} & 1 < a \\ \text {does not exist} & 1 \ge a \end {cases}$

Proof:
From Raw Moment of Pareto Distribution, we have:
The $n$th raw moment $\expect {X^n}$ of $X$ is given by: 
:$\expect {X^n} = \begin {cases} \dfrac {a b^n} {a - n} & n < a \\ \text {does not exist} & n \ge a \end {cases}$
Therefore, for $n = 1$ we have:
:$\expect X = \begin {cases} \dfrac {a b} {a - 1} & 1 < a \\ \text {does not exist} & 1 \ge a \end {cases}$
{{qed}}
Category:Pareto Distribution
Category:Expectation
4vuj127vgz8h6e2p0mt68fscjyxyijn
Theorem: Variance of Pareto Distribution

Let $X$ be a continuous random variable with the Pareto distribution with $a, b \in \R_{> 0}$.
Then the variance of $X$ is given by: 
:$\var X = \begin {cases} \dfrac {a b^2 } {\paren {a - 2} \paren {a - 1}^2 } & 2 < a \\ \text {does not exist} & 2 \ge a \end {cases}$

Proof:
By Variance as Expectation of Square minus Square of Expectation, we have: 
:$\var X = \expect {X^2} - \paren {\expect X}^2$
By Expectation of Pareto Distribution, we have: 
:$\expect X = \begin {cases} \dfrac {a b} {a - 1} & 1 < a \\ \text {does not exist} & 1 \ge a \end {cases}$
From Raw Moment of Pareto Distribution, we have:
The $n$th raw moment $\expect {X^n}$ of $X$ is given by: 
:$\expect {X^n} = \begin {cases} \dfrac {a b^n} {a - n} & n < a \\ \text {does not exist} & n \ge a \end {cases}$
Therefore, for $n = 2$ we have:
:$\expect {X^2} = \begin {cases} \dfrac {a b^2} {a - 2} & 2 < a \\ \text {does not exist} & 2 \ge a \end {cases}$
So:
{{begin-eqn}}
{{eqn | l = \var X
      | r = \dfrac {a b^2} {a - 2} - \paren {\dfrac {a b} {a - 1} }^2
}}
{{eqn | r = \dfrac {a b^2 \paren {a - 1}^2 - a^2 b^2 \paren {a - 2} } {\paren {a - 2} \paren {a - 1}^2 }
}}
{{eqn | r = \dfrac {a b^2 } {\paren {a - 2} \paren {a - 1}^2 }
}}
{{end-eqn}}
{{qed}}
Category:Variance
Category:Pareto Distribution
t4fadcov6unwwtapbqzu9nzatwlpmfl
Theorem: Ordered Set with Order Type of Natural Numbers plus Dual has Minimum Element

Let $\struct {S, \preccurlyeq}$ be an ordered structure such that:
:$\map \ot {S, \preccurlyeq} = \omega + \omega^*$
where:
:$\ot$ denotes order type
:$\omega$ denotes the order type of the natural numbers $\N$
:$\omega^*$ denotes the dual of $\omega$
:$+$ denotes addition of order types.
Then $\struct {S, \preccurlyeq}$ has a smallest element.

Proof:
By definition of order type addition:
:$\struct {S, \preccurlyeq}$ is isomorphic to $\struct {\N, \le} \oplus \struct {\N, \ge}$
where:
:$\cong$ denotes order isomorphism
:$\oplus$ denotes order sum.
By the Well-Ordering Principle, $\struct {\N, \le}$ has a smallest element.
By definition of order sum, every element of $\struct {\N, \le}$ precedes every element of $\struct {\N, \ge}$.
Hence the smallest element of $\struct {\N, \le}$ is also the smallest element of $\struct {\N, \le} \oplus \struct {\N, \ge}$.
Hence the result.
{{qed}}
Theorem: Order Type Addition is not Commutative

The operation of order type addition is not commutative.

Proof:
Consider the order type $\omega^* + \omega$, where:
:$\omega$ denotes the order type of the natural numbers $\N$
:$\omega^*$ denotes the dual of $\omega$
:$+$ denotes addition of order types.
From Order Type of Integers under Usual Ordering, this is the order type of $\struct {\Z, \le}$, the set of integers under the usual ordering.
Now consider order type $\omega + \omega^*$.
From Ordered Set with Order Type of Natural Numbers plus Dual has Minimum Element, this is the order type of an ordered structure $\struct {S, \preccurlyeq}$ which has a smallest element.
But $\struct {\Z, \le}$ has no such smallest element.
It follows that $\struct {\Z, \le}$ is not isomorphic to $\struct {S, \preccurlyeq}$.
Hence $\omega + \omega^*$ and $\omega^* + \omega$ are different order types.
The result follows.
{{qed}}
Theorem: Skewness of Pareto Distribution

Let $X$ be a continuous random variable with the Pareto distribution with $a, b \in \R_{> 0}$.
Then the skewness $\gamma_1$ of $X$ is given by:
:$\gamma_1 = \begin {cases} \paren {\sqrt {\dfrac {\paren {a - 2} } a } } \paren { \dfrac {2 \paren {a + 1} } {a - 3} } & 3 < a \\ \text {does not exist} & 3 \ge a \end {cases}$

Proof:
From Skewness in terms of Non-Central Moments, we have: 
:$\gamma_1 = \dfrac {\expect {X^3} - 3 \mu \sigma^2 - \mu^3} {\sigma^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:
:$\expect {X^3} = \begin {cases} \dfrac {a b^3} {a - 3} & 3 < a \\ \text {does not exist} & 3 \ge a \end {cases}$
So: 
{{begin-eqn}}
{{eqn	| l = \gamma_1
	| r = \frac {\paren {\dfrac {a b^3} {a - 3} } - 3 \paren {\dfrac {a b } {\paren {a - 1} } } \paren {\dfrac {a b^2 } {\paren {a - 2} \paren {a - 1}^2 } } - \paren {\dfrac {a b } {\paren {a - 1} } }^3} {\paren {\dfrac {\sqrt a b } {\sqrt {\paren {a - 2} } \paren {a - 1} } }^3 }
}}
{{eqn	| r = \frac {\paren {\dfrac {a b^3} {a - 3} } \paren {\dfrac {\paren {a - 1} } {\paren {a - 1} } }^3 - 3 \paren {\dfrac {a^2 b^3 } {\paren {a - 2} \paren {a - 1}^3 } } - \paren {\dfrac {a b } {\paren {a - 1} } }^3} {\paren {\dfrac {\sqrt a b } {\sqrt {\paren {a - 2} } \paren {a - 1} } }^3 }
        | c = multiplying by $1$
}}
{{eqn	| r = \dfrac {\paren {\dfrac 1 {a - 3} } \paren { a - 1}^3 - 3 \paren {\dfrac a {\paren {a - 2} } } - a^2} {\paren {\dfrac {\sqrt a } {\paren {a - 2} \sqrt {\paren {a - 2} } } } }
        | c = canceling $\dfrac {a b^3} {\paren {a - 1}^3}$ from numerator and denominator
}}
{{eqn	| r = \paren {\sqrt {\dfrac {\paren {a - 2} } a } } \paren {\paren {\dfrac {a - 2} {a - 3} } \paren { a - 1}^3 - 3 a - a^2 \paren {a - 2} } 
        | c = 
}}
{{eqn	| r = \paren {\sqrt {\dfrac {\paren {a - 2} } a } } \paren {\paren {\dfrac {a - 2} {a - 3} } \paren { a^3 - 3 a^2 + 3 a - 1} - 3 a - a^3 + 2 a^2 } 
        | c = 
}}
{{eqn	| r = \paren {\sqrt {\dfrac {\paren {a - 2} } a } } \paren {\paren {\dfrac {a - 2} {a - 3} } \paren { a^3 - 3 a^2 + 3 a - 1} - \paren {3 a + a^3 - 2 a^2} \paren {\dfrac {a - 3} {a - 3} } } 
        | c = multiplying by $1$
}}
{{eqn	| r = \paren {\sqrt {\dfrac {\paren {a - 2} } a } } \paren {\dfrac {a^4 - 3 a^3 + 3 a^2 - a - 2 a^3 + 6 a^2 - 6a + 2 - 3 a^2 - a^4 + 2 a^3 + 9a + 3 a^3 - 6 a^2} {a - 3} }
        | c = 
}}
{{eqn	| r = \paren {\sqrt {\dfrac {\paren {a - 2} } a } } \paren {\dfrac {\paren {1 - 1} a^4 + \paren {-3 - 2 + 2 + 3} a^3 + \paren {3 + 6 - 3 - 6} a^2 + \paren {-1 - 6 + 9} a + 2} {a - 3} }
        | c = grouping terms
}}
{{eqn	| r = \paren {\sqrt {\dfrac {\paren {a - 2} } a } } \paren { \dfrac {2 \paren {a + 1} } {a - 3} }
        | c = 
}}
{{end-eqn}}
{{qed}}
Category:Skewness
Category:Pareto Distribution
5j8tqln03x4o04yjysm36vukxwocytr
Theorem: Simple Order Product of Pair of Ordered Sets is Ordered Set

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\struct {S_1, \preccurlyeq_1} \otimes^s \struct {S_2, \preccurlyeq_2}$ denote the '''simple (order) product''' of $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$.
Then $\struct {S_1, \preccurlyeq_1} \otimes^s \struct {S_2, \preccurlyeq_2}$ is also an ordered set.

Proof:
Let $\struct {T, \preccurlyeq_s} := \struct {S_1, \preccurlyeq_1} \otimes^s \struct {S_2, \preccurlyeq_2}$.
By definition of simple product:
:$T := S_1 \times S_2$ where $\times$ denotes Cartesian product
:$\forall \tuple {a, b}, \tuple {c, d} \in T: \tuple {a, b} \preccurlyeq_s \tuple {c, d} \iff a \preccurlyeq_1 c \text { and } b \preccurlyeq_2 d$
We check in turn each of the criteria for an ordering:
Theorem: Simple Order Product of Totally Ordered Sets may not be Totally Ordered

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be totally ordered sets.
Let $\struct {S_1, \preccurlyeq_1} \otimes^s \struct {S_2, \preccurlyeq_2}$ denote the '''simple (order) product''' of $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$.
Then it is not necessarily the case that $\struct {S_1, \preccurlyeq_1} \otimes^s \struct {S_2, \preccurlyeq_2}$ is also a totally ordered set.

Proof:
From Simple Order Product of Pair of Ordered Sets is Ordered Set, we do have that $\struct {S_1, \preccurlyeq_1} \otimes^s \struct {S_2, \preccurlyeq_2}$ is an ordered set.
Let us take the simple product of the ordered set that is the natural numbers under the usual ordering with itself:
:$\struct {\N, \le} \otimes^s \struct {\N, \le}$
We have from the Well-Ordering Principle that $\struct {\N, \le}$ is a well-ordered set, and so {{afortiori}} a totally ordered set.
Consider the ordered pairs of natural numbers:
:$s = \tuple {1, 4}$
:$t = \tuple {2, 3}$
Both $s$ and $t$ are elements of $\N \times \N$.
We have that:
:$1 \le 2$
but:
:$4 \not \le 3$
So it is not the case either that:
:$1 \le 2$ and $4 \le 3$
or:
:$2 \le 1$ and $3 \le 4$
Hence $s$ and $t$ are non-comparable elements.
The result follows by definition of totally ordered set.
{{qed}}
Theorem: Antilexicographic Order is Ordering

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\preccurlyeq_a$ be the lexicographic order on $S_1 \times S_2$''':
:$\tuple {x_1, x_2} \preccurlyeq_a \tuple {y_1, y_2} \iff \paren {x_2 \prec_2 y_2} \lor \paren {x_2 = y_2 \land x_1 \preccurlyeq_1 y_1}$
Then $\preccurlyeq_a$ is an ordering on $S_1 \times S_2$.

Proof:
In the following, $\tuple {x_1, x_2}, \tuple {y_1, y_2}, \tuple {z_1, z_2} \in S_1 \times S_2$.
Checking in turn each of the criteria for an ordering:
Theorem: Moment Generating Function of Pareto Distribution

Let $X$ be a continuous random variable with a Pareto distribution with parameters a and b for $a, b \in \R_{> 0}$. 
Then the moment generating function $M_X$ of $X$ is given by: 
:$\map {M_X} t = \begin {cases} a \paren {-b t}^a \map \Gamma {-a, -b t} & t < 0 \\ 1 & t = 0 \\ \text {does not exist} & t > 0 \end {cases}$

Proof:
From the definition of the Pareto distribution, $X$ has probability density function:
:$\map {f_X} x = \dfrac {a b^a} {x^{a + 1} }$
From the definition of a moment generating function:
:$\ds \map {M_X} t = \expect { e^{t X} } = \int_b^\infty e^{t x} \map {f_X} x \rd x$
First take $t < 0$. 
Then:
:$\ds \map {M_X} t = a b^a \int_b^\infty x^{-\paren {a + 1} } e^{t x} \rd x $
let:
{{begin-eqn}}
{{eqn | l = u
      | r = -t x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = -t
      | c = Derivative of Power
}}
{{end-eqn}}
Then: 
{{begin-eqn}}
{{eqn	| l = \map {M_X} t
        | r = -\dfrac {a b^a} t \int_{-bt}^\infty \paren {-\dfrac u t}^{-\paren {a + 1} } e^{-u} \rd u
	| c = 
}}
{{eqn	| r =  -\dfrac {a b^a} t \int_{-bt}^\infty \paren {-\dfrac 1 t}^{-\paren {a + 1} } u^{-\paren {a + 1} } e^{-u} \rd u
	| c = 
}}
{{eqn	| r =  a \paren {-b t}^a \int_{-bt}^\infty u^{-\paren {a + 1} } e^{-u} \rd u
	| c = 
}}
{{eqn	| r = a \paren {-b t}^a \map \Gamma {-a, -b t}
        | c = {{Defof|Gamma Distribution}}
}}
{{end-eqn}}
{{qed|lemma}}
Now take $t = 0$. 
Our integral becomes: 
{{begin-eqn}}
{{eqn 	| l = a b^a \int_b^\infty x^{-a - 1} \rd x
	| r = a b^a \bigintlimits {-\dfrac 1 {a x^a} } b \infty
	| c = Primitive of Power, Fundamental Theorem of Calculus
}}
{{eqn	| r = - b^a \lim_{x \mathop \to \infty} \dfrac 1 {x^a } - a b^a \paren {-\dfrac 1 {a b^a} }
        | c = 
}}
{{eqn	| o = \to
	| r = 1
	| c = since $a > 0$, $\dfrac 1 {x^a} \to 0$ as $x \mathop \to \infty$
}}
{{end-eqn}}
{{qed|lemma}}
Finally take $t > 0$.
Then:
{{begin-eqn}}
{{eqn	| l = \map {M_X} t
	| r = a b^a \int_b^\infty \dfrac {e^{t x} \rd x } {x^{a + 1} }
}}
{{eqn	| r = a b^a \paren {\bigintlimits {\dfrac {e^{t x} } {\paren {a + 1 - 1} x^{a + 1 - 1} } } b \infty + \frac {t} {a + 1 - 1} \int_b^\infty \frac {e^{t x} \rd x} {x^{a + 1 - 1} } }
	| c = Primitive of Exponential of a x over Power of x
}}
{{eqn	| o = \to
	| r = \infty
	| c = 
}}
{{end-eqn}}
As a consequence of Exponential Dominates Polynomial, we have:
:$x^a < e^{t x}$
for sufficiently large $x$. 
Therefore, in this case, the integrand increases without bound. 
We conclude that the integral is divergent.
Hence $\expect {e^{t X} }$ does not exist for $t > 0$. 
{{qed}}
Category:Moment Generating Functions
Category:Pareto Distribution
t0h5ejz16xpbmizkdoodhodngv20htd
Theorem: Skewness of Logistic Distribution

Let $X$ be a continuous random variable which satisfies the logistic distribution:
:$X \sim \map {\operatorname {Logistic} } {\mu, s}$
Then the skewness $\gamma_1$ of $X$ is equal to $0$.

Proof:
From Skewness in terms of Non-Central Moments, we have: 
:$\gamma_1 = \dfrac {\expect {X^3} - 3 \mu \sigma^2 - \mu^3} {\sigma^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}$ 
To calculate $\gamma_1$, we must calculate $\expect {X^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}' ' '} 0 = \mu^3 \int_{\to 0}^{\to 1} \rd u - 3 \mu^2 s \int_{\to 0}^{\to 1} \map \ln {\dfrac {1 - u} u} \rd u + 3 \mu s^2 \int_{\to 0}^{\to 1} \map {\ln^2} {\dfrac {1 - u} u} \rd u - s^3 \int_{\to 0}^{\to 1} \map {\ln^3} {\dfrac {1 - u} u} \rd u$
Therefore:
{{begin-eqn}}
{{eqn	| l = \expect {X^3}
	| r = \mu^3 - 3 \mu^2 s \paren {0} + 3 \mu s^2 \paren {\dfrac {\pi^2} 3} - s^3 \paren {0}
        | c = Variance of Logistic Distribution/Lemma 4 and Expectation of Logistic Distribution/Lemma 3
}}
{{eqn	| r = \mu^3 + \mu s^2 \pi^2
	| c = 
}}
{{end-eqn}}
So: 
{{begin-eqn}}
{{eqn	| l = \gamma_1
	| r = \frac {\mu^3 + \mu s^2 \pi^2 - 3 \mu \paren {\dfrac {s^2 \pi^2} 3} - \mu^3} {\paren {\dfrac {s \pi} {\sqrt 3} }^3}
}}
{{eqn	| r = 0
}}
{{end-eqn}}
{{qed}}
Category:Skewness
Category:Logistic Distribution
qf6pv187o7xqqfnwhqs6k65mt2gwkr1
Theorem: Antilexicographic Product on Pair of Well-Ordered Sets is Well-Ordered

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be well-ordered sets.
Let $S_1 \otimes^a S_2 = \struct {S_1 \times S_2, \preccurlyeq_a}$ be the antilexicographic product of $S_1$ and $S_2$.
Then $\struct {S_1 \times S_2, \preccurlyeq_a}$ is itself a well-ordered set.

Proof:
By definition, a well-ordered set is a totally ordered set which is well-founded.
From Antilexicographic Product of Totally Ordered Sets is Totally Ordered, we have that $\preccurlyeq_a$ is a totally ordered set.
It remains to be shown that $\preccurlyeq_a$ is a well-founded relation.
Let $T = S_1 \times S_2$.
Let $A$ be a non-empty subset of $T$.
Let $A_2$ be the set of all of the second cooordinates of the ordered pairs that comprise $A$:
:$A_2 = \set {b \in S_2: \tuple {a, b} \in A}$
We have that:
:$A_2$ is a non-empty subset of $S_2$
:$S_2$ is well-ordered by $\preccurlyeq_2$
Hence $A_2$ contains a minimal element $y$ by $\preccurlyeq_a$.
Let $A_y$ be the subset of $A$ in which the second cooordinate equals $y$.
:$A_y = \set {\tuple {a, b} \in A: b = y}$
Let $A_x$ be the set of first cooordinates of $A_y$.
:$A_x = \set {a \in S_1: \tuple {a, y} \in A}$
Then:
:$A_x$ is a non-empty subset of $S_1$
:$S_1$ is well-ordered by $\preccurlyeq_1$
So $A_x$ contains a minimal element $x$.
Thus we have constructed $\tuple {x, y}$, which is the minimal element of $A$ by $\preccurlyeq_a$.
As $A$ is arbitrary, it follows that every non-empty subset of $T$ has a minimal element by $\preccurlyeq_a$.
That is, $\preccurlyeq_a$ is a well-founded relation.
Hence, by definition, $T$ is well-ordered by $\preccurlyeq_a$.
{{qed}}
Theorem: Order Type Multiplication is Well-Defined Operation

The multiplication operation on order types is well-defined.

Proof:
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\struct {T_1, \preccurlyeq_{1'} }$ and $\struct {T_2, \preccurlyeq_{2'} }$ be ordered sets such that:
:$\struct {S_1, \preccurlyeq_1}$ is isomorphic to $\struct {T_1, \preccurlyeq_{1'} }$
:$\struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {T_2, \preccurlyeq_{2'} }$
Let $\alpha := \map \ot {S_1, \preccurlyeq_1}$ and $\beta := \map \ot {S_2, \preccurlyeq_2}$ denote the order types of $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ respectively.
Let $\alpha' := \map \ot {T_1, \preccurlyeq_{1'} }$ and $\beta' := \map \ot {T_2, \preccurlyeq_{2'} }$ denote the order types of $\struct {T_1, \preccurlyeq_{1'} }$ and $\struct {T_2, \preccurlyeq_{2'} }$ respectively.
It is required to show that:
:$\alpha \cdot \beta$
is the same as:
:$\alpha' \cdot \beta'$
We have that:
{{begin-eqn}}
{{eqn | l = \alpha \cdot \beta
      | r = \map \ot {\struct {S_1, \preccurlyeq_1} \otimes^a \struct {S_2, \preccurlyeq_2} }
      | c = 
}}
{{eqn | r = \map \ot {\struct {T_1, \preccurlyeq_{1'} } \otimes^a \struct {T_2, \preccurlyeq_{2'} } }
      | c = Order Isomorphism is Preserved by Antilexicographic Order
}}
{{eqn | r = \alpha' \cdot \beta'
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Order Isomorphism is Preserved by Antilexicographic Order

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\struct {T_1, \preccurlyeq_{1'} }$ and $\struct {T_2, \preccurlyeq_{2'} }$ be ordered sets such that:
:$\struct {S_1, \preccurlyeq_1}$ is isomorphic to $\struct {T_1, \preccurlyeq_{1'} }$
:$\struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {T_2, \preccurlyeq_{2'} }$
Then the antilexicographic order $\struct {S_1, \preccurlyeq_1} \otimes^a \struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {T_2, \preccurlyeq_{2'} } \otimes^a \struct {T_2, \preccurlyeq_{2'} }$.

Proof:
{{ProofWanted|tedious}}
Theorem: Order Type Addition is Associative

Let $\alpha$, $\beta$ and $\gamma$ be order types of ordered sets.
Then:
:$\paren {\alpha + \beta} + \gamma = \alpha + \paren {\beta + \gamma}$
where $+$ denotes order type addition.

Proof:
Let $\struct {S_1, \preccurlyeq_1}$, $\struct {S_2, \preccurlyeq_2}$ and $\struct {S_3, \preccurlyeq_3}$ be ordered structures such that:
{{begin-eqn}}
{{eqn | l = \map \ot {S_1, \preccurlyeq_1}
      | r = \alpha
}}
{{eqn | l = \map \ot {S_2, \preccurlyeq_2}
      | r = \beta
}}
{{eqn | l = \map \ot {S_3, \preccurlyeq_3}
      | r = \gamma
}}
{{end-eqn}}
where $\ot$ denotes order type.
Thus by definition of order type we are required to show that:
:$\paren {\struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2} } \oplus \struct {S_3, \preccurlyeq_3} \cong \struct {S_1, \preccurlyeq_1} \oplus \paren {\struct {S_2, \preccurlyeq_2} \oplus \struct {S_3, \preccurlyeq_3} }$
where:
:$\oplus$ denotes order sum
:$\cong$ denotes order isomorphism.
Let:
{{begin-eqn}}
{{eqn | l = \struct {T_a, \preccurlyeq_a}
      | o = :=
      | r = \struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2}
}}
{{eqn | r = \struct {S_1 \times S_2, \preccurlyeq_a}
}}
{{eqn | l = \struct {T_b, \preccurlyeq_b}
      | o = :=
      | r = \struct {S_2, \preccurlyeq_2} \oplus \struct {S_3, \preccurlyeq_3}
}}
{{eqn | r = \struct {S_2 \times S_3, \preccurlyeq_b}
}}
{{end-eqn}}
{{ProofWanted|this is daunting}}