1.1  Floor and Ceiling

The functions fl and cg, known as the floor and ceiling, respectively, are approximations of reals by integers. The floor is also known as the greatest integer function, because the value of $ fl(x)$ may be characterized as the greatest integer not exceeding $ x$:1.1

Definition 1.1.1   (fl-def) For each $ x \in \mathbb{R}$, $ fl(x)$ is the unique integer that satisifies

$\displaystyle fl(x) \leq x < fl(x) + 1.$

Notation: We shall abbreviate $ fl(x)$ as $ \lfloor x \rfloor$.

The equality in Definition 1.1.1 holds if and only if $ x$ is an integer:

  (fl-integerp) For all $ x \in \mathbb{R}$, $ \lfloor x \rfloor = x \Leftrightarrow x \in \mathbb{Z}$.

PROOF: If $ \lfloor x \rfloor = x$, then $ x \in \mathbb{Z}$ by Definition 1.1.1. On the other hand, if $ x \in \mathbb{Z}$, then since $ \lfloor x \rfloor$ is the unique integer in the half-open interval $ [\lfloor x \rfloor, \lfloor x \rfloor + 1)$, Definition 1.1.1 implies $ \lfloor x \rfloor = x.$ 

Monotonicity is an immediate consequence of the definition:

  (fl-monotone-linear) If $ x \in \mathbb{R}$, $ y \in \mathbb{R}$, and $ x \leq y$, then $ \lfloor x \rfloor \leq \lfloor y \rfloor$.

PROOF: If $ x \leq y$, then Definition 1.1.1 implies $ \lfloor x \rfloor \leq y$. By a second application of the same lemma, $ y < \lfloor y \rfloor + 1$. Hence, $ \lfloor x \rfloor < \lfloor y \rfloor + 1$, and the result follows from Definition 1.1.1

  (n<=fl-linear) Let $ x \in \mathbb{R}$, $ n \in \mathbb{Z}$, and $ n \leq x$, then $ n \leq \lfloor x \rfloor$.

PROOF: By Definition 1.1.1 and Lemma 1.1.2, $ n = \lfloor n \rfloor \leq \lfloor x \rfloor$


The following two lemmas are rewrite rules to be used in the simplification of floor expressions.

  (fl+int-rewrite) If $ x \in \mathbb{R}$ and $ n \in \mathbb{Z}$, then $ \lfloor x+n \rfloor = \lfloor x \rfloor + n$.

PROOF: Applying Definition 1.1.1 and shifting by $ n$, we have $ \lfloor x \rfloor + n \leq x + n < \lfloor x \rfloor + n + 1$. The result now follows from Definition 1.1.1

  (fl/int-rewrite) If $ x \in \mathbb{R}$, $ n \in \mathbb{Z}$, and $ n > 0$, then $ \lfloor \lfloor x \rfloor /n \rfloor = \lfloor x/n \rfloor$.

PROOF: Since $ \lfloor x \rfloor \leq x$, $ \lfloor x \rfloor/n \leq x/n$, and by Lemma 1.1.2, $ \lfloor \lfloor x \rfloor/n \rfloor \leq \lfloor x/n \rfloor$. To derive the reverse inequality, note that since $ x/n \geq \lfloor x/n \rfloor$, we have $ x \geq n\lfloor x/n \rfloor$. Now by Corollary 1.1.3, $ \lfloor x \rfloor \geq n\lfloor x/n \rfloor$, and hence $ \lfloor x \rfloor/n \geq \lfloor x/n \rfloor$. Finally, another application of Corollary 1.1.3 yields $ \lfloor \lfloor x \rfloor/n \rfloor \geq \lfloor x/n \rfloor$.

The next result will used in a variety of inductive proofs pertaining to the bit vectors. (See, for example, the proof of Lemma 2.3.22.)

  (fl-half-int) For all $ n \in \mathbb{Z}$, $ \vert\lfloor n/2\rfloor\vert \leq \vert n\vert$, and if $ n \notin \{0,-1\}$, then $ \vert\lfloor n/2\rfloor\vert < \vert n\vert$.

PROOF: It is clear that equality holds for $ n = 0$ or $ n = -1$. If $ n \geq 1$, then

$\displaystyle \left\vert\lfloor n/2 \rfloor\right\vert = \lfloor n/2 \rfloor \leq n/2 < n = \vert n\vert.
$

If $ n \leq -2$, then

$\displaystyle \left\vert\lfloor n/2 \rfloor\right\vert = -\lfloor n/2 \rfloor < -(n/2 - 1) = -n/2 + 1 \leq -n = \vert n\vert. $

The floor commutes with negation only for integer arguments:

  (minus-fl) For all $ x \in \mathbb{R}$,

$\displaystyle \lfloor -x \rfloor = \left\{\begin{array}{ll}
-\lfloor x \rfloor...
...
-\lfloor x \rfloor - 1 & \mbox{if $x \notin \mathbb{Z}$}. \end{array} \right.$

PROOF: If $ x \in \mathbb{Z}$, then Lemma 1.1.1 implies

$\displaystyle \lfloor -x \rfloor = -x = -\lfloor x \rfloor.$

Otherwise,

$\displaystyle \lfloor x \rfloor < x < \lfloor x \rfloor + 1,$

which implies

$\displaystyle -\lfloor x \rfloor - 1 < -x < -\lfloor x \rfloor,$

and by Definition 1.1.1,

$\displaystyle \lfloor -x \rfloor = -\lfloor x \rfloor - 1.$

When $ x$ is expressed as a ratio of integers, we also have the following unconditional expression for $ \lfloor -x \rfloor$.

  (fl-m-n) If $ m \in \mathbb{Z}$, $ n \in \mathbb{Z}$, and $ n > 0$, then

$\displaystyle \lfloor -m/n \rfloor = - \lfloor (m-1)/n \rfloor - 1.$

PROOF: Suppose first that $ m/n \in \mathbb{Z}$. Then

$\displaystyle \lfloor (m-1)/n \rfloor = \lfloor m/n - 1/n \rfloor = m/n + \lfloor -1/n \rfloor = m/n - 1$

and

$\displaystyle - \lfloor (m-1)/n \rfloor - 1 = -m/n = \lfloor -m/n \rfloor.$

Now suppose $ m/n \notin \mathbb{Z}$. Then $ m/n > \lfloor m/n \rfloor$, which implies $ m > \lfloor m/n \rfloor n$, and hence $ m \geq \lfloor m/n \rfloor n + 1$. Thus, we have

$\displaystyle \lfloor m/n \rfloor \leq (m-1)/n < m/n < \lfloor m/n \rfloor + 1,$

and by Definition 1.1.1, $ \lfloor (m-1)/n \rfloor = \lfloor m/n \rfloor$. Finally, by Lemma 1.1.7,

$\displaystyle \lfloor -m/n \rfloor = - \lfloor m/n \rfloor - 1 = - \lfloor (m-1)/n \rfloor - 1.$

Examples:
$ \lfloor -\frac{6}{5} \rfloor = -\lfloor \frac{6-1}{5} \rfloor - 1 = -\lfloor 1 \rfloor - 1 = -1 - 1 = -2$
$ \lfloor -1 \rfloor = \lfloor -\frac{5}{5} \rfloor = -\lfloor \frac{5-1}{5} \rfloor - 1 = -\lfloor \frac{4}{5} \rfloor - 1 = 0 - 1 = -1$
$ \lfloor -\frac{4}{5} \rfloor = -\lfloor \frac{4-1}{5} \rfloor - 1 = -\lfloor \frac{3}{5} \rfloor - 1 = 0 - 1 = -1$

The ceiling of a real number $ x$ may be characterized as the least integer not exceeded by $ x$. It is defined most conveniently using the floor, as follows.

Definition 1.1.2   (cg) For all $ x \in \mathbb{R}$, $ cg(x) = - \lfloor -x \rfloor$.

Notation: We shall abbreviate $ cg(x)$ as $ \lceil x \rceil$.

The following two essential properties, corresponding to Definition 1.1.1, follow immediately from Definition 1.1.2.

  (cg-def) For all $ x \in \mathbb{R}$, $ \lceil x \rceil \in \mathbb{Z}$ and $ \lceil x \rceil \geq x > \lceil x \rceil - 1.$

PROOF: By Definition 1.1.1, $ \lfloor -x \rfloor \leq -x < \lfloor -x \rfloor + 1$, which leads to $ -\lfloor -x \rfloor \geq x < -\lfloor -x \rfloor - 1$. The lemma now follows from Definition 1.1.2


The next six results correspond to properties of the floor that are listed above.

  (cg-integerp) For all $ x \in \mathbb{R}$, $ \lceil x \rceil = x \Leftrightarrow x \in \mathbb{Z}$.

PROOF: If $ \lceil x \rceil = x$, then $ x \in \mathbb{Z}$ by Lemma 1.1.9. On the other hand, if $ x \in \mathbb{Z}$, then since $ \lceil x \rceil$ is the unique integer in the half-open interval $ (\lceil x \rceil - 1, \lceil x \rceil]$, Lemma 1.1.9 implies $ \lceil x \rceil = x.$ 

  (cg-monotone-linear) If $ x \in \mathbb{R}$, $ y \in \mathbb{R}$, and $ x \leq y$, then $ \lceil x \rceil \leq \lceil y \rceil$.

PROOF: If $ x \leq y$, then Lemma 1.1.9 implies $ x \leq \lceil y \rceil$. By a second application of the same lemma, $ \lceil x \rceil - 1 < x$. Hence, $ \lceil x \rceil - 1 < \lceil y \rceil$, and the result follows from Lemma 1.1.9

  (n>=cg-linear) If $ x \in \mathbb{R}$, $ n \in \mathbb{Z}$, and $ n \geq x$, then $ n \geq \lceil x \rceil$.

PROOF: By Lemmas 1.1.9 and 1.1.11, $ n = \lceil n \rceil \geq \lceil x \rceil$

  (cg+int-rewrite) If $ x \in \mathbb{R}$ and $ n \in \mathbb{Z}$, then $ \lceil x+n \rceil = \lceil x \rceil + n$.

PROOF: Applying Lemma 1.1.9 and shifting by $ n$, we have $ \lceil x \rceil + n \geq x + n > \lceil x \rceil + n - 1$. The result now follows from Lemma 1.1.9

  (cg/int-rewrite)
If $ x \in \mathbb{R}$, $ n \in \mathbb{Z}$, and $ n > 0$, then $ \lceil \lceil x \rceil /n \rceil = \lceil x/n \rceil$.

PROOF: Since $ \lceil x \rceil \geq x$, $ \lceil x \rceil/n \geq x/n$, and by Lemma 1.1.11, $ \lceil \lceil x \rceil/n \rceil \geq \lceil x/n \rceil$. To derive the reverse inequality, note that since $ x/n \leq \lceil x/n \rceil$, we have $ x \leq n\lceil x/n \rceil$. Now by Corollary 1.1.12, $ \lceil x \rceil \leq n\lceil x/n \rceil$, and hence $ \lceil x \rceil/n \leq \lceil x/n \rceil$. Finally, another application of Corollary 1.1.12 yields $ \lceil \lceil x \rceil/n \rceil \leq \lceil x/n \rceil$.


The floor and the ceiling are related as follows.

  (fl-cg) For all $ x \in \mathbb{R}$,

$\displaystyle \lceil x \rceil = \left\{\begin{array}{ll}
\lfloor x \rfloor & \...
...
\lfloor x \rfloor + 1 & \mbox{if $x \notin \mathbb{Z}$}. \end{array} \right.$

PROOF: If $ x \in \mathbb{Z}$, then of course, $ \lceil x \rceil = \lfloor x \rfloor = x$. Otherwise, by Lemma 1.1.1, $ x \neq \lfloor x \rfloor$, and hence Definition 1.1.1 yields $ \lfloor x \rfloor < x < \lfloor x \rfloor + 1$. Rearranging these inequalities, we have $ \lfloor x \rfloor + 1 > x > (\lfloor x \rfloor + 1) - 1$. By Lemma 1.1.9, $ \lceil x \rceil = \lfloor x \rfloor +1$


David Russinoff 2017-08-01