Upper Bound of Ordinal Sum

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x$ and $y$ be ordinals.

Suppose $x > 1$.

Let $\sequence {a_n}$ be a finite sequence of ordinals such that:

$a_n < x$ for all $n$

Let $\sequence {b_n}$ be a strictly decreasing finite sequence of ordinals such that:

$b_n < y$ for all $n$


Then:

$\ds \sum_{i \mathop = 1}^n x^{b_i} a_i < x^y$


Proof

The proof shall proceed by finite induction on $n$:

For all $n \in \N_{\ge 0}$, let $\map P n$ be the proposition:

$\ds \sum_{i \mathop = 1}^n x^{b_i} a_i < x^y$


Basis for the Induction

$\map P 0$ says that:
$\ds \sum_{i \mathop = 1}^0 x^{b_i} a_i < x^y$
\(\ds \sum_{i \mathop = 1}^0 x^{b_i} a_i\) \(=\) \(\ds 0\) Definition of Ordinal Sum
\(\ds \) \(<\) \(\ds x^y\) Exponent Not Equal to Zero

This is our basis for the induction.

$\Box$


Induction Hypothesis

Now we need to show that, if $\map P k$ is true, where $k \ge 0$, then it logically follows that $\map P {k + 1}$ is true.


So this is our induction hypothesis:

$\ds \sum_{i \mathop = 1}^k x^{b_i} a_i < x^y$


Then we need to show:

$\ds \sum_{i \mathop = 1}^{k \mathop + 1} x^{b_i} a_i < x^y$


Induction Step

This is our induction step:


By the inductive hypothesis:

$\ds \sum_{i \mathop = 1}^k x^{b_{i + 1}} a_{i + 1} < x^{b_1}$ since $b_1$ is greater than all $b_i$ for $i > 1$.

Then:

\(\ds \sum_{i \mathop = 1}^{k + 1} x^{b_i} a_i\) \(=\) \(\ds x^{b_1} a_1 + \sum_{i \mathop = 1}^k x^{b_{i + 1} } a_{i + 1}\) General Associative Law for Ordinal Sum
\(\ds \) \(<\) \(\ds x^{b_1} a_1 + x^{b_1}\) Membership is Left Compatible with Ordinal Addition
\(\ds \) \(=\) \(\ds x^{b_1} a_1^+\) Ordinal Multiplication is Left Distributive
\(\ds \) \(\le\) \(\ds x^{b_1^+}\) Membership is Left Compatible with Ordinal Multiplication and Successor of Element of Ordinal is Subset
\(\ds \) \(\le\) \(\ds x^y\) Membership is Left Compatible with Ordinal Exponentiation and Successor of Element of Ordinal is Subset


This article, or a section of it, needs explaining.
In particular: In the above, particularly the last couple of lines, it is not clear how the results invoked correspond to the operations performed. In any case, it is worth expanding those steps out to show how the individual steps are performed. ProofWiki prefers to perform steps individually.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Explain}} from the code.


So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.


Therefore:

$\ds \sum_{i \mathop = 1}^n a_i x^{b_i} < x^y$

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Upper_Bound_of_Ordinal_Sum&oldid=512458"