# Monotone Real Function is Darboux Integrable

## Theorem

Let $\closedint a b$ be a closed real interval, where $a < b$.

Let $f: \closedint a b \to \R$ be a monotone real function.

Then $f$ is Darboux integrable over $\closedint a b$.

## Proof

We consider the case where $f$ is increasing; the case where $f$ is decreasing is handled similarly.

Let $\epsilon \in \R_{>0}$ be a strictly positive real number.

By the Archimedean Principle, there exists a natural number $n$ such that:

$n > \dfrac {\paren {b - a} \paren {\map f b - \map f a} } {\epsilon}$

For $k \in \set {0, 1, 2, \ldots, n}$, define:

$x_k = a + k \dfrac {b - a} n$

Then:

$a = x_0 < x_1 < \cdots < x_n = b$

and hence $P = \set {x_0, x_1, \ldots, x_n}$ is a subdivision of $\closedint a b$.

The lower sum and upper sum of $f$ belonging to the subdivision $P$ are, respectively:

$\displaystyle \map L P = \sum_{k \mathop = 1}^n \map f {x_{k - 1} } \paren {x_k - x_{k - 1} } = \frac {b - a} n \sum_{k \mathop = 1}^n \map f {x_{k - 1} }$
$\displaystyle \map U P = \sum_{k \mathop = 1}^n \map f {x_k} \paren {x_k - x_{k - 1} } = \frac {b - a} n \sum_{k \mathop = 1}^n \map f {x_k}$

Therefore:

 $\displaystyle 0$ $\le$ $\displaystyle \overline {\int_a^b} \map f x \rd x - \underline {\int_a^b} \map f x \rd x$ $\displaystyle$ $\le$ $\displaystyle \map U P - \map L P$ $\displaystyle$ $=$ $\displaystyle \frac {\paren {b - a} \paren {\map f b - \map f a} } n$ $\displaystyle$ $<$ $\displaystyle \epsilon$

Since $\epsilon \in \R_{>0}$ is arbitrary, the result follows.

$\blacksquare$
{"ft_lang_label":"__label__en","ft_lang_prob":0.57437813,"math_prob":1.000006,"size":1721,"snap":"2020-24-2020-29","text_gpt3_token_len":638,"char_repetition_ratio":0.1566686,"word_repetition_ratio":0.20754717,"special_character_ratio":0.39976758,"punctuation_ratio":0.10280374,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":1.0000098,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-07-07T06:09:06Z\",\"WARC-Record-ID\":\"<urn:uuid:4712e4e9-c51c-4642-8d6b-c33697b97b97>\",\"Content-Length\":\"39391\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:e4fce11e-4368-42f1-9b2a-722f668d451d>\",\"WARC-Concurrent-To\":\"<urn:uuid:b6dbff89-1d14-412e-a6f7-0e56f9d022b1>\",\"WARC-IP-Address\":\"172.67.198.93\",\"WARC-Target-URI\":\"https://proofwiki.org/wiki/Monotone_Real_Function_is_Darboux_Integrable\",\"WARC-Payload-Digest\":\"sha1:DVUN7DJ74EJA5H2UXKI2M63U6AKCWBT3\",\"WARC-Block-Digest\":\"sha1:NODSQJ4E3YC5W7YFKTAHFI44EX2XYYYQ\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-29/CC-MAIN-2020-29_segments_1593655891654.18_warc_CC-MAIN-20200707044954-20200707074954-00156.warc.gz\"}"}