Floor function

Stub grade: B

This page is a stub

This page is a stub, so it contains little or minimal information and is on a to-do list for being expanded.The message provided is:

Research consensus and handling negative numbers

$\newcommand{\Floor}[1]{ {\text{Floor}{\left({#1}\right)} } }$

Definition

For $x\in\mathbb{R}_{\ge 0}$ there is no variation on the meaning of the floor function, however for negative numbers there are varying conventions.

Non-negative

Defined as follows:

• $\text{Floor}:\mathbb{R}_{\ge 0}\rightarrow\mathbb{N}_0$ by $\text{Floor}:x\mapsto$$\text{Max}$$(T_x)$ where $T_x:\eq\big\{n\in\mathbb{N}_0\ \big\vert\ n\le x\big\}\subseteq\mathbb{N}_0\subseteq\mathbb{R}_{\ge 0}$ - note that the maximum element is defined as $T_x$ is always finite.
• This has the property that $x\le\Floor{x}$.

Negative numbers

Researching this opened my eyes to a massive dispute.... consensus seems to be that $x\le \Floor{x}$ is maintained, rounding is a separate and massive issue!

Future work

Properties

1. $\forall n\in\mathbb{N}_0\subseteq\mathbb{R}_{\ge 0}\big[\Floor{n}\eq n\big]$, or $\text{Floor}\vert_{\mathbb{N}_0}\eq\text{Id}_{\mathbb{N}_0}$ - its restriction to $\mathbb{N}_0$ is the identity map on $\mathbb{N}_0$
2. $\forall x,y\in\mathbb{R}_{\ge 0}\big[(x\le y)\implies\big(\Floor{x}\le\Floor{y}\big)\big]$ - monotonicity
3. $\forall x\in\mathbb{R}_{\ge 0}\exists\epsilon\in[0,1)\subseteq\mathbb{R}\big[x\eq\Floor{x}+\epsilon\big]$ - the characteristic property of the floor function

I believe that $3\implies 1$ and $3\implies 2$ might be possible, so these are perhaps in the wrong order. I just wanted to write down some notes before they get put into the massive stack of unfiled paper

This is a corollary to property 3 coupled with the definition (domain and co domain) of the floor function:

• $\forall x\in\mathbb{R}_{\ge 0}\big[\Floor{x}\le x<\Floor{x}+1\big]$

This statement is a critical part of finding Mdms and was used in:

• Mdm of a discrete distribution lemma
  • Which at the time of writing (Alec (talk) 21:20, 21 January 2018 (UTC)) only exists as notes: Notes:Mdm of a discrete distribution lemma