Partial Proof of the Floor Integration Method

We will prove the correctness of this algorithm by a sequence of definitions and propositions.

First we define $f^+(x)$ and $f^-(x)$ as shorthand for the left and right hand derivatives of some function $f$ at $x$.

Now we will define a special operator that will serve as a means of formalizing the questions algorithm.

> Definition: We define the implied derivative to be an operator that takes in a function $f$ and returns a set of functions as shown by the expression $f^{\to} = \{g | \forall_{x \in R} (g(x) = f^+(x)) \lor (g(x) = f^-(x))\}$.

We will define a piecewise constant function via the following:

> A piecewise constant function $g$ is any function that has a left and right hand derivative of $0$ everywhere.

We now need to prove that any result of the algorithm has an implied derivative equal to the original function. We define such a function to be an implied antiderivative.