description/proof of that for sequence on linearly-ordered set, limit superior is independent of leading finite elements
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of linearly-ordered set.
- The reader knows a definition of limit superior of sequence on partially-ordered set.
- The reader admits the proposition that for any linearly-ordered set, any nonempty finite subset has the maximum and the minimum.
Target Context
- The reader will have a description and a proof of the proposition that for any sequence on any linearly-ordered set, the limit superior is independent of any leading finite elements.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(J\): \(\subseteq \mathbb{N}\), such that \(J \neq \emptyset\)
\(S\): \(\in \{\text{ the linearly-ordered sets }\}\) with any linear ordering, \(\lt\)
\(s\): \(: J \to S\)
\(s'\): \(: J \to S\)
//
Statements:
\(\exists N \in \mathbb{N} \setminus \{0\} \text{ such that } N \lt \vert J \vert (\forall n \in \mathbb{N} \setminus \{0\} \text{ such that } N \lt n (s (J_n) = s' (J_n)))\)
\(\implies\)
(
\(\lnot \exists lim sup s \iff \lnot \exists lim sup s'\)
\(\land\)
\((\exists lim sup s \lor \exists lim sup s') \implies lim sup s = lim sup s'\)
)
//
2: Proof
Whole Strategy: Step 0: definite \(t_m := Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\) and \(t'_m := Sup (\{s' (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\) and see that \(t_{m'} \le t_m\) and \(t'_{m'} \le t'_m\) for each \(m \lt m'\); Step 1: deal with the case that \(J\) is finite, and suppose otherwise, thereafter; Step 2: suppose that \(lim sup s\) does not exist; Step 3: see that \(lim sup s'\) does not exist; Step 4: see that if \(lim sup s'\) does not exist, \(lim sup s\) does not exist; Step 5: conclude the proposition.
Step 0:
Let us define \(t_m := Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\) and \(t'_m := Sup (\{s' (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\).
Let \(m, m' \in \mathbb{N} \setminus \{0\}\) be any such that \(m \lt m'\).
Let us see that if \(t_{m'}\) exists, \(t_m\) exists and \(t_{m'} \le t_m\).
Let us suppose that \(t_{m'}\) exists.
\(t_m = Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\} \cup \{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m' \le n\})\).
\(Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\})\) exists, by the proposition that for any linearly-ordered set, any nonempty finite subset has the maximum and the minimum.
When \(t_{m'} \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\})\), \(t_m = Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\})\), because for each \(m \le n \lt m'\), \(s (J_n) \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\})\), and for each \(m' \le n\), \(s (J_n) \le t_{m'} \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\})\), so, \(Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\}) \in Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\), and if there was a \(u \in Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\) such that \(u \lt Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\})\), \(u \lt s (J_n)\) for an \(m \le n \lt m'\), a contradiction against that \(u\) was in the set of the upper bounds, so, \(Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\}) = Min (Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})) = t_m\).
When \(Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\}) \lt t_{m'}\), \(t_m = t_{m'}\), because for each \(m \le n \lt m'\), \(s (J_n) \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\}) \le t_{m'}\), and for each \(m' \le n\), \(s (J_n) \le t_{m'}\), so, \(t_{m'} \in Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\), and if there was a \(u \in Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\) such that \(u \lt t_{m'}\), \(u \in Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m' \le n\})\), a contradiction against that \(t_{m'}\) was the minimum of the set of the upper bounds, so, \(t'_m = Min (Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})) = t_m\).
So, \(t_m\) exists anyway.
Let us see that \(t_{m'} \le t_m\).
As has been seen above, when \(t_{m'} \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\})\), \(t_{m'} \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\}) = t_m\); when \(Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n \lt m'\}) \lt t_{m'}\), \(t_{m'} = t_m \le t_m\).
So, anyway, \(t_{m'} \le t_m\).
As an aside, if \(t_m\) exists, \(t_{m'}\) may not exist, because for example, for \(S = \mathbb{Q}\), when \(t_{m'}\) does not exist as a sequence asymptotic to \(\sqrt{2}\), \(t_m\) can exist by \(s (J_m) = 2\).
Step 1:
When \(\vert J \vert = n \in \mathbb{N} \setminus \{0\}\), \(lim sup s = s (J_n)\) and \(lim sup s' = s' (J_n)\) exist, and as \(s (J_n) = s' (J_n)\), \(lim sup s = lim sup s'\).
Let us suppose otherwise, hereafter.
Step 2:
Let us suppose that \(lim sup s\) does not exist, which means that \(t_m\) does not exist for an \(m \in \mathbb{N} \setminus \{0\}\) or \(t_m\) exists for each \(m \in \mathbb{N} \setminus \{0\}\) but \(Inf (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\})\) does not exist.
Step 3:
Let us suppose that \(t_m\) does not exist for an \(m \in \mathbb{N} \setminus \{0\}\).
When \(N \lt m\), \(\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\} = \{s' (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}\), so, also \(t'_m\) does not exist, so, \(lim sup s'\) does not exist.
Let us suppose that \(m \le N\).
By Step 0, if \(t_{N + 1}\) existed, \(t_m\) would exist, so, \(t_{N + 1}\) does not exist.
But as \(t'_{N + 1} = t_{N + 1}\), \(t'_{N + 1}\) does not exist.
So, \(lim sup s'\) does not exist.
Let us suppose that \(t_m\) exists for each \(m \in \mathbb{N} \setminus \{0\}\) but \(Inf (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\})\) does not exist.
Let us see that \(Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\}) = Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\})\).
For each \(u \in Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\})\), \(u \le t_m\) for each \(m \in \mathbb{N} \setminus \{0\}\), so, especially for each \(m \in \mathbb{N} \setminus \{0\}\) such that \(N + 1 \le m\), which means that \(u \in Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\})\).
For each \(u \in Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\})\), \(u \le t_m\) for each \(m \in \mathbb{N} \setminus \{0\}\) such that \(N + 1 \le m\), but by Step 0, for each \(m \in \mathbb{N} \setminus \{0\}\) such that \(m \le N\), \(u \le t_{N + 1} \le t_m\), so, \(u \le t_m\) for each \(m \in \mathbb{N} \setminus \{0\}\), which means that \(u \in Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\})\).
So, as \(Inf (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\}) = Max (Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\}))\) does not exist, \(Max (Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\}))\) does not exist.
But as \(\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\} = \{t'_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\}\), \(Inf (\{t'_m \vert m \in \mathbb{N} \setminus \{0\}\}) = Max (Lb (\{t'_m \vert m \in \mathbb{N} \setminus \{0\}\})) = Max (Lb (\{t'_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\}))\) does not exist.
So, \(lim sup s'\) does not exist.
Step 4:
Symmetrically, if \(lim sup s'\) does not exist, \(lim sup s\) does not exist.
Step 5:
Let us suppose that \(lim sup s\) exists.
As has been seen in Step 3, \(Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\}) = Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\})\).
So, \(lim sup s = Inf (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\}) = Max (Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\})) = Max (Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\})) = Max (Lb (\{t'_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\})) = Max (Lb (\{t'_m \vert m \in \mathbb{N} \setminus \{0\}\})) = Inf (\{t'_m \vert m \in \mathbb{N} \setminus \{0\}\}) = lim sup s'\).
When \(lim sup s'\) exists, symmetrically, \(lim sup s = lim sup s'\).
