2 Orders of magnitude
The hyperreals \({}^* {\mathbb R}\) are already defined in Mathlib, using a Lean-canonically chosen ultrafilter on \({\mathbb N}\). One could consider generalizing the hyperreal construction to other filters or ultrafilters, but given the extensive library support for the Mathlib hyperreals, and the fact that it already enjoys enough of a transfer principle for most applications, we will base our theory here on the Mathlib hyperreals.
The positive hyperreals \({}^* {\mathbb R}^+\) are the set of hyperreals \(X \in {}^* {\mathbb R}\) such that \(X {\gt} 0\). (Note that \(X\) could be infinitesimal or infinite).
If \(X,Y\) are positive hyperreals, we write \(X \lesssim Y\) if \(X \leq CY\) for some real \(C{\gt}0\). We write \(X \asymp Y\) if \(X \lesssim Y \lesssim X\). We write \(X \ll Y\) if \(X \leq \varepsilon Y\) for all real \(\varepsilon {\gt}0\).
\(\lesssim \) is a pre-order on \({}^* {\mathbb R}^+\), with \(\asymp \) the associated equivalence relation, and \(\ll \) the associated strict order. Any two positive hyperreals are comparable under \(\lesssim \).
Easy.
The space \(\O \) of orders of magnitude is defined to be the quotient space \({}^* {\mathbb R}^+ / \asymp \) of the positive hyperreals by the relation of asymptotic equivalence. For a positive hyperreal \(X\), we let \(\Theta (X)\) denote the order of magnitude of \(X\); this is a surjection from \({}^* {\mathbb R}^+\) to \(\O \).
For positive hyperreals \(X,Y\), we have \(\Theta (X) = \Theta (Y)\) if and only if \(X \asymp Y\). Similarly, we have \(\Theta (X) {\lt} \Theta (Y)\) if and only if \(X \ll Y\), and \(\Theta (X) \leq \Theta (Y)\) if and only if \(X \lesssim Y\).
Easy.
We linearly order \(\O \) by the requirement that \(\Theta (X) \leq \Theta (Y)\) if and only if \(X \lesssim Y\), and \(\Theta (X) {\lt} \Theta (Y)\) if and only if \(X \ll Y\).
We define \(1 := \Theta (1)\).
We have \(\Theta (C) = 1\) for all real \(C{\gt}0\).
Easy.
We define addition on \(\O \) by the requirement that \(\Theta (X) + \Theta (Y) = \Theta (X+Y)\) for positive hyperreals \(X,Y\). Similarly we define multiplication, inverse, and division. We define real exponentiation by requiring that \(\Theta (X^\alpha ) = \Theta (X)^\alpha \) for positive hyperreals \(X\) and real \(\alpha \).
For all orders of magnitude \(\Theta (X), \Theta (Y)\), we have \(\Theta (X) + \Theta (Y) = \max (\Theta (X), \Theta (Y))\).
Easy.
\(\O \) is an ordered additive idempotent commutative monoid.
Easy.
\(\O \) is a multiplicative ordered commutative group that distributes over addition. (It is not a semiring in the Mathlib sense because it does not have a zero element.)
Easy.
Let \(\Theta (X), \Theta (Y)\) be orders of magnitude, and \(\alpha ,\beta \) be real numbers.
We have \(\Theta (XY)^\alpha = \Theta (X^\alpha Y^\alpha )\) and \(\Theta (X/Y)^\alpha = \Theta (X^\alpha / Y^\alpha )\).
We have \(\Theta (X^{\alpha \beta }) = \Theta (X^\alpha )^\beta \).
We have \(\Theta (X)^0 = 1\), \(\Theta (X)^1 = \Theta (X)\), and \(\Theta (X)^{-1} = 1 / \Theta (X)\).
We have \(\Theta (1)^\alpha = 1\).
We have \(\Theta (X+Y)^\alpha = \Theta (X)^\alpha + \Theta (Y)^\alpha \) for \(\alpha \geq 0\).
If \(\alpha \geq 0\) and \(\Theta (X) \leq \Theta (Y)\), then \(\Theta (X)^\alpha \leq \Theta (Y)^\alpha \).
If \(\alpha {\gt} 0\), then \(\Theta (X) \leq \Theta (Y)\), if and only if \(\Theta (X)^\alpha \leq \Theta (Y)^\alpha \), and \(\Theta (X) {\lt} \Theta (Y)\) if and only if \(\Theta (X)^\alpha {\lt} \Theta (Y)^\alpha \).
If \(\alpha \leq 0\) and \(\Theta (X) \leq \Theta (Y)\), then \(\Theta (X)^\alpha \geq \Theta (Y)^\alpha \).
If \(\alpha {\lt} 0\), then \(\Theta (X) \leq \Theta (Y)\), if and only if \(\Theta (X)^\alpha \geq \Theta (Y)^\alpha \), and \(\Theta (X) {\lt} \Theta (Y)\) if and only if \(\Theta (X)^\alpha {\gt} \Theta (Y)^\alpha \).
Straightforward.
We define \(\log \O \) to be the collection of formal logarithms of magnitude \(\log (\Theta (X))\) of orders of magnitude \(\Theta (X)\). \(1\), multiplication, and exponentiation of orders of magnitude become \(0\), addition, and scalar multiplication; and order is preserved. By definition, \(\log \colon \O \to \log \O \) is a order isomorphism.
For orders of magnitude \(\Theta (X), \Theta (Y)\), we have \(\log (\Theta (X) + \Theta (Y)) = \max (\log (\Theta (X)), \log (\Theta (Y)))\).
Immediate from Lemma 9.
For orders of magnitude \(\Theta (X), \Theta (Y)\), we have \(\log (1) = 0\) (and more generally \(\log (C) = 0\) for any real \(C{\gt}0\)), \(\log (\Theta (X) \Theta (Y)) = \log (\Theta (X)) + \log (\Theta (Y))\), and \(\log (\Theta (X) / \Theta (Y)) = \log (\Theta (X)) - \log (\Theta (Y))\). For any real \(\alpha \), we have \(\log (\Theta (X)^\alpha ) = \alpha \log (\Theta (X))\).
\(\log \O \) is a linearly ordered real vector space.
Straightforward from Lemma 15.
Let \(I_1 \supset I_2 \supset \dots \) be a sequence of internal sets in the hyperreals. If each of the \(I_n\) is non-empty, then \(\bigcap _{n=1}^\infty I_n\) is non-empty.
Write each \(I_n\) as an ultraproduct of \(I_{n,m}\). Then, we can find a nested sequence \(E_1 \supset E_2 \supset \dots \) of large sets in the ultrafilter such that \(\bigcap _{n \leq n_0} I_{n,m}\) is non-empty for all \(m \in E_{n_0}\) and all \(n_0\), and also \(n_0 \not\in E_{n_0}\). If we then pick \(x_m\) to lie in \(\bigcap _{n \leq n_0} E_{n,m}\) where \(n_0\) is the largest number for which \(m \in E_{n_0}\), the ultralimit of the \(x_m\) will have the required properties.
Let \(I_1 \supset I_2 \supset \dots \) be a decreasing sequence of non-empty open intervals (possibly unbounded) in \(\O \). Then \(\bigcap _{n=1}^\infty I_n\) is non-empty.
Pull back each of the \(I_n\) to the hyperreals as a countable intersection of internal sets, and apply Lemma 17.
Let \(I_1 \supset I_2 \supset \dots \) be a decreasing sequence of non-empty intervals (possibly unbounded or closed) in \(\O \). Then \(\bigcap _{n=1}^\infty I_n\) is non-empty.
If one of the \(I_n\) is a singleton, the claim is straightforward. Otherwise, replace each \(I_n\) by its interior and use Lemma 18.