Proof of Darboux Sums Bound the Lebesgue Integral on a Closed Interval

Step 1: the measure space and the shift. Write $\mathcal{B}'=\mathcal{B}_{[a,b]}$ and $\lambda'=\lambda_{[a,b]}$. By Lebesgue Measure on the Real Line: Existence, Lengths of Intervals and Uniqueness (iv), Lebesgue Measure on the Real Line: Existence, Lengths of Intervals and Uniqueness (i) and Integrals of Functions over a Measurable Subset (i), $\lambda'$ is a measure on $([a,b],\mathcal{B}')$, and as $[a,b]\in\mathcal{B}'$,

$$\lambda'([a,b])=\lambda([a,b])=b-a<\infty$$

(Lebesgue Measure on the Real Line: Existence, Lengths of Intervals and Uniqueness (i), Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (ii)), so $\lambda'$ is finite. Also $B\ge|f(a)|\ge0$ (Rules of Arithmetic and Order in an Ordered Field (x)). By Bounded Measurable Functions on a Finite Measure Space Are Integrable (i), $f\in\mathcal{L}^{1}(\lambda')$; by Bounded Measurable Functions on a Finite Measure Space Are Integrable (ii), the function $g=f+B$ lies in $\mathcal{M}^{+}$ and in $\mathcal{L}^{1}(\lambda')$, and both its integrals are the real number

$$J=\int g\,d\lambda'=\int f\,d\lambda'+B(b-a).$$

Step 2: values on the cells. Let $P$ be a partition of $[a,b]$, let $n$, the listing $a=x_{1}<\dots<x_{n+1}=b$ and the cells $E_{i}=(x_{i},x_{i+1})$, $i\in[n]$, be as in Step Functions on a Partition of a Closed Interval as Simple Functions, and let $M,m:[n]\to\mathbb{R}$ and the sets $S_{i}$ be as in Upper and Lower Darboux Sums of a Bounded Function on a Partition (i). For $t\in E_{i}$, $t\in[x_{i},x_{i+1}]$, so $f(t)\in S_{i}$ and $m(i)\le f(t)\le M(i)$; every element of $S_{i}$ is $\ge-B$, so $m(i)\ge-B$; and $M(i)\ge f(x_{i})\ge-B$ (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (i), Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv), Rules of Arithmetic and Order in an Ordered Field (x)). Let $\alpha,\beta:[n]\to\mathbb{R}$ be the functions with

$$\alpha_{i}=m(i)+B,\qquad\beta_{i}=M(i)+B\qquad(i\in[n]),$$

the pointwise sums of $m$ and $M$ with the constant function $B$ (Pointwise Operations on Real-Valued Maps (i), Pointwise Operations on Real-Valued Maps (ii)); then $\alpha_{i}\ge0$ and $\beta_{i}\ge0$ (Rules of Arithmetic and Order in an Ordered Field (iv)).

Step 3: step functions below and above $g$. By Step Functions on a Partition of a Closed Interval as Simple Functions (ii) there are functions $s,\sigma:[a,b]\to\mathbb{R}$ with $s=\alpha_{i}$ and $\sigma=\beta_{i}$ on each $E_{i}$, and $s=0$ and $\sigma=2B$ on $P$. Both have values $\ge0$ ($2B\ge0$ as $B\ge0$, Rules of Arithmetic and Order in an Ordered Field (iv)), so by Step Functions on a Partition of a Closed Interval as Simple Functions (iii) they are nonnegative simple functions on $([a,b],\mathcal{B}')$ with

$$I_{\lambda'}(s)=\sum_{i=1}^{n}\alpha_{i}\,(x_{i+1}-x_{i}),\qquad I_{\lambda'}(\sigma)=\sum_{i=1}^{n}\beta_{i}\,(x_{i+1}-x_{i}).$$

We have $s\le g\le\sigma$ on $[a,b]$: on $E_{i}$ by Step 2 and Rules of Arithmetic and Order in an Ordered Field (iv); on $P$ as $0\le g$ and $g=f+B\le2B$; and these sets cover $[a,b]$ by Step Functions on a Partition of a Closed Interval as Simple Functions (i). The order of $[0,\infty]$ is that of $\mathbb{R}$ on reals (The Extended Real Line, Its Order, and [0,∞] (iii)), so by Basic Properties of the Integral of Nonnegative Measurable Maps (i) and Basic Properties of the Integral of Nonnegative Measurable Maps (iii),

$$I_{\lambda'}(s)\le J\le I_{\lambda'}(\sigma).$$

Step 4: Darboux sums. With $\Delta_{i}=x_{i+1}-x_{i}$ and $\sum_{i=1}^{n}\Delta_{i}=b-a$ (The Increasing Listing of a Partition: Endpoints, Lengths, Covering, Unions, Inserting a Point, Concatenation and Uniform Partitions (iii)),

$$\sum_{i=1}^{n}\alpha_{i}\Delta_{i}=\sum_{i=1}^{n}m(i)\Delta_{i}+B\sum_{i=1}^{n}\Delta_{i}=L(f,P)+B(b-a),\qquad\sum_{i=1}^{n}\beta_{i}\Delta_{i}=U(f,P)+B(b-a)$$

(Upper and Lower Darboux Sums of a Bounded Function on a Partition (iii), Upper and Lower Darboux Sums of a Bounded Function on a Partition (ii), Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (iv), Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (v), Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality (i), Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (v)). By Steps 1 and 3,

$$L(f,P)+B(b-a)\le\int f\,d\lambda'+B(b-a)\le U(f,P)+B(b-a),$$

and subtracting $B(b-a)$ gives $L(f,P)\le\int f\,d\lambda'\le U(f,P)$ (Rules of Arithmetic and Order in an Ordered Field (iv)).