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 perfect symmetry between them.

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 as a lower real and include 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 ± 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 often called (upper or lower) semicontinuous numbers. To see why, consider a locale (or topological space) L, and consider the (upper or lower) semicontinuous functions (real-valued) on L. On the one hand, these are the same as the continuous functions from L 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 L.

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

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 real 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 generalise 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 number?s.

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 of rational numbers.

Lower reals

An extended lower real number is any subset L of such that

  • if aL, then a<b for some bL; and
  • if a<b and bL, then aL.

We can actually combine these into a single rule:

  • aL if and only if a<b for some bL.

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

  • some aL.

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

  • some bL.

When treated explicitly as a subset of , we call L a lower set. When we interpret L as a number x, we write a<x to mean that aL. Conversely, we can interpret any rational number, or even any real number, x as a bounded lower real, specifically as the set of all rational numbers less than x. We interpret as the lower real whose lower set is all of ; we interpret as the extended lower real whose lower set is empty.

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.

Upper reals

An extended upper real number is any subset U of such that

  • if bU, then a<b for some aU; and
  • if a<b and aU, then bU.

We can actually combine these into a single rule:

  • bU if and only if a<b for some aU.

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

  • some bU.

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

  • some aU.

When treated explicitly as a subset of , we call U an upper set. When we interpret U as a number x, we write x<b to mean that bU. Conversely, we can interpret any rational number, or even any real number, x as a bounded upper real, specifically as the set of all rational numbers greater than x. We interpret as the upper real whose upper set is all of ; we interpret as the extended upper real whose upper set is empty.

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.

Order relations

We define order relations between extended lower reals x and y as follows:

  • x<y if and only if there exists a rational number a such that a<y but not a<x;
  • xy if and only if a<y for every rational number a such that a<x.

In other words, is on lower sets, and < is (in an appropriate sense).

We define order relations between extended upper reals x and y as follows:

  • x<y if and only if there exists a rational number b such that x<b but not y<b;
  • xy if and only if x<b for every rational number b such that y<b.

In other words, is on upper sets, and < is .

We now have multiple meanings for x<y or xy 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 for every extended number x, and <x< for every bounded number x. Finally, xy if x<y.

Each version of is a partial order and each version of < is a quasiorder. By excluded middle, is a total order and < is the corresponding linear order, but neither of these results holds constructively. In particular, the comparison law for < is invalid, which is why one-sided reals are not as well behaved as ordinary (located Dedekind) 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 . 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 . 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,]. Notice that we get 0=0 with lower reals but 0= with extended upper reals; thus, [0,[ is a rig for either lower or upper reals, while [0,] 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, += with extended lower reals but += with extended upper reals.)

If you really want to do arbitrary arithmetic operations 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. (Also, we haven't written it yet.)

In topos theory

There is a bijective correspondence of internal extended lower real numbers in a sheaf topos Sh(X) of a topological space X and upper semicontinuous functions X{+}:

Let Δ() denote the constant sheaf of rational numbers on X. A lower real number U in Sh(X) is then defined as a subsheaf of Δ() satisfying the axioms above (interpreted in the internal language). Such a lower real number induces an upper semicontinuous function xinfU x, where U x denotes the stalk of U at x (taken as a subset of ).

Conversely, an upper semicontinuous function f:X{+} defines an internal lower real number U with sections

U(A){φ:AxA:φ(x)>f(x)}Δ()(A)U(A) \coloneqq \{ \varphi : A \to \mathbb{Q} | \forall x \in A: \varphi(x) \gt f(x) \} \subseteq \Delta(\mathbb{Q})(A)

over open sets AX.

See C. Mulvey, 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 for details (page 28).

Revised on February 8, 2013 20:14:16 by Ingo Blechschmidt (137.250.162.16)