Theorem: Condition for Darboux Integrability

Let $\closedint a b$ be a closed real interval.
Let $f$ be a bounded real function defined on $\closedint a b$.
Then $f$ is Darboux integrable {{iff}}:
:for every $\epsilon \in \R_{>0}$, there exists a finite subdivision $S$ of $\closedint a b$ such that $\map U S - \map L S < \epsilon$
where
:$\map U S$ is the upper Darboux sum of $f$ on $\closedint a b$ {{WRT}} $S$
:$\map L S$ is the lower Darboux sum of $f$ on $\closedint a b$ {{WRT}} $S$

Proof:
=== Necessary Condition ===
Let $f$ be Darboux integrable.
Let $\epsilon \in \R_{>0}$ be given.
It is to be proved that a finite subdivision $S$ of $\closedint a b$ exists such that:
:$\map U S - \map L S < \epsilon$
As $f$ is Darboux integrable:
:$\ds \int_a^b \map f x \rd x$ exists.
By the definition of the Darboux integral:
:the lower Darboux integral $\ds \underline {\int_a^b} \map f x \rd x$ exists.
Thus by the definition of lower Darboux integral:
:$\sup_P \map L P$ exists
where:
:$\map L P$ denotes the lower Darboux sum of $f$ on $\closedint a b$ {{WRT}} the finite subdivision $P$
:$\sup_P \map L P$ denotes the supremum for $\map L P$.
Therefore by Supremum of Subset of Real Numbers is Arbitrarily Close:
:a finite subdivision $S_1$ of $\closedint a b$ exists, satisfying:
::$\sup_P \map L P - \map L {S_1} < \dfrac \epsilon 2$
In a similar way:
By the definition of the Darboux integral:
:the upper Darboux integral $\ds \overline {\int_a^b} \map f x \rd x$ exists.
Thus by the definition of upper Darboux integral:
:$\inf_P \map U P$ exists
where:
:$\map U P$ denotes the upper Darboux sum of $f$ on $\closedint a b$ {{WRT}} the finite subdivision $P$
:$\inf_P \map U P$ denotes the infimum for $\map U P$.
Therefore by Infimum of Subset of Real Numbers is Arbitrarily Close:
:a finite subdivision $S_2$ of $\closedint a b$ exists, satisfying:
::$\map U {S_2} - \inf_P \map U P < \dfrac \epsilon 2$
Now let $S := S_1 \cup S_2$ be defined.
We observe:
:$S$ is either equal to $S_1$ or finer than $S_1$
:$S$ is either equal to $S_2$ or finer than $S_2$
We find:
:$\map L S \ge \map L {S_1}$ by Lower Sum of Refinement
:$\map U S \le \map U {S_2}$ by Upper Sum of Refinement
{{Recall|Darboux Integrable Function|Darboux integrable}}:
:$\ds \overline {\int_a^b} \map f x \rd x = \underline {\int_a^b} \map f x \rd x$
Hence we have:
{{begin-eqn}}
{{eqn | l = \map U S - \map L S
      | o = \le
      | r = \map U {S_2} - \map L S
      | c = as $\map U S \le \map U {S_2}$
}}
{{eqn | o = \le
      | r = \map U {S_2} - \map L {S_1}
      | c = as $\map L S \ge L \map L {S_1}$
}}
{{eqn | r = \map U {S_2} - \overline {\int_a^b} \map f x \rd x + \overline {\int_a^b} \map f x \rd x - \map L {S_1}
}}
{{eqn | r = \map U {S_2} - \overline{\int_a^b} \map f x \rd x + \underline{\int_a^b} \map f x \rd x - \map L {S_1}
      | c = as $\ds \overline {\int_a^b} \map f x \rd x = \underline {\int_a^b} \map f x \rd x$
}}
{{eqn | r = \map U {S_2} - \inf_P \map U P + \sup_P \map L P - \map L {S_1}
      | c = {{Defof|Upper Darboux Integral}} and {{Defof|Lower Darboux Integral}}
}}
{{eqn | o = <
      | r = \frac \epsilon 2 + \sup_P \map L P - \map L {S_1}
      | c = as $\map U {S_2} - \inf_P \map U P < \dfrac \epsilon 2$
}}
{{eqn | o = <
      | r = \frac \epsilon 2 + \frac \epsilon 2
      | c = as $\sup_P \map L P - \map L {S_1} < \dfrac \epsilon 2$
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
{{qed|lemma}}