- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
\(\O \) is an ordered additive idempotent commutative monoid.
\(\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.)
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.
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.
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))\).
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.
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 \).
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 \).
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\).
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 \).
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\).