nLab
one-sided real number

One-sided real numbers

Summary

There are really two notions of one-sided real number: lower reals and upper reals. But there is a nearly perfect symmetry between them (although the lower reals seem to get slightly more use).

These are largely concepts in constructive mathematics. Using excluded middle, a bounded one-sided real number is simply a real number, but constructively they are more general (and less well behaved). Lower reals are particularly important in constructive measure theory as the values taken by positive measures (and more generally are used to define extended positive cones).

However, even in classical mathematics, there are some differences, at least in emphasis and application. First, it is most natural to include \infty as a lower real and include -\infty as an upper real. (However, you can restrict to bounded lower/upper reals to avoid that, or alternatively genralise to extended lower/upper reals if you want to include both ±\pm\infty at once.) Also, the natural topology on the lower reals is the lower semicontinuous topology (and the natural topology on the upper reals is the upper semicontinuous topology).

One-sided numbers are sometimes called (upper or lower) semicontinuous numbers. To see why, consider a locale (or topological space) LL, and consider the (upper or lower) semicontinuous functions (real-valued) on LL. On the one hand, these are the same as the continuous functions from LL to (classically) the set of real numbers equipped with the semicontinuous topology or to (constructively) a locale whose points are the one-sided real numbers. On the other hand, these semicontinuous functions are precisely the internal one-sided real numbers in the topos of sheaves over LL.

Lower and upper reals don't interact well together; for a system that naturally includes both (and, constructively, much more), use the MacNeille real numbers.

Idea

(In the following, ‘number’ without qualification may be taken to mean either a real number or a rational number; the result is the same either way. Indeed, we could take any dense set of real numbers.)

A lower real number is the supremum of an inhabited set of numbers. A bounded lower real is the supremum of an inhabited set of numbers that has a finite upper bound. An extended lower real is the supremum of an arbitrary set of numbers.

An upper real number is the infimum of an inhabited set of numbers. A bounded upper real is the infimum of an inhabited set of numbers that has a finite lower bound. An extended lower real is the infimum of an arbitrary set of numbers.

We cannot generalize further by taking more extrema of the same sort. Explicitly, the supremum of any inhabited set of lower reals is a lower real and the infimum of any inhabited set of upper reals is an upper real. (Similar results obtain if we use either bounded or extended reals, so long as we also either require the set to bounded or allow it to be empty.) However, mixing extrema takes us further to the MacNeille real numbers.

Definitions

There are some choices as to how exactly to represent one-sided real numbers; we will define them here as certain subsets of the set \mathbb{Q} of rational numbers. If we replaced \mathbb{Q} with any other dense subset of the real line, then the definitions would end up being equivalent.

Lower reals

An extended lower real number is any subset LL of \mathbb{Q} such that

  • if aLa \in L, then a<ba \lt b for some bLb \in L; and
  • if a<ba \lt b and bLb \in L, then aLa \in L.

We can actually combine these into a single rule:

  • aLa \in L if and only if a<ba \lt b for some bLb \in L.

A lower real number is an extended lower real LL such that:

  • some aLa \in L.

A bounded lower real number is a lower real LL such that

  • some bLb \notin L.

When treated explicitly as a subset of \mathbb{Q}, we call LL a lower set. When we interpret LL as a one-sided real number xx, we write a<xa \lt x to mean that aLa \in L. Conversely, we can interpret any rational number, or even any real number, xx as a bounded lower real, specifically as the set of all rational numbers less than xx. (A bounded lower real is located if it is the lower real obtained in this way from a real number; classically, every bounded lower real number is located.) We interpret \infty as the lower real whose lower set is all of \mathbb{Q}; we interpret -\infty as the extended lower real whose lower set is empty.

Upper reals

An extended upper real number is any subset UU of \mathbb{Q} such that

  • if bUb \in U, then a<ba \lt b for some aUa \in U; and
  • if a<ba \lt b and aUa \in U, then bUb \in U.

We can actually combine these into a single rule:

  • bUb \in U if and only if a<ba \lt b for some aUa \in U.

An upper real number is an extended upper real UU such that:

  • some bUb \in U.

A bounded upper real number is an upper real UU such that

  • some aUa \notin U.

When treated explicitly as a subset of \mathbb{Q}, we call UU an upper set. When we interpret UU as a one-sided real number xx, we write x<bx \lt b to mean that bUb \in U. Conversely, we can interpret any rational number, or even any real number, xx as a bounded upper real, specifically as the set of all rational numbers greater than xx. (A bounded upper real is located if it is the upper real obtained in this way from a real number; classically, every bounded upper real number is located.) We interpret -\infty as the upper real whose upper set is all of \mathbb{Q}; we interpret \infty as the extended upper real whose upper set is empty.

Order relations

We define order relations between extended lower reals xx and yy as follows:

  • x<yx \lt y if and only if there exists a rational number aa such that a<ya \lt y but not a<xa \lt x;
  • xyx \leq y if and only if a<ya \lt y for every rational number aa such that a<xa \lt x.

In other words, \leq is \subseteq on lower sets, and <\lt is \subsetneq (in an appropriate sense).

We define order relations between extended upper reals xx and yy as follows:

  • x<yx \lt y if and only if there exists a rational number bb such that x<bx \lt b but not y<by \lt b;
  • xyx \leq y if and only if x<bx \lt b for every rational number bb such that y<by \lt b.

In other words, \leq is \supseteq on upper sets, and <\lt is \supsetneq.

We now have multiple meanings for x<yx \lt y or xyx \leq y if one or both of these is already a rational number or a real number, but it is a theorem that the meanings are all consistent. We also have x-\infty \leq x \leq \infty for every extended number xx, and <x<-\infty \lt x \lt \infty for every bounded number xx. Finally, xyx \leq y if x<yx \lt y or x=yx = y; the converse holds classically.

Each version of \leq is a partial order and each version of <\lt is a quasiorder. By excluded middle, \leq is a total order and <\lt is the corresponding linear order, but neither of these results holds constructively. In particular, the comparison law for <\lt is invalid, which is why one-sided reals are not as well behaved as ordinary (located) real numbers.

Suprema and infima

Given any collection of extended lower reals, their supremum is an extended lower real which is found by taking the union of lower sets. The supremum of an inhabited set of lower reals is a lower real, and the supremum of an inhabited set of bounded lower reals is bounded iff the set has a bounded lower real as an upper bound. In any case, this supremum really is the supremum under \leq. This agrees with the notion of supremum of real numbers in the real number system, when that exists. Every extended lower real is also the supremum in this sense of its corresponding lower set, interpreted as a set of lower reals that happen to all be rational numbers.

Given any collection of extended upper reals, their infimum is an extended upper real which is found by taking the union of upper sets. The infimum of an inhabited set of upper reals is an upper real, and the infimum of an inhabited set of bounded upper reals is bounded iff the set has a bounded upper real as a lower bound. In any case, this infimum really is the infimum under \leq. This agrees with the notion of infimum of real numbers in the real number system, when that exists. Every extended upper real is also the infimum in this sense of its corresponding upper set, interpreted as a set of upper reals that happen to all be rational numbers.

Constructively, we cannot necessarily take the infimum of a set of lower reals, nor the supremum of a set of upper reals. We can, however, interpret such a supremum or infimum as a MacNeille real number.

Arithmetic

In general, you can extend order-preserving functions of rational numbers to lower reals and to upper reals; you simply take the image of the lower or upper set and close it downward or upwards, as appropriate. If you have an order-reversing function of rational numbers, then you can apply it to a lower real to get an upper real and conversely; this is about the only interaction that I know of between the two kinds of one-sided real.

Since addition is order-preserving, it works nicely, at least to make a monoid; but subtraction doesn't work in general. Multiplication has trouble with negative numbers but produces good results if you restrict to [0,][0,\infty]. Notice that we get 0=00 \cdot \infty = 0 with lower reals but 0=0 \cdot \infty = \infty with extended upper reals; thus, [0,[{[{0,\infty}[} is a rig for either lower or upper reals, while [0,][0,\infty] is a rig only for lower reals. (This doesn't so much mean that upper reals behave worse than lower reals, as that extended reals on either side behave worse.) We can also use logarithms to translate between addition and multiplication. (In particular, +=-\infty + \infty = -\infty with extended lower reals but +=-\infty + \infty = \infty with extended upper reals.)

Of course, arithmetic with one-sided real numbers is much easier than this in classical mathematics, where the bounded or extended versions may be identified; but even there, the natural operations involving ±\pm\infty may differ. Accordingly, the conventions for arithmetic with infinities can signal which sort of number is appropriate for a constructive development.

If you really want to do arbitrary arithmetic operations constructively on upper or lower reals, then again you need their common generalisation, the MacNeille reals.

Topology

Let's put this on a separate page: semicontinuous topology. For one thing, it's more advanced than the elementary stuff above; for another thing, it's more interesting in classical mathematics; and finally, it's more complicated in constructive mathematics. The main point is that each type of one-sided real number has its own natural topology, and these differ (both classically and constructively) from the usual topology on the real line.

In topos theory

There is a bijective correspondence of internal extended lower real numbers in a sheaf topos Sh(X)\mathrm{Sh}(X) of a topological space XX and lower semicontinuous functions X{+}X \to \mathbb{R} \cup \{ +\infty \}, or equivalently a continuous function X{+}X \to \mathbb{R} \cup \{ +\infty \}, when the latter is equipped with the lower semicontinuous topology. (We will work classically in the external logic.)

Let Δ()\Delta(\mathbb{Q}) denote the constant sheaf of rational numbers on XX. A lower real number UU in Sh(X)\mathrm{Sh}(X) is then defined as a subsheaf of Δ()\Delta(\mathbb{Q}) satisfying the axioms above (interpreted in the internal language). Such a lower real number induces a lower semicontinuous function xsupU xx \mapsto \sup U_x, where U xU_x denotes the stalk of UU at xx (taken as a subset of \mathbb{Q}).

Conversely, a lower semicontinuous function f:X{+}f : X \to \mathbb{R} \cup \{ +\infty \} defines an internal lower real number UU with sections

U(A){φ:A|xA:φ(x)<f(x)}Δ()(A)U(A) \coloneqq \{ \varphi : A \to \mathbb{Q} | \forall x \in A: \varphi(x) \lt f(x) \} \subseteq \Delta(\mathbb{Q})(A)

over open sets AXA \subseteq X.

See Mulvey (1974, page 28) for details.

For the externally constructive version of this, it is best to take XX to be a locale; we need to use the (external) locale LL of lower real numbers in place of {}\mathbb{R} \cup \{\infty\}, and the notion of semicontinuous map is replaced with a continuous map (in the sense of locales) to LL.

References

  • C. Mulvey (1974): Intuitionistic Algebra and Representations of Rings. In Hofmann, Liukkonen: Recent Advances in the Representation Theory of Rings and C*-Algebras by Continuous Sections, AMS 1974.

Revised on September 24, 2013 11:51:48 by Toby Bartels (98.23.150.36)